# Theory Pdifference

```(*  Title:      RSAPSS/Pdifference.thy

Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)
section "Positive differences"

theory Pdifference
imports "HOL-Computational_Algebra.Primes" Mod
begin

definition
pdifference :: "nat ⇒ nat ⇒ nat" where
[simp]: "pdifference a b = (if a < b then (b-a) else (a-b))"

lemma timesdistributesoverpdifference:
"m*(pdifference a b) = pdifference (m*(a::nat)) (m* (b::nat))"

lemma addconst: "a = (b::nat) ⟹ c+a = c+b"
by auto

lemma invers: "a ≤ x ⟹ (x::nat) = x - a + a"
by auto

lemma invers2: "⟦a ≤ b; (b-a) = p*q⟧ ⟹ (b::nat) = a+p*q"
apply (assumption)
apply (subst add.commute, rule invers, simp)
done

lemma modadd: "⟦b = a+p*q⟧ ⟹ (a::nat) mod p = b mod p"
by auto

lemma equalmodstrick1: "pdifference a b mod p = 0 ⟹ a mod p = b mod p"
using mod_eq_dvd_iff_nat [of a b p] mod_eq_dvd_iff_nat [of b a p]
by (cases "a < b") auto

lemma diff_add_assoc: "b ≤ c ⟹ c - (c - b) = c - c + (b::nat)"
by auto

lemma diff_add_assoc2: "a ≤ c ⟹ c - (c - a + b) = (c - c + (a::nat) - b)"
apply (subst diff_diff_left [symmetric])
apply auto
done

lemma diff_add_diff: "x ≤ b ⟹ (b::nat) - x + y - b = y - x"
by (induct b) auto

lemma equalmodstrick2:
assumes "a mod p = b mod p"
shows "pdifference a b mod p = 0"
proof -
{ fix a b
assume *: "a mod p = b mod p"
have "a - b = a div p * p + a mod p - b div p * p - b mod p"
by simp
also have "… = a div p * p - b div p * p"
using * by (simp only:)
also have "… = (a div p - b div p) * p"
finally have "(a - b) mod p = 0"
by simp
}
from this [OF assms] this [OF assms [symmetric]]
show ?thesis by simp
qed

lemma primekeyrewrite:
fixes p::nat shows "⟦prime p; p dvd (a*b);~(p dvd a)⟧ ⟹ p dvd b"
apply (subst (asm) prime_dvd_mult_nat)
apply auto
done

lemma multzero: "⟦0 < m mod p; m*a = 0⟧ ⟹ (a::nat) = 0"
by auto

lemma primekeytrick:
fixes A B :: nat
assumes "(M * A) mod P = (M * B) mod P"
assumes "M mod P ≠ 0" and "prime P"
shows "A mod P = B mod P"
proof -
from assms have "M > 0"
by (auto intro: ccontr)
from assms have *: "⋀q. P dvd M * q ⟹ P dvd q"
using primekeyrewrite [of P M] unfolding dvd_eq_mod_eq_0 [symmetric] by blast
from equalmodstrick2 [OF assms(1)] ‹M > 0› show ?thesis
apply -
apply (rule equalmodstrick1)
apply (auto intro: * dvdI simp add: dvd_eq_mod_eq_0 [symmetric] diff_mult_distrib2 [symmetric])
done
qed

end

```