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

changeset 501:5a166a832472

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 Tue, 12 Apr 2022 15:45:56 +0900
parents a97a1f1e27fa
children 3c03f5bf9e16
files src/zorn.agda
diffstat 1 files changed, 23 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Apr 12 14:17:00 2022 +0900
+++ b/src/zorn.agda	Tue Apr 12 15:45:56 2022 +0900
@@ -124,41 +124,42 @@
 
 -- there is a y, & y > & x
 
-record Sup> {A : HOD} (x : Element A) : Set (suc n) where
+record OSup> (A : HOD) {x : Ordinal} (ax : A ∋ * x) : Set n where
    field
-      y : Element A
-      y>x : IChainSet x ∋ elm y → & (elm x) o< & (elm y)
+      y : Ordinal
+      icy : odef (IChainSet {A} (me ax)) y 
+      y>x : x o< y
 
 -- finite IChain
 
-record InFiniteIChain {A : HOD} (x : Element A) (z : Ordinal) : Set (suc n) where
+record InFiniteIChain (A : HOD) {x : Ordinal}  (ax : A ∋ * x) : Set n where
    field
-      ny : (y : Element A ) → & (elm y) o< z → Element A
-      y>x : {y : Element A} → (lt : & (elm y) o< z )→ IChainSet x ∋ elm y → elm y < elm (ny y lt )
+      chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< x
+      c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
+          → OSup> (IChainSet {A} (me ax)) (d→∋ (IChainSet {A} (me ax)) cy)
+      
+record IsIFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
+   field
+      icy : odef (IChainSet {A} (me ax)) y  
+      c-finite : ¬ OSup> (IChainSet {A} (me ax)) (d→∋ (IChainSet {A} (me ax)) icy)
       
 Zorn-lemma-case : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
-    → (x : Element A) → Sup> x ∨ Dec ( InFiniteIChain x (& A))
+    → (x : Element A) → OSup> A (d→∋ A (is-elm x)) ∨ Maximal A ∨ InFiniteIChain A (d→∋ A (is-elm x))
 Zorn-lemma-case {A}  0<A PO x = zc2 where
     Gtx : HOD
     Gtx = record { od = record { def = λ y → odef ( IChainSet x ) y ∧  ( & (elm x) o< y ) } ; odmax = & A
-        ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 (proj1 lt))))  }
-    zc2 :  Sup> x ∨ Dec (InFiniteIChain x (& A))
+        ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A (proj1 (proj1 lt))))  }
+    HG : HOD
+    HG = record { od = record { def = λ y → odef A y ∧ IsIFC A (d→∋ A (is-elm x) ) y } ; odmax = & A
+        ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A  (proj1 lt) ))  }
+    zc2 :  OSup> A (d→∋ A (is-elm x))  ∨ Maximal A ∨ InFiniteIChain A  (d→∋ A (is-elm x))
     zc2 with  is-o∅ (& Gtx)
-    ... | no not = case1 record { y = record { elm = ODC.minimal O Gtx (λ eq → not (=od∅→≡o∅ eq) ); is-elm = {!!} }  ; y>x = {!!} }
-    ... | yes nogt = case2 {!!} where
-        zc3 : {y : Element A} → IChainSet x ∋ elm y → ¬ (& (elm x) o< & (elm y))
-        zc3 = {!!}
-        zcind : (z : Ordinal ) → ((y : Ordinal) → y o< z → Dec (InFiniteIChain x y ) ) → Dec (InFiniteIChain x z)
-        zcind z prev with trio< (& A) z
-        ... | tri< a ¬b ¬c = {!!}
-        ... | tri≈ ¬a b ¬c = {!!}
-        ... | tri> ¬a ¬b c with ODC.∋-p O A (* z)
-        ... | no nota = {!!}
-        ... | yes az = {!!}
-        zc4 : Dec (InFiniteIChain x (& A))
-        zc4 = TransFinite zcind (& A)
+    ... | no nogt = case1 {!!}
+    ... | yes nogt with is-o∅ (& HG)
+    ... | no  nohg = case2 (case1 {!!} )
+    ... | yes  nohg = case2 (case2 {!!} )
 
 
 Zorn-lemma : { A : HOD }