75 fun enrich_with_fact l t = |
75 fun enrich_with_fact l t = |
76 Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
76 Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) |
77 |
77 |
78 val enrich_with_assms = fold (uncurry enrich_with_fact) |
78 val enrich_with_assms = fold (uncurry enrich_with_fact) |
79 |
79 |
80 fun enrich_with_proof (Proof (_, assms, isar_steps)) = |
80 fun enrich_with_proof (Proof {assumptions, steps = isar_steps, ...}) = |
81 enrich_with_assms assms #> fold enrich_with_step isar_steps |
81 enrich_with_assms assumptions #> fold enrich_with_step isar_steps |
82 and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) = |
82 and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) = |
83 enrich_with_fact l t #> fold enrich_with_proof subproofs |
83 enrich_with_fact l t #> fold enrich_with_proof subproofs |
84 | enrich_with_step _ = I |
84 | enrich_with_step _ = I |
85 in |
85 in |
86 enrich_with_proof proof ctxt |
86 enrich_with_proof proof ctxt |
107 (names |
107 (names |
108 |>> map string_of_label |
108 |>> map string_of_label |
109 |> apply2 (maps (thms_of_name ctxt))) |
109 |> apply2 (maps (thms_of_name ctxt))) |
110 handle ERROR msg => error ("preplay error: " ^ msg) |
110 handle ERROR msg => error ("preplay error: " ^ msg) |
111 |
111 |
112 fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = |
112 fun thm_of_proof ctxt (Proof {fixes, assumptions, steps}) = |
113 let |
113 let |
114 val thy = Proof_Context.theory_of ctxt |
114 val thy = Proof_Context.theory_of ctxt |
115 |
115 |
116 val concl = |
116 val concl = |
117 (case try List.last steps of |
117 (case try List.last steps of |
118 SOME (Prove (_, [], _, t, _, _, _, _)) => t |
118 SOME (Prove (_, [], _, t, _, _, _, _)) => t |
119 | _ => raise Fail "preplay error: malformed subproof") |
119 | _ => raise Fail "preplay error: malformed subproof") |
120 |
120 |
121 val var_idx = maxidx_of_term concl + 1 |
121 val var_idx = maxidx_of_term concl + 1 |
122 fun var_of_free (x, T) = Var ((x, var_idx), T) |
122 fun var_of_free (x, T) = Var ((x, var_idx), T) |
123 val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees |
123 val subst = map (`var_of_free #> swap #> apfst Free) fixes |
124 in |
124 in |
125 Logic.list_implies (assms |> map snd, concl) |
125 Logic.list_implies (assumptions |> map snd, concl) |
126 |> subst_free subst |
126 |> subst_free subst |
127 |> Skip_Proof.make_thm thy |
127 |> Skip_Proof.make_thm thy |
128 end |
128 end |
129 |
129 |
130 (* may throw exceptions *) |
130 (* may throw exceptions *) |
242 |
242 |
243 fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) = |
243 fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) = |
244 Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths)) |
244 Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths)) |
245 | forced_outcome_of_step _ _ = Played Time.zeroTime |
245 | forced_outcome_of_step _ _ = Played Time.zeroTime |
246 |
246 |
247 fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) = |
247 fun preplay_outcome_of_isar_proof preplay_data (Proof {steps, ...}) = |
248 fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps |
248 fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps |
249 (Played Time.zeroTime) |
249 (Played Time.zeroTime) |
250 |
250 |
251 end; |
251 end; |