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

changeset 389:cb183674facf

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, 25 Jul 2020 13:12:29 +0900
parents 19687f3304c9
children d58edc4133b0
files generic-filter.agda
diffstat 1 files changed, 17 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/generic-filter.agda	Sat Jul 25 12:54:28 2020 +0900
+++ b/generic-filter.agda	Sat Jul 25 13:12:29 2020 +0900
@@ -173,14 +173,14 @@
 open CountableOrdinal 
 open CountableHOD
 
-PGHOD : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
-PGHOD P 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 ) }
+PGHOD :  (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
+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 P i C p =h= od∅ )
+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 P i C p ) not)
+next-p P 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 
@@ -202,16 +202,19 @@
 --  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 
 ---             else p n
 
-Gω2r :  (x : Ordinal) → (lt : infinite ∋ ord→od x ) →  Hω2 (ω→nat (ord→od x) lt ) x
-Gω2r  x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) →  Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} {!!} (ord→od x)) where
-    ψ : HOD  → Set n
-    ψ y = (lt : odef infinite (od→ord y) ) →  Hω2 (ω→nat y lt ) (od→ord y )
-    ind : {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 {x} prev lt with ω→nat x lt
-    ... | Zero = subst (λ k → Hω2 Zero k) ? hφ
-    ... | Suc t = {!!}
+ψ : 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 {