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)