equal
deleted
inserted
replaced
25 val mk_supp_ty: typ -> term -> term |
25 val mk_supp_ty: typ -> term -> term |
26 val mk_supp: term -> term |
26 val mk_supp: term -> term |
27 |
27 |
28 val mk_equiv: thm -> thm |
28 val mk_equiv: thm -> thm |
29 val safe_mk_equiv: thm -> thm |
29 val safe_mk_equiv: thm -> thm |
|
30 |
|
31 val mk_diff: term * term -> term |
|
32 val mk_union: term * term -> term |
|
33 val fold_union: term list -> term |
30 |
34 |
31 (* datatype operations *) |
35 (* datatype operations *) |
32 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
36 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
33 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
37 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
34 (term * typ * typ list) list list |
38 (term * typ * typ list) list list |
70 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
74 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
71 |
75 |
72 |
76 |
73 fun mk_equiv r = r RS @{thm eq_reflection}; |
77 fun mk_equiv r = r RS @{thm eq_reflection}; |
74 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
78 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
|
79 |
|
80 |
|
81 (* functions that construct differences and unions |
|
82 but avoid producing empty atom sets *) |
|
83 |
|
84 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
|
85 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
|
86 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
|
87 |
|
88 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} |
|
89 | mk_union (t1 , @{term "{}::atom set"}) = t1 |
|
90 | mk_union (@{term "{}::atom set"}, t2) = t2 |
|
91 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2) |
|
92 |
|
93 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} |
75 |
94 |
76 |
95 |
77 (** datatypes **) |
96 (** datatypes **) |
78 |
97 |
79 |
98 |