src/HOL/simpdata.ML
changeset 6293 2a4357301973
parent 6128 2acc5d36610c
child 6301 08245f5a436d
     1.1 --- a/src/HOL/simpdata.ML	Mon Mar 01 18:11:54 1999 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Mon Mar 01 18:37:23 1999 +0100
     1.3 @@ -356,24 +356,6 @@
     1.4  
     1.5  (** 'if' congruence rules: neither included by default! *)
     1.6  
     1.7 -(*Simplifies x assuming c and y assuming ~c*)
     1.8 -qed_goal "if_cong" HOL.thy
     1.9 -  "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
    1.10 -\  (if b then x else y) = (if c then u else v)"
    1.11 -  (fn rew::prems =>
    1.12 -   [stac rew 1, stac split_if 1, stac split_if 1,
    1.13 -    blast_tac (HOL_cs addDs prems) 1]);
    1.14 -
    1.15 -(*Prevents simplification of x and y: much faster*)
    1.16 -qed_goal "if_weak_cong" HOL.thy
    1.17 -  "b=c ==> (if b then x else y) = (if c then x else y)"
    1.18 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.19 -
    1.20 -(*Prevents simplification of t: much faster*)
    1.21 -qed_goal "let_weak_cong" HOL.thy
    1.22 -  "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
    1.23 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.24 -
    1.25  (*In general it seems wrong to add distributive laws by default: they
    1.26    might cause exponential blow-up.  But imp_disjL has been in for a while
    1.27    and cannot be removed without affecting existing proofs.  Moreover, 
    1.28 @@ -431,6 +413,23 @@
    1.29       addcongs [imp_cong]
    1.30       addsplits [split_if];
    1.31  
    1.32 +(*Simplifies x assuming c and y assuming ~c*)
    1.33 +val prems = Goalw [if_def]
    1.34 +  "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \
    1.35 +\  (if b then x else y) = (if c then u else v)";
    1.36 +by (asm_simp_tac (HOL_ss addsimps prems) 1);
    1.37 +qed "if_cong";
    1.38 +
    1.39 +(*Prevents simplification of x and y: much faster*)
    1.40 +qed_goal "if_weak_cong" HOL.thy
    1.41 +  "b=c ==> (if b then x else y) = (if c then x else y)"
    1.42 +  (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.43 +
    1.44 +(*Prevents simplification of t: much faster*)
    1.45 +qed_goal "let_weak_cong" HOL.thy
    1.46 +  "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
    1.47 +  (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.48 +
    1.49  qed_goal "if_distrib" HOL.thy
    1.50    "f(if c then x else y) = (if c then f x else f y)" 
    1.51    (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);