equal
deleted
inserted
replaced
191 then have "2 \<le> q - 1" by arith |
191 then have "2 \<le> q - 1" by arith |
192 then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto) |
192 then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto) |
193 then show ?thesis by auto |
193 then show ?thesis by auto |
194 qed |
194 qed |
195 |
195 |
196 ML {* fast_arith_split_limit := 0; *} (*FIXME*) |
|
197 |
|
198 lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> |
196 lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> |
199 (p * b \<noteq> q * a)" |
197 (p * b \<noteq> q * a)" |
200 proof |
198 proof |
201 assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2" |
199 assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2" |
202 then have "q dvd (p * b)" by (auto simp add: dvd_def) |
200 then have "q dvd (p * b)" by (auto simp add: dvd_def) |
233 with prems show ?thesis by auto |
231 with prems show ?thesis by auto |
234 qed |
232 qed |
235 then have p1: "q \<le> -1" by arith |
233 then have p1: "q \<le> -1" by arith |
236 with q_g_2 show False by auto |
234 with q_g_2 show False by auto |
237 qed |
235 qed |
238 |
|
239 ML {* fast_arith_split_limit := 9; *} (*FIXME*) |
|
240 |
236 |
241 lemma (in QRTEMP) P_set_finite: "finite (P_set)" |
237 lemma (in QRTEMP) P_set_finite: "finite (P_set)" |
242 using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite) |
238 using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite) |
243 |
239 |
244 lemma (in QRTEMP) Q_set_finite: "finite (Q_set)" |
240 lemma (in QRTEMP) Q_set_finite: "finite (Q_set)" |