src/HOL/simpdata.ML
changeset 4205 96632970d203
parent 4189 b8c7a6bc6c16
child 4320 24d9e6639cd4
     1.1 --- a/src/HOL/simpdata.ML	Wed Nov 12 12:24:55 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Nov 12 12:30:15 1997 +0100
     1.3 @@ -340,11 +340,16 @@
     1.4   (fn _ => [blast_tac (HOL_cs addIs [select_equality]) 1]);
     1.5  
     1.6  qed_goal "expand_if" HOL.thy
     1.7 -    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
     1.8 - (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
     1.9 +    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
    1.10 +	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
    1.11           stac if_P 2,
    1.12           stac if_not_P 1,
    1.13 -         REPEAT(blast_tac HOL_cs 1) ]);
    1.14 +         ALLGOALS (blast_tac HOL_cs)]);
    1.15 +
    1.16 +qed_goal "split_if_asm" HOL.thy
    1.17 +    "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" (K [
    1.18 +	stac expand_if 1,
    1.19 +        blast_tac HOL_cs 1]);
    1.20  
    1.21  qed_goal "if_bool_eq" HOL.thy
    1.22                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    1.23 @@ -364,8 +369,8 @@
    1.24  fun split_inside_tac splits = mktac (map mk_meta_eq splits)
    1.25  end;
    1.26  
    1.27 -val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
    1.28 -					    contrapos2 notnotD;
    1.29 +val split_asm_tac = mk_case_split_asm_tac split_tac 
    1.30 +			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
    1.31  
    1.32  infix 4 addsplits;
    1.33  fun ss addsplits splits = ss addloop (split_tac splits);