merged
authorhaftmann
Tue, 01 Jun 2010 11:18:51 +0200
changeset 37225 32c5251f78cd
parent 37219 7c5311e54ea4 (diff)
parent 37224 f4d3c929c526 (current diff)
child 37226 7c59ab0a419b
child 37236 739d8b9c59da
child 37242 97097e589715
merged
--- a/src/HOL/Word/WordDefinition.thy	Tue Jun 01 10:30:54 2010 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Jun 01 11:18:51 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 *}