# HG changeset patch
# User huffman
# Date 1321536250 -3600
# Node ID 26aebb8ac9c11de7bf19cf324abbf663b9adabf6
# Parent  c0304794e9e49a5c2aacaf98bb01c048f0097ed4
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations

diff -r c0304794e9e4 -r 26aebb8ac9c1 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Nov 17 12:38:03 2011 +0100
+++ b/src/HOL/Word/Word.thy	Thu Nov 17 14:24:10 2011 +0100
@@ -30,6 +30,8 @@
 
 code_datatype word_of_int
 
+subsection {* Random instance *}
+
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
@@ -118,10 +120,86 @@
 translations
   "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
 
+subsection {* Type-definition locale instantiations *}
+
+lemmas word_size_gt_0 [iff] = 
+  xtr1 [OF word_size len_gt_0, standard]
+lemmas lens_gt_0 = word_size_gt_0 len_gt_0
+lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
+
+lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
+  by (simp add: uints_def range_bintrunc)
+
+lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
+  by (simp add: sints_def range_sbintrunc)
+
+lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded 
+  atLeast_def lessThan_def Collect_conj_eq [symmetric]]
+  
+lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
+  unfolding atLeastLessThan_alt by auto
+
+lemma 
+  uint_0:"0 <= uint x" and 
+  uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
+  by (auto simp: uint [simplified])
+
+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 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]
+
+interpretation word_uint:
+  td_ext "uint::'a::len0 word \<Rightarrow> int" 
+         word_of_int 
+         "uints (len_of TYPE('a::len0))"
+         "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
+  by (rule td_ext_uint)
+  
+lemmas td_uint = word_uint.td_thm
+
+lemmas td_ext_ubin = td_ext_uint 
+  [simplified len_gt_0 no_bintr_alt1 [symmetric]]
+
+interpretation word_ubin:
+  td_ext "uint::'a::len0 word \<Rightarrow> int" 
+         word_of_int 
+         "uints (len_of TYPE('a::len0))"
+         "bintrunc (len_of TYPE('a::len0))"
+  by (rule td_ext_ubin)
+
+lemma split_word_all:
+  "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
+proof
+  fix x :: "'a word"
+  assume "\<And>x. PROP P (word_of_int x)"
+  hence "PROP P (word_of_int (uint x))" .
+  thus "PROP P x" by simp
+qed
 
 subsection  "Arithmetic operations"
 
-instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord}"
+definition
+  word_succ :: "'a :: len0 word => 'a word"
+where
+  "word_succ a = word_of_int (Int.succ (uint a))"
+
+definition
+  word_pred :: "'a :: len0 word => 'a word"
+where
+  "word_pred a = word_of_int (Int.pred (uint a))"
+
+instantiation word :: (len0) "{number, Divides.div, ord, comm_monoid_mult, comm_ring}"
 begin
 
 definition
@@ -157,19 +235,83 @@
 definition
   word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
 
-instance ..
+lemmas word_arith_wis = 
+  word_add_def word_mult_def word_minus_def 
+  word_succ_def word_pred_def word_0_wi word_1_wi
+
+lemmas arths = 
+  bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
+                folded word_ubin.eq_norm, standard]
+
+lemma wi_homs: 
+  shows
+  wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
+  wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
+  wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
+  wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
+  wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
+  by (auto simp: word_arith_wis arths)
+
+lemmas wi_hom_syms = wi_homs [symmetric]
+
+lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
+  unfolding word_sub_wi diff_minus
+  by (simp only : word_uint.Rep_inverse wi_hom_syms)
+    
+lemmas word_diff_minus = word_sub_def [standard]
+
+lemma word_of_int_sub_hom:
+  "(word_of_int a) - word_of_int b = word_of_int (a - b)"
+  unfolding word_sub_def diff_minus by (simp only : wi_homs)
+
+lemmas new_word_of_int_homs = 
+  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
+
+lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
+
+lemmas word_of_int_hom_syms =
+  new_word_of_int_hom_syms [unfolded succ_def pred_def]
+
+lemmas word_of_int_homs =
+  new_word_of_int_homs [unfolded succ_def pred_def]
+
+lemmas word_of_int_add_hom = word_of_int_homs (2)
+lemmas word_of_int_mult_hom = word_of_int_homs (3)
+lemmas word_of_int_minus_hom = word_of_int_homs (4)
+lemmas word_of_int_succ_hom = word_of_int_homs (5)
+lemmas word_of_int_pred_hom = word_of_int_homs (6)
+lemmas word_of_int_0_hom = word_of_int_homs (7)
+lemmas word_of_int_1_hom = word_of_int_homs (8)
+
+instance
+  by default (auto simp: split_word_all word_of_int_homs algebra_simps)
 
 end
 
-definition
-  word_succ :: "'a :: len0 word => 'a word"
-where
-  "word_succ a = word_of_int (Int.succ (uint a))"
-
-definition
-  word_pred :: "'a :: len0 word => 'a word"
-where
-  "word_pred a = word_of_int (Int.pred (uint a))"
+lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
+  unfolding word_arith_wis
+  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
+
+lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
+
+instance word :: (len) comm_ring_1
+  by (intro_classes) (simp add: lenw1_zero_neq_one)
+
+lemma word_of_nat: "of_nat n = word_of_int (int n)"
+  by (induct n) (auto simp add : word_of_int_hom_syms)
+
+lemma word_of_int: "of_int = word_of_int"
+  apply (rule ext)
+  apply (case_tac x rule: int_diff_cases)
+  apply (simp add: word_of_nat word_of_int_sub_hom)
+  done
+
+lemma word_number_of_eq: 
+  "number_of w = (of_int w :: 'a :: len word)"
+  unfolding word_number_of_def word_of_int by auto
+
+instance word :: (len) number_ring
+  by (intro_classes) (simp add : word_number_of_eq)
 
 definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
   "a udvd b = (EX n>=0. uint b = n * uint a)"
@@ -181,7 +323,6 @@
   "(x <s y) = (x <=s y & x ~= y)"
 
 
-
 subsection "Bit-wise operations"
 
 instantiation word :: (len0) bits
@@ -327,62 +468,6 @@
 
 lemmas of_nth_def = word_set_bits_def
 
-lemmas word_size_gt_0 [iff] = 
-  xtr1 [OF word_size len_gt_0, standard]
-lemmas lens_gt_0 = word_size_gt_0 len_gt_0
-lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
-
-lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
-  by (simp add: uints_def range_bintrunc)
-
-lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
-  by (simp add: sints_def range_sbintrunc)
-
-lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded 
-  atLeast_def lessThan_def Collect_conj_eq [symmetric]]
-  
-lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
-  unfolding atLeastLessThan_alt by auto
-
-lemma 
-  uint_0:"0 <= uint x" and 
-  uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
-  by (auto simp: uint [simplified])
-
-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 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]
-
-interpretation word_uint:
-  td_ext "uint::'a::len0 word \<Rightarrow> int" 
-         word_of_int 
-         "uints (len_of TYPE('a::len0))"
-         "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
-  by (rule td_ext_uint)
-  
-lemmas td_uint = word_uint.td_thm
-
-lemmas td_ext_ubin = td_ext_uint 
-  [simplified len_gt_0 no_bintr_alt1 [symmetric]]
-
-interpretation word_ubin:
-  td_ext "uint::'a::len0 word \<Rightarrow> int" 
-         word_of_int 
-         "uints (len_of TYPE('a::len0))"
-         "bintrunc (len_of TYPE('a::len0))"
-  by (rule td_ext_ubin)
-
 lemma sint_sbintrunc': 
   "sint (word_of_int bin :: 'a word) = 
     (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
@@ -984,10 +1069,6 @@
 interpretation signed: linorder "word_sle" "word_sless"
   by (rule signed_linorder)
 
-lemmas word_arith_wis = 
-  word_add_def word_mult_def word_minus_def 
-  word_succ_def word_pred_def word_0_wi word_1_wi
-
 lemma udvdI: 
   "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
   by (auto simp: udvd_def)
@@ -1116,59 +1197,13 @@
   unfolding ucast_def word_1_wi
   by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
 
-(* abstraction preserves the operations
-  (the definitions tell this for bins in range uint) *)
-
-lemmas arths = 
-  bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
-                folded word_ubin.eq_norm, standard]
-
-lemma wi_homs: 
-  shows
-  wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
-  wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
-  wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
-  wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
-  wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
-  by (auto simp: word_arith_wis arths)
-
-lemmas wi_hom_syms = wi_homs [symmetric]
-
-lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
-  unfolding word_sub_wi diff_minus
-  by (simp only : word_uint.Rep_inverse wi_hom_syms)
-    
-lemmas word_diff_minus = word_sub_def [standard]
-
-lemma word_of_int_sub_hom:
-  "(word_of_int a) - word_of_int b = word_of_int (a - b)"
-  unfolding word_sub_def diff_minus by (simp only : wi_homs)
-
-lemmas new_word_of_int_homs = 
-  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
-
-lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
-
-lemmas word_of_int_hom_syms =
-  new_word_of_int_hom_syms [unfolded succ_def pred_def]
-
-lemmas word_of_int_homs =
-  new_word_of_int_homs [unfolded succ_def pred_def]
-
-lemmas word_of_int_add_hom = word_of_int_homs (2)
-lemmas word_of_int_mult_hom = word_of_int_homs (3)
-lemmas word_of_int_minus_hom = word_of_int_homs (4)
-lemmas word_of_int_succ_hom = word_of_int_homs (5)
-lemmas word_of_int_pred_hom = word_of_int_homs (6)
-lemmas word_of_int_0_hom = word_of_int_homs (7)
-lemmas word_of_int_1_hom = word_of_int_homs (8)
-
 (* now, to get the weaker results analogous to word_div/mod_def *)
 
 lemmas word_arith_alts = 
   word_sub_wi [unfolded succ_def pred_def, standard]
   word_arith_wis [unfolded succ_def pred_def, standard]
 
+(* FIXME: Lots of duplicate lemmas *)
 lemmas word_sub_alt = word_arith_alts (1)
 lemmas word_add_alt = word_arith_alts (2)
 lemmas word_mult_alt = word_arith_alts (3)
@@ -1234,6 +1269,7 @@
   "\<exists>y. x = word_of_int y"
   by (rule_tac x="uint x" in exI) simp
 
+(* FIXME: redundant theorems *)
 lemma word_arith_eqs:
   fixes a :: "'a::len0 word"
   fixes b :: "'a::len0 word"
@@ -1287,17 +1323,9 @@
   "0 <= (y :: 'a :: len0 word)"
   unfolding word_le_def by auto
   
-instance word :: (len0) semigroup_add
-  by intro_classes (simp add: word_add_assoc)
-
 instance word :: (len0) linorder
   by intro_classes (auto simp: word_less_def word_le_def)
 
-instance word :: (len0) ring
-  by intro_classes
-     (auto simp: word_arith_eqs word_diff_minus 
-                 word_diff_self [unfolded word_diff_minus])
-
 lemma word_m1_ge [simp] : "word_pred 0 >= y"
   unfolding word_le_def
   by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
@@ -1352,12 +1380,6 @@
 
 lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
 
-lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
-  unfolding word_arith_wis
-  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
-
-lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
-
 lemma no_no [simp] : "number_of (number_of b) = number_of b"
   by (simp add: number_of_eq)
 
@@ -1727,30 +1749,6 @@
 
 subsection "Arithmetic type class instantiations"
 
-instance word :: (len0) comm_monoid_add ..
-
-instance word :: (len0) comm_monoid_mult
-  apply (intro_classes)
-   apply (simp add: word_mult_commute)
-  apply (simp add: word_mult_1)
-  done
-
-instance word :: (len0) comm_semiring 
-  by (intro_classes) (simp add : word_left_distrib)
-
-instance word :: (len0) ab_group_add ..
-
-instance word :: (len0) comm_ring ..
-
-instance word :: (len) comm_semiring_1 
-  by (intro_classes) (simp add: lenw1_zero_neq_one)
-
-instance word :: (len) comm_ring_1 ..
-
-instance word :: (len0) comm_semiring_0 ..
-
-instance word :: (len0) order ..
-
 (* note that iszero_def is only for class comm_semiring_1_cancel,
    which requires word length >= 1, ie 'a :: len word *) 
 lemma zero_bintrunc:
@@ -1764,26 +1762,10 @@
 lemmas word_le_0_iff [simp] =
   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
 
-lemma word_of_nat: "of_nat n = word_of_int (int n)"
-  by (induct n) (auto simp add : word_of_int_hom_syms)
-
-lemma word_of_int: "of_int = word_of_int"
-  apply (rule ext)
-  apply (case_tac x rule: int_diff_cases)
-  apply (simp add: word_of_nat word_of_int_sub_hom)
-  done
-
 lemma word_of_int_nat: 
   "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   by (simp add: of_nat_nat word_of_int)
 
-lemma word_number_of_eq: 
-  "number_of w = (of_int w :: 'a :: len word)"
-  unfolding word_number_of_def word_of_int by auto
-
-instance word :: (len) number_ring
-  by (intro_classes) (simp add : word_number_of_eq)
-
 lemma iszero_word_no [simp] : 
   "iszero (number_of bin :: 'a :: len word) = 
     iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"