src/HOL/simpdata.ML
changeset 4830 bd73675adbed
parent 4794 9db0916ecdae
child 4930 89271bc4e7ed
     1.1 --- a/src/HOL/simpdata.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -209,7 +209,7 @@
     1.4  prove "disj_not1" "(~P | Q) = (P --> Q)";
     1.5  prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
     1.6  
     1.7 -(*Avoids duplication of subgoals after expand_if, when the true and false 
     1.8 +(*Avoids duplication of subgoals after split_if, when the true and false 
     1.9    cases boil down to the same thing.*) 
    1.10  prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
    1.11  
    1.12 @@ -261,27 +261,29 @@
    1.13  qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
    1.14   (K [Blast_tac 1]);
    1.15  
    1.16 -qed_goal "expand_if" HOL.thy
    1.17 +qed_goal "split_if" HOL.thy
    1.18      "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
    1.19  	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
    1.20           stac if_P 2,
    1.21           stac if_not_P 1,
    1.22           ALLGOALS (Blast_tac)]);
    1.23 +(* for backwards compatibility: *)
    1.24 +val expand_if = split_if;
    1.25  
    1.26  qed_goal "split_if_asm" HOL.thy
    1.27      "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
    1.28 -    (K [stac expand_if 1,
    1.29 +    (K [stac split_if 1,
    1.30  	Blast_tac 1]);
    1.31  
    1.32  (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
    1.33  qed_goal "if_bool_eq_conj" HOL.thy
    1.34      "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.35 -    (K [rtac expand_if 1]);
    1.36 +    (K [rtac split_if 1]);
    1.37  
    1.38  (*And this form is useful for expanding IFs on the LEFT*)
    1.39  qed_goal "if_bool_eq_disj" HOL.thy
    1.40      "(if P then Q else R) = ((P&Q) | (~P&R))"
    1.41 -    (K [stac expand_if 1,
    1.42 +    (K [stac split_if 1,
    1.43  	Blast_tac 1]);
    1.44  
    1.45  
    1.46 @@ -359,10 +361,10 @@
    1.47  fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
    1.48  
    1.49  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    1.50 -  (K [split_tac [expand_if] 1, Blast_tac 1]);
    1.51 +  (K [split_tac [split_if] 1, Blast_tac 1]);
    1.52  
    1.53  qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
    1.54 -  (K [split_tac [expand_if] 1, Blast_tac 1]);
    1.55 +  (K [split_tac [split_if] 1, Blast_tac 1]);
    1.56  
    1.57  (** 'if' congruence rules: neither included by default! *)
    1.58  
    1.59 @@ -371,7 +373,7 @@
    1.60    "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
    1.61  \  (if b then x else y) = (if c then u else v)"
    1.62    (fn rew::prems =>
    1.63 -   [stac rew 1, stac expand_if 1, stac expand_if 1,
    1.64 +   [stac rew 1, stac split_if 1, stac split_if 1,
    1.65      blast_tac (HOL_cs addDs prems) 1]);
    1.66  
    1.67  (*Prevents simplification of x and y: much faster*)
    1.68 @@ -418,11 +420,11 @@
    1.69       @ ex_simps @ all_simps @ simp_thms)
    1.70       addsimprocs [defALL_regroup,defEX_regroup]
    1.71       addcongs [imp_cong]
    1.72 -     addsplits [expand_if];
    1.73 +     addsplits [split_if];
    1.74  
    1.75  qed_goal "if_distrib" HOL.thy
    1.76    "f(if c then x else y) = (if c then f x else f y)" 
    1.77 -  (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    1.78 +  (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
    1.79  
    1.80  qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
    1.81    (K [rtac ext 1, rtac refl 1]);