Prod.ML

 goalw Prod.thy [split_def] "split(<a,b>, c) = c(a,b)";
 by (sstac [fst_conv, snd_conv] 1);
 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 **)
 
 val prems = goal Prod.thy "c(a,b) ==> split(<a,b>, c)";

 
 goal Prod.thy 
     "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";
 by (rtac image_eqI 1);
 by (rtac (prod_fun RS sym) 1);