Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
authorchaieb
Mon Jul 21 13:36:44 2008 +0200 (2008-07-21)
changeset 2766762500b980749
parent 27666 1436d81d1294
child 27668 6eb20b2cecf8
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/IntDiv.thy	Mon Jul 21 13:36:39 2008 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Mon Jul 21 13:36:44 2008 +0200
     1.3 @@ -1513,6 +1513,51 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
     1.8 +proof
     1.9 +  assume H: "x mod n = y mod n"
    1.10 +  hence "x mod n - y mod n = 0" by simp
    1.11 +  hence "(x mod n - y mod n) mod n = 0" by simp 
    1.12 +  hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
    1.13 +  thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
    1.14 +next
    1.15 +  assume H: "n dvd x - y"
    1.16 +  then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
    1.17 +  hence "x = n*k + y" by simp
    1.18 +  hence "x mod n = (n*k + y) mod n" by simp
    1.19 +  thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
    1.20 +qed
    1.21 +
    1.22 +lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
    1.23 +  shows "\<exists>q. x = y + n * q"
    1.24 +proof-
    1.25 +  from xy have th: "int x - int y = int (x - y)" by simp 
    1.26 +  from xyn have "int x mod int n = int y mod int n" 
    1.27 +    by (simp add: zmod_int[symmetric])
    1.28 +  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
    1.29 +  hence "n dvd x - y" by (simp add: th zdvd_int)
    1.30 +  then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
    1.31 +qed
    1.32 +
    1.33 +lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
    1.34 +  (is "?lhs = ?rhs")
    1.35 +proof
    1.36 +  assume H: "x mod n = y mod n"
    1.37 +  {assume xy: "x \<le> y"
    1.38 +    from H have th: "y mod n = x mod n" by simp
    1.39 +    from nat_mod_eq_lemma[OF th xy] have ?rhs 
    1.40 +      apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
    1.41 +  moreover
    1.42 +  {assume xy: "y \<le> x"
    1.43 +    from nat_mod_eq_lemma[OF H xy] have ?rhs 
    1.44 +      apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
    1.45 +  ultimately  show ?rhs using linear[of x y] by blast  
    1.46 +next
    1.47 +  assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
    1.48 +  hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
    1.49 +  thus  ?lhs by simp
    1.50 +qed
    1.51 +
    1.52  code_modulename SML
    1.53    IntDiv Integer
    1.54