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