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.10  
    1.11  lemma cong_mult_rcancel_int:
    1.12 @@ -416,7 +416,7 @@
    1.13  done
    1.14  
    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.20  
    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.45  
    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.49    apply (simp add: cong_altdef_int)
    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.54  
    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