random instance for sets
authorbulwahn
Mon Jan 23 14:00:52 2012 +0100 (2012-01-23)
changeset 4631156fae81902ce
parent 46310 8af202923906
child 46312 518cc38a1a8c
random instance for sets
src/HOL/Quickcheck.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Random.thy
     1.1 --- a/src/HOL/Quickcheck.thy	Mon Jan 23 11:59:00 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Mon Jan 23 14:00:52 2012 +0100
     1.3 @@ -129,6 +129,38 @@
     1.4    "beyond k 0 = 0"
     1.5    by (simp add: beyond_def)
     1.6  
     1.7 +
     1.8 +definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
     1.9 +definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
    1.10 +
    1.11 +instantiation set :: (random) random
    1.12 +begin
    1.13 +
    1.14 +primrec random_aux_set
    1.15 +where
    1.16 +  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
    1.17 +| "random_aux_set (Suc_code_numeral i) j = collapse (Random.select_weight [(1, Pair valterm_emptyset), (Suc_code_numeral i, random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
    1.18 +
    1.19 +lemma [code]:
    1.20 +  "random_aux_set i j = collapse (Random.select_weight [(1, Pair valterm_emptyset), (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
    1.21 +proof (induct i rule: code_numeral.induct)
    1.22 +print_cases
    1.23 +  case zero
    1.24 +  show ?case by (subst select_weight_drop_zero[symmetric])
    1.25 +    (simp add: filter.simps random_aux_set.simps[simplified])
    1.26 +next
    1.27 +  case (Suc_code_numeral i)
    1.28 +  show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
    1.29 +qed
    1.30 +
    1.31 +definition random_set
    1.32 +where
    1.33 +  "random_set i = random_aux_set i i" 
    1.34 +
    1.35 +instance ..
    1.36 +
    1.37 +end
    1.38 +
    1.39  lemma random_aux_rec:
    1.40    fixes random_aux :: "code_numeral \<Rightarrow> 'a"
    1.41    assumes "random_aux 0 = rhs 0"
     2.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Jan 23 11:59:00 2012 +0100
     2.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Jan 23 14:00:52 2012 +0100
     2.3 @@ -142,9 +142,6 @@
     2.4  
     2.5  end
     2.6  
     2.7 -definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
     2.8 -definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
     2.9 -
    2.10  instantiation set :: (full_exhaustive) full_exhaustive
    2.11  begin
    2.12  
     3.1 --- a/src/HOL/Random.thy	Mon Jan 23 11:59:00 2012 +0100
     3.2 +++ b/src/HOL/Random.thy	Mon Jan 23 14:00:52 2012 +0100
     3.3 @@ -114,7 +114,7 @@
     3.4    "select_weight ((0, x) # xs) = select_weight xs"
     3.5    by (simp add: select_weight_def)
     3.6  
     3.7 -lemma select_weigth_drop_zero:
     3.8 +lemma select_weight_drop_zero:
     3.9    "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
    3.10  proof -
    3.11    have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
    3.12 @@ -122,7 +122,7 @@
    3.13    then show ?thesis by (simp only: select_weight_def pick_drop_zero)
    3.14  qed
    3.15  
    3.16 -lemma select_weigth_select:
    3.17 +lemma select_weight_select:
    3.18    assumes "xs \<noteq> []"
    3.19    shows "select_weight (map (Pair 1) xs) = select xs"
    3.20  proof -