src/HOL/Number_Theory/Cong.thy
 changeset 36350 bc7982c54e37 parent 35644 d20cf282342e child 37293 2c9ed7478e6e
1.1 --- a/src/HOL/Number_Theory/Cong.thy	Mon Apr 26 11:34:17 2010 +0200
1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Mon Apr 26 11:34:19 2010 +0200
1.3 @@ -350,7 +350,7 @@
1.4    apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
1.5    (* any way around this? *)
1.6    apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
1.7 -  apply (auto simp add: ring_simps)
1.8 +  apply (auto simp add: field_simps)
1.9  done
1.11  lemma cong_mult_rcancel_int:
1.12 @@ -416,7 +416,7 @@
1.13  done
1.15  lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
1.16 -  apply (auto simp add: cong_altdef_int dvd_def ring_simps)
1.17 +  apply (auto simp add: cong_altdef_int dvd_def field_simps)
1.18    apply (rule_tac [!] x = "-k" in exI, auto)
1.19  done
1.21 @@ -428,14 +428,14 @@
1.22    apply (unfold dvd_def, auto)
1.23    apply (rule_tac x = k in exI)
1.24    apply (rule_tac x = 0 in exI)
1.25 -  apply (auto simp add: ring_simps)
1.26 +  apply (auto simp add: field_simps)
1.27    apply (subst (asm) cong_sym_eq_nat)
1.28    apply (subst (asm) cong_altdef_nat)
1.29    apply force
1.30    apply (unfold dvd_def, auto)
1.31    apply (rule_tac x = 0 in exI)
1.32    apply (rule_tac x = k in exI)
1.33 -  apply (auto simp add: ring_simps)
1.34 +  apply (auto simp add: field_simps)
1.35    apply (unfold cong_nat_def)
1.36    apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
1.37    apply (erule ssubst)back
1.38 @@ -533,7 +533,7 @@
1.39    apply (auto simp add: cong_iff_lin_nat dvd_def)
1.40    apply (rule_tac x="k1 * k" in exI)
1.41    apply (rule_tac x="k2 * k" in exI)
1.42 -  apply (simp add: ring_simps)
1.43 +  apply (simp add: field_simps)
1.44  done
1.46  lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
1.47 @@ -559,7 +559,7 @@
1.48  lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
1.50    apply (subst dvd_minus_iff [symmetric])
1.51 -  apply (simp add: ring_simps)
1.52 +  apply (simp add: field_simps)
1.53  done
1.55  lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
1.56 @@ -603,7 +603,7 @@
1.57    apply (unfold dvd_def)
1.58    apply auto [1]
1.59    apply (rule_tac x = k in exI)
1.60 -  apply (auto simp add: ring_simps) [1]
1.61 +  apply (auto simp add: field_simps) [1]
1.62    apply (subst cong_altdef_nat)
1.63    apply (auto simp add: dvd_def)
1.64  done
1.65 @@ -611,7 +611,7 @@
1.66  lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
1.67    apply (subst cong_altdef_nat)
1.68    apply assumption
1.69 -  apply (unfold dvd_def, auto simp add: ring_simps)
1.70 +  apply (unfold dvd_def, auto simp add: field_simps)
1.71    apply (rule_tac x = k in exI)
1.72    apply auto
1.73  done