53 val satisfy_thm: witness list -> thm -> thm |
53 val satisfy_thm: witness list -> thm -> thm |
54 val satisfy_morphism: witness list -> morphism |
54 val satisfy_morphism: witness list -> morphism |
55 val satisfy_facts: witness list -> |
55 val satisfy_facts: witness list -> |
56 (Attrib.binding * (thm list * Attrib.src list) list) list -> |
56 (Attrib.binding * (thm list * Attrib.src list) list) list -> |
57 (Attrib.binding * (thm list * Attrib.src list) list) list |
57 (Attrib.binding * (thm list * Attrib.src list) list) list |
58 val generalize_facts: Proof.context -> Proof.context -> |
|
59 (Attrib.binding * (thm list * Attrib.src list) list) list -> |
|
60 (Attrib.binding * (thm list * Attrib.src list) list) list |
|
61 val eq_morphism: theory -> thm list -> morphism |
58 val eq_morphism: theory -> thm list -> morphism |
62 val transfer_morphism: theory -> morphism |
59 val transfer_morphism: theory -> morphism |
63 val init: context_i -> Context.generic -> Context.generic |
60 val init: context_i -> Context.generic -> Context.generic |
64 val activate_i: context_i -> Proof.context -> context_i * Proof.context |
61 val activate_i: context_i -> Proof.context -> context_i * Proof.context |
65 val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context |
62 val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context |
454 fun eq_morphism thy thms = Morphism.morphism |
451 fun eq_morphism thy thms = Morphism.morphism |
455 {binding = I, |
452 {binding = I, |
456 typ = I, |
453 typ = I, |
457 term = MetaSimplifier.rewrite_term thy thms [], |
454 term = MetaSimplifier.rewrite_term thy thms [], |
458 fact = map (MetaSimplifier.rewrite_rule thms)}; |
455 fact = map (MetaSimplifier.rewrite_rule thms)}; |
459 |
|
460 |
|
461 (* generalize type/term parameters *) |
|
462 |
|
463 val maxidx_atts = fold Args.maxidx_values; |
|
464 |
|
465 fun generalize_facts inner outer facts = |
|
466 let |
|
467 val thy = ProofContext.theory_of inner; |
|
468 val maxidx = |
|
469 fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1; |
|
470 val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer; |
|
471 val exp_term = Drule.term_rule thy (singleton exp_fact); |
|
472 val exp_typ = Logic.type_map exp_term; |
|
473 val morphism = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
|
474 in facts_map (morph_ctxt morphism) facts end; |
|
475 |
456 |
476 |
457 |
477 (* transfer to theory using closure *) |
458 (* transfer to theory using closure *) |
478 |
459 |
479 fun transfer_morphism thy = |
460 fun transfer_morphism thy = |