Theory Foundation_Axiom

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: Transset_M [OF Transset_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
end