HOL/Prod: swapped args of split and simplified
HOL/Prod/mem_splitI, mem_splitE, prod_cs: new

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

--- a/Prod.thy	Thu Aug 18 12:23:52 1994 +0200
+++ b/Prod.thy	Thu Aug 18 12:38:12 1994 +0200
@@ -27,7 +27,7 @@
   Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
   fst	   :: "'a * 'b => 'a"
   snd	   :: "'a * 'b => 'b"
-  split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
+  split    :: "[['a,'b]=>'c, 'a * 'b] => 'c"
   prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
   Pair	   :: "['a,'b] => 'a * 'b"
   "@Tuple" :: "args => 'a*'b"			("(1<_>)")
@@ -56,8 +56,8 @@
   Pair_def         "Pair(a,b) == Abs_Prod(Pair_Rep(a,b))"
   fst_def          "fst(p) == @a. ? b. p = <a,b>"
   snd_def          "snd(p) == @b. ? a. p = <a,b>"
-  split_def        "split(p,c) == c(fst(p),snd(p))"
-  prod_fun_def     "prod_fun(f,g) == (%z.split(z, %x y.<f(x), g(y)>))"
+  split_def        "split(c,p) == c(fst(p),snd(p))"
+  prod_fun_def     "prod_fun(f,g) == split(%x y.<f(x), g(y)>)"
   Sigma_def        "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
 
   Unit_def         "Unit == {p. p=True}"