Prod.ML

--- a/Prod.ML	Mon Feb 13 15:12:08 1995 +0100
+++ b/Prod.ML	Thu Feb 16 08:56:21 1995 +0100
@@ -58,12 +58,12 @@
 by (rtac refl 1);
 qed "split";
 
-val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
+val prod_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (res_inst_tac[("p","s")] PairE 1);
 by (res_inst_tac[("p","t")] PairE 1);
-by (asm_simp_tac pair_ss 1);
+by (asm_simp_tac prod_ss 1);
 qed "Pair_fst_snd_eq";
 
 (*Prevents simplification of c: much faster*)
@@ -71,14 +71,15 @@
   "p=q ==> split(c,p) = split(c,q)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
+(* Do not add as rewrite rule: invalidates some proofs in IMP *)
 goal Prod.thy "p = <fst(p),snd(p)>";
 by (res_inst_tac [("p","p")] PairE 1);
-by (asm_simp_tac pair_ss 1);
+by (asm_simp_tac prod_ss 1);
 qed "surjective_pairing";
 
 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);
+by (asm_simp_tac prod_ss 1);
 qed "surjective_pairing2";
 
 (*For use with split_tac and the simplifier*)
@@ -94,7 +95,7 @@
   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);
+by (asm_simp_tac prod_ss 1);
 qed "splitI";
 
 val prems = goalw Prod.thy [split_def]
@@ -107,7 +108,7 @@
 qed "splitD";
 
 goal Prod.thy "!!a b c. z: c(a,b) ==> z: split(c, <a,b>)";
-by (asm_simp_tac pair_ss 1);
+by (asm_simp_tac prod_ss 1);
 qed "mem_splitI";
 
 val prems = goalw Prod.thy [split_def]
@@ -125,13 +126,13 @@
     "prod_fun(f1 o f2, g1 o g2) = (prod_fun(f1,g1) o prod_fun(f2,g2))";
 by (rtac ext 1);
 by (res_inst_tac [("p","x")] PairE 1);
-by (asm_simp_tac (pair_ss addsimps [prod_fun,o_def]) 1);
+by (asm_simp_tac (prod_ss addsimps [prod_fun,o_def]) 1);
 qed "prod_fun_compose";
 
 goal Prod.thy "prod_fun(%x.x, %y.y) = (%z.z)";
 by (rtac ext 1);
 by (res_inst_tac [("p","z")] PairE 1);
-by (asm_simp_tac (pair_ss addsimps [prod_fun]) 1);
+by (asm_simp_tac (prod_ss addsimps [prod_fun]) 1);
 qed "prod_fun_ident";
 
 val prems = goal Prod.thy "<a,b>:r ==> <f(a),g(b)> : prod_fun(f,g)``r";
@@ -234,5 +235,3 @@
                      addSEs [SigmaE2, SigmaE, mem_splitE, 
 			     fst_imageE, snd_imageE, prod_fun_imageE,
 			     Pair_inject];
-
-val prod_ss = pair_ss;