src/HOL/Random.thy
changeset 31633 ea47e2b63588
parent 31268 3ced22320ceb
child 31636 138625ae4067
--- a/src/HOL/Random.thy	Sun Jun 14 09:13:59 2009 +0200
+++ b/src/HOL/Random.thy	Sun Jun 14 17:20:19 2009 +0200
@@ -143,28 +143,6 @@
       expand_fun_eq pick_same [symmetric])
 qed
 
-definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
-  [code del]: "select_default k x y = range k
-     o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
-
-lemma select_default_zero:
-  "fst (select_default 0 x y s) = y"
-  by (simp add: scomp_apply split_beta select_default_def)
-
-lemma select_default_code [code]:
-  "select_default k x y = (if k = 0
-    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
-    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
-proof
-  fix s
-  have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
-    by (simp add: range_def scomp_Pair scomp_apply split_beta)
-  then show "select_default k x y s = (if k = 0
-    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
-    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
-    by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
-qed
-
 
 subsection {* @{text ML} interface *}