merged

--- a/src/HOL/Code_Numeral.thy	Wed May 27 21:08:47 2009 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed May 27 22:20:29 2009 +0200
@@ -215,7 +215,13 @@
   "of_nat n < of_nat m \<longleftrightarrow> n < m"
   by simp
 
-lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
+lemma code_numeral_zero_minus_one:
+  "(0::code_numeral) - 1 = 0"
+  by simp
+
+lemma Suc_code_numeral_minus_one:
+  "Suc_code_numeral n - 1 = n"
+  by simp
 
 lemma of_nat_code [code]:
   "of_nat = Nat.of_nat"

--- a/src/HOL/Quickcheck.thy	Wed May 27 21:08:47 2009 +0200
+++ b/src/HOL/Quickcheck.thy	Wed May 27 22:20:29 2009 +0200
@@ -73,6 +73,10 @@
 definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   "beyond k l = (if l > k then l else 0)"
 
+lemma beyond_zero:
+  "beyond k 0 = 0"
+  by (simp add: beyond_def)
+
 use "Tools/quickcheck_generators.ML"
 setup {* Quickcheck_Generators.setup *}
 
@@ -100,6 +104,8 @@
 end
 
 
+hide (open) const collapse beyond
+
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)
 

--- a/src/HOL/Random.thy	Wed May 27 21:08:47 2009 +0200
+++ b/src/HOL/Random.thy	Wed May 27 22:20:29 2009 +0200
@@ -118,6 +118,10 @@
   then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
 qed
 
+lemma select_weight_cons_zero:
+  "select_weight ((0, x) # xs) = select_weight xs"
+  by (simp add: select_weight_def)
+
 lemma select_weigth_drop_zero:
   "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
 proof -

--- a/src/HOL/Tools/primrec_package.ML	Wed May 27 21:08:47 2009 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed May 27 22:20:29 2009 +0200
@@ -16,7 +16,7 @@
   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> thm list * theory
-  val add_primrec_simple: ((binding * typ) * mixfix) list -> (binding * term) list ->
+  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string * thm list list) * local_theory
 end;
 
@@ -252,9 +252,9 @@
 
 (* primrec definition *)
 
-fun add_primrec_simple fixes spec lthy =
+fun add_primrec_simple fixes ts lthy =
   let
-    val ((prefix, (fs, defs)), prove) = distill lthy fixes (map snd spec);
+    val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   in
     lthy
     |> fold_map (LocalTheory.define Thm.definitionK) defs
@@ -274,7 +274,7 @@
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
-    |> add_primrec_simple fixes spec
+    |> add_primrec_simple fixes (map snd spec)
     |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
           (attr_bindings prefix ~~ simps)
     #-> (fn simps' => LocalTheory.note Thm.generatedK