Theory Proper_Extension

sectionSeparative notions and proper extensions
theory Proper_Extension
  imports
    Names

begin

textThe key ingredient to obtain a proper extension is to have
a separative preorder:

locale separative_notion = forcing_notion +
  assumes separative: "p  q. r. q  p  r  p  q  r"
begin

textFor separative preorders, the complement of every filter is
dense. Hence an $M$-generic filter cannot belong to the ground model.

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

end ― ‹localeseparative_notion

locale ctm_separative = forcing_data1 + separative_notion
begin

context
  fixes G
  assumes generic: "M_generic(G)"
begin

interpretation G_generic1  leq 𝟭 M enum G
  by unfold_locales (simp add:generic)

lemma generic_not_in_M:
  shows "G  M"
proof
  assume "GM"
  then
  have " - G  M"
    using Diff_closed by simp
  moreover
  have "¬(qG. q   - G)" "( - G)  "
    unfolding Diff_def by auto
  moreover
  note generic
  ultimately
  show "False"
    using filter_complement_dense[of G] M_generic_denseD[of "-G"]
    by auto
qed

theorem proper_extension: "M  M[G]"
  using generic G_in_Gen_Ext one_in_G generic_not_in_M
  by force
end
end ― ‹localectm_separative

end