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

comparison OD.agda @ 364:67580311cc8e

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, 18 Jul 2020 11:38:33 +0900
parents aad9249d1e8f
children 7f919d6b045b
comparison
equal deleted inserted replaced
363:aad9249d1e8f 364:67580311cc8e
1 {-# OPTIONS --allow-unsolved-metas #-}
1 open import Level 2 open import Level
2 open import Ordinals 3 open import Ordinals
3 module OD {n : Level } (O : Ordinals {n} ) where 4 module OD {n : Level } (O : Ordinals {n} ) where
4 5
5 open import zf 6 open import zf
398 399
399 infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 400 infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD
400 infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 401 infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
401 u : (y : Ordinal ) → HOD 402 u : (y : Ordinal ) → HOD
402 u y = Union (ord→od y , (ord→od y , ord→od y)) 403 u y = Union (ord→od y , (ord→od y , ord→od y))
404 -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
405 lemma8 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
406 lemma8 = ho<
407 --- (x,y) < next (omax x y) < next (osuc y) = next y
408 lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
409 lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
410 lemma81 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
411 lemma81 {y} = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
412 lemma9 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
413 lemma9 = lemmaa (c<→o< (case1 refl))
414 lemma71 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
415 lemma71 = next< lemma81 lemma9
416 lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
417 lemma1 = ho<
418 --- main recursion
403 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 419 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
404 lemma {o∅} iφ = x<nx 420 lemma {o∅} iφ = x<nx
405 lemma (isuc {y} x) = lemma2 where 421 lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
406 -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
407 lemma0 : y o< next o∅
408 lemma0 = lemma x
409 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
410 lemma8 = ho<
411 --- (x,y) < next (omax x y) < next (osuc y) = next y
412 lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
413 lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
414 lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
415 lemma81 = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
416 lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
417 lemma9 = lemmaa (c<→o< (case1 refl))
418 lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
419 lemma71 = next< lemma81 lemma9
420 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
421 lemma1 = ho<
422 lemma2 : od→ord (u y) o< next o∅
423 lemma2 = next< lemma0 (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
424 422
425 nat→ω : Nat → HOD 423 nat→ω : Nat → HOD
426 nat→ω Zero = od∅ 424 nat→ω Zero = od∅
427 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 425 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
428 426
429 ω→nat : (n : HOD) → infinite ∋ n → Nat 427 ω→nat : (n : HOD) → infinite ∋ n → Nat
430 ω→nat n = lemma where 428 ω→nat n = lemma where
431 lemma : {y : Ordinal} → infinite-d y → Nat 429 lemma : {y : Ordinal} → infinite-d y → Nat
432 lemma iφ = Zero 430 lemma iφ = Zero
433 lemma (isuc lt) = Suc (lemma lt) 431 lemma (isuc lt) = Suc (lemma lt)
432
433 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
434 ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ
435 ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n}))
434 436
435 _=h=_ : (x y : HOD) → Set n 437 _=h=_ : (x y : HOD) → Set n
436 x =h= y = od x == od y 438 x =h= y = od x == od y
437 439
438 infixr 200 _∈_ 440 infixr 200 _∈_