equal
deleted
inserted
replaced
46 val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context |
46 val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context |
47 val import_inst: bool -> term list -> Proof.context -> |
47 val import_inst: bool -> term list -> Proof.context -> |
48 (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context |
48 (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context |
49 val importT_terms: term list -> Proof.context -> term list * Proof.context |
49 val importT_terms: term list -> Proof.context -> term list * Proof.context |
50 val import_terms: bool -> term list -> Proof.context -> term list * Proof.context |
50 val import_terms: bool -> term list -> Proof.context -> term list * Proof.context |
51 val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context |
51 val importT_thms: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context |
52 val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context |
52 val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context |
53 val import_thms: bool -> thm list -> Proof.context -> |
53 val import_thms: bool -> thm list -> Proof.context -> |
54 ((ctyp list * cterm list) * thm list) * Proof.context |
54 ((ctyp list * cterm list) * thm list) * Proof.context |
55 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
55 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
56 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
56 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
375 |
375 |
376 fun import_terms is_open ts ctxt = |
376 fun import_terms is_open ts ctxt = |
377 let val (inst, ctxt') = import_inst is_open ts ctxt |
377 let val (inst, ctxt') = import_inst is_open ts ctxt |
378 in (map (TermSubst.instantiate inst) ts, ctxt') end; |
378 in (map (TermSubst.instantiate inst) ts, ctxt') end; |
379 |
379 |
380 fun importT ths ctxt = |
380 fun importT_thms ths ctxt = |
381 let |
381 let |
382 val thy = ProofContext.theory_of ctxt; |
382 val thy = ProofContext.theory_of ctxt; |
383 val certT = Thm.ctyp_of thy; |
383 val certT = Thm.ctyp_of thy; |
384 val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; |
384 val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; |
385 val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT; |
385 val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT; |
408 |
408 |
409 fun gen_trade imp exp f ctxt ths = |
409 fun gen_trade imp exp f ctxt ths = |
410 let val ((_, ths'), ctxt') = imp ths ctxt |
410 let val ((_, ths'), ctxt') = imp ths ctxt |
411 in exp ctxt' ctxt (f ctxt' ths') end; |
411 in exp ctxt' ctxt (f ctxt' ths') end; |
412 |
412 |
413 val tradeT = gen_trade importT exportT; |
413 val tradeT = gen_trade importT_thms exportT; |
414 val trade = gen_trade (import_thms true) export; |
414 val trade = gen_trade (import_thms true) export; |
415 |
415 |
416 |
416 |
417 (* focus on outermost parameters *) |
417 (* focus on outermost parameters *) |
418 |
418 |