--- a/src/HOL/Quickcheck.thy Mon Jun 08 08:38:50 2009 +0200
+++ b/src/HOL/Quickcheck.thy Mon Jun 08 08:38:51 2009 +0200
@@ -40,6 +40,26 @@
end
+instantiation char :: random
+begin
+
+definition
+ "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Eval.term_of c))"
+
+instance ..
+
+end
+
+instantiation String.literal :: random
+begin
+
+definition
+ "random _ = Pair (STR [], \<lambda>u. Code_Eval.term_of (STR []))"
+
+instance ..
+
+end
+
instantiation nat :: random
begin
@@ -77,6 +97,13 @@
"beyond k 0 = 0"
by (simp add: beyond_def)
+lemma random_aux_rec:
+ fixes random_aux :: "code_numeral \<Rightarrow> 'a"
+ assumes "random_aux 0 = rhs 0"
+ and "\<And>k. random_aux (Suc_code_numeral k) = rhs (Suc_code_numeral k)"
+ shows "random_aux k = rhs k"
+ using assms by (rule code_numeral.induct)
+
use "Tools/quickcheck_generators.ML"
setup {* Quickcheck_Generators.setup *}
--- a/src/HOL/ex/Quickcheck_Generators.thy Mon Jun 08 08:38:50 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy Mon Jun 08 08:38:51 2009 +0200
@@ -136,6 +136,8 @@
("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
fun add_random_inst [@{type_name bool}] thy = thy
| add_random_inst [@{type_name nat}] thy = thy
+ | add_random_inst [@{type_name char}] thy = thy
+ | add_random_inst [@{type_name String.literal}] thy = thy
| add_random_inst tycos thy = random_inst tycos thy
handle REC msg => (warning msg; thy)
| TYP msg => (warning msg; thy)