moved split_tac
authoroheimb
Wed Nov 27 20:36:33 1996 +0100 (1996-11-27)
changeset 2263c741309167bf
parent 2262 c7ee913746fd
child 2264 f298678bd54a
moved split_tac
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Wed Nov 27 17:00:25 1996 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Nov 27 20:36:33 1996 +0100
     1.3 @@ -262,6 +262,17 @@
     1.4                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
     1.5                     (fn _ => [rtac expand_if 1]);
     1.6  
     1.7 +local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
     1.8 +in
     1.9 +fun split_tac splits = mktac (map mk_meta_eq splits)
    1.10 +end;
    1.11 +
    1.12 +local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
    1.13 +in
    1.14 +fun split_inside_tac splits = mktac (map mk_meta_eq splits)
    1.15 +end;
    1.16 +
    1.17 +
    1.18  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    1.19    (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
    1.20  
    1.21 @@ -308,17 +319,6 @@
    1.22        addcongs [imp_cong];
    1.23  
    1.24  
    1.25 -local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
    1.26 -in
    1.27 -fun split_tac splits = mktac (map mk_meta_eq splits)
    1.28 -end;
    1.29 -
    1.30 -local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
    1.31 -in
    1.32 -fun split_inside_tac splits = mktac (map mk_meta_eq splits)
    1.33 -end;
    1.34 -
    1.35 -
    1.36  qed_goal "if_distrib" HOL.thy
    1.37    "f(if c then x else y) = (if c then f x else f y)" 
    1.38    (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);