99 |> maps (thms_of_name ctxt)) |
99 |> maps (thms_of_name ctxt)) |
100 handle ERROR msg => error ("preplay error: " ^ msg) |
100 handle ERROR msg => error ("preplay error: " ^ msg) |
101 |
101 |
102 (* turn terms/proofs into theorems *) |
102 (* turn terms/proofs into theorems *) |
103 fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
103 fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
104 fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) = |
104 |
105 let |
105 fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = |
106 val concl = (case try List.last steps of |
106 let |
107 SOME (Prove (_, Fix [], _, t, _, _)) => t |
107 val concl = |
108 | _ => raise Fail "preplay error: malformed subproof") |
108 (case try List.last steps of |
|
109 SOME (Prove (_, [], _, t, _, _)) => t |
|
110 | _ => raise Fail "preplay error: malformed subproof") |
109 val var_idx = maxidx_of_term concl + 1 |
111 val var_idx = maxidx_of_term concl + 1 |
110 fun var_of_free (x, T) = Var((x, var_idx), T) |
112 fun var_of_free (x, T) = Var((x, var_idx), T) |
111 val substitutions = |
113 val substitutions = |
112 map (`var_of_free #> swap #> apfst Free) fixed_frees |
114 map (`var_of_free #> swap #> apfst Free) fixed_frees |
113 in |
115 in |
133 |
135 |
134 |
136 |
135 (* main function for preplaying isar_steps; may throw exceptions *) |
137 (* main function for preplaying isar_steps; may throw exceptions *) |
136 fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time |
138 fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time |
137 | preplay_raw debug type_enc lam_trans ctxt timeout |
139 | preplay_raw debug type_enc lam_trans ctxt timeout |
138 (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) = |
140 (Prove (_, xs, _, t, subproofs, (fact_names, proof_method))) = |
139 let |
141 let |
140 val (prop, obtain) = |
142 val (prop, obtain) = |
141 (case xs of |
143 (case xs of |
142 [] => (t, false) |
144 [] => (t, false) |
143 | _ => |
145 | _ => |
199 Proof_Context.put_thms false |
201 Proof_Context.put_thms false |
200 (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
202 (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
201 |
203 |
202 val enrich_with_assms = fold (uncurry enrich_with_fact) |
204 val enrich_with_assms = fold (uncurry enrich_with_fact) |
203 |
205 |
204 fun enrich_with_proof (Proof (_, Assume assms, isar_steps)) = |
206 fun enrich_with_proof (Proof (_, assms, isar_steps)) = |
205 enrich_with_assms assms #> fold enrich_with_step isar_steps |
207 enrich_with_assms assms #> fold enrich_with_step isar_steps |
206 |
208 |
207 and enrich_with_step (Let _) = I |
209 and enrich_with_step (Let _) = I |
208 | enrich_with_step (Prove (_, _, l, t, subproofs, _)) = |
210 | enrich_with_step (Prove (_, _, l, t, subproofs, _)) = |
209 enrich_with_fact l t #> fold enrich_with_proof subproofs |
211 enrich_with_fact l t #> fold enrich_with_proof subproofs |