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];