66 local |
66 local |
67 open Unsynchronized |
67 open Unsynchronized |
68 val metis_fail = ref false |
68 val metis_fail = ref false |
69 in |
69 in |
70 fun handle_metis_fail try_metis () = |
70 fun handle_metis_fail try_metis () = |
71 try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime) |
71 try_metis () handle exp => |
|
72 (if debug then raise exp else metis_fail := true; SOME Time.zeroTime) |
72 fun get_time lazy_time = |
73 fun get_time lazy_time = |
73 if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time |
74 if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time |
74 val metis_fail = fn () => !metis_fail |
75 val metis_fail = fn () => !metis_fail |
75 end |
76 end |
76 |
77 |
77 (* Shrink top level proof - do not shrink case splits *) |
78 (* Shrink proof on top level - do not shrink case splits *) |
78 fun shrink_top_level on_top_level ctxt proof = |
79 fun shrink_top_level on_top_level ctxt proof = |
79 let |
80 let |
80 (* proof vector *) |
81 (* proof vector *) |
81 val proof_vect = proof |> map SOME |> Vector.fromList |
82 val proof_vect = proof |> map SOME |> Vector.fromList |
82 val n = Vector.length proof_vect |
83 val n = Vector.length proof_vect |
121 |>> map string_for_label |
122 |>> map string_for_label |
122 |> op @ |
123 |> op @ |
123 |> maps (thms_of_name ctxt) |
124 |> maps (thms_of_name ctxt) |
124 |
125 |
125 (* TODO: add "Obtain" case *) |
126 (* TODO: add "Obtain" case *) |
126 fun try_metis timeout (succedent, Prove (_, _, t, byline)) = |
127 exception ZeroTime |
127 if not preplay then K (SOME Time.zeroTime) else |
128 fun try_metis timeout (succedent, step) = |
128 let |
129 (if not preplay then K (SOME Time.zeroTime) else |
129 val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
130 let |
130 val facts = |
131 val (t, byline, obtain) = |
131 (case byline of |
132 (case step of |
132 By_Metis fact_names => resolve_fact_names fact_names |
133 Prove (_, _, t, byline) => (t, byline, false) |
133 | Case_Split (cases, fact_names) => |
134 | Obtain (_, xs, _, t, byline) => |
134 resolve_fact_names fact_names |
135 (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
135 @ (case the succedent of |
136 (see ~~/src/Pure/Isar/obtain.ML) *) |
136 Assume (_, t) => make_thm t |
137 let |
137 | Obtain (_, _, _, t, _) => make_thm t |
138 (*val thesis = Term.Free ("thesis", HOLogic.boolT) |
138 | Prove (_, _, t, _) => make_thm t |
139 |> HOLogic.mk_Trueprop |
139 | _ => error "Internal error: unexpected succedent of case split") |
140 val frees = map Term.Free xs |
140 :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) |
141 |
141 | _ => error "Internal error: malformed case split") |
142 (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
142 #> make_thm) |
143 val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis)) |
143 cases) |
144 |
144 val goal = |
145 (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
145 Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t |
146 val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis))*) |
146 fun tac {context = ctxt, prems = _} = |
147 |
147 Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
148 val thesis = Term.Free ("thesis", HOLogic.boolT) |
148 in |
149 val prop = |
149 take_time timeout (fn () => goal tac) |
150 HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis) |
150 end |
151 |> fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) xs |
151 | try_metis _ _ = K (SOME Time.zeroTime) |
152 |> rpair thesis |
|
153 |> HOLogic.mk_imp |
|
154 |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t)) |
|
155 |> HOLogic.mk_Trueprop |
|
156 in |
|
157 (prop, byline, true) |
|
158 end |
|
159 | _ => raise ZeroTime) |
|
160 val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
|
161 val facts = |
|
162 (case byline of |
|
163 By_Metis fact_names => resolve_fact_names fact_names |
|
164 | Case_Split (cases, fact_names) => |
|
165 resolve_fact_names fact_names |
|
166 @ (case the succedent of |
|
167 Assume (_, t) => make_thm t |
|
168 | Obtain (_, _, _, t, _) => make_thm t |
|
169 | Prove (_, _, t, _) => make_thm t |
|
170 | _ => error "Internal error: unexpected succedent of case split") |
|
171 :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) |
|
172 | _ => error "Internal error: malformed case split") |
|
173 #> make_thm) |
|
174 cases) |
|
175 val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
|
176 |> obtain ? Config.put Metis_Tactic.new_skolem true |
|
177 val goal = |
|
178 Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t |
|
179 fun tac {context = ctxt, prems = _} = |
|
180 Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
|
181 in |
|
182 take_time timeout (fn () => goal tac) |
|
183 end) |
|
184 handle ZeroTime => K (SOME Time.zeroTime) |
152 |
185 |
153 val try_metis_quietly = the_default NONE oo try oo try_metis |
186 val try_metis_quietly = the_default NONE oo try oo try_metis |
154 |
187 |
155 (* cache metis preplay times in lazy time vector *) |
188 (* cache metis preplay times in lazy time vector *) |
156 val metis_time = |
189 val metis_time = |