src/Provers/splitter.ML
changeset 4668 131989b78417
parent 4519 055f2067d373
child 4930 89271bc4e7ed
     1.1 --- a/src/Provers/splitter.ML	Sat Feb 28 15:40:03 1998 +0100
     1.2 +++ b/src/Provers/splitter.ML	Sat Feb 28 15:40:50 1998 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun split_format_err() = error("Wrong format for split rule");
     1.8 +
     1.9  fun mk_case_split_tac_2 iffD order =
    1.10  let
    1.11  
    1.12 @@ -242,7 +244,6 @@
    1.13      term_lift_inst_rule (state, i, ixnTs, [((P2, T), abss (cntxt, Ts))], thm)
    1.14    end;
    1.15  
    1.16 -
    1.17  (*****************************************************************************
    1.18     The split-tactic
    1.19     
    1.20 @@ -256,8 +257,8 @@
    1.21              (case concl_of thm of _$(t as _$lhs)$_ =>
    1.22                 (case strip_comb lhs of (Const(a,_),args) =>
    1.23                    (a,(thm,fastype_of t,length args))
    1.24 -                | _ => error("Wrong format for split rule"))
    1.25 -             | _ => error("Wrong format for split rule"))
    1.26 +                | _ => split_format_err())
    1.27 +             | _ => split_format_err())
    1.28        val cmap = map const splits;
    1.29        fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
    1.30        fun lift_split_tac st = st |>
    1.31 @@ -278,6 +279,16 @@
    1.32  
    1.33  in split_tac end;
    1.34  
    1.35 +(* FIXME: this junk is only HOL specific and should therefore not go here! *)
    1.36 +(* const_of_split_thm is used in HOL/simpdata.ML *)
    1.37 +
    1.38 +fun const_of_split_thm thm =
    1.39 +  (case concl_of thm of
    1.40 +     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$_) =>
    1.41 +        (case strip_comb t of
    1.42 +           (Const(a,_),_) => a
    1.43 +         | _              => split_format_err())
    1.44 +   | _ => split_format_err());
    1.45  
    1.46  fun mk_case_split_asm_tac split_tac 
    1.47  			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
    1.48 @@ -292,13 +303,7 @@
    1.49  
    1.50  fun split_asm_tac []     = K no_tac
    1.51    | split_asm_tac splits = 
    1.52 -  let fun const thm =
    1.53 -            (case concl_of thm of Const ("Trueprop",_)$
    1.54 -				 (Const ("op =", _)$(Var _$t)$_) =>
    1.55 -               (case strip_comb t of (Const(a,_),_) => a
    1.56 -                | _ => error("Wrong format for split rule"))
    1.57 -             | _ =>    error("Wrong format for split rule"))
    1.58 -      val cname_list = map const splits;
    1.59 +  let val cname_list = map const_of_split_thm splits;
    1.60        fun is_case (a,_) = a mem cname_list;
    1.61        fun tac (t,i) = 
    1.62  	  let val n = find_index (exists_Const is_case) 
    1.63 @@ -330,6 +335,8 @@
    1.64  
    1.65  in
    1.66  
    1.67 +val const_of_split_thm = const_of_split_thm;
    1.68 +
    1.69  fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
    1.70  
    1.71  fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);