Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison BAlgbra.agda @ 331:12071f79f3cf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOD done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 16:56:21 +0900
parents 5544f4921a44
children 2a8a51375e49
comparison
equal deleted inserted replaced
330:0faa7120e4b5 331:12071f79f3cf
17 17
18 open inOrdinal O 18 open inOrdinal O
19 open OD O 19 open OD O
20 open OD.OD 20 open OD.OD
21 open ODAxiom odAxiom 21 open ODAxiom odAxiom
22 open HOD
22 23
23 open _∧_ 24 open _∧_
24 open _∨_ 25 open _∨_
25 open Bool 26 open Bool
26 27
27 _∩_ : ( A B : HOD ) → HOD 28 _∩_ : ( A B : HOD ) → HOD
28 A ∩ B = record { def = λ x → def A x ∧ def B x } 29 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
30 odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
29 31
30 _∪_ : ( A B : HOD ) → HOD 32 _∪_ : ( A B : HOD ) → HOD
31 A ∪ B = record { def = λ x → def A x ∨ def B x } 33 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
34 odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
35 lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
36 lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
37 lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
32 38
33 _＼_ : ( A B : HOD ) → HOD 39 _＼_ : ( A B : HOD ) → HOD
34 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } 40 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
35 41
36 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) 42 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
37 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 43 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
38 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x 44 lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
39 lemma1 {x} lt = lemma3 lt where 45 lemma1 {x} lt = lemma3 lt where
40 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) 46 lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (ord→od y) x → ¬ (¬ ( odef A x ∨ odef B x) )
41 lemma4 {y} z with proj1 z 47 lemma4 {y} z with proj1 z
42 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) ) 48 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) oiso (proj2 z)) )
43 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) ) 49 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) oiso (proj2 z)) )
44 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x 50 lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (ord→od u) x) → ⊥) → odef (A ∪ B) x
45 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice 51 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice
46 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x 52 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
47 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A 53 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
48 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x})) 54 (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x}))
49 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B 55 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
50 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) 56 (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x}))
51 57
52 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) 58 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B )
53 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 59 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
54 lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x 60 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
55 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } 61 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) }
56 lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x 62 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
57 lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = 63 lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
58 record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } } 64 record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
59 65
60 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) 66 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r )
61 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 67 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
62 lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x 68 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
63 lemma1 {x} lt with proj2 lt 69 lemma1 {x} lt with proj2 lt
64 lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } ) 70 lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } )
65 lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } ) 71 lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } )
66 lemma2 : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x 72 lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
67 lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } 73 lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) }
68 lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } 74 lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) }
69 75
70 dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) 76 dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r )
71 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 77 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
72 lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x 78 lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
73 lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp } 79 lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
74 lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) } 80 lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) }
75 lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x 81 lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
76 lemma2 {x} lt with proj1 lt | proj2 lt 82 lemma2 {x} lt with proj1 lt | proj2 lt
77 lemma2 {x} lt | case1 cp | _ = case1 cp 83 lemma2 {x} lt | case1 cp | _ = case1 cp
78 lemma2 {x} lt | _ | case1 cp = case1 cp 84 lemma2 {x} lt | _ | case1 cp = case1 cp
79 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } ) 85 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } )
80 86