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

comparison ordinal-definable.agda @ 84:4b2aff372b7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
omax ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jun 2019 23:58:58 +0900
parents e013ccf00567
children 296388c03358
comparison
equal deleted inserted replaced
83:e013ccf00567 84:4b2aff372b7c
252 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} 252 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
253 Replace X ψ = sup-od ψ 253 Replace X ψ = sup-od ψ
254 Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n} 254 Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
255 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 255 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
256 _,_ : OD {suc n} → OD {suc n} → OD {suc n} 256 _,_ : OD {suc n} → OD {suc n} → OD {suc n}
257 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } 257 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
258 Union : OD {suc n} → OD {suc n} 258 Union : OD {suc n} → OD {suc n}
259 Union U = record { def = λ y → osuc y o< (od→ord U) } 259 Union U = record { def = λ y → osuc y o< (od→ord U) }
260 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 260 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
261 Power : OD {suc n} → OD {suc n} 261 Power : OD {suc n} → OD {suc n}
262 Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) } 262 Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) }
291 ; replacement = {!!} 291 ; replacement = {!!}
292 } where 292 } where
293 open _∧_ 293 open _∧_
294 open Minimumo 294 open Minimumo
295 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 295 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
296 proj1 (pair A B ) = case1 refl 296 proj1 (pair A B ) = omax-x {n} {od→ord A} {od→ord B}
297 proj2 (pair A B ) = case2 refl 297 proj2 (pair A B ) = omax-y {n} {od→ord A} {od→ord B}
298 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 298 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
299 empty x () 299 empty x ()
300 --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) } 300 --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) }
301 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x 301 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
302 power→ A t P∋t {x} t∋x = proj1 (P∋t (od→ord x) ) 302 power→ A t P∋t {x} t∋x = proj1 (P∋t (od→ord x) )
341 reg {y} t with proj1 t 341 reg {y} t with proj1 t
342 ... | x∈∅ = x∈∅ 342 ... | x∈∅ = x∈∅
343 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 343 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
344 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 344 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
345 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 345 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
346 pair-or : {x y : OD {suc n} } → (x , x) ∋ y → (y == x ) ∨ (x ∋ y ) 346 pair-osuc : {x y : OD {suc n}} → (x , x) ∋ y → (od→ord y ) o< osuc (od→ord x)
347 pair-or {x} {y} lt with tri-c< x y 347 pair-osuc {x} {y} z with union← (x , x) y z
348 pair-or {x} {y} lt | tri< a ¬b ¬c = {!!} -- x < y < ( x , x ) 348 ... | t = {!!}
349 pair-or {x} {y} lt | tri≈ ¬a b ¬c = case1 (eq-sym b)
350 pair-or {x} {y} lt | tri> ¬a ¬b c = case2 c
351 pair-osuc : (x : OD) → od→ord (x , x) ≡ osuc (od→ord x)
352 pair-osuc x with trio< (od→ord (x , x)) (osuc (od→ord x))
353 pair-osuc x | tri< a ¬b ¬c = ⊥-elim ( osuc-< a (c<→o< (proj1 (pair x x )) ))
354 pair-osuc x | tri≈ ¬a b ¬c = b
355 pair-osuc x | tri> ¬a ¬b c with pair-or (def-subst (o<→c< c ) oiso refl ) -- (x , x) ∋ ord→od (osuc (od→ord x) )
356 pair-osuc x | tri> ¬a ¬b c | case1 eq = ⊥-elim ( o<→¬== (def-subst {suc n} (o<→c< c ) refl diso ) eq )
357 pair-osuc x | tri> ¬a ¬b c | case2 lt = ⊥-elim (c<> c lt ) where
358 lemma2 : (z : Ordinal {suc n} ) → lv (od→ord (ord→od z , ord→od z) ) ≡ lv z
359 lemma2 z = {!!}
360 next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x)) 349 next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
361 eq→ (next x ) {y} z = {!!} 350 eq→ (next x ) {y} z = {!!} -- z : y o< osuc (osuc ox ) → y < osuc ox
362 eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_} 351 eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_}
363 (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where 352 (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where
353 lemma0 : (x , x) ∋ ord→od y
354 lemma0 = o<-subst {suc n} {od→ord (ord→od y)} {od→ord {!!}} (c<→o< z) {!!} {!!}
364 lemma1 : (x , (x , x)) ∋ ord→od (osuc y) -- z : def (ord→od (osuc (od→ord x))) y 355 lemma1 : (x , (x , x)) ∋ ord→od (osuc y) -- z : def (ord→od (osuc (od→ord x))) y
365 lemma1 with tri-c< (x , x) (ord→od (osuc (od→ord x))) 356 lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< z) oiso refl)
366 lemma1 | tri< a ¬b ¬c = {!!} 357 lemma1 | case1 x = {!!}
367 lemma1 | tri≈ ¬a b ¬c = {!!} 358 lemma1 | case2 t = {!!}
368 lemma1 | tri> ¬a ¬b c = {!!} 359 -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!}
369 lemma2 : ord→od (osuc y) ∋ ord→od y 360 lemma2 : ord→od (osuc y) ∋ ord→od y
370 lemma2 = o<→c< <-osuc 361 lemma2 = o<→c< <-osuc
371 next' : (x : OD) → ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x)) 362 next' : (x : OD) → ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x))
372 next' x = subst ( λ k → k == ord→od (osuc (od→ord x))) (sym oiso) (next x) 363 next' x = subst ( λ k → k == ord→od (osuc (od→ord x))) (sym oiso) (next x)
373 infinite : OD {suc n} 364 infinite : OD {suc n}