# HG changeset patch
# User blanchet
# Date 1381083846 -7200
# Node ID 447354985f6a774e0dfb61dca4e2e34bc0ffdbf8
# Parent  7be49e2bfccc8e8449df9e95da2cce5ce6a72c2d
generate optimized DNF formula

diff -r 7be49e2bfccc -r 447354985f6a src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 06 20:24:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 06 20:24:06 2013 +0200
@@ -602,7 +602,7 @@
         else primrec_error_eqn "not a constructor" ctr) [] rhs' []
       |> AList.group (op =);
 
-    val ctr_premss = map (single o mk_disjs o map mk_conjs o snd) cond_ctrs;
+    val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs);
     val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
         binder_types (fastype_of ctr)
         |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args =>
@@ -652,7 +652,7 @@
 fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
     ({fun_args, ctr_no, prems, ...} : co_eqn_data_disc) =
   if is_none (#pred (nth ctr_specs ctr_no)) then I else
-    mk_conjs prems
+    s_conjs prems
     |> curry subst_bounds (List.rev fun_args)
     |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
     |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
@@ -756,7 +756,7 @@
         #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs [])
         #> maps (uncurry (map o pair)
           #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
-              ((c, c', a orelse a'), (x, s_not (mk_conjs y)))
+              ((c, c', a orelse a'), (x, s_not (s_conjs y)))
             ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
             ||> Logic.list_implies
             ||> curry Logic.list_all (map dest_Free fun_args))))
diff -r 7be49e2bfccc -r 447354985f6a src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 06 20:24:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 06 20:24:06 2013 +0200
@@ -51,10 +51,11 @@
      nested_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
-  val mk_conjs: term list -> term
-  val mk_disjs: term list -> term
   val s_not: term -> term
   val s_not_conj: term list -> term list
+  val s_conjs: term list -> term
+  val s_disjs: term list -> term
+  val s_dnf: term list list -> term list
 
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
@@ -161,6 +162,41 @@
 
 val s_not_conj = conjuncts_s o s_not o mk_conjs;
 
+fun s_conj c @{const True} = c
+  | s_conj c d = HOLogic.mk_conj (c, d);
+
+fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs;
+
+fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
+
+fun propagate_units css =
+  (case List.partition (can the_single) css of
+     ([], _) => css
+   | ([u] :: uss, css') =>
+     [u] :: propagate_units (map (propagate_unit_neg (s_not u))
+       (map (propagate_unit_pos u) (uss @ css'))));
+
+fun s_conjs cs =
+  if member (op aconv) cs @{const False} then @{const False}
+  else mk_conjs (remove (op aconv) @{const True} cs);
+
+fun s_disjs ds =
+  if member (op aconv) ds @{const True} then @{const True}
+  else mk_disjs (remove (op aconv) @{const False} ds);
+
+fun s_dnf css0 =
+  let val css = propagate_units css0 in
+    if null css then
+      [@{const False}]
+    else if exists null css then
+      []
+    else
+      map (fn c :: cs => (c, cs)) css
+      |> AList.coalesce (op =)
+      |> map (fn (c, css) => c :: s_dnf css)
+      |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)])
+  end;
+
 fun factor_out_types ctxt massage destU U T =
   (case try destU U of
     SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt