1.1 --- a/src/HOL/Library/Fin_Fun.thy	Sun Jun 14 09:13:59 2009 +0200
     1.2 +++ b/src/HOL/Library/Fin_Fun.thy	Sun Jun 14 17:20:19 2009 +0200
     1.3 @@ -76,10 +76,13 @@
     1.4  subsection {* The finfun type *}
     1.5  
     1.6  typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
     1.7 -apply(auto)
     1.8 -apply(rule_tac x="\<lambda>x. arbitrary" in exI)
     1.9 -apply(auto)
    1.10 -done
    1.11 +proof -
    1.12 +  have "\<exists>f. finite {x. f x \<noteq> undefined}"
    1.13 +  proof
    1.14 +    show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
    1.15 +  qed
    1.16 +  then show ?thesis by auto
    1.17 +qed
    1.18  
    1.19  syntax
    1.20    "finfun"      :: "type \<Rightarrow> type \<Rightarrow> type"         ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21)
    1.21 @@ -318,32 +321,27 @@
    1.22  instantiation finfun :: (random, random) random
    1.23  begin
    1.24  
    1.25 -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
    1.26 -    "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0
    1.27 -       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))
    1.28 -       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
    1.29 -  | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i
    1.30 -       (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)))))
    1.31 -       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
    1.32 -                         
    1.33 +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
    1.34 +    "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
    1.35 +       [(1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
    1.36 +  | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight
    1.37 +       [(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.38 +         (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
    1.39 +
    1.40  definition 
    1.41 -  "random i = random_finfun' i i"
    1.42 +  "random i = random_finfun_aux i i"
    1.43  
    1.44  instance ..
    1.45  
    1.46  end
    1.47  
    1.48 -lemma select_default_zero:
    1.49 -  "Random.select_default 0 y y = Random.select_default 0 x y"
    1.50 -  by (simp add: select_default_def)
    1.51 -
    1.52 -lemma random_finfun'_code [code]:
    1.53 -  "random_finfun' i j = Quickcheck.collapse (Random.select_default (i - 1)
    1.54 -    (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)))))
    1.55 -    (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
    1.56 +lemma random_finfun_aux_code [code]:
    1.57 +  "random_finfun_aux i j = Quickcheck.collapse (Random.select_weight
    1.58 +     [(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.59 +       (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
    1.60    apply (cases i rule: code_numeral.exhaust)
    1.61 -  apply (simp_all only: random_finfun'.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
    1.62 -  apply (subst select_default_zero) apply (simp only:)
    1.63 +  apply (simp_all only: random_finfun_aux.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
    1.64 +  apply (subst select_weight_cons_zero) apply (simp only:)
    1.65    done
    1.66  
    1.67  no_notation fcomp (infixl "o>" 60)

     2.1 --- a/src/HOL/Random.thy	Sun Jun 14 09:13:59 2009 +0200
     2.2 +++ b/src/HOL/Random.thy	Sun Jun 14 17:20:19 2009 +0200
     2.3 @@ -143,28 +143,6 @@
     2.4        expand_fun_eq pick_same [symmetric])
     2.5  qed
     2.6  
     2.7 -definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
     2.8 -  [code del]: "select_default k x y = range k
     2.9 -     o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
    2.10 -
    2.11 -lemma select_default_zero:
    2.12 -  "fst (select_default 0 x y s) = y"
    2.13 -  by (simp add: scomp_apply split_beta select_default_def)
    2.14 -
    2.15 -lemma select_default_code [code]:
    2.16 -  "select_default k x y = (if k = 0
    2.17 -    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
    2.18 -    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
    2.19 -proof
    2.20 -  fix s
    2.21 -  have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
    2.22 -    by (simp add: range_def scomp_Pair scomp_apply split_beta)
    2.23 -  then show "select_default k x y s = (if k = 0
    2.24 -    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
    2.25 -    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
    2.26 -    by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
    2.27 -qed
    2.28 -
    2.29  
    2.30  subsection {* @{text ML} interface *}
    2.31