experimental move of Quickcheck and related theories to HOL image
authorhaftmann
Sat May 16 20:16:49 2009 +0200 (2009-05-16)
changeset 31186b458b4ac570f
parent 31185 cd29afc027cc
child 31188 e5d01f8a916d
experimental move of Quickcheck and related theories to HOL image
src/HOL/Code_Index.thy
src/HOL/Complex_Main.thy
src/HOL/IsaMakefile
src/HOL/Library/Code_Index.thy
src/HOL/Library/Library.thy
src/HOL/Library/Quickcheck.thy
src/HOL/Library/Random.thy
src/HOL/Quickcheck.thy
src/HOL/Random.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Code_Index.thy	Sat May 16 20:16:49 2009 +0200
     1.3 @@ -0,0 +1,336 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header {* Type of indices *}
     1.7 +
     1.8 +theory Code_Index
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +text {*
    1.13 +  Indices are isomorphic to HOL @{typ nat} but
    1.14 +  mapped to target-language builtin integers.
    1.15 +*}
    1.16 +
    1.17 +subsection {* Datatype of indices *}
    1.18 +
    1.19 +typedef (open) index = "UNIV \<Colon> nat set"
    1.20 +  morphisms nat_of of_nat by rule
    1.21 +
    1.22 +lemma of_nat_nat_of [simp]:
    1.23 +  "of_nat (nat_of k) = k"
    1.24 +  by (rule nat_of_inverse)
    1.25 +
    1.26 +lemma nat_of_of_nat [simp]:
    1.27 +  "nat_of (of_nat n) = n"
    1.28 +  by (rule of_nat_inverse) (rule UNIV_I)
    1.29 +
    1.30 +lemma [measure_function]:
    1.31 +  "is_measure nat_of" by (rule is_measure_trivial)
    1.32 +
    1.33 +lemma index:
    1.34 +  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
    1.35 +proof
    1.36 +  fix n :: nat
    1.37 +  assume "\<And>n\<Colon>index. PROP P n"
    1.38 +  then show "PROP P (of_nat n)" .
    1.39 +next
    1.40 +  fix n :: index
    1.41 +  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
    1.42 +  then have "PROP P (of_nat (nat_of n))" .
    1.43 +  then show "PROP P n" by simp
    1.44 +qed
    1.45 +
    1.46 +lemma index_case:
    1.47 +  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
    1.48 +  shows P
    1.49 +  by (rule assms [of "nat_of k"]) simp
    1.50 +
    1.51 +lemma index_induct_raw:
    1.52 +  assumes "\<And>n. P (of_nat n)"
    1.53 +  shows "P k"
    1.54 +proof -
    1.55 +  from assms have "P (of_nat (nat_of k))" .
    1.56 +  then show ?thesis by simp
    1.57 +qed
    1.58 +
    1.59 +lemma nat_of_inject [simp]:
    1.60 +  "nat_of k = nat_of l \<longleftrightarrow> k = l"
    1.61 +  by (rule nat_of_inject)
    1.62 +
    1.63 +lemma of_nat_inject [simp]:
    1.64 +  "of_nat n = of_nat m \<longleftrightarrow> n = m"
    1.65 +  by (rule of_nat_inject) (rule UNIV_I)+
    1.66 +
    1.67 +instantiation index :: zero
    1.68 +begin
    1.69 +
    1.70 +definition [simp, code del]:
    1.71 +  "0 = of_nat 0"
    1.72 +
    1.73 +instance ..
    1.74 +
    1.75 +end
    1.76 +
    1.77 +definition [simp]:
    1.78 +  "Suc_index k = of_nat (Suc (nat_of k))"
    1.79 +
    1.80 +rep_datatype "0 \<Colon> index" Suc_index
    1.81 +proof -
    1.82 +  fix P :: "index \<Rightarrow> bool"
    1.83 +  fix k :: index
    1.84 +  assume "P 0" then have init: "P (of_nat 0)" by simp
    1.85 +  assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
    1.86 +    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
    1.87 +    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
    1.88 +  from init step have "P (of_nat (nat_of k))"
    1.89 +    by (induct "nat_of k") simp_all
    1.90 +  then show "P k" by simp
    1.91 +qed simp_all
    1.92 +
    1.93 +declare index_case [case_names nat, cases type: index]
    1.94 +declare index.induct [case_names nat, induct type: index]
    1.95 +
    1.96 +lemma index_decr [termination_simp]:
    1.97 +  "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
    1.98 +  by (cases k) simp
    1.99 +
   1.100 +lemma [simp, code]:
   1.101 +  "index_size = nat_of"
   1.102 +proof (rule ext)
   1.103 +  fix k
   1.104 +  have "index_size k = nat_size (nat_of k)"
   1.105 +    by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
   1.106 +  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
   1.107 +  finally show "index_size k = nat_of k" .
   1.108 +qed
   1.109 +
   1.110 +lemma [simp, code]:
   1.111 +  "size = nat_of"
   1.112 +proof (rule ext)
   1.113 +  fix k
   1.114 +  show "size k = nat_of k"
   1.115 +  by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
   1.116 +qed
   1.117 +
   1.118 +lemmas [code del] = index.recs index.cases
   1.119 +
   1.120 +lemma [code]:
   1.121 +  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
   1.122 +  by (cases k, cases l) (simp add: eq)
   1.123 +
   1.124 +lemma [code nbe]:
   1.125 +  "eq_class.eq (k::index) k \<longleftrightarrow> True"
   1.126 +  by (rule HOL.eq_refl)
   1.127 +
   1.128 +
   1.129 +subsection {* Indices as datatype of ints *}
   1.130 +
   1.131 +instantiation index :: number
   1.132 +begin
   1.133 +
   1.134 +definition
   1.135 +  "number_of = of_nat o nat"
   1.136 +
   1.137 +instance ..
   1.138 +
   1.139 +end
   1.140 +
   1.141 +lemma nat_of_number [simp]:
   1.142 +  "nat_of (number_of k) = number_of k"
   1.143 +  by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
   1.144 +
   1.145 +code_datatype "number_of \<Colon> int \<Rightarrow> index"
   1.146 +
   1.147 +
   1.148 +subsection {* Basic arithmetic *}
   1.149 +
   1.150 +instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
   1.151 +begin
   1.152 +
   1.153 +definition [simp, code del]:
   1.154 +  "(1\<Colon>index) = of_nat 1"
   1.155 +
   1.156 +definition [simp, code del]:
   1.157 +  "n + m = of_nat (nat_of n + nat_of m)"
   1.158 +
   1.159 +definition [simp, code del]:
   1.160 +  "n - m = of_nat (nat_of n - nat_of m)"
   1.161 +
   1.162 +definition [simp, code del]:
   1.163 +  "n * m = of_nat (nat_of n * nat_of m)"
   1.164 +
   1.165 +definition [simp, code del]:
   1.166 +  "n div m = of_nat (nat_of n div nat_of m)"
   1.167 +
   1.168 +definition [simp, code del]:
   1.169 +  "n mod m = of_nat (nat_of n mod nat_of m)"
   1.170 +
   1.171 +definition [simp, code del]:
   1.172 +  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
   1.173 +
   1.174 +definition [simp, code del]:
   1.175 +  "n < m \<longleftrightarrow> nat_of n < nat_of m"
   1.176 +
   1.177 +instance proof
   1.178 +qed (auto simp add: index left_distrib div_mult_self1)
   1.179 +
   1.180 +end
   1.181 +
   1.182 +lemma zero_index_code [code inline, code]:
   1.183 +  "(0\<Colon>index) = Numeral0"
   1.184 +  by (simp add: number_of_index_def Pls_def)
   1.185 +lemma [code post]: "Numeral0 = (0\<Colon>index)"
   1.186 +  using zero_index_code ..
   1.187 +
   1.188 +lemma one_index_code [code inline, code]:
   1.189 +  "(1\<Colon>index) = Numeral1"
   1.190 +  by (simp add: number_of_index_def Pls_def Bit1_def)
   1.191 +lemma [code post]: "Numeral1 = (1\<Colon>index)"
   1.192 +  using one_index_code ..
   1.193 +
   1.194 +lemma plus_index_code [code nbe]:
   1.195 +  "of_nat n + of_nat m = of_nat (n + m)"
   1.196 +  by simp
   1.197 +
   1.198 +definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
   1.199 +  [simp, code del]: "subtract_index = op -"
   1.200 +
   1.201 +lemma subtract_index_code [code nbe]:
   1.202 +  "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
   1.203 +  by simp
   1.204 +
   1.205 +lemma minus_index_code [code]:
   1.206 +  "n - m = subtract_index n m"
   1.207 +  by simp
   1.208 +
   1.209 +lemma times_index_code [code nbe]:
   1.210 +  "of_nat n * of_nat m = of_nat (n * m)"
   1.211 +  by simp
   1.212 +
   1.213 +lemma less_eq_index_code [code nbe]:
   1.214 +  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
   1.215 +  by simp
   1.216 +
   1.217 +lemma less_index_code [code nbe]:
   1.218 +  "of_nat n < of_nat m \<longleftrightarrow> n < m"
   1.219 +  by simp
   1.220 +
   1.221 +lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
   1.222 +
   1.223 +lemma of_nat_code [code]:
   1.224 +  "of_nat = Nat.of_nat"
   1.225 +proof
   1.226 +  fix n :: nat
   1.227 +  have "Nat.of_nat n = of_nat n"
   1.228 +    by (induct n) simp_all
   1.229 +  then show "of_nat n = Nat.of_nat n"
   1.230 +    by (rule sym)
   1.231 +qed
   1.232 +
   1.233 +lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
   1.234 +  by (cases i) auto
   1.235 +
   1.236 +definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   1.237 +  "nat_of_aux i n = nat_of i + n"
   1.238 +
   1.239 +lemma nat_of_aux_code [code]:
   1.240 +  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
   1.241 +  by (auto simp add: nat_of_aux_def index_not_eq_zero)
   1.242 +
   1.243 +lemma nat_of_code [code]:
   1.244 +  "nat_of i = nat_of_aux i 0"
   1.245 +  by (simp add: nat_of_aux_def)
   1.246 +
   1.247 +definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
   1.248 +  [code del]: "div_mod_index n m = (n div m, n mod m)"
   1.249 +
   1.250 +lemma [code]:
   1.251 +  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   1.252 +  unfolding div_mod_index_def by auto
   1.253 +
   1.254 +lemma [code]:
   1.255 +  "n div m = fst (div_mod_index n m)"
   1.256 +  unfolding div_mod_index_def by simp
   1.257 +
   1.258 +lemma [code]:
   1.259 +  "n mod m = snd (div_mod_index n m)"
   1.260 +  unfolding div_mod_index_def by simp
   1.261 +
   1.262 +hide (open) const of_nat nat_of
   1.263 +
   1.264 +subsection {* ML interface *}
   1.265 +
   1.266 +ML {*
   1.267 +structure Index =
   1.268 +struct
   1.269 +
   1.270 +fun mk k = HOLogic.mk_number @{typ index} k;
   1.271 +
   1.272 +end;
   1.273 +*}
   1.274 +
   1.275 +
   1.276 +subsection {* Code generator setup *}
   1.277 +
   1.278 +text {* Implementation of indices by bounded integers *}
   1.279 +
   1.280 +code_type index
   1.281 +  (SML "int")
   1.282 +  (OCaml "int")
   1.283 +  (Haskell "Int")
   1.284 +
   1.285 +code_instance index :: eq
   1.286 +  (Haskell -)
   1.287 +
   1.288 +setup {*
   1.289 +  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
   1.290 +    false false) ["SML", "OCaml", "Haskell"]
   1.291 +*}
   1.292 +
   1.293 +code_reserved SML Int int
   1.294 +code_reserved OCaml Pervasives int
   1.295 +
   1.296 +code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.297 +  (SML "Int.+/ ((_),/ (_))")
   1.298 +  (OCaml "Pervasives.( + )")
   1.299 +  (Haskell infixl 6 "+")
   1.300 +
   1.301 +code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.302 +  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   1.303 +  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   1.304 +  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
   1.305 +
   1.306 +code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.307 +  (SML "Int.*/ ((_),/ (_))")
   1.308 +  (OCaml "Pervasives.( * )")
   1.309 +  (Haskell infixl 7 "*")
   1.310 +
   1.311 +code_const div_mod_index
   1.312 +  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
   1.313 +  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
   1.314 +  (Haskell "divMod")
   1.315 +
   1.316 +code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   1.317 +  (SML "!((_ : Int.int) = _)")
   1.318 +  (OCaml "!((_ : int) = _)")
   1.319 +  (Haskell infixl 4 "==")
   1.320 +
   1.321 +code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   1.322 +  (SML "Int.<=/ ((_),/ (_))")
   1.323 +  (OCaml "!((_ : int) <= _)")
   1.324 +  (Haskell infix 4 "<=")
   1.325 +
   1.326 +code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   1.327 +  (SML "Int.</ ((_),/ (_))")
   1.328 +  (OCaml "!((_ : int) < _)")
   1.329 +  (Haskell infix 4 "<")
   1.330 +
   1.331 +text {* Evaluation *}
   1.332 +
   1.333 +lemma [code, code del]:
   1.334 +  "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
   1.335 +
   1.336 +code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
   1.337 +  (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)")
   1.338 +
   1.339 +end
     2.1 --- a/src/HOL/Complex_Main.thy	Fri May 15 16:52:28 2009 +0200
     2.2 +++ b/src/HOL/Complex_Main.thy	Sat May 16 20:16:49 2009 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4    Ln
     2.5    Taylor
     2.6    Integration
     2.7 -  "Library/Quickcheck"
     2.8 +  Quickcheck
     2.9  begin
    2.10  
    2.11  end
     3.1 --- a/src/HOL/IsaMakefile	Fri May 15 16:52:28 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Sat May 16 20:16:49 2009 +0200
     3.3 @@ -206,6 +206,7 @@
     3.4  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
     3.5    ATP_Linkup.thy \
     3.6    Code_Eval.thy \
     3.7 +  Code_Index.thy \
     3.8    Equiv_Relations.thy \
     3.9    Groebner_Basis.thy \
    3.10    Hilbert_Choice.thy \
    3.11 @@ -286,16 +287,16 @@
    3.12    Transcendental.thy \
    3.13    GCD.thy \
    3.14    Parity.thy \
    3.15 +  Quickcheck.thy \
    3.16    Lubs.thy \
    3.17    PReal.thy \
    3.18 +  Random.thy \
    3.19    Rational.thy \
    3.20    RComplete.thy \
    3.21    RealDef.thy \
    3.22    RealPow.thy \
    3.23    Real.thy \
    3.24    RealVector.thy \
    3.25 -  Library/Random.thy \
    3.26 -  Library/Quickcheck.thy \
    3.27    Tools/float_syntax.ML \
    3.28    Tools/Qelim/ferrante_rackoff_data.ML \
    3.29    Tools/Qelim/ferrante_rackoff.ML \
    3.30 @@ -335,7 +336,7 @@
    3.31    Library/comm_ring.ML Library/Coinductive_List.thy			\
    3.32    Library/AssocList.thy	Library/Formal_Power_Series.thy	\
    3.33    Library/Binomial.thy Library/Eval_Witness.thy				\
    3.34 -  Library/Code_Index.thy Library/Code_Char.thy				\
    3.35 +  Library/Code_Char.thy				\
    3.36    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
    3.37    Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy	\
    3.38    Library/Boolean_Algebra.thy Library/Countable.thy			\
     4.1 --- a/src/HOL/Library/Code_Index.thy	Fri May 15 16:52:28 2009 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,336 +0,0 @@
     4.4 -(* Author: Florian Haftmann, TU Muenchen *)
     4.5 -
     4.6 -header {* Type of indices *}
     4.7 -
     4.8 -theory Code_Index
     4.9 -imports Main
    4.10 -begin
    4.11 -
    4.12 -text {*
    4.13 -  Indices are isomorphic to HOL @{typ nat} but
    4.14 -  mapped to target-language builtin integers.
    4.15 -*}
    4.16 -
    4.17 -subsection {* Datatype of indices *}
    4.18 -
    4.19 -typedef (open) index = "UNIV \<Colon> nat set"
    4.20 -  morphisms nat_of of_nat by rule
    4.21 -
    4.22 -lemma of_nat_nat_of [simp]:
    4.23 -  "of_nat (nat_of k) = k"
    4.24 -  by (rule nat_of_inverse)
    4.25 -
    4.26 -lemma nat_of_of_nat [simp]:
    4.27 -  "nat_of (of_nat n) = n"
    4.28 -  by (rule of_nat_inverse) (rule UNIV_I)
    4.29 -
    4.30 -lemma [measure_function]:
    4.31 -  "is_measure nat_of" by (rule is_measure_trivial)
    4.32 -
    4.33 -lemma index:
    4.34 -  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
    4.35 -proof
    4.36 -  fix n :: nat
    4.37 -  assume "\<And>n\<Colon>index. PROP P n"
    4.38 -  then show "PROP P (of_nat n)" .
    4.39 -next
    4.40 -  fix n :: index
    4.41 -  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
    4.42 -  then have "PROP P (of_nat (nat_of n))" .
    4.43 -  then show "PROP P n" by simp
    4.44 -qed
    4.45 -
    4.46 -lemma index_case:
    4.47 -  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
    4.48 -  shows P
    4.49 -  by (rule assms [of "nat_of k"]) simp
    4.50 -
    4.51 -lemma index_induct_raw:
    4.52 -  assumes "\<And>n. P (of_nat n)"
    4.53 -  shows "P k"
    4.54 -proof -
    4.55 -  from assms have "P (of_nat (nat_of k))" .
    4.56 -  then show ?thesis by simp
    4.57 -qed
    4.58 -
    4.59 -lemma nat_of_inject [simp]:
    4.60 -  "nat_of k = nat_of l \<longleftrightarrow> k = l"
    4.61 -  by (rule nat_of_inject)
    4.62 -
    4.63 -lemma of_nat_inject [simp]:
    4.64 -  "of_nat n = of_nat m \<longleftrightarrow> n = m"
    4.65 -  by (rule of_nat_inject) (rule UNIV_I)+
    4.66 -
    4.67 -instantiation index :: zero
    4.68 -begin
    4.69 -
    4.70 -definition [simp, code del]:
    4.71 -  "0 = of_nat 0"
    4.72 -
    4.73 -instance ..
    4.74 -
    4.75 -end
    4.76 -
    4.77 -definition [simp]:
    4.78 -  "Suc_index k = of_nat (Suc (nat_of k))"
    4.79 -
    4.80 -rep_datatype "0 \<Colon> index" Suc_index
    4.81 -proof -
    4.82 -  fix P :: "index \<Rightarrow> bool"
    4.83 -  fix k :: index
    4.84 -  assume "P 0" then have init: "P (of_nat 0)" by simp
    4.85 -  assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
    4.86 -    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
    4.87 -    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
    4.88 -  from init step have "P (of_nat (nat_of k))"
    4.89 -    by (induct "nat_of k") simp_all
    4.90 -  then show "P k" by simp
    4.91 -qed simp_all
    4.92 -
    4.93 -declare index_case [case_names nat, cases type: index]
    4.94 -declare index.induct [case_names nat, induct type: index]
    4.95 -
    4.96 -lemma index_decr [termination_simp]:
    4.97 -  "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
    4.98 -  by (cases k) simp
    4.99 -
   4.100 -lemma [simp, code]:
   4.101 -  "index_size = nat_of"
   4.102 -proof (rule ext)
   4.103 -  fix k
   4.104 -  have "index_size k = nat_size (nat_of k)"
   4.105 -    by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
   4.106 -  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
   4.107 -  finally show "index_size k = nat_of k" .
   4.108 -qed
   4.109 -
   4.110 -lemma [simp, code]:
   4.111 -  "size = nat_of"
   4.112 -proof (rule ext)
   4.113 -  fix k
   4.114 -  show "size k = nat_of k"
   4.115 -  by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
   4.116 -qed
   4.117 -
   4.118 -lemmas [code del] = index.recs index.cases
   4.119 -
   4.120 -lemma [code]:
   4.121 -  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
   4.122 -  by (cases k, cases l) (simp add: eq)
   4.123 -
   4.124 -lemma [code nbe]:
   4.125 -  "eq_class.eq (k::index) k \<longleftrightarrow> True"
   4.126 -  by (rule HOL.eq_refl)
   4.127 -
   4.128 -
   4.129 -subsection {* Indices as datatype of ints *}
   4.130 -
   4.131 -instantiation index :: number
   4.132 -begin
   4.133 -
   4.134 -definition
   4.135 -  "number_of = of_nat o nat"
   4.136 -
   4.137 -instance ..
   4.138 -
   4.139 -end
   4.140 -
   4.141 -lemma nat_of_number [simp]:
   4.142 -  "nat_of (number_of k) = number_of k"
   4.143 -  by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
   4.144 -
   4.145 -code_datatype "number_of \<Colon> int \<Rightarrow> index"
   4.146 -
   4.147 -
   4.148 -subsection {* Basic arithmetic *}
   4.149 -
   4.150 -instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
   4.151 -begin
   4.152 -
   4.153 -definition [simp, code del]:
   4.154 -  "(1\<Colon>index) = of_nat 1"
   4.155 -
   4.156 -definition [simp, code del]:
   4.157 -  "n + m = of_nat (nat_of n + nat_of m)"
   4.158 -
   4.159 -definition [simp, code del]:
   4.160 -  "n - m = of_nat (nat_of n - nat_of m)"
   4.161 -
   4.162 -definition [simp, code del]:
   4.163 -  "n * m = of_nat (nat_of n * nat_of m)"
   4.164 -
   4.165 -definition [simp, code del]:
   4.166 -  "n div m = of_nat (nat_of n div nat_of m)"
   4.167 -
   4.168 -definition [simp, code del]:
   4.169 -  "n mod m = of_nat (nat_of n mod nat_of m)"
   4.170 -
   4.171 -definition [simp, code del]:
   4.172 -  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
   4.173 -
   4.174 -definition [simp, code del]:
   4.175 -  "n < m \<longleftrightarrow> nat_of n < nat_of m"
   4.176 -
   4.177 -instance proof
   4.178 -qed (auto simp add: index left_distrib div_mult_self1)
   4.179 -
   4.180 -end
   4.181 -
   4.182 -lemma zero_index_code [code inline, code]:
   4.183 -  "(0\<Colon>index) = Numeral0"
   4.184 -  by (simp add: number_of_index_def Pls_def)
   4.185 -lemma [code post]: "Numeral0 = (0\<Colon>index)"
   4.186 -  using zero_index_code ..
   4.187 -
   4.188 -lemma one_index_code [code inline, code]:
   4.189 -  "(1\<Colon>index) = Numeral1"
   4.190 -  by (simp add: number_of_index_def Pls_def Bit1_def)
   4.191 -lemma [code post]: "Numeral1 = (1\<Colon>index)"
   4.192 -  using one_index_code ..
   4.193 -
   4.194 -lemma plus_index_code [code nbe]:
   4.195 -  "of_nat n + of_nat m = of_nat (n + m)"
   4.196 -  by simp
   4.197 -
   4.198 -definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
   4.199 -  [simp, code del]: "subtract_index = op -"
   4.200 -
   4.201 -lemma subtract_index_code [code nbe]:
   4.202 -  "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
   4.203 -  by simp
   4.204 -
   4.205 -lemma minus_index_code [code]:
   4.206 -  "n - m = subtract_index n m"
   4.207 -  by simp
   4.208 -
   4.209 -lemma times_index_code [code nbe]:
   4.210 -  "of_nat n * of_nat m = of_nat (n * m)"
   4.211 -  by simp
   4.212 -
   4.213 -lemma less_eq_index_code [code nbe]:
   4.214 -  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
   4.215 -  by simp
   4.216 -
   4.217 -lemma less_index_code [code nbe]:
   4.218 -  "of_nat n < of_nat m \<longleftrightarrow> n < m"
   4.219 -  by simp
   4.220 -
   4.221 -lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
   4.222 -
   4.223 -lemma of_nat_code [code]:
   4.224 -  "of_nat = Nat.of_nat"
   4.225 -proof
   4.226 -  fix n :: nat
   4.227 -  have "Nat.of_nat n = of_nat n"
   4.228 -    by (induct n) simp_all
   4.229 -  then show "of_nat n = Nat.of_nat n"
   4.230 -    by (rule sym)
   4.231 -qed
   4.232 -
   4.233 -lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
   4.234 -  by (cases i) auto
   4.235 -
   4.236 -definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   4.237 -  "nat_of_aux i n = nat_of i + n"
   4.238 -
   4.239 -lemma nat_of_aux_code [code]:
   4.240 -  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
   4.241 -  by (auto simp add: nat_of_aux_def index_not_eq_zero)
   4.242 -
   4.243 -lemma nat_of_code [code]:
   4.244 -  "nat_of i = nat_of_aux i 0"
   4.245 -  by (simp add: nat_of_aux_def)
   4.246 -
   4.247 -definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
   4.248 -  [code del]: "div_mod_index n m = (n div m, n mod m)"
   4.249 -
   4.250 -lemma [code]:
   4.251 -  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   4.252 -  unfolding div_mod_index_def by auto
   4.253 -
   4.254 -lemma [code]:
   4.255 -  "n div m = fst (div_mod_index n m)"
   4.256 -  unfolding div_mod_index_def by simp
   4.257 -
   4.258 -lemma [code]:
   4.259 -  "n mod m = snd (div_mod_index n m)"
   4.260 -  unfolding div_mod_index_def by simp
   4.261 -
   4.262 -hide (open) const of_nat nat_of
   4.263 -
   4.264 -subsection {* ML interface *}
   4.265 -
   4.266 -ML {*
   4.267 -structure Index =
   4.268 -struct
   4.269 -
   4.270 -fun mk k = HOLogic.mk_number @{typ index} k;
   4.271 -
   4.272 -end;
   4.273 -*}
   4.274 -
   4.275 -
   4.276 -subsection {* Code generator setup *}
   4.277 -
   4.278 -text {* Implementation of indices by bounded integers *}
   4.279 -
   4.280 -code_type index
   4.281 -  (SML "int")
   4.282 -  (OCaml "int")
   4.283 -  (Haskell "Int")
   4.284 -
   4.285 -code_instance index :: eq
   4.286 -  (Haskell -)
   4.287 -
   4.288 -setup {*
   4.289 -  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
   4.290 -    false false) ["SML", "OCaml", "Haskell"]
   4.291 -*}
   4.292 -
   4.293 -code_reserved SML Int int
   4.294 -code_reserved OCaml Pervasives int
   4.295 -
   4.296 -code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   4.297 -  (SML "Int.+/ ((_),/ (_))")
   4.298 -  (OCaml "Pervasives.( + )")
   4.299 -  (Haskell infixl 6 "+")
   4.300 -
   4.301 -code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   4.302 -  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   4.303 -  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   4.304 -  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
   4.305 -
   4.306 -code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   4.307 -  (SML "Int.*/ ((_),/ (_))")
   4.308 -  (OCaml "Pervasives.( * )")
   4.309 -  (Haskell infixl 7 "*")
   4.310 -
   4.311 -code_const div_mod_index
   4.312 -  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
   4.313 -  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
   4.314 -  (Haskell "divMod")
   4.315 -
   4.316 -code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   4.317 -  (SML "!((_ : Int.int) = _)")
   4.318 -  (OCaml "!((_ : int) = _)")
   4.319 -  (Haskell infixl 4 "==")
   4.320 -
   4.321 -code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   4.322 -  (SML "Int.<=/ ((_),/ (_))")
   4.323 -  (OCaml "!((_ : int) <= _)")
   4.324 -  (Haskell infix 4 "<=")
   4.325 -
   4.326 -code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   4.327 -  (SML "Int.</ ((_),/ (_))")
   4.328 -  (OCaml "!((_ : int) < _)")
   4.329 -  (Haskell infix 4 "<")
   4.330 -
   4.331 -text {* Evaluation *}
   4.332 -
   4.333 -lemma [code, code del]:
   4.334 -  "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
   4.335 -
   4.336 -code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
   4.337 -  (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)")
   4.338 -
   4.339 -end
     5.1 --- a/src/HOL/Library/Library.thy	Fri May 15 16:52:28 2009 +0200
     5.2 +++ b/src/HOL/Library/Library.thy	Sat May 16 20:16:49 2009 +0200
     5.3 @@ -9,7 +9,6 @@
     5.4    Boolean_Algebra
     5.5    Char_ord
     5.6    Code_Char_chr
     5.7 -  Code_Index
     5.8    Code_Integer
     5.9    Coinductive_List
    5.10    Commutative_Ring
    5.11 @@ -45,11 +44,9 @@
    5.12    Preorder
    5.13    Primes
    5.14    Product_Vector
    5.15 -  Quickcheck
    5.16    Quicksort
    5.17    Quotient
    5.18    Ramsey
    5.19 -  Random
    5.20    Reflection
    5.21    RBT
    5.22    State_Monad
     6.1 --- a/src/HOL/Library/Quickcheck.thy	Fri May 15 16:52:28 2009 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,232 +0,0 @@
     6.4 -(* Author: Florian Haftmann, TU Muenchen *)
     6.5 -
     6.6 -header {* A simple counterexample generator *}
     6.7 -
     6.8 -theory Quickcheck
     6.9 -imports Main Real Random
    6.10 -begin
    6.11 -
    6.12 -notation fcomp (infixl "o>" 60)
    6.13 -notation scomp (infixl "o\<rightarrow>" 60)
    6.14 -
    6.15 -
    6.16 -subsection {* The @{text random} class *}
    6.17 -
    6.18 -class random = typerep +
    6.19 -  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    6.20 -
    6.21 -
    6.22 -subsection {* Quickcheck generator *}
    6.23 -
    6.24 -ML {*
    6.25 -structure Quickcheck =
    6.26 -struct
    6.27 -
    6.28 -open Quickcheck;
    6.29 -
    6.30 -val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
    6.31 -
    6.32 -val target = "Quickcheck";
    6.33 -
    6.34 -fun mk_generator_expr thy prop tys =
    6.35 -  let
    6.36 -    val bound_max = length tys - 1;
    6.37 -    val bounds = map_index (fn (i, ty) =>
    6.38 -      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
    6.39 -    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    6.40 -    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    6.41 -    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
    6.42 -      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
    6.43 -    val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
    6.44 -    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    6.45 -    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    6.46 -    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    6.47 -      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    6.48 -    fun mk_split ty = Sign.mk_const thy
    6.49 -      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    6.50 -    fun mk_scomp_split ty t t' =
    6.51 -      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
    6.52 -        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
    6.53 -    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    6.54 -      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
    6.55 -  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
    6.56 -
    6.57 -fun compile_generator_expr thy t =
    6.58 -  let
    6.59 -    val tys = (map snd o fst o strip_abs) t;
    6.60 -    val t' = mk_generator_expr thy t tys;
    6.61 -    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
    6.62 -      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    6.63 -  in f #> Random_Engine.run end;
    6.64 -
    6.65 -end
    6.66 -*}
    6.67 -
    6.68 -setup {*
    6.69 -  Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
    6.70 -  #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
    6.71 -*}
    6.72 -
    6.73 -
    6.74 -subsection {* Fundamental types*}
    6.75 -
    6.76 -definition (in term_syntax)
    6.77 -  "termify_bool b = (if b then termify True else termify False)"
    6.78 -
    6.79 -instantiation bool :: random
    6.80 -begin
    6.81 -
    6.82 -definition
    6.83 -  "random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))"
    6.84 -
    6.85 -instance ..
    6.86 -
    6.87 -end
    6.88 -
    6.89 -definition (in term_syntax)
    6.90 -  "termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)"
    6.91 -
    6.92 -instantiation itself :: (typerep) random
    6.93 -begin
    6.94 -
    6.95 -definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    6.96 -  "random_itself _ = Pair (termify_itself TYPE('a))"
    6.97 -
    6.98 -instance ..
    6.99 -
   6.100 -end
   6.101 -
   6.102 -text {* Type @{typ "'a \<Rightarrow> 'b"} *}
   6.103 -
   6.104 -ML {*
   6.105 -structure Random_Engine =
   6.106 -struct
   6.107 -
   6.108 -open Random_Engine;
   6.109 -
   6.110 -fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
   6.111 -    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
   6.112 -    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
   6.113 -    (seed : Random_Engine.seed) =
   6.114 -  let
   6.115 -    val (seed', seed'') = random_split seed;
   6.116 -    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
   6.117 -    val fun_upd = Const (@{const_name fun_upd},
   6.118 -      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
   6.119 -    fun random_fun' x =
   6.120 -      let
   6.121 -        val (seed, fun_map, f_t) = ! state;
   6.122 -      in case AList.lookup (uncurry eq) fun_map x
   6.123 -       of SOME y => y
   6.124 -        | NONE => let
   6.125 -              val t1 = term_of x;
   6.126 -              val ((y, t2), seed') = random seed;
   6.127 -              val fun_map' = (x, y) :: fun_map;
   6.128 -              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
   6.129 -              val _ = state := (seed', fun_map', f_t');
   6.130 -            in y end
   6.131 -      end;
   6.132 -    fun term_fun' () = #3 (! state);
   6.133 -  in ((random_fun', term_fun'), seed'') end;
   6.134 -
   6.135 -end
   6.136 -*}
   6.137 -
   6.138 -axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   6.139 -  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   6.140 -  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   6.141 -
   6.142 -code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
   6.143 -  -- {* With enough criminal energy this can be abused to derive @{prop False};
   6.144 -  for this reason we use a distinguished target @{text Quickcheck}
   6.145 -  not spoiling the regular trusted code generation *}
   6.146 -
   6.147 -instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   6.148 -begin
   6.149 -
   6.150 -definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   6.151 -  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
   6.152 -
   6.153 -instance ..
   6.154 -
   6.155 -end
   6.156 -
   6.157 -code_reserved Quickcheck Random_Engine
   6.158 -
   6.159 -
   6.160 -subsection {* Numeric types *}
   6.161 -
   6.162 -function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   6.163 -  "termify_numeral k = (if k = 0 then termify Int.Pls
   6.164 -    else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))"
   6.165 -  by pat_completeness auto
   6.166 -
   6.167 -declare (in term_syntax) termify_numeral.psimps [simp del]
   6.168 -
   6.169 -termination termify_numeral by (relation "measure Code_Index.nat_of")
   6.170 -  (simp_all add: index)
   6.171 -
   6.172 -definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   6.173 -  "termify_int_number k = termify number_of <\<cdot>> termify_numeral k"
   6.174 -
   6.175 -definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where
   6.176 -  "termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k"
   6.177 -
   6.178 -declare termify_nat_number_def [simplified snd_conv, code]
   6.179 -
   6.180 -instantiation nat :: random
   6.181 -begin
   6.182 -
   6.183 -definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   6.184 -  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))"
   6.185 -
   6.186 -instance ..
   6.187 -
   6.188 -end
   6.189 -
   6.190 -definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   6.191 -  [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
   6.192 -
   6.193 -instantiation int :: random
   6.194 -begin
   6.195 -
   6.196 -definition
   6.197 -  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
   6.198 -     then let j = k - i in termify_int_number j
   6.199 -     else let j = i - k in term_uminus (termify_int_number j)))"
   6.200 -
   6.201 -instance ..
   6.202 -
   6.203 -end
   6.204 -
   6.205 -definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where
   6.206 -  [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
   6.207 -
   6.208 -instantiation rat :: random
   6.209 -begin
   6.210 -
   6.211 -definition
   6.212 -  "random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))"
   6.213 -
   6.214 -instance ..
   6.215 -
   6.216 -end
   6.217 -
   6.218 -definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
   6.219 -  [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
   6.220 -
   6.221 -instantiation real :: random
   6.222 -begin
   6.223 -
   6.224 -definition
   6.225 -  "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
   6.226 -
   6.227 -instance ..
   6.228 -
   6.229 -end
   6.230 -
   6.231 -
   6.232 -no_notation fcomp (infixl "o>" 60)
   6.233 -no_notation scomp (infixl "o\<rightarrow>" 60)
   6.234 -
   6.235 -end
     7.1 --- a/src/HOL/Library/Random.thy	Fri May 15 16:52:28 2009 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,177 +0,0 @@
     7.4 -(* Author: Florian Haftmann, TU Muenchen *)
     7.5 -
     7.6 -header {* A HOL random engine *}
     7.7 -
     7.8 -theory Random
     7.9 -imports Code_Index
    7.10 -begin
    7.11 -
    7.12 -notation fcomp (infixl "o>" 60)
    7.13 -notation scomp (infixl "o\<rightarrow>" 60)
    7.14 -
    7.15 -
    7.16 -subsection {* Auxiliary functions *}
    7.17 -
    7.18 -definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
    7.19 -  "inc_shift v k = (if v = k then 1 else k + 1)"
    7.20 -
    7.21 -definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
    7.22 -  "minus_shift r k l = (if k < l then r + k - l else k - l)"
    7.23 -
    7.24 -fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
    7.25 -  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    7.26 -
    7.27 -
    7.28 -subsection {* Random seeds *}
    7.29 -
    7.30 -types seed = "index \<times> index"
    7.31 -
    7.32 -primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
    7.33 -  "next (v, w) = (let
    7.34 -     k =  v div 53668;
    7.35 -     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
    7.36 -     l =  w div 52774;
    7.37 -     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
    7.38 -     z =  minus_shift 2147483562 v' (w' + 1) + 1
    7.39 -   in (z, (v', w')))"
    7.40 -
    7.41 -lemma next_not_0:
    7.42 -  "fst (next s) \<noteq> 0"
    7.43 -  by (cases s) (auto simp add: minus_shift_def Let_def)
    7.44 -
    7.45 -primrec seed_invariant :: "seed \<Rightarrow> bool" where
    7.46 -  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
    7.47 -
    7.48 -lemma if_same: "(if b then f x else f y) = f (if b then x else y)"
    7.49 -  by (cases b) simp_all
    7.50 -
    7.51 -definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
    7.52 -  "split_seed s = (let
    7.53 -     (v, w) = s;
    7.54 -     (v', w') = snd (next s);
    7.55 -     v'' = inc_shift 2147483562 v;
    7.56 -     s'' = (v'', w');
    7.57 -     w'' = inc_shift 2147483398 w;
    7.58 -     s''' = (v', w'')
    7.59 -   in (s'', s'''))"
    7.60 -
    7.61 -
    7.62 -subsection {* Base selectors *}
    7.63 -
    7.64 -fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    7.65 -  "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
    7.66 -
    7.67 -definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
    7.68 -  "range k = iterate (log 2147483561 k)
    7.69 -      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
    7.70 -    o\<rightarrow> (\<lambda>v. Pair (v mod k))"
    7.71 -
    7.72 -lemma range:
    7.73 -  "k > 0 \<Longrightarrow> fst (range k s) < k"
    7.74 -  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
    7.75 -
    7.76 -definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    7.77 -  "select xs = range (Code_Index.of_nat (length xs))
    7.78 -    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
    7.79 -     
    7.80 -lemma select:
    7.81 -  assumes "xs \<noteq> []"
    7.82 -  shows "fst (select xs s) \<in> set xs"
    7.83 -proof -
    7.84 -  from assms have "Code_Index.of_nat (length xs) > 0" by simp
    7.85 -  with range have
    7.86 -    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
    7.87 -  then have
    7.88 -    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
    7.89 -  then show ?thesis
    7.90 -    by (simp add: scomp_apply split_beta select_def)
    7.91 -qed
    7.92 -
    7.93 -primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
    7.94 -  "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
    7.95 -
    7.96 -lemma pick_member:
    7.97 -  "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
    7.98 -  by (induct xs arbitrary: i) simp_all
    7.99 -
   7.100 -lemma pick_drop_zero:
   7.101 -  "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
   7.102 -  by (induct xs) (auto simp add: expand_fun_eq)
   7.103 -
   7.104 -definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   7.105 -  "select_weight xs = range (listsum (map fst xs))
   7.106 -   o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
   7.107 -
   7.108 -lemma select_weight_member:
   7.109 -  assumes "0 < listsum (map fst xs)"
   7.110 -  shows "fst (select_weight xs s) \<in> set (map snd xs)"
   7.111 -proof -
   7.112 -  from range assms
   7.113 -    have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
   7.114 -  with pick_member
   7.115 -    have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
   7.116 -  then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
   7.117 -qed
   7.118 -
   7.119 -definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   7.120 -  [code del]: "select_default k x y = range k
   7.121 -     o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
   7.122 -
   7.123 -lemma select_default_zero:
   7.124 -  "fst (select_default 0 x y s) = y"
   7.125 -  by (simp add: scomp_apply split_beta select_default_def)
   7.126 -
   7.127 -lemma select_default_code [code]:
   7.128 -  "select_default k x y = (if k = 0
   7.129 -    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
   7.130 -    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
   7.131 -proof
   7.132 -  fix s
   7.133 -  have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
   7.134 -    by (simp add: range_def scomp_Pair scomp_apply split_beta)
   7.135 -  then show "select_default k x y s = (if k = 0
   7.136 -    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
   7.137 -    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
   7.138 -    by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
   7.139 -qed
   7.140 -
   7.141 -
   7.142 -subsection {* @{text ML} interface *}
   7.143 -
   7.144 -ML {*
   7.145 -structure Random_Engine =
   7.146 -struct
   7.147 -
   7.148 -type seed = int * int;
   7.149 -
   7.150 -local
   7.151 -
   7.152 -val seed = ref 
   7.153 -  (let
   7.154 -    val now = Time.toMilliseconds (Time.now ());
   7.155 -    val (q, s1) = IntInf.divMod (now, 2147483562);
   7.156 -    val s2 = q mod 2147483398;
   7.157 -  in (s1 + 1, s2 + 1) end);
   7.158 -
   7.159 -in
   7.160 -
   7.161 -fun run f =
   7.162 -  let
   7.163 -    val (x, seed') = f (! seed);
   7.164 -    val _ = seed := seed'
   7.165 -  in x end;
   7.166 -
   7.167 -end;
   7.168 -
   7.169 -end;
   7.170 -*}
   7.171 -
   7.172 -hide (open) type seed
   7.173 -hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
   7.174 -  iterate range select pick select_weight select_default
   7.175 -
   7.176 -no_notation fcomp (infixl "o>" 60)
   7.177 -no_notation scomp (infixl "o\<rightarrow>" 60)
   7.178 -
   7.179 -end
   7.180 -
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Quickcheck.thy	Sat May 16 20:16:49 2009 +0200
     8.3 @@ -0,0 +1,232 @@
     8.4 +(* Author: Florian Haftmann, TU Muenchen *)
     8.5 +
     8.6 +header {* A simple counterexample generator *}
     8.7 +
     8.8 +theory Quickcheck
     8.9 +imports Main Real Random
    8.10 +begin
    8.11 +
    8.12 +notation fcomp (infixl "o>" 60)
    8.13 +notation scomp (infixl "o\<rightarrow>" 60)
    8.14 +
    8.15 +
    8.16 +subsection {* The @{text random} class *}
    8.17 +
    8.18 +class random = typerep +
    8.19 +  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    8.20 +
    8.21 +
    8.22 +subsection {* Quickcheck generator *}
    8.23 +
    8.24 +ML {*
    8.25 +structure Quickcheck =
    8.26 +struct
    8.27 +
    8.28 +open Quickcheck;
    8.29 +
    8.30 +val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
    8.31 +
    8.32 +val target = "Quickcheck";
    8.33 +
    8.34 +fun mk_generator_expr thy prop tys =
    8.35 +  let
    8.36 +    val bound_max = length tys - 1;
    8.37 +    val bounds = map_index (fn (i, ty) =>
    8.38 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
    8.39 +    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    8.40 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    8.41 +    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
    8.42 +      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
    8.43 +    val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
    8.44 +    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    8.45 +    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    8.46 +    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    8.47 +      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    8.48 +    fun mk_split ty = Sign.mk_const thy
    8.49 +      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    8.50 +    fun mk_scomp_split ty t t' =
    8.51 +      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
    8.52 +        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
    8.53 +    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    8.54 +      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
    8.55 +  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
    8.56 +
    8.57 +fun compile_generator_expr thy t =
    8.58 +  let
    8.59 +    val tys = (map snd o fst o strip_abs) t;
    8.60 +    val t' = mk_generator_expr thy t tys;
    8.61 +    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
    8.62 +      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    8.63 +  in f #> Random_Engine.run end;
    8.64 +
    8.65 +end
    8.66 +*}
    8.67 +
    8.68 +setup {*
    8.69 +  Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
    8.70 +  #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
    8.71 +*}
    8.72 +
    8.73 +
    8.74 +subsection {* Fundamental types*}
    8.75 +
    8.76 +definition (in term_syntax)
    8.77 +  "termify_bool b = (if b then termify True else termify False)"
    8.78 +
    8.79 +instantiation bool :: random
    8.80 +begin
    8.81 +
    8.82 +definition
    8.83 +  "random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))"
    8.84 +
    8.85 +instance ..
    8.86 +
    8.87 +end
    8.88 +
    8.89 +definition (in term_syntax)
    8.90 +  "termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)"
    8.91 +
    8.92 +instantiation itself :: (typerep) random
    8.93 +begin
    8.94 +
    8.95 +definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    8.96 +  "random_itself _ = Pair (termify_itself TYPE('a))"
    8.97 +
    8.98 +instance ..
    8.99 +
   8.100 +end
   8.101 +
   8.102 +text {* Type @{typ "'a \<Rightarrow> 'b"} *}
   8.103 +
   8.104 +ML {*
   8.105 +structure Random_Engine =
   8.106 +struct
   8.107 +
   8.108 +open Random_Engine;
   8.109 +
   8.110 +fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
   8.111 +    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
   8.112 +    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
   8.113 +    (seed : Random_Engine.seed) =
   8.114 +  let
   8.115 +    val (seed', seed'') = random_split seed;
   8.116 +    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
   8.117 +    val fun_upd = Const (@{const_name fun_upd},
   8.118 +      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
   8.119 +    fun random_fun' x =
   8.120 +      let
   8.121 +        val (seed, fun_map, f_t) = ! state;
   8.122 +      in case AList.lookup (uncurry eq) fun_map x
   8.123 +       of SOME y => y
   8.124 +        | NONE => let
   8.125 +              val t1 = term_of x;
   8.126 +              val ((y, t2), seed') = random seed;
   8.127 +              val fun_map' = (x, y) :: fun_map;
   8.128 +              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
   8.129 +              val _ = state := (seed', fun_map', f_t');
   8.130 +            in y end
   8.131 +      end;
   8.132 +    fun term_fun' () = #3 (! state);
   8.133 +  in ((random_fun', term_fun'), seed'') end;
   8.134 +
   8.135 +end
   8.136 +*}
   8.137 +
   8.138 +axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   8.139 +  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   8.140 +  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   8.141 +
   8.142 +code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
   8.143 +  -- {* With enough criminal energy this can be abused to derive @{prop False};
   8.144 +  for this reason we use a distinguished target @{text Quickcheck}
   8.145 +  not spoiling the regular trusted code generation *}
   8.146 +
   8.147 +instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   8.148 +begin
   8.149 +
   8.150 +definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   8.151 +  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
   8.152 +
   8.153 +instance ..
   8.154 +
   8.155 +end
   8.156 +
   8.157 +code_reserved Quickcheck Random_Engine
   8.158 +
   8.159 +
   8.160 +subsection {* Numeric types *}
   8.161 +
   8.162 +function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   8.163 +  "termify_numeral k = (if k = 0 then termify Int.Pls
   8.164 +    else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))"
   8.165 +  by pat_completeness auto
   8.166 +
   8.167 +declare (in term_syntax) termify_numeral.psimps [simp del]
   8.168 +
   8.169 +termination termify_numeral by (relation "measure Code_Index.nat_of")
   8.170 +  (simp_all add: index)
   8.171 +
   8.172 +definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   8.173 +  "termify_int_number k = termify number_of <\<cdot>> termify_numeral k"
   8.174 +
   8.175 +definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where
   8.176 +  "termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k"
   8.177 +
   8.178 +declare termify_nat_number_def [simplified snd_conv, code]
   8.179 +
   8.180 +instantiation nat :: random
   8.181 +begin
   8.182 +
   8.183 +definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   8.184 +  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))"
   8.185 +
   8.186 +instance ..
   8.187 +
   8.188 +end
   8.189 +
   8.190 +definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   8.191 +  [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
   8.192 +
   8.193 +instantiation int :: random
   8.194 +begin
   8.195 +
   8.196 +definition
   8.197 +  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
   8.198 +     then let j = k - i in termify_int_number j
   8.199 +     else let j = i - k in term_uminus (termify_int_number j)))"
   8.200 +
   8.201 +instance ..
   8.202 +
   8.203 +end
   8.204 +
   8.205 +definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where
   8.206 +  [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
   8.207 +
   8.208 +instantiation rat :: random
   8.209 +begin
   8.210 +
   8.211 +definition
   8.212 +  "random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))"
   8.213 +
   8.214 +instance ..
   8.215 +
   8.216 +end
   8.217 +
   8.218 +definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
   8.219 +  [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
   8.220 +
   8.221 +instantiation real :: random
   8.222 +begin
   8.223 +
   8.224 +definition
   8.225 +  "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
   8.226 +
   8.227 +instance ..
   8.228 +
   8.229 +end
   8.230 +
   8.231 +
   8.232 +no_notation fcomp (infixl "o>" 60)
   8.233 +no_notation scomp (infixl "o\<rightarrow>" 60)
   8.234 +
   8.235 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Random.thy	Sat May 16 20:16:49 2009 +0200
     9.3 @@ -0,0 +1,177 @@
     9.4 +(* Author: Florian Haftmann, TU Muenchen *)
     9.5 +
     9.6 +header {* A HOL random engine *}
     9.7 +
     9.8 +theory Random
     9.9 +imports Code_Index
    9.10 +begin
    9.11 +
    9.12 +notation fcomp (infixl "o>" 60)
    9.13 +notation scomp (infixl "o\<rightarrow>" 60)
    9.14 +
    9.15 +
    9.16 +subsection {* Auxiliary functions *}
    9.17 +
    9.18 +definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
    9.19 +  "inc_shift v k = (if v = k then 1 else k + 1)"
    9.20 +
    9.21 +definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
    9.22 +  "minus_shift r k l = (if k < l then r + k - l else k - l)"
    9.23 +
    9.24 +fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
    9.25 +  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    9.26 +
    9.27 +
    9.28 +subsection {* Random seeds *}
    9.29 +
    9.30 +types seed = "index \<times> index"
    9.31 +
    9.32 +primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
    9.33 +  "next (v, w) = (let
    9.34 +     k =  v div 53668;
    9.35 +     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
    9.36 +     l =  w div 52774;
    9.37 +     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
    9.38 +     z =  minus_shift 2147483562 v' (w' + 1) + 1
    9.39 +   in (z, (v', w')))"
    9.40 +
    9.41 +lemma next_not_0:
    9.42 +  "fst (next s) \<noteq> 0"
    9.43 +  by (cases s) (auto simp add: minus_shift_def Let_def)
    9.44 +
    9.45 +primrec seed_invariant :: "seed \<Rightarrow> bool" where
    9.46 +  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
    9.47 +
    9.48 +lemma if_same: "(if b then f x else f y) = f (if b then x else y)"
    9.49 +  by (cases b) simp_all
    9.50 +
    9.51 +definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
    9.52 +  "split_seed s = (let
    9.53 +     (v, w) = s;
    9.54 +     (v', w') = snd (next s);
    9.55 +     v'' = inc_shift 2147483562 v;
    9.56 +     s'' = (v'', w');
    9.57 +     w'' = inc_shift 2147483398 w;
    9.58 +     s''' = (v', w'')
    9.59 +   in (s'', s'''))"
    9.60 +
    9.61 +
    9.62 +subsection {* Base selectors *}
    9.63 +
    9.64 +fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    9.65 +  "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
    9.66 +
    9.67 +definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
    9.68 +  "range k = iterate (log 2147483561 k)
    9.69 +      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
    9.70 +    o\<rightarrow> (\<lambda>v. Pair (v mod k))"
    9.71 +
    9.72 +lemma range:
    9.73 +  "k > 0 \<Longrightarrow> fst (range k s) < k"
    9.74 +  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
    9.75 +
    9.76 +definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    9.77 +  "select xs = range (Code_Index.of_nat (length xs))
    9.78 +    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
    9.79 +     
    9.80 +lemma select:
    9.81 +  assumes "xs \<noteq> []"
    9.82 +  shows "fst (select xs s) \<in> set xs"
    9.83 +proof -
    9.84 +  from assms have "Code_Index.of_nat (length xs) > 0" by simp
    9.85 +  with range have
    9.86 +    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
    9.87 +  then have
    9.88 +    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
    9.89 +  then show ?thesis
    9.90 +    by (simp add: scomp_apply split_beta select_def)
    9.91 +qed
    9.92 +
    9.93 +primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
    9.94 +  "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
    9.95 +
    9.96 +lemma pick_member:
    9.97 +  "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
    9.98 +  by (induct xs arbitrary: i) simp_all
    9.99 +
   9.100 +lemma pick_drop_zero:
   9.101 +  "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
   9.102 +  by (induct xs) (auto simp add: expand_fun_eq)
   9.103 +
   9.104 +definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   9.105 +  "select_weight xs = range (listsum (map fst xs))
   9.106 +   o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
   9.107 +
   9.108 +lemma select_weight_member:
   9.109 +  assumes "0 < listsum (map fst xs)"
   9.110 +  shows "fst (select_weight xs s) \<in> set (map snd xs)"
   9.111 +proof -
   9.112 +  from range assms
   9.113 +    have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
   9.114 +  with pick_member
   9.115 +    have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
   9.116 +  then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
   9.117 +qed
   9.118 +
   9.119 +definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   9.120 +  [code del]: "select_default k x y = range k
   9.121 +     o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
   9.122 +
   9.123 +lemma select_default_zero:
   9.124 +  "fst (select_default 0 x y s) = y"
   9.125 +  by (simp add: scomp_apply split_beta select_default_def)
   9.126 +
   9.127 +lemma select_default_code [code]:
   9.128 +  "select_default k x y = (if k = 0
   9.129 +    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
   9.130 +    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
   9.131 +proof
   9.132 +  fix s
   9.133 +  have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
   9.134 +    by (simp add: range_def scomp_Pair scomp_apply split_beta)
   9.135 +  then show "select_default k x y s = (if k = 0
   9.136 +    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
   9.137 +    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
   9.138 +    by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
   9.139 +qed
   9.140 +
   9.141 +
   9.142 +subsection {* @{text ML} interface *}
   9.143 +
   9.144 +ML {*
   9.145 +structure Random_Engine =
   9.146 +struct
   9.147 +
   9.148 +type seed = int * int;
   9.149 +
   9.150 +local
   9.151 +
   9.152 +val seed = ref 
   9.153 +  (let
   9.154 +    val now = Time.toMilliseconds (Time.now ());
   9.155 +    val (q, s1) = IntInf.divMod (now, 2147483562);
   9.156 +    val s2 = q mod 2147483398;
   9.157 +  in (s1 + 1, s2 + 1) end);
   9.158 +
   9.159 +in
   9.160 +
   9.161 +fun run f =
   9.162 +  let
   9.163 +    val (x, seed') = f (! seed);
   9.164 +    val _ = seed := seed'
   9.165 +  in x end;
   9.166 +
   9.167 +end;
   9.168 +
   9.169 +end;
   9.170 +*}
   9.171 +
   9.172 +hide (open) type seed
   9.173 +hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
   9.174 +  iterate range select pick select_weight select_default
   9.175 +
   9.176 +no_notation fcomp (infixl "o>" 60)
   9.177 +no_notation scomp (infixl "o\<rightarrow>" 60)
   9.178 +
   9.179 +end
   9.180 +