author | wenzelm |
Tue, 09 Apr 2013 15:29:25 +0200 | |
changeset 51658 | 21c10672633b |
parent 50578 | 9efc99c990d5 |
child 56161 | 300f613060b0 |
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 |
50578 | 80 |
rev (Par_List.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 = |
50578 | 89 |
Pretty.block |
90 |
(flat (separate [Pretty.str " and", Pretty.brk 1] |
|
91 |
(map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is)))) |
|
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) " :: |
|
50578 | 96 |
separate (Pretty.str " or ") (map pretty_indexes set_of_indexes)) |
46589 | 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 |
|
50578 | 109 |
val msg = |
110 |
"Found " ^ string_of_int (length with_superfluous_assumptions) ^ |
|
111 |
" theorems with (potentially) superfluous assumptions" |
|
112 |
val end_msg = |
|
113 |
"Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^ |
|
114 |
string_of_int total ^ " total) in the theory " ^ quote thy_name |
|
46589 | 115 |
in |
50287 | 116 |
[Pretty.str (msg ^ ":"), Pretty.str ""] @ |
117 |
map pretty_thm with_superfluous_assumptions @ |
|
50286 | 118 |
[Pretty.str "", Pretty.str end_msg] |
119 |
end |> Pretty.chunks |> Pretty.writeln |
|
46589 | 120 |
|
50286 | 121 |
end |
46589 | 122 |
|
123 |
val _ = |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46716
diff
changeset
|
124 |
Outer_Syntax.improper_command @{command_spec "find_unused_assms"} |
50578 | 125 |
"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
|
126 |
(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
|
127 |
Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name))) |
46589 | 128 |
|
50286 | 129 |
end |