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

changeset 462:667c54e6fa1f

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 Sun, 20 Mar 2022 16:29:03 +0900
parents 0e018784bed3
children 433866b43992
files src/generic-filter.agda
diffstat 1 files changed, 25 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Sun Mar 20 11:41:48 2022 +0900
+++ b/src/generic-filter.agda	Sun Mar 20 16:29:03 2022 +0900
@@ -190,6 +190,11 @@
            fd02 = dense-d D Lp0
            fd04 : dense-f D Lp0 ⊆ P
            fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
+           fd09 : (i : Nat ) → odef L (find-p L C i (& p0))
+           fd09 Zero = Lp0
+           fd09 (Suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
+           ... | yes _ = fd09 i
+           ... | no _ = {!!}
            an :  Nat
            an = ctl← C (& (dense D)) MD  
            pn : Ordinal
@@ -198,12 +203,25 @@
            pn+1 = find-p L C (Suc an) (& p0)
            fd07 : odef (dense D) pn+1
            fd07 with is-o∅ ( & ( PGHOD an L C (find-p L C an (& p0))) )
-           ... | yes _ = {!!}
-           ... | no _ = {!!}
-           fd09 : (i : Nat ) → odef L (find-p L C i (& p0))
-           fd09 Zero = Lp0
-           fd09 (Suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
-           ... | yes _ = fd09 i
+           ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 ⟪ fd13 , ⟪ fd14 , fd15 ⟫ ⟫ ) ) where
+              fd12 : L ∋ * (find-p L C an (& p0))
+              fd12 = subst (λ k → odef L k) (sym &iso) (fd09 an )
+              fd11 : Ordinal
+              fd11 = & ( dense-f D fd12 )
+              fd13 : L ∋ ( dense-f D fd12 )
+              fd13 = incl (d⊆P D) (  dense-d D fd12 )
+              fd14 : (* (ctl→ C an)) ∋ ( dense-f D fd12 )
+              fd14 = subst (λ k → odef k (& ( dense-f D fd12 ) )) fd16 (  dense-d D fd12 ) where
+                  fd16 : dense D ≡ * (ctl→ C an) 
+                  fd16 = begin dense D ≡⟨ sym *iso ⟩
+                    * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→  C MD )) ⟩
+                    * (ctl→ C an) ∎  where open ≡-Reasoning
+              fd15 :  (y : Ordinal) → odef (* (& (dense-f D fd12))) y → odef (* (find-p L C an (& p0))) y
+              fd15 y lt = subst (λ k → odef  (* (find-p L C an (& p0)))  k ) &iso ( incl (dense-p D  fd12 ) fd16  ) where
+                  fd16 : odef (dense-f D fd12) (& ( * y))
+                  fd16 = subst₂ (λ j k → odef j k ) (*iso) (sym &iso) lt
+              fd10 :  PGHOD an L C (find-p L C an (& p0)) =h= od∅
+              fd10 = ≡o∅→=od∅ y
            ... | no _ = {!!}
            fd03 : odef (PDHOD L p0 C) pn+1
            fd03 = record { gr = Suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (Suc an)} 
@@ -229,7 +247,7 @@
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
 
-record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (G : GenericFilter LP {!!} ) : Set (suc n) where
+record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter LP (ctl-M C) ) : Set (suc n) where
    field
      valx : HOD
 
@@ -246,10 +264,3 @@
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
   ind x valy = record { od = record { def = λ y → valS x y (& (filter (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
 
-
---
---   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
---
-
-
-