|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
1124
|
3 module BAlgebra {n : Level } (O : Ordinals {n}) where
|
|
431
|
4
|
|
|
5 open import zf
|
|
|
6 open import logic
|
|
|
7 import OrdUtil
|
|
|
8 import OD
|
|
|
9 import ODUtil
|
|
|
10 import ODC
|
|
|
11
|
|
|
12 open import Relation.Nullary
|
|
|
13 open import Relation.Binary
|
|
|
14 open import Data.Empty
|
|
|
15 open import Relation.Binary
|
|
|
16 open import Relation.Binary.Core
|
|
|
17 open import Relation.Binary.PropositionalEquality
|
|
|
18 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )
|
|
|
19
|
|
|
20 open inOrdinal O
|
|
|
21 open Ordinals.Ordinals O
|
|
|
22 open Ordinals.IsOrdinals isOrdinal
|
|
|
23 open Ordinals.IsNext isNext
|
|
|
24 open OrdUtil O
|
|
|
25 open ODUtil O
|
|
|
26
|
|
|
27 open OD O
|
|
|
28 open OD.OD
|
|
|
29 open ODAxiom odAxiom
|
|
|
30 open HOD
|
|
|
31
|
|
|
32 open _∧_
|
|
|
33 open _∨_
|
|
|
34 open Bool
|
|
|
35
|
|
|
36 --_∩_ : ( A B : HOD ) → HOD
|
|
|
37 --A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
|
|
|
38 -- odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
|
|
|
39
|
|
450
|
40 ∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
|
|
|
41 ∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
|
|
|
42
|
|
431
|
43 _∪_ : ( A B : HOD ) → HOD
|
|
|
44 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
|
|
|
45 odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
|
|
|
46 lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
|
|
|
47 lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
|
|
|
48 lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
|
|
|
49
|
|
|
50 _＼_ : ( A B : HOD ) → HOD
|
|
|
51 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
|
|
|
52
|
|
451
|
53 ¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
|
|
|
54 ¬∅∋ {x} = ¬x<0
|
|
|
55
|
|
1123
|
56 L＼L=0 : { L : HOD } → L ＼ L ≡ od∅
|
|
|
57 L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← = lem1 } ) where
|
|
|
58 lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
|
|
|
59 lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx)
|
|
|
60 lem1 : {x : Ordinal} → odef od∅ x → odef (L ＼ L) x
|
|
|
61 lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
|
|
|
62
|
|
451
|
63 [a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
|
|
|
64 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
|
|
|
65 ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
|
|
|
66
|
|
480
|
67 U-F=∅→F⊆U : {F U : HOD} → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U
|
|
1096
|
68 U-F=∅→F⊆U {F} {U} not = gt02 where
|
|
480
|
69 gt02 : { x : Ordinal } → odef F x → odef U x
|
|
|
70 gt02 {x} fx with ODC.∋-p O U (* x)
|
|
|
71 ... | yes y = subst (λ k → odef U k ) &iso y
|
|
|
72 ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ )
|
|
|
73
|
|
431
|
74 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
|
|
|
75 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
|
|
|
76 lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
|
|
1096
|
77 lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) (sym *iso) (sym *iso) abo )
|
|
|
78 ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin
|
|
|
79 * owner ≡⟨ cong (*) (sym a=o) ⟩
|
|
|
80 * (& A) ≡⟨ *iso ⟩
|
|
|
81 A ∎ ) ox ) where open ≡-Reasoning
|
|
|
82 ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) *iso ) ox)
|
|
431
|
83 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
|
|
|
84 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A
|
|
|
85 ⟪ case1 refl , d→∋ A A∋x ⟫ )
|
|
|
86 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B
|
|
|
87 ⟪ case2 refl , d→∋ B B∋x ⟫ )
|
|
|
88
|
|
|
89 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B )
|
|
|
90 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
|
|
|
91 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
|
|
|
92 lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫
|
|
|
93 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
|
|
|
94 lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫
|
|
|
95
|
|
|
96 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r )
|
|
|
97 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
|
|
|
98 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
|
|
|
99 lemma1 {x} lt with proj2 lt
|
|
|
100 lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫
|
|
|
101 lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫
|
|
|
102 lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
|
|
|
103 lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫
|
|
|
104 lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫
|
|
|
105
|
|
|
106 dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r )
|
|
|
107 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
|
|
|
108 lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
|
|
|
109 lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫
|
|
|
110 lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫
|
|
|
111 lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
|
|
|
112 lemma2 {x} lt with proj1 lt | proj2 lt
|
|
|
113 lemma2 {x} lt | case1 cp | _ = case1 cp
|
|
|
114 lemma2 {x} lt | _ | case1 cp = case1 cp
|
|
|
115 lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫
|
|
|
116
|
|
|
117 record IsBooleanAlgebra ( L : Set n)
|
|
|
118 ( b1 : L )
|
|
|
119 ( b0 : L )
|
|
|
120 ( -_ : L → L )
|
|
|
121 ( _+_ : L → L → L )
|
|
|
122 ( _x_ : L → L → L ) : Set (suc n) where
|
|
|
123 field
|
|
|
124 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
|
|
|
125 x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c
|
|
|
126 +-sym : {a b : L } → a + b ≡ b + a
|
|
|
127 -sym : {a b : L } → a x b ≡ b x a
|
|
|
128 +-aab : {a b : L } → a + ( a x b ) ≡ a
|
|
|
129 x-aab : {a b : L } → a x ( a + b ) ≡ a
|
|
|
130 +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c )
|
|
|
131 x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c )
|
|
|
132 a+0 : {a : L } → a + b0 ≡ a
|
|
|
133 ax1 : {a : L } → a x b1 ≡ a
|
|
|
134 a+-a1 : {a : L } → a + ( - a ) ≡ b1
|
|
|
135 ax-a0 : {a : L } → a x ( - a ) ≡ b0
|
|
|
136
|
|
|
137 record BooleanAlgebra ( L : Set n) : Set (suc n) where
|
|
|
138 field
|
|
|
139 b1 : L
|
|
|
140 b0 : L
|
|
|
141 -_ : L → L
|
|
|
142 _+_ : L → L → L
|
|
|
143 _x_ : L → L → L
|
|
|
144 isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_
|
|
|
145
|
