# HG changeset patch
# User blanchet
# Date 1380111678 -7200
# Node ID eb3075935edf318eb33fd994cab0d33b624ddc8f
# Parent  028ec3e310ec8d5ddbd709311155b33140145d45
move useful functions to library

diff -r 028ec3e310ec -r eb3075935edf src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 13:39:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 14:21:18 2013 +0200
@@ -51,12 +51,6 @@
 val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
 fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
   strip_qnt_body @{const_name all} 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};
-fun invert_prems [t] = map s_not (HOLogic.disjuncts t)
-  | invert_prems ts = [mk_disjs (map s_not ts)];
-fun invert_prems_disj [t] = map s_not (HOLogic.disjuncts t)
-  | invert_prems_disj ts = [mk_disjs (map (mk_conjs o map s_not o HOLogic.disjuncts) ts)];
 fun abstract vs =
   let fun a n (t $ u) = a n t $ a n u
         | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b)
@@ -450,7 +444,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 sequential then maps invert_prems_disj matchedss else []) @
+      (if catch_all orelse sequential then maps negate_disj matchedss else []) @
       (if catch_all then [] else prems);
 
     val matchedsss' = AList.delete (op =) fun_name matchedsss
@@ -691,7 +685,7 @@
         ctr = #ctr (nth ctr_specs n),
         ctr_no = n,
         disc = #disc (nth ctr_specs n),
-        prems = maps (invert_prems o #prems) disc_eqns,
+        prems = maps (negate_conj o #prems) disc_eqns,
         auto_gen = true,
         user_eqn = undef_const};
     in
@@ -790,7 +784,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 (invert_prems o #prems) disc_eqns)
+            val prems = the_default (maps (negate_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 028ec3e310ec -r eb3075935edf src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 13:39:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 14:21:18 2013 +0200
@@ -52,6 +52,12 @@
      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 massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
   val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ list ->
@@ -63,6 +69,7 @@
     term -> term
   val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
     typ list -> term -> 'a -> 'a
+
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list) * local_theory
@@ -142,9 +149,21 @@
 fun s_not @{const True} = @{const False}
   | s_not @{const False} = @{const True}
   | s_not (@{const Not} $ t) = t
+  (* TODO: is the next case really needed? *)
   | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not 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;
+
+fun negate_conj [t] = s_not_disj t
+  | negate_conj ts = [mk_disjs (map s_not ts)];
+
+fun negate_disj [t] = s_not_disj t
+  | negate_disj ts = [mk_disjs (map (mk_conjs o s_not_disj) ts)];
+
 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