Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison BAlgbra.agda @ 329:5544f4921a44
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 12:32:09 +0900 |
parents | d9d3654baee1 |
children | 12071f79f3cf |
comparison
equal
deleted
inserted
replaced
328:72f3e3b44c27 | 329:5544f4921a44 |
---|---|
22 | 22 |
23 open _∧_ | 23 open _∧_ |
24 open _∨_ | 24 open _∨_ |
25 open Bool | 25 open Bool |
26 | 26 |
27 _∩_ : ( A B : OD ) → OD | 27 _∩_ : ( A B : HOD ) → HOD |
28 A ∩ B = record { def = λ x → def A x ∧ def B x } | 28 A ∩ B = record { def = λ x → def A x ∧ def B x } |
29 | 29 |
30 _∪_ : ( A B : OD ) → OD | 30 _∪_ : ( A B : HOD ) → HOD |
31 A ∪ B = record { def = λ x → def A x ∨ def B x } | 31 A ∪ B = record { def = λ x → def A x ∨ def B x } |
32 | 32 |
33 _\_ : ( A B : OD ) → OD | 33 _\_ : ( A B : HOD ) → HOD |
34 A \ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } | 34 A \ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } |
35 | 35 |
36 ∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B ) | 36 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) |
37 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 37 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
38 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x | 38 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x |
39 lemma1 {x} lt = lemma3 lt where | 39 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) ) | 40 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) |
41 lemma4 {y} z with proj1 z | 41 lemma4 {y} z with proj1 z |
47 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A | 47 lemma2 {x} (case1 A∋x) = subst (λ k → def (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})) | 48 (record { proj1 = case1 refl ; proj2 = subst (λ k → def 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 | 49 lemma2 {x} (case2 B∋x) = subst (λ k → def (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})) | 50 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) |
51 | 51 |
52 ∩-Select : { A B : OD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) | 52 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) |
53 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 53 ∩-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 | 54 lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x |
55 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } | 55 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } |
56 lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x | 56 lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x |
57 lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = | 57 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) } } | 58 record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } } |
59 | 59 |
60 dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) | 60 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 | 61 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 | 62 lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x |
63 lemma1 {x} lt with proj2 lt | 63 lemma1 {x} lt with proj2 lt |
64 lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } ) | 64 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 } ) | 65 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 | 66 lemma2 : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x |
67 lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } | 67 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 ) } | 68 lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } |
69 | 69 |
70 dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) | 70 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 | 71 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 | 72 lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x |
73 lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp } | 73 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) } | 74 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 | 75 lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x |