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