# HG changeset patch
# User wenzelm
# Date 1354208741 -3600
# Node ID 5a1194acbecdfc1ca00e2ed82dca8348f1f4df4d
# Parent  986598b0efd11392c8d71e88d03fb91d1d59edcb# Parent  6cb7a7b97eac9d7877aeea84f2403b6ca8f0e3a2
merged

diff -r 986598b0efd1 -r 5a1194acbecd Admin/isatest/settings/mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M4	Thu Nov 29 17:54:20 2012 +0100
+++ b/Admin/isatest/settings/mac-poly-M4	Thu Nov 29 18:05:41 2012 +0100
@@ -27,3 +27,5 @@
 
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
 
+ISABELLE_FULL_TEST=true
+
diff -r 986598b0efd1 -r 5a1194acbecd Admin/isatest/settings/mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8	Thu Nov 29 17:54:20 2012 +0100
+++ b/Admin/isatest/settings/mac-poly-M8	Thu Nov 29 18:05:41 2012 +0100
@@ -27,3 +27,5 @@
 
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
 
+ISABELLE_FULL_TEST=true
+
diff -r 986598b0efd1 -r 5a1194acbecd Admin/isatest/settings/mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M4	Thu Nov 29 17:54:20 2012 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4	Thu Nov 29 18:05:41 2012 +0100
@@ -27,5 +27,3 @@
 
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
 
-ISABELLE_FULL_TEST=true
-
diff -r 986598b0efd1 -r 5a1194acbecd Admin/isatest/settings/mac-poly64-M8
--- a/Admin/isatest/settings/mac-poly64-M8	Thu Nov 29 17:54:20 2012 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8	Thu Nov 29 18:05:41 2012 +0100
@@ -27,5 +27,3 @@
 
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
 
-ISABELLE_FULL_TEST=true
-
diff -r 986598b0efd1 -r 5a1194acbecd src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Nov 29 17:54:20 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Nov 29 18:05:41 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 =
@@ -41,67 +47,77 @@
     val ctxt' = ctxt
        |> Config.put Quickcheck.abort_potential true
        |> Config.put Quickcheck.quiet true
-    val all_thms = filter (fn (s, _) => length (Long_Name.explode s) = 2)  (* FIXME !? *)
-      (thms_of (Proof_Context.theory_of ctxt) thy_name)
+    val all_thms =
+      filter (fn (s, _) => length (Long_Name.explode s) = 2)  (* FIXME !? *)
+        (thms_of (Proof_Context.theory_of ctxt) thy_name)
     fun check_single conjecture =
-      case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
-         SOME (SOME _) => false
-       | SOME NONE => true
-       | NONE => false
+      (case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
+        SOME (SOME _) => false
+      | SOME NONE => true
+      | NONE => false)
     fun build X Ss =
-      fold (fn S => fold
-        (fn x => if member (op =) S x then I
-          else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
+      fold
+        (fn S => fold
+          (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
-        ([], _) => cons (s, NONE)
+      (case Logic.strip_horn (prop_of (Thm.unvarify_global th)) of
+        ([], _) => (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 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
+          let
+            fun mk_conjecture is = Logic.list_implies (drop_indexes is ts, t)
+            val singles = filter (check_single o mk_conjecture o single) (0 upto (length ts - 1))
+            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
+            (s, SOME maximals)
+          end)
   in
-    fold check all_thms []
+    rev (map 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) =
+
+fun pretty_thm (s, 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 =
+      map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) 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 +125,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