equal
deleted
inserted
replaced
38 |
38 |
39 lemma abelian_group: "abelian_group R" |
39 lemma abelian_group: "abelian_group R" |
40 apply (insert m_gt_one) |
40 apply (insert m_gt_one) |
41 apply (rule abelian_groupI) |
41 apply (rule abelian_groupI) |
42 apply (unfold R_def residue_ring_def) |
42 apply (unfold R_def residue_ring_def) |
43 apply (auto simp add: mod_add_right_eq [symmetric] ac_simps) |
43 apply (auto simp add: mod_add_right_eq ac_simps) |
44 apply (case_tac "x = 0") |
44 apply (case_tac "x = 0") |
45 apply force |
45 apply force |
46 apply (subgoal_tac "(x + (m - x)) mod m = 0") |
46 apply (subgoal_tac "(x + (m - x)) mod m = 0") |
47 apply (erule bexI) |
47 apply (erule bexI) |
48 apply auto |
48 apply auto |
53 apply (unfold R_def residue_ring_def) |
53 apply (unfold R_def residue_ring_def) |
54 apply (rule comm_monoidI) |
54 apply (rule comm_monoidI) |
55 apply auto |
55 apply auto |
56 apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m") |
56 apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m") |
57 apply (erule ssubst) |
57 apply (erule ssubst) |
58 apply (subst mod_mult_right_eq [symmetric])+ |
58 apply (subst mod_mult_right_eq)+ |
59 apply (simp_all only: ac_simps) |
59 apply (simp_all only: ac_simps) |
60 done |
60 done |
61 |
61 |
62 lemma cring: "cring R" |
62 lemma cring: "cring R" |
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) |
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) |
70 apply (simp add: field_simps) |
70 apply (simp add: field_simps) |
71 done |
71 done |
72 |
72 |
73 end |
73 end |
74 |
74 |
114 apply (insert m_gt_one) |
114 apply (insert m_gt_one) |
115 apply (unfold R_def a_inv_def m_inv_def residue_ring_def) |
115 apply (unfold R_def a_inv_def m_inv_def residue_ring_def) |
116 apply auto |
116 apply auto |
117 apply (rule the_equality) |
117 apply (rule the_equality) |
118 apply auto |
118 apply auto |
119 apply (subst mod_add_right_eq [symmetric]) |
119 apply (subst mod_add_right_eq) |
120 apply auto |
120 apply auto |
121 apply (subst mod_add_left_eq [symmetric]) |
121 apply (subst mod_add_left_eq) |
122 apply auto |
122 apply auto |
123 apply (subgoal_tac "y mod m = - x mod m") |
123 apply (subgoal_tac "y mod m = - x mod m") |
124 apply simp |
124 apply simp |
125 apply (metis minus_add_cancel mod_mult_self1 mult.commute) |
125 apply (metis minus_add_cancel mod_mult_self1 mult.commute) |
126 done |
126 done |
141 unfolding res_carrier_eq |
141 unfolding res_carrier_eq |
142 using insert m_gt_one by auto |
142 using insert m_gt_one by auto |
143 |
143 |
144 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m" |
144 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m" |
145 unfolding R_def residue_ring_def |
145 unfolding R_def residue_ring_def |
146 apply auto |
146 by (auto simp add: mod_simps) |
147 apply presburger |
|
148 done |
|
149 |
147 |
150 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" |
148 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" |
151 unfolding R_def residue_ring_def |
149 unfolding R_def residue_ring_def |
152 by auto (metis mod_mult_eq) |
150 by (auto simp add: mod_simps) |
153 |
151 |
154 lemma zero_cong: "\<zero> = 0" |
152 lemma zero_cong: "\<zero> = 0" |
155 unfolding R_def residue_ring_def by auto |
153 unfolding R_def residue_ring_def by auto |
156 |
154 |
157 lemma one_cong: "\<one> = 1 mod m" |
155 lemma one_cong: "\<one> = 1 mod m" |