# HG changeset patch # User bulwahn # Date 1329927773 -3600 # Node ID 6893119867781d5550a25b33f6fa7ae91b89a417 # Parent 4895d7f1be4297393389c94dfa61cc6887b7f022 adding new command "find_unused_assms" diff -r 4895d7f1be42 -r 689311986778 etc/isar-keywords.el --- a/etc/isar-keywords.el Wed Feb 22 12:30:01 2012 +0100 +++ b/etc/isar-keywords.el Wed Feb 22 17:22:53 2012 +0100 @@ -92,6 +92,7 @@ "finally" "find_consts" "find_theorems" + "find_unused_assms" "fix" "fixrec" "from" @@ -358,6 +359,7 @@ "export_code" "find_consts" "find_theorems" + "find_unused_assms" "full_prf" "header" "help" diff -r 4895d7f1be42 -r 689311986778 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Wed Feb 22 12:30:01 2012 +0100 +++ b/src/HOL/Quickcheck_Narrowing.thy Wed Feb 22 17:22:53 2012 +0100 @@ -8,6 +8,7 @@ ("Tools/Quickcheck/PNF_Narrowing_Engine.hs") ("Tools/Quickcheck/Narrowing_Engine.hs") ("Tools/Quickcheck/narrowing_generators.ML") + ("Tools/Quickcheck/find_unused_assms.ML") begin subsection {* Counterexample generator *} @@ -452,10 +453,15 @@ *) +subsection {* The @{text find_unused_assms} command *} + +use "Tools/Quickcheck/find_unused_assms.ML" + +subsection {* Closing up *} + hide_type code_int narrowing_type narrowing_term cons property hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero hide_const (open) Var Ctr "apply" sum cons hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def - end diff -r 4895d7f1be42 -r 689311986778 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Wed Feb 22 17:22:53 2012 +0100 @@ -0,0 +1,116 @@ +(* Title: HOL/Tools/Quickcheck/find_unused_assms.ML + Author: Lukas Bulwahn, TU Muenchen + +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; + +structure Find_Unused_Assms : FIND_UNUSED_ASSMS = +struct + +fun all_unconcealed_thms_of thy = + let + val facts = Global_Theory.facts_of thy + in + Facts.fold_static + (fn (s, ths) => + if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths)) + facts [] + end; + +fun thms_of thy thy_name = all_unconcealed_thms_of thy + |> 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 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 = + let + val ctxt' = ctxt + |> Config.put Quickcheck.abort_potential true + |> Config.put Quickcheck.quiet true + val all_thms = filter (fn (s, _) => length (space_explode "." s) = 2) + (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 + 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 [] + fun check (s, th) = + 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 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 + in + fold check all_thms [] + end + +(* printing results *) + +fun pretty_indexes is = + Pretty.block (separate (Pretty.str " and ") + (map (fn x => Pretty.str (string_of_int (x + 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)) + +fun print_unused_assms ctxt opt_thy_name = + let + val start = Timing.start () + 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 msg = "Found " ^ string_of_int (length with_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)" + ^ " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs"; + in + ([Pretty.str (msg ^ ":"), Pretty.str ""] @ + map pretty_thm with_superfluous_assumptions + @ [Pretty.str "", Pretty.str end_msg]) + end |> Pretty.chunks |> Pretty.writeln; + + +val _ = + Outer_Syntax.improper_command "find_unused_assms" "find theorems with superfluous assumptions" + Keyword.diag + (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))); + +end;