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

diff ordinal.agda @ 334:ba3ebb9a16c6 release

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 16:59:13 +0900
parents 0faa7120e4b5
children feb0fcc430a9
line wrap: on
line diff
--- a/ordinal.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -211,6 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
+   ; next = next
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -218,14 +219,36 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
+     ; TransFinite1 = TransFinite2
+     ; not-limit = not-limit
+     ; next-limit = next-limit
    }
   } where
+     next : Ordinal {suc n} → Ordinal {suc n}
+     next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
+     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y)
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
+         lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
+         lemma x (case1 lt) = case1 lt
+     not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
+     not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
+     not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
-     TransFinite1 : { ψ : ord1  → Set (suc (suc n)) }
+     TransFinite1 : { ψ : ord1  → Set (suc n) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x
-     TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+     TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
+     TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
+          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord1)  → ψ x
+     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
         caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
             ψ (record { lv = lx ; ord = Φ lx })
         caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
@@ -233,3 +256,4 @@
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
 
+