author | blanchet |
Wed, 17 Sep 2014 08:23:53 +0200 | |
changeset 58354 | 04ac60da613e |
parent 56334 | 6b3739fee456 |
child 58893 | 9e0ecb66d6a7 |
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 |
||
56161 | 16 |
fun thms_of thy thy_name = Global_Theory.all_thms_of thy false |
50286 | 17 |
|> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name) |
46589 | 18 |
|
50286 | 19 |
fun do_while P f s list = |
20 |
if P s then |
|
21 |
let val s' = f s |
|
22 |
in do_while P f s' (cons s' list) end |
|
23 |
else list |
|
46589 | 24 |
|
50286 | 25 |
fun drop_indexes is xs = |
26 |
fold_index (fn (i, x) => if member (op =) is i then I else cons x) xs [] |
|
46589 | 27 |
|
28 |
fun find_max_subsets [] = [] |
|
29 |
| find_max_subsets (ss :: sss) = ss :: |
|
30 |
(find_max_subsets (map (filter_out (fn s => exists (fn s' => subset (op =) (s, s')) ss)) sss)) |
|
31 |
||
50286 | 32 |
|
46589 | 33 |
(* main functionality *) |
34 |
||
35 |
fun find_unused_assms ctxt thy_name = |
|
36 |
let |
|
37 |
val ctxt' = ctxt |
|
38 |
|> Config.put Quickcheck.abort_potential true |
|
39 |
|> Config.put Quickcheck.quiet true |
|
50287 | 40 |
val all_thms = |
41 |
filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *) |
|
42 |
(thms_of (Proof_Context.theory_of ctxt) thy_name) |
|
46589 | 43 |
fun check_single conjecture = |
50287 | 44 |
(case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of |
45 |
SOME (SOME _) => false |
|
46 |
| SOME NONE => true |
|
47 |
| NONE => false) |
|
46589 | 48 |
fun build X Ss = |
50287 | 49 |
fold |
50 |
(fn S => fold |
|
51 |
(fn x => |
|
52 |
if member (op =) S x then I |
|
53 |
else insert (eq_set (op =)) (insert (op =) x S)) X) Ss [] |
|
46589 | 54 |
fun check (s, th) = |
50286 | 55 |
(case Logic.strip_horn (prop_of (Thm.unvarify_global th)) of |
50287 | 56 |
([], _) => (s, NONE) |
46589 | 57 |
| (ts, t) => |
50287 | 58 |
let |
59 |
fun mk_conjecture is = Logic.list_implies (drop_indexes is ts, t) |
|
60 |
val singles = filter (check_single o mk_conjecture o single) (0 upto (length ts - 1)) |
|
61 |
val multiples = |
|
62 |
do_while (not o null) |
|
63 |
(fn I => filter (check_single o mk_conjecture) (build singles I)) |
|
64 |
(map single singles) [(map single singles)] |
|
65 |
val maximals = flat (find_max_subsets multiples) |
|
66 |
in |
|
67 |
(s, SOME maximals) |
|
68 |
end) |
|
46589 | 69 |
in |
50578 | 70 |
rev (Par_List.map check all_thms) |
46589 | 71 |
end |
72 |
||
50286 | 73 |
|
46589 | 74 |
(* printing results *) |
75 |
||
50286 | 76 |
local |
77 |
||
46589 | 78 |
fun pretty_indexes is = |
50578 | 79 |
Pretty.block |
80 |
(flat (separate [Pretty.str " and", Pretty.brk 1] |
|
81 |
(map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is)))) |
|
50286 | 82 |
|
50287 | 83 |
fun pretty_thm (s, set_of_indexes) = |
46589 | 84 |
Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 :: |
85 |
Pretty.str "unnecessary assumption(s) " :: |
|
50578 | 86 |
separate (Pretty.str " or ") (map pretty_indexes set_of_indexes)) |
46589 | 87 |
|
50286 | 88 |
in |
89 |
||
46589 | 90 |
fun print_unused_assms ctxt opt_thy_name = |
91 |
let |
|
92 |
val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name |
|
93 |
val results = find_unused_assms ctxt thy_name |
|
94 |
val total = length results |
|
95 |
val with_assumptions = length (filter (is_some o snd) results) |
|
50286 | 96 |
val with_superfluous_assumptions = |
50287 | 97 |
map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results |
46589 | 98 |
|
50578 | 99 |
val msg = |
100 |
"Found " ^ string_of_int (length with_superfluous_assumptions) ^ |
|
101 |
" theorems with (potentially) superfluous assumptions" |
|
102 |
val end_msg = |
|
103 |
"Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^ |
|
104 |
string_of_int total ^ " total) in the theory " ^ quote thy_name |
|
46589 | 105 |
in |
50287 | 106 |
[Pretty.str (msg ^ ":"), Pretty.str ""] @ |
107 |
map pretty_thm with_superfluous_assumptions @ |
|
50286 | 108 |
[Pretty.str "", Pretty.str end_msg] |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56161
diff
changeset
|
109 |
end |> Pretty.writeln_chunks |
46589 | 110 |
|
50286 | 111 |
end |
46589 | 112 |
|
113 |
val _ = |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46716
diff
changeset
|
114 |
Outer_Syntax.improper_command @{command_spec "find_unused_assms"} |
50578 | 115 |
"find theorems with (potentially) superfluous assumptions" |
51658
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
50578
diff
changeset
|
116 |
(Scan.option Parse.name >> (fn name => |
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
50578
diff
changeset
|
117 |
Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name))) |
46589 | 118 |
|
50286 | 119 |
end |