38 val resort_tfree_or_tvar: sort -> typ -> typ |
38 val resort_tfree_or_tvar: sort -> typ -> typ |
39 val variant_types: string list -> sort list -> Proof.context -> |
39 val variant_types: string list -> sort list -> Proof.context -> |
40 (string * sort) list * Proof.context |
40 (string * sort) list * Proof.context |
41 val variant_tfrees: string list -> Proof.context -> typ list * Proof.context |
41 val variant_tfrees: string list -> Proof.context -> typ list * Proof.context |
42 |
42 |
43 val name_of_const: string -> term -> string |
43 val base_name_of_typ: typ -> string |
|
44 val name_of_const: string -> (typ -> typ) -> term -> string |
44 |
45 |
45 val typ_subst_nonatomic: (typ * typ) list -> typ -> typ |
46 val typ_subst_nonatomic: (typ * typ) list -> typ -> typ |
46 val subst_nonatomic_types: (typ * typ) list -> term -> term |
47 val subst_nonatomic_types: (typ * typ) list -> term -> term |
47 |
48 |
48 val lhs_head_of : thm -> term |
49 val lhs_head_of : thm -> term |
196 |
197 |
197 fun variant_tfrees ss = |
198 fun variant_tfrees ss = |
198 apfst (map TFree) o |
199 apfst (map TFree) o |
199 variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type}); |
200 variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type}); |
200 |
201 |
201 fun name_of_const what t = |
202 fun add_components_of_typ (Type (s, Ts)) = |
|
203 cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts |
|
204 | add_components_of_typ _ = I; |
|
205 |
|
206 fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []); |
|
207 |
|
208 fun suffix_with_type s (Type (_, Ts)) = |
|
209 space_implode "_" (s :: fold_rev add_components_of_typ Ts []) |
|
210 | suffix_with_type s _ = s; |
|
211 |
|
212 fun name_of_const what get_fcT t = |
202 (case head_of t of |
213 (case head_of t of |
203 Const (s, _) => s |
214 Const (s, T) => suffix_with_type s (get_fcT T) |
204 | Free (s, _) => s |
215 | Free (s, T) => suffix_with_type s (get_fcT T) |
205 | _ => error ("Cannot extract name of " ^ what)); |
216 | _ => error ("Cannot extract name of " ^ what)); |
206 |
217 |
207 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*) |
218 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*) |
208 fun typ_subst_nonatomic [] = I |
219 fun typ_subst_nonatomic [] = I |
209 | typ_subst_nonatomic inst = |
220 | typ_subst_nonatomic inst = |