# HG changeset patch
# User haftmann
# Date 1233004457 -3600
# Node ID 199e2fb7f588a986e6792fce96ca97bb374fd379
# Parent  5111ce425e7a4fd3a3bcec0c9043ca02e6064d35
streamlined definitions, executable equality

diff -r 5111ce425e7a -r 199e2fb7f588 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Jan 26 22:14:17 2009 +0100
+++ b/src/HOL/Word/WordDefinition.thy	Mon Jan 26 22:14:17 2009 +0100
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Jeremy Dawson and Gerwin Klein, NICTA
   
   Basic definition of word type and basic theorems following from 
@@ -12,8 +11,50 @@
 imports Size BinBoolList TdThs
 begin
 
-typedef (open word) 'a word
-  = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
+subsection {* Type definition *}
+
+typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
+  morphisms uint Abs_word by auto
+
+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)" 
+
+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
+
+
+subsection {* Type conversions and casting *}
+
+definition sint :: "'a :: len word => int" where
+  -- {* treats the most-significant-bit as a sign bit *}
+  sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
+
+definition unat :: "'a :: len0 word => nat" where
+  "unat w = nat (uint w)"
+
+definition uints :: "nat => int set" where
+  -- "the sets of integers representing the words"
+  "uints n = range (bintrunc n)"
+
+definition sints :: "nat => int set" where
+  "sints n = range (sbintrunc (n - 1))"
+
+definition unats :: "nat => nat set" where
+  "unats n = {i. i < 2 ^ n}"
+
+definition norm_sint :: "nat => int => int" where
+  "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
+
+definition scast :: "'a :: len word => 'b :: len word" where
+  -- "cast a word to a different length"
+  "scast w = word_of_int (sint w)"
+
+definition ucast :: "'a :: len0 word => 'b :: len0 word" where
+  "ucast w = word_of_int (uint w)"
 
 instantiation word :: (len0) size
 begin
@@ -25,83 +66,39 @@
 
 end
 
-definition
-  -- {* representation of words using unsigned or signed bins, 
-        only difference in these is the type class *}
-  word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
-where
-  [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
-
-code_datatype word_of_int
-
+definition source_size :: "('a :: len0 word => 'b) => nat" where
+  -- "whether a cast (or other) function is to a longer or shorter length"
+  "source_size c = (let arb = undefined ; x = c arb in size arb)"  
 
-subsection "Type conversions and casting"
+definition target_size :: "('a => 'b :: len0 word) => nat" where
+  "target_size c = size (c undefined)"
 
-constdefs
-  -- {* uint and sint cast a word to an integer,
-        uint treats the word as unsigned,
-        sint treats the most-significant-bit as a sign bit *}
-  uint :: "'a :: len0 word => int"
-  "uint w == Rep_word w"
-  sint :: "'a :: len word => int"
-  sint_uint: "sint w == sbintrunc (len_of TYPE ('a) - 1) (uint w)"
-  unat :: "'a :: len0 word => nat"
-  "unat w == nat (uint w)"
+definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool" where
+  "is_up c \<longleftrightarrow> source_size c <= target_size c"
 
-  -- "the sets of integers representing the words"
-  uints :: "nat => int set"
-  "uints n == range (bintrunc n)"
-  sints :: "nat => int set"
-  "sints n == range (sbintrunc (n - 1))"
-  unats :: "nat => nat set"
-  "unats n == {i. i < 2 ^ n}"
-  norm_sint :: "nat => int => int"
-  "norm_sint n w == (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
+definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool" where
+  "is_down c \<longleftrightarrow> target_size c <= source_size c"
 
-  -- "cast a word to a different length"
-  scast :: "'a :: len word => 'b :: len word"
-  "scast w == word_of_int (sint w)"
-  ucast :: "'a :: len0 word => 'b :: len0 word"
-  "ucast w == word_of_int (uint w)"
+definition of_bl :: "bool list => 'a :: len0 word" where
+  "of_bl bl = word_of_int (bl_to_bin bl)"
 
-  -- "whether a cast (or other) function is to a longer or shorter length"
-  source_size :: "('a :: len0 word => 'b) => nat"
-  "source_size c == let arb = undefined ; x = c arb in size arb"  
-  target_size :: "('a => 'b :: len0 word) => nat"
-  "target_size c == size (c undefined)"
-  is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
-  "is_up c == source_size c <= target_size c"
-  is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
-  "is_down c == target_size c <= source_size c"
+definition to_bl :: "'a :: len0 word => bool list" where
+  "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
 
-constdefs
-  of_bl :: "bool list => 'a :: len0 word" 
-  "of_bl bl == word_of_int (bl_to_bin bl)"
-  to_bl :: "'a :: len0 word => bool list"
-  "to_bl w == 
-  bin_to_bl (len_of TYPE ('a)) (uint w)"
+definition word_reverse :: "'a :: len0 word => 'a word" where
+  "word_reverse w = of_bl (rev (to_bl w))"
 
-  word_reverse :: "'a :: len0 word => 'a word"
-  "word_reverse w == of_bl (rev (to_bl w))"
-
-constdefs
-  word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b"
-  "word_int_case f w == f (uint w)"
+definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
+  "word_int_case f w = f (uint w)"
 
 syntax
   of_int :: "int => 'a"
 translations
-  "case x of of_int y => b" == "word_int_case (%y. b) x"
+  "case x of of_int y => b" == "CONST word_int_case (%y. b) x"
 
 
 subsection  "Arithmetic operations"
 
-declare uint_def [code del]
-
-lemma [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
-  by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse)
-    (insert range_bintrunc, auto)
-
 instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
 begin
 
@@ -186,8 +183,6 @@
 
 subsection "Bit-wise operations"
 
-
-
 instantiation word :: (len0) bits
 begin
 
@@ -337,21 +332,21 @@
   unfolding atLeastLessThan_alt by auto
 
 lemma 
-  Rep_word_0:"0 <= Rep_word x" and 
-  Rep_word_lt: "Rep_word (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
-  by (auto simp: Rep_word [simplified])
+  uint_0:"0 <= uint x" and 
+  uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
+  by (auto simp: uint [simplified])
 
-lemma Rep_word_mod_same:
-  "Rep_word x mod 2 ^ len_of TYPE('a) = Rep_word (x::'a::len0 word)"
-  by (simp add: int_mod_eq Rep_word_lt Rep_word_0)
+lemma uint_mod_same:
+  "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
+  by (simp add: int_mod_eq uint_lt uint_0)
 
 lemma td_ext_uint: 
   "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0))) 
     (%w::int. w mod 2 ^ len_of TYPE('a))"
   apply (unfold td_ext_def')
-  apply (simp add: uints_num uint_def word_of_int_def bintrunc_mod2p)
-  apply (simp add: Rep_word_mod_same Rep_word_0 Rep_word_lt
-                   word.Rep_word_inverse word.Abs_word_inverse int_mod_lem)
+  apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
+  apply (simp add: uint_mod_same uint_0 uint_lt
+                   word.uint_inverse word.Abs_word_inverse int_mod_lem)
   done
 
 lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
@@ -793,10 +788,7 @@
 lemmas is_down = is_down_def [unfolded source_size target_size]
 lemmas is_up = is_up_def [unfolded source_size target_size]
 
-lemmas is_up_down = 
-  trans [OF is_up [THEN meta_eq_to_obj_eq] 
-            is_down [THEN meta_eq_to_obj_eq, symmetric], 
-         standard]
+lemmas is_up_down =  trans [OF is_up is_down [symmetric], standard]
 
 lemma down_cast_same': "uc = ucast ==> is_down uc ==> uc = scast"
   apply (unfold is_down)
@@ -950,4 +942,17 @@
 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
 lemmas word_log_bin_defs = word_log_defs
 
+text {* Executable equality *}
+
+instantiation word :: ("{len0}") eq
+begin
+
+definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+  "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
+
+instance proof
+qed (simp add: eq eq_word_def)
+
 end
+
+end