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

comparison OD.agda @ 324:fbabb20f222e

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 Sat, 04 Jul 2020 18:18:17 +0900
parents e228e96965f0
children 1a54dbe1ea4c
comparison
equal deleted inserted replaced
323:e228e96965f0 324:fbabb20f222e
130 lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y 130 lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y
131 lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt)) 131 lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt))
132 lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y 132 lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
133 lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt ) 133 lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
134 134
135
135 _∋_ : ( a x : HOD ) → Set n 136 _∋_ : ( a x : HOD ) → Set n
136 _∋_ a x = odef a ( od→ord x ) 137 _∋_ a x = odef a ( od→ord x )
137 138
138 _c<_ : ( x a : HOD ) → Set n 139 _c<_ : ( x a : HOD ) → Set n
139 x c< a = a ∋ x 140 x c< a = a ∋ x
238 subset-lemma {A} {x} = record { 239 subset-lemma {A} {x} = record {
239 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } 240 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) }
240 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 241 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt }
241 } 242 }
242 243
244 od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
245 od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
246
243 power< : {A x : HOD } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x 247 power< : {A x : HOD } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
244 power< {A} {x} x⊆A = ⊆→o≤ (λ {y} x∋y → subst (λ k → def (od A) k) diso (lemma y x∋y ) ) where 248 power< {A} {x} x⊆A = ⊆→o≤ (λ {y} x∋y → subst (λ k → def (od A) k) diso (lemma y x∋y ) ) where
245 lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y)) 249 lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
246 lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y ) 250 lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
247 251
248 open import Data.Unit 252 open import Data.Unit
249 253
250 ε-induction : { ψ : HOD → Set (suc n)} 254 ε-induction : { ψ : HOD → Set n}
251 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) 255 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x )
252 → (x : HOD ) → ψ x 256 → (x : HOD ) → ψ x
253 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where 257 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where
254 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) 258 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
255 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 259 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
313 data infinite-d : ( x : Ordinal ) → Set n where 317 data infinite-d : ( x : Ordinal ) → Set n where
314 iφ : infinite-d o∅ 318 iφ : infinite-d o∅
315 isuc : {x : Ordinal } → infinite-d x → 319 isuc : {x : Ordinal } → infinite-d x →
316 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 320 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
317 321
318 is-ω : (x : Ordinal) → Dec (infinite-d x )
319 is-ω x = {!!}
320
321 infinite : HOD 322 infinite : HOD
322 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma1 } where 323 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
323 lemma : {y : Ordinal} → Lift (suc n) (infinite-d y → y o< next o∅ ) 324 u : HOD → HOD
324 lemma {y} = TransFinite {λ x → Lift (suc n) (infinite-d x → x o< next o∅) } ind y where 325 u x = Union (x , (x , x))
325 ind : (x : Ordinal) → ((z : Ordinal) → z o< x → Lift (suc n) (infinite-d z → z o< (next o∅))) → 326 lemma1 : {x : HOD} → u x ⊆ Union (u x , (u x , u x))
326 Lift (suc n) (infinite-d x → x o< (next o∅)) 327 lemma1 {x} = record { incl = λ {y} lt → lemma2 y lt } where
327 ind x prev with {!!} 328 lemma2 : (y : HOD) → u x ∋ y → ((z : Ordinal) → (z ≡ od→ord (u x)) ∨ (z ≡ od→ord (u x , u x)) ∧ def (od (ord→od z)) (od→ord y) → ⊥) → ⊥
328 ... | ttt = {!!} 329 lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt }
329 lemma1 : {y : Ordinal} → infinite-d y → y o< next o∅ 330 lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x)) ))
330 lemma1 {y} with lemma {y} 331 lemma3 {x} = od⊆→o≤ lemma1
331 lemma1 {y} | lift p = p 332 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
333 lemma {y} = TransFinite {λ x → infinite-d x → x o< next o∅ } ind y where
334 ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅)) →
335 infinite-d x → x o< (next o∅)
336 ind o∅ prev iφ = proj1 next-limit
337 ind x prev (isuc lt) = lemma0 where
338 lemma0 : {x : Ordinal} → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
339 lemma0 {x} = {!!}
332 340
333 _=h=_ : (x y : HOD) → Set n 341 _=h=_ : (x y : HOD) → Set n
334 x =h= y = od x == od y 342 x =h= y = od x == od y
335 343
336 infixr 200 _∈_ 344 infixr 200 _∈_