author | wenzelm |
Thu, 29 Nov 2012 17:12:51 +0100 | |
changeset 50287 | 6cb7a7b97eac |
parent 50286 | e8b29ddbb61f |
child 50578 | 9efc99c990d5 |
permissions | -rw-r--r-- |
46589 | 1 |
(* Title: HOL/Tools/Quickcheck/find_unused_assms.ML |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
3 |
||
50286 | 4 |
Finding unused assumptions in lemmas (using Quickcheck). |
46589 | 5 |
*) |
6 |
||
7 |
signature FIND_UNUSED_ASSMS = |
|
8 |
sig |
|
9 |
val find_unused_assms : Proof.context -> string -> (string * int list list option) list |
|
10 |
val print_unused_assms : Proof.context -> string option -> unit |
|
50286 | 11 |
end |
46589 | 12 |
|
13 |
structure Find_Unused_Assms : FIND_UNUSED_ASSMS = |
|
14 |
struct |
|
15 |
||
16 |
fun all_unconcealed_thms_of thy = |
|
17 |
let |
|
18 |
val facts = Global_Theory.facts_of thy |
|
19 |
in |
|
20 |
Facts.fold_static |
|
21 |
(fn (s, ths) => |
|
22 |
if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths)) |
|
23 |
facts [] |
|
50286 | 24 |
end |
46589 | 25 |
|
26 |
fun thms_of thy thy_name = all_unconcealed_thms_of thy |
|
50286 | 27 |
|> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name) |
46589 | 28 |
|
50286 | 29 |
fun do_while P f s list = |
30 |
if P s then |
|
31 |
let val s' = f s |
|
32 |
in do_while P f s' (cons s' list) end |
|
33 |
else list |
|
46589 | 34 |
|
50286 | 35 |
fun drop_indexes is xs = |
36 |
fold_index (fn (i, x) => if member (op =) is i then I else cons x) xs [] |
|
46589 | 37 |
|
38 |
fun find_max_subsets [] = [] |
|
39 |
| find_max_subsets (ss :: sss) = ss :: |
|
40 |
(find_max_subsets (map (filter_out (fn s => exists (fn s' => subset (op =) (s, s')) ss)) sss)) |
|
41 |
||
50286 | 42 |
|
46589 | 43 |
(* main functionality *) |
44 |
||
45 |
fun find_unused_assms ctxt thy_name = |
|
46 |
let |
|
47 |
val ctxt' = ctxt |
|
48 |
|> Config.put Quickcheck.abort_potential true |
|
49 |
|> Config.put Quickcheck.quiet true |
|
50287 | 50 |
val all_thms = |
51 |
filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *) |
|
52 |
(thms_of (Proof_Context.theory_of ctxt) thy_name) |
|
46589 | 53 |
fun check_single conjecture = |
50287 | 54 |
(case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of |
55 |
SOME (SOME _) => false |
|
56 |
| SOME NONE => true |
|
57 |
| NONE => false) |
|
46589 | 58 |
fun build X Ss = |
50287 | 59 |
fold |
60 |
(fn S => fold |
|
61 |
(fn x => |
|
62 |
if member (op =) S x then I |
|
63 |
else insert (eq_set (op =)) (insert (op =) x S)) X) Ss [] |
|
46589 | 64 |
fun check (s, th) = |
50286 | 65 |
(case Logic.strip_horn (prop_of (Thm.unvarify_global th)) of |
50287 | 66 |
([], _) => (s, NONE) |
46589 | 67 |
| (ts, t) => |
50287 | 68 |
let |
69 |
fun mk_conjecture is = Logic.list_implies (drop_indexes is ts, t) |
|
70 |
val singles = filter (check_single o mk_conjecture o single) (0 upto (length ts - 1)) |
|
71 |
val multiples = |
|
72 |
do_while (not o null) |
|
73 |
(fn I => filter (check_single o mk_conjecture) (build singles I)) |
|
74 |
(map single singles) [(map single singles)] |
|
75 |
val maximals = flat (find_max_subsets multiples) |
|
76 |
in |
|
77 |
(s, SOME maximals) |
|
78 |
end) |
|
46589 | 79 |
in |
50287 | 80 |
rev (map check all_thms) |
46589 | 81 |
end |
82 |
||
50286 | 83 |
|
46589 | 84 |
(* printing results *) |
85 |
||
50286 | 86 |
local |
87 |
||
46589 | 88 |
fun pretty_indexes is = |
89 |
Pretty.block (separate (Pretty.str " and ") |
|
50286 | 90 |
(map (fn i => Pretty.str (string_of_int (i + 1))) (sort int_ord is)) |
46589 | 91 |
@ [Pretty.brk 1]) |
50286 | 92 |
|
50287 | 93 |
fun pretty_thm (s, set_of_indexes) = |
46589 | 94 |
Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 :: |
95 |
Pretty.str "unnecessary assumption(s) " :: |
|
96 |
separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes)) |
|
97 |
||
50286 | 98 |
in |
99 |
||
46589 | 100 |
fun print_unused_assms ctxt opt_thy_name = |
101 |
let |
|
102 |
val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name |
|
103 |
val results = find_unused_assms ctxt thy_name |
|
104 |
val total = length results |
|
105 |
val with_assumptions = length (filter (is_some o snd) results) |
|
50286 | 106 |
val with_superfluous_assumptions = |
50287 | 107 |
map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results |
46589 | 108 |
|
109 |
val msg = "Found " ^ string_of_int (length with_superfluous_assumptions) |
|
50286 | 110 |
^ " theorem(s) with (potentially) superfluous assumptions" |
46589 | 111 |
val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions" |
112 |
^ " in the theory " ^ quote thy_name |
|
50286 | 113 |
^ " with a total of " ^ string_of_int total ^ " theorem(s)" |
46589 | 114 |
in |
50287 | 115 |
[Pretty.str (msg ^ ":"), Pretty.str ""] @ |
116 |
map pretty_thm with_superfluous_assumptions @ |
|
50286 | 117 |
[Pretty.str "", Pretty.str end_msg] |
118 |
end |> Pretty.chunks |> Pretty.writeln |
|
46589 | 119 |
|
50286 | 120 |
end |
46589 | 121 |
|
122 |
val _ = |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46716
diff
changeset
|
123 |
Outer_Syntax.improper_command @{command_spec "find_unused_assms"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46716
diff
changeset
|
124 |
"find theorems with superfluous assumptions" |
46589 | 125 |
(Scan.option Parse.name |
126 |
>> (fn opt_thy_name => |
|
127 |
Toplevel.no_timing o Toplevel.keep (fn state => |
|
50286 | 128 |
print_unused_assms (Toplevel.context_of state) opt_thy_name))) |
46589 | 129 |
|
50286 | 130 |
end |