# HG changeset patch # User wenzelm # Date 1243455629 -7200 # Node ID 40c00d6848002d3bd122232cb51a79ed894a9f7d # Parent dcbe1f9fe2cd460de463cb27ee684e57eec11fea# Parent 18085db7b1476aceff33583b92ac0b313d949c03 merged diff -r 18085db7b147 -r 40c00d684800 src/HOL/Code_Numeral.thy --- 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 \ 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" diff -r 18085db7b147 -r 40c00d684800 src/HOL/Quickcheck.thy --- 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 \ code_numeral \ 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\" 60) diff -r 18085db7b147 -r 40c00d684800 src/HOL/Random.thy --- 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 (\(k, _). k > 0) xs) = select_weight xs" proof - diff -r 18085db7b147 -r 40c00d684800 src/HOL/Tools/primrec_package.ML --- 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