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

comparison generic-filter.agda @ 427:9b0630f03c4b

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, 08 Aug 2020 18:14:14 +0900
parents cc7909f86841
children 94392feeebc5
comparison
equal deleted inserted replaced
426:47aacf417930 427:9b0630f03c4b
183 -- a(n) ∈ M 183 -- a(n) ∈ M
184 -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q 184 -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q
185 -- 185 --
186 PGHOD : (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD 186 PGHOD : (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
187 PGHOD i C P p = record { od = record { def = λ x → 187 PGHOD i C P p = record { od = record { def = λ x →
188 odef P x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } 188 odef (Power P) x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) }
189 ; odmax = odmax P ; <odmax = λ {y} lt → <odmax P (proj1 lt) } 189 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }
190 190
191 --- 191 ---
192 -- p(n+1) = if PGHOD n qn otherwise p(n) 192 -- p(n+1) = if PGHOD n qn otherwise p(n)
193 -- 193 --
194 next-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal 194 next-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal
195 next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ ) 195 next-p C P i p with is-o∅ ( & (PGHOD i C P p))
196 next-p C P i p | yes y = p 196 next-p C P i p | yes y = p
197 next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) not) 197 next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) (λ eq → not (=od∅→≡o∅ eq))) -- axiom of choice
198 198
199 --- 199 ---
200 -- ascendant search on p(n) 200 -- ascendant search on p(n)
201 -- 201 --
202 find-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal 202 find-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
208 -- 208 --
209 record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where 209 record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where
210 field 210 field
211 gr : Nat 211 gr : Nat
212 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y 212 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
213 px∈ω : odef (Power P) x 213 x∈PP : odef (Power P) x
214 214
215 open PDN 215 open PDN
216 216
217 --- 217 ---
218 -- G as a HOD 218 -- G as a HOD
219 -- 219 --
220 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD 220 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD
221 PDHOD C P = record { od = record { def = λ x → PDN C P x } 221 PDHOD C P = record { od = record { def = λ x → PDN C P x }
222 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.px∈ω lt) } where 222 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt) } where
223 223
224 open PDN 224 open PDN
225 225
226 ---- 226 ----
227 -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set ) 227 -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
228 -- 228 --
229 -- p 0 ≡ ∅ 229 -- p 0 ≡ ∅
230 -- p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q (axiom of choice) 230 -- p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q (axiom of choice)
231 --- else p n 231 --- else p n
232
233 P∅ : {P : HOD} → odef (Power P) o∅
234 P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where
235 lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
236 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt ))
237 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
238 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
232 239
233 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P 240 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
234 P-GenericFilter C P = record { 241 P-GenericFilter C P = record {
235 genf = record { filter = PDHOD C P ; f⊆PL = f⊆PL ; filter1 = {!!} ; filter2 = {!!} } 242 genf = record { filter = PDHOD C P ; f⊆PL = f⊆PL ; filter1 = {!!} ; filter2 = {!!} }
236 ; generic = λ D → {!!} 243 ; generic = λ D → {!!}
237 } where 244 } where
238 P∅ : {P : HOD} → odef (Power P) o∅
239 P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where
240 lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
241 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt ))
242 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
243 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
244 find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y 245 find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y
245 find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso 246 find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso
246 ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py)) 247 ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py))
247 find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x) y {!!} {!!} 248 find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x) y {!!} {!!}
248 f⊆PL : PDHOD C P ⊆ Power P 249 f⊆PL : PDHOD C P ⊆ Power P
272 lemma726 = {!!} 273 lemma726 = {!!}
273 274
274 -- 275 --
275 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } 276 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
276 -- 277 --
277 278 -- W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) | { i ∈ Nat → p i ≠ i1 } is finite }
278 279 --
279 280
280 281
282