Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate Ordinals.agda @ 388:19687f3304c9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 25 Jul 2020 12:54:28 +0900 |
| parents | 8b0715e28b33 |
| children | 43b0a6ca7602 |
| rev | line source |
|---|---|
| 16 | 1 open import Level |
|
220
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
2 module Ordinals where |
| 3 | 3 |
|
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
4 open import zf |
| 3 | 5 |
| 23 | 6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 75 | 7 open import Data.Empty |
|
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
8 open import Relation.Binary.PropositionalEquality |
|
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
204
diff
changeset
|
9 open import logic |
|
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
204
diff
changeset
|
10 open import nat |
|
220
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
11 open import Data.Unit using ( ⊤ ) |
|
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
12 open import Relation.Nullary |
|
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
13 open import Relation.Binary |
|
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
14 open import Relation.Binary.Core |
| 3 | 15 |
| 320 | 16 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where |
| 16 | 17 field |
| 221 | 18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z |
| 19 OTri : Trichotomous {n} _≡_ _o<_ | |
| 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) | |
| 21 <-osuc : { x : ord } → x o< osuc x | |
| 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) | |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
23 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) |
| 324 | 24 TransFinite : { ψ : ord → Set n } |
|
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) |
|
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
26 → ∀ (x : ord) → ψ x |
| 388 | 27 TransFinite1 : { ψ : ord → Set (suc n) } |
| 28 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) | |
| 29 → ∀ (x : ord) → ψ x | |
| 16 | 30 |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
31 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
32 field |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
33 x<nx : { y : ord } → (y o< next y ) |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
34 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
35 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z)) |
|
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
36 |
|
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
37 record Ordinals {n : Level} : Set (suc (suc n)) where |
|
220
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
38 field |
|
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
39 ord : Set n |
| 221 | 40 o∅ : ord |
| 41 osuc : ord → ord | |
| 42 _o<_ : ord → ord → Set n | |
| 320 | 43 next : ord → ord |
| 44 isOrdinal : IsOrdinals ord o∅ osuc _o<_ next | |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
45 isNext : IsNext ord o∅ osuc _o<_ next |
| 17 | 46 |
| 221 | 47 module inOrdinal {n : Level} (O : Ordinals {n} ) where |
| 3 | 48 |
| 221 | 49 Ordinal : Set n |
| 50 Ordinal = Ordinals.ord O | |
| 51 | |
| 52 _o<_ : Ordinal → Ordinal → Set n | |
| 53 _o<_ = Ordinals._o<_ O | |
| 218 | 54 |
| 221 | 55 osuc : Ordinal → Ordinal |
| 56 osuc = Ordinals.osuc O | |
| 218 | 57 |
| 221 | 58 o∅ : Ordinal |
| 59 o∅ = Ordinals.o∅ O | |
|
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
60 |
| 320 | 61 next : Ordinal → Ordinal |
| 62 next = Ordinals.next O | |
| 63 | |
| 221 | 64 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) |
| 65 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) | |
| 66 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) | |
| 235 | 67 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) |
| 388 | 68 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O) |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
69 |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
70 x<nx = IsNext.x<nx (Ordinals.isNext O) |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
71 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
72 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O) |
| 321 | 73 |
| 221 | 74 o<-dom : { x y : Ordinal } → x o< y → Ordinal |
| 75 o<-dom {x} _ = x | |
|
74
819da8c08f05
ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
76 |
| 221 | 77 o<-cod : { x y : Ordinal } → x o< y → Ordinal |
| 78 o<-cod {_} {y} _ = y | |
| 147 | 79 |
| 221 | 80 o<-subst : {Z X z x : Ordinal } → Z o< X → Z ≡ z → X ≡ x → z o< x |
| 81 o<-subst df refl refl = df | |
| 94 | 82 |
| 221 | 83 ordtrans : {x y z : Ordinal } → x o< y → y o< z → x o< z |
| 84 ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O) | |
| 94 | 85 |
| 221 | 86 trio< : Trichotomous _≡_ _o<_ |
| 87 trio< = IsOrdinals.OTri (Ordinals.isOrdinal O) | |
|
9
5ed16e2d8eb7
try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
88 |
| 221 | 89 o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥ |
| 90 o<¬≡ {ox} {oy} eq lt with trio< ox oy | |
| 91 o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq | |
| 92 o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt | |
| 93 o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq | |
| 23 | 94 |
| 221 | 95 o<> : {x y : Ordinal } → y o< x → x o< y → ⊥ |
| 96 o<> {ox} {oy} lt tl with trio< ox oy | |
| 97 o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt | |
| 98 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl | |
| 99 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl | |
| 23 | 100 |
| 221 | 101 osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥ |
| 102 osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox | |
| 103 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y | |
| 104 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x | |
| 180 | 105 |
| 221 | 106 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox |
| 107 ---- y < osuc y < x < osuc x | |
| 108 ---- y < osuc y = x < osuc x | |
| 109 ---- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥ | |
| 110 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox | |
| 111 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 112 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc | |
| 113 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c | |
| 114 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox) | |
| 115 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox) | |
| 116 | |
| 338 | 117 osucprev : {ox oy : Ordinal } → osuc oy o< osuc ox → oy o< ox |
| 118 osucprev {ox} {oy} oy<ox with trio< oy ox | |
| 119 osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a | |
| 120 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox ) | |
| 121 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox ) | |
| 122 | |
| 221 | 123 open _∧_ |
| 84 | 124 |
| 221 | 125 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) |
| 126 proj2 (osuc2 x y) lt = osucc lt | |
| 127 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy | |
| 128 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy | |
| 129 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy | |
| 129 | 130 |
| 221 | 131 _o≤_ : Ordinal → Ordinal → Set n |
| 326 | 132 a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b ) |
| 221 | 133 |
| 129 | 134 |
| 221 | 135 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob |
| 136 xo<ab {oa} {ob} a→b with trio< oa ob | |
| 137 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 138 xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc | |
| 139 xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) | |
| 88 | 140 |
| 221 | 141 maxα : Ordinal → Ordinal → Ordinal |
| 142 maxα x y with trio< x y | |
| 143 maxα x y | tri< a ¬b ¬c = y | |
| 144 maxα x y | tri> ¬a ¬b c = x | |
| 145 maxα x y | tri≈ ¬a refl ¬c = x | |
| 84 | 146 |
| 308 | 147 omin : Ordinal → Ordinal → Ordinal |
| 148 omin x y with trio< x y | |
| 149 omin x y | tri< a ¬b ¬c = x | |
| 150 omin x y | tri> ¬a ¬b c = y | |
| 151 omin x y | tri≈ ¬a refl ¬c = x | |
| 88 | 152 |
| 308 | 153 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y |
| 221 | 154 min1 {x} {y} {z} z<x z<y with trio< x y |
| 155 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x | |
| 156 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x | |
| 157 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y | |
| 84 | 158 |
| 221 | 159 -- |
| 160 -- max ( osuc x , osuc y ) | |
| 161 -- | |
| 162 | |
| 163 omax : ( x y : Ordinal ) → Ordinal | |
| 164 omax x y with trio< x y | |
| 165 omax x y | tri< a ¬b ¬c = osuc y | |
| 166 omax x y | tri> ¬a ¬b c = osuc x | |
| 167 omax x y | tri≈ ¬a refl ¬c = osuc x | |
| 86 | 168 |
| 221 | 169 omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y |
| 170 omax< x y lt with trio< x y | |
| 171 omax< x y lt | tri< a ¬b ¬c = refl | |
| 172 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) | |
| 173 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) | |
| 86 | 174 |
| 221 | 175 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y |
| 176 omax≡ x y eq with trio< x y | |
| 177 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) | |
| 178 omax≡ x y eq | tri≈ ¬a refl ¬c = refl | |
| 179 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) | |
| 91 | 180 |
| 221 | 181 omax-x : ( x y : Ordinal ) → x o< omax x y |
| 182 omax-x x y with trio< x y | |
| 183 omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 184 omax-x x y | tri> ¬a ¬b c = <-osuc | |
| 185 omax-x x y | tri≈ ¬a refl ¬c = <-osuc | |
| 16 | 186 |
| 221 | 187 omax-y : ( x y : Ordinal ) → y o< omax x y |
| 188 omax-y x y with trio< x y | |
| 189 omax-y x y | tri< a ¬b ¬c = <-osuc | |
| 190 omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc | |
| 191 omax-y x y | tri≈ ¬a refl ¬c = <-osuc | |
| 192 | |
| 193 omxx : ( x : Ordinal ) → omax x x ≡ osuc x | |
| 194 omxx x with trio< x x | |
| 195 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) | |
| 196 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) | |
| 197 omxx x | tri≈ ¬a refl ¬c = refl | |
| 198 | |
| 199 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) | |
| 200 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) | |
| 201 | |
| 202 open _∧_ | |
| 16 | 203 |
| 326 | 204 o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j |
| 205 o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc | |
| 221 | 206 OrdTrans : Transitive _o≤_ |
| 326 | 207 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c |
| 208 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc | |
| 209 OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc | |
| 210 OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc | |
| 211 OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc | |
|
97
f2b579106770
power set using sup on Def
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
212 |
| 221 | 213 OrdPreorder : Preorder n n n |
| 214 OrdPreorder = record { Carrier = Ordinal | |
| 215 ; _≈_ = _≡_ | |
| 216 ; _∼_ = _o≤_ | |
| 217 ; isPreorder = record { | |
| 218 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | |
| 326 | 219 ; reflexive = o≤-refl |
| 221 | 220 ; trans = OrdTrans |
| 221 } | |
| 222 } | |
| 165 | 223 |
| 258 | 224 FExists : {m l : Level} → ( ψ : Ordinal → Set m ) |
| 221 | 225 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) |
| 226 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) | |
| 227 → ¬ p | |
| 258 | 228 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) |
| 221 | 229 |
| 339 | 230 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z |
| 231 next< {x} {y} {z} x<nz y<nx with trio< y (next z) | |
| 232 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a | |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
233 next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx) |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
234 (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) )))) |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
235 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx ) |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
236 (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc )))) |
| 339 | 237 |
| 342 | 238 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y |
| 239 osuc< {x} {y} refl = <-osuc | |
| 240 | |
| 340 | 241 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
242 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy |
| 340 | 243 |
| 341 | 244 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) |
| 245 nexto≡ {x} with trio< (next x) (next (osuc x) ) | |
| 342 | 246 -- next x o< next (osuc x ) -> osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
247 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx x<nx ) a |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
248 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) |
| 341 | 249 nexto≡ {x} | tri≈ ¬a b ¬c = b |
| 342 | 250 -- next (osuc x) o< next x -> osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ... |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
251 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c |
|
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
252 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) |
| 346 | 253 |
| 352 | 254 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y) |
| 255 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where | |
| 256 y<nx : y o< next x | |
| 257 y<nx = osuc< (sym eq) | |
| 258 | |
| 309 | 259 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where |
| 260 field | |
| 261 os→ : (x : Ordinal) → x o< maxordinal → Ordinal | |
| 262 os← : Ordinal → Ordinal | |
| 263 os←limit : (x : Ordinal) → os← x o< maxordinal | |
| 264 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x | |
| 265 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x | |
| 266 | |
| 361 | 267 module o≤-Reasoning {n : Level} (O : Ordinals {n} ) where |
| 268 | |
| 269 open inOrdinal O | |
| 270 | |
| 271 resp-o< : Ordinals._o<_ O Respects₂ _≡_ | |
| 272 resp-o< = resp₂ _o<_ | |
| 273 | |
| 274 trans1 : {i j k : Ordinal} → i o< j → j o< osuc k → i o< k | |
| 275 trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok | |
| 276 trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j | |
| 277 trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k | |
| 278 | |
| 279 trans2 : {i j k : Ordinal} → i o< osuc j → j o< k → i o< k | |
| 280 trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj | |
| 281 trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k | |
| 282 trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k | |
| 283 | |
| 284 open import Relation.Binary.Reasoning.Base.Triple {n} {_} {_} {_} {Ordinal } {_≡_} {_o≤_} {_o<_} | |
| 285 (Preorder.isPreorder OrdPreorder) | |
| 286 ordtrans --<-trans | |
| 287 (resp₂ _o<_) --(resp₂ _<_) | |
| 288 (λ x → ordtrans x <-osuc ) --<⇒≤ | |
| 289 trans1 --<-transˡ | |
| 290 trans2 --<-transʳ | |
| 291 public | |
| 292 hiding (_≈⟨_⟩_) | |
| 293 |