extended addsplits and delsplits to handle also split rules for assumptions
authoroheimb
Thu May 14 16:50:09 1998 +0200 (1998-05-14 ago)
changeset 493089271bc4e7ed
parent 4929 bc3ec5af8593
child 4931 2ec84dee7911
extended addsplits and delsplits to handle also split rules for assumptions
extended const_of_split_thm, renamed it to split_thm_info
NEWS
src/FOL/simpdata.ML
src/HOL/simpdata.ML
src/Provers/splitter.ML
     1.1 --- a/NEWS	Thu May 14 16:44:04 1998 +0200
     1.2 +++ b/NEWS	Thu May 14 16:50:09 1998 +0200
     1.3 @@ -97,8 +97,8 @@
     1.4    remove it in a specific call of the simplifier using
     1.5    `... delsplits [split_if]'.
     1.6    You can also add/delete other case splitting rules to/from the default
     1.7 -  simpset: every datatype generates a suitable rule `split_t_case' (where t
     1.8 -  is the name of the datatype).
     1.9 +  simpset: every datatype generates suitable rules `split_t_case' and
    1.10 +  `split_t_case_asm' (where t is the name of the datatype).
    1.11  
    1.12  * new theory Vimage (inverse image of a function, syntax f-``B);
    1.13  
    1.14 @@ -267,19 +267,16 @@
    1.15         (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
    1.16       )
    1.17  
    1.18 -  which can be added to a simpset via `addsplits'. The existing theorems
    1.19 -  expand_list_case and expand_option_case have been renamed to
    1.20 -  split_list_case and split_option_case.
    1.21 -
    1.22 -  Additionally, there is a theorem `split_t_case_asm' of the form
    1.23 +  and a theorem `split_t_case_asm' of the form
    1.24  
    1.25    P(t_case f1 ... fn x) =
    1.26      ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
    1.27          ...
    1.28         (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
    1.29       )
    1.30 -
    1.31 -  it be used with the new `split_asm_tac'.
    1.32 +  which can be added to a simpset via `addsplits'. The existing theorems
    1.33 +  expand_list_case and expand_option_case have been renamed to
    1.34 +  split_list_case and split_option_case.
    1.35  
    1.36  * HOL/Arithmetic:
    1.37    - `pred n' is automatically converted to `n-1'.
     2.1 --- a/src/FOL/simpdata.ML	Thu May 14 16:44:04 1998 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Thu May 14 16:50:09 1998 +0200
     2.3 @@ -264,13 +264,20 @@
     2.4  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
     2.5  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
     2.6  
     2.7 -infix 4 addsplits;
     2.8 +infix 4 addsplits delsplits;
     2.9  fun ss addsplits splits =
    2.10 -  let fun addsplit(ss,split) =
    2.11 -        let val name = "split " ^ const_of_split_thm split
    2.12 -        in ss addloop (name,split_tac [split]) end
    2.13 +  let fun addsplit (ss,split) =
    2.14 +        let val (name,asm) = split_thm_info split 
    2.15 +        in ss addloop (name ^ (if asm then " asm" else ""),
    2.16 +		       (if asm then split_asm_tac else split_tac) [split]) end
    2.17    in foldl addsplit (ss,splits) end;
    2.18  
    2.19 +fun ss delsplits splits =
    2.20 +  let fun delsplit(ss,split) =
    2.21 +        let val (name,asm) = split_thm_info split 
    2.22 +        in ss delloop (name ^ (if asm then " asm" else "")) end
    2.23 +  in foldl delsplit (ss,splits) end;
    2.24 +
    2.25  val IFOL_simps =
    2.26     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    2.27      imp_simps @ iff_simps @ quant_simps;
     3.1 --- a/src/HOL/simpdata.ML	Thu May 14 16:44:04 1998 +0200
     3.2 +++ b/src/HOL/simpdata.ML	Thu May 14 16:50:09 1998 +0200
     3.3 @@ -346,15 +346,16 @@
     3.4  infix 4 addsplits delsplits;
     3.5  
     3.6  fun ss addsplits splits =
     3.7 -  let fun addsplit(ss,split) =
     3.8 -        let val name = "split " ^ const_of_split_thm split
     3.9 -        in ss addloop (name,split_tac [split]) end
    3.10 +  let fun addsplit (ss,split) =
    3.11 +        let val (name,asm) = split_thm_info split 
    3.12 +        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
    3.13 +		       (if asm then split_asm_tac else split_tac) [split]) end
    3.14    in foldl addsplit (ss,splits) end;
    3.15  
    3.16  fun ss delsplits splits =
    3.17    let fun delsplit(ss,split) =
    3.18 -        let val name = "split " ^ const_of_split_thm split
    3.19 -        in ss delloop name end
    3.20 +        let val (name,asm) = split_thm_info split 
    3.21 +        in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
    3.22    in foldl delsplit (ss,splits) end;
    3.23  
    3.24  fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
     4.1 --- a/src/Provers/splitter.ML	Thu May 14 16:44:04 1998 +0200
     4.2 +++ b/src/Provers/splitter.ML	Thu May 14 16:50:09 1998 +0200
     4.3 @@ -279,14 +279,13 @@
     4.4  
     4.5  in split_tac end;
     4.6  
     4.7 -(* FIXME: this junk is only HOL specific and should therefore not go here! *)
     4.8 -(* const_of_split_thm is used in HOL/simpdata.ML *)
     4.9 -
    4.10 -fun const_of_split_thm thm =
    4.11 +(* FIXME: this junk is only FOL/HOL specific and should therefore not go here!*)
    4.12 +(* split_thm_info is used in FOL/simpdata.ML and HOL/simpdata.ML *)
    4.13 +fun split_thm_info thm =
    4.14    (case concl_of thm of
    4.15 -     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$_) =>
    4.16 +     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$c) =>
    4.17          (case strip_comb t of
    4.18 -           (Const(a,_),_) => a
    4.19 +           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
    4.20           | _              => split_format_err())
    4.21     | _ => split_format_err());
    4.22  
    4.23 @@ -303,7 +302,7 @@
    4.24  
    4.25  fun split_asm_tac []     = K no_tac
    4.26    | split_asm_tac splits = 
    4.27 -  let val cname_list = map const_of_split_thm splits;
    4.28 +  let val cname_list = map (fst o split_thm_info) splits;
    4.29        fun is_case (a,_) = a mem cname_list;
    4.30        fun tac (t,i) = 
    4.31  	  let val n = find_index (exists_Const is_case) 
    4.32 @@ -335,7 +334,7 @@
    4.33  
    4.34  in
    4.35  
    4.36 -val const_of_split_thm = const_of_split_thm;
    4.37 +val split_thm_info = split_thm_info;
    4.38  
    4.39  fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
    4.40