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

changeset 471:2b048496cb21

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 Mon, 28 Mar 2022 15:03:50 +0900
parents f57f92c7c874
children 66a7d30d125a
files src/ODC.agda
diffstat 1 files changed, 33 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODC.agda	Mon Mar 28 08:51:19 2022 +0900
+++ b/src/ODC.agda	Mon Mar 28 15:03:50 2022 +0900
@@ -148,10 +148,11 @@
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
+    → ( {a b c : HOD} → a < b → b < c → a < c )
     → PartialOrderSet A _<_
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B  _<_  )
     → Maximal A _<_ 
-Zorn-lemma {A} {_<_} 0<A PO supP = zorn00 where
+Zorn-lemma {A} {_<_} 0<A TR PO supP = zorn00 where
      HasMaximal : HOD
      HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
@@ -163,21 +164,44 @@
          z03 = c<→o< (SUP.A∋maximal sp)
          z02 :  (x : HOD) → ZChain.B z ∋ x → SUP.sup sp < x → ⊥
          z02 x xe s<x = ( z01 (incl (ZChain.B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x )
-     ind :  (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
+     ind :  HasMaximal =h= od∅
+         → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
-     ind x prev with Oprev-p x
-     ... | yes _ = {!!}
-     ind x prev | no ¬ox with trio< (& A) x
+     ind nomx x prev with Oprev-p x
+     ... | yes op with ∋-p A (* x)
+     ... | no ¬Ax = record  { B = ZChain.B zc1 ; B⊆A =  ZChain.B⊆A  zc1 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = z04 } where
+          px = Oprev.oprev op
+          zc1 : ZChain A px _<_
+          zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
+          z05 : SUP A (ZChain.B zc1) _<_ 
+          z05 = supP (ZChain.B zc1) (ZChain.B⊆A zc1) (ZChain.total zc1)
+          z06 :  (sup : HOD) (as : A ∋ sup) → & sup o< x → HOD
+          z06 sup as s<x with trio< (& sup) x
+          ... | tri≈ ¬a b ¬c = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans b (sym &iso)) as) )  
+          ... | tri> ¬a ¬b c = ⊥-elim (¬a s<x)
+          ... | tri< a ¬b ¬c with osuc-≡< (subst (λ k → (& sup) o< k ) (sym (Oprev.oprev=x op)) a )
+          ... | case2 lt = ZChain.fb zc1 as
+          ... | case1 eq = {!!}
+          z04 :  (sup : HOD) (as : A ∋ sup) → & sup o< x → sup < ZChain.fb zc1 as
+          z04 sup as s<x with trio< (& sup) x
+          ... | tri≈ ¬a b ¬c = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans b (sym &iso)) as) )  
+          ... | tri> ¬a ¬b c = ⊥-elim (¬a s<x)
+          ... | tri< a ¬b ¬c with osuc-≡< (subst (λ k → (& sup) o< k ) (sym (Oprev.oprev=x op)) a )
+          ... | case2 lt = ZChain.¬x≤sup zc1 _ as lt
+          ... | case1 eq = ?
+     ... | yes Ax = {!!}
+     -- ... | no ¬Ax = record { B = B (prev B) ; B⊆A = {!!} ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} }
+     ind nomx x prev | no ¬ox with trio< (& A) x
      ... | tri< a ¬b ¬c = {!!}
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b c = {!!}
      zorn00 : Maximal A _<_
      zorn00 with is-o∅ ( & HasMaximal )
      ... | no not = record { maximal = minimal HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}; ¬maximal<x  = {!!} }
-     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A)) ( supP B (ZChain.B⊆A (z (& A))) (ZChain.total (z (& A)))) ) where
-         z : (x : Ordinal) → ZChain A x _<_ 
-         z = TransFinite ind 
-         B = ZChain.B (z (& A))
+     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A) (≡o∅→=od∅ ¬Maximal)) ( supP B (ZChain.B⊆A (z (& A) (≡o∅→=od∅ ¬Maximal))) (ZChain.total (z (& A) (≡o∅→=od∅ ¬Maximal))) )) where
+         z : (x : Ordinal) → HasMaximal =h= od∅  → ZChain A x _<_ 
+         z x nomx = TransFinite (ind nomx) x
+         B = ZChain.B (z (& A) (≡o∅→=od∅ ¬Maximal)  )
 
 open import zfc