prod.ML

--- a/prod.ML	Thu Sep 16 14:29:14 1993 +0200
+++ b/prod.ML	Wed Sep 22 15:43:05 1993 +0200
@@ -58,17 +58,21 @@
 by (rtac refl 1);
 val split = result();
 
-(*FIXME: split's congruence rule should only simplifies the pair*)
 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split];
 
+(*Prevents simplification of c: much faster*)
+val split_weak_cong = prove_goal Prod.thy
+  "p=q ==> split(p,c) = split(q,c)"
+  (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
 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 pair_ss 1);
 val surjective_pairing = result();
 
 goal Prod.thy "p = split(p, %x y.<x,y>)";
 by (res_inst_tac [("p","p")] PairE 1);
-by(asm_simp_tac pair_ss 1);
+by (asm_simp_tac pair_ss 1);
 val surjective_pairing2 = result();
 
 (** split used as a logical connective, with result type bool **)
@@ -99,13 +103,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 (pair_ss addsimps [prod_fun,o_def]) 1);
 val prod_fun_compose = result();
 
 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 (pair_ss addsimps [prod_fun]) 1);
 val prod_fun_ident = result();
 
 val prems = goal Prod.thy "<a,b>:r ==> <f(a),g(b)> : prod_fun(f,g)``r";