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 "xM[G]" "yM[G] . yx"
    then
    have "yM[G] . yxM[G]"
      by simp
    then
    obtain y where "yxM[G]" "zy. z  xM[G]"
      using foundation[of "xM[G]"]  by blast
    then
    have "yM[G] . y  x  (zM[G] . z  x  z  y)"
      by auto
  }
  then
  show ?thesis
    unfolding foundation_ax_def by auto
qed

end ― ‹localeforcing_data1

end