187 fun curried_type (Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>prod\<close>, Ts), T])) = |
187 fun curried_type (Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>prod\<close>, Ts), T])) = |
188 Ts ---> T; |
188 Ts ---> T; |
189 |
189 |
190 fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs); |
190 fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs); |
191 |
191 |
192 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^const>\<open>True\<close>; |
192 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^Const>\<open>True\<close>; |
193 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^const>\<open>False\<close>; |
193 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^Const>\<open>False\<close>; |
194 val mk_dnf = mk_disjs o map mk_conjs; |
194 val mk_dnf = mk_disjs o map mk_conjs; |
195 |
195 |
196 val conjuncts_s = filter_out (curry (op aconv) \<^const>\<open>True\<close>) o HOLogic.conjuncts; |
196 val conjuncts_s = filter_out (curry (op aconv) \<^Const>\<open>True\<close>) o HOLogic.conjuncts; |
197 |
197 |
198 fun s_not \<^const>\<open>True\<close> = \<^const>\<open>False\<close> |
198 fun s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close> |
199 | s_not \<^const>\<open>False\<close> = \<^const>\<open>True\<close> |
199 | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close> |
200 | s_not (\<^const>\<open>Not\<close> $ t) = t |
200 | s_not \<^Const_>\<open>Not for t\<close> = t |
201 | s_not (\<^const>\<open>conj\<close> $ t $ u) = \<^const>\<open>disj\<close> $ s_not t $ s_not u |
201 | s_not \<^Const_>\<open>conj for t u\<close> = \<^Const>\<open>disj for \<open>s_not t\<close> \<open>s_not u\<close>\<close> |
202 | s_not (\<^const>\<open>disj\<close> $ t $ u) = \<^const>\<open>conj\<close> $ s_not t $ s_not u |
202 | s_not \<^Const_>\<open>disj for t u\<close> = \<^Const>\<open>conj for \<open>s_not t\<close> \<open>s_not u\<close>\<close> |
203 | s_not t = \<^const>\<open>Not\<close> $ t; |
203 | s_not t = \<^Const>\<open>Not for t\<close>; |
204 |
204 |
205 val s_not_conj = conjuncts_s o s_not o mk_conjs; |
205 val s_not_conj = conjuncts_s o s_not o mk_conjs; |
206 |
206 |
207 fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^const>\<open>False\<close>] else cs; |
207 fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^Const>\<open>False\<close>] else cs; |
208 fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs; |
208 fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs; |
209 |
209 |
210 fun propagate_units css = |
210 fun propagate_units css = |
211 (case List.partition (can the_single) css of |
211 (case List.partition (can the_single) css of |
212 ([], _) => css |
212 ([], _) => css |
213 | ([u] :: uss, css') => |
213 | ([u] :: uss, css') => |
214 [u] :: propagate_units (map (propagate_unit_neg (s_not u)) |
214 [u] :: propagate_units (map (propagate_unit_neg (s_not u)) |
215 (map (propagate_unit_pos u) (uss @ css')))); |
215 (map (propagate_unit_pos u) (uss @ css')))); |
216 |
216 |
217 fun s_conjs cs = |
217 fun s_conjs cs = |
218 if member (op aconv) cs \<^const>\<open>False\<close> then \<^const>\<open>False\<close> |
218 if member (op aconv) cs \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close> |
219 else mk_conjs (remove (op aconv) \<^const>\<open>True\<close> cs); |
219 else mk_conjs (remove (op aconv) \<^Const>\<open>True\<close> cs); |
220 |
220 |
221 fun s_disjs ds = |
221 fun s_disjs ds = |
222 if member (op aconv) ds \<^const>\<open>True\<close> then \<^const>\<open>True\<close> |
222 if member (op aconv) ds \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close> |
223 else mk_disjs (remove (op aconv) \<^const>\<open>False\<close> ds); |
223 else mk_disjs (remove (op aconv) \<^Const>\<open>False\<close> ds); |
224 |
224 |
225 fun s_dnf css0 = |
225 fun s_dnf css0 = |
226 let val css = propagate_units css0 in |
226 let val css = propagate_units css0 in |
227 if null css then |
227 if null css then |
228 [\<^const>\<open>False\<close>] |
228 [\<^Const>\<open>False\<close>] |
229 else if exists null css then |
229 else if exists null css then |
230 [] |
230 [] |
231 else |
231 else |
232 map (fn c :: cs => (c, cs)) css |
232 map (fn c :: cs => (c, cs)) css |
233 |> AList.coalesce (op =) |
233 |> AList.coalesce (op =) |