src/HOL/Number_Theory/Residues.thy
changeset 64593 50c715579715
parent 64282 261d42f0bfac
child 65066 c64d778a593a
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4    apply (insert m_gt_one)
     1.5    apply (rule abelian_groupI)
     1.6    apply (unfold R_def residue_ring_def)
     1.7 -  apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
     1.8 +  apply (auto simp add: mod_add_right_eq ac_simps)
     1.9    apply (case_tac "x = 0")
    1.10    apply force
    1.11    apply (subgoal_tac "(x + (m - x)) mod m = 0")
    1.12 @@ -55,7 +55,7 @@
    1.13    apply auto
    1.14    apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
    1.15    apply (erule ssubst)
    1.16 -  apply (subst mod_mult_right_eq [symmetric])+
    1.17 +  apply (subst mod_mult_right_eq)+
    1.18    apply (simp_all only: ac_simps)
    1.19    done
    1.20  
    1.21 @@ -64,9 +64,9 @@
    1.22    apply (rule abelian_group)
    1.23    apply (rule comm_monoid)
    1.24    apply (unfold R_def residue_ring_def, auto)
    1.25 -  apply (subst mod_add_eq [symmetric])
    1.26 +  apply (subst mod_add_eq)
    1.27    apply (subst mult.commute)
    1.28 -  apply (subst mod_mult_right_eq [symmetric])
    1.29 +  apply (subst mod_mult_right_eq)
    1.30    apply (simp add: field_simps)
    1.31    done
    1.32  
    1.33 @@ -116,9 +116,9 @@
    1.34    apply auto
    1.35    apply (rule the_equality)
    1.36    apply auto
    1.37 -  apply (subst mod_add_right_eq [symmetric])
    1.38 +  apply (subst mod_add_right_eq)
    1.39    apply auto
    1.40 -  apply (subst mod_add_left_eq [symmetric])
    1.41 +  apply (subst mod_add_left_eq)
    1.42    apply auto
    1.43    apply (subgoal_tac "y mod m = - x mod m")
    1.44    apply simp
    1.45 @@ -143,13 +143,11 @@
    1.46  
    1.47  lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
    1.48    unfolding R_def residue_ring_def
    1.49 -  apply auto
    1.50 -  apply presburger
    1.51 -  done
    1.52 +  by (auto simp add: mod_simps)
    1.53  
    1.54  lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
    1.55    unfolding R_def residue_ring_def
    1.56 -  by auto (metis mod_mult_eq)
    1.57 +  by (auto simp add: mod_simps)
    1.58  
    1.59  lemma zero_cong: "\<zero> = 0"
    1.60    unfolding R_def residue_ring_def by auto