44 string -> term list list -> term list -> Proof.context -> bool -> Proof.state -> |
44 string -> term list list -> term list -> Proof.context -> bool -> Proof.state -> |
45 Proof.state |
45 Proof.state |
46 val transform_witness: morphism -> witness -> witness |
46 val transform_witness: morphism -> witness -> witness |
47 val conclude_witness: witness -> thm |
47 val conclude_witness: witness -> thm |
48 val pretty_witness: Proof.context -> witness -> Pretty.T |
48 val pretty_witness: Proof.context -> witness -> Pretty.T |
49 val instT_type: typ Symtab.table -> typ -> typ |
|
50 val instT_term: typ Symtab.table -> term -> term |
|
51 val instT_thm: theory -> typ Symtab.table -> thm -> thm |
|
52 val instT_morphism: theory -> typ Symtab.table -> morphism |
49 val instT_morphism: theory -> typ Symtab.table -> morphism |
53 val inst_term: typ Symtab.table * term Symtab.table -> term -> term |
|
54 val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm |
|
55 val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism |
50 val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism |
56 val satisfy_thm: witness list -> thm -> thm |
|
57 val satisfy_morphism: witness list -> morphism |
51 val satisfy_morphism: witness list -> morphism |
58 val satisfy_facts: witness list -> |
|
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 option |
52 val eq_morphism: theory -> thm list -> morphism option |
62 val transfer_morphism: theory -> morphism |
53 val transfer_morphism: theory -> morphism |
63 val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
54 val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
64 Context.generic -> (string * thm list) list * Context.generic |
55 Context.generic -> (string * thm list) list * Context.generic |
65 val init: context_i -> Context.generic -> Context.generic |
56 val init: context_i -> Context.generic -> Context.generic |
459 (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of |
450 (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of |
460 NONE => I |
451 NONE => I |
461 | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm)); |
452 | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm)); |
462 |
453 |
463 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; |
454 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; |
464 val satisfy_facts = facts_map o transform_ctxt o satisfy_morphism; |
|
465 |
455 |
466 |
456 |
467 (* rewriting with equalities *) |
457 (* rewriting with equalities *) |
468 |
458 |
469 fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism |
459 fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism |