94 by (drule_tac a = x in pos_mod_sign, arith, simp) |
94 by (drule_tac a = x in pos_mod_sign, arith, simp) |
95 |
95 |
96 lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))"; |
96 lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))"; |
97 by (auto simp add: SRStar_def zcong_def zdvd_not_zless) |
97 by (auto simp add: SRStar_def zcong_def zdvd_not_zless) |
98 |
98 |
99 lemma StandardRes_SRStar_prop2: "[| 2 < p; p \<in> zprime; x \<in> SRStar p |] |
99 lemma StandardRes_SRStar_prop2: "[| 2 < p; zprime p; x \<in> SRStar p |] |
100 ==> StandardRes p (MultInv p x) \<in> SRStar p"; |
100 ==> StandardRes p (MultInv p x) \<in> SRStar p"; |
101 apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp); |
101 apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp); |
102 apply (rule MultInv_prop3) |
102 apply (rule MultInv_prop3) |
103 apply (auto simp add: SRStar_def zcong_def zdvd_not_zless) |
103 apply (auto simp add: SRStar_def zcong_def zdvd_not_zless) |
104 done |
104 done |
105 |
105 |
106 lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x"; |
106 lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x"; |
107 by (auto simp add: SRStar_SR_prop StandardRes_SR_prop) |
107 by (auto simp add: SRStar_SR_prop StandardRes_SR_prop) |
108 |
108 |
109 lemma StandardRes_SRStar_prop4: "[| p \<in> zprime; 2 < p; x \<in> SRStar p |] |
109 lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \<in> SRStar p |] |
110 ==> StandardRes p x \<in> SRStar p"; |
110 ==> StandardRes p x \<in> SRStar p"; |
111 by (frule StandardRes_SRStar_prop3, auto) |
111 by (frule StandardRes_SRStar_prop3, auto) |
112 |
112 |
113 lemma SRStar_mult_prop1: "[| p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] |
113 lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] |
114 ==> (StandardRes p (x * y)):SRStar p"; |
114 ==> (StandardRes p (x * y)):SRStar p"; |
115 apply (frule_tac x = x in StandardRes_SRStar_prop4, auto) |
115 apply (frule_tac x = x in StandardRes_SRStar_prop4, auto) |
116 apply (frule_tac x = y in StandardRes_SRStar_prop4, auto) |
116 apply (frule_tac x = y in StandardRes_SRStar_prop4, auto) |
117 apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) |
117 apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) |
118 done |
118 done |
119 |
119 |
120 lemma SRStar_mult_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)); |
120 lemma SRStar_mult_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)); |
121 x \<in> SRStar p |] |
121 x \<in> SRStar p |] |
122 ==> StandardRes p (a * MultInv p x) \<in> SRStar p"; |
122 ==> StandardRes p (a * MultInv p x) \<in> SRStar p"; |
123 apply (frule_tac x = x in StandardRes_SRStar_prop2, auto) |
123 apply (frule_tac x = x in StandardRes_SRStar_prop2, auto) |
124 apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1) |
124 apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1) |
125 apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) |
125 apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) |