Theory Proper_Extension

section‹Separative notions and proper extensions›
theory Proper_Extension
  imports
    Names

begin

text‹The key ingredient to obtain a proper extension is to have
a ∗‹separative preorder›:›

locale separative_notion = forcing_notion +
  assumes separative: "p∈P ⟹ ∃q∈P. ∃r∈P. q ≼ p ∧ r ≼ p ∧ q ⊥ r"
begin

text‹For separative preorders, the complement of every filter is
dense. Hence an $M$-generic filter can't belong to the ground model.›

lemma filter_complement_dense:
  assumes "filter(G)" shows "dense(P - G)"
proof
  fix p
  assume "p∈P"
  show "∃d∈P - G. d ≼ p"
  proof (cases "p∈G")
    case True
    note ‹p∈P› assms
    moreover
    obtain q r where "q ≼ p" "r ≼ p" "q ⊥ r" "q∈P" "r∈P" 
      using separative[OF ‹p∈P›]
      by force
    with ‹filter(G)›
    obtain s where "s ≼ p" "s ∉ G" "s ∈ P"
      using filter_imp_compat[of G q r]
      by auto
    then
    show ?thesis by blast
  next
    case False
    with ‹p∈P› 
    show ?thesis using leq_reflI unfolding Diff_def by auto
  qed
qed

end (* separative_notion *)

locale ctm_separative = forcing_data + separative_notion
begin

lemma generic_not_in_M: assumes "M_generic(G)"  shows "G ∉ M"
proof
  assume "G∈M"
  then
  have "P - G ∈ M" 
    using P_in_M Diff_closed by simp
  moreover
  have "¬(∃q∈G. q ∈ P - G)" "(P - G) ⊆ P"
    unfolding Diff_def by auto
  moreover
  note assms
  ultimately
  show "False"
    using filter_complement_dense[of G] M_generic_denseD[of G "P-G"] 
      M_generic_def by simp ― ‹need to put generic ==> filter in claset›
qed

theorem proper_extension: assumes "M_generic(G)" shows "M ≠ M[G]"
  using assms G_in_Gen_Ext[of G] one_in_G[of G] generic_not_in_M
  by force

end (* ctm_separative *)

end