author wenzelm Tue Jan 05 21:57:21 2016 +0100 (2016-01-05) changeset 62072 bf3d9f113474 parent 62071 4e6e850e97c2 child 62073 ff4ce77a49ce
isabelle update_cartouches -c -t;
 src/HOL/Library/Nonpos_Ints.thy file | annotate | diff | revisions src/HOL/Library/Poly_Deriv.thy file | annotate | diff | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Gamma.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Summation.thy file | annotate | diff | revisions
```     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.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.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.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.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)
```