# HG changeset patch
# User oheimb
# Date 878672985 -3600
# Node ID 5c6cb2a258169d0fd944cda2a87eb8fbb7d00e0e
# Parent  0a08c2b9b1edb7617ab6d42f03ddd6027debeddb
added several theorems

diff -r 0a08c2b9b1ed -r 5c6cb2a25816 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Tue Nov 04 20:48:38 1997 +0100
+++ b/src/HOL/Prod.ML	Tue Nov 04 20:49:45 1997 +0100
@@ -54,6 +54,8 @@
 by (REPEAT (eresolve_tac [prem,exE] 1));
 qed "PairE";
 
+fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
+
 (* replace parameters of product type by individual component parameters *)
 local
 fun is_pair (_,Type("*",_)) = true
@@ -133,6 +135,9 @@
 by (rtac refl 1);
 qed "split";
 
+val split_select = prove_goalw Prod.thy [split_def] 
+	"(®(x,y). P x y) = (®xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
+
 Addsimps [fst_conv, snd_conv, split];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
@@ -157,9 +162,16 @@
 by (Asm_simp_tac 1);
 qed "surjective_pairing2";
 
+val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
+	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
+Addsimps [surj_pair];
+
 qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
   (fn _ => [rtac ext 1, split_all_tac 1, rtac split 1]);
 
+val split_beta = prove_goal Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
+	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
+
 (*For use with split_tac and the simplifier*)
 goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
 by (stac surjective_pairing 1);
@@ -192,6 +204,12 @@
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
 qed "splitE";
 
+val splitE2 = prove_goal Prod.thy 
+"[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
+	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
+	rtac (split_beta RS subst) 1,
+	rtac (hd prems) 1]);
+
 goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
 by (etac (split RS iffD1) 1);
 qed "splitD";
@@ -306,6 +324,9 @@
 qed "mem_Sigma_iff";
 AddIffs [mem_Sigma_iff]; 
 
+val Collect_Prod = prove_goal Prod.thy 
+	"{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]);
+Addsimps [Collect_Prod];
 
 (*Suggested by Pierre Chartier*)
 goal Prod.thy