94 | _ => error "preplay error: malformed case split") |
94 | _ => error "preplay error: malformed case split") |
95 #> make_thm) cases |
95 #> make_thm) cases |
96 | Subblock proof => |
96 | Subblock proof => |
97 let |
97 let |
98 val (steps, last_step) = split_last proof |
98 val (steps, last_step) = split_last proof |
99 (* TODO: assuming Fix may only occur at the beginning of a subblock, |
|
100 this can be optimized *) |
|
101 val fixed_frees = |
|
102 fold (fn Fix xs => append (map Free xs) | _ => I) steps [] |
|
103 (* TODO: make sure the var indexnames are actually fresh *) |
|
104 fun var_of_free (Free (x, T)) = Var((x, 1), T) |
|
105 | var_of_free _ = error "preplay error: not a free variable" |
|
106 val substitutions = map (`var_of_free #> swap) fixed_frees |
|
107 val concl = |
99 val concl = |
108 (case last_step of |
100 (case last_step of |
109 Prove (_, _, t, _) => t |
101 Prove (_, _, t, _) => t |
110 | _ => error "preplay error: unexpected conclusion of subblock") |
102 | _ => error "preplay error: unexpected conclusion of subblock") |
|
103 (* TODO: assuming Fix may only occur at the beginning of a subblock, |
|
104 this can be optimized *) |
|
105 val fixed_frees = fold (fn Fix xs => append xs | _ => I) steps [] |
|
106 val var_idx = maxidx_of_term concl + 1 |
|
107 fun var_of_free (x, T) = Var((x, var_idx), T) |
|
108 val substitutions = |
|
109 map (`var_of_free #> swap #> apfst Free) fixed_frees |
111 in |
110 in |
112 concl |> subst_free substitutions |> make_thm |> single |
111 concl |> subst_free substitutions |> make_thm |> single |
113 end) |
112 end) |
114 val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
113 val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
115 |> obtain ? Config.put Metis_Tactic.new_skolem true |
114 |> obtain ? Config.put Metis_Tactic.new_skolem true |