# HG changeset patch
# User paulson
# Date 920309843 -3600
# Node ID 2a435730197388d652fa2488aaeede73f025c304
# Parent  e50e1142dd062ab4af5690aba4a3f10923f513bf
simpler proofs of congruence rules

diff -r e50e1142dd06 -r 2a4357301973 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Mon Mar 01 18:11:54 1999 +0100
+++ b/src/HOL/simpdata.ML	Mon Mar 01 18:37:23 1999 +0100
@@ -356,24 +356,6 @@
 
 (** 'if' congruence rules: neither included by default! *)
 
-(*Simplifies x assuming c and y assuming ~c*)
-qed_goal "if_cong" HOL.thy
-  "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
-\  (if b then x else y) = (if c then u else v)"
-  (fn rew::prems =>
-   [stac rew 1, stac split_if 1, stac split_if 1,
-    blast_tac (HOL_cs addDs prems) 1]);
-
-(*Prevents simplification of x and y: much faster*)
-qed_goal "if_weak_cong" HOL.thy
-  "b=c ==> (if b then x else y) = (if c then x else y)"
-  (fn [prem] => [rtac (prem RS arg_cong) 1]);
-
-(*Prevents simplification of t: much faster*)
-qed_goal "let_weak_cong" HOL.thy
-  "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
-  (fn [prem] => [rtac (prem RS arg_cong) 1]);
-
 (*In general it seems wrong to add distributive laws by default: they
   might cause exponential blow-up.  But imp_disjL has been in for a while
   and cannot be removed without affecting existing proofs.  Moreover, 
@@ -431,6 +413,23 @@
      addcongs [imp_cong]
      addsplits [split_if];
 
+(*Simplifies x assuming c and y assuming ~c*)
+val prems = Goalw [if_def]
+  "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \
+\  (if b then x else y) = (if c then u else v)";
+by (asm_simp_tac (HOL_ss addsimps prems) 1);
+qed "if_cong";
+
+(*Prevents simplification of x and y: much faster*)
+qed_goal "if_weak_cong" HOL.thy
+  "b=c ==> (if b then x else y) = (if c then x else y)"
+  (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
+(*Prevents simplification of t: much faster*)
+qed_goal "let_weak_cong" HOL.thy
+  "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
+  (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)" 
   (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);