equal
deleted
inserted
replaced
120 |
120 |
121 val mk_map: int -> typ list -> typ list -> term -> term |
121 val mk_map: int -> typ list -> typ list -> term -> term |
122 val mk_pred: typ list -> term -> term |
122 val mk_pred: typ list -> term -> term |
123 val mk_rel: int -> typ list -> typ list -> term -> term |
123 val mk_rel: int -> typ list -> typ list -> term -> term |
124 val mk_set: typ list -> term -> term |
124 val mk_set: typ list -> term -> term |
125 val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term |
125 val build_map: Proof.context -> typ list -> typ list -> (typ * typ -> term) -> typ * typ -> term |
126 val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) -> |
126 val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> typ list -> |
127 typ * typ -> term |
127 (typ * typ -> term) -> typ * typ -> term |
128 val build_set: Proof.context -> typ -> typ -> term |
128 val build_set: Proof.context -> typ -> typ -> term |
129 val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list |
129 val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list |
130 val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list -> |
130 val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list -> |
131 'a list |
131 'a list |
132 |
132 |
742 fun mk_rel live Ts Us t = |
742 fun mk_rel live Ts Us t = |
743 let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in |
743 let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in |
744 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
744 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
745 end; |
745 end; |
746 |
746 |
747 fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts build_simple = |
747 fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts simple_Us build_simple = |
748 let |
748 let |
749 fun build (TU as (T, U)) = |
749 fun build (TU as (T, U)) = |
750 if exists (curry (op =) T) simple_Ts then |
750 if exists (curry (op =) T) simple_Ts orelse exists (curry (op =) U) simple_Us then |
751 build_simple TU |
751 build_simple TU |
752 else if T = U andalso not (exists_subtype_in simple_Ts T) then |
752 else if T = U andalso not (exists_subtype_in simple_Ts T) andalso |
|
753 not (exists_subtype_in simple_Us U) then |
753 const T |
754 const T |
754 else |
755 else |
755 (case TU of |
756 (case TU of |
756 (Type (s, Ts), Type (s', Us)) => |
757 (Type (s, Ts), Type (s', Us)) => |
757 if s = s' then |
758 if s = s' then |