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

comparison HOD.agda @ 118:78fe704c3543

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Union done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Jun 2019 20:32:30 +0900
parents a4c97390d312
children 6e264c78e420
comparison
equal deleted inserted replaced
117:a4c97390d312 118:78fe704c3543
81 81
82 _c≤_ : {n : Level} → HOD {n} → HOD {n} → Set (suc n) 82 _c≤_ : {n : Level} → HOD {n} → HOD {n} → Set (suc n)
83 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) 83 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
84 84
85 cseq : {n : Level} → HOD {n} → HOD {n} 85 cseq : {n : Level} → HOD {n} → HOD {n}
86 cseq x = record { def = λ y → osuc y o< (od→ord x) ; otrans = lemma } where 86 cseq x = record { def = λ y → def x (osuc y) ; otrans = lemma } where
87 lemma : {ox : Ordinal} → osuc ox o< od→ord x → { oy : Ordinal}→ oy o< ox → osuc oy o< od→ord x 87 lemma : {ox : Ordinal} → def x (osuc ox) → { oy : Ordinal}→ oy o< ox → def x (osuc oy)
88 lemma {ox} oox<Ox {oy} oy<ox = ordtrans (osucc oy<ox ) oox<Ox 88 lemma {ox} oox<Ox {oy} oy<ox = otrans x oox<Ox (osucc oy<ox )
89 89
90 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x 90 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x
91 def-subst df refl refl = df 91 def-subst df refl refl = df
92 92
93 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x 93 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x
278 infixr 220 _⊆_ 278 infixr 220 _⊆_
279 isZF : IsZF (HOD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (Ord omega) 279 isZF : IsZF (HOD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (Ord omega)
280 isZF = record { 280 isZF = record {
281 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 281 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
282 ; pair = pair 282 ; pair = pair
283 ; union-u = λ _ z _ → csuc z 283 ; union-u = λ X z UX∋z → union-u {X} {z} UX∋z
284 ; union→ = union→ 284 ; union→ = union→
285 ; union← = union← 285 ; union← = union←
286 ; empty = empty 286 ; empty = empty
287 ; power→ = power→ 287 ; power→ = power→
288 ; power← = power← 288 ; power← = power←
333 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 333 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
334 lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t 334 lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
335 lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) {!!} 335 lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) {!!}
336 lemma : od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x))) 336 lemma : od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
337 lemma = sup-o< 337 lemma = sup-o<
338 union-lemma-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z 338 union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
339 union-lemma-u {X} {z} U>z = lemma <-osuc where 339 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
340 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
341 lemma {oz} {ooz} lt = def-subst {suc n} {ord→od ooz} {!!} refl refl
342 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 340 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
343 union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y )) 341 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
344 union→ X y u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) 342 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx))
345 union→ X y u xx | tri< a ¬b ¬c | () 343 union→ X z u xx | tri< a ¬b ¬c | ()
346 union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where 344 union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b where
347 lemma : {oX ou ooy : Ordinal {suc n}} → ou ≡ ooy → ou o< oX → ooy o< oX 345 union→ X z u xx | tri> ¬a ¬b c = otrans X (proj1 xx) c
348 lemma refl lt = lt 346 union← : (X z : HOD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
349 union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 347 union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
350 union← : (X z : HOD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z ) 348 lemma : X ∋ union-u {X} {z} X∋z
351 union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z } 349 lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord
352 ψiso : {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y → ψ y 350 ψiso : {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y → ψ y
353 ψiso {ψ} t refl = t 351 ψiso {ψ} t refl = t
354 selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y) 352 selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
355 selection {X} {ψ} {y} = record { proj1 = λ s → record { 353 selection {X} {ψ} {y} = record { proj1 = λ s → record {
356 proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) } 354 proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) }
382 lemma2 : {x : HOD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x) 380 lemma2 : {x : HOD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x)
383 lemma2 = trans ( cong ( λ k → od→ord k ) xx-union ) {!!} 381 lemma2 = trans ( cong ( λ k → od→ord k ) xx-union ) {!!}
384 lemma : {x : HOD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x)) 382 lemma : {x : HOD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
385 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 ) 383 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 )
386 uxxx-union : {x : HOD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } 384 uxxx-union : {x : HOD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
387 uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) lemma where 385 uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) {!!} where
388 lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x)) 386 lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
389 lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) {!!} 387 lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) {!!}
390 uxxx-2 : {x : HOD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) } 388 uxxx-2 : {x : HOD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) }
391 eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt 389 eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt
392 eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt 390 eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt