src/HOL/Library/Univ_Poly.thy
 changeset 29879 4425849f5db7 parent 29667 53103fc8ffa3 child 30488 5c4c3a9e9102
equal inserted replaced
29878:06efd6e731c6 29879:4425849f5db7
`   342 apply (rule_tac x="map (\<lambda>n. i n) [0 ..< Suc (length p)]" in exI)`
`   342 apply (rule_tac x="map (\<lambda>n. i n) [0 ..< Suc (length p)]" in exI)`
`   343 apply (auto simp add: image_iff)`
`   343 apply (auto simp add: image_iff)`
`   344 apply (erule_tac x="x" in allE, clarsimp)`
`   344 apply (erule_tac x="x" in allE, clarsimp)`
`   345 by (case_tac "n=length p", auto simp add: order_le_less)`
`   345 by (case_tac "n=length p", auto simp add: order_le_less)`
`   346 `
`   346 `
`   367 lemma (in ring_char_0) UNIV_ring_char_0_infinte: `
`   347 lemma (in ring_char_0) UNIV_ring_char_0_infinte: `
`   368   "\<not> (finite (UNIV:: 'a set))" `
`   348   "\<not> (finite (UNIV:: 'a set))" `
`   369 proof`
`   349 proof`
`   370   assume F: "finite (UNIV :: 'a set)"`
`   350   assume F: "finite (UNIV :: 'a set)"`
`   371   have "finite (UNIV :: nat set)"`
`   351   have "finite (UNIV :: nat set)"`
`   372   proof (rule finite_imageD)`
`   352   proof (rule finite_imageD)`
`   373     have "of_nat ` UNIV \<subseteq> UNIV" by simp`
`   353     have "of_nat ` UNIV \<subseteq> UNIV" by simp`
`   374     then show "finite (of_nat ` UNIV :: 'a set)" using F by (rule finite_subset)`
`   354     then show "finite (of_nat ` UNIV :: 'a set)" using F by (rule finite_subset)`
`   375     show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: inj_on_def)`
`   355     show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: inj_on_def)`
`   376   qed`
`   356   qed`
`   377   with UNIV_nat_infinite show False ..`
`   357   with infinite_UNIV_nat show False ..`
`   378 qed`
`   358 qed`
`   379 `
`   359 `
`   380 lemma (in idom_char_0) poly_roots_finite: "(poly p \<noteq> poly []) = `
`   360 lemma (in idom_char_0) poly_roots_finite: "(poly p \<noteq> poly []) = `
`   381   finite {x. poly p x = 0}"`
`   361   finite {x. poly p x = 0}"`
`   382 proof`
`   362 proof`