# HG changeset patch
# User haftmann
# Date 1275376332 -7200
# Node ID 7c5311e54ea40e55ef61ad9416c3fe104beba589
# Parent  ffd587207d5d6211d2d38ee4eed2d7e9a0e347a8
added random instance for word

diff -r ffd587207d5d -r 7c5311e54ea4 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon May 31 22:08:40 2010 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Jun 01 09:12:12 2010 +0200
@@ -19,13 +19,31 @@
 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
   -- {* representation of words using unsigned or signed bins, 
         only difference in these is the type class *}
-  [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
+  "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
 
 lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)"
   by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse)
 
 code_datatype word_of_int
 
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation word :: ("{len0, typerep}") random
+begin
+
+definition
+  "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\<rightarrow> (\<lambda>k. Pair (
+     let j = word_of_int (Code_Numeral.int_of k) :: 'a word
+     in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
 
 subsection {* Type conversions and casting *}