replace almost_everywhere_zero by Infinite_Set.MOST
authorhoelzl
Thu Apr 09 15:17:21 2015 +0200 (2015-04-09)
changeset 59983cd2efd7d06bd
parent 59982 f402fd001429
child 59985 5574138cf97c
replace almost_everywhere_zero by Infinite_Set.MOST
src/HOL/Library/Polynomial.thy
     1.1 --- a/src/HOL/Library/Polynomial.thy	Thu Apr 09 13:57:37 2015 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Apr 09 15:17:21 2015 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  section {* Polynomials as type over a ring structure *}
     1.5  
     1.6  theory Polynomial
     1.7 -imports Main GCD "~~/src/HOL/Library/More_List"
     1.8 +imports Main GCD "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
     1.9  begin
    1.10  
    1.11  subsection {* Auxiliary: operations for lists (later) representing coefficients *}
    1.12 @@ -50,48 +50,13 @@
    1.13    "tl (x ## xs) = xs"
    1.14    by (simp add: cCons_def)
    1.15  
    1.16 -
    1.17 -subsection {* Almost everywhere zero functions *}
    1.18 -
    1.19 -definition almost_everywhere_zero :: "(nat \<Rightarrow> 'a::zero) \<Rightarrow> bool"
    1.20 -where
    1.21 -  "almost_everywhere_zero f \<longleftrightarrow> (\<exists>n. \<forall>i>n. f i = 0)"
    1.22 -
    1.23 -lemma almost_everywhere_zeroI:
    1.24 -  "(\<And>i. i > n \<Longrightarrow> f i = 0) \<Longrightarrow> almost_everywhere_zero f"
    1.25 -  by (auto simp add: almost_everywhere_zero_def)
    1.26 -
    1.27 -lemma almost_everywhere_zeroE:
    1.28 -  assumes "almost_everywhere_zero f"
    1.29 -  obtains n where "\<And>i. i > n \<Longrightarrow> f i = 0"
    1.30 -proof -
    1.31 -  from assms have "\<exists>n. \<forall>i>n. f i = 0" by (simp add: almost_everywhere_zero_def)
    1.32 -  then obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by blast
    1.33 -  with that show thesis .
    1.34 -qed
    1.35 -
    1.36 -lemma almost_everywhere_zero_case_nat:
    1.37 -  assumes "almost_everywhere_zero f"
    1.38 -  shows "almost_everywhere_zero (case_nat a f)"
    1.39 -  using assms
    1.40 -  by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split)
    1.41 -    blast
    1.42 -
    1.43 -lemma almost_everywhere_zero_Suc:
    1.44 -  assumes "almost_everywhere_zero f"
    1.45 -  shows "almost_everywhere_zero (\<lambda>n. f (Suc n))"
    1.46 -proof -
    1.47 -  from assms obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by (erule almost_everywhere_zeroE)
    1.48 -  then have "\<And>i. i > n \<Longrightarrow> f (Suc i) = 0" by auto
    1.49 -  then show ?thesis by (rule almost_everywhere_zeroI)
    1.50 -qed
    1.51 -
    1.52 +lemma MOST_SucD: "(\<forall>\<^sub>\<infinity> n. P (Suc n)) \<Longrightarrow> (\<forall>\<^sub>\<infinity> n. P n)"
    1.53 +  by (auto simp: MOST_nat) (metis Suc_lessE)
    1.54  
    1.55  subsection {* Definition of type @{text poly} *}
    1.56  
    1.57 -typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. almost_everywhere_zero f}"
    1.58 -  morphisms coeff Abs_poly
    1.59 -  unfolding almost_everywhere_zero_def by auto
    1.60 +typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
    1.61 +  morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
    1.62  
    1.63  setup_lifting type_definition_poly
    1.64  
    1.65 @@ -101,8 +66,7 @@
    1.66  lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
    1.67    by (simp add: poly_eq_iff)
    1.68  
    1.69 -lemma coeff_almost_everywhere_zero:
    1.70 -  "almost_everywhere_zero (coeff p)"
    1.71 +lemma MOST_coeff_eq_0: "\<forall>\<^sub>\<infinity> n. coeff p n = 0"
    1.72    using coeff [of p] by simp
    1.73  
    1.74  
    1.75 @@ -116,8 +80,8 @@
    1.76    assumes "degree p < n"
    1.77    shows "coeff p n = 0"
    1.78  proof -
    1.79 -  from coeff_almost_everywhere_zero
    1.80 -  have "\<exists>n. \<forall>i>n. coeff p i = 0" by (blast intro: almost_everywhere_zeroE)
    1.81 +  have "\<exists>n. \<forall>i>n. coeff p i = 0"
    1.82 +    using MOST_coeff_eq_0 by (simp add: MOST_nat)
    1.83    then have "\<forall>i>degree p. coeff p i = 0"
    1.84      unfolding degree_def by (rule LeastI_ex)
    1.85    with assms show ?thesis by simp
    1.86 @@ -139,7 +103,7 @@
    1.87  begin
    1.88  
    1.89  lift_definition zero_poly :: "'a poly"
    1.90 -  is "\<lambda>_. 0" by (rule almost_everywhere_zeroI) simp
    1.91 +  is "\<lambda>_. 0" by (rule MOST_I) simp
    1.92  
    1.93  instance ..
    1.94  
    1.95 @@ -184,7 +148,7 @@
    1.96  
    1.97  lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    1.98    is "\<lambda>a p. case_nat a (coeff p)"
    1.99 -  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_case_nat)
   1.100 +  by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)
   1.101  
   1.102  lemmas coeff_pCons = pCons.rep_eq
   1.103  
   1.104 @@ -247,7 +211,8 @@
   1.105  proof
   1.106    show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
   1.107      by transfer
   1.108 -      (simp add: Abs_poly_inverse almost_everywhere_zero_Suc fun_eq_iff split: nat.split)
   1.109 +       (simp_all add: MOST_inj[where f=Suc and P="\<lambda>n. p n = 0" for p] fun_eq_iff Abs_poly_inverse
   1.110 +                 split: nat.split)
   1.111  qed
   1.112  
   1.113  lemma pCons_induct [case_names 0 pCons, induct type: poly]:
   1.114 @@ -483,7 +448,7 @@
   1.115  
   1.116  lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
   1.117    is "\<lambda>a m n. if m = n then a else 0"
   1.118 -  by (auto intro!: almost_everywhere_zeroI)
   1.119 +  by (simp add: MOST_iff_cofinite)
   1.120  
   1.121  lemma coeff_monom [simp]:
   1.122    "coeff (monom a m) n = (if m = n then a else 0)"
   1.123 @@ -536,11 +501,9 @@
   1.124  
   1.125  lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   1.126    is "\<lambda>p q n. coeff p n + coeff q n"
   1.127 -proof (rule almost_everywhere_zeroI) 
   1.128 -  fix q p :: "'a poly" and i
   1.129 -  assume "max (degree q) (degree p) < i"
   1.130 -  then show "coeff p i + coeff q i = 0"
   1.131 -    by (simp add: coeff_eq_0)
   1.132 +proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
   1.133 +  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n + coeff q n = 0"
   1.134 +    by simp
   1.135  qed
   1.136  
   1.137  lemma coeff_add [simp]:
   1.138 @@ -564,11 +527,9 @@
   1.139  
   1.140  lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   1.141    is "\<lambda>p q n. coeff p n - coeff q n"
   1.142 -proof (rule almost_everywhere_zeroI) 
   1.143 -  fix q p :: "'a poly" and i
   1.144 -  assume "max (degree q) (degree p) < i"
   1.145 -  then show "coeff p i - coeff q i = 0"
   1.146 -    by (simp add: coeff_eq_0)
   1.147 +proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
   1.148 +  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n - coeff q n = 0"
   1.149 +    by simp
   1.150  qed
   1.151  
   1.152  lemma coeff_diff [simp]:
   1.153 @@ -590,11 +551,9 @@
   1.154  
   1.155  lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   1.156    is "\<lambda>p n. - coeff p n"
   1.157 -proof (rule almost_everywhere_zeroI)
   1.158 -  fix p :: "'a poly" and i
   1.159 -  assume "degree p < i"
   1.160 -  then show "- coeff p i = 0"
   1.161 -    by (simp add: coeff_eq_0)
   1.162 +proof (rule MOST_rev_mp[OF MOST_coeff_eq_0])
   1.163 +  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> - coeff p n = 0"
   1.164 +    by simp
   1.165  qed
   1.166  
   1.167  lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   1.168 @@ -748,7 +707,7 @@
   1.169  
   1.170  lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   1.171    is "\<lambda>a p n. a * coeff p n"
   1.172 -proof (rule almost_everywhere_zeroI)
   1.173 +proof (intro MOST_nat[THEN iffD2] exI allI impI) 
   1.174    fix a :: 'a and p :: "'a poly" and i
   1.175    assume "degree p < i"
   1.176    then show "a * coeff p i = 0"