106 done |
106 done |
107 |
107 |
108 lemma Union_SetS_finite: "2 < p ==> finite (\<Union>(SetS a p))" |
108 lemma Union_SetS_finite: "2 < p ==> finite (\<Union>(SetS a p))" |
109 by (auto simp add: SetS_finite SetS_elems_finite) |
109 by (auto simp add: SetS_finite SetS_elems_finite) |
110 |
110 |
111 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); |
111 lemma card_sum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); |
112 \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S" |
112 \<forall>X \<in> S. card X = n |] ==> sum card S = sum (%x. n) S" |
113 by (induct set: finite) auto |
113 by (induct set: finite) auto |
114 |
114 |
115 lemma SetS_card: |
115 lemma SetS_card: |
116 assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" |
116 assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" |
117 shows "int(card(SetS a p)) = (p - 1) div 2" |
117 shows "int(card(SetS a p)) = (p - 1) div 2" |
118 proof - |
118 proof - |
119 have "(p - 1) = 2 * int(card(SetS a p))" |
119 have "(p - 1) = 2 * int(card(SetS a p))" |
120 proof - |
120 proof - |
121 have "p - 1 = int(card(\<Union>(SetS a p)))" |
121 have "p - 1 = int(card(\<Union>(SetS a p)))" |
122 by (auto simp add: assms MultInvPair_prop2 SRStar_card) |
122 by (auto simp add: assms MultInvPair_prop2 SRStar_card) |
123 also have "... = int (setsum card (SetS a p))" |
123 also have "... = int (sum card (SetS a p))" |
124 by (auto simp add: assms SetS_finite SetS_elems_finite |
124 by (auto simp add: assms SetS_finite SetS_elems_finite |
125 MultInvPair_prop1c [of p a] card_Union_disjoint) |
125 MultInvPair_prop1c [of p a] card_Union_disjoint) |
126 also have "... = int(setsum (%x.2) (SetS a p))" |
126 also have "... = int(sum (%x.2) (SetS a p))" |
127 using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite |
127 using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite |
128 card_setsum_aux simp del: setsum_constant) |
128 card_sum_aux simp del: sum_constant) |
129 also have "... = 2 * int(card( SetS a p))" |
129 also have "... = 2 * int(card( SetS a p))" |
130 by (auto simp add: assms SetS_finite setsum_const2) |
130 by (auto simp add: assms SetS_finite sum_const2) |
131 finally show ?thesis . |
131 finally show ?thesis . |
132 qed |
132 qed |
133 then show ?thesis by auto |
133 then show ?thesis by auto |
134 qed |
134 qed |
135 |
135 |