# HG changeset patch
# User wenzelm
# Date 1354204793 -3600
# Node ID e8b29ddbb61f0305903268a78777c63175b518e4
# Parent  f25bcb8a4591d5006dd13a0f28c847e32f46c7b5
tuned;

diff -r f25bcb8a4591 -r e8b29ddbb61f src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Nov 29 16:52:13 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Nov 29 16:59:53 2012 +0100
@@ -1,14 +1,14 @@
 (*  Title:      HOL/Tools/Quickcheck/find_unused_assms.ML
     Author:     Lukas Bulwahn, TU Muenchen
 
-Finding unused assumptions in lemmas (using Quickcheck)
+Finding unused assumptions in lemmas (using Quickcheck).
 *)
 
 signature FIND_UNUSED_ASSMS =
 sig
   val find_unused_assms : Proof.context -> string -> (string * int list list option) list
   val print_unused_assms : Proof.context -> string option -> unit
-end;
+end
 
 structure Find_Unused_Assms : FIND_UNUSED_ASSMS =
 struct
@@ -21,19 +21,25 @@
       (fn (s, ths) =>
         if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
       facts []
-  end;
+  end
 
 fun thms_of thy thy_name = all_unconcealed_thms_of thy
-  |> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name);
+  |> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name)
 
-fun do_while P f s = if P s then (let val s' = f s in (do_while P f s') o (cons s') end) else I
+fun do_while P f s list =
+  if P s then
+    let val s' = f s
+    in do_while P f s' (cons s' list) end
+  else list
 
-fun drop_indexes is xs = fold_index (fn (i, x) => if member (op =) is i then I else cons x) xs []
+fun drop_indexes is xs =
+  fold_index (fn (i, x) => if member (op =) is i then I else cons x) xs []
 
 fun find_max_subsets [] = []
   | find_max_subsets (ss :: sss) = ss ::
       (find_max_subsets (map (filter_out (fn s => exists (fn s' => subset (op =) (s, s')) ss)) sss))
 
+
 (* main functionality *)
 
 fun find_unused_assms ctxt thy_name =
@@ -53,55 +59,60 @@
         (fn x => if member (op =) S x then I
           else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
     fun check (s, th) =
-      case Logic.strip_horn (prop_of (Thm.unvarify_global th)) of
+      (case Logic.strip_horn (prop_of (Thm.unvarify_global th)) of
         ([], _) => cons (s, NONE)
       | (ts, t) =>
         let
           fun mk_conjecture is = (Logic.list_implies (drop_indexes is ts, t))
-          val singles = filter (check_single o mk_conjecture o single) (map_index fst ts) 
+          val singles = filter (check_single o mk_conjecture o single) (map_index fst ts)
           val multiples = do_while (not o null)
             (fn I => filter (check_single o mk_conjecture) (build singles I))
             (map single singles) [(map single singles)]
           val maximals = flat (find_max_subsets multiples)
         in
           cons (s, SOME maximals)
-        end
+        end)
   in
     fold check all_thms []
   end
 
+
 (* printing results *)
 
+local
+
 fun pretty_indexes is =
   Pretty.block (separate (Pretty.str " and ")
-      (map (fn x => Pretty.str (string_of_int (x + 1))) (sort int_ord is))
+      (map (fn i => Pretty.str (string_of_int (i + 1))) (sort int_ord is))
      @ [Pretty.brk 1])
-  
+
 fun pretty_thm (s, SOME set_of_indexes) =
   Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 ::
     Pretty.str "unnecessary assumption(s) " ::
     separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes))
 
+in
+
 fun print_unused_assms ctxt opt_thy_name =
   let
     val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
     val results = find_unused_assms ctxt thy_name
     val total = length results
     val with_assumptions = length (filter (is_some o snd) results)
-    val with_superfluous_assumptions = filter_out (fn (_, r) => r = SOME [])
-      (filter (is_some o snd) results)
+    val with_superfluous_assumptions =
+      filter_out (fn (_, r) => r = SOME []) (filter (is_some o snd) results)
 
     val msg = "Found " ^ string_of_int (length with_superfluous_assumptions)
-      ^ " theorem(s) with (potentially) superfluous assumptions"      
+      ^ " theorem(s) with (potentially) superfluous assumptions"
     val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
       ^ " in the theory " ^ quote thy_name
-      ^ " with a total of " ^ string_of_int total ^ " theorem(s)"  
+      ^ " with a total of " ^ string_of_int total ^ " theorem(s)"
   in
-    ([Pretty.str (msg ^ ":"), Pretty.str ""] @
-        map pretty_thm with_superfluous_assumptions
-    @ [Pretty.str "", Pretty.str end_msg])
-  end |> Pretty.chunks |> Pretty.writeln;
+    [Pretty.str (msg ^ ":"), Pretty.str ""] @ map pretty_thm with_superfluous_assumptions @
+    [Pretty.str "", Pretty.str end_msg]
+  end |> Pretty.chunks |> Pretty.writeln
 
+end
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
@@ -109,6 +120,6 @@
     (Scan.option Parse.name
       >> (fn opt_thy_name =>
         Toplevel.no_timing o Toplevel.keep (fn state =>
-          print_unused_assms (Toplevel.context_of state) opt_thy_name)));
+          print_unused_assms (Toplevel.context_of state) opt_thy_name)))
 
-end;
+end