1.1 --- a/src/HOL/Quickcheck.thy Mon May 18 15:45:36 2009 +0200
1.2 +++ b/src/HOL/Quickcheck.thy Mon May 18 15:45:38 2009 +0200
1.3 @@ -70,27 +70,22 @@
1.4
1.5 subsection {* Fundamental types*}
1.6
1.7 -definition (in term_syntax)
1.8 - "termify_bool b = (if b then termify True else termify False)"
1.9 -
1.10 instantiation bool :: random
1.11 begin
1.12
1.13 definition
1.14 - "random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))"
1.15 + "random i = Random.range i o\<rightarrow>
1.16 + (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
1.17
1.18 instance ..
1.19
1.20 end
1.21
1.22 -definition (in term_syntax)
1.23 - "termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)"
1.24 -
1.25 instantiation itself :: (typerep) random
1.26 begin
1.27
1.28 definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
1.29 - "random_itself _ = Pair (termify_itself TYPE('a))"
1.30 + "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
1.31
1.32 instance ..
1.33
1.34 @@ -156,70 +151,55 @@
1.35
1.36 subsection {* Numeric types *}
1.37
1.38 -function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
1.39 - "termify_numeral k = (if k = 0 then termify Int.Pls
1.40 - else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))"
1.41 - by pat_completeness auto
1.42 -
1.43 -declare (in term_syntax) termify_numeral.psimps [simp del]
1.44 -
1.45 -termination termify_numeral by (relation "measure Code_Index.nat_of")
1.46 - (simp_all add: index)
1.47 -
1.48 -definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
1.49 - "termify_int_number k = termify number_of <\<cdot>> termify_numeral k"
1.50 -
1.51 -definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where
1.52 - "termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k"
1.53 -
1.54 -declare termify_nat_number_def [simplified snd_conv, code]
1.55 -
1.56 instantiation nat :: random
1.57 begin
1.58
1.59 -definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
1.60 - "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))"
1.61 +definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
1.62 + "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
1.63 + let n = Code_Index.nat_of k
1.64 + in (n, \<lambda>_. Code_Eval.term_of n)))"
1.65
1.66 instance ..
1.67
1.68 end
1.69
1.70 -definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
1.71 - [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
1.72 -
1.73 instantiation int :: random
1.74 begin
1.75
1.76 definition
1.77 - "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
1.78 - then let j = k - i in termify_int_number j
1.79 - else let j = i - k in term_uminus (termify_int_number j)))"
1.80 + "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
1.81 + let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
1.82 + in (j, \<lambda>_. Code_Eval.term_of j)))"
1.83
1.84 instance ..
1.85
1.86 end
1.87
1.88 -definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where
1.89 - [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
1.90 +definition (in term_syntax)
1.91 + valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
1.92 + [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
1.93
1.94 instantiation rat :: random
1.95 begin
1.96
1.97 definition
1.98 - "random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))"
1.99 + "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
1.100 + let j = Code_Index.int_of (denom + 1)
1.101 + in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
1.102
1.103 instance ..
1.104
1.105 end
1.106
1.107 -definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
1.108 - [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
1.109 +definition (in term_syntax)
1.110 + valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
1.111 + [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
1.112
1.113 instantiation real :: random
1.114 begin
1.115
1.116 definition
1.117 - "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
1.118 + "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
1.119
1.120 instance ..
1.121