author  wenzelm 
Tue, 15 Jan 2013 16:34:19 +0100  
changeset 50901  f4a6c360af35 
parent 50786  af8ecf09a58c 
child 50908  02ed5abcc0e5 
permissions  rwrr 
50263  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
Author: Steffen Juilf Smolka, TU Muenchen 

4 

50265  5 
Shrinking and preplaying 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 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

11 
val shrink_proof : 
50557  12 
bool > Proof.context > string > string > bool > Time.time option 
13 
> real > isar_step list > isar_step list * (bool * (bool * Time.time)) 

50259  14 
end 
15 

50269  16 
structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK = 
50259  17 
struct 
18 

50265  19 
open Sledgehammer_Util 
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50263
diff
changeset

20 
open Sledgehammer_Proof 
50259  21 

22 
(* Parameters *) 

23 
val merge_timeout_slack = 1.2 

24 

25 
(* Data structures, orders *) 

26 
val label_ord = prod_ord int_ord fast_string_ord o pairself swap 

27 
structure Label_Table = Table( 

28 
type key = label 

29 
val ord = label_ord) 

30 

31 
(* clean vector interface *) 

32 
fun get i v = Vector.sub (v, i) 

33 
fun replace x i v = Vector.update (v, i, x) 

34 
fun update f i v = replace (get i v > f) i v 

50273  35 
fun v_map_index f v = Vector.foldr (op::) nil v > map_index f > Vector.fromList 
50259  36 
fun v_fold_index f v s = 
37 
Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v > snd 

38 

39 
(* Queue interface to table *) 

40 
fun pop tab key = 

41 
let val v = hd (Inttab.lookup_list tab key) in 

42 
(v, Inttab.remove_list (op =) (key, v) tab) 

43 
end 

44 
fun pop_max tab = pop tab (the (Inttab.max_key tab)) 

45 
fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab 

46 

50271
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

47 
(* Timing *) 
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

48 
fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) 
50557  49 
val no_time = (false, Time.zeroTime) 
50271
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

50 
fun take_time timeout tac arg = 
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

51 
let val timing = Timing.start () in 
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

52 
(TimeLimit.timeLimit timeout tac arg; 
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

53 
Timing.result timing > #cpu > SOME) 
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

54 
handle TimeLimit.TimeOut => NONE 
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

55 
end 
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

56 

2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50270
diff
changeset

57 

50259  58 
(* Main function for shrinking proofs *) 
59 
fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout 

60 
isar_shrink proof = 

61 
let 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

62 
(* 60 seconds seems like a good interpreation of "no timeout" *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

63 
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

64 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

65 
(* handle metis preplay fail *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

66 
local 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

67 
open Unsynchronized 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

68 
val metis_fail = ref false 
50259  69 
in 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

70 
fun handle_metis_fail try_metis () = 
50901  71 
try_metis () handle exn => 
72 
(if Exn.is_interrupt exn orelse debug then reraise exn 

50785
34e8e0e86639
proper exception handling; reraise interrupt exceptions
smolkas
parents:
50780
diff
changeset

73 
else metis_fail := true; SOME Time.zeroTime) 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

74 
fun get_time lazy_time = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

75 
if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

76 
val metis_fail = fn () => !metis_fail 
50259  77 
end 
78 

50779  79 
(* 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

80 
fun shrink_top_level on_top_level ctxt proof = 
50259  81 
let 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

82 
(* proof vector *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

83 
val proof_vect = proof > map SOME > Vector.fromList 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

84 
val n = Vector.length proof_vect 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

85 
val n_metis = metis_steps_top_level proof 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

86 
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

87 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

88 
(* table for mapping from (toplevel)label to proof position *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

89 
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

90 
 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

91 
 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

92 
 update_table _ = I 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

93 
val label_index_table = fold_index update_table proof Label_Table.empty 
50711  94 
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

95 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

96 
(* proof references *) 
50711  97 
fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs 
98 
 refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

99 
 refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = 
50711  100 
lookup_indices lfs @ maps (maps refs) cases 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

101 
 refs _ = [] 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

102 
val refed_by_vect = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

103 
Vector.tabulate (n, (fn _ => [])) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

104 
> 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

105 
> 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

106 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

107 
(* candidates for elimination, use table as priority queue (greedy 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

108 
algorithm) *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

109 
fun add_if_cand proof_vect (i, [j]) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

110 
(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

111 
(Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => 
50780  112 
cons (Term.size_of_term t, i) 
113 
 (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => 

114 
cons (Term.size_of_term t, i) 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

115 
 _ => I) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

116 
 add_if_cand _ _ = I 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

117 
val cand_tab = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

118 
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

119 
> Inttab.make_list 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

120 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

121 
(* Metis Preplaying *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

122 
fun resolve_fact_names names = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

123 
names 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

124 
>> map string_for_label 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

125 
> op @ 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

126 
> maps (thms_of_name ctxt) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

127 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

128 
(* TODO: add "Obtain" case *) 
50786  129 
exception ZEROTIME 
50779  130 
fun try_metis timeout (succedent, step) = 
131 
(if not preplay then K (SOME Time.zeroTime) else 

132 
let 

133 
val (t, byline, obtain) = 

134 
(case step of 

135 
Prove (_, _, t, byline) => (t, byline, false) 

136 
 Obtain (_, xs, _, t, byline) => 

137 
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis 

138 
(see ~~/src/Pure/Isar/obtain.ML) *) 

139 
let 

140 
(*val thesis = Term.Free ("thesis", HOLogic.boolT) 

141 
> HOLogic.mk_Trueprop 

142 
val frees = map Term.Free xs 

143 

144 
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) 

145 
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis)) 

146 

147 
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) 

148 
val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis))*) 

149 

150 
val thesis = Term.Free ("thesis", HOLogic.boolT) 

151 
val prop = 

50780  152 
HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis) 
50779  153 
> fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) xs 
154 
> rpair thesis 

155 
> HOLogic.mk_imp 

156 
> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t)) 

157 
> HOLogic.mk_Trueprop 

158 
in 

159 
(prop, byline, true) 

160 
end 

50786  161 
 _ => raise ZEROTIME) 
50779  162 
val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) 
163 
val facts = 

164 
(case byline of 

165 
By_Metis fact_names => resolve_fact_names fact_names 

166 
 Case_Split (cases, fact_names) => 

167 
resolve_fact_names fact_names 

168 
@ (case the succedent of 

169 
Assume (_, t) => make_thm t 

170 
 Obtain (_, _, _, t, _) => make_thm t 

171 
 Prove (_, _, t, _) => make_thm t 

172 
 _ => error "Internal error: unexpected succedent of case split") 

173 
:: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) 

174 
 _ => error "Internal error: malformed case split") 

175 
#> make_thm) 

176 
cases) 

177 
val ctxt = ctxt > Config.put Metis_Tactic.verbose debug 

178 
> obtain ? Config.put Metis_Tactic.new_skolem true 

179 
val goal = 

180 
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t 

181 
fun tac {context = ctxt, prems = _} = 

182 
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 

183 
in 

184 
take_time timeout (fn () => goal tac) 

185 
end) 

50786  186 
handle ZEROTIME => K (SOME Time.zeroTime) 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

187 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

188 
val try_metis_quietly = the_default NONE oo try oo try_metis 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

189 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

190 
(* cache metis preplay times in lazy time vector *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

191 
val metis_time = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

192 
v_map_index 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

193 
(Lazy.lazy o handle_metis_fail o try_metis preplay_timeout 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

194 
o apfst (fn i => try (the o get (i1)) proof_vect) o apsnd the) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

195 
proof_vect 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

196 
fun sum_up_time lazy_time_vector = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

197 
Vector.foldl 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

198 
((fn (SOME t, (b, ts)) => (b, Time.+(t, ts)) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

199 
 (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout))) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

200 
o apfst get_time) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

201 
no_time lazy_time_vector 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

202 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

203 
(* Merging *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

204 
(* TODO: consider adding "Obtain" cases *) 
50780  205 
fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 = 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

206 
let 
50780  207 
val (step_constructor, lfs2, gfs2) = 
208 
(case step2 of 

209 
(Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) => 

210 
(fn by => Prove (qs2, label2, t, by), lfs2, gfs2) 

211 
 (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => 

50785
34e8e0e86639
proper exception handling; reraise interrupt exceptions
smolkas
parents:
50780
diff
changeset

212 
(fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) 
34e8e0e86639
proper exception handling; reraise interrupt exceptions
smolkas
parents:
50780
diff
changeset

213 
 _ => error "Internal error: unmergeable Isar steps" ) 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

214 
val lfs = remove (op =) label1 lfs2 > union (op =) lfs1 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

215 
val gfs = union (op =) gfs1 gfs2 
50780  216 
in step_constructor (By_Metis (lfs, gfs)) end 
50785
34e8e0e86639
proper exception handling; reraise interrupt exceptions
smolkas
parents:
50780
diff
changeset

217 
 merge _ _ = error "Internal error: unmergeable Isar steps" 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

218 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

219 
fun try_merge metis_time (s1, i) (s2, j) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

220 
(case get i metis_time > Lazy.force of 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

221 
NONE => (NONE, metis_time) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

222 
 SOME t1 => 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

223 
(case get j metis_time > Lazy.force of 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

224 
NONE => (NONE, metis_time) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

225 
 SOME t2 => 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

226 
let 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

227 
val s12 = merge s1 s2 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

228 
val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

229 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

230 
case try_metis_quietly timeout (NONE, s12) () of 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

231 
NONE => (NONE, metis_time) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

232 
 some_t12 => 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

233 
(SOME s12, metis_time 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

234 
> replace (Time.zeroTime > SOME > Lazy.value) i 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

235 
> replace (Lazy.value some_t12) j) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

236 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

237 
end)) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

238 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

239 
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

240 
if Inttab.is_empty cand_tab 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

241 
orelse n_metis' <= target_n_metis 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

242 
orelse (on_top_level andalso n'<3) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

243 
then 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

244 
(Vector.foldr 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

245 
(fn (NONE, proof) => proof  (SOME s, proof) => s :: proof) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

246 
[] proof_vect, 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

247 
sum_up_time metis_time) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

248 
else 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

249 
let 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

250 
val (i, cand_tab) = pop_max cand_tab 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

251 
val j = get i refed_by > the_single 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

252 
val s1 = get i proof_vect > the 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

253 
val s2 = get j proof_vect > the 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

254 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

255 
case try_merge metis_time (s1, i) (s2, j) of 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

256 
(NONE, metis_time) => 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

257 
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

258 
 (s, metis_time) => 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

259 
let 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

260 
val refs = refs s1 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

261 
val refed_by = refed_by > fold 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

262 
(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

263 
val new_candidates = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

264 
fold (add_if_cand proof_vect) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

265 
(map (fn i => (i, get i refed_by)) refs) [] 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

266 
val cand_tab = add_list cand_tab new_candidates 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

267 
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

268 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

269 
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

270 
(n_metis'  1) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

271 
end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

272 
end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

273 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

274 
merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis 
50259  275 
end 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

276 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

277 
fun do_proof on_top_level ctxt proof = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

278 
let 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

279 
(* Enrich context with toplevel facts *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

280 
val thy = Proof_Context.theory_of ctxt 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

281 
(* TODO: add Skolem variables to context? *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

282 
fun enrich_with_fact l t = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

283 
Proof_Context.put_thms false 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

284 
(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

285 
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

286 
 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

287 
 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

288 
 enrich_with_step _ = I 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

289 
val rich_ctxt = fold enrich_with_step proof ctxt 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

290 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

291 
(* Shrink case_splits and toplevl *) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

292 
val ((proof, top_level_time), lower_level_time) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

293 
proof > do_case_splits rich_ctxt 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

294 
>> shrink_top_level on_top_level rich_ctxt 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

295 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

296 
(proof, ext_time_add lower_level_time top_level_time) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

297 
end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

298 

ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

299 
and do_case_splits ctxt proof = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

300 
let 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

301 
fun shrink_each_and_collect_time shrink candidates = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

302 
let fun f_m cand time = shrink cand > ext_time_add time 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

303 
in fold_map f_m candidates no_time end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

304 
val shrink_case_split = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

305 
shrink_each_and_collect_time (do_proof false ctxt) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

306 
fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

307 
let val (cases, time) = shrink_case_split cases 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

308 
in (Prove (qs, l, t, Case_Split (cases, facts)), time) end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

309 
 shrink step = (step, no_time) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

310 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

311 
shrink_each_and_collect_time shrink proof 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

312 
end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

313 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

314 
do_proof true ctxt proof 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

315 
> apsnd (pair (metis_fail ())) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50557
diff
changeset

316 
end 
50259  317 

318 
end 