48 handle TimeLimit.TimeOut => (true, timeout) |
48 handle TimeLimit.TimeOut => (true, timeout) |
49 end |
49 end |
50 |
50 |
51 (* lookup facts in context *) |
51 (* lookup facts in context *) |
52 fun resolve_fact_names ctxt names = |
52 fun resolve_fact_names ctxt names = |
53 names |
53 (names |
54 |>> map string_for_label |
54 |>> map string_for_label |
55 |> op @ |
55 |> op @ |
56 |> maps (thms_of_name ctxt) |
56 |> maps (thms_of_name ctxt)) |
|
57 handle ERROR msg => error ("preplay error: " ^ msg) |
57 |
58 |
58 (* *) |
59 (* *) |
59 fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
60 fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
60 fun fact_of_subproof ctxt proof = |
61 fun fact_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) = |
61 let |
62 let |
62 val (fixed_frees, assms, concl) = split_proof proof |
63 val concl = (case try List.last steps of |
|
64 SOME (Prove (_, _, t, _)) => t |
|
65 | _ => error "preplay error: malformed subproof") |
63 val var_idx = maxidx_of_term concl + 1 |
66 val var_idx = maxidx_of_term concl + 1 |
64 fun var_of_free (x, T) = Var((x, var_idx), T) |
67 fun var_of_free (x, T) = Var((x, var_idx), T) |
65 val substitutions = |
68 val substitutions = |
66 map (`var_of_free #> swap #> apfst Free) fixed_frees |
69 map (`var_of_free #> swap #> apfst Free) fixed_frees |
67 val assms = assms |> map snd |
|
68 in |
70 in |
69 Logic.list_implies(assms, concl) |
71 Logic.list_implies (assms |> map snd, concl) |
70 |> subst_free substitutions |
72 |> subst_free substitutions |
71 |> thm_of_term ctxt |
73 |> thm_of_term ctxt |
72 end |
74 end |
73 |
75 |
74 exception ZEROTIME |
76 exception ZEROTIME |
76 let |
78 let |
77 val (t, subproofs, fact_names, obtain) = |
79 val (t, subproofs, fact_names, obtain) = |
78 (case step of |
80 (case step of |
79 Prove (_, _, t, By_Metis (subproofs, fact_names)) => |
81 Prove (_, _, t, By_Metis (subproofs, fact_names)) => |
80 (t, subproofs, fact_names, false) |
82 (t, subproofs, fact_names, false) |
81 | Obtain (_, xs, _, t, By_Metis (subproofs, fact_names)) => |
83 | Obtain (_, Fix xs, _, t, By_Metis (subproofs, fact_names)) => |
82 (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
84 (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
83 (see ~~/src/Pure/Isar/obtain.ML) *) |
85 (see ~~/src/Pure/Isar/obtain.ML) *) |
84 let |
86 let |
85 val thesis = Term.Free ("thesis", HOLogic.boolT) |
87 val thesis = Term.Free ("thesis", HOLogic.boolT) |
86 val thesis_prop = thesis |> HOLogic.mk_Trueprop |
88 val thesis_prop = thesis |> HOLogic.mk_Trueprop |
96 in |
98 in |
97 (prop, subproofs, fact_names, true) |
99 (prop, subproofs, fact_names, true) |
98 end |
100 end |
99 | _ => raise ZEROTIME) |
101 | _ => raise ZEROTIME) |
100 val facts = |
102 val facts = |
101 map (fact_of_subproof ctxt) subproofs @ |
103 map (fact_of_proof ctxt) subproofs @ |
102 resolve_fact_names ctxt fact_names |
104 resolve_fact_names ctxt fact_names |
103 val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
105 val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
104 |> obtain ? Config.put Metis_Tactic.new_skolem true |
106 |> obtain ? Config.put Metis_Tactic.new_skolem true |
105 val goal = |
107 val goal = |
106 Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t |
108 Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t |