# HG changeset patch # User paulson # Date 1022840844 -7200 # Node ID d5234c261813b29a6884ac06b2adda126e4da9ab # Parent e961c197f141439ce1ba22aeca6a36a80a9de1ed finished an incomplete proof diff -r e961c197f141 -r d5234c261813 src/HOL/NumberTheory/IntPrimes.thy --- a/src/HOL/NumberTheory/IntPrimes.thy Fri May 31 12:22:21 2002 +0200 +++ b/src/HOL/NumberTheory/IntPrimes.thy Fri May 31 12:27:24 2002 +0200 @@ -663,14 +663,17 @@ lemma "[a = b] (mod m) = (a mod m = b mod m)" apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO) - apply (case_tac "0 < m") - apply (simp add: zcong_zmod_eq) + apply (simp add: linorder_neq_iff) + apply (erule disjE) + prefer 2 apply (simp add: zcong_zmod_eq) + txt{*Remainding case: @{term "m<0"}*} apply (rule_tac t = m in zminus_zminus [THEN subst]) apply (subst zcong_zminus) apply (subst zcong_zmod_eq) apply arith - oops -- {* FIXME: finish this proof? *} - + apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) + apply (simp add: zmod_zminus2_eq_if) + done subsection {* Modulo *}