src/HOL/Library/Univ_Poly.thy
changeset 29879 4425849f5db7
parent 29667 53103fc8ffa3
child 30488 5c4c3a9e9102
     1.1 --- a/src/HOL/Library/Univ_Poly.thy	Wed Feb 11 11:22:42 2009 -0800
     1.2 +++ b/src/HOL/Library/Univ_Poly.thy	Thu Feb 12 18:14:43 2009 +0100
     1.3 @@ -344,26 +344,6 @@
     1.4  apply (erule_tac x="x" in allE, clarsimp)
     1.5  by (case_tac "n=length p", auto simp add: order_le_less)
     1.6  
     1.7 -lemma UNIV_nat_infinite: "\<not> finite (UNIV :: nat set)"
     1.8 -  unfolding finite_conv_nat_seg_image
     1.9 -proof(auto simp add: expand_set_eq image_iff)
    1.10 -  fix n::nat and f:: "nat \<Rightarrow> nat"
    1.11 -  let ?N = "{i. i < n}"
    1.12 -  let ?fN = "f ` ?N"
    1.13 -  let ?y = "Max ?fN + 1"
    1.14 -  from nat_seg_image_imp_finite[of "?fN" "f" n] 
    1.15 -  have thfN: "finite ?fN" by simp
    1.16 -  {assume "n =0" hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto}
    1.17 -  moreover
    1.18 -  {assume nz: "n \<noteq> 0"
    1.19 -    hence thne: "?fN \<noteq> {}" by (auto simp add: neq0_conv)
    1.20 -    have "\<forall>x\<in> ?fN. Max ?fN \<ge> x" using nz Max_ge_iff[OF thfN thne] by auto
    1.21 -    hence "\<forall>x\<in> ?fN. ?y > x" by auto
    1.22 -    hence "?y \<notin> ?fN" by auto
    1.23 -    hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto }
    1.24 -  ultimately show "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by blast
    1.25 -qed
    1.26 -
    1.27  lemma (in ring_char_0) UNIV_ring_char_0_infinte: 
    1.28    "\<not> (finite (UNIV:: 'a set))" 
    1.29  proof
    1.30 @@ -374,7 +354,7 @@
    1.31      then show "finite (of_nat ` UNIV :: 'a set)" using F by (rule finite_subset)
    1.32      show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: inj_on_def)
    1.33    qed
    1.34 -  with UNIV_nat_infinite show False ..
    1.35 +  with infinite_UNIV_nat show False ..
    1.36  qed
    1.37  
    1.38  lemma (in idom_char_0) poly_roots_finite: "(poly p \<noteq> poly []) =