Theory Foundation_Axiom

section‹The Axiom of Foundation in $M[G]$›

theory Foundation_Axiom
  imports
    Names
begin

context forcing_data1
begin

(* Slick proof essentially by Paulson (adapted from L) *)
lemma foundation_in_MG : "foundation_ax(##(M[G]))"
  unfolding foundation_ax_def
  by (rule rallI, cut_tac A=x in foundation, auto intro: transitivity_MG)

(* Same theorem as above, declarative proof,
   without using transitivity *)
lemma "foundation_ax(##(M[G]))"
proof -
  {
    fix x
    assume "x∈M[G]" "∃y∈M[G] . y∈x"
    then
    have "∃y∈M[G] . y∈x∩M[G]"
      by simp
    then
    obtain y where "y∈x∩M[G]" "∀z∈y. z ∉ x∩M[G]"
      using foundation[of "x∩M[G]"]  by blast
    then
    have "∃y∈M[G] . y ∈ x ∧ (∀z∈M[G] . z ∉ x ∨ z ∉ y)"
      by auto
  }
  then
  show ?thesis
    unfolding foundation_ax_def by auto
qed

end ― ‹\<^locale>‹forcing_data1››

end