289 |
289 |
290 fun assume_witness thy t = |
290 fun assume_witness thy t = |
291 Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); |
291 Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); |
292 |
292 |
293 fun prove_witness ctxt t tac = |
293 fun prove_witness ctxt t tac = |
294 Witness (t, Goal.close_result (Goal.prove ctxt [] [] (Logic.protect t) (fn _ => |
294 Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ => |
295 Tactic.rtac Drule.protectI 1 THEN tac))); |
295 Tactic.rtac Drule.protectI 1 THEN tac))); |
296 |
296 |
297 val close_witness = map_witness (fn (t, th) => (t, Goal.close_result th)); |
297 val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th)); |
298 |
298 |
299 fun conclude_witness (Witness (_, th)) = |
299 fun conclude_witness (Witness (_, th)) = |
300 Goal.close_result (MetaSimplifier.norm_hhf_protect (Goal.conclude th)); |
300 Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th)); |
301 |
301 |
302 fun compose_witness (Witness (_, th)) r = |
302 fun compose_witness (Witness (_, th)) r = |
303 let |
303 let |
304 val th' = Goal.conclude th; |
304 val th' = Goal.conclude th; |
305 val A = Thm.cprem_of r 1; |
305 val A = Thm.cprem_of r 1; |