33 |
33 |
34 val mk_diff: term * term -> term |
34 val mk_diff: term * term -> term |
35 val mk_append: term * term -> term |
35 val mk_append: term * term -> term |
36 val mk_union: term * term -> term |
36 val mk_union: term * term -> term |
37 val fold_union: term list -> term |
37 val fold_union: term list -> term |
|
38 val mk_conj: term * term -> term |
|
39 val fold_conj: term list -> term |
38 |
40 |
39 (* datatype operations *) |
41 (* datatype operations *) |
40 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
42 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
41 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
43 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
42 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
44 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
100 |
102 |
101 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
103 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
102 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
104 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
103 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
105 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
104 |
106 |
105 fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"} |
107 fun mk_append (t1, @{term "[]::atom list"}) = t1 |
106 | mk_append (t1, @{term "[]::atom list"}) = t1 |
|
107 | mk_append (@{term "[]::atom list"}, t2) = t2 |
108 | mk_append (@{term "[]::atom list"}, t2) = t2 |
108 | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) |
109 | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) |
109 |
110 |
110 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} |
111 fun mk_union (t1, @{term "{}::atom set"}) = t1 |
111 | mk_union (t1 , @{term "{}::atom set"}) = t1 |
|
112 | mk_union (@{term "{}::atom set"}, t2) = t2 |
112 | mk_union (@{term "{}::atom set"}, t2) = t2 |
113 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) |
113 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) |
114 |
114 |
115 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} |
115 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} |
116 |
116 |
117 |
117 fun mk_conj (t1, @{term "True"}) = t1 |
118 |
118 | mk_conj (@{term "True"}, t2) = t2 |
|
119 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
|
120 |
|
121 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
119 |
122 |
120 (** datatypes **) |
123 (** datatypes **) |
121 |
124 |
122 |
125 |
123 (* returns the type of the nth datatype *) |
126 (* returns the type of the nth datatype *) |