equal
deleted
inserted
replaced
279 apply (drule_tac x = xa in spec) |
279 apply (drule_tac x = xa in spec) |
280 apply (clarsimp simp add: field_simps) |
280 apply (clarsimp simp add: field_simps) |
281 apply (drule_tac x = m in spec) |
281 apply (drule_tac x = m in spec) |
282 apply (auto simp add:field_simps) |
282 apply (auto simp add:field_simps) |
283 done |
283 done |
284 lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0, standard] |
284 lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0] |
285 |
285 |
286 lemma poly_roots_index_length0: "poly p (x::'a::idom) \<noteq> poly [] x ==> |
286 lemma poly_roots_index_length0: "poly p (x::'a::idom) \<noteq> poly [] x ==> |
287 \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)" |
287 \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)" |
288 by (blast intro: poly_roots_index_lemma1) |
288 by (blast intro: poly_roots_index_lemma1) |
289 |
289 |
320 apply (auto simp only: poly_mult List.list.size) |
320 apply (auto simp only: poly_mult List.list.size) |
321 apply (drule_tac x = xa in spec) |
321 apply (drule_tac x = xa in spec) |
322 apply (clarsimp simp add: field_simps) |
322 apply (clarsimp simp add: field_simps) |
323 done |
323 done |
324 |
324 |
325 lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard] |
325 lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma] |
326 |
326 |
327 lemma poly_roots_index_length: "poly p (x::'a::idom) \<noteq> poly [] x ==> |
327 lemma poly_roots_index_length: "poly p (x::'a::idom) \<noteq> poly [] x ==> |
328 \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i" |
328 \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i" |
329 by (blast intro: poly_roots_index_lemma2) |
329 by (blast intro: poly_roots_index_lemma2) |
330 |
330 |