author | wenzelm |
Mon, 25 Sep 2023 18:45:41 +0200 | |
changeset 78705 | fde0b195cb7d |
parent 77893 | dfc1db3f0fcb |
child 80306 | c2537860ccf8 |
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 |
|
70117 | 9 |
val check_unused_assms: Proof.context -> string * thm -> string * int list list option |
10 |
val find_unused_assms: Proof.context -> string -> (string * int list list option) list |
|
11 |
val print_unused_assms: Proof.context -> string option -> unit |
|
50286 | 12 |
end |
46589 | 13 |
|
14 |
structure Find_Unused_Assms : FIND_UNUSED_ASSMS = |
|
15 |
struct |
|
16 |
||
60638 | 17 |
fun thms_of thy thy_name = |
18 |
Global_Theory.all_thms_of thy false |
|
77889
5db014c36f42
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
wenzelm
parents:
70117
diff
changeset
|
19 |
|> filter (fn (_, th) => Thm.theory_base_name th = thy_name) |
46589 | 20 |
|
50286 | 21 |
fun do_while P f s list = |
22 |
if P s then |
|
23 |
let val s' = f s |
|
24 |
in do_while P f s' (cons s' list) end |
|
25 |
else list |
|
46589 | 26 |
|
50286 | 27 |
fun drop_indexes is xs = |
28 |
fold_index (fn (i, x) => if member (op =) is i then I else cons x) xs [] |
|
46589 | 29 |
|
30 |
fun find_max_subsets [] = [] |
|
31 |
| find_max_subsets (ss :: sss) = ss :: |
|
32 |
(find_max_subsets (map (filter_out (fn s => exists (fn s' => subset (op =) (s, s')) ss)) sss)) |
|
33 |
||
50286 | 34 |
|
46589 | 35 |
(* main functionality *) |
36 |
||
70117 | 37 |
fun check_unused_assms ctxt = |
46589 | 38 |
let |
60825 | 39 |
val thy = Proof_Context.theory_of ctxt |
46589 | 40 |
val ctxt' = ctxt |
41 |
|> Config.put Quickcheck.abort_potential true |
|
42 |
|> Config.put Quickcheck.quiet true |
|
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 [] |
|
70117 | 54 |
fun check (name, th) = |
60825 | 55 |
(case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global thy th)) of |
70117 | 56 |
([], _) => (name, 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) |
|
70117 | 66 |
in (name, SOME maximals) end) |
67 |
in check end |
|
68 |
||
69 |
fun find_unused_assms ctxt thy_name = |
|
70 |
let |
|
71 |
val thy = Proof_Context.theory_of ctxt |
|
72 |
val all_thms = |
|
73 |
thms_of thy thy_name |
|
77893 | 74 |
|> filter (fn (name, _) => Long_Name.count name = 2) (* FIXME !? *) |
70117 | 75 |
|> sort_by #1 |
76 |
val check = check_unused_assms ctxt |
|
77 |
in rev (Par_List.map check all_thms) end |
|
46589 | 78 |
|
50286 | 79 |
|
46589 | 80 |
(* printing results *) |
81 |
||
50286 | 82 |
local |
83 |
||
46589 | 84 |
fun pretty_indexes is = |
50578 | 85 |
Pretty.block |
86 |
(flat (separate [Pretty.str " and", Pretty.brk 1] |
|
87 |
(map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is)))) |
|
50286 | 88 |
|
70117 | 89 |
fun pretty_thm (name, set_of_indexes) = |
90 |
Pretty.block (Pretty.str name :: Pretty.str ":" :: Pretty.brk 1 :: |
|
91 |
Pretty.str "unnecessary assumption " :: |
|
50578 | 92 |
separate (Pretty.str " or ") (map pretty_indexes set_of_indexes)) |
46589 | 93 |
|
50286 | 94 |
in |
95 |
||
46589 | 96 |
fun print_unused_assms ctxt opt_thy_name = |
97 |
let |
|
77889
5db014c36f42
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
wenzelm
parents:
70117
diff
changeset
|
98 |
val thy_name = |
5db014c36f42
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
wenzelm
parents:
70117
diff
changeset
|
99 |
the_default (Context.theory_base_name (Proof_Context.theory_of ctxt)) opt_thy_name |
46589 | 100 |
val results = find_unused_assms ctxt thy_name |
101 |
val total = length results |
|
102 |
val with_assumptions = length (filter (is_some o snd) results) |
|
50286 | 103 |
val with_superfluous_assumptions = |
70117 | 104 |
results |> map_filter |
105 |
(fn (_, NONE) => NONE | (_, SOME []) => NONE | (name, SOME r) => SOME (name, r)) |
|
46589 | 106 |
|
50578 | 107 |
val msg = |
108 |
"Found " ^ string_of_int (length with_superfluous_assumptions) ^ |
|
109 |
" theorems with (potentially) superfluous assumptions" |
|
110 |
val end_msg = |
|
111 |
"Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^ |
|
112 |
string_of_int total ^ " total) in the theory " ^ quote thy_name |
|
46589 | 113 |
in |
50287 | 114 |
[Pretty.str (msg ^ ":"), Pretty.str ""] @ |
115 |
map pretty_thm with_superfluous_assumptions @ |
|
50286 | 116 |
[Pretty.str "", Pretty.str end_msg] |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56161
diff
changeset
|
117 |
end |> Pretty.writeln_chunks |
46589 | 118 |
|
50286 | 119 |
end |
46589 | 120 |
|
121 |
val _ = |
|
67149 | 122 |
Outer_Syntax.command \<^command_keyword>\<open>find_unused_assms\<close> |
50578 | 123 |
"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
|
124 |
(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
|
125 |
Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name))) |
46589 | 126 |
|
50286 | 127 |
end |