7 signature CODE_UNIT = |
7 signature CODE_UNIT = |
8 sig |
8 sig |
9 (*typ instantiations*) |
9 (*typ instantiations*) |
10 val typscheme: theory -> string * typ -> (string * sort) list * typ |
10 val typscheme: theory -> string * typ -> (string * sort) list * typ |
11 val inst_thm: theory -> sort Vartab.table -> thm -> thm |
11 val inst_thm: theory -> sort Vartab.table -> thm -> thm |
12 val constrain_thm: theory -> sort -> thm -> thm |
|
13 |
12 |
14 (*constant aliasses*) |
13 (*constant aliasses*) |
15 val add_const_alias: thm -> theory -> theory |
14 val add_const_alias: thm -> theory -> theory |
16 val triv_classes: theory -> class list |
15 val triv_classes: theory -> class list |
17 val resubst_alias: theory -> string -> string |
16 val resubst_alias: theory -> string -> string |
76 fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v |
75 fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v |
77 of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) |
76 of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) |
78 (tvar, (v, inter_sort (sort, sort')))) |
77 (tvar, (v, inter_sort (sort, sort')))) |
79 | NONE => NONE; |
78 | NONE => NONE; |
80 val insts = map_filter mk_inst tvars; |
79 val insts = map_filter mk_inst tvars; |
81 in Thm.instantiate (insts, []) thm end; |
|
82 |
|
83 fun constrain_thm thy sort thm = |
|
84 let |
|
85 val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)) sort |
|
86 val tvars = (Term.add_tvars o Thm.prop_of) thm []; |
|
87 fun mk_inst (tvar as (v, sort)) = pairself (Thm.ctyp_of thy o TVar o pair v) |
|
88 (sort, constrain sort) |
|
89 val insts = map mk_inst tvars; |
|
90 in Thm.instantiate (insts, []) thm end; |
80 in Thm.instantiate (insts, []) thm end; |
91 |
81 |
92 fun expand_eta thy k thm = |
82 fun expand_eta thy k thm = |
93 let |
83 let |
94 val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; |
84 val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; |