56 val t = apply_fixes_concl env names concl |
56 val t = apply_fixes_concl env names concl |
57 in export_fixes env names (f ctxt' (thms1 @ thms2) t) end |
57 in export_fixes env names (f ctxt' (thms1 @ thms2) t) end |
58 |
58 |
59 fun replay_thm ctxt assumed nthms |
59 fun replay_thm ctxt assumed nthms |
60 (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) = |
60 (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) = |
61 if Z3_New_Replay_Methods.is_assumption rule then |
61 if Z3_New_Proof.is_assumption rule then |
62 (case Inttab.lookup assumed id of |
62 (case Inttab.lookup assumed id of |
63 SOME (_, thm) => thm |
63 SOME (_, thm) => thm |
64 | NONE => Thm.assume (SMT2_Util.certify ctxt concl)) |
64 | NONE => Thm.assume (SMT2_Util.certify ctxt concl)) |
65 else |
65 else |
66 under_fixes (Z3_New_Replay_Methods.method_for rule) ctxt |
66 under_fixes (Z3_New_Replay_Methods.method_for rule) ctxt |
113 val thms' = if exact then thms else th :: thms |
113 val thms' = if exact then thms else th :: thms |
114 in (((i, (id, th)) :: iidths, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end |
114 in (((i, (id, th)) :: iidths, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end |
115 |
115 |
116 fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...}) |
116 fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...}) |
117 (cx as ((iidths, thms), (ctxt, ptab))) = |
117 (cx as ((iidths, thms), (ctxt, ptab))) = |
118 if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then |
118 if Z3_New_Proof.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then |
119 let |
119 let |
120 val ct = SMT2_Util.certify ctxt concl |
120 val ct = SMT2_Util.certify ctxt concl |
121 val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) |
121 val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) |
122 val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 |
122 val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 |
123 in |
123 in |