open import Level
open import Ordinals
module filter {n : Level } (O : Ordinals {n})   where

open import zf
open import logic
import OD 

open import Relation.Nullary 
open import Data.Empty 
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
import BAlgbra 

open BAlgbra O

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom

import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O


import ODC
open ODC O

open _∧_
open _∨_
open Bool

-- Kunen p.76 and p.53, we use ⊆
record Filter  ( L : HOD  ) : Set (suc n) where
   field
       filter  : HOD   
       f⊆L     : filter ⊆ L
       filter1 : { p q : HOD } →  L ∋ q → filter ∋ p →  p ⊆ q  → filter ∋ q
       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)

open Filter

record prime-filter { L : HOD } (F : Filter L) : Set (suc (suc n)) where
   field
       proper  : ¬ (filter F ∋ od∅)
       prime   : {p q : HOD } →  filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )

record ultra-filter { L : HOD } (P : HOD ) (F : Filter L) : Set (suc (suc n)) where
   field
       L⊆PP :  L ⊆ Power P
       proper  : ¬ (filter F ∋ od∅)
       ultra   : {p : HOD } → L ∋ p →  ( filter F ∋ p ) ∨ (  filter F ∋ ( P ＼ p) )

open _⊆_

∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p 
∈-filter {L} {p} F lt = {!!} -- power→⊆ L p ( incl ? lt )

∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }

∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }

q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
q∩q⊆q = record { incl = λ lt → proj1 lt } 

open HOD

-----
--
--  ultra filter is prime
--

filter-lemma1 :  {P L : HOD} → (F : Filter L)  → ∀ {p q : HOD } → ultra-filter P F  → prime-filter F 
filter-lemma1 {P} {L} F u = record {
         proper = ultra-filter.proper u
       ; prime = lemma3
    } where
  lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
  lemma3 {p} {q} lt with ultra-filter.ultra u {!!} -- (∪-lemma1 (∈-filter P lt) )
  ... | case1 p∈P  = case1 p∈P
  ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where
    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
    lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
       ;  eq← = λ {x} lt → ⟪  case2 (proj1 lt) , proj2 lt ⟫
      } where
         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
         lemma4 x lt with proj1 lt
         lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
         lemma4 x lt | case2 qx = qx
    lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
    lemma6 = filter2 F lt ¬p∈P
    lemma7 : filter F ∋ (q ∩ (L ＼ p))
    lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!}
    lemma8 : (q ∩ (L ＼ p)) ⊆ q
    lemma8 = q∩q⊆q

-----
--
--  if Filter contains L, prime filter is ultra
--

filter-lemma2 :  {P L : HOD} → (F : Filter L)  → filter F ∋ L → prime-filter F → ultra-filter P F
filter-lemma2 {P} {L} F f∋L prime = record {
         L⊆PP = {!!}
       ; proper = prime-filter.proper prime
       ; ultra = λ {p}  p⊆L → prime-filter.prime prime {!!} -- (lemma p  p⊆L)
   } where
        open _==_
        p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 
        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
        eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
        eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
        lemma : (p : HOD) → p ⊆ L   →  filter F ∋ (p ∪ (P ＼ p))
        lemma p p⊆L = {!!} -- subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L

record Dense  (L : HOD )  : Set (suc n) where
   field
       dense : HOD
       d⊆P :  dense ⊆ L
       dense-f : {p : HOD} → L ∋ p  → HOD
       dense-d :  { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
       dense-p :  { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p  

record Ideal  ( L : HOD  ) : Set (suc n) where
   field
       ideal : HOD   
       i⊆L :  ideal ⊆ L 
       ideal1 : { p q : HOD } →  L ∋ q  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)

open Ideal

proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
proper-ideal {L} P {p} = ideal P ∋ od∅

prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )


record GenericFilter (L : HOD) : Set (suc n) where
    field
       genf : Filter L
       generic : (D : Dense L ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )