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

comparison src/ODUtil.agda @ 1150:fe0129c40745

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 Tue, 17 Jan 2023 11:21:18 +0900
parents 3091ac71a999
children 8a071bf52407
comparison
equal deleted inserted replaced
1149:f8a30e568eca 1150:fe0129c40745
43 43
44 cseq : HOD → HOD 44 cseq : HOD → HOD
45 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where 45 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
46 lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x) 46 lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
47 lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) 47 lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )
48
49 ∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
50 ∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
51
52 _∪_ : ( A B : HOD ) → HOD
53 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
54 odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
55 lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
56 lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
57 lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
58
59 _＼_ : ( A B : HOD ) → HOD
60 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
61
62 ¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
63 ¬∅∋ {x} = ¬x<0
48 64
49 65
50 pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) ) 66 pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
51 pair-xx<xy {x} {y} = ⊆→o≤ lemma where 67 pair-xx<xy {x} {y} = ⊆→o≤ lemma where
52 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z 68 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
229 → { p q : HOD } → Union (Power P) ∋ p → Union (Power P) ∋ q → Union (Power P) ∋ (p ∩ q) 245 → { p q : HOD } → Union (Power P) ∋ p → Union (Power P) ∋ q → Union (Power P) ∋ (p ∩ q)
230 UPower∩ {P} each {p} {q} record { owner = x ; ao = ppx ; ox = xz } record { owner = y ; ao = ppy ; ox = yz } 246 UPower∩ {P} each {p} {q} record { owner = x ; ao = ppx ; ox = xz } record { owner = y ; ao = ppy ; ox = yz }
231 = record { owner = & P ; ao = PPP ; ox = lem03 } where 247 = record { owner = & P ; ao = PPP ; ox = lem03 } where
232 lem03 : odef (* (& P)) (& (p ∩ q)) 248 lem03 : odef (* (& P)) (& (p ∩ q))
233 lem03 = subst (λ k → odef k (& (p ∩ q))) (sym *iso) ( each (ppx _ xz) (ppy _ yz) ) 249 lem03 = subst (λ k → odef k (& (p ∩ q))) (sym *iso) ( each (ppx _ xz) (ppy _ yz) )
250
251 -- ∋-irr : {X x : HOD} → (a b : X ∋ x ) → a ≡ b
252 -- ∋-irr {X} {x} _ _ = refl
253 -- is requed in
254 -- Replace∩ : {X P Q : HOD} → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
255 -- → Replace' (P ∩ Q) (λ _ pq → ψ _ (P⊆X (proj1 pq ))) ≡ Replace' P (λ _ p → ψ _ (P⊆X p)) ∩ Replace' Q (λ _ q → ψ _ (Q⊆X q))
256 -- Replace∩ {X} {P} {Q} {ψ} P⊆X Q⊆X = ==→o≡ record { eq→ = lem04 ; eq← = ? } where
257 -- lem04 : {x : Ordinal} → OD.def (od (Replace' (P ∩ Q) (λ z pq → ψ z (P⊆X (proj1 pq)) ))) x
258 -- → OD.def (od (Replace' P (λ z p → ψ z (P⊆X p)) ∩ Replace' Q (λ z q → ψ z (Q⊆X q)))) x
259 -- lem04 {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪
260 -- record { z = _ ; az = proj1 az ; x=ψz = ? } ,
261 -- record { z = _ ; az = proj2 az ; x=ψz = ? } ⟫
262
263 Repl∪ψ : {X P Q : HOD} → (ψ : (x : HOD) → X ∋ x → HOD) → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X ) → (x : HOD) → (P ∪ Q) ∋ x → HOD
264 Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case1 p) = ψ _ (P⊆X p)
265 Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case2 q) = ψ _ (Q⊆X q)
266
267 Replace∪ : {X P Q : HOD} → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
268 → Replace' (P ∪ Q) (Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X) ≡ Replace' P (λ _ p → ψ _ (P⊆X p)) ∪ Replace' Q (λ _ q → ψ _ (Q⊆X q))
269 Replace∪ {X} {P} {Q} {ψ} P⊆X Q⊆X = ==→o≡ record { eq→ = ? ; eq← = ? }
270
271
272