47 |
47 |
48 val mk_diff: term * term -> term |
48 val mk_diff: term * term -> term |
49 val mk_append: term * term -> term |
49 val mk_append: term * term -> term |
50 val mk_union: term * term -> term |
50 val mk_union: term * term -> term |
51 val fold_union: term list -> term |
51 val fold_union: term list -> term |
|
52 val fold_append: term list -> term |
52 val mk_conj: term * term -> term |
53 val mk_conj: term * term -> term |
53 val fold_conj: term list -> term |
54 val fold_conj: term list -> term |
54 |
55 |
55 (* fresh arguments for a term *) |
56 (* fresh arguments for a term *) |
56 val fresh_args: Proof.context -> term -> term list |
57 val fresh_args: Proof.context -> term -> term list |
142 (* functions that construct differences, appends and unions |
143 (* functions that construct differences, appends and unions |
143 but avoid producing empty atom sets or empty atom lists *) |
144 but avoid producing empty atom sets or empty atom lists *) |
144 |
145 |
145 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
146 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
146 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
147 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
|
148 | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"} |
|
149 | mk_diff (t1, @{term "set ([]::atom list)"}) = t1 |
147 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
150 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
148 |
151 |
149 fun mk_append (t1, @{term "[]::atom list"}) = t1 |
152 fun mk_append (t1, @{term "[]::atom list"}) = t1 |
150 | mk_append (@{term "[]::atom list"}, t2) = t2 |
153 | mk_append (@{term "[]::atom list"}, t2) = t2 |
151 | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) |
154 | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) |
152 |
155 |
153 fun mk_union (t1, @{term "{}::atom set"}) = t1 |
156 fun mk_union (t1, @{term "{}::atom set"}) = t1 |
154 | mk_union (@{term "{}::atom set"}, t2) = t2 |
157 | mk_union (@{term "{}::atom set"}, t2) = t2 |
|
158 | mk_union (t1, @{term "set ([]::atom list)"}) = t1 |
|
159 | mk_union (@{term "set ([]::atom list)"}, t2) = t2 |
155 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) |
160 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) |
156 |
161 |
157 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} |
162 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} |
|
163 fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"} |
158 |
164 |
159 fun mk_conj (t1, @{term "True"}) = t1 |
165 fun mk_conj (t1, @{term "True"}) = t1 |
160 | mk_conj (@{term "True"}, t2) = t2 |
166 | mk_conj (@{term "True"}, t2) = t2 |
161 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
167 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
162 |
168 |