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

comparison OD.agda @ 187:ac872f6b8692

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Todo
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jul 2019 11:08:24 +0900
parents 914cc522c53a
children 1f2c8b094908
comparison
equal deleted inserted replaced
186:914cc522c53a 187:ac872f6b8692
68 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 68 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
69 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ 69 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ
70 -- contra-position of mimimulity of supermum required in Power Set Axiom 70 -- contra-position of mimimulity of supermum required in Power Set Axiom
71 -- sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 71 -- sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
72 -- sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 72 -- sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
73 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ )
74 -- mimimul and x∋minimul is an Axiom of choice 73 -- mimimul and x∋minimul is an Axiom of choice
75 minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 74 minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n}
76 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) 75 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
77 x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) 76 x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
78 -- 77 -- minimulity (may proved by ε-induction )
79 minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) 78 minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) )
80 79
81 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 80 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
82 _∋_ {n} a x = def a ( od→ord x ) 81 _∋_ {n} a x = def a ( od→ord x )
83 82
100 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )} 99 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
101 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where 100 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
102 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) 101 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
103 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) 102 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) )
104 103
105 otrans : {n : Level} {a x : Ordinal {n} } → def (Ord a) x → { y : Ordinal {n} } → y o< x → def (Ord a) y 104 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y
106 otrans {n} {a} {x} x<a {y} y<x = ordtrans y<x x<a 105 otrans x<a y<x = ordtrans y<x x<a
107 106
108 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} 107 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
109 ∅3 {n} {x} = TransFinite {n} c2 c3 x where 108 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
110 c0 : Nat → Ordinal {n} → Set n 109 c0 : Nat → Ordinal {n} → Set n
111 c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} 110 c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n}
157 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x 156 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
158 157
159 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x 158 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x
160 c≤-refl x = case1 refl 159 c≤-refl x = case1 refl
161 160
162 ∋→o< : {n : Level} → { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
163 ∋→o< {n} {a} {x} lt = t where
164 t : (od→ord x) o< (od→ord a)
165 t = c<→o< {suc n} {x} {a} lt
166
167 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} 161 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
168 o∅≡od∅ {n} = ==→o≡ lemma where 162 o∅≡od∅ {n} = ==→o≡ lemma where
169 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x 163 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x
170 lemma0 {x} lt = o<-subst (c<→o< {suc n} {ord→od x} {ord→od o∅} (def-subst {suc n} {ord→od o∅} {x} lt refl (sym diso)) ) diso diso 164 lemma0 {x} lt = o<-subst (c<→o< {suc n} {ord→od x} {ord→od o∅} (def-subst {suc n} {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
171 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅) x 165 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅) x
174 lemma : ord→od o∅ == od∅ 168 lemma : ord→od o∅ == od∅
175 lemma = record { eq→ = lemma0 ; eq← = lemma1 } 169 lemma = record { eq→ = lemma0 ; eq← = lemma1 }
176 170
177 ord-od∅ : {n : Level} → od→ord (od∅ {suc n}) ≡ o∅ {suc n} 171 ord-od∅ : {n : Level} → od→ord (od∅ {suc n}) ≡ o∅ {suc n}
178 ord-od∅ {n} = sym ( subst (λ k → k ≡ od→ord (od∅ {suc n}) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) ) 172 ord-od∅ {n} = sym ( subst (λ k → k ≡ od→ord (od∅ {suc n}) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )
179
180 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x )
181 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
182
183 o≡→¬c< : {n : Level} → { x y : OD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y
184 o≡→¬c< {n} {x} {y} oeq lt = o<¬≡ (orefl oeq ) (c<→o< lt)
185 173
186 ∅0 : {n : Level} → record { def = λ x → Lift n ⊥ } == od∅ {n} 174 ∅0 : {n : Level} → record { def = λ x → Lift n ⊥ } == od∅ {n}
187 eq→ ∅0 {w} (lift ()) 175 eq→ ∅0 {w} (lift ())
188 eq← ∅0 {w} (case1 ()) 176 eq← ∅0 {w} (case1 ())
189 eq← ∅0 {w} (case2 ()) 177 eq← ∅0 {w} (case2 ())
309 297
310 empty : {n : Level } (x : OD {suc n} ) → ¬ (od∅ ∋ x) 298 empty : {n : Level } (x : OD {suc n} ) → ¬ (od∅ ∋ x)
311 empty x (case1 ()) 299 empty x (case1 ())
312 empty x (case2 ()) 300 empty x (case2 ())
313 301
314 ord-⊆ : ( t x : OD {suc n} ) → _⊆_ t (Ord (od→ord t )) {x}
315 ord-⊆ t x lt = c<→o< lt
316 o<→c< : {x y : Ordinal {suc n}} {z : OD {suc n}}→ x o< y → _⊆_ (Ord x) (Ord y) {z} 302 o<→c< : {x y : Ordinal {suc n}} {z : OD {suc n}}→ x o< y → _⊆_ (Ord x) (Ord y) {z}
317 o<→c< lt lt1 = ordtrans lt1 lt 303 o<→c< lt lt1 = ordtrans lt1 lt
318 304
319 ⊆→o< : {x y : Ordinal {suc n}} → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y 305 ⊆→o< : {x y : Ordinal {suc n}} → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y
320 ⊆→o< {x} {y} lt with trio< x y 306 ⊆→o< {x} {y} lt with trio< x y