79 val import: bool -> thm list -> Proof.context -> |
79 val import: bool -> thm list -> Proof.context -> |
80 ((ctyp TVars.table * cterm Vars.table) * thm list) * Proof.context |
80 ((ctyp TVars.table * cterm Vars.table) * thm list) * Proof.context |
81 val import_vars: Proof.context -> thm -> thm |
81 val import_vars: Proof.context -> thm -> thm |
82 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
82 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
83 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
83 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
|
84 val dest_abs: term -> Proof.context -> ((string * typ) * term) * Proof.context |
|
85 val dest_abs_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context |
|
86 val dest_all: term -> Proof.context -> ((string * typ) * term) * Proof.context |
|
87 val dest_all_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context |
84 val is_bound_focus: Proof.context -> bool |
88 val is_bound_focus: Proof.context -> bool |
85 val set_bound_focus: bool -> Proof.context -> Proof.context |
89 val set_bound_focus: bool -> Proof.context -> Proof.context |
86 val restore_bound_focus: Proof.context -> Proof.context -> Proof.context |
90 val restore_bound_focus: Proof.context -> Proof.context -> Proof.context |
87 val focus_params: binding list option -> term -> Proof.context -> |
91 val focus_params: binding list option -> term -> Proof.context -> |
88 (string list * (string * typ) list) * Proof.context |
92 (string list * (string * typ) list) * Proof.context |
648 |
652 |
649 val tradeT = gen_trade importT exportT; |
653 val tradeT = gen_trade importT exportT; |
650 val trade = gen_trade (import true) export; |
654 val trade = gen_trade (import true) export; |
651 |
655 |
652 |
656 |
|
657 (* destruct binders *) |
|
658 |
|
659 local |
|
660 |
|
661 fun gen_dest_abs exn dest term_of arg ctxt = |
|
662 (case term_of arg of |
|
663 Abs (a, T, _) => |
|
664 let |
|
665 val (x, ctxt') = yield_singleton bound_fixes (a, T) ctxt; |
|
666 val res = dest x arg handle Term.USED_FREE _ => |
|
667 raise Fail ("Bad context: clash of fresh free for bound: " ^ |
|
668 Syntax.string_of_term ctxt (Free (x, T)) ^ " vs. " ^ |
|
669 Syntax.string_of_term ctxt' (Free (x, T))); |
|
670 in (res, ctxt') end |
|
671 | _ => raise exn ("dest_abs", [arg])); |
|
672 |
|
673 in |
|
674 |
|
675 val dest_abs = gen_dest_abs TERM Term.dest_abs_fresh I; |
|
676 val dest_abs_cterm = gen_dest_abs CTERM Thm.dest_abs_fresh Thm.term_of; |
|
677 |
|
678 fun dest_all t ctxt = |
|
679 (case t of |
|
680 Const ("Pure.all", _) $ u => dest_abs u ctxt |
|
681 | _ => raise TERM ("dest_all", [t])); |
|
682 |
|
683 fun dest_all_cterm ct ctxt = |
|
684 (case Thm.term_of ct of |
|
685 Const ("Pure.all", _) $ _ => dest_abs_cterm (Thm.dest_arg ct) ctxt |
|
686 | _ => raise CTERM ("dest_all", [ct])); |
|
687 |
|
688 end; |
|
689 |
|
690 |
653 (* focus on outermost parameters: \<And>x y z. B *) |
691 (* focus on outermost parameters: \<And>x y z. B *) |
654 |
692 |
655 val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false); |
693 val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false); |
656 val is_bound_focus = Config.apply bound_focus; |
694 val is_bound_focus = Config.apply bound_focus; |
657 val set_bound_focus = Config.put bound_focus; |
695 val set_bound_focus = Config.put bound_focus; |