# HG changeset patch
# User bulwahn
# Date 1327323652 -3600
# Node ID 56fae81902ce254baec7f7b39e3727e20c66274a
# Parent  8af202923906d486c946c7d3aeadc5e4e83f49bd
random instance for sets

diff -r 8af202923906 -r 56fae81902ce src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Mon Jan 23 11:59:00 2012 +0100
+++ b/src/HOL/Quickcheck.thy	Mon Jan 23 14:00:52 2012 +0100
@@ -129,6 +129,38 @@
   "beyond k 0 = 0"
   by (simp add: beyond_def)
 
+
+definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
+definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+
+instantiation set :: (random) random
+begin
+
+primrec random_aux_set
+where
+  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
+| "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))))])"
+
+lemma [code]:
+  "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))))])"
+proof (induct i rule: code_numeral.induct)
+print_cases
+  case zero
+  show ?case by (subst select_weight_drop_zero[symmetric])
+    (simp add: filter.simps random_aux_set.simps[simplified])
+next
+  case (Suc_code_numeral i)
+  show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
+qed
+
+definition random_set
+where
+  "random_set i = random_aux_set i i" 
+
+instance ..
+
+end
+
 lemma random_aux_rec:
   fixes random_aux :: "code_numeral \<Rightarrow> 'a"
   assumes "random_aux 0 = rhs 0"
diff -r 8af202923906 -r 56fae81902ce src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Jan 23 11:59:00 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Jan 23 14:00:52 2012 +0100
@@ -142,9 +142,6 @@
 
 end
 
-definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
-definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
-
 instantiation set :: (full_exhaustive) full_exhaustive
 begin
 
diff -r 8af202923906 -r 56fae81902ce src/HOL/Random.thy
--- a/src/HOL/Random.thy	Mon Jan 23 11:59:00 2012 +0100
+++ b/src/HOL/Random.thy	Mon Jan 23 14:00:52 2012 +0100
@@ -114,7 +114,7 @@
   "select_weight ((0, x) # xs) = select_weight xs"
   by (simp add: select_weight_def)
 
-lemma select_weigth_drop_zero:
+lemma select_weight_drop_zero:
   "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
 proof -
   have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
@@ -122,7 +122,7 @@
   then show ?thesis by (simp only: select_weight_def pick_drop_zero)
 qed
 
-lemma select_weigth_select:
+lemma select_weight_select:
   assumes "xs \<noteq> []"
   shows "select_weight (map (Pair 1) xs) = select xs"
 proof -