61 val elim_implies: thm -> thm -> thm |
61 val elim_implies: thm -> thm -> thm |
62 val forall_elim_var: int -> thm -> thm |
62 val forall_elim_var: int -> thm -> thm |
63 val forall_elim_vars: int -> thm -> thm |
63 val forall_elim_vars: int -> thm -> thm |
64 val instantiate': ctyp option list -> cterm option list -> thm -> thm |
64 val instantiate': ctyp option list -> cterm option list -> thm -> thm |
65 val forall_intr_frees: thm -> thm |
65 val forall_intr_frees: thm -> thm |
66 val unvarify_global: thm -> thm |
66 val unvarify_global: theory -> thm -> thm |
|
67 val unvarify_axiom: theory -> string -> thm |
67 val close_derivation: thm -> thm |
68 val close_derivation: thm -> thm |
68 val rename_params_rule: string list * int -> thm -> thm |
69 val rename_params_rule: string list * int -> thm -> thm |
69 val rename_boundvars: term -> term -> thm -> thm |
70 val rename_boundvars: term -> term -> thm -> thm |
70 val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory |
71 val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory |
71 val add_axiom_global: binding * term -> theory -> (string * thm) * theory |
72 val add_axiom_global: binding * term -> theory -> (string * thm) * theory |
374 in fold Thm.forall_intr frees th end; |
375 in fold Thm.forall_intr frees th end; |
375 |
376 |
376 |
377 |
377 (* unvarify_global: global schematic variables *) |
378 (* unvarify_global: global schematic variables *) |
378 |
379 |
379 fun unvarify_global th = |
380 fun unvarify_global thy th = |
380 let |
381 let |
381 val thy = Thm.theory_of_thm th; |
|
382 |
|
383 val prop = Thm.full_prop_of th; |
382 val prop = Thm.full_prop_of th; |
384 val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) |
383 val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) |
385 handle TERM (msg, _) => raise THM (msg, 0, [th]); |
384 handle TERM (msg, _) => raise THM (msg, 0, [th]); |
386 |
385 |
387 val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); |
386 val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); |
388 val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => |
387 val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => |
389 let val T' = Term_Subst.instantiateT instT T |
388 let val T' = Term_Subst.instantiateT instT T |
390 in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); |
389 in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); |
391 in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end; |
390 in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end; |
|
391 |
|
392 fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; |
392 |
393 |
393 |
394 |
394 (* close_derivation *) |
395 (* close_derivation *) |
395 |
396 |
396 fun close_derivation thm = |
397 fun close_derivation thm = |
457 |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); |
458 |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); |
458 val axm_name = Sign.full_name thy' b; |
459 val axm_name = Sign.full_name thy' b; |
459 val axm' = Thm.axiom thy' axm_name; |
460 val axm' = Thm.axiom thy' axm_name; |
460 val thm = |
461 val thm = |
461 Thm.instantiate (recover, []) axm' |
462 Thm.instantiate (recover, []) axm' |
462 |> unvarify_global |
463 |> unvarify_global thy' |
463 |> fold elim_implies of_sorts; |
464 |> fold elim_implies of_sorts; |
464 in ((axm_name, thm), thy') end; |
465 in ((axm_name, thm), thy') end; |
465 |
466 |
466 fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; |
467 fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; |
467 |
468 |
474 val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy; |
475 val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy; |
475 val axm_name = Sign.full_name thy' b; |
476 val axm_name = Sign.full_name thy' b; |
476 val axm' = Thm.axiom thy' axm_name; |
477 val axm' = Thm.axiom thy' axm_name; |
477 val thm = |
478 val thm = |
478 Thm.instantiate (recover, []) axm' |
479 Thm.instantiate (recover, []) axm' |
479 |> unvarify_global |
480 |> unvarify_global thy' |
480 |> fold_rev Thm.implies_intr prems; |
481 |> fold_rev Thm.implies_intr prems; |
481 in ((axm_name, thm), thy') end; |
482 in ((axm_name, thm), thy') end; |
482 |
483 |
483 fun add_def_global unchecked overloaded arg thy = |
484 fun add_def_global unchecked overloaded arg thy = |
484 add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy; |
485 add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy; |