author | smolkas |
Thu, 17 Jan 2013 11:56:34 +0100 | |
changeset 50924 | beb95bf66b21 |
parent 50923 | 141d8f575f6f |
child 51128 | 0021ea861129 |
permissions | -rw-r--r-- |
50263 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
50923 | 5 |
Shrinking of reconstructed isar proofs. |
50263 | 6 |
*) |
7 |
||
50259 | 8 |
signature SLEDGEHAMMER_SHRINK = |
9 |
sig |
|
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50263
diff
changeset
|
10 |
type isar_step = Sledgehammer_Proof.isar_step |
50924 | 11 |
type preplay_time = Sledgehammer_Preplay.preplay_time |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
12 |
val shrink_proof : |
50557 | 13 |
bool -> Proof.context -> string -> string -> bool -> Time.time option |
50924 | 14 |
-> real -> isar_step list -> isar_step list * (bool * preplay_time) |
50259 | 15 |
end |
16 |
||
50269 | 17 |
structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK = |
50259 | 18 |
struct |
19 |
||
50265 | 20 |
open Sledgehammer_Util |
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50263
diff
changeset
|
21 |
open Sledgehammer_Proof |
50923 | 22 |
open Sledgehammer_Preplay |
50259 | 23 |
|
24 |
(* Parameters *) |
|
25 |
val merge_timeout_slack = 1.2 |
|
26 |
||
27 |
(* Data structures, orders *) |
|
28 |
val label_ord = prod_ord int_ord fast_string_ord o pairself swap |
|
29 |
structure Label_Table = Table( |
|
30 |
type key = label |
|
31 |
val ord = label_ord) |
|
32 |
||
33 |
(* clean vector interface *) |
|
34 |
fun get i v = Vector.sub (v, i) |
|
35 |
fun replace x i v = Vector.update (v, i, x) |
|
36 |
fun update f i v = replace (get i v |> f) i v |
|
50273 | 37 |
fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList |
50259 | 38 |
fun v_fold_index f v s = |
39 |
Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd |
|
40 |
||
41 |
(* Queue interface to table *) |
|
42 |
fun pop tab key = |
|
43 |
let val v = hd (Inttab.lookup_list tab key) in |
|
44 |
(v, Inttab.remove_list (op =) (key, v) tab) |
|
45 |
end |
|
46 |
fun pop_max tab = pop tab (the (Inttab.max_key tab)) |
|
47 |
fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab |
|
48 |
||
49 |
(* Main function for shrinking proofs *) |
|
50 |
fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout |
|
51 |
isar_shrink proof = |
|
52 |
let |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
53 |
(* 60 seconds seems like a good interpreation of "no timeout" *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
54 |
val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) |
50271
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset
|
55 |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
56 |
(* handle metis preplay fail *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
57 |
local |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
58 |
open Unsynchronized |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
59 |
val metis_fail = ref false |
50259 | 60 |
in |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
61 |
fun handle_metis_fail try_metis () = |
50901 | 62 |
try_metis () handle exn => |
63 |
(if Exn.is_interrupt exn orelse debug then reraise exn |
|
50924 | 64 |
else metis_fail := true; some_preplay_time) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
65 |
fun get_time lazy_time = |
50924 | 66 |
if !metis_fail andalso not (Lazy.is_finished lazy_time) |
67 |
then some_preplay_time |
|
68 |
else Lazy.force lazy_time |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
69 |
val metis_fail = fn () => !metis_fail |
50259 | 70 |
end |
71 |
||
50779 | 72 |
(* Shrink proof on top level - do not shrink case splits *) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
73 |
fun shrink_top_level on_top_level ctxt proof = |
50259 | 74 |
let |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
75 |
(* proof vector *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
76 |
val proof_vect = proof |> map SOME |> Vector.fromList |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
77 |
val n = Vector.length proof_vect |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
78 |
val n_metis = metis_steps_top_level proof |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
79 |
val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
80 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
81 |
(* table for mapping from (top-level-)label to proof position *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
82 |
fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
83 |
| update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
84 |
| update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
85 |
| update_table _ = I |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
86 |
val label_index_table = fold_index update_table proof Label_Table.empty |
50711 | 87 |
val lookup_indices = map_filter (Label_Table.lookup label_index_table) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
88 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
89 |
(* proof references *) |
50711 | 90 |
fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs |
91 |
| refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
92 |
| refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = |
50711 | 93 |
lookup_indices lfs @ maps (maps refs) cases |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
94 |
| refs _ = [] |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
95 |
val refed_by_vect = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
96 |
Vector.tabulate (n, (fn _ => [])) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
97 |
|> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
98 |
|> Vector.map rev (* after rev, indices are sorted in ascending order *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
99 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
100 |
(* candidates for elimination, use table as priority queue (greedy |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
101 |
algorithm) *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
102 |
fun add_if_cand proof_vect (i, [j]) = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
103 |
(case (the (get i proof_vect), the (get j proof_vect)) of |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
104 |
(Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => |
50780 | 105 |
cons (Term.size_of_term t, i) |
106 |
| (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => |
|
107 |
cons (Term.size_of_term t, i) |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
108 |
| _ => I) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
109 |
| add_if_cand _ _ = I |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
110 |
val cand_tab = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
111 |
v_fold_index (add_if_cand proof_vect) refed_by_vect [] |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
112 |
|> Inttab.make_list |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
113 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
114 |
(* cache metis preplay times in lazy time vector *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
115 |
val metis_time = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
116 |
v_map_index |
50924 | 117 |
(if not preplay then K (zero_preplay_time) #> Lazy.value |
50923 | 118 |
else |
50924 | 119 |
apsnd the (* step *) |
120 |
#> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *) |
|
50923 | 121 |
#> try_metis debug type_enc lam_trans ctxt preplay_timeout |
122 |
#> handle_metis_fail |
|
123 |
#> Lazy.lazy) |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
124 |
proof_vect |
50923 | 125 |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
126 |
fun sum_up_time lazy_time_vector = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
127 |
Vector.foldl |
50924 | 128 |
(apfst get_time #> uncurry add_preplay_time) |
129 |
zero_preplay_time lazy_time_vector |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
130 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
131 |
(* Merging *) |
50780 | 132 |
fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 = |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
133 |
let |
50780 | 134 |
val (step_constructor, lfs2, gfs2) = |
135 |
(case step2 of |
|
136 |
(Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) => |
|
137 |
(fn by => Prove (qs2, label2, t, by), lfs2, gfs2) |
|
50924 | 138 |
| (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => |
50785
34e8e0e86639
proper exception handling; reraise interrupt exceptions
smolkas
parents:
50780
diff
changeset
|
139 |
(fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) |
50924 | 140 |
| _ => error "sledgehammer_shrink: unmergeable Isar steps" ) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
141 |
val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
142 |
val gfs = union (op =) gfs1 gfs2 |
50780 | 143 |
in step_constructor (By_Metis (lfs, gfs)) end |
50924 | 144 |
| merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps" |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
145 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
146 |
fun try_merge metis_time (s1, i) (s2, j) = |
50924 | 147 |
if not preplay then (merge s1 s2 |> SOME, metis_time) |
148 |
else |
|
149 |
(case get i metis_time |> Lazy.force of |
|
150 |
(true, _) => (NONE, metis_time) |
|
151 |
| (_, t1) => |
|
152 |
(case get j metis_time |> Lazy.force of |
|
153 |
(true, _) => (NONE, metis_time) |
|
154 |
| (_, t2) => |
|
155 |
let |
|
156 |
val s12 = merge s1 s2 |
|
157 |
val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) |
|
158 |
in |
|
159 |
case try_metis_quietly debug type_enc lam_trans ctxt timeout |
|
160 |
(NONE, s12) () of |
|
161 |
(true, _) => (NONE, metis_time) |
|
162 |
| exact_time => |
|
163 |
(SOME s12, metis_time |
|
164 |
|> replace (zero_preplay_time |> Lazy.value) i |
|
165 |
|> replace (Lazy.value exact_time) j) |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
166 |
|
50924 | 167 |
end)) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
168 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
169 |
fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
170 |
if Inttab.is_empty cand_tab |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
171 |
orelse n_metis' <= target_n_metis |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
172 |
orelse (on_top_level andalso n'<3) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
173 |
then |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
174 |
(Vector.foldr |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
175 |
(fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
176 |
[] proof_vect, |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
177 |
sum_up_time metis_time) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
178 |
else |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
179 |
let |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
180 |
val (i, cand_tab) = pop_max cand_tab |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
181 |
val j = get i refed_by |> the_single |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
182 |
val s1 = get i proof_vect |> the |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
183 |
val s2 = get j proof_vect |> the |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
184 |
in |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
185 |
case try_merge metis_time (s1, i) (s2, j) of |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
186 |
(NONE, metis_time) => |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
187 |
merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
188 |
| (s, metis_time) => |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
189 |
let |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
190 |
val refs = refs s1 |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
191 |
val refed_by = refed_by |> fold |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
192 |
(update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
193 |
val new_candidates = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
194 |
fold (add_if_cand proof_vect) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
195 |
(map (fn i => (i, get i refed_by)) refs) [] |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
196 |
val cand_tab = add_list cand_tab new_candidates |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
197 |
val proof_vect = proof_vect |> replace NONE i |> replace s j |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
198 |
in |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
199 |
merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
200 |
(n_metis' - 1) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
201 |
end |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
202 |
end |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
203 |
in |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
204 |
merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis |
50259 | 205 |
end |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
206 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
207 |
fun do_proof on_top_level ctxt proof = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
208 |
let |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
209 |
(* Enrich context with top-level facts *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
210 |
val thy = Proof_Context.theory_of ctxt |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
211 |
(* TODO: add Skolem variables to context? *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
212 |
fun enrich_with_fact l t = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
213 |
Proof_Context.put_thms false |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
214 |
(string_for_label l, SOME [Skip_Proof.make_thm thy t]) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
215 |
fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
216 |
| enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
217 |
| enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
218 |
| enrich_with_step _ = I |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
219 |
val rich_ctxt = fold enrich_with_step proof ctxt |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
220 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
221 |
(* Shrink case_splits and top-levl *) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
222 |
val ((proof, top_level_time), lower_level_time) = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
223 |
proof |> do_case_splits rich_ctxt |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
224 |
|>> shrink_top_level on_top_level rich_ctxt |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
225 |
in |
50924 | 226 |
(proof, add_preplay_time lower_level_time top_level_time) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
227 |
end |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
228 |
|
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
229 |
and do_case_splits ctxt proof = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
230 |
let |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
231 |
fun shrink_each_and_collect_time shrink candidates = |
50924 | 232 |
let fun f_m cand time = shrink cand ||> add_preplay_time time |
233 |
in fold_map f_m candidates zero_preplay_time end |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
234 |
val shrink_case_split = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
235 |
shrink_each_and_collect_time (do_proof false ctxt) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
236 |
fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) = |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
237 |
let val (cases, time) = shrink_case_split cases |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
238 |
in (Prove (qs, l, t, Case_Split (cases, facts)), time) end |
50924 | 239 |
| shrink step = (step, zero_preplay_time) |
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
240 |
in |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
241 |
shrink_each_and_collect_time shrink proof |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
242 |
end |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
243 |
in |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
244 |
do_proof true ctxt proof |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
245 |
|> apsnd (pair (metis_fail ())) |
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset
|
246 |
end |
50259 | 247 |
|
248 |
end |