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

changeset 390:d58edc4133b0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generic filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Jul 2020 13:33:53 +0900
parents cb183674facf
children e98b5774d180
files generic-filter.agda
diffstat 1 files changed, 25 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/generic-filter.agda	Sat Jul 25 13:12:29 2020 +0900
+++ b/generic-filter.agda	Sat Jul 25 13:33:53 2020 +0900
@@ -162,12 +162,12 @@
 
 record CountableHOD : Set (suc (suc n)) where
    field
-       phod : HOD
-       ptl→ : Nat → Ordinal
-       ptl→∈P : (i : Nat) → odef phod (ptl→ i)
-       ptl← : (x : Ordinal) → odef phod x → Nat
-       ptl-iso→ : { x : Ordinal } → (lt : odef phod x ) → ptl→ (ptl← x lt ) ≡ x 
-       ptl-iso← : { x : Nat }  → ptl← (ptl→ x ) (ptl→∈P x) ≡ x
+       mhod : HOD
+       mtl→ : Nat → Ordinal
+       mtl→∈P : (i : Nat) → odef mhod (mtl→ i)
+       mtl← : (x : Ordinal) → odef mhod x → Nat
+       mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x 
+       mtl-iso← : { x : Nat }  → mtl← (mtl→ x ) (mtl→∈P x) ≡ x
    
        
 open CountableOrdinal 
@@ -177,47 +177,36 @@
 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 ) }
    ; odmax = ctl→ C i  ; <odmax = λ {y} lt → odefo→o< (proj1 lt)}  
 
-next-p : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal
-next-p P i C p with ODC.decp O ( PGHOD i C p =h= od∅ )
-next-p P i C p | yes y = p
-next-p P i C p | no not = od→ord (ODC.minimal O (PGHOD i C p ) not)
+next-p : (M : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal
+next-p M i C p with ODC.decp O ( PGHOD i C p =h= od∅ )
+next-p M i C p | yes y = p
+next-p M i C p | no not = od→ord (ODC.minimal O (PGHOD i C p ) not)
 
-data PD (P : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set n where
-    pd0 : PD P C o∅ 0 
-    pdsuc : {p : Ordinal } {i : Nat} → PD P C p i  → PD P C (next-p P i C p) (Suc i) 
+data PD (M : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set n where
+    pd0 : PD M C o∅ 0 
+    pdsuc : {p : Ordinal } {i : Nat} → PD M C p i  → PD M C (next-p M i C p) (Suc i) 
 
-record PDN (P : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where
+record PDN (M : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where
    field
-       px∈ω : odef (phod P) x
-       pdod : PD P C x (ptl← P x px∈ω)
+       gr : Ordinal
+       pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od gr) y
+       px∈ω  : odef (mhod M) x
+       grx∈ω : odef (mhod M) gr
+       pdod : PD M C x (mtl← M gr grx∈ω)
 
 open PDN
 
-PDHOD : (P : CountableHOD ) → (C : CountableOrdinal) → HOD
-PDHOD P C = record { od = record { def = λ x →  PDN P C x }
-    ; odmax = odmax (phod P) ; <odmax = λ {y} lt → <odmax (phod P) (px∈ω lt) } where
+PDHOD : (M : CountableHOD ) → (C : CountableOrdinal) → HOD
+PDHOD M C = record { od = record { def = λ x →  PDN M C x }
+    ; odmax = odmax (mhod M) ; <odmax = λ {y} lt → ordtrans (<odmax (mhod M) (px∈ω lt)) {!!}  } where
 
 --
 --  p 0 ≡ ∅
 --  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 
 ---             else p n
 
-ψ : HOD  → Set n
-ψ y = (lt : odef infinite (od→ord y) ) →  Hω2 (ω→nat y lt ) (od→ord y )
-ind : (C : CountableOrdinal) → {x : HOD} → ({y : HOD} → OD.def (od x) (od→ord y) →
-   (lt : infinite-d (od→ord y)) → Hω2 (ω→nat y lt) (od→ord y)) →
-   (lt : infinite-d (od→ord x)) → Hω2 (ω→nat x lt) (od→ord x)
-ind C {x} prev lt with ω→nat x lt
-... | Zero = subst (λ k → Hω2 Zero k) {!!} hφ
-... | Suc i with ODC.decp O ( PGHOD i C {!!} =h= od∅ ) | prev {{!!}} {!!} {!!}
-ind C {x} prev lt | Suc i | yes p | s1 = he ?
-ind C {x} prev lt | Suc i | no ¬p | s1 = {!!}
-
-Gω2r :  (C : CountableOrdinal) → (x : Ordinal) → (lt : infinite ∋ ord→od x ) →  Hω2 (ω→nat (ord→od x) lt ) x
-Gω2r C x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) →  Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} (ind C) (ord→od x)) 
-
-P-GenericFilter : {P : CountableHOD } → (C : CountableOrdinal) → GenericFilter (phod P)
-P-GenericFilter {P} C = record {
-      genf = record { filter = PDHOD P C ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
+P-GenericFilter : {M : CountableHOD } → (C : CountableOrdinal) → GenericFilter (mhod M)
+P-GenericFilter {M} C = record {
+      genf = record { filter = PDHOD M C ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
     ; generic = λ D → {!!}
    }