Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/ODUtil.agda @ 1100:c90eec304cfa
PFOD
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Dec 2022 14:00:57 +0900 |
parents | 55ab5de1ae02 |
children | 3b894bbefe92 |
comparison
equal
deleted
inserted
replaced
1099:c2501d308c95 | 1100:c90eec304cfa |
---|---|
182 lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 | 182 lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 |
183 lemma6 refl HE.refl = refl | 183 lemma6 refl HE.refl = refl |
184 lemma : nat→ω (ω→nato ltd) ≡ * x₁ | 184 lemma : nat→ω (ω→nato ltd) ≡ * x₁ |
185 lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 ) | 185 lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 ) |
186 | 186 |
187 | |
188 ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : infinite-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x | |
189 ω→nat-iso0 Zero iφ eq = refl | |
190 ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) o∅≡od∅ )) | |
191 ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (subst (λ k → k ≡ od∅ ) *iso eq )) | |
192 ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where | |
193 lemma1 : * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i | |
194 lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k) | |
195 ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym | |
196 (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq )))))) | |
197 | |
187 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i | 198 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i |
188 ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where | 199 ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso |
189 lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡ nat→ω i → ω→nato ltd ≡ i | 200 |
190 lemma {x} Zero iφ eq = refl | |
191 lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅ | |
192 lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅ ) *iso eq )) | |
193 lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) ) where -- * x ≡ nat→ω i | |
194 lemma1 : * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i | |
195 lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k) | |
196 ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym | |
197 (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq )))))) | |
198 |