# HG changeset patch
# User haftmann
# Date 1244443131 -7200
# Node ID 88210717bfc8de52d9e2a29bcb5781fcf3a8bd44
# Parent  7288382fd5499d00d6b6fce5e6ea0bb948c7ac22
added generator for char and trivial generator for String.literal

diff -r 7288382fd549 -r 88210717bfc8 src/HOL/Quickcheck.thy
--- 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 *}
 
diff -r 7288382fd549 -r 88210717bfc8 src/HOL/ex/Quickcheck_Generators.thy
--- 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)