# HG changeset patch
# User wenzelm
# Date 1321045747 -3600
# Node ID 98af01f897c98de7cf455063c18977bf7c70e673
# Parent  77c5b334a7ae607a151dd3e7d5b04c96d6ba2c37# Parent  dcd02d1a25d7d495f5cb37d6e85be28167544c13
merged

diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Nov 11 22:09:07 2011 +0100
@@ -100,12 +100,12 @@
   val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
   fun subtract_nat compfuns (_ : typ) =
     let
-      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
+      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
     in
       absdummy @{typ nat} (absdummy @{typ nat}
         (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
           (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
-          Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
+          Predicate_Compile_Aux.mk_empty compfuns @{typ nat} $
           Predicate_Compile_Aux.mk_single compfuns
           (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
     end
@@ -118,7 +118,7 @@
   fun enumerate_nats compfuns  (_ : typ) =
     let
       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
-      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
+      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
     in
       absdummy @{typ nat} (absdummy @{typ nat}
         (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 22:09:07 2011 +0100
@@ -202,6 +202,10 @@
 
 use "Tools/nat_numeral_simprocs.ML"
 
+simproc_setup nat_combine_numerals
+  ("(i::nat) + j" | "Suc (i + j)") =
+  {* fn phi => Nat_Numeral_Simprocs.combine_numerals *}
+
 simproc_setup nateq_cancel_numerals
   ("(l::nat) + m = n" | "(l::nat) = m + n" |
    "(l::nat) * m = n" | "(l::nat) = m * n" |
@@ -226,6 +230,46 @@
    "Suc m - n" | "m - Suc n") =
   {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
 
+simproc_setup nat_eq_cancel_numeral_factor
+  ("(l::nat) * m = n" | "(l::nat) = m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
+
+simproc_setup nat_less_cancel_numeral_factor
+  ("(l::nat) * m < n" | "(l::nat) < m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
+
+simproc_setup nat_le_cancel_numeral_factor
+  ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
+
+simproc_setup nat_div_cancel_numeral_factor
+  ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
+  {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
+
+simproc_setup nat_dvd_cancel_numeral_factor
+  ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
+  {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
+
+simproc_setup nat_eq_cancel_factor
+  ("(l::nat) * m = n" | "(l::nat) = m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
+
+simproc_setup nat_less_cancel_factor
+  ("(l::nat) * m < n" | "(l::nat) < m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *}
+
+simproc_setup nat_le_cancel_factor
+  ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
+
+simproc_setup nat_div_cancel_factor
+  ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
+  {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *}
+
+simproc_setup nat_dvd_cancel_factor
+  ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
+  {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
+
 declaration {* 
   K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
   #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
@@ -247,7 +291,7 @@
        @{simproc intless_cancel_numerals},
        @{simproc intle_cancel_numerals}]
   #> Lin_Arith.add_simprocs
-      [Nat_Numeral_Simprocs.combine_numerals,
+      [@{simproc nat_combine_numerals},
        @{simproc nateq_cancel_numerals},
        @{simproc natless_cancel_numerals},
        @{simproc natle_cancel_numerals},
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 22:09:07 2011 +0100
@@ -66,23 +66,23 @@
   val find_split_thm : theory -> term -> thm option
   (* datastructures and setup for generic compilation *)
   datatype compilation_funs = CompilationFuns of {
-    mk_predT : typ -> typ,
-    dest_predT : typ -> typ,
-    mk_bot : typ -> term,
+    mk_monadT : typ -> typ,
+    dest_monadT : typ -> typ,
+    mk_empty : typ -> term,
     mk_single : term -> term,
     mk_bind : term * term -> term,
-    mk_sup : term * term -> term,
+    mk_plus : term * term -> term,
     mk_if : term -> term,
     mk_iterate_upto : typ -> term * term * term -> term,
     mk_not : term -> term,
     mk_map : typ -> typ -> term -> term -> term
   };
-  val mk_predT : compilation_funs -> typ -> typ
-  val dest_predT : compilation_funs -> typ -> typ
-  val mk_bot : compilation_funs -> typ -> term
+  val mk_monadT : compilation_funs -> typ -> typ
+  val dest_monadT : compilation_funs -> typ -> typ
+  val mk_empty : compilation_funs -> typ -> term
   val mk_single : compilation_funs -> term -> term
   val mk_bind : compilation_funs -> term * term -> term
-  val mk_sup : compilation_funs -> term * term -> term
+  val mk_plus : compilation_funs -> term * term -> term
   val mk_if : compilation_funs -> term -> term
   val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term
   val mk_not : compilation_funs -> term -> term
@@ -699,24 +699,24 @@
 (* datastructures and setup for generic compilation *)
 
 datatype compilation_funs = CompilationFuns of {
-  mk_predT : typ -> typ,
-  dest_predT : typ -> typ,
-  mk_bot : typ -> term,
+  mk_monadT : typ -> typ,
+  dest_monadT : typ -> typ,
+  mk_empty : typ -> term,
   mk_single : term -> term,
   mk_bind : term * term -> term,
-  mk_sup : term * term -> term,
+  mk_plus : term * term -> term,
   mk_if : term -> term,
   mk_iterate_upto : typ -> term * term * term -> term,
   mk_not : term -> term,
   mk_map : typ -> typ -> term -> term -> term
 };
 
-fun mk_predT (CompilationFuns funs) = #mk_predT funs
-fun dest_predT (CompilationFuns funs) = #dest_predT funs
-fun mk_bot (CompilationFuns funs) = #mk_bot funs
+fun mk_monadT (CompilationFuns funs) = #mk_monadT funs
+fun dest_monadT (CompilationFuns funs) = #dest_monadT funs
+fun mk_empty (CompilationFuns funs) = #mk_empty funs
 fun mk_single (CompilationFuns funs) = #mk_single funs
 fun mk_bind (CompilationFuns funs) = #mk_bind funs
-fun mk_sup (CompilationFuns funs) = #mk_sup funs
+fun mk_plus (CompilationFuns funs) = #mk_plus funs
 fun mk_if (CompilationFuns funs) = #mk_if funs
 fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs
 fun mk_not (CompilationFuns funs) = #mk_not funs
@@ -729,7 +729,7 @@
     val Ts = binder_types T
     val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
   in
-    inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
+    inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs))
   end;
 
 (* Different options for compiler *)
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 22:09:07 2011 +0100
@@ -7,16 +7,16 @@
 structure Predicate_Comp_Funs =
 struct
 
-fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
+fun mk_monadT T = Type (@{type_name Predicate.pred}, [T])
 
-fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
-  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+fun dest_monadT (Type (@{type_name Predicate.pred}, [T])) = T
+  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
+fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T);
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
+  in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end;
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
@@ -24,42 +24,42 @@
     Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name sup};
+val mk_plus = HOLogic.mk_binop @{const_name sup};
 
 fun mk_if cond = Const (@{const_name Predicate.if_pred},
-  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
   list_comb (Const (@{const_name Code_Numeral.iterate_upto},
-      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T),
+      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T),
     [f, from, to])
 
 fun mk_not t =
   let
-    val T = mk_predT HOLogic.unitT
+    val T = mk_monadT HOLogic.unitT
   in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
 
 fun mk_Enum f =
   let val T as Type ("fun", [T', _]) = fastype_of f
   in
-    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
+    Const (@{const_name Predicate.Pred}, T --> mk_monadT T') $ f    
   end;
 
 fun mk_Eval (f, x) =
   let
-    val T = dest_predT (fastype_of f)
+    val T = dest_monadT (fastype_of f)
   in
-    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
+    Const (@{const_name Predicate.eval}, mk_monadT T --> T --> HOLogic.boolT) $ f $ x
   end;
 
 fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
 
 fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
-  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
+  (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp;
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
-    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
+    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
 end;
@@ -67,16 +67,16 @@
 structure CPS_Comp_Funs =
 struct
 
-fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
+fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
 
-fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
-  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
+  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_predT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T);
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_predT T) $ t end;
+  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end;
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
@@ -84,16 +84,16 @@
     Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
 
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
-  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
 
 fun mk_not t =
   let
-    val T = mk_predT HOLogic.unitT
+    val T = mk_monadT HOLogic.unitT
   in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
 
 fun mk_Enum f = error "not implemented"
@@ -105,8 +105,8 @@
 fun mk_map T1 T2 tf tp = error "not implemented"
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
-    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
+    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
 end;
@@ -114,16 +114,16 @@
 structure Pos_Bounded_CPS_Comp_Funs =
 struct
 
-fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
+fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
 
-fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
-  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
+  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_predT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T);
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_predT T) $ t end;
+  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end;
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
@@ -131,10 +131,10 @@
     Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
 
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
-  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
 
@@ -143,7 +143,7 @@
     val nT = @{typ "(unit Quickcheck_Exhaustive.unknown =>
       Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => code_numeral =>
       Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
-    val T = mk_predT HOLogic.unitT
+    val T = mk_monadT HOLogic.unitT
   in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
 
 fun mk_Enum f = error "not implemented"
@@ -155,8 +155,8 @@
 fun mk_map T1 T2 tf tp = error "not implemented"
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
-    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
+    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
 end;
@@ -164,21 +164,21 @@
 structure Neg_Bounded_CPS_Comp_Funs =
 struct
 
-fun mk_predT T =
+fun mk_monadT T =
   (Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T])
     --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
     --> @{typ "code_numeral => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
 
-fun dest_predT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
+fun dest_monadT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
     @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
     @{typ "code_numeral => term list Quickcheck_Exhaustive.three_valued"}])) = T
-  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_predT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T);
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_predT T) $ t end;
+  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end;
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
@@ -186,16 +186,16 @@
     Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
 
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
-  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) = error "not implemented"
 
 fun mk_not t =
   let
-    val T = mk_predT HOLogic.unitT
+    val T = mk_monadT HOLogic.unitT
     val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"}
   in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
 
@@ -208,8 +208,8 @@
 fun mk_map T1 T2 tf tp = error "not implemented"
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
-    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
+    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
 end;
@@ -219,13 +219,13 @@
 struct
 
 fun mk_randompredT T =
-  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_predT T, @{typ Random.seed})
+  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed})
 
 fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
   [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
   | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
 
-fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
+fun mk_empty T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
 
 fun mk_single t =
   let               
@@ -241,7 +241,7 @@
     Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck.union}
 
 fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
   HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
@@ -260,8 +260,8 @@
   (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_randompredT, dest_monadT = dest_randompredT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
 end;
@@ -276,7 +276,7 @@
   Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
 
-fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
+fun mk_empty T = Const (@{const_name DSequence.empty}, mk_dseqT T);
 
 fun mk_single t =
   let val T = fastype_of t
@@ -288,7 +288,7 @@
     Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
+val mk_plus = HOLogic.mk_binop @{const_name DSequence.union};
 
 fun mk_if cond = Const (@{const_name DSequence.if_seq},
   HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
@@ -302,8 +302,8 @@
   (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_dseqT, dest_monadT = dest_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
@@ -318,7 +318,7 @@
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
   | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
 
-fun mk_bot T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
+fun mk_empty T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
 
 fun mk_single t =
   let
@@ -339,7 +339,7 @@
     Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
+val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
 
 fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
   HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
@@ -358,13 +358,13 @@
   (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
@@ -379,7 +379,7 @@
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
   | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
 
-fun mk_bot T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
+fun mk_empty T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
 
 fun mk_single t =
   let
@@ -400,7 +400,7 @@
     Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
+val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
 
 fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
   HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
@@ -419,13 +419,13 @@
   (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
@@ -442,7 +442,7 @@
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
   | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
-fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+fun mk_empty T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
 
 fun mk_single t =
   let
@@ -463,7 +463,7 @@
     Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
+val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
 
 fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
   HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
@@ -487,13 +487,13 @@
   (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 end;
 
@@ -511,7 +511,7 @@
         [Type (@{type_name Option.option}, [T])])])])])])) = T
   | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
-fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+fun mk_empty T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
 
 fun mk_single t =
   let
@@ -532,7 +532,7 @@
     Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
+val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
 
 fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
   HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
@@ -554,13 +554,13 @@
   (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
@@ -577,7 +577,7 @@
   Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
   | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
-fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
 
 fun mk_single t =
   let
@@ -591,7 +591,7 @@
     Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union};
 
 fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
@@ -607,8 +607,8 @@
   (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    {mk_monadT = mk_random_dseqT, dest_monadT = dest_random_dseqT,
+    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 22:09:07 2011 +0100
@@ -312,11 +312,11 @@
     let
       val [depth] = additional_arguments
       val (_, Ts) = split_modeT mode (binder_types T)
-      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
       val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
     in
       if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
-        $ mk_bot compfuns (dest_predT compfuns T')
+        $ mk_empty compfuns (dest_monadT compfuns T')
         $ compilation
     end,
   transform_additional_arguments =
@@ -337,7 +337,7 @@
   mk_random = (fn T => fn additional_arguments =>
   list_comb (Const(@{const_name Quickcheck.iter},
   [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
-    Predicate_Comp_Funs.mk_predT T), additional_arguments)),
+    Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
   modify_funT = (fn T =>
     let
       val (Ts, U) = strip_type T
@@ -363,7 +363,7 @@
   mk_random = (fn T => fn additional_arguments =>
   list_comb (Const(@{const_name Quickcheck.iter},
   [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
-    Predicate_Comp_Funs.mk_predT T), tl additional_arguments)),
+    Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
   modify_funT = (fn T =>
     let
       val (Ts, U) = strip_type T
@@ -383,11 +383,11 @@
       val depth = hd (additional_arguments)
       val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
         mode (binder_types T)
-      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
       val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
     in
       if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
-        $ mk_bot compfuns (dest_predT compfuns T')
+        $ mk_empty compfuns (dest_monadT compfuns T')
         $ compilation
     end,
   transform_additional_arguments =
@@ -658,7 +658,7 @@
     val name' = singleton (Name.variant_list (name :: names)) "y";
     val T = HOLogic.mk_tupleT (map fastype_of out_ts);
     val U = fastype_of success_t;
-    val U' = dest_predT compfuns U;
+    val U' = dest_monadT compfuns U;
     val v = Free (name, T);
     val v' = Free (name', T);
   in
@@ -667,8 +667,8 @@
         if null eqs'' then success_t
         else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
           foldr1 HOLogic.mk_conj eqs'' $ success_t $
-            mk_bot compfuns U'),
-       (v', mk_bot compfuns U')])
+            mk_empty compfuns U'),
+       (v', mk_empty compfuns U')])
   end;
 
 fun string_of_tderiv ctxt (t, deriv) = 
@@ -928,7 +928,7 @@
               compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
                 inp (in_ts', out_ts') moded_ps'
             end
-        in SOME (foldr1 (mk_sup compfuns) (map compile_clause' moded_clauses)) end
+        in SOME (foldr1 (mk_plus compfuns) (map compile_clause' moded_clauses)) end
     | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) =
       let
         val (i, is) = argument_position_of mode position
@@ -943,18 +943,18 @@
             val args = map2 (curry Free) argnames Ts
             val pattern = list_comb (Const (c, T), args)
             val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs
-            val compilation = the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
+            val compilation = the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
               (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
         in
           (pattern, compilation)
         end
         val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
           ((map compile_single_case switched_clauses) @
-            [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))])
+            [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
       in
         case compile_switch_tree all_vs ctxt_eqs left_clauses of
           NONE => SOME switch
-        | SOME left_comp => SOME (mk_sup compfuns (switch, left_comp))
+        | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp))
       end
   in
     compile_switch_tree all_vs [] switch_tree
@@ -978,11 +978,11 @@
       (all_vs @ param_vs)
     val compfuns = Comp_Mod.compfuns compilation_modifiers
     fun is_param_type (T as Type ("fun",[_ , T'])) =
-      is_some (try (dest_predT compfuns) T) orelse is_param_type T'
-      | is_param_type T = is_some (try (dest_predT compfuns) T)
+      is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
+      | is_param_type T = is_some (try (dest_monadT compfuns) T)
     val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
       (binder_types T)
-    val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs)
+    val predT = mk_monadT compfuns (HOLogic.mk_tupleT outTs)
     val funT = Comp_Mod.funT_of compilation_modifiers mode T
     val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
       (fn T => fn (param_vs, names) =>
@@ -998,7 +998,7 @@
     val param_modes = param_vs ~~ ho_arg_modes_of mode
     val compilation =
       if detect_switches options then
-        the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
+        the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
           (compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
             in_ts' outTs (mk_switch_tree ctxt mode moded_cls))
       else
@@ -1010,9 +1010,9 @@
         in
           Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
             (if null cl_ts then
-              mk_bot compfuns (HOLogic.mk_tupleT outTs)
+              mk_empty compfuns (HOLogic.mk_tupleT outTs)
             else
-              foldr1 (mk_sup compfuns) cl_ts)
+              foldr1 (mk_plus compfuns) cl_ts)
         end
     val fun_const =
       Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
@@ -1341,7 +1341,7 @@
               (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
             val args = map2 (curry Free) arg_names Ts
             val predfun = Const (function_name_of Pred ctxt predname full_mode,
-              Ts ---> Predicate_Comp_Funs.mk_predT @{typ unit})
+              Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit})
             val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
@@ -1833,7 +1833,7 @@
         val (_, outargs) = split_mode (head_mode_of deriv) all_args
         val t_pred = compile_expr comp_modifiers ctxt
           (body, deriv) [] additional_arguments;
-        val T_pred = dest_predT compfuns (fastype_of t_pred)
+        val T_pred = dest_monadT compfuns (fastype_of t_pred)
         val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output
       in
         if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
@@ -1876,7 +1876,7 @@
       | New_Pos_Random_DSeq => []
       | Pos_Generator_DSeq => []
     val t = analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr;
-    val T = dest_predT compfuns (fastype_of t);
+    val T = dest_monadT compfuns (fastype_of t);
     val t' =
       if stats andalso compilation = New_Pos_Random_DSeq then
         mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 22:09:07 2011 +0100
@@ -186,23 +186,23 @@
   set_no_higher_order_predicate (!no_higher_order_predicate)
     (if !debug then debug_options else options)
 
-val mk_predT = Predicate_Compile_Aux.mk_predT Predicate_Comp_Funs.compfuns
+val mk_predT = Predicate_Compile_Aux.mk_monadT Predicate_Comp_Funs.compfuns
 val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns
 val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns
 
-val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
+val mk_randompredT = Predicate_Compile_Aux.mk_monadT RandomPredCompFuns.compfuns
 val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
 val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
 
 val mk_new_randompredT =
-  Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
+  Predicate_Compile_Aux.mk_monadT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
 val mk_new_return =
   Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
 val mk_new_bind =
   Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
 
 val mk_new_dseqT =
-  Predicate_Compile_Aux.mk_predT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
+  Predicate_Compile_Aux.mk_monadT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
 val mk_gen_return =
   Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
 val mk_gen_bind =
@@ -210,7 +210,7 @@
   
 
 val mk_cpsT =
-  Predicate_Compile_Aux.mk_predT Pos_Bounded_CPS_Comp_Funs.compfuns
+  Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns
 val mk_cps_return =
   Predicate_Compile_Aux.mk_single Pos_Bounded_CPS_Comp_Funs.compfuns
 val mk_cps_bind =
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/abel_cancel.ML
--- a/src/HOL/Tools/abel_cancel.ML	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Tools/abel_cancel.ML	Fri Nov 11 22:09:07 2011 +0100
@@ -24,6 +24,7 @@
       add_atoms pos x #> add_atoms (not pos) y
   | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
       add_atoms (not pos) x
+  | add_atoms pos (Const (@{const_name Groups.zero}, _)) = I
   | add_atoms pos x = cons (pos, x);
 
 fun atoms t = add_atoms true t [];
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 22:09:07 2011 +0100
@@ -5,16 +5,24 @@
 
 signature NAT_NUMERAL_SIMPROCS =
 sig
-  val combine_numerals: simproc
+  val combine_numerals: simpset -> cterm -> thm option
   val eq_cancel_numerals: simpset -> cterm -> thm option
   val less_cancel_numerals: simpset -> cterm -> thm option
   val le_cancel_numerals: simpset -> cterm -> thm option
   val diff_cancel_numerals: simpset -> cterm -> thm option
-  val cancel_factors: simproc list
-  val cancel_numeral_factors: simproc list
+  val eq_cancel_numeral_factor: simpset -> cterm -> thm option
+  val less_cancel_numeral_factor: simpset -> cterm -> thm option
+  val le_cancel_numeral_factor: simpset -> cterm -> thm option
+  val div_cancel_numeral_factor: simpset -> cterm -> thm option
+  val dvd_cancel_numeral_factor: simpset -> cterm -> thm option
+  val eq_cancel_factor: simpset -> cterm -> thm option
+  val less_cancel_factor: simpset -> cterm -> thm option
+  val le_cancel_factor: simpset -> cterm -> thm option
+  val div_cancel_factor: simpset -> cterm -> thm option
+  val dvd_cancel_factor: simpset -> cterm -> thm option
 end;
 
-structure Nat_Numeral_Simprocs =
+structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
 struct
 
 (*Maps n to #n for n = 0, 1, 2*)
@@ -232,9 +240,7 @@
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
 
-val combine_numerals =
-  Numeral_Simprocs.prep_simproc @{theory}
-    ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
+fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct)
 
 
 (*** Applying CancelNumeralFactorFun ***)
@@ -298,24 +304,11 @@
   val neg_exchanges = true
 )
 
-val cancel_numeral_factors =
-  map (Numeral_Simprocs.prep_simproc @{theory})
-   [("nateq_cancel_numeral_factors",
-     ["(l::nat) * m = n", "(l::nat) = m * n"],
-     K EqCancelNumeralFactor.proc),
-    ("natless_cancel_numeral_factors",
-     ["(l::nat) * m < n", "(l::nat) < m * n"],
-     K LessCancelNumeralFactor.proc),
-    ("natle_cancel_numeral_factors",
-     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
-     K LeCancelNumeralFactor.proc),
-    ("natdiv_cancel_numeral_factors",
-     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
-     K DivCancelNumeralFactor.proc),
-    ("natdvd_cancel_numeral_factors",
-     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
-     K DvdCancelNumeralFactor.proc)];
-
+fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
+fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
+fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
+fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
+fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct)
 
 
 (*** Applying ExtractCommonTermFun ***)
@@ -387,72 +380,10 @@
   fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
 );
 
-val cancel_factor =
-  map (Numeral_Simprocs.prep_simproc @{theory})
-   [("nat_eq_cancel_factor",
-     ["(l::nat) * m = n", "(l::nat) = m * n"],
-     K EqCancelFactor.proc),
-    ("nat_less_cancel_factor",
-     ["(l::nat) * m < n", "(l::nat) < m * n"],
-     K LessCancelFactor.proc),
-    ("nat_le_cancel_factor",
-     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
-     K LeCancelFactor.proc),
-    ("nat_divide_cancel_factor",
-     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
-     K DivideCancelFactor.proc),
-    ("nat_dvd_cancel_factor",
-     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
-     K DvdCancelFactor.proc)];
+fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
+fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
+fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
+fun div_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
+fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
 
 end;
-
-
-Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
-Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
-Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s; by (Simp_tac 1));
-
-(*combine_numerals*)
-test "k + 3*k = (u::nat)";
-test "Suc (i + 3) = u";
-test "Suc (i + j + 3 + k) = u";
-test "k + j + 3*k + j = (u::nat)";
-test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
-test "(2*n*m) + (3*(m*n)) = (u::nat)";
-(*negative numerals: FAIL*)
-test "Suc (i + j + -3 + k) = u";
-
-(*cancel_numeral_factors*)
-test "9*x = 12 * (y::nat)";
-test "(9*x) div (12 * (y::nat)) = z";
-test "9*x < 12 * (y::nat)";
-test "9*x <= 12 * (y::nat)";
-
-(*cancel_factor*)
-test "x*k = k*(y::nat)";
-test "k = k*(y::nat)";
-test "a*(b*c) = (b::nat)";
-test "a*(b*c) = d*(b::nat)*(x*a)";
-
-test "x*k < k*(y::nat)";
-test "k < k*(y::nat)";
-test "a*(b*c) < (b::nat)";
-test "a*(b*c) < d*(b::nat)*(x*a)";
-
-test "x*k <= k*(y::nat)";
-test "k <= k*(y::nat)";
-test "a*(b*c) <= (b::nat)";
-test "a*(b*c) <= d*(b::nat)*(x*a)";
-
-test "(x*k) div (k*(y::nat)) = (uu::nat)";
-test "(k) div (k*(y::nat)) = (uu::nat)";
-test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
-test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
-*)
diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 22:05:18 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 22:09:07 2011 +0100
@@ -5,7 +5,7 @@
 header {* Testing of arithmetic simprocs *}
 
 theory Simproc_Tests
-imports Rat
+imports Main
 begin
 
 text {*
@@ -21,12 +21,33 @@
   fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
 *}
 
+subsection {* Abelian group cancellation simprocs *}
+
+notepad begin
+  fix a b c u :: "'a::ab_group_add"
+  {
+    assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
+      by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact
+  next
+    assume "a + 0 = b + 0" have "a + c = b + c"
+      by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact
+  }
+end
+(* TODO: more tests for Groups.abel_cancel_{sum,relation} *)
 
 subsection {* @{text int_combine_numerals} *}
 
+(* FIXME: int_combine_numerals often unnecessarily regroups addition
+and rewrites subtraction to negation. Ideally it should behave more
+like Groups.abel_cancel_sum, preserving the shape of terms as much as
+possible. *)
+
 notepad begin
   fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring"
   {
+    assume "a + - b = u" have "(a + c) - (b + c) = u"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
     assume "10 + (2 * l + oo) = uu"
     have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
@@ -324,10 +345,11 @@
   }
 end
 
-lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
+lemma
+  fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
+  shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
 oops -- "FIXME: need simproc to cover this case"
 
-
 subsection {* @{text linordered_ring_less_cancel_factor} *}
 
 notepad begin
@@ -384,16 +406,49 @@
   }
 end
 
-lemma "2/3 * (x::rat) + x / 3 = uu"
+lemma
+  fixes x :: "'a::{linordered_field_inverse_zero,number_ring}"
+  shows "2/3 * x + x / 3 = uu"
 apply (tactic {* test [@{simproc field_combine_numerals}] *})?
 oops -- "FIXME: test fails"
 
+subsection {* @{text nat_combine_numerals} *}
+
+notepad begin
+  fix i j k m n u :: nat
+  {
+    assume "4*k = u" have "k + 3*k = u"
+      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
+  next
+    assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
+      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
+  next
+    assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
+      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
+  next
+    assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u"
+      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
+  next
+    assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u"
+    have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u"
+      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
+  next
+    assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u"
+      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
+  }
+end
+
+(*negative numerals: FAIL*)
+lemma "Suc (i + j + -3 + k) = u"
+apply (tactic {* test [@{simproc nat_combine_numerals}] *})?
+oops
+
 subsection {* @{text nateq_cancel_numerals} *}
 
 notepad begin
   fix i j k l oo u uu vv w y z w' y' z' :: "nat"
   {
-    assume "Suc 0 * u = 0" have "2*u = (u::nat)"
+    assume "Suc 0 * u = 0" have "2*u = u"
       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
   next
     assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
@@ -560,4 +615,101 @@
   }
 end
 
+subsection {* Factor-cancellation simprocs for type @{typ nat} *}
+
+text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
+@{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
+@{text nat_dvd_cancel_factor}. *}
+
+notepad begin
+  fix a b c d k x y uu :: nat
+  {
+    assume "k = 0 \<or> x = y" have "x*k = k*y"
+      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+  next
+    assume "k = 0 \<or> Suc 0 = y" have "k = k*y"
+      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+  next
+    assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b"
+      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+  next
+    assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)"
+      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
+  next
+    assume "0 < k \<and> x < y" have "x*k < k*y"
+      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+  next
+    assume "0 < k \<and> Suc 0 < y" have "k < k*y"
+      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+  next
+    assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b"
+      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+  next
+    assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)"
+      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
+  next
+    assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y"
+      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
+  next
+    assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y"
+      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
+  next
+    assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b"
+      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
+  next
+    assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)"
+      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
+  next
+    assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
+  next
+    assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
+  next
+    assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
+  next
+    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
+    have "(a*(b*c)) div (d*b*(x*a)) = uu"
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
+  next
+    assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
+      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+  next
+    assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"
+      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+  next
+    assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)"
+      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+  next
+    assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))"
+      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+  next
+    assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"
+      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
+  }
 end
+
+subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
+
+notepad begin
+  fix x y z :: nat
+  {
+    assume "3 * x = 4 * y" have "9*x = 12 * y"
+      by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
+  next
+    assume "3 * x < 4 * y" have "9*x < 12 * y"
+      by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
+  next
+    assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
+      by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
+      by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
+  next
+    assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
+      by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
+  }
+end
+
+end