# HG changeset patch
# User huffman
# Date 1228924374 28800
# Node ID 3c8f483337319b70b4d75881300169e65eb76831
# Parent  9dbf8249d979a67aac1e79a481b3819323264057
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs

diff -r 9dbf8249d979 -r 3c8f48333731 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Dec 10 06:34:10 2008 -0800
+++ b/src/HOL/IntDiv.thy	Wed Dec 10 07:52:54 2008 -0800
@@ -1472,6 +1472,29 @@
   IntDiv.zpower_zmod
   zminus_zmod zdiff_zmod_left zdiff_zmod_right
 
+text {* Distributive laws for function @{text nat}. *}
+
+lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
+apply (rule linorder_cases [of y 0])
+apply (simp add: div_nonneg_neg_le0)
+apply simp
+apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
+done
+
+(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
+lemma nat_mod_distrib:
+  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
+apply (case_tac "y = 0", simp add: DIVISION_BY_ZERO)
+apply (simp add: nat_eq_iff zmod_int)
+done
+
+text{*Suggested by Matthias Daum*}
+lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
+apply (subgoal_tac "nat x div nat k < nat x")
+ apply (simp (asm_lr) add: nat_div_distrib [symmetric])
+apply (rule Divides.div_less_dividend, simp_all)
+done
+
 text {* code generator setup *}
 
 context ring_1
diff -r 9dbf8249d979 -r 3c8f48333731 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Wed Dec 10 06:34:10 2008 -0800
+++ b/src/HOL/NatBin.thy	Wed Dec 10 07:52:54 2008 -0800
@@ -118,52 +118,8 @@
 done
 
 
-text{*Distributive laws for type @{text nat}.  The others are in theory
-   @{text IntArith}, but these require div and mod to be defined for type
-   "int".  They also need some of the lemmas proved above.*}
-
-lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
-apply (case_tac "0 <= z'")
-apply (auto simp add: div_nonneg_neg_le0)
-apply (case_tac "z' = 0", simp)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m div int m'")
- prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
-apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac r = "int (m mod m') " in quorem_div)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-done
-
-(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib:
-     "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
-apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m mod int m'")
- prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
-apply (rule int_int_eq [THEN iffD1], simp)
-apply (rule_tac q = "int (m div m') " in quorem_mod)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-done
-
-text{*Suggested by Matthias Daum*}
-lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x")
- apply (simp (asm_lr) add: nat_div_distrib [symmetric])
-apply (rule Divides.div_less_dividend, simp_all) 
-done
-
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma int_nat_number_of [simp]:
      "int (number_of v) =  
          (if neg (number_of v :: int) then 0  
@@ -195,7 +151,6 @@
 
 subsubsection{*Addition *}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma add_nat_number_of [simp]:
      "(number_of v :: nat) + number_of v' =  
          (if v < Int.Pls then number_of v'  
@@ -303,7 +258,6 @@
      "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
 by (auto elim!: nonneg_eq_int)
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma eq_nat_number_of [simp]:
      "((number_of v :: nat) = number_of v') =  
       (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0