Theory Foundation_Axiom

section‹The Axiom of Foundation in $M[G]$›
theory Foundation_Axiom
imports
  Names
begin

context forcing_data
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  (* context forcing_data *)
end