src/HOL/Library/Univ_Poly.thy
changeset 29879 4425849f5db7
parent 29667 53103fc8ffa3
child 30488 5c4c3a9e9102
equal deleted 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 
   347 lemma UNIV_nat_infinite: "\<not> finite (UNIV :: nat set)"
       
   348   unfolding finite_conv_nat_seg_image
       
   349 proof(auto simp add: expand_set_eq image_iff)
       
   350   fix n::nat and f:: "nat \<Rightarrow> nat"
       
   351   let ?N = "{i. i < n}"
       
   352   let ?fN = "f ` ?N"
       
   353   let ?y = "Max ?fN + 1"
       
   354   from nat_seg_image_imp_finite[of "?fN" "f" n] 
       
   355   have thfN: "finite ?fN" by simp
       
   356   {assume "n =0" hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto}
       
   357   moreover
       
   358   {assume nz: "n \<noteq> 0"
       
   359     hence thne: "?fN \<noteq> {}" by (auto simp add: neq0_conv)
       
   360     have "\<forall>x\<in> ?fN. Max ?fN \<ge> x" using nz Max_ge_iff[OF thfN thne] by auto
       
   361     hence "\<forall>x\<in> ?fN. ?y > x" by auto
       
   362     hence "?y \<notin> ?fN" by auto
       
   363     hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto }
       
   364   ultimately show "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by blast
       
   365 qed
       
   366 
       
   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