--- 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