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

changeset 1282:dc5aaf39f27d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Apr 2023 15:32:29 +0900
parents 437e48221ed5
children f4dac8be0a01
files src/BAlgebra.agda
diffstat 1 files changed, 21 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgebra.agda	Thu Apr 06 14:04:35 2023 +0900
+++ b/src/BAlgebra.agda	Thu Apr 06 15:32:29 2023 +0900
@@ -137,7 +137,7 @@
        +-assoc : {a b c : L } → (a + ( b + c )) == ((a + b) + c)
        x-assoc : {a b c : L } → (a x ( b x c )) == ((a x b) x c)
        +-sym : {a b : L } → (a + b) == (b + a)
-       -sym : {a b : L } → (a x b)  == (b x a)
+       x-sym : {a b : L } → (a x b)  == (b x a)
        +-aab : {a b : L } → (a + ( a x b )) == a
        x-aab : {a b : L } → (a x ( a + b )) == a
        +-dist : {a b c : L } → (a + ( b x c )) == (( a + b ) x ( a + c ))
@@ -171,18 +171,19 @@
   ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt))  ⟧ 
    ; isBooleanAlgebra = record {
        +-assoc = λ {a} {b} {c} → ==→o≡ record { eq→ = ba01 a b c ; eq← = ba02 a b c  }
-     ; x-assoc = λ {a} {b} {c} → ==→o≡ record { eq→ = λ lt → ⟪ ⟪ proj1 lt  , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt)  ⟫ 
-                                              ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt)  , proj2 lt ⟫ ⟫ } 
-     ; +-sym = ?
-     ; -sym = λ {a} {b} → ==→o≡ record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫  }
+     ; x-assoc = λ {a} {b} {c} → ==→o≡ 
+        record { eq→ = λ lt → ⟪ ⟪ proj1 lt  , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt)  ⟫ 
+               ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt)  , proj2 lt ⟫ ⟫ } 
+     ; +-sym = λ {a} {b} → ==→o≡ record { eq→ = λ {x} lt → ba05 {hod a} {hod b} lt  ; eq← = ba05 {hod b} {hod a} }
+     ; x-sym = λ {a} {b} → ==→o≡ record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫  }
      ; +-aab = λ {a} {b} → ==→o≡ record { eq→ = ba03 a b ; eq← = case1  }
      ; x-aab = λ {a} {b} → ==→o≡ record { eq→ = proj1 ; eq← = λ ax →  ⟪ ax , case1 ax ⟫ }
      ; +-dist = dist-ord2
      ; x-dist = dist-ord
      ; a+0 = λ {a} → ==→o≡ record { eq→ = ba04 (hod a) ; eq← = case1 }
      ; ax1 = λ {a} → ==→o≡ record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , x⊆P a ax ⟫ }
-     ; a+-a1 = λ {a} → ==→o≡ record { eq→ = ? ; eq← = ? }
-     ; ax-a0 =  λ {a} → ==→o≡ record { eq→ = ? ; eq← = λ lt → ⊥-elim (¬x<0 lt) }
+     ; a+-a1 = λ {a} → ==→o≡ record { eq→ = ba06 a ; eq← = ba07 a }
+     ; ax-a0 =  λ {a} → ==→o≡ record { eq→ = ba08 a ; eq← = λ lt → ⊥-elim (¬x<0 lt) }
        } } where
      ba00 : (x y : PowerP P ) →  (hod x ∪ hod y) ⊆ P
      ba00 x y (case1 px) = x⊆P x px
@@ -204,3 +205,16 @@
      ba04 : (a : HOD) →  {x : Ordinal} → odef a x ∨ odef od∅ x → odef a x
      ba04 a (case1 ax) = ax
      ba04 a (case2 x) = ⊥-elim (¬x<0 x)
+     ba05 : {a b : HOD} {x : Ordinal} →  odef a x ∨ odef b x → odef b x ∨ odef a x
+     ba05 (case1 x) = case2 x
+     ba05 (case2 x) = case1 x
+     ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P ＼ hod a) x → OD.def (od P) x
+     ba06 a {x} (case1 ax) = x⊆P a ax
+     ba06 a {x} (case2 nax) = proj1 nax
+     ba07 : (a : PowerP P ) → { x : Ordinal} → OD.def (od P) x → odef (hod a) x ∨ odef (P ＼ hod a) x 
+     ba07 a {x} px with ODC.∋-p O (hod a) (* x)
+     ... | yes y = case1 (subst (λ k → odef (hod a) k) &iso y)
+     ... | no n = case2 ⟪ px , subst (λ k → ¬ odef (hod a) k) &iso n ⟫
+     ba08 : (a : PowerP P) → {x : Ordinal} → OD.def (od (hod a ∩ (P ＼ hod a))) x → OD.def (od od∅) x
+     ba08 a {x} ⟪ ax , ⟪ px , nax ⟫ ⟫ = ⊥-elim ( nax ax )
+