src/HOL/Quickcheck.thy
changeset 31194 1d6926f96440
parent 31186 b458b4ac570f
child 31203 5c8fb4fd67e0
     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 +instantiation int :: random
    1.71 +begin
    1.72 +
    1.73 +definition
    1.74 +  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
    1.75 +     let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
    1.76 +     in (j, \<lambda>_. Code_Eval.term_of j)))"
    1.77  
    1.78  instance ..
    1.79  
    1.80  end
    1.81  
    1.82 -definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
    1.83 -  [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
    1.84 +definition (in term_syntax)
    1.85 +  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.86 +  [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
    1.87  
    1.88 -instantiation int :: random
    1.89 +instantiation rat :: random
    1.90  begin
    1.91  
    1.92  definition
    1.93 -  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
    1.94 -     then let j = k - i in termify_int_number j
    1.95 -     else let j = i - k in term_uminus (termify_int_number j)))"
    1.96 +  "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
    1.97 +     let j = Code_Index.int_of (denom + 1)
    1.98 +     in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
    1.99  
   1.100  instance ..
   1.101  
   1.102  end
   1.103  
   1.104 -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.105 -  [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
   1.106 -
   1.107 -instantiation rat :: random
   1.108 -begin
   1.109 -
   1.110 -definition
   1.111 -  "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.112 -
   1.113 -instance ..
   1.114 -
   1.115 -end
   1.116 -
   1.117 -definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
   1.118 -  [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
   1.119 +definition (in term_syntax)
   1.120 +  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
   1.121 +  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   1.122  
   1.123  instantiation real :: random
   1.124  begin
   1.125  
   1.126  definition
   1.127 -  "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
   1.128 +  "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
   1.129  
   1.130  instance ..
   1.131