theory Gen_ext_pair imports Names Forcing_data begin
context M_extra_assms
begin
lemma one_in_M : "one ∈ M"
by (insert trans_M,insert one_in_P,insert P_in_M,rule Transset_intf)
lemma pairs_in_M :
" ⟦ a ∈ M ; b ∈ M ; c ∈ M ; d ∈ M ⟧ ⟹ {⟨a,c⟩,⟨b,d⟩} ∈ M"
by (unfold Pair_def, ((rule upairM)+,assumption+)+)
lemma sigma_in_M :
"one ∈ G ⟹ τ ∈ M ⟹ ρ ∈ M ⟹ {⟨τ,one⟩,⟨ρ,one⟩} ∈ M"
by (rule pairs_in_M,simp_all add: upair_ax_def one_in_M)
lemma valsigma :
"one ∈ G ⟹ {⟨τ,one⟩,⟨ρ,one⟩} ∈ M ⟹
val(G,{⟨τ,one⟩,⟨ρ,one⟩}) = {val(G,τ),val(G,ρ)}"
apply (insert one_in_P)
apply (rule trans)
apply (rule def_val,assumption)
apply (auto simp add: Sep_and_Replace)
done
lemma pairing_axiom :
"one ∈ G ⟹ upair_ax(##M[G])"
apply (simp add: upair_ax_def)
apply (rule ballI)+
apply (drule GenExtD)+
apply (rule bexE,assumption)
apply (rule_tac A="M" and P="λw. y=val(G,w)" in bexE,assumption)
apply (rename_tac x y τ ρ)
apply (rule_tac x="val(G,{⟨τ,one⟩,⟨ρ,one⟩})" in bexI)
apply (subst valsigma,assumption+)
defer 1 apply (simp add: upair_def)
apply (rule GenExtI)
apply (insert sigma_in_M,simp_all add: upair_ax_def)
done
end
end