equal
deleted
inserted
replaced
113 val set_transfer_of_bnf: bnf -> thm list |
113 val set_transfer_of_bnf: bnf -> thm list |
114 val wit_thms_of_bnf: bnf -> thm list |
114 val wit_thms_of_bnf: bnf -> thm list |
115 val wit_thmss_of_bnf: bnf -> thm list list |
115 val wit_thmss_of_bnf: bnf -> thm list list |
116 |
116 |
117 val mk_map: int -> typ list -> typ list -> term -> term |
117 val mk_map: int -> typ list -> typ list -> term -> term |
|
118 val mk_pred: typ list -> term -> term |
118 val mk_rel: int -> typ list -> typ list -> term -> term |
119 val mk_rel: int -> typ list -> typ list -> term -> term |
119 val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term |
120 val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term |
120 val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) -> |
121 val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) -> |
121 typ * typ -> term |
122 typ * typ -> term |
122 val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list |
123 val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list |
710 fun mk_map live Ts Us t = |
711 fun mk_map live Ts Us t = |
711 let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in |
712 let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in |
712 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
713 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
713 end; |
714 end; |
714 |
715 |
|
716 fun mk_pred Ts t = |
|
717 let val Type (_, Ts0) = domain_type (body_fun_type (fastype_of t)) in |
|
718 Term.subst_atomic_types (Ts0 ~~ Ts) t |
|
719 end; |
|
720 |
715 fun mk_rel live Ts Us t = |
721 fun mk_rel live Ts Us t = |
716 let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in |
722 let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in |
717 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
723 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
718 end; |
724 end; |
719 |
725 |