equal
deleted
inserted
replaced
63 apply (rule cringI) |
63 apply (rule cringI) |
64 apply (rule abelian_group) |
64 apply (rule abelian_group) |
65 apply (rule comm_monoid) |
65 apply (rule comm_monoid) |
66 apply (unfold R_def residue_ring_def, auto) |
66 apply (unfold R_def residue_ring_def, auto) |
67 apply (subst mod_add_eq [symmetric]) |
67 apply (subst mod_add_eq [symmetric]) |
68 apply (subst mult_commute) |
68 apply (subst mult.commute) |
69 apply (subst mod_mult_right_eq [symmetric]) |
69 apply (subst mod_mult_right_eq [symmetric]) |
70 apply (simp add: field_simps) |
70 apply (simp add: field_simps) |
71 done |
71 done |
72 |
72 |
73 end |
73 end |
103 apply auto |
103 apply auto |
104 apply (subgoal_tac "x ~= 0") |
104 apply (subgoal_tac "x ~= 0") |
105 apply auto |
105 apply auto |
106 apply (metis invertible_coprime_int) |
106 apply (metis invertible_coprime_int) |
107 apply (subst (asm) coprime_iff_invertible'_int) |
107 apply (subst (asm) coprime_iff_invertible'_int) |
108 apply (auto simp add: cong_int_def mult_commute) |
108 apply (auto simp add: cong_int_def mult.commute) |
109 done |
109 done |
110 |
110 |
111 lemma res_neg_eq: "\<ominus> x = (- x) mod m" |
111 lemma res_neg_eq: "\<ominus> x = (- x) mod m" |
112 apply (insert m_gt_one) |
112 apply (insert m_gt_one) |
113 apply (unfold R_def a_inv_def m_inv_def residue_ring_def) |
113 apply (unfold R_def a_inv_def m_inv_def residue_ring_def) |
118 apply auto |
118 apply auto |
119 apply (subst mod_add_left_eq [symmetric]) |
119 apply (subst mod_add_left_eq [symmetric]) |
120 apply auto |
120 apply auto |
121 apply (subgoal_tac "y mod m = - x mod m") |
121 apply (subgoal_tac "y mod m = - x mod m") |
122 apply simp |
122 apply simp |
123 apply (metis minus_add_cancel mod_mult_self1 mult_commute) |
123 apply (metis minus_add_cancel mod_mult_self1 mult.commute) |
124 done |
124 done |
125 |
125 |
126 lemma finite [iff]: "finite (carrier R)" |
126 lemma finite [iff]: "finite (carrier R)" |
127 by (subst res_carrier_eq, auto) |
127 by (subst res_carrier_eq, auto) |
128 |
128 |
157 (* revise algebra library to use 1? *) |
157 (* revise algebra library to use 1? *) |
158 lemma pow_cong: "(x mod m) (^) n = x^n mod m" |
158 lemma pow_cong: "(x mod m) (^) n = x^n mod m" |
159 apply (insert m_gt_one) |
159 apply (insert m_gt_one) |
160 apply (induct n) |
160 apply (induct n) |
161 apply (auto simp add: nat_pow_def one_cong) |
161 apply (auto simp add: nat_pow_def one_cong) |
162 apply (metis mult_commute mult_cong) |
162 apply (metis mult.commute mult_cong) |
163 done |
163 done |
164 |
164 |
165 lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m" |
165 lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m" |
166 by (metis mod_minus_eq res_neg_eq) |
166 by (metis mod_minus_eq res_neg_eq) |
167 |
167 |
194 |
194 |
195 (* Other useful facts about the residue ring *) |
195 (* Other useful facts about the residue ring *) |
196 |
196 |
197 lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2" |
197 lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2" |
198 apply (simp add: res_one_eq res_neg_eq) |
198 apply (simp add: res_one_eq res_neg_eq) |
199 apply (metis add_commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff |
199 apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff |
200 zero_neq_one zmod_zminus1_eq_if) |
200 zero_neq_one zmod_zminus1_eq_if) |
201 done |
201 done |
202 |
202 |
203 end |
203 end |
204 |
204 |