Prod.ML

--- a/Prod.ML	Thu Aug 18 12:23:52 1994 +0200
+++ b/Prod.ML	Thu Aug 18 12:38:12 1994 +0200
@@ -53,7 +53,7 @@
 by (REPEAT (eresolve_tac [prem,exE] 1));
 val PairE = result();
 
-goalw Prod.thy [split_def] "split(<a,b>, c) = c(a,b)";
+goalw Prod.thy [split_def] "split(c, <a,b>) = c(a,b)";
 by (sstac [fst_conv, snd_conv] 1);
 by (rtac refl 1);
 val split = result();
@@ -68,7 +68,7 @@
 
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy
-  "p=q ==> split(p,c) = split(q,c)"
+  "p=q ==> split(c,p) = split(c,q)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
 goal Prod.thy "p = <fst(p),snd(p)>";
@@ -76,29 +76,41 @@
 by (asm_simp_tac pair_ss 1);
 val surjective_pairing = result();
 
-goal Prod.thy "p = split(p, %x y.<x,y>)";
+goal Prod.thy "p = split(%x y.<x,y>, p)";
 by (res_inst_tac [("p","p")] PairE 1);
 by (asm_simp_tac pair_ss 1);
 val surjective_pairing2 = result();
 
-(** split used as a logical connective, with result type bool **)
-
-val prems = goal Prod.thy "c(a,b) ==> split(<a,b>, c)";
-by (stac split 1);
-by (resolve_tac prems 1);
-val splitI = result();
-
-val prems = goalw Prod.thy [split_def]
-    "[| split(p,c);  !!x y. [| p = <x,y>;  c(x,y) |] ==> Q |] ==> Q";
-by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
-val splitE = result();
-
-goal Prod.thy "R(split(p,c)) = (! x y. p = <x,y> --> R(c(x,y)))";
+(*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);
 by (stac split 1);
 by (fast_tac (HOL_cs addSEs [Pair_inject]) 1);
 val expand_split = result();
 
+(** split used as a logical connective or set former **)
+
+(*These rules are for use with fast_tac.
+  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
+
+goal Prod.thy "!!a b c. c(a,b) ==> split(c, <a,b>)";
+by (asm_simp_tac pair_ss 1);
+val splitI = result();
+
+val prems = goalw Prod.thy [split_def]
+    "[| split(c,p);  !!x y. [| p = <x,y>;  c(x,y) |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+val splitE = result();
+
+goal Prod.thy "!!a b c. z: c(a,b) ==> z: split(c, <a,b>)";
+by (asm_simp_tac pair_ss 1);
+val mem_splitI = result();
+
+val prems = goalw Prod.thy [split_def]
+    "[| z: split(c,p);  !!x y. [| p = <x,y>;  z: c(x,y) |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+val mem_splitE = result();
+
 (*** prod_fun -- action of the product functor upon functions ***)
 
 goalw Prod.thy [prod_fun_def] "prod_fun(f,g,<a,b>) = <f(a),g(b)>";
@@ -212,3 +224,11 @@
 by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
 by (rtac (Rep_Unit_inverse RS sym) 1);
 val unit_eq = result();
+
+val prod_cs = set_cs addSIs [SigmaI, mem_splitI] 
+                     addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
+                     addSEs [SigmaE2, SigmaE, mem_splitE, 
+			     fst_imageE, snd_imageE, prod_fun_imageE,
+			     Pair_inject];
+
+val prod_ss = pair_ss;