# HG changeset patch
# User blanchet
# Date 1381083845 -7200
# Node ID 7be49e2bfccc8e8449df9e95da2cce5ce6a72c2d
# Parent  4a7aa85b6b47cd844ca58b75594cf16260cea737
rationalized negation code

diff -r 4a7aa85b6b47 -r 7be49e2bfccc src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Oct 05 11:06:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 06 20:24:05 2013 +0200
@@ -507,7 +507,7 @@
     val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
     val prems = map (abstract (List.rev fun_args)) prems';
     val real_prems =
-      (if catch_all orelse seq then maps negate_disj matchedss else []) @
+      (if catch_all orelse seq then maps s_not_conj matchedss else []) @
       (if catch_all then [] else prems);
 
     val matchedsss' = AList.delete (op =) fun_name matchedsss
@@ -784,7 +784,7 @@
         ctr = #ctr (nth ctr_specs n),
         ctr_no = n,
         disc = #disc (nth ctr_specs n),
-        prems = maps (negate_conj o #prems) disc_eqns,
+        prems = maps (s_not_conj o #prems) disc_eqns,
         auto_gen = true,
         user_eqn = undef_const};
     in
@@ -888,7 +888,7 @@
           let
             val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs;
             val ctr_no = find_index (equal ctr o #ctr) ctr_specs;
-            val prems = the_default (maps (negate_conj o #prems) disc_eqns)
+            val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
                 (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
             val sel_corec = find_index (equal sel) (#sels ctr_spec)
               |> nth (#sel_corecs ctr_spec);
diff -r 4a7aa85b6b47 -r 7be49e2bfccc src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sat Oct 05 11:06:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 06 20:24:05 2013 +0200
@@ -51,12 +51,10 @@
      nested_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
-  val s_not: term -> term
   val mk_conjs: term list -> term
   val mk_disjs: term list -> term
-  val s_not_disj: term -> term list
-  val negate_conj: term list -> term list
-  val negate_disj: term list -> term list
+  val s_not: term -> term
+  val s_not_conj: term list -> term list
 
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
@@ -148,21 +146,20 @@
 fun unexpected_corec_call ctxt t =
   error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
 
-fun s_not @{const True} = @{const False}
-  | s_not @{const False} = @{const True}
-  | s_not (@{const Not} $ t) = t
-  | s_not t = HOLogic.mk_not t
-
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
 
-val s_not_disj = map s_not o HOLogic.disjuncts;
+val conjuncts_s = filter_out (curry (op =) @{const True}) o HOLogic.conjuncts;
 
-fun negate_conj [t] = s_not_disj t
-  | negate_conj ts = [mk_disjs (map s_not ts)];
+fun s_not @{const True} = @{const False}
+  | s_not @{const False} = @{const True}
+  | s_not (@{const Not} $ t) = t
+  | s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u
+  | s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u
+  | s_not (@{const implies} $ t $ u) = @{const conj} $ t $ s_not u
+  | s_not t = @{const Not} $ t;
 
-fun negate_disj [t] = s_not_disj t
-  | negate_disj ts = [mk_disjs (map (mk_conjs o s_not_disj) ts)];
+val s_not_conj = conjuncts_s o s_not o mk_conjs;
 
 fun factor_out_types ctxt massage destU U T =
   (case try destU U of
@@ -230,8 +227,8 @@
       (case Term.strip_comb t of
         (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
       | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
-        fld (conds @ HOLogic.conjuncts cond) then_branch
-        o fld (conds @ s_not_disj cond) else_branch
+        fld (conds @ conjuncts_s cond) then_branch
+        o fld (conds @ s_not_conj [cond]) else_branch
       | (Const (c, _), args as _ :: _ :: _) =>
         let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
           if n >= 0 andalso n < length args then
@@ -241,7 +238,7 @@
                 NONE => apsnd (f conds t)
               | SOME (conds', branches) =>
                 apfst (cons s) o fold_rev (uncurry fld)
-                  (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
+                  (map (append conds o conjuncts_s) conds' ~~ branches))
             | _ => apsnd (f conds t))
           else
             apsnd (f conds t)