# HG changeset patch
# User haftmann
# Date 1244992819 -7200
# Node ID ea47e2b635887c547bbb38354807bbc7503ad8be
# Parent  40d77573384820c40e51a3f0f9ba2e4851791f4b
dropped select_default

diff -r 40d775733848 -r ea47e2b63588 src/HOL/Library/Fin_Fun.thy
--- a/src/HOL/Library/Fin_Fun.thy	Sun Jun 14 09:13:59 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy	Sun Jun 14 17:20:19 2009 +0200
@@ -76,10 +76,13 @@
 subsection {* The finfun type *}
 
 typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
-apply(auto)
-apply(rule_tac x="\<lambda>x. arbitrary" in exI)
-apply(auto)
-done
+proof -
+  have "\<exists>f. finite {x. f x \<noteq> undefined}"
+  proof
+    show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
+  qed
+  then show ?thesis by auto
+qed
 
 syntax
   "finfun"      :: "type \<Rightarrow> type \<Rightarrow> type"         ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21)
@@ -318,32 +321,27 @@
 instantiation finfun :: (random, random) random
 begin
 
-primrec random_finfun' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
-    "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0
-       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))
-       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
-  | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i
-       (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
-       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
-                         
+primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+    "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
+       [(1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+  | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight
+       [(Suc_code_numeral i, random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+         (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+
 definition 
-  "random i = random_finfun' i i"
+  "random i = random_finfun_aux i i"
 
 instance ..
 
 end
 
-lemma select_default_zero:
-  "Random.select_default 0 y y = Random.select_default 0 x y"
-  by (simp add: select_default_def)
-
-lemma random_finfun'_code [code]:
-  "random_finfun' i j = Quickcheck.collapse (Random.select_default (i - 1)
-    (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
-    (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
+lemma random_finfun_aux_code [code]:
+  "random_finfun_aux i j = Quickcheck.collapse (Random.select_weight
+     [(i, random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+       (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
   apply (cases i rule: code_numeral.exhaust)
-  apply (simp_all only: random_finfun'.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
-  apply (subst select_default_zero) apply (simp only:)
+  apply (simp_all only: random_finfun_aux.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
+  apply (subst select_weight_cons_zero) apply (simp only:)
   done
 
 no_notation fcomp (infixl "o>" 60)
diff -r 40d775733848 -r ea47e2b63588 src/HOL/Random.thy
--- 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 *}