src/HOL/simpdata.ML
changeset 965 24eef3860714
parent 941 f8a202891ac9
child 988 8317adb1c444
     1.1 --- a/src/HOL/simpdata.ML	Fri Mar 17 22:46:26 1995 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Mon Mar 20 15:35:28 1995 +0100
     1.3 @@ -71,27 +71,28 @@
     1.4  
     1.5  val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
     1.6  
     1.7 -val if_True = prove_goalw HOL.thy [if_def] "if True x y = x"
     1.8 +val if_True = prove_goalw HOL.thy [if_def] "(if True then x else y) = x"
     1.9   (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
    1.10  
    1.11 -val if_False = prove_goalw HOL.thy [if_def] "if False x y = y"
    1.12 +val if_False = prove_goalw HOL.thy [if_def] "(if False then x else y) = y"
    1.13   (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
    1.14  
    1.15 -val if_P = prove_goal HOL.thy "P ==> if P x y = x"
    1.16 +val if_P = prove_goal HOL.thy "P ==> (if P then x else y) = x"
    1.17   (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
    1.18  
    1.19 -val if_not_P = prove_goal HOL.thy "~P ==> if P x y = y"
    1.20 +val if_not_P = prove_goal HOL.thy "~P ==> (if P then x else y) = y"
    1.21   (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
    1.22  
    1.23  val expand_if = prove_goal HOL.thy
    1.24 -    "P(if Q x y) = ((Q --> P(x)) & (~Q --> P(y)))"
    1.25 +    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
    1.26   (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
    1.27  	 rtac (if_P RS ssubst) 2,
    1.28  	 rtac (if_not_P RS ssubst) 1,
    1.29  	 REPEAT(fast_tac HOL_cs 1) ]);
    1.30  
    1.31 -val if_bool_eq = prove_goal HOL.thy "if P Q R = ((P-->Q) & (~P-->R))"
    1.32 -  (fn _ => [rtac expand_if 1]);
    1.33 +val if_bool_eq = prove_goal HOL.thy
    1.34 +                   "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.35 +                   (fn _ => [rtac expand_if 1]);
    1.36  
    1.37  infix addcongs;
    1.38  fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
    1.39 @@ -99,7 +100,7 @@
    1.40  val mksimps_pairs =
    1.41    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    1.42     ("All", [spec]), ("True", []), ("False", []),
    1.43 -   ("if", [if_bool_eq RS iffD1])];
    1.44 +   ("If", [if_bool_eq RS iffD1])];
    1.45  
    1.46  fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
    1.47  
    1.48 @@ -139,14 +140,15 @@
    1.49  
    1.50  (*Simplifies x assuming c and y assuming ~c*)
    1.51  val if_cong = prove_goal HOL.thy
    1.52 -  "[| b=c; c ==> x=u; ~c ==> y=v |] ==> if b x y = if c u v"
    1.53 +  "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
    1.54 +\  (if b then x else y) = (if c then u else v)"
    1.55    (fn rew::prems =>
    1.56     [stac rew 1, stac expand_if 1, stac expand_if 1,
    1.57      fast_tac (HOL_cs addDs prems) 1]);
    1.58  
    1.59  (*Prevents simplification of x and y: much faster*)
    1.60  val if_weak_cong = prove_goal HOL.thy
    1.61 -  "b=c ==> if b x y = if c x y"
    1.62 +  "b=c ==> (if b then x else y) = (if c then x else y)"
    1.63    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.64  
    1.65  (*Prevents simplification of t: much faster*)