isabelle update_cartouches -c -t;
authorwenzelm
Tue Jan 05 21:57:21 2016 +0100 (2016-01-05)
changeset 62072bf3d9f113474
parent 62071 4e6e850e97c2
child 62073 ff4ce77a49ce
isabelle update_cartouches -c -t;
src/HOL/Library/Nonpos_Ints.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Polynomial.thy
src/HOL/Multivariate_Analysis/Gamma.thy
src/HOL/Multivariate_Analysis/Summation.thy
     1.1 --- a/src/HOL/Library/Nonpos_Ints.thy	Tue Jan 05 21:55:40 2016 +0100
     1.2 +++ b/src/HOL/Library/Nonpos_Ints.thy	Tue Jan 05 21:57:21 2016 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4    hence "(of_int m :: 'a) = of_nat n" by simp
     1.5    also have "... = of_int (int n)" by simp
     1.6    finally have "m = int n" by (subst (asm) of_int_eq_iff)
     1.7 -  with `m \<le> 0` show "n = 0" by auto
     1.8 +  with \<open>m \<le> 0\<close> show "n = 0" by auto
     1.9  qed simp
    1.10  
    1.11  lemma nonpos_Ints_of_int: "n \<le> 0 \<Longrightarrow> of_int n \<in> \<int>\<^sub>\<le>\<^sub>0"
    1.12 @@ -84,10 +84,10 @@
    1.13  proof
    1.14    assume "of_real x \<in> (\<int>\<^sub>\<le>\<^sub>0 :: 'a set)"
    1.15    then obtain n where "(of_real x :: 'a) = of_int n" "n \<le> 0" by (erule nonpos_Ints_cases)
    1.16 -  note `of_real x = of_int n`
    1.17 +  note \<open>of_real x = of_int n\<close>
    1.18    also have "of_int n = of_real (of_int n)" by (rule of_real_of_int_eq [symmetric])
    1.19    finally have "x = of_int n" by (subst (asm) of_real_eq_iff)
    1.20 -  with `n \<le> 0` show "x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: nonpos_Ints_of_int)
    1.21 +  with \<open>n \<le> 0\<close> show "x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: nonpos_Ints_of_int)
    1.22  qed (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int)
    1.23  
    1.24  lemma nonpos_Ints_altdef: "\<int>\<^sub>\<le>\<^sub>0 = {n \<in> \<int>. (n :: 'a :: linordered_idom) \<le> 0}"
     2.1 --- a/src/HOL/Library/Poly_Deriv.thy	Tue Jan 05 21:55:40 2016 +0100
     2.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jan 05 21:57:21 2016 +0100
     2.3 @@ -167,7 +167,7 @@
     2.4      proof -
     2.5        assume "p\<noteq>0"
     2.6        then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
     2.7 -      have gt_0:"lead_coeff p >0" using pCons(3) `p\<noteq>0` by auto
     2.8 +      have gt_0:"lead_coeff p >0" using pCons(3) \<open>p\<noteq>0\<close> by auto
     2.9        def n\<equiv>"max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
    2.10        show ?thesis 
    2.11          proof (rule_tac x=n in exI,rule,rule) 
    2.12 @@ -176,9 +176,9 @@
    2.13              using gte_lcoeff unfolding n_def by auto
    2.14            hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
    2.15              by (intro frac_le,auto)
    2.16 -          hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using `n\<le>x`[unfolded n_def] by auto
    2.17 +          hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using \<open>n\<le>x\<close>[unfolded n_def] by auto
    2.18            thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
    2.19 -            using `lead_coeff p \<le> poly p x` `poly p x>0` `p\<noteq>0`
    2.20 +            using \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x>0\<close> \<open>p\<noteq>0\<close>
    2.21              by (auto simp add:field_simps)
    2.22          qed
    2.23      qed
     3.1 --- a/src/HOL/Library/Polynomial.thy	Tue Jan 05 21:55:40 2016 +0100
     3.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jan 05 21:57:21 2016 +0100
     3.3 @@ -475,7 +475,7 @@
     3.4                   coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
     3.5            by (simp add: field_simps setsum_right_distrib coeff_pCons)
     3.6        also note setsum_atMost_Suc_shift[symmetric]
     3.7 -      also note degree_pCons_eq[OF `p \<noteq> 0`, of a, symmetric]
     3.8 +      also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
     3.9        finally show ?thesis .
    3.10     qed simp
    3.11  qed simp
    3.12 @@ -2145,19 +2145,19 @@
    3.13      next
    3.14        case False assume "degree (q * pcompose p q) = 0"
    3.15        hence "degree q=0 \<or> pcompose p q=0" by (auto simp add:degree_mult_eq_0)
    3.16 -      moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) `p\<noteq>0` 
    3.17 +      moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) \<open>p\<noteq>0\<close> 
    3.18          proof -
    3.19            assume "pcompose p q=0" "degree q\<noteq>0"
    3.20            hence "degree p=0" using pCons.hyps(2) by auto
    3.21            then obtain a1 where "p=[:a1:]"
    3.22              by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
    3.23 -          thus False using `pcompose p q=0` `p\<noteq>0` by auto
    3.24 +          thus False using \<open>pcompose p q=0\<close> \<open>p\<noteq>0\<close> by auto
    3.25          qed
    3.26        ultimately have "degree (pCons a p) * degree q=0" by auto
    3.27        moreover have "degree (pcompose (pCons a p) q) = 0" 
    3.28          proof -
    3.29            have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
    3.30 -            using `degree (q * pcompose p q) = 0` by simp
    3.31 +            using \<open>degree (q * pcompose p q) = 0\<close> by simp
    3.32            also have "... \<ge> degree ([:a:] + q * pcompose p q)"
    3.33              by (rule degree_add_le_max)
    3.34            finally show ?thesis by (auto simp add:pcompose_pCons)
    3.35 @@ -2172,7 +2172,7 @@
    3.36          unfolding pcompose_pCons
    3.37          using degree_add_eq_right[of "[:a:]" ] asm by auto       
    3.38        thus ?thesis 
    3.39 -        using pCons.hyps(2) degree_mult_eq[OF `q\<noteq>0` `pcompose p q\<noteq>0`] by auto
    3.40 +        using pCons.hyps(2) degree_mult_eq[OF \<open>q\<noteq>0\<close> \<open>pcompose p q\<noteq>0\<close>] by auto
    3.41      qed
    3.42    ultimately show ?case by blast
    3.43  qed
    3.44 @@ -2186,11 +2186,11 @@
    3.45    then obtain a where "p=[:a:]" 
    3.46      by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
    3.47    hence "a=0" using assms(1) by auto
    3.48 -  thus ?thesis using `p=[:a:]` by simp
    3.49 +  thus ?thesis using \<open>p=[:a:]\<close> by simp
    3.50  qed
    3.51  
    3.52  
    3.53 -subsection {* Leading coefficient *}
    3.54 +subsection \<open>Leading coefficient\<close>
    3.55  
    3.56  definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
    3.57    "lead_coeff p= coeff p (degree p)"
    3.58 @@ -2232,7 +2232,7 @@
    3.59      proof -
    3.60        assume "degree ( q * pcompose p q) = 0"
    3.61        hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
    3.62 -      hence "p=0" using pcompose_eq_0[OF _ `degree q > 0`] by simp
    3.63 +      hence "p=0" using pcompose_eq_0[OF _ \<open>degree q > 0\<close>] by simp
    3.64        thus ?thesis by auto
    3.65      qed
    3.66    moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case" 
     4.1 --- a/src/HOL/Multivariate_Analysis/Gamma.thy	Tue Jan 05 21:55:40 2016 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Tue Jan 05 21:57:21 2016 +0100
     4.3 @@ -169,7 +169,7 @@
     4.4    also have "\<dots> \<le> dist z (of_int n)"
     4.5      using round_Re_minimises_norm[of z] by (simp add: dist_complex_def)
     4.6    finally have "dist t (of_int n) > 0" by simp
     4.7 -  with `t = of_int n` show False by simp
     4.8 +  with \<open>t = of_int n\<close> show False by simp
     4.9  qed
    4.10  
    4.11  lemma no_nonpos_Int_in_ball':
    4.12 @@ -377,7 +377,7 @@
    4.13      finally have "of_nat N \<ge> 2 * (norm z + d)" .
    4.14      moreover have "N \<ge> 2" "N \<ge> M" unfolding N_def by simp_all
    4.15      moreover have "(\<Sum>k=m..n. 1/(of_nat k)\<^sup>2) < e'" if "m \<ge> N" for m n
    4.16 -      using M[OF order.trans[OF `N \<ge> M` that]] unfolding real_norm_def
    4.17 +      using M[OF order.trans[OF \<open>N \<ge> M\<close> that]] unfolding real_norm_def
    4.18        by (subst (asm) abs_of_nonneg) (auto intro: setsum_nonneg simp: divide_simps)
    4.19      moreover note calculation
    4.20    } note N = this
    4.21 @@ -1959,7 +1959,7 @@
    4.22    let ?h = "\<lambda>z::complex. (of_real pi * cot (of_real pi*z) + Digamma z - Digamma (1 - z))"
    4.23    def h \<equiv> "\<lambda>z::complex. if z \<in> \<int> then 0 else ?h z"
    4.24  
    4.25 -  -- \<open>@{term g} is periodic with period 1.\<close>
    4.26 +  \<comment> \<open>@{term g} is periodic with period 1.\<close>
    4.27    interpret g: periodic_fun_simple' g
    4.28    proof
    4.29      fix z :: complex
    4.30 @@ -1979,7 +1979,7 @@
    4.31      qed (simp add: g_def)
    4.32    qed
    4.33  
    4.34 -  -- \<open>@{term g} is entire.\<close>
    4.35 +  \<comment> \<open>@{term g} is entire.\<close>
    4.36    have g_g': "(g has_field_derivative (h z * g z)) (at z)" for z :: complex
    4.37    proof (cases "z \<in> \<int>")
    4.38      let ?h' = "\<lambda>z. Beta z (1 - z) * ((Digamma z - Digamma (1 - z)) * sin (z * of_real pi) +
    4.39 @@ -2204,7 +2204,7 @@
    4.40    show ?thesis
    4.41    proof (cases "z \<in> \<int>")
    4.42      case False
    4.43 -    with `g z = pi` show ?thesis by (auto simp: g_def divide_simps)
    4.44 +    with \<open>g z = pi\<close> show ?thesis by (auto simp: g_def divide_simps)
    4.45    next
    4.46      case True
    4.47      then obtain n where n: "z = of_int n" by (elim Ints_cases)
     5.1 --- a/src/HOL/Multivariate_Analysis/Summation.thy	Tue Jan 05 21:55:40 2016 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Summation.thy	Tue Jan 05 21:57:21 2016 +0100
     5.3 @@ -141,7 +141,7 @@
     5.4    with l obtain l' where l': "l = ereal l'" by (cases l) simp_all
     5.5  
     5.6    def c \<equiv> "(1 - l') / 2"
     5.7 -  from l and `l \<ge> 0` have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def 
     5.8 +  from l and \<open>l \<ge> 0\<close> have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def 
     5.9      by (simp_all add: field_simps l')
    5.10    have "\<forall>C>l. eventually (\<lambda>n. ereal (root n (norm (f n))) < C) sequentially"
    5.11      by (subst Limsup_le_iff[symmetric]) (simp add: l_def)