src/HOL/simpdata.ML
 changeset 4769 bb60149fe21b parent 4744 4469d498cd48 child 4794 9db0916ecdae
```     1.1 --- a/src/HOL/simpdata.ML	Thu Apr 02 13:47:03 1998 +0200
1.2 +++ b/src/HOL/simpdata.ML	Thu Apr 02 13:48:28 1998 +0200
1.3 @@ -57,7 +57,7 @@
1.4
1.5  local
1.6
1.7 -  fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]);
1.8 +  fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
1.9
1.10    val P_imp_P_iff_True = prover "P --> (P = True)" RS mp;
1.11    val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
1.12 @@ -133,7 +133,7 @@
1.13
1.14  val imp_cong = impI RSN
1.15      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
1.16 -        (fn _=> [blast_tac HOL_cs 1]) RS mp RS mp);
1.17 +        (fn _=> [Blast_tac 1]) RS mp RS mp);
1.18
1.19  (*Miniscoping: pushing in existential quantifiers*)
1.20  val ex_simps = map prover
1.21 @@ -175,7 +175,7 @@
1.22            METAHYPS (fn prems => resolve_tac prems 1) 1,
1.23            rtac TrueI 1]);
1.24
1.25 -fun prove nm thm  = qed_goal nm HOL.thy thm (K [blast_tac HOL_cs 1]);
1.26 +fun prove nm thm  = qed_goal nm HOL.thy thm (K [Blast_tac 1]);
1.27
1.28  prove "conj_commute" "(P&Q) = (Q&P)";
1.29  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
1.30 @@ -228,19 +228,19 @@
1.31
1.32  let val th = prove_goal HOL.thy
1.33                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
1.34 -                (fn _=> [blast_tac HOL_cs 1])
1.35 +                (fn _=> [Blast_tac 1])
1.36  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
1.37
1.38  let val th = prove_goal HOL.thy
1.39                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
1.40 -                (fn _=> [blast_tac HOL_cs 1])
1.41 +                (fn _=> [Blast_tac 1])
1.42  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
1.43
1.44  (* '|' congruence rule: not included by default! *)
1.45
1.46  let val th = prove_goal HOL.thy
1.47                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
1.48 -                (fn _=> [blast_tac HOL_cs 1])
1.49 +                (fn _=> [Blast_tac 1])
1.50  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
1.51
1.52  prove "eq_sym_conv" "(x=y) = (y=x)";
1.53 @@ -268,16 +268,23 @@
1.54  	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
1.55           stac if_P 2,
1.56           stac if_not_P 1,
1.57 -         ALLGOALS (blast_tac HOL_cs)]);
1.58 +         ALLGOALS (Blast_tac)]);
1.59
1.60  qed_goal "split_if_asm" HOL.thy
1.61 -    "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" (K [
1.62 -	stac expand_if 1,
1.63 -        blast_tac HOL_cs 1]);
1.64 +    "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
1.65 +    (K [stac expand_if 1,
1.66 +	Blast_tac 1]);
1.67
1.68 -qed_goal "if_bool_eq" HOL.thy
1.69 -                   "(if P then Q else R) = ((P-->Q) & (~P-->R))"
1.70 -                   (K [rtac expand_if 1]);
1.71 +(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
1.72 +qed_goal "if_bool_eq_conj" HOL.thy
1.73 +    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
1.74 +    (K [rtac expand_if 1]);
1.75 +
1.76 +(*And this form is useful for expanding IFs on the LEFT*)
1.77 +qed_goal "if_bool_eq_disj" HOL.thy
1.78 +    "(if P then Q else R) = ((P&Q) | (~P&R))"
1.79 +    (K [stac expand_if 1,
1.80 +	Blast_tac 1]);
1.81
1.82
1.83  (*** make simplification procedures for quantifier elimination ***)
1.84 @@ -354,10 +361,10 @@
1.85  fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
1.86
1.87  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
1.88 -  (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
1.89 +  (K [split_tac [expand_if] 1, Blast_tac 1]);
1.90
1.91  qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
1.92 -  (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
1.93 +  (K [split_tac [expand_if] 1, Blast_tac 1]);
1.94
1.95  (** 'if' congruence rules: neither included by default! *)
1.96
1.97 @@ -388,7 +395,7 @@
1.98  val mksimps_pairs =
1.99    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
1.100     ("All", [spec]), ("True", []), ("False", []),
1.101 -   ("If", [if_bool_eq RS iffD1])];
1.102 +   ("If", [if_bool_eq_conj RS iffD1])];
1.103
1.104  fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
1.105  				 atac, etac FalseE];
```