# HG changeset patch
# User huffman
# Date 1187659023 -7200
# Node ID af83eeb4a702514575c6b664206a93f09300759a
# Parent  223622422d7b32645aed816413f21787a99b8845
move udvd, div and mod stuff from WordDefinition to WordArith

diff -r 223622422d7b -r af83eeb4a702 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Tue Aug 21 03:02:27 2007 +0200
+++ b/src/HOL/Word/WordArith.thy	Tue Aug 21 03:17:03 2007 +0200
@@ -11,21 +11,10 @@
 
 theory WordArith imports WordDefinition begin
 
-
 lemmas word_arith_wis [THEN meta_eq_to_obj_eq] = 
   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 ==> uint b = n * uint a ==> a udvd b"
-  by (auto simp: udvd_def)
-
-lemmas word_div_no [simp] = 
-  word_div_def [of "number_of ?a" "number_of ?b"]
-
-lemmas word_mod_no [simp] = 
-  word_mod_def [of "number_of ?a" "number_of ?b"]
-
 (* following two are available in class number_ring, 
   but convenient to have them here here;
   note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1
@@ -221,11 +210,6 @@
   unfolded uint_sint bintr_arith1s bintr_ariths 
     len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
 
-lemmas uint_div_alt = word_div_def
-  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
-lemmas uint_mod_alt = word_mod_def
-  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
-
 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
   unfolding word_pred_def number_of_eq
   by (simp add : pred_def word_no_wi)
@@ -392,6 +376,14 @@
 
 subsection "Divisibility"
 
+definition
+  udvd :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" (infixl "udvd" 50) where
+  "a udvd b \<equiv> \<exists>n\<ge>0. uint b = n * uint a"
+
+lemma udvdI: 
+  "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
+  by (auto simp: udvd_def)
+
 lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
   apply (unfold udvd_def)
   apply safe
@@ -408,6 +400,26 @@
 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
   unfolding dvd_def udvd_nat_alt by force
 
+
+subsection "Division with remainder"
+
+instance word :: (len0) Divides.div
+  word_div_def: "a div b == word_of_int (uint a div uint b)"
+  word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
+  ..
+
+lemmas word_div_no [simp] = 
+  word_div_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_mod_no [simp] = 
+  word_mod_def [of "number_of ?a" "number_of ?b"]
+
+lemmas uint_div_alt = word_div_def
+  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
+lemmas uint_mod_alt = word_mod_def
+  [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
+
+
 lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
   unfolding word_arith_wis
   by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
diff -r 223622422d7b -r af83eeb4a702 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Tue Aug 21 03:02:27 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Aug 21 03:17:03 2007 +0200
@@ -19,7 +19,6 @@
 instance word :: (type) one ..
 instance word :: (type) zero ..
 instance word :: (type) times ..
-instance word :: (type) Divides.div ..
 instance word :: (type) power ..
 instance word :: (type) size ..
 instance word :: (type) inverse ..
@@ -91,9 +90,6 @@
   word_pred :: "'a :: len0 word => 'a word"
   "word_pred a == word_of_int (Numeral.pred (uint a))"
 
-  udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
-  "a udvd b == EX n>=0. uint b = n * uint a"
-
 consts
   word_power :: "'a :: len0 word => nat => 'a word"
 primrec
@@ -106,8 +102,6 @@
   word_sub_wi: "a - b == word_of_int (uint a - uint b)"
   word_minus_def: "- a == word_of_int (- uint a)"
   word_mult_def: "a * b == word_of_int (uint a * uint b)"
-  word_div_def: "a div b == word_of_int (uint a div uint b)"
-  word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
 
 
 subsection "Bit-wise operations"