HACKED declaration of addsplits
authorpaulson
Thu Jul 02 17:56:06 1998 +0200 (1998-07-02 ago)
changeset 5115caf39b7b7a12
parent 5114 c729d4c299c1
child 5116 8eb343ab5748
HACKED declaration of addsplits
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu Jul 02 17:48:11 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Jul 02 17:56:06 1998 +0200
     1.3 @@ -264,20 +264,36 @@
     1.4  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
     1.5  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
     1.6  
     1.7 +(** FIXME: this is a PATCH until similar code in Provers/splitter is
     1.8 +    generalized **)
     1.9 +
    1.10 +fun split_format_err() = error("Wrong format for split rule");
    1.11 +
    1.12 +fun split_thm_info thm =
    1.13 +  (case concl_of thm of
    1.14 +     Const("Trueprop",_) $ (Const("op <->", _)$(Var _$t)$c) =>
    1.15 +        (case strip_comb t of
    1.16 +           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
    1.17 +         | _              => split_format_err())
    1.18 +   | _ => split_format_err());
    1.19 +
    1.20  infix 4 addsplits delsplits;
    1.21  fun ss addsplits splits =
    1.22    let fun addsplit (ss,split) =
    1.23          let val (name,asm) = split_thm_info split 
    1.24 -        in ss addloop (name ^ (if asm then " asm" else ""),
    1.25 +        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
    1.26  		       (if asm then split_asm_tac else split_tac) [split]) end
    1.27    in foldl addsplit (ss,splits) end;
    1.28  
    1.29  fun ss delsplits splits =
    1.30    let fun delsplit(ss,split) =
    1.31          let val (name,asm) = split_thm_info split 
    1.32 -        in ss delloop (name ^ (if asm then " asm" else "")) end
    1.33 +        in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
    1.34    in foldl delsplit (ss,splits) end;
    1.35  
    1.36 +fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
    1.37 +fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
    1.38 +
    1.39  val IFOL_simps =
    1.40     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.41      imp_simps @ iff_simps @ quant_simps;