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

changeset 326:feeba7fd499a

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 Sun, 05 Jul 2020 03:45:41 +0900
parents 1a54dbe1ea4c
children cde56f704eac
files OD.agda Ordinals.agda
diffstat 2 files changed, 12 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Sat Jul 04 22:48:49 2020 +0900
+++ b/OD.agda	Sun Jul 05 03:45:41 2020 +0900
@@ -330,7 +330,9 @@
         lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x))   ))
         lemma3 {x} = od⊆→o≤ lemma1
         lemma4 : {x : HOD} → od→ord (u x) o< osuc (osuc (od→ord x))
-        lemma4 {x} = ordtrans (<odmax (x , x) {!!}) {!!}
+        lemma4 {x} = ordtrans (<odmax (u x , u x) (case2 refl)) 
+           (subst (λ k → k o< osuc (osuc (od→ord x))) (omax≡ _ _ refl) ( -- odmax (u x , u x) o< osuc (osuc (od→ord x))
+            osucc {!!} )) -- osuc (od→ord (u x)) o<  osuc (osuc (od→ord x))
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
         lemma {y} = TransFinite {λ x → infinite-d x → x o<  next o∅ } ind y where
            ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅))  →
--- a/Ordinals.agda	Sat Jul 04 22:48:49 2020 +0900
+++ b/Ordinals.agda	Sun Jul 05 03:45:41 2020 +0900
@@ -111,7 +111,7 @@
         proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
 
         _o≤_ :  Ordinal → Ordinal → Set  n
-        a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+        a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
 
 
         xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
@@ -183,11 +183,14 @@
 
         open _∧_
 
+        o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
+        o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
         OrdTrans :  Transitive  _o≤_
-        OrdTrans (case1 refl) (case1 refl) = case1 refl
-        OrdTrans (case1 refl) (case2 lt2) = case2 lt2
-        OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-        OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
+        OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
+        OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
+        OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b  b<c) <-osuc
 
         OrdPreorder :   Preorder n n n
         OrdPreorder  = record { Carrier = Ordinal
@@ -195,7 +198,7 @@
            ; _∼_   = _o≤_
            ; isPreorder   = record {
                 isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-                ; reflexive     = case1 
+                ; reflexive     = o≤-refl
                 ; trans         = OrdTrans 
              }
          }