misc tuning and simplification;

--- a/src/Provers/splitter.ML	Tue Oct 27 16:49:57 2009 +0100
+++ b/src/Provers/splitter.ML	Tue Oct 27 17:19:31 2009 +0100
@@ -26,9 +26,10 @@
 signature SPLITTER =
 sig
   (* somewhat more internal functions *)
-  val cmap_of_split_thms : thm list -> (string * (typ * term * thm * typ * int) list) list
-  val split_posns        : (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term ->
-    (thm * (typ * typ * int list) list * int list * typ * term) list  (* first argument is a "cmap", returns a list of "split packs" *)
+  val cmap_of_split_thms: thm list -> (string * (typ * term * thm * typ * int) list) list
+  val split_posns: (string * (typ * term * thm * typ * int) list) list ->
+    theory -> typ list -> term -> (thm * (typ * typ * int list) list * int list * typ * term) list
+    (* first argument is a "cmap", returns a list of "split packs" *)
   (* the "real" interface, providing a number of tactics *)
   val split_tac       : thm list -> int -> tactic
   val split_inside_tac: thm list -> int -> tactic
@@ -57,37 +58,33 @@
 
 fun split_format_err () = error "Wrong format for split rule";
 
-(* thm -> (string * typ) * bool *)
 fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
      Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
        (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
      | _ => split_format_err ())
    | _ => split_format_err ();
 
-(* thm list -> (string * (typ * term * thm * typ * int) list) list *)
 fun cmap_of_split_thms thms =
 let
   val splits = map Data.mk_eq thms
-  fun add_thm (cmap, thm) =
-        (case concl_of thm of _$(t as _$lhs)$_ =>
-           (case strip_comb lhs of (Const(a,aT),args) =>
-              let val info = (aT,lhs,thm,fastype_of t,length args)
-              in case AList.lookup (op =) cmap a of
-                   SOME infos => AList.update (op =) (a, info::infos) cmap
-                 | NONE => (a,[info])::cmap
-              end
-            | _ => split_format_err())
-         | _ => split_format_err())
+  fun add_thm thm cmap =
+    (case concl_of thm of _ $ (t as _ $ lhs) $ _ =>
+       (case strip_comb lhs of (Const(a,aT),args) =>
+          let val info = (aT,lhs,thm,fastype_of t,length args)
+          in case AList.lookup (op =) cmap a of
+               SOME infos => AList.update (op =) (a, info::infos) cmap
+             | NONE => (a,[info])::cmap
+          end
+        | _ => split_format_err())
+     | _ => split_format_err())
 in
-  Library.foldl add_thm ([], splits)
+  fold add_thm splits []
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* mk_case_split_tac                                                         *)
 (* ------------------------------------------------------------------------- *)
 
-(* (int * int -> order) -> thm list -> int -> tactic * <split_posns> *)
-
 fun mk_case_split_tac order =
 let
 
@@ -225,13 +222,11 @@
 local
   exception MATCH
 in
-  (* Context.theory -> Type.tyenv * (Term.typ * Term.typ) -> Type.tyenv *)
   fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
                             handle Type.TYPE_MATCH => raise MATCH
-  (* Context.theory -> Term.typ list * Term.term * Term.term -> bool *)
+
   fun fomatch sg args =
     let
-      (* Type.tyenv -> Term.typ list * Term.term * Term.term -> Type.tyenv *)
       fun mtch tyinsts = fn
           (Ts, Var(_,T), t) =>
             typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
@@ -247,10 +242,8 @@
             mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
         | _ => raise MATCH
     in (mtch Vartab.empty args; true) handle MATCH => false end;
-end  (* local *)
+end;
 
-(* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term ->
-  (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *)
 fun split_posns (cmap : (string * (typ * term * thm * typ * int) list) list) sg Ts t =
   let
     val T' = fastype_of1 (Ts, t);
@@ -355,8 +348,6 @@
    i      : number of subgoal the tactic should be applied to
 *****************************************************************************)
 
-(* thm list -> int -> tactic *)
-
 fun split_tac [] i = no_tac
   | split_tac splits i =
   let val cmap = cmap_of_split_thms splits
@@ -379,9 +370,9 @@
 in (split_tac, exported_split_posns) end;  (* mk_case_split_tac *)
 
 
-val (split_tac, split_posns)        = mk_case_split_tac              int_ord;
+val (split_tac, split_posns) = mk_case_split_tac int_ord;
 
-val (split_inside_tac, _)           = mk_case_split_tac (rev_order o int_ord);
+val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord);
 
 
 (*****************************************************************************
@@ -389,7 +380,7 @@
 
    splits : list of split-theorems to be tried
 ****************************************************************************)
-fun split_asm_tac []     = K no_tac
+fun split_asm_tac [] = K no_tac
   | split_asm_tac splits =
 
   let val cname_list = map (fst o fst o split_thm_info) splits;
@@ -431,25 +422,28 @@
 
 (* addsplits / delsplits *)
 
-fun string_of_typ (Type (s, Ts)) = (if null Ts then ""
-      else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
+fun string_of_typ (Type (s, Ts)) =
+      (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
   | string_of_typ _ = "_";
 
 fun split_name (name, T) asm = "split " ^
   (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
 
 fun ss addsplits splits =
-  let fun addsplit (ss,split) =
-        let val (name,asm) = split_thm_info split
-        in Simplifier.addloop (ss, (split_name name asm,
-                       (if asm then split_asm_tac else split_tac) [split])) end
-  in Library.foldl addsplit (ss,splits) end;
+  let
+    fun addsplit split ss =
+      let
+        val (name, asm) = split_thm_info split
+        val tac = (if asm then split_asm_tac else split_tac) [split]
+      in Simplifier.addloop (ss, (split_name name asm, tac)) end
+  in fold addsplit splits ss end;
 
 fun ss delsplits splits =
-  let fun delsplit(ss,split) =
-        let val (name,asm) = split_thm_info split
-        in Simplifier.delloop (ss, split_name name asm)
-  end in Library.foldl delsplit (ss,splits) end;
+  let
+    fun delsplit split ss =
+      let val (name, asm) = split_thm_info split
+      in Simplifier.delloop (ss, split_name name asm) end
+  in fold delsplit splits ss end;
 
 
 (* attributes *)
@@ -471,7 +465,8 @@
 (* theory setup *)
 
 val setup =
-  Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
+  Attrib.setup @{binding split}
+    (Attrib.add_del split_add split_del) "declare case split rule" #>
   Method.setup @{binding split}
     (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
     "apply case split rule";