src/HOL/Number_Theory/Cong.thy
changeset 36350 bc7982c54e37
parent 35644 d20cf282342e
child 37293 2c9ed7478e6e
equal deleted inserted replaced
36349:39be26d1bc28 36350:bc7982c54e37
   348     \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   348     \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   349   apply (simp only: cong_altdef_int)
   349   apply (simp only: cong_altdef_int)
   350   apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
   350   apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
   351   (* any way around this? *)
   351   (* any way around this? *)
   352   apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
   352   apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
   353   apply (auto simp add: ring_simps)
   353   apply (auto simp add: field_simps)
   354 done
   354 done
   355 
   355 
   356 lemma cong_mult_rcancel_int:
   356 lemma cong_mult_rcancel_int:
   357   "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
   357   "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
   358   apply (subst (1 2) cong_altdef_int)
   358   apply (subst (1 2) cong_altdef_int)
   414   apply (rule_tac x = "a mod m" in exI)
   414   apply (rule_tac x = "a mod m" in exI)
   415   apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
   415   apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
   416 done
   416 done
   417 
   417 
   418 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
   418 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
   419   apply (auto simp add: cong_altdef_int dvd_def ring_simps)
   419   apply (auto simp add: cong_altdef_int dvd_def field_simps)
   420   apply (rule_tac [!] x = "-k" in exI, auto)
   420   apply (rule_tac [!] x = "-k" in exI, auto)
   421 done
   421 done
   422 
   422 
   423 lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = 
   423 lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = 
   424     (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   424     (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   426   apply (case_tac "b <= a")
   426   apply (case_tac "b <= a")
   427   apply (subst (asm) cong_altdef_nat, assumption)
   427   apply (subst (asm) cong_altdef_nat, assumption)
   428   apply (unfold dvd_def, auto)
   428   apply (unfold dvd_def, auto)
   429   apply (rule_tac x = k in exI)
   429   apply (rule_tac x = k in exI)
   430   apply (rule_tac x = 0 in exI)
   430   apply (rule_tac x = 0 in exI)
   431   apply (auto simp add: ring_simps)
   431   apply (auto simp add: field_simps)
   432   apply (subst (asm) cong_sym_eq_nat)
   432   apply (subst (asm) cong_sym_eq_nat)
   433   apply (subst (asm) cong_altdef_nat)
   433   apply (subst (asm) cong_altdef_nat)
   434   apply force
   434   apply force
   435   apply (unfold dvd_def, auto)
   435   apply (unfold dvd_def, auto)
   436   apply (rule_tac x = 0 in exI)
   436   apply (rule_tac x = 0 in exI)
   437   apply (rule_tac x = k in exI)
   437   apply (rule_tac x = k in exI)
   438   apply (auto simp add: ring_simps)
   438   apply (auto simp add: field_simps)
   439   apply (unfold cong_nat_def)
   439   apply (unfold cong_nat_def)
   440   apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
   440   apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
   441   apply (erule ssubst)back
   441   apply (erule ssubst)back
   442   apply (erule subst)
   442   apply (erule subst)
   443   apply auto
   443   apply auto
   531 lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   531 lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   532     [x = y] (mod n)"
   532     [x = y] (mod n)"
   533   apply (auto simp add: cong_iff_lin_nat dvd_def)
   533   apply (auto simp add: cong_iff_lin_nat dvd_def)
   534   apply (rule_tac x="k1 * k" in exI)
   534   apply (rule_tac x="k1 * k" in exI)
   535   apply (rule_tac x="k2 * k" in exI)
   535   apply (rule_tac x="k2 * k" in exI)
   536   apply (simp add: ring_simps)
   536   apply (simp add: field_simps)
   537 done
   537 done
   538 
   538 
   539 lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   539 lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   540     [x = y] (mod n)"
   540     [x = y] (mod n)"
   541   by (auto simp add: cong_altdef_int dvd_def)
   541   by (auto simp add: cong_altdef_int dvd_def)
   557   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   557   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   558 
   558 
   559 lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
   559 lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
   560   apply (simp add: cong_altdef_int)
   560   apply (simp add: cong_altdef_int)
   561   apply (subst dvd_minus_iff [symmetric])
   561   apply (subst dvd_minus_iff [symmetric])
   562   apply (simp add: ring_simps)
   562   apply (simp add: field_simps)
   563 done
   563 done
   564 
   564 
   565 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   565 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   566   by (auto simp add: cong_altdef_int)
   566   by (auto simp add: cong_altdef_int)
   567 
   567 
   601   apply (rule iffI)
   601   apply (rule iffI)
   602   apply (drule cong_to_1_nat)
   602   apply (drule cong_to_1_nat)
   603   apply (unfold dvd_def)
   603   apply (unfold dvd_def)
   604   apply auto [1]
   604   apply auto [1]
   605   apply (rule_tac x = k in exI)
   605   apply (rule_tac x = k in exI)
   606   apply (auto simp add: ring_simps) [1]
   606   apply (auto simp add: field_simps) [1]
   607   apply (subst cong_altdef_nat)
   607   apply (subst cong_altdef_nat)
   608   apply (auto simp add: dvd_def)
   608   apply (auto simp add: dvd_def)
   609 done
   609 done
   610 
   610 
   611 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   611 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   612   apply (subst cong_altdef_nat)
   612   apply (subst cong_altdef_nat)
   613   apply assumption
   613   apply assumption
   614   apply (unfold dvd_def, auto simp add: ring_simps)
   614   apply (unfold dvd_def, auto simp add: field_simps)
   615   apply (rule_tac x = k in exI)
   615   apply (rule_tac x = k in exI)
   616   apply auto
   616   apply auto
   617 done
   617 done
   618 
   618 
   619 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   619 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"