# 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\'b. \b. finite {a. f a \ b}}" -apply(auto) -apply(rule_tac x="\x. arbitrary" in exI) -apply(auto) -done +proof - + have "\f. finite {x. f x \ undefined}" + proof + show "finite {x. (\y. undefined) x \ undefined}" by auto + qed + then show ?thesis by auto +qed syntax "finfun" :: "type \ type \ type" ("(_ \\<^isub>f /_)" [22, 21] 21) @@ -318,32 +321,27 @@ instantiation finfun :: (random, random) random begin -primrec random_finfun' :: "code_numeral \ code_numeral \ Random.seed \ ('a \\<^isub>f 'b \ (unit \ Code_Eval.term)) \ Random.seed" where - "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0 - (random j o\ (\y. Pair (valtermify_finfun_const y))) - (random j o\ (\y. Pair (valtermify_finfun_const y))))" - | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i - (random j o\ (\x. random j o\ (\y. random_finfun' i j o\ (\f. Pair (valtermify_finfun_update_code x y f))))) - (random j o\ (\y. Pair (valtermify_finfun_const y))))" - +primrec random_finfun_aux :: "code_numeral \ code_numeral \ Random.seed \ ('a \\<^isub>f 'b \ (unit \ Code_Eval.term)) \ Random.seed" where + "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight + [(1, random j o\ (\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\ (\x. random j o\ (\y. random_finfun_aux i j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), + (1, random j o\ (\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\ (\x. random j o\ (\y. random_finfun' (i - 1) j o\ (\f. Pair (valtermify_finfun_update_code x y f))))) - (random j o\ (\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\ (\x. random j o\ (\y. random_finfun_aux (i - 1) j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), + (1, random j o\ (\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 \ 'a \ 'a \ seed \ 'a \ seed" where - [code del]: "select_default k x y = range k - o\ (\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\ (\_. Pair y) - else range k o\ (\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\ (\_. Pair y) - else range k o\ (\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 *}