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

comparison generic-filter.agda @ 391:e98b5774d180

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generic filter defined
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Jul 2020 16:45:22 +0900
parents d58edc4133b0
children 55f44ec2a0c6
comparison
equal deleted inserted replaced
390:d58edc4133b0 391:e98b5774d180
171 171
172 172
173 open CountableOrdinal 173 open CountableOrdinal
174 open CountableHOD 174 open CountableHOD
175 175
176 PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD 176 PGHOD : (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
177 PGHOD i C p = record { od = record { def = λ x → odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) } 177 PGHOD i C P p = record { od = record { def = λ x → odef P x ∧ odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) }
178 ; odmax = ctl→ C i ; <odmax = λ {y} lt → odefo→o< (proj1 lt)} 178 ; odmax = odmax P ; <odmax = λ {y} lt → <odmax P (proj1 lt) }
179 179
180 next-p : (M : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal 180 next-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal
181 next-p M i C p with ODC.decp O ( PGHOD i C p =h= od∅ ) 181 next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ )
182 next-p M i C p | yes y = p 182 next-p C P i p | yes y = p
183 next-p M i C p | no not = od→ord (ODC.minimal O (PGHOD i C p ) not) 183 next-p C P i p | no not = od→ord (ODC.minimal O (PGHOD i C P p ) not)
184 184
185 data PD (M : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) → Set n where 185 find-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
186 pd0 : PD M C o∅ 0 186 find-p C P Zero x = x
187 pdsuc : {p : Ordinal } {i : Nat} → PD M C p i → PD M C (next-p M i C p) (Suc i) 187 find-p C P (Suc i) x = find-p C P i ( next-p C P i x )
188 188
189 record PDN (M : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where 189 record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where
190 field 190 field
191 gr : Ordinal 191 gr : Nat
192 pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od gr) y 192 pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od (find-p C P gr o∅)) y
193 px∈ω : odef (mhod M) x 193 px∈ω : odef P x
194 grx∈ω : odef (mhod M) gr
195 pdod : PD M C x (mtl← M gr grx∈ω)
196 194
197 open PDN 195 open PDN
198 196
199 PDHOD : (M : CountableHOD ) → (C : CountableOrdinal) → HOD 197 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD
200 PDHOD M C = record { od = record { def = λ x → PDN M C x } 198 PDHOD C P = record { od = record { def = λ x → PDN C P x }
201 ; odmax = odmax (mhod M) ; <odmax = λ {y} lt → ordtrans (<odmax (mhod M) (px∈ω lt)) {!!} } where 199 ; odmax = odmax (Power P) ; <odmax = {!!} } where
202 200
203 -- 201 --
204 -- p 0 ≡ ∅ 202 -- p 0 ≡ ∅
205 -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 203 -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q
206 --- else p n 204 --- else p n
207 205
208 P-GenericFilter : {M : CountableHOD } → (C : CountableOrdinal) → GenericFilter (mhod M) 206 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
209 P-GenericFilter {M} C = record { 207 P-GenericFilter C P = record {
210 genf = record { filter = PDHOD M C ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } 208 genf = record { filter = PDHOD C P ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
211 ; generic = λ D → {!!} 209 ; generic = λ D → {!!}
212 } 210 }