--- 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
+
--- 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
+
--- 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
-
--- 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
-
--- 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