# HG changeset patch
# User wenzelm
# Date 1148744520 -7200
# Node ID ff13585fbdab7eeacaadb19c6fc29c58c89fb3cc
# Parent  e9a06ce3a97aec2d30984c7043acf779478cbc96
complete_split_rule: all Vars;
tuned;

diff -r e9a06ce3a97a -r ff13585fbdab src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sat May 27 17:41:59 2006 +0200
+++ b/src/HOL/Tools/split_rule.ML	Sat May 27 17:42:00 2006 +0200
@@ -14,7 +14,7 @@
 signature SPLIT_RULE =
 sig
   include BASIC_SPLIT_RULE
-  val split_rule_var: term * thm -> thm
+  val split_rule_var: term -> thm -> thm
   val split_rule_goal: string list list -> thm -> thm
   val setup: theory -> theory
 end;
@@ -23,6 +23,7 @@
 struct
 
 
+
 (** theory context references **)
 
 val split_conv = thm "split_conv";
@@ -55,12 +56,12 @@
   | ap_split T T3 u = u;
 
 (*Curries any Var of function type in the rule*)
-fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
+fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
       let val T' = HOLogic.prodT_factors T1 ---> T2;
           val newt = ap_split T1 T2 (Var (v, T'));
-          val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
+          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
       in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
-  | split_rule_var' (t, rl) = rl;
+  | split_rule_var' t rl = rl;
 
 
 (* complete splitting of partially splitted rules *)
@@ -70,50 +71,56 @@
         (incr_boundvars 1 u) $ Bound 0))
   | ap_split' _ _ u = u;
 
-fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
+fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
       let
-        val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl))
+        val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
         val (Us', U') = strip_type T;
         val Us = Library.take (length ts, Us');
         val U = Library.drop (length ts, Us') ---> U';
         val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
-        fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
+        fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
               let
                 val Ts = HOLogic.prodT_factors T;
                 val ys = Term.variantlist (replicate (length Ts) a, xs);
               in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
               end
-          | mk_tuple (x, _) = x;
+          | mk_tuple _ x = x;
         val newt = ap_split' Us U (Var (v, T'));
-        val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
-        val (vs', insts) = Library.foldl mk_tuple ((vs, []), ts);
+        val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
+        val (vs', insts) = fold mk_tuple ts (vs, []);
       in
         (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
       end
-  | complete_split_rule_var (_, x) = x;
+  | complete_split_rule_var _ x = x;
 
-fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
-  | collect_vars (vs, t) = (case strip_comb t of
-        (v as Var _, ts) => (v, ts)::vs
-      | (t, ts) => Library.foldl collect_vars (vs, ts));
+fun collect_vars (Abs (_, _, t)) = collect_vars t
+  | collect_vars t =
+      (case strip_comb t of
+        (v as Var _, ts) => cons (v, ts)
+      | (t, ts) => fold collect_vars ts);
 
 
-val split_rule_var = Drule.standard o remove_internal_split o split_rule_var';
+val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var';
 
 (*curries ALL function variables occurring in a rule's conclusion*)
 fun split_rule rl =
-  foldr split_rule_var' rl (Term.term_vars (concl_of rl))
+  fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl
   |> remove_internal_split
   |> Drule.standard;
 
+(*curries ALL function variables*)
 fun complete_split_rule rl =
-  fst (foldr complete_split_rule_var
-    (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))
-    (collect_vars ([], concl_of rl)))
-  |> remove_internal_split
-  |> Drule.standard
-  |> RuleCases.save rl;
+  let
+    val prop = Thm.prop_of rl;
+    val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
+    val vars = collect_vars prop [];
+  in
+    fst (fold_rev complete_split_rule_var vars (rl, xs))
+    |> remove_internal_split
+    |> Drule.standard
+    |> RuleCases.save rl
+  end;
 
 
 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
@@ -121,12 +128,12 @@
 fun split_rule_goal xss rl =
   let
     fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
-    fun one_goal (i, xs) = fold (one_split (i+1)) xs;
+    fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   in
     rl
-    |> Library.fold_index one_goal xss
+    |> fold_index one_goal xss
     |> Simplifier.full_simplify split_rule_ss
-    |> Drule.standard 
+    |> Drule.standard
     |> RuleCases.save rl
   end;