src/HOL/Quickcheck.thy
changeset 31483 88210717bfc8
parent 31267 4a85a4afc97d
child 31603 fa30cd74d7d6
     1.1 --- a/src/HOL/Quickcheck.thy	Mon Jun 08 08:38:50 2009 +0200
     1.2 +++ b/src/HOL/Quickcheck.thy	Mon Jun 08 08:38:51 2009 +0200
     1.3 @@ -40,6 +40,26 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation char :: random
     1.8 +begin
     1.9 +
    1.10 +definition
    1.11 +  "random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Eval.term_of c))"
    1.12 +
    1.13 +instance ..
    1.14 +
    1.15 +end
    1.16 +
    1.17 +instantiation String.literal :: random
    1.18 +begin
    1.19 +
    1.20 +definition 
    1.21 +  "random _ = Pair (STR [], \<lambda>u. Code_Eval.term_of (STR []))"
    1.22 +
    1.23 +instance ..
    1.24 +
    1.25 +end
    1.26 +
    1.27  instantiation nat :: random
    1.28  begin
    1.29  
    1.30 @@ -77,6 +97,13 @@
    1.31    "beyond k 0 = 0"
    1.32    by (simp add: beyond_def)
    1.33  
    1.34 +lemma random_aux_rec:
    1.35 +  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
    1.36 +  assumes "random_aux 0 = rhs 0"
    1.37 +    and "\<And>k. random_aux (Suc_code_numeral k) = rhs (Suc_code_numeral k)"
    1.38 +  shows "random_aux k = rhs k"
    1.39 +  using assms by (rule code_numeral.induct)
    1.40 +
    1.41  use "Tools/quickcheck_generators.ML"
    1.42  setup {* Quickcheck_Generators.setup *}
    1.43