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

comparison Ordinals.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 bca043423554
comparison
equal deleted inserted replaced
289:9f926b2210bc 334:ba3ebb9a16c6
11 open import Data.Unit using ( ⊤ ) 11 open import Data.Unit using ( ⊤ )
12 open import Relation.Nullary 12 open import Relation.Nullary
13 open import Relation.Binary 13 open import Relation.Binary
14 open import Relation.Binary.Core 14 open import Relation.Binary.Core
15 15
16 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where 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
17 field 17 field
18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z 18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
19 OTri : Trichotomous {n} _≡_ _o<_ 19 OTri : Trichotomous {n} _≡_ _o<_
20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
21 <-osuc : { x : ord } → x o< osuc x 21 <-osuc : { x : ord } → x o< osuc x
22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
23 TransFinite : { ψ : ord → Set (suc n) } 23 not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y )
25 TransFinite : { ψ : ord → Set n }
26 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
27 → ∀ (x : ord) → ψ x
28 TransFinite1 : { ψ : ord → Set (suc n) }
24 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 29 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
25 → ∀ (x : ord) → ψ x 30 → ∀ (x : ord) → ψ x
26 31
27 32
28 record Ordinals {n : Level} : Set (suc (suc n)) where 33 record Ordinals {n : Level} : Set (suc (suc n)) where
29 field 34 field
30 ord : Set n 35 ord : Set n
31 o∅ : ord 36 o∅ : ord
32 osuc : ord → ord 37 osuc : ord → ord
33 _o<_ : ord → ord → Set n 38 _o<_ : ord → ord → Set n
34 isOrdinal : IsOrdinals ord o∅ osuc _o<_ 39 next : ord → ord
40 isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
35 41
36 module inOrdinal {n : Level} (O : Ordinals {n} ) where 42 module inOrdinal {n : Level} (O : Ordinals {n} ) where
37 43
38 Ordinal : Set n 44 Ordinal : Set n
39 Ordinal = Ordinals.ord O 45 Ordinal = Ordinals.ord O
44 osuc : Ordinal → Ordinal 50 osuc : Ordinal → Ordinal
45 osuc = Ordinals.osuc O 51 osuc = Ordinals.osuc O
46 52
47 o∅ : Ordinal 53 o∅ : Ordinal
48 o∅ = Ordinals.o∅ O 54 o∅ = Ordinals.o∅ O
55
56 next : Ordinal → Ordinal
57 next = Ordinals.next O
49 58
50 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) 59 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
51 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) 60 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
52 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) 61 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
53 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) 62 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
54 63 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O)
64 next-limit = IsOrdinals.next-limit (Ordinals.isOrdinal O)
65
55 o<-dom : { x y : Ordinal } → x o< y → Ordinal 66 o<-dom : { x y : Ordinal } → x o< y → Ordinal
56 o<-dom {x} _ = x 67 o<-dom {x} _ = x
57 68
58 o<-cod : { x y : Ordinal } → x o< y → Ordinal 69 o<-cod : { x y : Ordinal } → x o< y → Ordinal
59 o<-cod {_} {y} _ = y 70 o<-cod {_} {y} _ = y
102 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy 113 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
103 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy 114 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
104 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 115 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy
105 116
106 _o≤_ : Ordinal → Ordinal → Set n 117 _o≤_ : Ordinal → Ordinal → Set n
107 a o≤ b = (a ≡ b) ∨ ( a o< b ) 118 a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b )
108 119
109 120
110 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob 121 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob
111 xo<ab {oa} {ob} a→b with trio< oa ob 122 xo<ab {oa} {ob} a→b with trio< oa ob
112 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc 123 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
117 maxα x y with trio< x y 128 maxα x y with trio< x y
118 maxα x y | tri< a ¬b ¬c = y 129 maxα x y | tri< a ¬b ¬c = y
119 maxα x y | tri> ¬a ¬b c = x 130 maxα x y | tri> ¬a ¬b c = x
120 maxα x y | tri≈ ¬a refl ¬c = x 131 maxα x y | tri≈ ¬a refl ¬c = x
121 132
122 minα : Ordinal → Ordinal → Ordinal 133 omin : Ordinal → Ordinal → Ordinal
123 minα x y with trio< x y 134 omin x y with trio< x y
124 minα x y | tri< a ¬b ¬c = x 135 omin x y | tri< a ¬b ¬c = x
125 minα x y | tri> ¬a ¬b c = y 136 omin x y | tri> ¬a ¬b c = y
126 minα x y | tri≈ ¬a refl ¬c = x 137 omin x y | tri≈ ¬a refl ¬c = x
127 138
128 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y 139 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y
129 min1 {x} {y} {z} z<x z<y with trio< x y 140 min1 {x} {y} {z} z<x z<y with trio< x y
130 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x 141 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
131 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x 142 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
132 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y 143 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
133 144
174 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) 185 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x)
175 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) 186 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
176 187
177 open _∧_ 188 open _∧_
178 189
190 o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j
191 o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
179 OrdTrans : Transitive _o≤_ 192 OrdTrans : Transitive _o≤_
180 OrdTrans (case1 refl) (case1 refl) = case1 refl 193 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
181 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 194 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
182 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 195 OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
183 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) 196 OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
197 OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc
184 198
185 OrdPreorder : Preorder n n n 199 OrdPreorder : Preorder n n n
186 OrdPreorder = record { Carrier = Ordinal 200 OrdPreorder = record { Carrier = Ordinal
187 ; _≈_ = _≡_ 201 ; _≈_ = _≡_
188 ; _∼_ = _o≤_ 202 ; _∼_ = _o≤_
189 ; isPreorder = record { 203 ; isPreorder = record {
190 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 204 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
191 ; reflexive = case1 205 ; reflexive = o≤-refl
192 ; trans = OrdTrans 206 ; trans = OrdTrans
193 } 207 }
194 } 208 }
195 209
196 FExists : {m l : Level} → ( ψ : Ordinal → Set m ) 210 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
197 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) 211 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
198 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 212 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
199 → ¬ p 213 → ¬ p
200 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 214 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
201 215
216 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
217 field
218 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
219 os← : Ordinal → Ordinal
220 os←limit : (x : Ordinal) → os← x o< maxordinal
221 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x
222 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x
223