1.1 --- a/src/HOL/Tools/split_rule.ML	Sat May 27 17:41:59 2006 +0200
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Sat May 27 17:42:00 2006 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  signature SPLIT_RULE =
     1.5  sig
     1.6    include BASIC_SPLIT_RULE
     1.7 -  val split_rule_var: term * thm -> thm
     1.8 +  val split_rule_var: term -> thm -> thm
     1.9    val split_rule_goal: string list list -> thm -> thm
    1.10    val setup: theory -> theory
    1.11  end;
    1.12 @@ -23,6 +23,7 @@
    1.13  struct
    1.14  
    1.15  
    1.16 +
    1.17  (** theory context references **)
    1.18  
    1.19  val split_conv = thm "split_conv";
    1.20 @@ -55,12 +56,12 @@
    1.21    | ap_split T T3 u = u;
    1.22  
    1.23  (*Curries any Var of function type in the rule*)
    1.24 -fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
    1.25 +fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
    1.26        let val T' = HOLogic.prodT_factors T1 ---> T2;
    1.27            val newt = ap_split T1 T2 (Var (v, T'));
    1.28 -          val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
    1.29 +          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    1.30        in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    1.31 -  | split_rule_var' (t, rl) = rl;
    1.32 +  | split_rule_var' t rl = rl;
    1.33  
    1.34  
    1.35  (* complete splitting of partially splitted rules *)
    1.36 @@ -70,50 +71,56 @@
    1.37          (incr_boundvars 1 u) $ Bound 0))
    1.38    | ap_split' _ _ u = u;
    1.39  
    1.40 -fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
    1.41 +fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
    1.42        let
    1.43 -        val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl))
    1.44 +        val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    1.45          val (Us', U') = strip_type T;
    1.46          val Us = Library.take (length ts, Us');
    1.47          val U = Library.drop (length ts, Us') ---> U';
    1.48          val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
    1.49 -        fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
    1.50 +        fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    1.51                let
    1.52                  val Ts = HOLogic.prodT_factors T;
    1.53                  val ys = Term.variantlist (replicate (length Ts) a, xs);
    1.54                in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
    1.55                  (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
    1.56                end
    1.57 -          | mk_tuple (x, _) = x;
    1.58 +          | mk_tuple _ x = x;
    1.59          val newt = ap_split' Us U (Var (v, T'));
    1.60 -        val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
    1.61 -        val (vs', insts) = Library.foldl mk_tuple ((vs, []), ts);
    1.62 +        val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    1.63 +        val (vs', insts) = fold mk_tuple ts (vs, []);
    1.64        in
    1.65          (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    1.66        end
    1.67 -  | complete_split_rule_var (_, x) = x;
    1.68 +  | complete_split_rule_var _ x = x;
    1.69  
    1.70 -fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
    1.71 -  | collect_vars (vs, t) = (case strip_comb t of
    1.72 -        (v as Var _, ts) => (v, ts)::vs
    1.73 -      | (t, ts) => Library.foldl collect_vars (vs, ts));
    1.74 +fun collect_vars (Abs (_, _, t)) = collect_vars t
    1.75 +  | collect_vars t =
    1.76 +      (case strip_comb t of
    1.77 +        (v as Var _, ts) => cons (v, ts)
    1.78 +      | (t, ts) => fold collect_vars ts);
    1.79  
    1.80  
    1.81 -val split_rule_var = Drule.standard o remove_internal_split o split_rule_var';
    1.82 +val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var';
    1.83  
    1.84  (*curries ALL function variables occurring in a rule's conclusion*)
    1.85  fun split_rule rl =
    1.86 -  foldr split_rule_var' rl (Term.term_vars (concl_of rl))
    1.87 +  fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl
    1.88    |> remove_internal_split
    1.89    |> Drule.standard;
    1.90  
    1.91 +(*curries ALL function variables*)
    1.92  fun complete_split_rule rl =
    1.93 -  fst (foldr complete_split_rule_var
    1.94 -    (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))
    1.95 -    (collect_vars ([], concl_of rl)))
    1.96 -  |> remove_internal_split
    1.97 -  |> Drule.standard
    1.98 -  |> RuleCases.save rl;
    1.99 +  let
   1.100 +    val prop = Thm.prop_of rl;
   1.101 +    val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
   1.102 +    val vars = collect_vars prop [];
   1.103 +  in
   1.104 +    fst (fold_rev complete_split_rule_var vars (rl, xs))
   1.105 +    |> remove_internal_split
   1.106 +    |> Drule.standard
   1.107 +    |> RuleCases.save rl
   1.108 +  end;
   1.109  
   1.110  
   1.111  val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
   1.112 @@ -121,12 +128,12 @@
   1.113  fun split_rule_goal xss rl =
   1.114    let
   1.115      fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
   1.116 -    fun one_goal (i, xs) = fold (one_split (i+1)) xs;
   1.117 +    fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   1.118    in
   1.119      rl
   1.120 -    |> Library.fold_index one_goal xss
   1.121 +    |> fold_index one_goal xss
   1.122      |> Simplifier.full_simplify split_rule_ss
   1.123 -    |> Drule.standard 
   1.124 +    |> Drule.standard
   1.125      |> RuleCases.save rl
   1.126    end;
   1.127