# HG changeset patch # User wenzelm # Date 1432584703 -7200 # Node ID ff82ba1893c80c00396f7a2c3de645f9c70188f4 # Parent cc71f01f9fdec21f4a3133b7b4ebe7cc3bf63101# Parent 82453d0f49eeb44714916581488029187ffc57fc merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML; diff -r 82453d0f49ee -r ff82ba1893c8 Admin/isatest/settings/afp-poly diff -r 82453d0f49ee -r ff82ba1893c8 CONTRIBUTORS --- a/CONTRIBUTORS Mon May 25 12:04:43 2015 +0200 +++ b/CONTRIBUTORS Mon May 25 22:11:43 2015 +0200 @@ -3,6 +3,10 @@ who is listed as an author in one of the source files of this Isabelle distribution. +Contributions to this Isabelle version +-------------------------------------- + + Contributions to Isabelle2015 ----------------------------- diff -r 82453d0f49ee -r ff82ba1893c8 NEWS --- a/NEWS Mon May 25 12:04:43 2015 +0200 +++ b/NEWS Mon May 25 22:11:43 2015 +0200 @@ -3,6 +3,13 @@ (Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.) +New in this Isabelle version +---------------------------- + +*** HOL *** + +* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY. + New in Isabelle2015 (May 2015) ------------------------------ diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon May 25 22:11:43 2015 +0200 @@ -86,8 +86,8 @@ internal constructions and most of the internal proof obligations are omitted if the @{text quick_and_dirty} option is enabled.} The package is described in a number of papers -@{cite "traytel-et-al-2012" and "blanchette-et-al-wit" and - "blanchette-et-al-2014-impl" and "panny-et-al-2014"}. +@{cite "traytel-et-al-2012" and "blanchette-et-al-2014-impl" and +"panny-et-al-2014" and "blanchette-et-al-2015-wit"}. The central notion is that of a \emph{bounded natural functor} (BNF)---a well-behaved type constructor for which nested (co)recursion is supported. @@ -140,18 +140,10 @@ \newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak in.\allowbreak tum.\allowbreak de}} -\newcommand\authoremailii{\texttt{desh{\color{white}NOSPAM}\kern-\wd\boxA{}arna@\allowbreak -in.\allowbreak tum.\allowbreak de}} -\newcommand\authoremailiii{\texttt{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak -in.\allowbreak tum.\allowbreak de}} -\newcommand\authoremailiv{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak -in.\allowbreak tum.\allowbreak de}} -\newcommand\authoremailv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak -in.\allowbreak tum.\allowbreak de}} Comments and bug reports concerning either the package or this tutorial should -be directed to the authors at \authoremaili, \authoremailii, \authoremailiii, -\authoremailiv, and \authoremailv. +be directed to the first author at \authoremaili or to the +\texttt{cl-isabelle-users} mailing list. *} @@ -1645,7 +1637,7 @@ text {* \blankline *} lemma termi_TCons[simp]: "termi (TCons x xs) = termi xs" - by (cases xs) auto + by (cases xs) auto subsection {* Compatibility Issues @@ -2651,7 +2643,7 @@ text {* Bounded natural functors (BNFs) are a semantic criterion for where (co)re\-cur\-sion may appear on the right-hand side of an equation -@{cite "traytel-et-al-2012" and "blanchette-et-al-wit"}. +@{cite "traytel-et-al-2012" and "blanchette-et-al-2015-wit"}. An $n$-ary BNF is a type constructor equipped with a map function (functorial action), $n$ set functions (natural transformations), @@ -2689,9 +2681,9 @@ *} typedef ('d, 'a) fn = "UNIV \ ('d \ 'a) set" - by simp - - text {* \blankline *} + by simp + +text {* \blankline *} setup_lifting type_definition_fn @@ -3216,6 +3208,10 @@ \emph{The names of variables are often suboptimal in the properties generated by the package.} +\item +\emph{The compatibility layer sometimes produces induction principles with a +slightly different shape than the old package.} + \end{enumerate} *} @@ -3232,8 +3228,9 @@ from the \emph{Archive of Formal Proofs} to the new datatypes. Florian Haftmann and Christian Urban provided general advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder found an elegant proof that eliminated one of -the BNF proof obligations. Gerwin Klein, Andreas Lochbihler, Tobias Nipkow, and -Christian Sternagel suggested many textual improvements to this tutorial. +the BNF proof obligations. Mamoun Filali-Amine, Gerwin Klein, Andreas +Lochbihler, Tobias Nipkow, and Christian Sternagel suggested many textual +improvements to this tutorial. *} end diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Datatypes/document/root.tex --- a/src/Doc/Datatypes/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Datatypes/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[12pt,a4paper]{article} % fleqn +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{cite} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/How_to_Prove_it/document/prelude.tex --- a/src/Doc/How_to_Prove_it/document/prelude.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/How_to_Prove_it/document/prelude.tex Mon May 25 22:11:43 2015 +0200 @@ -5,6 +5,7 @@ \usepackage[bottom]{footmisc}% places footnotes at page bottom \usepackage{alltt} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Implementation/document/root.tex --- a/src/Doc/Implementation/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Implementation/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[12pt,a4paper,fleqn]{report} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{latexsym,graphicx} \usepackage[refpage]{nomencl} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Isar_Ref/document/root.tex --- a/src/Doc/Isar_Ref/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Isar_Ref/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[12pt,a4paper,fleqn]{report} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{amssymb} \usepackage{wasysym} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/JEdit/document/root.tex --- a/src/Doc/JEdit/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/JEdit/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[12pt,a4paper]{report} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{supertabular} \usepackage{graphicx} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Locales/document/root.tex --- a/src/Doc/Locales/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Locales/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[11pt,a4paper]{article} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{tikz} \usepackage{subfigure} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Main/document/root.tex --- a/src/Doc/Main/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Main/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[12pt,a4paper]{article} +\usepackage{lmodern} \usepackage[T1]{fontenc} \oddsidemargin=4.6mm diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Nitpick/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[a4paper,12pt]{article} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amssymb} @@ -2786,6 +2787,10 @@ \item[\labelitemi] All constants, types, free variables, and schematic variables whose names start with \textit{Nitpick}{.} are reserved for internal use. + +\item[\labelitemi] Some users report technical issues with the default SAT +solver on Windows. Setting the \textit{sat\_solver} option +(\S\ref{optimizations}) to \textit{MiniSat\_JNI} should solve this. \end{enum} \let\em=\sl diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[a4paper,12pt]{article} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amssymb} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/System/document/root.tex --- a/src/Doc/System/document/root.tex Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/System/document/root.tex Mon May 25 22:11:43 2015 +0200 @@ -1,4 +1,5 @@ \documentclass[12pt,a4paper]{report} +\usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{supertabular} \usepackage{graphicx} diff -r 82453d0f49ee -r ff82ba1893c8 src/Doc/manual.bib --- a/src/Doc/manual.bib Mon May 25 12:04:43 2015 +0200 +++ b/src/Doc/manual.bib Mon May 25 22:11:43 2015 +0200 @@ -332,11 +332,19 @@ author = "Jasmin Christian Blanchette and Tobias Nipkow", crossref = {itp2010}} -@unpublished{blanchette-et-al-wit, - author = {J. C. Blanchette and A. Popescu and D. Traytel}, - title = {Witnessing (Co)datatypes}, - year = 2014, - note = {\url{http://www21.in.tum.de/~blanchet/wit.pdf}}} +@inproceedings{blanchette-et-al-2015-wit, + author = {Jasmin Christian Blanchette and + Andrei Popescu and + Dmitriy Traytel}, + title = {Witnessing (Co)datatypes}, + booktitle = {{ESOP} 2015}, + pages = {359--382}, + year = {2015}, + editor = {Jan Vitek}, + series = {LNCS}, + volume = {9032}, + publisher = {Springer} +} @inproceedings{blanchette-et-al-2014-impl, author = "Jasmin Christian Blanchette and Johannes H{\"o}lzl diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Mon May 25 22:11:43 2015 +0200 @@ -2038,9 +2038,6 @@ using elems unfolding Cs apply (induct Cs', simp) - apply clarsimp - apply (subgoal_tac "\cs. (\x\set cs. P x) \ - multiset_of (map (assocs G) cs) = multiset_of Cs'") proof clarsimp fix a Cs' cs assume ih: "\X. X = a \ X \ set Cs' \ \x. P x \ X = assocs G x" @@ -2060,7 +2057,7 @@ show "\cs. (\x\set cs. P x) \ multiset_of (map (assocs G) cs) = multiset_of Cs' + {#a#}" by fast - qed simp + qed thus ?thesis by (simp add: fmset_def) qed diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Binomial.thy Mon May 25 22:11:43 2015 +0200 @@ -200,6 +200,13 @@ apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) done +lemma binomial_le_pow2: "n choose k \ 2^n" + apply (induction n arbitrary: k) + apply (simp add: binomial.simps) + apply (case_tac k) + apply (auto simp: power_Suc) + by (simp add: add_le_mono mult_2) + text{*The absorption property*} lemma Suc_times_binomial: "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)" @@ -700,6 +707,16 @@ shows "0 < k \ a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)" by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc) +lemma gchoose_row_sum_weighted: + fixes r :: "'a::field_char_0" + shows "(\k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))" +proof (induct m) + case 0 show ?case by simp +next + case (Suc m) + from Suc show ?case + by (simp add: algebra_simps distrib gbinomial_mult_1) +qed lemma binomial_symmetric: assumes kn: "k \ n" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Complete_Lattices.thy Mon May 25 22:11:43 2015 +0200 @@ -556,6 +556,14 @@ shows "(\x\A. f x) \ f (\A)" using `mono f` by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD) +lemma mono_INF: + "f (INF i : I. A i) \ (INF x : I. f (A x))" + by (intro complete_lattice_class.INF_greatest monoD[OF `mono f`] INF_lower) + +lemma mono_SUP: + "(SUP x : I. f (A x)) \ f (SUP i : I. A i)" + by (intro complete_lattice_class.SUP_least monoD[OF `mono f`] SUP_upper) + end end diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Mon May 25 22:11:43 2015 +0200 @@ -452,6 +452,9 @@ end +instance complete_linorder < conditionally_complete_linorder + .. + lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \ X \ {} \ Sup X = Max X" using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon May 25 22:11:43 2015 +0200 @@ -95,12 +95,12 @@ let val cring_ctxt = ctxt addsimps cring_simps; (*FIXME really the full simpset!?*) val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g); - val norm_eq_th = + val norm_eq_th = (* may collapse to True *) simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq}); in cut_tac norm_eq_th i THEN (simp_tac cring_ctxt i) - THEN (simp_tac cring_ctxt i) + THEN TRY(simp_tac cring_ctxt i) end); end; diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Deriv.thy Mon May 25 22:11:43 2015 +0200 @@ -609,6 +609,84 @@ lemma mult_commute_abs: "(\x. x * c) = op * (c::'a::ab_semigroup_mult)" by (simp add: fun_eq_iff mult.commute) +subsection {* Vector derivative *} + +lemma has_field_derivative_iff_has_vector_derivative: + "(f has_field_derivative y) F \ (f has_vector_derivative y) F" + unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs .. + +lemma has_field_derivative_subset: + "(f has_field_derivative y) (at x within s) \ t \ s \ (f has_field_derivative y) (at x within t)" + unfolding has_field_derivative_def by (rule has_derivative_subset) + +lemma has_vector_derivative_const[simp, derivative_intros]: "((\x. c) has_vector_derivative 0) net" + by (auto simp: has_vector_derivative_def) + +lemma has_vector_derivative_id[simp, derivative_intros]: "((\x. x) has_vector_derivative 1) net" + by (auto simp: has_vector_derivative_def) + +lemma has_vector_derivative_minus[derivative_intros]: + "(f has_vector_derivative f') net \ ((\x. - f x) has_vector_derivative (- f')) net" + by (auto simp: has_vector_derivative_def) + +lemma has_vector_derivative_add[derivative_intros]: + "(f has_vector_derivative f') net \ (g has_vector_derivative g') net \ + ((\x. f x + g x) has_vector_derivative (f' + g')) net" + by (auto simp: has_vector_derivative_def scaleR_right_distrib) + +lemma has_vector_derivative_setsum[derivative_intros]: + "(\i. i \ I \ (f i has_vector_derivative f' i) net) \ + ((\x. \i\I. f i x) has_vector_derivative (\i\I. f' i)) net" + by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_setsum_right intro!: derivative_eq_intros) + +lemma has_vector_derivative_diff[derivative_intros]: + "(f has_vector_derivative f') net \ (g has_vector_derivative g') net \ + ((\x. f x - g x) has_vector_derivative (f' - g')) net" + by (auto simp: has_vector_derivative_def scaleR_diff_right) + +lemma (in bounded_linear) has_vector_derivative: + assumes "(g has_vector_derivative g') F" + shows "((\x. f (g x)) has_vector_derivative f g') F" + using has_derivative[OF assms[unfolded has_vector_derivative_def]] + by (simp add: has_vector_derivative_def scaleR) + +lemma (in bounded_bilinear) has_vector_derivative: + assumes "(f has_vector_derivative f') (at x within s)" + and "(g has_vector_derivative g') (at x within s)" + shows "((\x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)" + using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]] + by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib) + +lemma has_vector_derivative_scaleR[derivative_intros]: + "(f has_field_derivative f') (at x within s) \ (g has_vector_derivative g') (at x within s) \ + ((\x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)" + unfolding has_field_derivative_iff_has_vector_derivative + by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR]) + +lemma has_vector_derivative_mult[derivative_intros]: + "(f has_vector_derivative f') (at x within s) \ (g has_vector_derivative g') (at x within s) \ + ((\x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)" + by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult]) + +lemma has_vector_derivative_of_real[derivative_intros]: + "(f has_field_derivative D) F \ ((\x. of_real (f x)) has_vector_derivative (of_real D)) F" + by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real]) + (simp add: has_field_derivative_iff_has_vector_derivative) + +lemma has_vector_derivative_continuous: "(f has_vector_derivative D) (at x within s) \ continuous (at x within s) f" + by (auto intro: has_derivative_continuous simp: has_vector_derivative_def) + +lemma has_vector_derivative_mult_right[derivative_intros]: + fixes a :: "'a :: real_normed_algebra" + shows "(f has_vector_derivative x) F \ ((\x. a * f x) has_vector_derivative (a * x)) F" + by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right]) + +lemma has_vector_derivative_mult_left[derivative_intros]: + fixes a :: "'a :: real_normed_algebra" + shows "(f has_vector_derivative x) F \ ((\x. f x * a) has_vector_derivative (x * a)) F" + by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left]) + + subsection {* Derivatives *} lemma DERIV_D: "DERIV f x :> D \ (\h. (f (x + h) - f x) / h) -- 0 --> D" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Extraction.thy Mon May 25 22:11:43 2015 +0200 @@ -32,7 +32,7 @@ induct_atomize induct_atomize' induct_rulify induct_rulify' induct_rulify_fallback induct_trueI True_implies_equals implies_True_equals TrueE - False_implies_equals + False_implies_equals implies_False_swap lemmas [extraction_expand_def] = HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Filter.thy --- a/src/HOL/Filter.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Filter.thy Mon May 25 22:11:43 2015 +0200 @@ -822,6 +822,11 @@ lemma filterlim_Suc: "filterlim Suc sequentially sequentially" by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq) +lemma filterlim_If: + "LIM x inf F (principal {x. P x}). f x :> G \ + LIM x inf F (principal {x. \ P x}). g x :> G \ + LIM x F. if P x then f x else g x :> G" + unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff) subsection {* Limits to @{const at_top} and @{const at_bot} *} diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/GCD.thy Mon May 25 22:11:43 2015 +0200 @@ -755,24 +755,16 @@ done lemma coprime_exp_nat: "coprime (d::nat) a \ coprime d (a^n)" - by (induct n, simp_all add: coprime_mult_nat) + by (induct n, simp_all add: power_Suc coprime_mult_nat) lemma coprime_exp_int: "coprime (d::int) a \ coprime d (a^n)" - by (induct n, simp_all add: coprime_mult_int) + by (induct n, simp_all add: power_Suc coprime_mult_int) lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \ coprime (a^n) (b^m)" - apply (rule coprime_exp_nat) - apply (subst gcd_commute_nat) - apply (rule coprime_exp_nat) - apply (subst gcd_commute_nat, assumption) -done + by (simp add: coprime_exp_nat gcd_nat.commute) lemma coprime_exp2_int [intro]: "coprime (a::int) b \ coprime (a^n) (b^m)" - apply (rule coprime_exp_int) - apply (subst gcd_commute_int) - apply (rule coprime_exp_int) - apply (subst gcd_commute_int, assumption) -done + by (simp add: coprime_exp_int gcd_int.commute) lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" proof (cases) @@ -783,24 +775,11 @@ by (auto simp:div_gcd_coprime_nat) hence "gcd ((a div gcd a b)^n * (gcd a b)^n) ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" - apply (subst (1 2) mult.commute) - apply (subst gcd_mult_distrib_nat [symmetric]) - apply simp - done + by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral) also have "(a div gcd a b)^n * (gcd a b)^n = a^n" - apply (subst div_power) - apply auto - apply (rule dvd_div_mult_self) - apply (rule dvd_power_same) - apply auto - done + by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) also have "(b div gcd a b)^n * (gcd a b)^n = b^n" - apply (subst div_power) - apply auto - apply (rule dvd_div_mult_self) - apply (rule dvd_power_same) - apply auto - done + by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) finally show ?thesis . qed @@ -908,7 +887,7 @@ have "a' dvd a'^n" by (simp add: m) with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp - hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute) + hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute power_Suc) from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1 have "a' dvd b'" by (subst (asm) mult.commute, blast) hence "a'*?g dvd b'*?g" by simp @@ -947,21 +926,13 @@ qed lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" - apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") - apply force - apply (rule dvd_diff_nat) - apply auto -done + by (simp add: gcd_nat.commute) lemma coprime_Suc_nat [simp]: "coprime (Suc n) n" using coprime_plus_one_nat by (simp add: One_nat_def) lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" - apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") - apply force - apply (rule dvd_diff) - apply auto -done + by (simp add: gcd_int.commute) lemma coprime_minus_one_nat: "(n::nat) \ 0 \ coprime (n - 1) n" using coprime_plus_one_nat [of "n - 1"] @@ -985,36 +956,23 @@ apply (auto simp add: gcd_mult_cancel_int) done -lemma coprime_common_divisor_nat: "coprime (a::nat) b \ x dvd a \ - x dvd b \ x = 1" - apply (subgoal_tac "x dvd gcd a b") - apply simp - apply (erule (1) gcd_greatest) -done +lemma coprime_common_divisor_nat: + "coprime (a::nat) b \ x dvd a \ x dvd b \ x = 1" + by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1) -lemma coprime_common_divisor_int: "coprime (a::int) b \ x dvd a \ - x dvd b \ abs x = 1" - apply (subgoal_tac "x dvd gcd a b") - apply simp - apply (erule (1) gcd_greatest) -done +lemma coprime_common_divisor_int: + "coprime (a::int) b \ x dvd a \ x dvd b \ abs x = 1" + using gcd_greatest by fastforce -lemma coprime_divisors_nat: "(d::int) dvd a \ e dvd b \ coprime a b \ - coprime d e" - apply (auto simp add: dvd_def) - apply (frule coprime_lmult_int) - apply (subst gcd_commute_int) - apply (subst (asm) (2) gcd_commute_int) - apply (erule coprime_lmult_int) -done +lemma coprime_divisors_nat: + "(d::int) dvd a \ e dvd b \ coprime a b \ coprime d e" + by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int) lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \ coprime x m" -apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) -done +by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) lemma invertible_coprime_int: "(x::int) * y mod m = 1 \ coprime x m" -apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) -done +by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) subsection {* Bezout's theorem *} diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/HOL.thy Mon May 25 22:11:43 2015 +0200 @@ -1270,6 +1270,12 @@ lemma False_implies_equals: "(False \ P) \ Trueprop True" by default simp_all +(* This is not made a simp rule because it does not improve any proofs + but slows some AFP entries down by 5% (cpu time). May 2015 *) +lemma implies_False_swap: "NO_MATCH (Trueprop False) P \ + (False \ PROP P \ PROP Q) \ (PROP P \ False \ PROP Q)" +by(rule swap_prems_eq) + lemma ex_simps: "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))" @@ -1292,7 +1298,8 @@ lemmas [simp] = triv_forall_equality (*prunes params*) - True_implies_equals (*prune asms `True'*) + True_implies_equals implies_True_equals (*prune True in asms*) + False_implies_equals (*prune False in asms*) if_True if_False if_cancel diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/HOLCF/FOCUS/Buffer_adm.thy --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Mon May 25 22:11:43 2015 +0200 @@ -22,8 +22,8 @@ (? d. ft\s=Def(Md d)) & (rt\s=<> | ft\(rt\s)=Def \ & rt\(rt\s):A))" by (unfold BufAC_Asm_F_def, auto) -lemma cont_BufAC_Asm_F: "down_continuous BufAC_Asm_F" -by (auto simp add: down_continuous_def BufAC_Asm_F_def3) +lemma cont_BufAC_Asm_F: "inf_continuous BufAC_Asm_F" +by (auto simp add: inf_continuous_def BufAC_Asm_F_def3) lemma BufAC_Cmt_F_def3: "((s,t):BufAC_Cmt_F C) = (!d x. @@ -37,8 +37,8 @@ apply (auto intro: surjectiv_scons [symmetric]) done -lemma cont_BufAC_Cmt_F: "down_continuous BufAC_Cmt_F" -by (auto simp add: down_continuous_def BufAC_Cmt_F_def3) +lemma cont_BufAC_Cmt_F: "inf_continuous BufAC_Cmt_F" +by (auto simp add: inf_continuous_def BufAC_Cmt_F_def3) (**** adm_BufAC_Asm ***********************************************************) @@ -184,7 +184,7 @@ lemma BufAC_Cmt_iterate_all: "(x\BufAC_Cmt) = (\n. x\(BufAC_Cmt_F ^^ n) top)" apply (unfold BufAC_Cmt_def) -apply (subst cont_BufAC_Cmt_F [THEN down_continuous_gfp]) +apply (subst cont_BufAC_Cmt_F [THEN inf_continuous_gfp]) apply (fast) done diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Mon May 25 22:11:43 2015 +0200 @@ -121,8 +121,8 @@ lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top; - down_continuous F |] ==> adm (%x. x:gfp F)" -apply (erule down_continuous_gfp[of F, THEN ssubst]) + inf_continuous F |] ==> adm (%x. x:gfp F)" +apply (erule inf_continuous_gfp[of F, THEN ssubst]) apply (simp (no_asm)) apply (rule adm_lemmas) apply (rule flatstream_admI) @@ -170,10 +170,10 @@ done lemma stream_antiP2_non_gfp_admI: -"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; down_continuous F |] +"!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; inf_continuous F |] ==> adm (%u. ~ u:gfp F)" apply (unfold adm_def) -apply (simp add: down_continuous_gfp) +apply (simp add: inf_continuous_gfp) apply (fast dest!: is_ub_thelub) done diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Mon May 25 22:11:43 2015 +0200 @@ -169,7 +169,7 @@ apply oghoare --\35 vc\ apply simp_all ---\21 vc\ +--\16 vc\ apply(tactic \ALLGOALS (clarify_tac @{context})\) --\11 vc\ apply simp_all @@ -191,7 +191,7 @@ apply force --\6 subgoals left\ prefer 6 -apply(erule_tac x=i in allE) +apply(erule_tac x=j in allE) apply fastforce --\5 subgoals left\ prefer 5 @@ -433,14 +433,14 @@ apply(tactic \ALLGOALS (clarify_tac @{context})\) --\112 subgoals left\ apply(simp_all (no_asm)) ---\97 subgoals left\ +--\43 subgoals left\ apply(tactic \ALLGOALS (conjI_Tac (K all_tac))\) ---\930 subgoals left\ +--\419 subgoals left\ apply(tactic \ALLGOALS (clarify_tac @{context})\) --\99 subgoals left\ -apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym]) +apply(simp_all only:length_0_conv [THEN sym]) --\20 subgoals left\ -apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma) +apply (simp_all del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma) --\9 subgoals left\ apply (force simp add:less_Suc_eq) apply(hypsubst_thin, drule sym) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/IMP/BExp.thy --- a/src/HOL/IMP/BExp.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/IMP/BExp.thy Mon May 25 22:11:43 2015 +0200 @@ -16,15 +16,6 @@ <''x'' := 3, ''y'' := 1>" -text{* To improve automation: *} - -lemma bval_And_if[simp]: - "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" -by(simp) - -declare bval.simps(3)[simp del] --"remove the original eqn" - - subsection "Constant Folding" text{* Optimizing constructors: *} diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Inductive.thy Mon May 25 22:11:43 2015 +0200 @@ -56,32 +56,10 @@ subsection {* General induction rules for least fixed points *} -theorem lfp_induct: - assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P" - shows "lfp f <= P" -proof - - have "inf (lfp f) P <= lfp f" by (rule inf_le1) - with mono have "f (inf (lfp f) P) <= f (lfp f)" .. - also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric]) - finally have "f (inf (lfp f) P) <= lfp f" . - from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI) - hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound) - also have "inf (lfp f) P <= P" by (rule inf_le2) - finally show ?thesis . -qed - -lemma lfp_induct_set: - assumes lfp: "a: lfp(f)" - and mono: "mono(f)" - and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" - shows "P(a)" - by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) - (auto simp: intro: indhyp) - -lemma lfp_ordinal_induct: +lemma lfp_ordinal_induct[case_names mono step union]: fixes f :: "'a\complete_lattice \ 'a" assumes mono: "mono f" - and P_f: "\S. P S \ P (f S)" + and P_f: "\S. P S \ S \ lfp f \ P (f S)" and P_Union: "\M. \S\M. P S \ P (Sup M)" shows "P (lfp f)" proof - @@ -92,13 +70,29 @@ show "Sup ?M \ lfp f" by (blast intro: Sup_least) hence "f (Sup ?M) \ f (lfp f)" by (rule mono [THEN monoD]) hence "f (Sup ?M) \ lfp f" using mono [THEN lfp_unfold] by simp - hence "f (Sup ?M) \ ?M" using P_f P_Union by simp + hence "f (Sup ?M) \ ?M" using P_Union by simp (intro P_f Sup_least, auto) hence "f (Sup ?M) \ Sup ?M" by (rule Sup_upper) thus "lfp f \ Sup ?M" by (rule lfp_lowerbound) qed finally show ?thesis . qed +theorem lfp_induct: + assumes mono: "mono f" and ind: "f (inf (lfp f) P) \ P" + shows "lfp f \ P" +proof (induction rule: lfp_ordinal_induct) + case (step S) then show ?case + by (intro order_trans[OF _ ind] monoD[OF mono]) auto +qed (auto intro: mono Sup_least) + +lemma lfp_induct_set: + assumes lfp: "a: lfp(f)" + and mono: "mono(f)" + and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" + shows "P(a)" + by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) + (auto simp: intro: indhyp) + lemma lfp_ordinal_induct_set: assumes mono: "mono f" and P_f: "!!S. P S ==> P(f S)" @@ -179,17 +173,35 @@ lemma coinduct_set: "[| mono(f); a: X; X \ f(X Un gfp(f)) |] ==> a : gfp(f)" by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+ -lemma coinduct: "[| mono(f); X \ f (sup X (gfp f)) |] ==> X \ gfp(f)" - apply (rule order_trans) - apply (rule sup_ge1) - apply (rule gfp_upperbound) - apply (erule coinduct_lemma) - apply assumption - done - lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))" by (blast dest: gfp_lemma2 mono_Un) +lemma gfp_ordinal_induct[case_names mono step union]: + fixes f :: "'a\complete_lattice \ 'a" + assumes mono: "mono f" + and P_f: "\S. P S \ gfp f \ S \ P (f S)" + and P_Union: "\M. \S\M. P S \ P (Inf M)" + shows "P (gfp f)" +proof - + let ?M = "{S. gfp f \ S \ P S}" + have "P (Inf ?M)" using P_Union by simp + also have "Inf ?M = gfp f" + proof (rule antisym) + show "gfp f \ Inf ?M" by (blast intro: Inf_greatest) + hence "f (gfp f) \ f (Inf ?M)" by (rule mono [THEN monoD]) + hence "gfp f \ f (Inf ?M)" using mono [THEN gfp_unfold] by simp + hence "f (Inf ?M) \ ?M" using P_Union by simp (intro P_f Inf_greatest, auto) + hence "Inf ?M \ f (Inf ?M)" by (rule Inf_lower) + thus "Inf ?M \ gfp f" by (rule gfp_upperbound) + qed + finally show ?thesis . +qed + +lemma coinduct: assumes mono: "mono f" and ind: "X \ f (sup X (gfp f))" shows "X \ gfp f" +proof (induction rule: gfp_ordinal_induct) + case (step S) then show ?case + by (intro order_trans[OF ind _] monoD[OF mono]) auto +qed (auto intro: mono Inf_greatest) subsection {* Even Stronger Coinduction Rule, by Martin Coen *} @@ -248,6 +260,103 @@ lemma gfp_mono: "(!!Z. f Z \ g Z) ==> gfp f \ gfp g" by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) +subsection {* Rules for fixed point calculus *} + + +lemma lfp_rolling: + assumes "mono g" "mono f" + shows "g (lfp (\x. f (g x))) = lfp (\x. g (f x))" +proof (rule antisym) + have *: "mono (\x. f (g x))" + using assms by (auto simp: mono_def) + + show "lfp (\x. g (f x)) \ g (lfp (\x. f (g x)))" + by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric]) + + show "g (lfp (\x. f (g x))) \ lfp (\x. g (f x))" + proof (rule lfp_greatest) + fix u assume "g (f u) \ u" + moreover then have "g (lfp (\x. f (g x))) \ g (f u)" + by (intro assms[THEN monoD] lfp_lowerbound) + ultimately show "g (lfp (\x. f (g x))) \ u" + by auto + qed +qed + +lemma lfp_square: + assumes "mono f" shows "lfp f = lfp (\x. f (f x))" +proof (rule antisym) + show "lfp f \ lfp (\x. f (f x))" + by (intro lfp_lowerbound) (simp add: assms lfp_rolling) + show "lfp (\x. f (f x)) \ lfp f" + by (intro lfp_lowerbound) (simp add: lfp_unfold[OF assms, symmetric]) +qed + +lemma lfp_lfp: + assumes f: "\x y w z. x \ y \ w \ z \ f x w \ f y z" + shows "lfp (\x. lfp (f x)) = lfp (\x. f x x)" +proof (rule antisym) + have *: "mono (\x. f x x)" + by (blast intro: monoI f) + show "lfp (\x. lfp (f x)) \ lfp (\x. f x x)" + by (intro lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric]) + show "lfp (\x. lfp (f x)) \ lfp (\x. f x x)" (is "?F \ _") + proof (intro lfp_lowerbound) + have *: "?F = lfp (f ?F)" + by (rule lfp_unfold) (blast intro: monoI lfp_mono f) + also have "\ = f ?F (lfp (f ?F))" + by (rule lfp_unfold) (blast intro: monoI lfp_mono f) + finally show "f ?F ?F \ ?F" + by (simp add: *[symmetric]) + qed +qed + +lemma gfp_rolling: + assumes "mono g" "mono f" + shows "g (gfp (\x. f (g x))) = gfp (\x. g (f x))" +proof (rule antisym) + have *: "mono (\x. f (g x))" + using assms by (auto simp: mono_def) + show "g (gfp (\x. f (g x))) \ gfp (\x. g (f x))" + by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric]) + + show "gfp (\x. g (f x)) \ g (gfp (\x. f (g x)))" + proof (rule gfp_least) + fix u assume "u \ g (f u)" + moreover then have "g (f u) \ g (gfp (\x. f (g x)))" + by (intro assms[THEN monoD] gfp_upperbound) + ultimately show "u \ g (gfp (\x. f (g x)))" + by auto + qed +qed + +lemma gfp_square: + assumes "mono f" shows "gfp f = gfp (\x. f (f x))" +proof (rule antisym) + show "gfp (\x. f (f x)) \ gfp f" + by (intro gfp_upperbound) (simp add: assms gfp_rolling) + show "gfp f \ gfp (\x. f (f x))" + by (intro gfp_upperbound) (simp add: gfp_unfold[OF assms, symmetric]) +qed + +lemma gfp_gfp: + assumes f: "\x y w z. x \ y \ w \ z \ f x w \ f y z" + shows "gfp (\x. gfp (f x)) = gfp (\x. f x x)" +proof (rule antisym) + have *: "mono (\x. f x x)" + by (blast intro: monoI f) + show "gfp (\x. f x x) \ gfp (\x. gfp (f x))" + by (intro gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric]) + show "gfp (\x. gfp (f x)) \ gfp (\x. f x x)" (is "?F \ _") + proof (intro gfp_upperbound) + have *: "?F = gfp (f ?F)" + by (rule gfp_unfold) (blast intro: monoI gfp_mono f) + also have "\ = f ?F (gfp (f ?F))" + by (rule gfp_unfold) (blast intro: monoI gfp_mono f) + finally show "?F \ f ?F ?F" + by (simp add: *[symmetric]) + qed +qed subsection {* Inductive predicates and sets *} diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Inequalities.thy --- a/src/HOL/Inequalities.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Inequalities.thy Mon May 25 22:11:43 2015 +0200 @@ -7,38 +7,22 @@ imports Real_Vector_Spaces begin -lemma setsum_triangle_reindex: - fixes n :: nat - shows "(\(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))" - apply (simp add: setsum.Sigma) - apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"]) - apply auto - done - -lemma gauss_sum_div2: "(2::'a::semiring_div) \ 0 \ - setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)" -using gauss_sum[where n=n and 'a = 'a,symmetric] by auto - -lemma Setsum_Icc_int: assumes "0 \ m" and "(m::int) \ n" -shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" -proof- - { fix k::int assume "k\0" - hence "\ {1..k::int} = k * (k+1) div 2" - by (rule gauss_sum_div2[where 'a = int, transferred]) simp - } note 1 = this - have "{m..n} = {0..n} - {0..m-1}" using `m\0` by auto - hence "\{m..n} = \{0..n} - \{0..m-1}" using assms - by (force intro!: setsum_diff) - also have "{0..n} = {0} Un {1..n}" using assms by auto - also have "\({0} \ {1..n}) = \{1..n}" by(simp add: setsum.union_disjoint) - also have "\ = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]]) - also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})" - using assms by auto - also have "\ \ = m*(m-1) div 2" using `m\0` by(simp add: 1 mult.commute) - also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2" - apply(subgoal_tac "even(n*(n+1)) \ even(m*(m-1))") - by (auto (*simp: even_def[symmetric]*)) - finally show ?thesis . +lemma Setsum_Icc_int: "(m::int) \ n \ \ {m..n} = (n*(n+1) - m*(m-1)) div 2" +proof(induct i == "nat(n-m)" arbitrary: m n) + case 0 + hence "m = n" by arith + thus ?case by (simp add: algebra_simps) +next + case (Suc i) + have 0: "i = nat((n-1) - m)" "m \ n-1" using Suc(2,3) by arith+ + have "\ {m..n} = \ {m..1+(n-1)}" by simp + also have "\ = \ {m..n-1} + n" using `m \ n` + by(subst atLeastAtMostPlus1_int_conv) simp_all + also have "\ = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" + by(simp add: Suc(1)[OF 0]) + also have "\ = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp + also have "\ = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps) + finally show ?case . qed lemma Setsum_Icc_nat: assumes "(m::nat) \ n" @@ -47,7 +31,7 @@ have "m*(m-1) \ n*(n + 1)" using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) hence "int(\ {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms - by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult + by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult split: zdiff_int_split) thus ?thesis by simp qed diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Int.thy --- a/src/HOL/Int.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Int.thy Mon May 25 22:11:43 2015 +0200 @@ -3,7 +3,7 @@ Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *) -section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} +section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} theory Int imports Equiv_Relations Power Quotient Fun_Def @@ -338,10 +338,10 @@ text{*An alternative condition is @{term "0 \ w"} *} corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" -by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) +by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) corollary nat_less_eq_zless: "0 \ w ==> (nat w < nat z) = (w (if 0 \ w then w = int m else m = 0)" by transfer (clarsimp simp add: le_imp_diff_is_add) - + corollary nat_eq_iff2: "m = nat w \ (if 0 \ w then w = int m else m = 0)" using nat_eq_iff [of w m] by auto @@ -378,7 +378,7 @@ lemma nat_2: "nat 2 = Suc (Suc 0)" by simp - + lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < of_nat m)" by transfer (clarsimp, arith) @@ -404,7 +404,7 @@ lemma nat_diff_distrib': "0 \ x \ 0 \ y \ nat (x - y) = nat x - nat y" by transfer clarsimp - + lemma nat_diff_distrib: "0 \ z' \ z' \ z \ nat (z - z') = nat z - nat z'" by (rule nat_diff_distrib') auto @@ -415,7 +415,7 @@ lemma le_nat_iff: "k \ 0 \ n \ nat k \ int n \ k" by transfer auto - + lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" by transfer (clarsimp simp add: less_diff_conv) @@ -427,7 +427,7 @@ end -lemma diff_nat_numeral [simp]: +lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) @@ -550,7 +550,7 @@ text {* Preliminaries *} -lemma le_imp_0_less: +lemma le_imp_0_less: assumes le: "0 \ z" shows "(0::int) < 1 + z" proof - @@ -565,7 +565,7 @@ proof (cases z) case (nonneg n) thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing - le_imp_0_less [THEN order_less_imp_le]) + le_imp_0_less [THEN order_less_imp_le]) next case (neg n) thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 @@ -580,19 +580,19 @@ "1 + z + z \ (0::int)" proof (cases z) case (nonneg n) - have le: "0 \ z+z" by (simp add: nonneg add_increasing) + have le: "0 \ z+z" by (simp add: nonneg add_increasing) thus ?thesis using le_imp_0_less [OF le] - by (auto simp add: add.assoc) + by (auto simp add: add.assoc) next case (neg n) show ?thesis proof assume eq: "1 + z + z = 0" have "(0::int) < 1 + (int n + int n)" - by (simp add: le_imp_0_less add_increasing) - also have "... = - (1 + z + z)" - by (simp add: neg add.assoc [symmetric]) - also have "... = 0" by (simp add: eq) + by (simp add: le_imp_0_less add_increasing) + also have "... = - (1 + z + z)" + by (simp add: neg add.assoc [symmetric]) + also have "... = 0" by (simp add: eq) finally have "0<0" .. thus False by blast qed @@ -699,12 +699,12 @@ hence "1 + z + z = 0" by (simp only: of_int_eq_iff) with odd_nonzero show False by blast qed -qed +qed lemma Nats_numeral [simp]: "numeral w \ Nats" using of_nat_in_Nats [of "numeral w"] by simp -lemma Ints_odd_less_0: +lemma Ints_odd_less_0: assumes in_Ints: "a \ Ints" shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" proof - @@ -787,9 +787,7 @@ text{*Simplify the term @{term "w + - z"}*} lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" -apply (insert zless_nat_conj [of 1 z]) -apply auto -done + using zless_nat_conj [of 1 z] by auto text{*This simplifies expressions of the form @{term "int n = z"} where z is an integer literal.*} @@ -857,7 +855,7 @@ lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" apply (cases "z=0 | w=0") -apply (auto simp add: abs_if nat_mult_distrib [symmetric] +apply (auto simp add: abs_if nat_mult_distrib [symmetric] nat_mult_distrib_neg [symmetric] mult_less_0_iff) done @@ -867,9 +865,9 @@ done lemma diff_nat_eq_if: - "nat z - nat z' = - (if z' < 0 then nat z - else let d = z-z' in + "nat z - nat z' = + (if z' < 0 then nat z + else let d = z-z' in if d < 0 then 0 else nat d)" by (simp add: Let_def nat_diff_distrib [symmetric]) @@ -891,8 +889,8 @@ proof - have "int_ge_less_than d \ measure (%z. nat (z-d))" by (auto simp add: int_ge_less_than_def) - thus ?thesis - by (rule wf_subset [OF wf_measure]) + thus ?thesis + by (rule wf_subset [OF wf_measure]) qed text{*This variant looks odd, but is typical of the relations suggested @@ -905,10 +903,10 @@ theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" proof - - have "int_ge_less_than2 d \ measure (%z. nat (1+z-d))" + have "int_ge_less_than2 d \ measure (%z. nat (1+z-d))" by (auto simp add: int_ge_less_than2_def) - thus ?thesis - by (rule wf_subset [OF wf_measure]) + thus ?thesis + by (rule wf_subset [OF wf_measure]) qed (* `set:int': dummy construction *) @@ -1009,7 +1007,7 @@ subsection{*Intermediate value theorems*} lemma int_val_lemma: - "(\i 1) --> + "(\i 1) --> f 0 \ k --> k \ f n --> (\i \ n. f i = (k::int))" unfolding One_nat_def apply (induct n) @@ -1027,9 +1025,9 @@ lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] lemma nat_intermed_int_val: - "[| \i. m \ i & i < n --> abs(f(i + 1::nat) - f i) \ 1; m < n; + "[| \i. m \ i & i < n --> abs(f(i + 1::nat) - f i) \ 1; m < n; f m \ k; k \ f n |] ==> ? i. m \ i & i \ n & f i = (k::int)" -apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k +apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k in int_val_lemma) unfolding One_nat_def apply simp @@ -1053,8 +1051,8 @@ proof assume "2 \ \m\" hence "2*\n\ \ \m\*\n\" - by (simp add: mult_mono 0) - also have "... = \m*n\" + by (simp add: mult_mono 0) + also have "... = \m*n\" by (simp add: abs_mult) also have "... = 1" by (simp add: mn) @@ -1077,10 +1075,10 @@ qed lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))" -apply (rule iffI) +apply (rule iffI) apply (frule pos_zmult_eq_1_iff_lemma) - apply (simp add: mult.commute [of m]) - apply (frule pos_zmult_eq_1_iff_lemma, auto) + apply (simp add: mult.commute [of m]) + apply (frule pos_zmult_eq_1_iff_lemma, auto) done lemma infinite_UNIV_int: "\ finite (UNIV::int set)" @@ -1226,14 +1224,14 @@ apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff) done -lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" +lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" shows "\a\ = \b\" proof cases assume "a = 0" with assms show ?thesis by simp next assume "a \ 0" - from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast - from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast + from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast + from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast from k k' have "a = a*k*k'" by simp with mult_cancel_left1[where c="a" and b="k*k'"] have kk':"k*k' = 1" using `a\0` by (simp add: mult.assoc) @@ -1242,7 +1240,7 @@ qed lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" - using dvd_add_right_iff [of k "- n" m] by simp + using dvd_add_right_iff [of k "- n" m] by simp lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps) @@ -1317,10 +1315,10 @@ then show "x dvd 1" by (auto intro: dvdI) qed -lemma zdvd_mult_cancel1: +lemma zdvd_mult_cancel1: assumes mp:"m \(0::int)" shows "(m * n dvd m) = (\n\ = 1)" proof - assume n1: "\n\ = 1" thus "m * n dvd m" + assume n1: "\n\ = 1" thus "m * n dvd m" by (cases "n >0") (auto simp add: minus_equation_iff) next assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Library/BigO.thy Mon May 25 22:11:43 2015 +0200 @@ -870,7 +870,7 @@ apply (drule bigo_LIMSEQ1) apply assumption apply (simp only: fun_diff_def) - apply (erule LIMSEQ_diff_approach_zero2) + apply (erule Lim_transform2) apply assumption done diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/Convex.thy --- a/src/HOL/Library/Convex.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Library/Convex.thy Mon May 25 22:11:43 2015 +0200 @@ -389,6 +389,16 @@ using `convex s` by (rule convex_linear_image) qed +lemma convex_scaled: + assumes "convex s" + shows "convex ((\x. x *\<^sub>R c) ` s)" +proof - + have "linear (\x. x *\<^sub>R c)" + by (simp add: linearI scaleR_add_left) + then show ?thesis + using `convex s` by (rule convex_linear_image) +qed + lemma convex_negations: assumes "convex s" shows "convex ((\x. - x) ` s)" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Library/Extended_Real.thy Mon May 25 22:11:43 2015 +0200 @@ -8,16 +8,90 @@ section {* Extended real number line *} theory Extended_Real -imports Complex_Main Extended_Nat Liminf_Limsup +imports Complex_Main Extended_Nat Liminf_Limsup Order_Continuity begin text {* -This should be part of @{theory Extended_Nat}, but then the AFP-entry @{text "Jinja_Thread"} fails, as it does -overload certain named from @{theory Complex_Main}. +This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the +AFP-entry @{text "Jinja_Thread"} fails, as it does overload certain named from @{theory Complex_Main}. *} +lemma continuous_at_left_imp_sup_continuous: + fixes f :: "'a \ 'a::{complete_linorder, linorder_topology}" + assumes "mono f" "\x. continuous (at_left x) f" + shows "sup_continuous f" + unfolding sup_continuous_def +proof safe + fix M :: "nat \ 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))" + using continuous_at_Sup_mono[OF assms, of "range M"] by simp +qed + +lemma sup_continuous_at_left: + fixes f :: "'a \ 'a::{complete_linorder, linorder_topology, first_countable_topology}" + assumes f: "sup_continuous f" + shows "continuous (at_left x) f" +proof cases + assume "x = bot" then show ?thesis + by (simp add: trivial_limit_at_left_bot) +next + assume x: "x \ bot" + show ?thesis + unfolding continuous_within + proof (intro tendsto_at_left_sequentially[of bot]) + fix S :: "nat \ 'a" assume S: "incseq S" and S_x: "S ----> x" + from S_x have x_eq: "x = (SUP i. S i)" + by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S) + show "(\n. f (S n)) ----> f x" + unfolding x_eq sup_continuousD[OF f S] + using S sup_continuous_mono[OF f] by (intro LIMSEQ_SUP) (auto simp: mono_def) + qed (insert x, auto simp: bot_less) +qed + +lemma sup_continuous_iff_at_left: + fixes f :: "'a \ 'a::{complete_linorder, linorder_topology, first_countable_topology}" + shows "sup_continuous f \ (\x. continuous (at_left x) f) \ mono f" + using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f] + sup_continuous_mono[of f] by auto + +lemma continuous_at_right_imp_inf_continuous: + fixes f :: "'a \ 'a::{complete_linorder, linorder_topology}" + assumes "mono f" "\x. continuous (at_right x) f" + shows "inf_continuous f" + unfolding inf_continuous_def +proof safe + fix M :: "nat \ 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))" + using continuous_at_Inf_mono[OF assms, of "range M"] by simp +qed + +lemma inf_continuous_at_right: + fixes f :: "'a \ 'a::{complete_linorder, linorder_topology, first_countable_topology}" + assumes f: "inf_continuous f" + shows "continuous (at_right x) f" +proof cases + assume "x = top" then show ?thesis + by (simp add: trivial_limit_at_right_top) +next + assume x: "x \ top" + show ?thesis + unfolding continuous_within + proof (intro tendsto_at_right_sequentially[of _ top]) + fix S :: "nat \ 'a" assume S: "decseq S" and S_x: "S ----> x" + from S_x have x_eq: "x = (INF i. S i)" + by (rule LIMSEQ_unique) (intro LIMSEQ_INF S) + show "(\n. f (S n)) ----> f x" + unfolding x_eq inf_continuousD[OF f S] + using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def) + qed (insert x, auto simp: less_top) +qed + +lemma inf_continuous_iff_at_right: + fixes f :: "'a \ 'a::{complete_linorder, linorder_topology, first_countable_topology}" + shows "inf_continuous f \ (\x. continuous (at_right x) f) \ mono f" + using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f] + inf_continuous_mono[of f] by auto + instantiation enat :: linorder_topology begin diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Mon May 25 22:11:43 2015 +0200 @@ -742,32 +742,28 @@ by (auto simp add: expand_fps_eq) qed -lemma fps_inverse_gp: "inverse (Abs_fps(\n. (1::'a::field))) - = Abs_fps (\n. if n= 0 then 1 else if n=1 then - 1 else 0)" - apply (rule fps_inverse_unique) - apply simp - apply (simp add: fps_eq_iff fps_mult_nth) - apply clarsimp +lemma setsum_zero_lemma: + fixes n::nat + assumes "0 < n" + shows "(\i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)" proof - - fix n :: nat - assume n: "n > 0" - let ?f = "\i. if n = i then (1::'a) else if n - i = 1 then - 1 else 0" - let ?g = "\i. if i = n then 1 else if i=n - 1 then - 1 else 0" + let ?f = "\i. if n = i then 1 else if n - i = 1 then - 1 else 0" + let ?g = "\i. if i = n then 1 else if i = n - 1 then - 1 else 0" let ?h = "\i. if i=n - 1 then - 1 else 0" have th1: "setsum ?f {0..n} = setsum ?g {0..n}" by (rule setsum.cong) auto have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}" - apply (insert n) apply (rule setsum.cong) + using assms apply auto done have eq: "{0 .. n} = {0.. n - 1} \ {n}" by auto - from n have d: "{0.. n - 1} \ {n} = {}" + from assms have d: "{0.. n - 1} \ {n} = {}" by auto have f: "finite {0.. n - 1}" "finite {n}" by auto - show "setsum ?f {0..n} = 0" + show ?thesis unfolding th1 apply (simp add: setsum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) unfolding th2 @@ -775,6 +771,12 @@ done qed +lemma fps_inverse_gp: "inverse (Abs_fps(\n. (1::'a::field))) + = Abs_fps (\n. if n= 0 then 1 else if n=1 then - 1 else 0)" + apply (rule fps_inverse_unique) + apply (simp_all add: fps_eq_iff fps_mult_nth setsum_zero_lemma) + done + subsection {* Formal Derivatives, and the MacLaurin theorem around 0 *} @@ -2885,8 +2887,7 @@ unfolding th using fact_gt_zero apply (simp add: field_simps del: of_nat_Suc fact_Suc) - apply (drule sym) - apply (simp add: field_simps of_nat_mult) + apply simp done } note th' = this @@ -2894,11 +2895,7 @@ next assume h: ?rhs show ?lhs - apply (subst h) - apply simp - apply (simp only: h[symmetric]) - apply simp - done + by (metis E_deriv fps_deriv_mult_const_left h mult.left_commute) qed lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r") @@ -2949,16 +2946,6 @@ apply auto done -lemma inverse_one_plus_X: - "inverse (1 + X) = Abs_fps (\n. (- 1 ::'a::field)^n)" - (is "inverse ?l = ?r") -proof - - have th: "?l * ?r = 1" - by (auto simp add: field_simps fps_eq_iff minus_one_power_iff) - have th': "?l $ 0 \ 0" by (simp add: ) - from fps_inverse_unique[OF th' th] show ?thesis . -qed - lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)" by (induct n) (auto simp add: field_simps E_add_mult) @@ -2993,7 +2980,7 @@ where "L c = fps_const (1/c) * Abs_fps (\n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)" lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)" - unfolding inverse_one_plus_X + unfolding fps_inverse_X_plus1 by (simp add: L_def fps_eq_iff del: of_nat_Suc) lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))" @@ -3438,12 +3425,6 @@ finally show ?thesis . qed -lemma divide_eq_iff: "a \ (0::'a::field) \ x / a = y \ x = y * a" - by auto - -lemma eq_divide_iff: "a \ (0::'a::field) \ x = y / a \ x * a = y" - by auto - lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0" unfolding fps_sin_def by simp @@ -3454,7 +3435,7 @@ "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))" unfolding fps_sin_def apply (cases n, simp) - apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc) + apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc) apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc) done @@ -3467,7 +3448,7 @@ lemma fps_cos_nth_add_2: "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))" unfolding fps_cos_def - apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc) + apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc) apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc) done @@ -3500,7 +3481,7 @@ apply (simp add: nat_add_1_add_1 fps_sin_nth_add_2 del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc') apply (subst minus_divide_left) - apply (subst eq_divide_iff) + apply (subst nonzero_eq_divide_eq) apply (simp del: of_nat_add of_nat_Suc) apply (simp only: ac_simps) done @@ -3518,7 +3499,7 @@ apply (simp add: nat_add_1_add_1 fps_cos_nth_add_2 del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc') apply (subst minus_divide_left) - apply (subst eq_divide_iff) + apply (subst nonzero_eq_divide_eq) apply (simp del: of_nat_add of_nat_Suc) apply (simp only: ac_simps) done @@ -3793,7 +3774,8 @@ THEN spec, of "\x. x < e"] have "eventually (\i. inverse (2 ^ i) < e) sequentially" unfolding eventually_nhds - apply safe + apply clarsimp + apply (rule FalseE) apply auto --{*slow*} done then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Library/Library.thy Mon May 25 22:11:43 2015 +0200 @@ -44,7 +44,6 @@ More_List Multiset_Order Numeral_Type - NthRoot_Limits OptionalSugar Option_ord Order_Continuity @@ -55,6 +54,7 @@ Polynomial Preorder Product_Vector + Quadratic_Discriminant Quotient_List Quotient_Option Quotient_Product diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/NthRoot_Limits.thy --- a/src/HOL/Library/NthRoot_Limits.thy Mon May 25 12:04:43 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,88 +0,0 @@ -theory NthRoot_Limits - imports Complex_Main -begin - -lemma LIMSEQ_root: "(\n. root n n) ----> 1" -proof - - def x \ "\n. root n n - 1" - have "x ----> sqrt 0" - proof (rule tendsto_sandwich[OF _ _ tendsto_const]) - show "(\x. sqrt (2 / x)) ----> sqrt 0" - by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) - (simp_all add: at_infinity_eq_at_top_bot) - { fix n :: nat assume "2 < n" - have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2" - using `2 < n` unfolding gbinomial_def binomial_gbinomial - by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric]) - also have "\ \ (\k\{0, 2}. of_nat (n choose k) * x n^k)" - by (simp add: x_def) - also have "\ \ (\k=0..n. of_nat (n choose k) * x n^k)" - using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) - also have "\ = (x n + 1) ^ n" - by (simp add: binomial_ring) - also have "\ = n" - using `2 < n` by (simp add: x_def) - finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \ real (n - 1) * 1" - by simp - then have "(x n)\<^sup>2 \ 2 / real n" - using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps) - from real_sqrt_le_mono[OF this] have "x n \ sqrt (2 / real n)" - by simp } - then show "eventually (\n. x n \ sqrt (2 / real n)) sequentially" - by (auto intro!: exI[of _ 3] simp: eventually_sequentially) - show "eventually (\n. sqrt 0 \ x n) sequentially" - by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) - qed - from tendsto_add[OF this tendsto_const[of 1]] show ?thesis - by (simp add: x_def) -qed - -lemma LIMSEQ_root_const: - assumes "0 < c" - shows "(\n. root n c) ----> 1" -proof - - { fix c :: real assume "1 \ c" - def x \ "\n. root n c - 1" - have "x ----> 0" - proof (rule tendsto_sandwich[OF _ _ tendsto_const]) - show "(\n. c / n) ----> 0" - by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) - (simp_all add: at_infinity_eq_at_top_bot) - { fix n :: nat assume "1 < n" - have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1" - using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric]) - also have "\ \ (\k\{0, 1}. of_nat (n choose k) * x n^k)" - by (simp add: x_def) - also have "\ \ (\k=0..n. of_nat (n choose k) * x n^k)" - using `1 < n` `1 \ c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) - also have "\ = (x n + 1) ^ n" - by (simp add: binomial_ring) - also have "\ = c" - using `1 < n` `1 \ c` by (simp add: x_def) - finally have "x n \ c / n" - using `1 \ c` `1 < n` by (simp add: field_simps) } - then show "eventually (\n. x n \ c / n) sequentially" - by (auto intro!: exI[of _ 3] simp: eventually_sequentially) - show "eventually (\n. 0 \ x n) sequentially" - using `1 \ c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) - qed - from tendsto_add[OF this tendsto_const[of 1]] have "(\n. root n c) ----> 1" - by (simp add: x_def) } - note ge_1 = this - - show ?thesis - proof cases - assume "1 \ c" with ge_1 show ?thesis by blast - next - assume "\ 1 \ c" - with `0 < c` have "1 \ 1 / c" - by simp - then have "(\n. 1 / root n (1 / c)) ----> 1 / 1" - by (intro tendsto_divide tendsto_const ge_1 `1 \ 1 / c` one_neq_zero) - then show ?thesis - by (rule filterlim_cong[THEN iffD1, rotated 3]) - (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide) - qed -qed - -end diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/Order_Continuity.thy --- a/src/HOL/Library/Order_Continuity.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Library/Order_Continuity.thy Mon May 25 22:11:43 2015 +0200 @@ -28,32 +28,38 @@ apply simp_all done +text \ + The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use + @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature + and have the advantage that these names are duals. +\ + subsection {* Continuity for complete lattices *} definition - continuous :: "('a::complete_lattice \ 'a::complete_lattice) \ bool" where - "continuous F \ (\M::nat \ 'a. mono M \ F (SUP i. M i) = (SUP i. F (M i)))" + sup_continuous :: "('a::complete_lattice \ 'a::complete_lattice) \ bool" where + "sup_continuous F \ (\M::nat \ 'a. mono M \ F (SUP i. M i) = (SUP i. F (M i)))" -lemma continuousD: "continuous F \ mono M \ F (SUP i::nat. M i) = (SUP i. F (M i))" - by (auto simp: continuous_def) +lemma sup_continuousD: "sup_continuous F \ mono M \ F (SUP i::nat. M i) = (SUP i. F (M i))" + by (auto simp: sup_continuous_def) -lemma continuous_mono: +lemma sup_continuous_mono: fixes F :: "'a::complete_lattice \ 'a::complete_lattice" - assumes [simp]: "continuous F" shows "mono F" + assumes [simp]: "sup_continuous F" shows "mono F" proof fix A B :: "'a" assume [simp]: "A \ B" have "F B = F (SUP n::nat. if n = 0 then A else B)" by (simp add: sup_absorb2 SUP_nat_binary) also have "\ = (SUP n::nat. if n = 0 then F A else F B)" - by (auto simp: continuousD mono_def intro!: SUP_cong) + by (auto simp: sup_continuousD mono_def intro!: SUP_cong) finally show "F A \ F B" by (simp add: SUP_nat_binary le_iff_sup) qed -lemma continuous_lfp: - assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U") +lemma sup_continuous_lfp: + assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U") proof (rule antisym) - note mono = continuous_mono[OF `continuous F`] + note mono = sup_continuous_mono[OF `sup_continuous F`] show "?U \ lfp F" proof (rule SUP_least) fix i show "(F ^^ i) bot \ lfp F" @@ -77,36 +83,38 @@ qed } thus ?thesis by (auto simp add: mono_iff_le_Suc) qed - hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def) - also have "\ \ ?U" by (fast intro: SUP_least SUP_upper) + hence "F ?U = (SUP i. (F ^^ Suc i) bot)" + using `sup_continuous F` by (simp add: sup_continuous_def) + also have "\ \ ?U" + by (fast intro: SUP_least SUP_upper) finally show "F ?U \ ?U" . qed qed definition - down_continuous :: "('a::complete_lattice \ 'a::complete_lattice) \ bool" where - "down_continuous F \ (\M::nat \ 'a. antimono M \ F (INF i. M i) = (INF i. F (M i)))" + inf_continuous :: "('a::complete_lattice \ 'a::complete_lattice) \ bool" where + "inf_continuous F \ (\M::nat \ 'a. antimono M \ F (INF i. M i) = (INF i. F (M i)))" -lemma down_continuousD: "down_continuous F \ antimono M \ F (INF i::nat. M i) = (INF i. F (M i))" - by (auto simp: down_continuous_def) +lemma inf_continuousD: "inf_continuous F \ antimono M \ F (INF i::nat. M i) = (INF i. F (M i))" + by (auto simp: inf_continuous_def) -lemma down_continuous_mono: +lemma inf_continuous_mono: fixes F :: "'a::complete_lattice \ 'a::complete_lattice" - assumes [simp]: "down_continuous F" shows "mono F" + assumes [simp]: "inf_continuous F" shows "mono F" proof fix A B :: "'a" assume [simp]: "A \ B" have "F A = F (INF n::nat. if n = 0 then B else A)" by (simp add: inf_absorb2 INF_nat_binary) also have "\ = (INF n::nat. if n = 0 then F B else F A)" - by (auto simp: down_continuousD antimono_def intro!: INF_cong) + by (auto simp: inf_continuousD antimono_def intro!: INF_cong) finally show "F A \ F B" by (simp add: INF_nat_binary le_iff_inf inf_commute) qed -lemma down_continuous_gfp: - assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U") +lemma inf_continuous_gfp: + assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U") proof (rule antisym) - note mono = down_continuous_mono[OF `down_continuous F`] + note mono = inf_continuous_mono[OF `inf_continuous F`] show "gfp F \ ?U" proof (rule INF_greatest) fix i show "gfp F \ (F ^^ i) top" @@ -133,7 +141,7 @@ have "?U \ (INF i. (F ^^ Suc i) top)" by (fast intro: INF_greatest INF_lower) also have "\ \ F ?U" - by (simp add: down_continuousD `down_continuous F` *) + by (simp add: inf_continuousD `inf_continuous F` *) finally show "?U \ F ?U" . qed qed diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Library/Quadratic_Discriminant.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Quadratic_Discriminant.thy Mon May 25 22:11:43 2015 +0200 @@ -0,0 +1,182 @@ +(* Title: Roots of real quadratics + Author: Tim Makarios , 2012 + +Originally from the AFP entry Tarskis_Geometry +*) + +section "Roots of real quadratics" + +theory Quadratic_Discriminant +imports Complex_Main +begin + +definition discrim :: "[real,real,real] \ real" where + "discrim a b c \ b\<^sup>2 - 4 * a * c" + +lemma complete_square: + fixes a b c x :: "real" + assumes "a \ 0" + shows "a * x\<^sup>2 + b * x + c = 0 \ (2 * a * x + b)\<^sup>2 = discrim a b c" +proof - + have "4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 4 * a * (a * x\<^sup>2 + b * x + c)" + by (simp add: algebra_simps power2_eq_square) + with `a \ 0` + have "a * x\<^sup>2 + b * x + c = 0 \ 4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 0" + by simp + thus "a * x\<^sup>2 + b * x + c = 0 \ (2 * a * x + b)\<^sup>2 = discrim a b c" + unfolding discrim_def + by (simp add: power2_eq_square algebra_simps) +qed + +lemma discriminant_negative: + fixes a b c x :: real + assumes "a \ 0" + and "discrim a b c < 0" + shows "a * x\<^sup>2 + b * x + c \ 0" +proof - + have "(2 * a * x + b)\<^sup>2 \ 0" by simp + with `discrim a b c < 0` have "(2 * a * x + b)\<^sup>2 \ discrim a b c" by arith + with complete_square and `a \ 0` show "a * x\<^sup>2 + b * x + c \ 0" by simp +qed + +lemma plus_or_minus_sqrt: + fixes x y :: real + assumes "y \ 0" + shows "x\<^sup>2 = y \ x = sqrt y \ x = - sqrt y" +proof + assume "x\<^sup>2 = y" + hence "sqrt (x\<^sup>2) = sqrt y" by simp + hence "sqrt y = \x\" by simp + thus "x = sqrt y \ x = - sqrt y" by auto +next + assume "x = sqrt y \ x = - sqrt y" + hence "x\<^sup>2 = (sqrt y)\<^sup>2 \ x\<^sup>2 = (- sqrt y)\<^sup>2" by auto + with `y \ 0` show "x\<^sup>2 = y" by simp +qed + +lemma divide_non_zero: + fixes x y z :: real + assumes "x \ 0" + shows "x * y = z \ y = z / x" +proof + assume "x * y = z" + with `x \ 0` show "y = z / x" by (simp add: field_simps) +next + assume "y = z / x" + with `x \ 0` show "x * y = z" by simp +qed + +lemma discriminant_nonneg: + fixes a b c x :: real + assumes "a \ 0" + and "discrim a b c \ 0" + shows "a * x\<^sup>2 + b * x + c = 0 \ + x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a)" +proof - + from complete_square and plus_or_minus_sqrt and assms + have "a * x\<^sup>2 + b * x + c = 0 \ + (2 * a) * x + b = sqrt (discrim a b c) \ + (2 * a) * x + b = - sqrt (discrim a b c)" + by simp + also have "\ \ (2 * a) * x = (-b + sqrt (discrim a b c)) \ + (2 * a) * x = (-b - sqrt (discrim a b c))" + by auto + also from `a \ 0` and divide_non_zero [of "2 * a" x] + have "\ \ x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a)" + by simp + finally show "a * x\<^sup>2 + b * x + c = 0 \ + x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a)" . +qed + +lemma discriminant_zero: + fixes a b c x :: real + assumes "a \ 0" + and "discrim a b c = 0" + shows "a * x\<^sup>2 + b * x + c = 0 \ x = -b / (2 * a)" + using discriminant_nonneg and assms + by simp + +theorem discriminant_iff: + fixes a b c x :: real + assumes "a \ 0" + shows "a * x\<^sup>2 + b * x + c = 0 \ + discrim a b c \ 0 \ + (x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a))" +proof + assume "a * x\<^sup>2 + b * x + c = 0" + with discriminant_negative and `a \ 0` have "\(discrim a b c < 0)" by auto + hence "discrim a b c \ 0" by simp + with discriminant_nonneg and `a * x\<^sup>2 + b * x + c = 0` and `a \ 0` + have "x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a)" + by simp + with `discrim a b c \ 0` + show "discrim a b c \ 0 \ + (x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a))" .. +next + assume "discrim a b c \ 0 \ + (x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a))" + hence "discrim a b c \ 0" and + "x = (-b + sqrt (discrim a b c)) / (2 * a) \ + x = (-b - sqrt (discrim a b c)) / (2 * a)" + by simp_all + with discriminant_nonneg and `a \ 0` show "a * x\<^sup>2 + b * x + c = 0" by simp +qed + +lemma discriminant_nonneg_ex: + fixes a b c :: real + assumes "a \ 0" + and "discrim a b c \ 0" + shows "\ x. a * x\<^sup>2 + b * x + c = 0" + using discriminant_nonneg and assms + by auto + +lemma discriminant_pos_ex: + fixes a b c :: real + assumes "a \ 0" + and "discrim a b c > 0" + shows "\ x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ a * y\<^sup>2 + b * y + c = 0" +proof - + let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)" + let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)" + from `discrim a b c > 0` have "sqrt (discrim a b c) \ 0" by simp + hence "sqrt (discrim a b c) \ - sqrt (discrim a b c)" by arith + with `a \ 0` have "?x \ ?y" by simp + moreover + from discriminant_nonneg [of a b c ?x] + and discriminant_nonneg [of a b c ?y] + and assms + have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all + ultimately + show "\ x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ a * y\<^sup>2 + b * y + c = 0" by blast +qed + +lemma discriminant_pos_distinct: + fixes a b c x :: real + assumes "a \ 0" and "discrim a b c > 0" + shows "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" +proof - + from discriminant_pos_ex and `a \ 0` and `discrim a b c > 0` + obtain w and z where "w \ z" + and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0" + by blast + show "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" + proof cases + assume "x = w" + with `w \ z` have "x \ z" by simp + with `a * z\<^sup>2 + b * z + c = 0` + show "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" by auto + next + assume "x \ w" + with `a * w\<^sup>2 + b * w + c = 0` + show "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" by auto + qed +qed + +end diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Limits.thy Mon May 25 22:11:43 2015 +0200 @@ -396,7 +396,7 @@ lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\x. f x - a) F" by (simp only: tendsto_iff Zfun_def dist_norm) -lemma tendsto_0_le: "\(f ---> 0) F; eventually (\x. norm (g x) \ norm (f x) * K) F\ +lemma tendsto_0_le: "\(f ---> 0) F; eventually (\x. norm (g x) \ norm (f x) * K) F\ \ (g ---> 0) F" by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) @@ -1134,7 +1134,7 @@ *} -lemma filterlim_tendsto_pos_mult_at_top: +lemma filterlim_tendsto_pos_mult_at_top: assumes f: "(f ---> c) F" and c: "0 < c" assumes g: "LIM x F. g x :> at_top" shows "LIM x F. (f x * g x :: real) :> at_top" @@ -1156,7 +1156,7 @@ qed qed -lemma filterlim_at_top_mult_at_top: +lemma filterlim_at_top_mult_at_top: assumes f: "LIM x F. f x :> at_top" assumes g: "LIM x F. g x :> at_top" shows "LIM x F. (f x * g x :: real) :> at_top" @@ -1183,6 +1183,12 @@ using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\x. - g x"] assms(3) unfolding filterlim_uminus_at_bot by simp +lemma filterlim_tendsto_neg_mult_at_bot: + assumes c: "(f ---> c) F" "(c::real) < 0" and g: "filterlim g at_top F" + shows "LIM x F. f x * g x :> at_bot" + using c filterlim_tendsto_pos_mult_at_top[of "\x. - f x" "- c" F, OF _ _ g] + unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp + lemma filterlim_pow_at_top: fixes f :: "real \ real" assumes "0 < n" and f: "LIM x F. f x :> at_top" @@ -1202,7 +1208,7 @@ shows "0 < n \ LIM x F. f x :> at_bot \ odd n \ LIM x F. (f x)^n :> at_bot" using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_bot) -lemma filterlim_tendsto_add_at_top: +lemma filterlim_tendsto_add_at_top: assumes f: "(f ---> c) F" assumes g: "LIM x F. g x :> at_top" shows "LIM x F. (f x + g x :: real) :> at_top" @@ -1225,7 +1231,7 @@ unfolding divide_inverse by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) -lemma filterlim_at_top_add_at_top: +lemma filterlim_at_top_add_at_top: assumes f: "LIM x F. f x :> at_top" assumes g: "LIM x F. g x :> at_top" shows "LIM x F. (f x + g x :: real) :> at_top" @@ -1315,16 +1321,108 @@ shows "\X ----> a; a \ 0\ \ Bseq (\n. inverse (X n))" by (rule Bfun_inverse) -lemma LIMSEQ_diff_approach_zero: - fixes L :: "'a::real_normed_vector" - shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L" - by (drule (1) tendsto_add, simp) +text{* Transformation of limit. *} + +lemma eventually_at2: + "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" + unfolding eventually_at dist_nz by auto + +lemma Lim_transform: + fixes a b :: "'a::real_normed_vector" + shows "\(g ---> a) F; ((\x. f x - g x) ---> 0) F\ \ (f ---> a) F" + using tendsto_add [of g a F "\x. f x - g x" 0] by simp + +lemma Lim_transform2: + fixes a b :: "'a::real_normed_vector" + shows "\(f ---> a) F; ((\x. f x - g x) ---> 0) F\ \ (g ---> a) F" + by (erule Lim_transform) (simp add: tendsto_minus_cancel) + +lemma Lim_transform_eventually: + "eventually (\x. f x = g x) net \ (f ---> l) net \ (g ---> l) net" + apply (rule topological_tendstoI) + apply (drule (2) topological_tendstoD) + apply (erule (1) eventually_elim2, simp) + done + +lemma Lim_transform_within: + assumes "0 < d" + and "\x'\S. 0 < dist x' x \ dist x' x < d \ f x' = g x'" + and "(f ---> l) (at x within S)" + shows "(g ---> l) (at x within S)" +proof (rule Lim_transform_eventually) + show "eventually (\x. f x = g x) (at x within S)" + using assms(1,2) by (auto simp: dist_nz eventually_at) + show "(f ---> l) (at x within S)" by fact +qed + +lemma Lim_transform_at: + assumes "0 < d" + and "\x'. 0 < dist x' x \ dist x' x < d \ f x' = g x'" + and "(f ---> l) (at x)" + shows "(g ---> l) (at x)" + using _ assms(3) +proof (rule Lim_transform_eventually) + show "eventually (\x. f x = g x) (at x)" + unfolding eventually_at2 + using assms(1,2) by auto +qed + +text{* Common case assuming being away from some crucial point like 0. *} -lemma LIMSEQ_diff_approach_zero2: - fixes L :: "'a::real_normed_vector" - shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L" - by (drule (1) tendsto_diff, simp) +lemma Lim_transform_away_within: + fixes a b :: "'a::t1_space" + assumes "a \ b" + and "\x\S. x \ a \ x \ b \ f x = g x" + and "(f ---> l) (at a within S)" + shows "(g ---> l) (at a within S)" +proof (rule Lim_transform_eventually) + show "(f ---> l) (at a within S)" by fact + show "eventually (\x. f x = g x) (at a within S)" + unfolding eventually_at_topological + by (rule exI [where x="- {b}"], simp add: open_Compl assms) +qed + +lemma Lim_transform_away_at: + fixes a b :: "'a::t1_space" + assumes ab: "a\b" + and fg: "\x. x \ a \ x \ b \ f x = g x" + and fl: "(f ---> l) (at a)" + shows "(g ---> l) (at a)" + using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp + +text{* Alternatively, within an open set. *} +lemma Lim_transform_within_open: + assumes "open S" and "a \ S" + and "\x\S. x \ a \ f x = g x" + and "(f ---> l) (at a)" + shows "(g ---> l) (at a)" +proof (rule Lim_transform_eventually) + show "eventually (\x. f x = g x) (at a)" + unfolding eventually_at_topological + using assms(1,2,3) by auto + show "(f ---> l) (at a)" by fact +qed + +text{* A congruence rule allowing us to transform limits assuming not at point. *} + +(* FIXME: Only one congruence rule for tendsto can be used at a time! *) + +lemma Lim_cong_within(*[cong add]*): + assumes "a = b" + and "x = y" + and "S = T" + and "\x. x \ b \ x \ T \ f x = g x" + shows "(f ---> x) (at a within S) \ (g ---> y) (at b within T)" + unfolding tendsto_def eventually_at_topological + using assms by simp + +lemma Lim_cong_at(*[cong add]*): + assumes "a = b" "x = y" + and "\x. x \ a \ f x = g x" + shows "((\x. f x) ---> x) (at a) \ ((g ---> y) (at a))" + unfolding tendsto_def eventually_at_topological + using assms by simp text{*An unbounded sequence's inverse tends to 0*} lemma LIMSEQ_inverse_zero: @@ -1684,7 +1782,7 @@ "\isCont f a; isCont g a\ \ isCont (\x. f x ** g x) a" by (fact continuous) -lemmas isCont_scaleR [simp] = +lemmas isCont_scaleR [simp] = bounded_bilinear.isCont [OF bounded_bilinear_scaleR] lemmas isCont_of_real [simp] = @@ -1740,7 +1838,7 @@ lemma (in bounded_linear) Cauchy: "Cauchy X \ Cauchy (\n. f (X n))" by (rule isUCont [THEN isUCont_Cauchy]) -lemma LIM_less_bound: +lemma LIM_less_bound: fixes f :: "real \ real" assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" shows "0 \ f x" @@ -1804,7 +1902,7 @@ show "P a b" proof (rule ccontr) - assume "\ P a b" + assume "\ P a b" { fix n have "\ P (l n) (u n)" proof (induct n) case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto @@ -1911,7 +2009,7 @@ lemma isCont_Lb_Ub: fixes f :: "real \ real" assumes "a \ b" "\x. a \ x \ x \ b \ isCont f x" - shows "\L M. (\x. a \ x \ x \ b \ L \ f x \ f x \ M) \ + shows "\L M. (\x. a \ x \ x \ b \ L \ f x \ f x \ M) \ (\y. L \ y \ y \ M \ (\x. a \ x \ x \ b \ (f x = y)))" proof - obtain M where M: "a \ M" "M \ b" "\x. a \ x \ x \ b \ f x \ f M" @@ -1974,8 +2072,8 @@ lemma isCont_inv_fun: fixes f g :: "real \ real" - shows "[| 0 < d; \z. \z - x\ \ d --> g(f(z)) = z; - \z. \z - x\ \ d --> isCont f z |] + shows "[| 0 < d; \z. \z - x\ \ d --> g(f(z)) = z; + \z. \z - x\ \ d --> isCont f z |] ==> isCont g (f x)" by (rule isCont_inverse_function) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/List.thy --- a/src/HOL/List.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/List.thy Mon May 25 22:11:43 2015 +0200 @@ -486,35 +486,38 @@ ML_val {* let - val read = Syntax.read_term @{context}; - fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1); + val read = Syntax.read_term @{context} o Syntax.implode_input; + fun check s1 s2 = + read s1 aconv read s2 orelse + error ("Check failed: " ^ + quote (Input.source_content s1) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]); in - check "[(x,y,z). b]" "if b then [(x, y, z)] else []"; - check "[(x,y,z). x\xs]" "map (\x. (x, y, z)) xs"; - check "[e x y. x\xs, y\ys]" "concat (map (\x. map (\y. e x y) ys) xs)"; - check "[(x,y,z). xb]" "if x < a then if b < x then [(x, y, z)] else [] else []"; - check "[(x,y,z). x\xs, x>b]" "concat (map (\x. if b < x then [(x, y, z)] else []) xs)"; - check "[(x,y,z). xxs]" "if x < a then map (\x. (x, y, z)) xs else []"; - check "[(x,y). Cons True x \ xs]" - "concat (map (\xa. case xa of [] \ [] | True # x \ [(x, y)] | False # x \ []) xs)"; - check "[(x,y,z). Cons x [] \ xs]" - "concat (map (\xa. case xa of [] \ [] | [x] \ [(x, y, z)] | x # aa # lista \ []) xs)"; - check "[(x,y,z). xb, x=d]" - "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []"; - check "[(x,y,z). xb, y\ys]" - "if x < a then if b < x then map (\y. (x, y, z)) ys else [] else []"; - check "[(x,y,z). xxs,y>b]" - "if x < a then concat (map (\x. if b < y then [(x, y, z)] else []) xs) else []"; - check "[(x,y,z). xxs, y\ys]" - "if x < a then concat (map (\x. map (\y. (x, y, z)) ys) xs) else []"; - check "[(x,y,z). x\xs, x>b, yx. if b < x then if y < a then [(x, y, z)] else [] else []) xs)"; - check "[(x,y,z). x\xs, x>b, y\ys]" - "concat (map (\x. if b < x then map (\y. (x, y, z)) ys else []) xs)"; - check "[(x,y,z). x\xs, y\ys,y>x]" - "concat (map (\x. concat (map (\y. if x < y then [(x, y, z)] else []) ys)) xs)"; - check "[(x,y,z). x\xs, y\ys,z\zs]" - "concat (map (\x. concat (map (\y. map (\z. (x, y, z)) zs) ys)) xs)" + check \[(x,y,z). b]\ \if b then [(x, y, z)] else []\; + check \[(x,y,z). x\xs]\ \map (\x. (x, y, z)) xs\; + check \[e x y. x\xs, y\ys]\ \concat (map (\x. map (\y. e x y) ys) xs)\; + check \[(x,y,z). xb]\ \if x < a then if b < x then [(x, y, z)] else [] else []\; + check \[(x,y,z). x\xs, x>b]\ \concat (map (\x. if b < x then [(x, y, z)] else []) xs)\; + check \[(x,y,z). xxs]\ \if x < a then map (\x. (x, y, z)) xs else []\; + check \[(x,y). Cons True x \ xs]\ + \concat (map (\xa. case xa of [] \ [] | True # x \ [(x, y)] | False # x \ []) xs)\; + check \[(x,y,z). Cons x [] \ xs]\ + \concat (map (\xa. case xa of [] \ [] | [x] \ [(x, y, z)] | x # aa # lista \ []) xs)\; + check \[(x,y,z). xb, x=d]\ + \if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []\; + check \[(x,y,z). xb, y\ys]\ + \if x < a then if b < x then map (\y. (x, y, z)) ys else [] else []\; + check \[(x,y,z). xxs,y>b]\ + \if x < a then concat (map (\x. if b < y then [(x, y, z)] else []) xs) else []\; + check \[(x,y,z). xxs, y\ys]\ + \if x < a then concat (map (\x. map (\y. (x, y, z)) ys) xs) else []\; + check \[(x,y,z). x\xs, x>b, y + \concat (map (\x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)\; + check \[(x,y,z). x\xs, x>b, y\ys]\ + \concat (map (\x. if b < x then map (\y. (x, y, z)) ys else []) xs)\; + check \[(x,y,z). x\xs, y\ys,y>x]\ + \concat (map (\x. concat (map (\y. if x < y then [(x, y, z)] else []) ys)) xs)\; + check \[(x,y,z). x\xs, y\ys,z\zs]\ + \concat (map (\x. concat (map (\y. map (\z. (x, y, z)) zs) ys)) xs)\ end; *} @@ -539,19 +542,19 @@ fun all_exists_conv cv ctxt ct = (case Thm.term_of ct of - Const (@{const_name HOL.Ex}, _) $ Abs _ => + Const (@{const_name Ex}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct | _ => cv ctxt ct) fun all_but_last_exists_conv cv ctxt ct = (case Thm.term_of ct of - Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) => + Const (@{const_name Ex}, _) $ Abs (_, _, Const (@{const_name Ex}, _) $ _) => Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct | _ => cv ctxt ct) fun Collect_conv cv ctxt ct = (case Thm.term_of ct of - Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct + Const (@{const_name Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct | _ => raise CTERM ("Collect_conv", [ct])) fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) @@ -567,119 +570,130 @@ (* term abstraction of list comprehension patterns *) -datatype termlets = If | Case of (typ * int) +datatype termlets = If | Case of typ * int + +local + +val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])} +val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} +val inst_Collect_mem_eq = @{lemma "set A = {x. x \ set A}" by simp} +val del_refl_eq = @{lemma "(t = t \ P) \ P" by simp} + +fun mk_set T = Const (@{const_name set}, HOLogic.listT T --> HOLogic.mk_setT T) +fun dest_set (Const (@{const_name set}, _) $ xs) = xs + +fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name Nil}, _))) = t + | dest_singleton_list t = raise TERM ("dest_singleton_list", [t]) + +(*We check that one case returns a singleton list and all other cases + return [], and return the index of the one singleton list case.*) +fun possible_index_of_singleton_case cases = + let + fun check (i, case_t) s = + (case strip_abs_body case_t of + (Const (@{const_name Nil}, _)) => s + | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE)) + in + fold_index check cases (SOME NONE) |> the_default NONE + end + +(*returns condition continuing term option*) +fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = + SOME (cond, then_t) + | dest_if _ = NONE + +(*returns (case_expr type index chosen_case constr_name) option*) +fun dest_case ctxt case_term = + let + val (case_const, args) = strip_comb case_term + in + (case try dest_Const case_const of + SOME (c, T) => + (case Ctr_Sugar.ctr_sugar_of_case ctxt c of + SOME {ctrs, ...} => + (case possible_index_of_singleton_case (fst (split_last args)) of + SOME i => + let + val constr_names = map (fst o dest_Const) ctrs + val (Ts, _) = strip_type T + val T' = List.last Ts + in SOME (List.last args, T', i, nth args i, nth constr_names i) end + | NONE => NONE) + | NONE => NONE) + | NONE => NONE) + end + +fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 + | tac ctxt (If :: cont) = + Splitter.split_tac ctxt @{thms split_if} 1 + THEN rtac @{thm conjI} 1 + THEN rtac @{thm impI} 1 + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION (right_hand_set_comprehension_conv (K + (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv + then_conv + rewr_conv' @{lemma "(True \ P) = P" by simp})) ctxt') 1) ctxt 1 + THEN tac ctxt cont + THEN rtac @{thm impI} 1 + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION (right_hand_set_comprehension_conv (K + (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv + then_conv rewr_conv' @{lemma "(False \ P) = False" by simp})) ctxt') 1) ctxt 1 + THEN rtac set_Nil_I 1 + | tac ctxt (Case (T, i) :: cont) = + let + val SOME {injects, distincts, case_thms, split, ...} = + Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T)) + in + (* do case distinction *) + Splitter.split_tac ctxt [split] 1 + THEN EVERY (map_index (fn (i', _) => + (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac) + THEN REPEAT_DETERM (rtac @{thm allI} 1) + THEN rtac @{thm impI} 1 + THEN (if i' = i then + (* continue recursively *) + Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K + ((HOLogic.conj_conv + (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv + (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects)))) + Conv.all_conv) + then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) + then_conv conjunct_assoc_conv)) ctxt' + then_conv + (HOLogic.Trueprop_conv + (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt'') => + Conv.repeat_conv + (all_but_last_exists_conv + (K (rewr_conv' + @{lemma "(\x. x = t \ P x) = P t" by simp})) ctxt'')) ctxt')))) 1) ctxt 1 + THEN tac ctxt cont + else + Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION + (right_hand_set_comprehension_conv (K + (HOLogic.conj_conv + ((HOLogic.eq_conv Conv.all_conv + (rewr_conv' (List.last prems))) then_conv + (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts))) + Conv.all_conv then_conv + (rewr_conv' @{lemma "(False \ P) = False" by simp}))) ctxt' then_conv + HOLogic.Trueprop_conv + (HOLogic.eq_conv Conv.all_conv + (Collect_conv (fn (_, ctxt'') => + Conv.repeat_conv + (Conv.bottom_conv + (K (rewr_conv' @{lemma "(\x. P) = P" by simp})) ctxt'')) ctxt'))) 1) ctxt 1 + THEN rtac set_Nil_I 1)) case_thms) + end + +in fun simproc ctxt redex = let - val set_Nil_I = @{thm trans} OF [@{thm list.set(1)}, @{thm empty_def}] - val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} - val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} - val del_refl_eq = @{lemma "(t = t & P) == P" by simp} - fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T) - fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs - fun dest_singleton_list (Const (@{const_name List.Cons}, _) - $ t $ (Const (@{const_name List.Nil}, _))) = t - | dest_singleton_list t = raise TERM ("dest_singleton_list", [t]) - (* We check that one case returns a singleton list and all other cases - return [], and return the index of the one singleton list case *) - fun possible_index_of_singleton_case cases = - let - fun check (i, case_t) s = - (case strip_abs_body case_t of - (Const (@{const_name List.Nil}, _)) => s - | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE)) - in - fold_index check cases (SOME NONE) |> the_default NONE - end - (* returns (case_expr type index chosen_case constr_name) option *) - fun dest_case case_term = - let - val (case_const, args) = strip_comb case_term - in - (case try dest_Const case_const of - SOME (c, T) => - (case Ctr_Sugar.ctr_sugar_of_case ctxt c of - SOME {ctrs, ...} => - (case possible_index_of_singleton_case (fst (split_last args)) of - SOME i => - let - val constr_names = map (fst o dest_Const) ctrs - val (Ts, _) = strip_type T - val T' = List.last Ts - in SOME (List.last args, T', i, nth args i, nth constr_names i) end - | NONE => NONE) - | NONE => NONE) - | NONE => NONE) - end - (* returns condition continuing term option *) - fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = - SOME (cond, then_t) - | dest_if _ = NONE - fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 - | tac ctxt (If :: cont) = - Splitter.split_tac ctxt [@{thm split_if}] 1 - THEN rtac @{thm conjI} 1 - THEN rtac @{thm impI} 1 - THEN Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (right_hand_set_comprehension_conv (K - (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv - then_conv - rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1 - THEN tac ctxt cont - THEN rtac @{thm impI} 1 - THEN Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (right_hand_set_comprehension_conv (K - (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv - then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1 - THEN rtac set_Nil_I 1 - | tac ctxt (Case (T, i) :: cont) = - let - val SOME {injects, distincts, case_thms, split, ...} = - Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T)) - in - (* do case distinction *) - Splitter.split_tac ctxt [split] 1 - THEN EVERY (map_index (fn (i', _) => - (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac) - THEN REPEAT_DETERM (rtac @{thm allI} 1) - THEN rtac @{thm impI} 1 - THEN (if i' = i then - (* continue recursively *) - Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K - ((HOLogic.conj_conv - (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv - (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects)))) - Conv.all_conv) - then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) - then_conv conjunct_assoc_conv)) context - then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => - Conv.repeat_conv - (all_but_last_exists_conv - (K (rewr_conv' - @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1 - THEN tac ctxt cont - else - Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION - (right_hand_set_comprehension_conv (K - (HOLogic.conj_conv - ((HOLogic.eq_conv Conv.all_conv - (rewr_conv' (List.last prems))) then_conv - (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts))) - Conv.all_conv then_conv - (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv - HOLogic.Trueprop_conv - (HOLogic.eq_conv Conv.all_conv - (Collect_conv (fn (_, ctxt) => - Conv.repeat_conv - (Conv.bottom_conv - (K (rewr_conv' - @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1 - THEN rtac set_Nil_I 1)) case_thms) - end fun make_inner_eqs bound_vs Tis eqs t = - (case dest_case t of + (case dest_case ctxt t of SOME (x, T, i, cont, constr_name) => let val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont) @@ -696,10 +710,10 @@ (case dest_if t of SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont | NONE => - if eqs = [] then NONE (* no rewriting, nothing to be done *) + if null eqs then NONE (*no rewriting, nothing to be done*) else let - val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t) + val Type (@{type_name list}, [rT]) = fastype_of1 (map snd bound_vs, t) val pat_eq = (case try dest_singleton_list t of SOME t' => @@ -721,19 +735,21 @@ in SOME ((Goal.prove ctxt [] [] rewrite_rule_t - (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection}) + (fn {context = ctxt', ...} => tac ctxt' (rev Tis))) RS @{thm eq_reflection}) end)) in make_inner_eqs [] [] [] (dest_set (Thm.term_of redex)) end end + +end *} -simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *} +simproc_setup list_to_set_comprehension ("set xs") = + {* K List_to_Set_Comprehension.simproc *} code_datatype set coset - hide_const (open) coset diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon May 25 22:11:43 2015 +0200 @@ -240,7 +240,7 @@ and closed_halfspace_Im_le: "closed {z. Im(z) \ b}" and closed_halfspace_Im_eq: "closed {z. Im(z) = b}" by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re - isCont_Im isCont_ident isCont_const)+ + isCont_Im continuous_ident continuous_const)+ lemma closed_complex_Reals: "closed (Reals :: complex set)" proof - @@ -1200,7 +1200,7 @@ also have "... \ (e * norm z) * norm z ^ Suc n" by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power) finally show "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc (Suc n)" - by (simp add: power_Suc) + by simp qed qed diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon May 25 22:11:43 2015 +0200 @@ -42,11 +42,8 @@ subsection{*The Exponential Function is Differentiable and Continuous*} -lemma complex_differentiable_at_exp: "exp complex_differentiable at z" - using DERIV_exp complex_differentiable_def by blast - lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)" - by (simp add: complex_differentiable_at_exp complex_differentiable_at_within) + using DERIV_exp complex_differentiable_at_within complex_differentiable_def by blast lemma continuous_within_exp: fixes z::"'a::{real_normed_field,banach}" @@ -461,9 +458,6 @@ subsection{* Taylor series for complex exponential, sine and cosine.*} -context -begin - declare power_Suc [simp del] lemma Taylor_exp: @@ -525,8 +519,9 @@ have *: "cmod (sin z - (\i\n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i))) \ exp \Im z\ * cmod z ^ Suc n / (fact n)" - proof (rule complex_taylor [of "closed_segment 0 z" n "\k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\Im z\" 0 z, -simplified]) + proof (rule complex_taylor [of "closed_segment 0 z" n + "\k x. (-1)^(k div 2) * (if even k then sin x else cos x)" + "exp\Im z\" 0 z, simplified]) show "convex (closed_segment 0 z)" by (rule convex_segment [of 0 z]) next @@ -603,7 +598,7 @@ done qed -end (* of context *) +declare power_Suc [simp] text{*32-bit Approximation to e*} lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \ (inverse(2 ^ 32)::real)" @@ -777,6 +772,11 @@ by blast qed +corollary Arg_gt_0: + assumes "z \ \ \ Re z < 0" + shows "Arg z > 0" + using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce + lemma Arg_of_real: "Arg(of_real x) = 0 \ 0 \ x" by (simp add: Arg_eq_0) @@ -952,6 +952,12 @@ corollary Ln_in_Reals [simp]: "z \ \ \ Re z > 0 \ ln z \ \" by (auto simp: Ln_of_real elim: Reals_cases) +corollary Im_Ln_of_real [simp]: "r > 0 \ Im (ln (of_real r)) = 0" + by (simp add: Ln_of_real) + +lemma cmod_Ln_Reals [simp]: "z \ Reals \ 0 < Re z \ cmod (ln z) = norm (ln (Re z))" + using Ln_of_real by force + lemma Ln_1: "ln 1 = (0::complex)" proof - have "ln (exp 0) = (0::complex)" @@ -975,7 +981,13 @@ using Ln_exp by blast lemma Re_Ln [simp]: "z \ 0 \ Re(Ln z) = ln(norm z)" -by (metis exp_Ln assms ln_exp norm_exp_eq_Re) + by (metis exp_Ln assms ln_exp norm_exp_eq_Re) + +corollary ln_cmod_le: + assumes z: "z \ 0" + shows "ln (cmod z) \ cmod (Ln z)" + using norm_exp [of "Ln z", simplified exp_Ln [OF z]] + by (metis Re_Ln complex_Re_le_cmod z) lemma exists_complex_root: fixes a :: complex @@ -1185,7 +1197,7 @@ also have "... = - (Ln ii)" by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one) also have "... = - (ii * pi/2)" - by (simp add: Ln_ii) + by simp finally show ?thesis . qed @@ -1201,11 +1213,22 @@ using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z] by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique) -lemma Ln_times_simple: +corollary Ln_times_simple: "\w \ 0; z \ 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \ pi\ \ Ln(w * z) = Ln(w) + Ln(z)" by (simp add: Ln_times) +corollary Ln_times_of_real: + "\r > 0; z \ 0\ \ Ln(of_real r * z) = ln r + Ln(z)" + using mpi_less_Im_Ln Im_Ln_le_pi + by (force simp: Ln_times) + +corollary Ln_divide_of_real: + "\r > 0; z \ 0\ \ Ln(z / of_real r) = Ln(z) - ln r" +using Ln_times_of_real [of "inverse r" z] +by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric] + del: of_real_inverse) + lemma Ln_minus: assumes "z \ 0" shows "Ln(-z) = (if Im(z) \ 0 \ ~(Re(z) < 0 \ Im(z) = 0) @@ -1260,12 +1283,164 @@ by (auto simp: of_real_numeral Ln_times) +subsection{*Relation between Ln and Arg, and hence continuity of Arg*} + +lemma Arg_Ln: + assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi" +proof (cases "z = 0") + case True + with assms show ?thesis + by simp +next + case False + then have "z / of_real(norm z) = exp(ii * of_real(Arg z))" + using Arg [of z] + by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff) + then have "- z / of_real(norm z) = exp (\ * (of_real (Arg z) - pi))" + using cis_conv_exp cis_pi + by (auto simp: exp_diff algebra_simps) + then have "ln (- z / of_real(norm z)) = ln (exp (\ * (of_real (Arg z) - pi)))" + by simp + also have "... = \ * (of_real(Arg z) - pi)" + using Arg [of z] assms pi_not_less_zero + by auto + finally have "Arg z = Im (Ln (- z / of_real (cmod z))) + pi" + by simp + also have "... = Im (Ln (-z) - ln (cmod z)) + pi" + by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False) + also have "... = Im (Ln (-z)) + pi" + by simp + finally show ?thesis . +qed + +lemma continuous_at_Arg: + assumes "z \ \ \ Re z < 0" + shows "continuous (at z) Arg" +proof - + have *: "isCont (\z. Im (Ln (- z)) + pi) z" + by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+ + then show ?thesis + apply (simp add: continuous_at) + apply (rule Lim_transform_within_open [of "-{z. z \ \ & 0 \ Re z}" _ "\z. Im(Ln(-z)) + pi"]) + apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge) + apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0]) + done +qed + +text{*Relation between Arg and arctangent in upper halfplane*} +lemma Arg_arctan_upperhalf: + assumes "0 < Im z" + shows "Arg z = pi/2 - arctan(Re z / Im z)" +proof (cases "z = 0") + case True with assms show ?thesis + by simp +next + case False + show ?thesis + apply (rule Arg_unique [of "norm z"]) + using False assms arctan [of "Re z / Im z"] pi_ge_two pi_half_less_two + apply (auto simp: exp_Euler cos_diff sin_diff) + using norm_complex_def [of z, symmetric] + apply (simp add: of_real_numeral sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide) + apply (metis complex_eq mult.assoc ring_class.ring_distribs(2)) + done +qed + +lemma Arg_eq_Im_Ln: + assumes "0 \ Im z" "0 < Re z" + shows "Arg z = Im (Ln z)" +proof (cases "z = 0 \ Im z = 0") + case True then show ?thesis + using assms Arg_eq_0 complex_is_Real_iff + apply auto + by (metis Arg_eq_0_pi Arg_eq_pi Im_Ln_eq_0 Im_Ln_eq_pi less_numeral_extra(3) zero_complex.simps(1)) +next + case False + then have "Arg z > 0" + using Arg_gt_0 complex_is_Real_iff by blast + then show ?thesis + using assms False + by (subst Arg_Ln) (auto simp: Ln_minus) +qed + +lemma continuous_within_upperhalf_Arg: + assumes "z \ 0" + shows "continuous (at z within {z. 0 \ Im z}) Arg" +proof (cases "z \ \ & 0 \ Re z") + case False then show ?thesis + using continuous_at_Arg continuous_at_imp_continuous_within by auto +next + case True + then have z: "z \ \" "0 < Re z" + using assms by (auto simp: complex_is_Real_iff complex_neq_0) + then have [simp]: "Arg z = 0" "Im (Ln z) = 0" + by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff) + show ?thesis + proof (clarsimp simp add: continuous_within Lim_within dist_norm) + fix e::real + assume "0 < e" + moreover have "continuous (at z) (\x. Im (Ln x))" + using z by (rule continuous_intros | simp) + ultimately + obtain d where d: "d>0" "\x. x \ z \ cmod (x - z) < d \ \Im (Ln x)\ < e" + by (auto simp: continuous_within Lim_within dist_norm) + { fix x + assume "cmod (x - z) < Re z / 2" + then have "\Re x - Re z\ < Re z / 2" + by (metis le_less_trans abs_Re_le_cmod minus_complex.simps(1)) + then have "0 < Re x" + using z by linarith + } + then show "\d>0. \x. 0 \ Im x \ x \ z \ cmod (x - z) < d \ \Arg x\ < e" + apply (rule_tac x="min d (Re z / 2)" in exI) + using z d + apply (auto simp: Arg_eq_Im_Ln) + done + qed +qed + +lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \ Im z} - {0}) Arg" + apply (auto simp: continuous_on_eq_continuous_within) + by (metis Diff_subset continuous_within_subset continuous_within_upperhalf_Arg) + +lemma open_Arg_less_Int: + assumes "0 \ s" "t \ 2*pi" + shows "open ({y. s < Arg y} \ {y. Arg y < t})" +proof - + have 1: "continuous_on (UNIV - {z \ \. 0 \ Re z}) Arg" + using continuous_at_Arg continuous_at_imp_continuous_within + by (auto simp: continuous_on_eq_continuous_within set_diff_eq) + have 2: "open (UNIV - {z \ \. 0 \ Re z})" + by (simp add: closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge open_Diff) + have "open ({z. s < z} \ {z. z < t})" + using open_lessThan [of t] open_greaterThan [of s] + by (metis greaterThan_def lessThan_def open_Int) + moreover have "{y. s < Arg y} \ {y. Arg y < t} \ - {z \ \. 0 \ Re z}" + using assms + by (auto simp: Arg_real) + ultimately show ?thesis + using continuous_imp_open_vimage [OF 1 2, of "{z. Re z > s} \ {z. Re z < t}"] + by auto +qed + +lemma open_Arg_gt: "open {z. t < Arg z}" +proof (cases "t < 0") + case True then have "{z. t < Arg z} = UNIV" + using Arg_ge_0 less_le_trans by auto + then show ?thesis + by simp +next + case False then show ?thesis + using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi + by auto +qed + +lemma closed_Arg_le: "closed {z. Arg z \ t}" + using open_Arg_gt [of t] + by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le) subsection{*Complex Powers*} -lemma powr_0 [simp]: "0 powr z = 0" - by (simp add: powr_def) - lemma powr_to_1 [simp]: "z powr 1 = (z::complex)" by (simp add: powr_def) @@ -1341,9 +1516,135 @@ "w \ \ \ 0 < Re w \ norm(w powr z) = Re w powr Re z" by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm) -lemma cmod_Ln_Reals [simp]:"z \ Reals \ 0 < Re z \ cmod (Ln z) = norm (ln (Re z))" + +subsection{*Some Limits involving Logarithms*} + +lemma lim_Ln_over_power: + fixes s::complex + assumes "0 < Re s" + shows "((\n. Ln n / (n powr s)) ---> 0) sequentially" +proof (simp add: lim_sequentially dist_norm, clarify) + fix e::real + assume e: "0 < e" + have "\xo>0. \x\xo. 0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2" + proof (rule_tac x="2/(e * (Re s)\<^sup>2)" in exI, safe) + show "0 < 2 / (e * (Re s)\<^sup>2)" + using e assms by (simp add: field_simps) + next + fix x::real + assume x: "2 / (e * (Re s)\<^sup>2) \ x" + then have "x>0" + using e assms + by (metis less_le_trans mult_eq_0_iff mult_pos_pos pos_less_divide_eq power2_eq_square + zero_less_numeral) + then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2" + using e assms x + apply (auto simp: field_simps) + apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans) + apply (auto simp: power2_eq_square field_simps add_pos_pos) + done + qed + then have "\xo>0. \x\xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2" + using e by (simp add: field_simps) + then have "\xo>0. \x\xo. x / e < exp (Re s * x)" + using assms + by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic]) + then have "\xo>0. \x\xo. x < e * exp (Re s * x)" + using e by (auto simp: field_simps) + with e show "\no. \n\no. norm (Ln (of_nat n) / of_nat n powr s) < e" + apply (auto simp: norm_divide norm_powr_real divide_simps) + apply (rule_tac x="nat (ceiling (exp xo))" in exI) + apply clarify + apply (drule_tac x="ln n" in spec) + apply (auto simp: real_of_nat_def exp_less_mono nat_ceiling_le_eq not_le) + apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff) + done +qed + +lemma lim_Ln_over_n: "((\n. Ln(of_nat n) / of_nat n) ---> 0) sequentially" + using lim_Ln_over_power [of 1] + by simp + +lemma Ln_Reals_eq: "x \ Reals \ Re x > 0 \ Ln x = of_real (ln (Re x))" using Ln_of_real by force +lemma powr_Reals_eq: "x \ Reals \ Re x > 0 \ x powr complex_of_real y = of_real (x powr y)" + by (simp add: powr_of_real) + +lemma lim_ln_over_power: + fixes s :: real + assumes "0 < s" + shows "((\n. ln n / (n powr s)) ---> 0) sequentially" + using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms + apply (subst filterlim_sequentially_Suc [symmetric]) + apply (simp add: lim_sequentially dist_norm + Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def) + done + +lemma lim_ln_over_n: "((\n. ln(real_of_nat n) / of_nat n) ---> 0) sequentially" + using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]] + apply (subst filterlim_sequentially_Suc [symmetric]) + apply (simp add: lim_sequentially dist_norm real_of_nat_def) + done + +lemma lim_1_over_complex_power: + assumes "0 < Re s" + shows "((\n. 1 / (of_nat n powr s)) ---> 0) sequentially" +proof - + have "\n>0. 3 \ n \ 1 \ ln (real_of_nat n)" + using ln3_gt_1 + by (force intro: order_trans [of _ "ln 3"] ln3_gt_1) + moreover have "(\n. cmod (Ln (of_nat n) / of_nat n powr s)) ----> 0" + using lim_Ln_over_power [OF assms] + by (metis tendsto_norm_zero_iff) + ultimately show ?thesis + apply (auto intro!: Lim_null_comparison [where g = "\n. norm (Ln(of_nat n) / of_nat n powr s)"]) + apply (auto simp: norm_divide divide_simps eventually_sequentially) + done +qed + +lemma lim_1_over_real_power: + fixes s :: real + assumes "0 < s" + shows "((\n. 1 / (of_nat n powr s)) ---> 0) sequentially" + using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms + apply (subst filterlim_sequentially_Suc [symmetric]) + apply (simp add: lim_sequentially dist_norm) + apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def) + done + +lemma lim_1_over_Ln: "((\n. 1 / Ln(of_nat n)) ---> 0) sequentially" +proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps) + fix r::real + assume "0 < r" + have ir: "inverse (exp (inverse r)) > 0" + by simp + obtain n where n: "1 < of_nat n * inverse (exp (inverse r))" + using ex_less_of_nat_mult [of _ 1, OF ir] + by auto + then have "exp (inverse r) < of_nat n" + by (simp add: divide_simps) + then have "ln (exp (inverse r)) < ln (of_nat n)" + by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff) + with `0 < r` have "1 < r * ln (real_of_nat n)" + by (simp add: field_simps) + moreover have "n > 0" using n + using neq0_conv by fastforce + ultimately show "\no. \n. Ln (of_nat n) \ 0 \ no \ n \ 1 < r * cmod (Ln (of_nat n))" + using n `0 < r` + apply (rule_tac x=n in exI) + apply (auto simp: divide_simps) + apply (erule less_le_trans, auto) + done +qed + +lemma lim_1_over_ln: "((\n. 1 / ln(real_of_nat n)) ---> 0) sequentially" + using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms + apply (subst filterlim_sequentially_Suc [symmetric]) + apply (simp add: lim_sequentially dist_norm) + apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def) + done + subsection{*Relation between Square Root and exp/ln, hence its derivative*} @@ -1526,7 +1827,7 @@ proof - have nz0: "1 + \*z \ 0" using assms - by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) + by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) less_irrefl minus_diff_eq mult.right_neutral right_minus_eq) have "z \ -\" using assms by auto @@ -1771,7 +2072,7 @@ by (blast intro: isCont_o2 [OF _ isCont_Arcsin]) lemma sin_Arcsin [simp]: "sin(Arcsin z) = z" -proof - +proof - have "\*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \ (\*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0" by (simp add: algebra_simps) --{*Cancelling a factor of 2*} moreover have "... \ (\*z) + csqrt (1 - z\<^sup>2) = 0" @@ -1903,7 +2204,7 @@ proof (cases "Im z = 0") case True then show ?thesis - using assms + using assms by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric]) next case False @@ -2323,13 +2624,13 @@ lemma arcsin_arctan: "-1 < x \ x < 1 \ arcsin x = arctan(x / sqrt(1 - x\<^sup>2))" by (simp add: arccos_arctan arcsin_arccos_eq) -lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \ 1 then sqrt (1 - x^2) else \ * sqrt (x^2 - 1))" +lemma csqrt_1_diff_eq: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \ 1 then sqrt (1 - x^2) else \ * sqrt (x^2 - 1))" by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg) lemma arcsin_arccos_sqrt_pos: "0 \ x \ x \ 1 \ arcsin x = arccos(sqrt(1 - x\<^sup>2))" apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos) apply (subst Arcsin_Arccos_csqrt_pos) - apply (auto simp: power_le_one zz) + apply (auto simp: power_le_one csqrt_1_diff_eq) done lemma arcsin_arccos_sqrt_neg: "-1 \ x \ x \ 0 \ arcsin x = -arccos(sqrt(1 - x\<^sup>2))" @@ -2339,7 +2640,7 @@ lemma arccos_arcsin_sqrt_pos: "0 \ x \ x \ 1 \ arccos x = arcsin(sqrt(1 - x\<^sup>2))" apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos) apply (subst Arccos_Arcsin_csqrt_pos) - apply (auto simp: power_le_one zz) + apply (auto simp: power_le_one csqrt_1_diff_eq) done lemma arccos_arcsin_sqrt_neg: "-1 \ x \ x \ 0 \ arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon May 25 22:11:43 2015 +0200 @@ -6356,6 +6356,24 @@ lemma segment_refl: "closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps) +lemma closed_segment_commute: "closed_segment a b = closed_segment b a" +proof - + have "{a, b} = {b, a}" by auto + thus ?thesis + by (simp add: segment_convex_hull) +qed + +lemma closed_segment_eq_real_ivl: + fixes a b::real + shows "closed_segment a b = (if a \ b then {a .. b} else {b .. a})" +proof - + have "b \ a \ closed_segment b a = {b .. a}" + and "a \ b \ closed_segment a b = {a .. b}" + by (auto simp: convex_hull_eq_real_cbox segment_convex_hull) + thus ?thesis + by (auto simp: closed_segment_commute) +qed + lemma between_mem_segment: "between (a,b) x \ x \ closed_segment a b" unfolding between_def by auto diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon May 25 22:11:43 2015 +0200 @@ -779,10 +779,225 @@ qed qed -text {* Still more general bound theorem. *} + +subsection {* More general bound theorems *} + +lemma differentiable_bound_general: + fixes f :: "real \ 'a::real_normed_vector" + assumes "a < b" + and f_cont: "continuous_on {a .. b} f" + and phi_cont: "continuous_on {a .. b} \" + and f': "\x. a < x \ x < b \ (f has_vector_derivative f' x) (at x)" + and phi': "\x. a < x \ x < b \ (\ has_vector_derivative \' x) (at x)" + and bnd: "\x. a < x \ x < b \ norm (f' x) \ \' x" + shows "norm (f b - f a) \ \ b - \ a" +proof - + { + fix x assume x: "a < x" "x < b" + have "0 \ norm (f' x)" by simp + also have "\ \ \' x" using x by (auto intro!: bnd) + finally have "0 \ \' x" . + } note phi'_nonneg = this + note f_tendsto = assms(2)[simplified continuous_on_def, rule_format] + note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format] + { + fix e::real assume "e > 0" + def e2 \ "e / 2" with `e > 0` have "e2 > 0" by simp + let ?le = "\x1. norm (f x1 - f a) \ \ x1 - \ a + e * (x1 - a) + e" + def A \ "{x2. a \ x2 \ x2 \ b \ (\x1\{a ..< x2}. ?le x1)}" + have A_subset: "A \ {a .. b}" by (auto simp: A_def) + { + fix x2 + assume a: "a \ x2" "x2 \ b" and le: "\x1\{a.. 0` + proof cases + assume "x2 \ a" with a have "a < x2" by simp + have "at x2 within {a <.. bot" + using `a < x2` + by (auto simp: trivial_limit_within islimpt_in_closure) + moreover + have "((\x1. (\ x1 - \ a) + e * (x1 - a) + e) ---> (\ x2 - \ a) + e * (x2 - a) + e) (at x2 within {a <..x1. norm (f x1 - f a)) ---> norm (f x2 - f a)) (at x2 within {a <..x. x > a) (at x2 within {a <.. A" + using assms by (auto simp: A_def) + hence [simp]: "A \ {}" by auto + have A_ivl: "\x1 x2. x2 \ A \ x1 \ {a ..x2} \ x1 \ A" + by (simp add: A_def) + have [simp]: "bdd_above A" by (auto simp: A_def) + def y \ "Sup A" + have "y \ b" + unfolding y_def + by (simp add: cSup_le_iff) (simp add: A_def) + have leI: "\x x1. a \ x1 \ x \ A \ x1 < x \ ?le x1" + by (auto simp: A_def intro!: le_cont) + have y_all_le: "\x1\{a.. y" + by (metis `a \ A` `bdd_above A` cSup_upper y_def) + have "y \ A" + using y_all_le `a \ y` `y \ b` + by (auto simp: A_def) + hence "A = {a .. y}" + using A_subset + by (auto simp: subset_iff y_def cSup_upper intro: A_ivl) + from le_cont[OF `a \ y` `y \ b` y_all_le] have le_y: "?le y" . + { + assume "a \ y" with `a \ y` have "a < y" by simp + have "y = b" + proof (rule ccontr) + assume "y \ b" + hence "y < b" using `y \ b` by simp + let ?F = "at y within {y.. has_vector_derivative \' y) ?F" + using `a < y` `y < b` + by (auto simp add: at_within_open[of _ "{a<..\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \ e2 * \x1 - y\" + "\\<^sub>F x1 in ?F. norm (\ x1 - \ y - (x1 - y) *\<^sub>R \' y) \ e2 * \x1 - y\" + using `e2 > 0` + by (auto simp: has_derivative_within_alt2 has_vector_derivative_def) + moreover + have "\\<^sub>F x1 in ?F. y \ x1" "\\<^sub>F x1 in ?F. x1 < b" + by (auto simp: eventually_at_filter) + ultimately + have "\\<^sub>F x1 in ?F. norm (f x1 - f y) \ (\ x1 - \ y) + e * \x1 - y\" + (is "\\<^sub>F x1 in ?F. ?le' x1") + proof eventually_elim + case elim + from norm_triangle_ineq2[THEN order_trans, OF elim(1)] + have "norm (f x1 - f y) \ norm (f' y) * \x1 - y\ + e2 * \x1 - y\" + by (simp add: ac_simps) + also have "norm (f' y) \ \' y" using bnd `a < y` `y < b` by simp + also + from elim have "\' y * \x1 - y\ \ \ x1 - \ y + e2 * \x1 - y\" + by (simp add: ac_simps) + finally + have "norm (f x1 - f y) \ \ x1 - \ y + e2 * \x1 - y\ + e2 * \x1 - y\" + by (auto simp: mult_right_mono) + thus ?case by (simp add: e2_def) + qed + moreover have "?le' y" by simp + ultimately obtain S + where S: "open S" "y \ S" "\x. x\S \ x \ {y.. ?le' x" + unfolding eventually_at_topological + by metis + from `open S` obtain d where d: "\x. dist x y < d \ x \ S" "d > 0" + by (force simp: dist_commute open_real_def ball_def + dest!: bspec[OF _ `y \ S`]) + def d' \ "min ((y + b)/2) (y + (d/2))" + have "d' \ A" + unfolding A_def + proof safe + show "a \ d'" using `a < y` `0 < d` `y < b` by (simp add: d'_def) + show "d' \ b" using `y < b` by (simp add: d'_def min_def) + fix x1 + assume x1: "x1 \ {a.. {a.. y" + hence x1': "x1 \ S" "x1 \ {y.. norm (f x1 - f y) + norm (f y - f a)" + by (rule order_trans[OF _ norm_triangle_ineq]) simp + also note S(3)[OF x1'] + also note le_y + finally have "?le x1" + using `x1 \ y` by (auto simp: algebra_simps) + } ultimately show "?le x1" by arith + qed + hence "d' \ y" + unfolding y_def + by (rule cSup_upper) simp + thus False using `d > 0` `y < b` + by (simp add: d'_def min_def split: split_if_asm) + qed + } moreover { + assume "a = y" + with `a < b` have "y < b" by simp + with `a = y` f_cont phi_cont `e2 > 0` + have 1: "\\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2" + and 2: "\\<^sub>F x in at y within {y..b}. dist (\ x) (\ y) < e2" + by (auto simp: continuous_on_def tendsto_iff) + have 3: "eventually (\x. y < x) (at y within {y..b})" + by (auto simp: eventually_at_filter) + have 4: "eventually (\x::real. x < b) (at y within {y..b})" + using _ `y < b` + by (rule order_tendstoD) (auto intro!: tendsto_eq_intros) + from 1 2 3 4 + have eventually_le: "eventually (\x. ?le x) (at y within {y .. b})" + proof eventually_elim + case (elim x1) + have "norm (f x1 - f a) = norm (f x1 - f y)" + by (simp add: `a = y`) + also have "norm (f x1 - f y) \ e2" + using elim `a = y` by (auto simp : dist_norm intro!: less_imp_le) + also have "\ \ e2 + (\ x1 - \ a + e2 + e * (x1 - a))" + using `0 < e` elim + by (intro add_increasing2[OF add_nonneg_nonneg order.refl]) + (auto simp: `a = y` dist_norm intro!: mult_nonneg_nonneg) + also have "\ = \ x1 - \ a + e * (x1 - a) + e" + by (simp add: e2_def) + finally show "?le x1" . + qed + from this[unfolded eventually_at_topological] `?le y` + obtain S + where S: "open S" "y \ S" "\x. x\S \ x \ {y..b} \ ?le x" + by metis + from `open S` obtain d where d: "\x. dist x y < d \ x \ S" "d > 0" + by (force simp: dist_commute open_real_def ball_def + dest!: bspec[OF _ `y \ S`]) + def d' \ "min b (y + (d/2))" + have "d' \ A" + unfolding A_def + proof safe + show "a \ d'" using `a = y` `0 < d` `y < b` by (simp add: d'_def) + show "d' \ b" by (simp add: d'_def) + fix x1 + assume "x1 \ {a.. S" "x1 \ {y..b}" + by (auto simp: `a = y` d'_def dist_real_def intro!: d ) + thus "?le x1" + by (rule S) + qed + hence "d' \ y" + unfolding y_def + by (rule cSup_upper) simp + hence "y = b" using `d > 0` `y < b` + by (simp add: d'_def) + } ultimately have "y = b" + by auto + with le_y have "norm (f b - f a) \ \ b - \ a + e * (b - a + 1)" + by (simp add: algebra_simps) + } note * = this + { + fix e::real assume "e > 0" + hence "norm (f b - f a) \ \ b - \ a + e" + using *[of "e / (b - a + 1)"] `a < b` by simp + } thus ?thesis + by (rule field_le_epsilon) +qed lemma differentiable_bound: - fixes f :: "'a::real_normed_vector \ 'b::real_inner" + fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "convex s" and "\x\s. (f has_derivative f' x) (at x within s)" and "\x\s. onorm (f' x) \ B" @@ -791,14 +1006,15 @@ shows "norm (f x - f y) \ B * norm (x - y)" proof - let ?p = "\u. x + u *\<^sub>R (y - x)" + let ?\ = "\h. h * B * norm (x - y)" have *: "\u. u\{0..1} \ x + u *\<^sub>R (y - x) \ s" using assms(1)[unfolded convex_alt,rule_format,OF x y] unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by (auto simp add: algebra_simps) - then have 1: "continuous_on {0 .. 1} (f \ ?p)" + have 0: "continuous_on (?p ` {0..1}) f" + using * + unfolding continuous_on_eq_continuous_within apply - - apply (rule continuous_intros)+ - unfolding continuous_on_eq_continuous_within apply rule apply (rule differentiable_imp_continuous_within) unfolding differentiable_def @@ -807,57 +1023,99 @@ apply (rule assms(2)[rule_format]) apply auto done - have 2: "\u\{0 <..< 1}. - ((f \ ?p) has_derivative f' (x + u *\<^sub>R (y - x)) \ (\u. 0 + u *\<^sub>R (y - x))) (at u)" - proof rule - case goal1 - let ?u = "x + u *\<^sub>R (y - x)" + from * have 1: "continuous_on {0 .. 1} (f \ ?p)" + by (intro continuous_intros 0)+ + { + fix u::real assume u: "u \{0 <..< 1}" + let ?u = "?p u" + interpret linear "(f' ?u)" + using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *) have "(f \ ?p has_derivative (f' ?u) \ (\u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)" apply (rule diff_chain_within) apply (rule derivative_intros)+ apply (rule has_derivative_within_subset) apply (rule assms(2)[rule_format]) - using goal1 * + using u * apply auto done - then show ?case - by (simp add: has_derivative_within_open[OF goal1 open_greaterThanLessThan]) - qed - obtain u where u: - "u \ {0<..<1}" - "norm ((f \ (\u. x + u *\<^sub>R (y - x))) 1 - (f \ (\u. x + u *\<^sub>R (y - x))) 0) - \ norm ((f' (x + u *\<^sub>R (y - x)) \ (\u. 0 + u *\<^sub>R (y - x))) (1 - 0))" - using mvt_general[OF zero_less_one 1 2] .. - have **: "\x y. x \ s \ norm (f' x y) \ B * norm y" - proof - - case goal1 - have "norm (f' x y) \ onorm (f' x) * norm y" - by (rule onorm[OF has_derivative_bounded_linear[OF assms(2)[rule_format,OF goal1]]]) - also have "\ \ B * norm y" - apply (rule mult_right_mono) - using assms(3)[rule_format,OF goal1] - apply (auto simp add: field_simps) - done - finally show ?case - by simp - qed + hence "((f \ ?p) has_vector_derivative f' ?u (y - x)) (at u)" + by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan] + scaleR has_vector_derivative_def o_def) + } note 2 = this + { + have "continuous_on {0..1} ?\" + by (rule continuous_intros)+ + } note 3 = this + { + fix u::real assume u: "u \{0 <..< 1}" + have "(?\ has_vector_derivative B * norm (x - y)) (at u)" + by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros) + } note 4 = this + { + fix u::real assume u: "u \{0 <..< 1}" + let ?u = "?p u" + interpret bounded_linear "(f' ?u)" + using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *) + have "norm (f' ?u (y - x)) \ onorm (f' ?u) * norm (y - x)" + by (rule onorm) fact + also have "onorm (f' ?u) \ B" + using u by (auto intro!: assms(3)[rule_format] *) + finally have "norm ((f' ?u) (y - x)) \ B * norm (x - y)" + by (simp add: mult_right_mono norm_minus_commute) + } note 5 = this have "norm (f x - f y) = norm ((f \ (\u. x + u *\<^sub>R (y - x))) 1 - (f \ (\u. x + u *\<^sub>R (y - x))) 0)" by (auto simp add: norm_minus_commute) - also have "\ \ norm (f' (x + u *\<^sub>R (y - x)) (y - x))" - using u by auto - also have "\ \ B * norm(y - x)" - apply (rule **) - using * and u - apply auto - done - finally show ?thesis - by (auto simp add: norm_minus_commute) + also + from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5] + have "norm ((f \ ?p) 1 - (f \ ?p) 0) \ B * norm (x - y)" + by simp + finally show ?thesis . +qed + +lemma + differentiable_bound_segment: + fixes f::"'a::real_normed_vector \ 'b::real_normed_vector" + assumes "\t. t \ {0..1} \ x0 + t *\<^sub>R a \ G" + assumes f': "\x. x \ G \ (f has_derivative f' x) (at x within G)" + assumes B: "\x\{0..1}. onorm (f' (x0 + x *\<^sub>R a)) \ B" + shows "norm (f (x0 + a) - f x0) \ norm a * B" +proof - + let ?G = "(\x. x0 + x *\<^sub>R a) ` {0..1}" + have "?G = op + x0 ` (\x. x *\<^sub>R a) ` {0..1}" by auto + also have "convex \" + by (intro convex_translation convex_scaled convex_real_interval) + finally have "convex ?G" . + moreover have "?G \ G" "x0 \ ?G" "x0 + a \ ?G" using assms by (auto intro: image_eqI[where x=1]) + ultimately show ?thesis + using has_derivative_subset[OF f' `?G \ G`] B + differentiable_bound[of "(\x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0] + by (auto simp: ac_simps) +qed + +lemma differentiable_bound_linearization: + fixes f::"'a::real_normed_vector \ 'b::real_normed_vector" + assumes "\t. t \ {0..1} \ a + t *\<^sub>R (b - a) \ S" + assumes f'[derivative_intros]: "\x. x \ S \ (f has_derivative f' x) (at x within S)" + assumes B: "\x\S. onorm (f' x - f' x0) \ B" + assumes "x0 \ S" + shows "norm (f b - f a - f' x0 (b - a)) \ norm (b - a) * B" +proof - + def g \ "\x. f x - f' x0 x" + have g: "\x. x \ S \ (g has_derivative (\i. f' x i - f' x0 i)) (at x within S)" + unfolding g_def using assms + by (auto intro!: derivative_eq_intros + bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f']) + from B have B: "\x\{0..1}. onorm (\i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \ B" + using assms by (auto simp: fun_diff_def) + from differentiable_bound_segment[OF assms(1) g B] `x0 \ S` + show ?thesis + by (simp add: g_def field_simps linear_sub[OF has_derivative_linear[OF f']]) qed text {* In particular. *} lemma has_derivative_zero_constant: - fixes f :: "'a::real_normed_vector \ 'b::real_inner" + fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "convex s" and "\x. x \ s \ (f has_derivative (\h. 0)) (at x within s)" shows "\c. \x\s. f x = c" @@ -872,7 +1130,7 @@ qed lemma has_derivative_zero_unique: - fixes f :: "'a::real_normed_vector \ 'b::real_inner" + fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "convex s" and "\x. x \ s \ (f has_derivative (\h. 0)) (at x within s)" and "x \ s" "y \ s" @@ -880,7 +1138,7 @@ using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force lemma has_derivative_zero_unique_connected: - fixes f :: "'a::real_normed_vector \ 'b::real_inner" + fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes "open s" "connected s" assumes f: "\x. x \ s \ (f has_derivative (\x. 0)) (at x)" assumes "x \ s" "y \ s" @@ -1573,7 +1831,7 @@ subsection {* Uniformly convergent sequence of derivatives *} lemma has_derivative_sequence_lipschitz_lemma: - fixes f :: "nat \ 'a::real_normed_vector \ 'b::real_inner" + fixes f :: "nat \ 'a::real_normed_vector \ 'b::real_normed_vector" assumes "convex s" and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" and "\n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" @@ -1608,7 +1866,7 @@ qed lemma has_derivative_sequence_lipschitz: - fixes f :: "nat \ 'a::real_normed_vector \ 'b::real_inner" + fixes f :: "nat \ 'a::real_normed_vector \ 'b::real_normed_vector" assumes "convex s" and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" and "\e>0. \N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" @@ -1628,7 +1886,7 @@ qed lemma has_derivative_sequence: - fixes f :: "nat \ 'a::real_normed_vector \ 'b::{real_inner, complete_space}" + fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" assumes "convex s" and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" and "\e>0. \N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" @@ -1832,7 +2090,7 @@ text {* Can choose to line up antiderivatives if we want. *} lemma has_antiderivative_sequence: - fixes f :: "nat \ 'a::real_normed_vector \ 'b::{real_inner, complete_space}" + fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" assumes "convex s" and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" and "\e>0. \N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" @@ -1853,7 +2111,7 @@ qed auto lemma has_antiderivative_limit: - fixes g' :: "'a::real_normed_vector \ 'a \ 'b::{real_inner, complete_space}" + fixes g' :: "'a::real_normed_vector \ 'a \ 'b::banach" assumes "convex s" and "\e>0. \f f'. \x\s. (f has_derivative (f' x)) (at x within s) \ (\h. norm (f' x h - g' x h) \ e * norm h)" @@ -1905,7 +2163,7 @@ subsection {* Differentiation of a series *} lemma has_derivative_series: - fixes f :: "nat \ 'a::real_normed_vector \ 'b::{real_inner, complete_space}" + fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" assumes "convex s" and "\n x. x \ s \ ((f n) has_derivative (f' n x)) (at x within s)" and "\e>0. \N. \n\N. \x\s. \h. norm (setsum (\i. f' i x h) {.. e * norm h" @@ -1922,81 +2180,6 @@ text {* Considering derivative @{typ "real \ 'b\real_normed_vector"} as a vector. *} -lemma has_field_derivative_iff_has_vector_derivative: - "(f has_field_derivative y) F \ (f has_vector_derivative y) F" - unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs .. - -lemma has_field_derivative_subset: - "(f has_field_derivative y) (at x within s) \ t \ s \ (f has_field_derivative y) (at x within t)" - unfolding has_field_derivative_def by (rule has_derivative_subset) - -lemma has_vector_derivative_const[simp, derivative_intros]: "((\x. c) has_vector_derivative 0) net" - by (auto simp: has_vector_derivative_def) - -lemma has_vector_derivative_id[simp, derivative_intros]: "((\x. x) has_vector_derivative 1) net" - by (auto simp: has_vector_derivative_def) - -lemma has_vector_derivative_minus[derivative_intros]: - "(f has_vector_derivative f') net \ ((\x. - f x) has_vector_derivative (- f')) net" - by (auto simp: has_vector_derivative_def) - -lemma has_vector_derivative_add[derivative_intros]: - "(f has_vector_derivative f') net \ (g has_vector_derivative g') net \ - ((\x. f x + g x) has_vector_derivative (f' + g')) net" - by (auto simp: has_vector_derivative_def scaleR_right_distrib) - -lemma has_vector_derivative_setsum[derivative_intros]: - "(\i. i \ I \ (f i has_vector_derivative f' i) net) \ - ((\x. \i\I. f i x) has_vector_derivative (\i\I. f' i)) net" - by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_setsum_right intro!: derivative_eq_intros) - -lemma has_vector_derivative_diff[derivative_intros]: - "(f has_vector_derivative f') net \ (g has_vector_derivative g') net \ - ((\x. f x - g x) has_vector_derivative (f' - g')) net" - by (auto simp: has_vector_derivative_def scaleR_diff_right) - -lemma (in bounded_linear) has_vector_derivative: - assumes "(g has_vector_derivative g') F" - shows "((\x. f (g x)) has_vector_derivative f g') F" - using has_derivative[OF assms[unfolded has_vector_derivative_def]] - by (simp add: has_vector_derivative_def scaleR) - -lemma (in bounded_bilinear) has_vector_derivative: - assumes "(f has_vector_derivative f') (at x within s)" - and "(g has_vector_derivative g') (at x within s)" - shows "((\x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)" - using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]] - by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib) - -lemma has_vector_derivative_scaleR[derivative_intros]: - "(f has_field_derivative f') (at x within s) \ (g has_vector_derivative g') (at x within s) \ - ((\x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)" - unfolding has_field_derivative_iff_has_vector_derivative - by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR]) - -lemma has_vector_derivative_mult[derivative_intros]: - "(f has_vector_derivative f') (at x within s) \ (g has_vector_derivative g') (at x within s) \ - ((\x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)" - by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult]) - -lemma has_vector_derivative_of_real[derivative_intros]: - "(f has_field_derivative D) F \ ((\x. of_real (f x)) has_vector_derivative (of_real D)) F" - by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real]) - (simp add: has_field_derivative_iff_has_vector_derivative) - -lemma has_vector_derivative_continuous: "(f has_vector_derivative D) (at x within s) \ continuous (at x within s) f" - by (auto intro: has_derivative_continuous simp: has_vector_derivative_def) - -lemma has_vector_derivative_mult_right[derivative_intros]: - fixes a :: "'a :: real_normed_algebra" - shows "(f has_vector_derivative x) F \ ((\x. a * f x) has_vector_derivative (a * x)) F" - by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right]) - -lemma has_vector_derivative_mult_left[derivative_intros]: - fixes a :: "'a :: real_normed_algebra" - shows "(f has_vector_derivative x) F \ ((\x. f x * a) has_vector_derivative (x * a)) F" - by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left]) - definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" lemma vector_derivative_unique_at: diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon May 25 22:11:43 2015 +0200 @@ -6887,6 +6887,121 @@ qed +subsection {* Taylor series expansion *} + +lemma + setsum_telescope: + fixes f::"nat \ 'a::ab_group_add" + shows "setsum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" + by (induct i) simp_all + +lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative: + assumes "p>0" + and f0: "Df 0 = f" + and Df: "\m t. m < p \ a \ t \ t \ b \ + (Df m has_vector_derivative Df (Suc m) t) (at t within {a .. b})" + and g0: "Dg 0 = g" + and Dg: "\m t. m < p \ a \ t \ t \ b \ + (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" + and ivl: "a \ t" "t \ b" + shows "((\t. \iR prod (Df i t) (Dg (p - Suc i) t)) + has_vector_derivative + prod (f t) (Dg p t) - (-1)^p *\<^sub>R prod (Df p t) (g t)) + (at t within {a .. b})" + using assms +proof cases + assume p: "p \ 1" + def p' \ "p - 2" + from assms p have p': "{..i. i \ p' \ Suc (Suc p' - i) = (Suc (Suc p') - i)" + by auto + let ?f = "\i. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg ((p - i)) t))" + have "(\iR (prod (Df i t) (Dg (Suc (p - Suc i)) t) + + prod (Df (Suc i) t) (Dg (p - Suc i) t))) = + (\i\(Suc p'). ?f i - ?f (Suc i))" + by (auto simp: algebra_simps p'(2) numeral_2_eq_2 * lessThan_Suc_atMost) + also note setsum_telescope + finally + have "(\iR (prod (Df i t) (Dg (Suc (p - Suc i)) t) + + prod (Df (Suc i) t) (Dg (p - Suc i) t))) + = prod (f t) (Dg p t) - (- 1) ^ p *\<^sub>R prod (Df p t) (g t)" + unfolding p'[symmetric] + by (simp add: assms) + thus ?thesis + using assms + by (auto intro!: derivative_eq_intros has_vector_derivative) +qed (auto intro!: derivative_eq_intros has_vector_derivative) + +lemma taylor_integral: + fixes f::"real\'a::banach" + assumes "p>0" + and f0: "Df 0 = f" + and Df: "\m t. m < p \ a \ t \ t \ b \ + (Df m has_vector_derivative Df (Suc m) t) (at t within {a .. b})" + and ivl: "a \ b" + shows "f b = (\iR Df i a) + + integral {a..b} (\x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)" +proof - + interpret bounded_bilinear "scaleR::real\'a\'a" + by (rule bounded_bilinear_scaleR) + def g \ "\s. (b - s)^(p - 1)/fact (p - 1)" + def Dg \ "\n s. if n < p then (-1)^n * (b - s)^(p - 1 - n) / fact (p - 1 - n) else 0" + have g0: "Dg 0 = g" + using `p > 0` + by (auto simp add: Dg_def divide_simps g_def split: split_if_asm) + { + fix m + assume "p > Suc m" + hence "p - Suc m = Suc (p - Suc (Suc m))" + by auto + hence "real (p - Suc m) * fact (p - Suc (Suc m)) = fact (p - Suc m)" + by auto + } note fact_eq = this + have Dg: "\m t. m < p \ a \ t \ t \ b \ + (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" + unfolding Dg_def + by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def + fact_eq real_eq_of_nat[symmetric] divide_simps) + from setsum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df, + OF `p > 0` g0 Dg f0 Df] + have deriv: "\t. a \ t \ t \ b \ + ((\t. \iR Dg i t *\<^sub>R Df (p - Suc i) t) has_vector_derivative + g t *\<^sub>R Df p t - (- 1) ^ p *\<^sub>R Dg p t *\<^sub>R f t) (at t within {a..b})" + by auto + from fundamental_theorem_of_calculus[rule_format, OF `a \ b` deriv] + have ftc: "integral {a..b} (\x. g x *\<^sub>R Df p x - (- 1) ^ p *\<^sub>R Dg p x *\<^sub>R f x) = + (\iR Dg i b *\<^sub>R Df (p - Suc i) b) - + (\iR Dg i a *\<^sub>R Df (p - Suc i) a)" + unfolding atLeastAtMost_iff by (auto dest!: integral_unique) + def p' \ "p - 1" + have p': "p = Suc p'" using `p > 0` by (simp add: p'_def) + have Dgp': "Dg p' = (\_. (- 1) ^ p')" + by (auto simp: Dg_def p') + have one: "\p'. (- 1::real) ^ p' * (- 1) ^ p' = 1" + "\p' k. (- 1::real) ^ p' * ((- 1) ^ p' * k) = k" + by (simp_all add: power_mult_distrib[symmetric] ) + from ftc + have "f b = + (\iR Df (p' - i) a) + + integral {a..b} (\x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)" + by (simp add: p' assms Dgp' one Dg_def g_def zero_power) + also + have "{..x. p - x - 1) ` {.. (\x. p - x - 1) ` {..iR Df (p' - i) a) = + (\iR Df i a)" + by (rule setsum.reindex_cong) (auto simp add: p' inj_on_def) + finally show "f b = (\iR Df i a) + + integral {a..b} (\x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)" . +qed + + subsection {* Attempt a systematic general set of "offset" results for components. *} lemma gauge_modify: diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon May 25 22:11:43 2015 +0200 @@ -28,7 +28,7 @@ lemma square_continuous: fixes e :: real shows "e > 0 \ \d. 0 < d \ (\y. \y - x\ < d \ \y * y - x * x\ < e)" - using isCont_power[OF isCont_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2] + using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2] apply (auto simp add: power2_eq_square) apply (rule_tac x="s" in exI) apply auto @@ -575,9 +575,8 @@ by simp also have "\ \ (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric]) + using mult_left_mono[OF p Suc.prems] apply (simp add: field_simps) - using mult_left_mono[OF p Suc.prems] - apply simp done finally show ?case by (simp add: real_of_nat_Suc field_simps) @@ -887,10 +886,8 @@ assumes "0 \ A" shows "dependent A" unfolding dependent_def - apply (rule_tac x=0 in bexI) using assms span_0 - apply auto - done + by auto lemma (in real_vector) span_add: "x \ span S \ y \ span S \ x + y \ span S" by (metis subspace_add subspace_span) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon May 25 22:11:43 2015 +0200 @@ -705,7 +705,7 @@ apply (clarsimp simp add: less_diff_eq) by (metis dist_commute dist_triangle_lt) assume ?rhs then have 2: "S = U \ T" - unfolding T_def + unfolding T_def by auto (metis dist_self) from 1 2 show ?lhs unfolding openin_open open_dist by fast @@ -1750,10 +1750,6 @@ text {* Some property holds "sufficiently close" to the limit point. *} -lemma eventually_at2: - "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" - unfolding eventually_at dist_nz by auto - lemma eventually_happens: "eventually P net \ trivial_limit net \ (\x. P x)" unfolding trivial_limit_def by (auto elim: eventually_rev_mp) @@ -2051,100 +2047,6 @@ shows "netlimit (at x within S) = x" using assms by (metis at_within_interior netlimit_at) -text{* Transformation of limit. *} - -lemma Lim_transform: - fixes f g :: "'a::type \ 'b::real_normed_vector" - assumes "((\x. f x - g x) ---> 0) net" "(f ---> l) net" - shows "(g ---> l) net" - using tendsto_diff [OF assms(2) assms(1)] by simp - -lemma Lim_transform_eventually: - "eventually (\x. f x = g x) net \ (f ---> l) net \ (g ---> l) net" - apply (rule topological_tendstoI) - apply (drule (2) topological_tendstoD) - apply (erule (1) eventually_elim2, simp) - done - -lemma Lim_transform_within: - assumes "0 < d" - and "\x'\S. 0 < dist x' x \ dist x' x < d \ f x' = g x'" - and "(f ---> l) (at x within S)" - shows "(g ---> l) (at x within S)" -proof (rule Lim_transform_eventually) - show "eventually (\x. f x = g x) (at x within S)" - using assms(1,2) by (auto simp: dist_nz eventually_at) - show "(f ---> l) (at x within S)" by fact -qed - -lemma Lim_transform_at: - assumes "0 < d" - and "\x'. 0 < dist x' x \ dist x' x < d \ f x' = g x'" - and "(f ---> l) (at x)" - shows "(g ---> l) (at x)" - using _ assms(3) -proof (rule Lim_transform_eventually) - show "eventually (\x. f x = g x) (at x)" - unfolding eventually_at2 - using assms(1,2) by auto -qed - -text{* Common case assuming being away from some crucial point like 0. *} - -lemma Lim_transform_away_within: - fixes a b :: "'a::t1_space" - assumes "a \ b" - and "\x\S. x \ a \ x \ b \ f x = g x" - and "(f ---> l) (at a within S)" - shows "(g ---> l) (at a within S)" -proof (rule Lim_transform_eventually) - show "(f ---> l) (at a within S)" by fact - show "eventually (\x. f x = g x) (at a within S)" - unfolding eventually_at_topological - by (rule exI [where x="- {b}"], simp add: open_Compl assms) -qed - -lemma Lim_transform_away_at: - fixes a b :: "'a::t1_space" - assumes ab: "a\b" - and fg: "\x. x \ a \ x \ b \ f x = g x" - and fl: "(f ---> l) (at a)" - shows "(g ---> l) (at a)" - using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp - -text{* Alternatively, within an open set. *} - -lemma Lim_transform_within_open: - assumes "open S" and "a \ S" - and "\x\S. x \ a \ f x = g x" - and "(f ---> l) (at a)" - shows "(g ---> l) (at a)" -proof (rule Lim_transform_eventually) - show "eventually (\x. f x = g x) (at a)" - unfolding eventually_at_topological - using assms(1,2,3) by auto - show "(f ---> l) (at a)" by fact -qed - -text{* A congruence rule allowing us to transform limits assuming not at point. *} - -(* FIXME: Only one congruence rule for tendsto can be used at a time! *) - -lemma Lim_cong_within(*[cong add]*): - assumes "a = b" - and "x = y" - and "S = T" - and "\x. x \ b \ x \ T \ f x = g x" - shows "(f ---> x) (at a within S) \ (g ---> y) (at b within T)" - unfolding tendsto_def eventually_at_topological - using assms by simp - -lemma Lim_cong_at(*[cong add]*): - assumes "a = b" "x = y" - and "\x. x \ a \ f x = g x" - shows "((\x. f x) ---> x) (at a) \ ((g ---> y) (at a))" - unfolding tendsto_def eventually_at_topological - using assms by simp text{* Useful lemmas on closure and set of possible sequential limits.*} @@ -4902,7 +4804,7 @@ lemmas continuous_within_id = continuous_ident -lemmas continuous_at_id = isCont_ident +lemmas continuous_at_id = continuous_ident lemma continuous_infdist[continuous_intros]: assumes "continuous F f" @@ -6793,6 +6695,90 @@ (if cbox a b = {} then {} else if 0 \ m then cbox (m *\<^sub>R a) (m *\<^sub>R b) else cbox (m *\<^sub>R b) (m *\<^sub>R a))" using image_affinity_cbox[of m 0 a b] by auto +lemma islimpt_greaterThanLessThan1: + fixes a b::"'a::{linorder_topology, dense_order}" + assumes "a < b" + shows "a islimpt {a<.. T" + from open_right[OF this `a < b`] + obtain c where c: "a < c" "{a.. T" by auto + with assms dense[of a "min c b"] + show "\y\{a<.. T \ y \ a" + by (metis atLeastLessThan_iff greaterThanLessThan_iff min_less_iff_conj + not_le order.strict_implies_order subset_eq) +qed + +lemma islimpt_greaterThanLessThan2: + fixes a b::"'a::{linorder_topology, dense_order}" + assumes "a < b" + shows "b islimpt {a<.. T" + from open_left[OF this `a < b`] + obtain c where c: "c < b" "{c<..b} \ T" by auto + with assms dense[of "max a c" b] + show "\y\{a<.. T \ y \ b" + by (metis greaterThanAtMost_iff greaterThanLessThan_iff max_less_iff_conj + not_le order.strict_implies_order subset_eq) +qed + +lemma closure_greaterThanLessThan[simp]: + fixes a b::"'a::{linorder_topology, dense_order}" + shows "a < b \ closure {a <..< b} = {a .. b}" (is "_ \ ?l = ?r") +proof + have "?l \ closure ?r" + by (rule closure_mono) auto + thus "closure {a<.. {a..b}" by simp +qed (auto simp: closure_def order.order_iff_strict islimpt_greaterThanLessThan1 + islimpt_greaterThanLessThan2) + +lemma closure_greaterThan[simp]: + fixes a b::"'a::{no_top, linorder_topology, dense_order}" + shows "closure {a<..} = {a..}" +proof - + from gt_ex obtain b where "a < b" by auto + hence "{a<..} = {a<.. {b..}" by auto + also have "closure \ = {a..}" using `a < b` unfolding closure_union + by auto + finally show ?thesis . +qed + +lemma closure_lessThan[simp]: + fixes b::"'a::{no_bot, linorder_topology, dense_order}" + shows "closure {.. {..a}" by auto + also have "closure \ = {..b}" using `a < b` unfolding closure_union + by auto + finally show ?thesis . +qed + +lemma closure_atLeastLessThan[simp]: + fixes a b::"'a::{linorder_topology, dense_order}" + assumes "a < b" + shows "closure {a ..< b} = {a .. b}" +proof - + from assms have "{a ..< b} = {a} \ {a <..< b}" by auto + also have "closure \ = {a .. b}" unfolding closure_union + by (auto simp add: assms less_imp_le) + finally show ?thesis . +qed + +lemma closure_greaterThanAtMost[simp]: + fixes a b::"'a::{linorder_topology, dense_order}" + assumes "a < b" + shows "closure {a <.. b} = {a .. b}" +proof - + from assms have "{a <.. b} = {b} \ {a <..< b}" by auto + also have "closure \ = {a .. b}" unfolding closure_union + by (auto simp add: assms less_imp_le) + finally show ?thesis . +qed + subsection {* Homeomorphisms *} diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Nat.thy Mon May 25 22:11:43 2015 +0200 @@ -1877,6 +1877,11 @@ shows "mono Q \ mono (\i. (Q ^^ i) \)" by (auto intro!: funpow_decreasing simp: mono_def) +lemma antimono_funpow: + fixes Q :: "('i \ 'a::{lattice, order_top}) \ ('i \ 'a)" + shows "mono Q \ antimono (\i. (Q ^^ i) \)" + by (auto intro!: funpow_increasing simp: antimono_def) + subsection {* The divides relation on @{typ nat} *} lemma dvd_1_left [iff]: "Suc 0 dvd k" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Nominal/Examples/Class2.thy --- a/src/HOL/Nominal/Examples/Class2.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Nominal/Examples/Class2.thy Mon May 25 22:11:43 2015 +0200 @@ -2865,13 +2865,7 @@ using ty_cases sum_cases apply(auto simp add: ty.inject) apply(drule_tac x="x" in meta_spec) -apply(auto simp add: ty.inject) -apply(rotate_tac 10) -apply(drule_tac x="a" in meta_spec) -apply(auto simp add: ty.inject) -apply(rotate_tac 10) -apply(drule_tac x="a" in meta_spec) -apply(auto simp add: ty.inject) +apply(fastforce simp add: ty.inject) done termination diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/NthRoot.thy Mon May 25 22:11:43 2015 +0200 @@ -7,7 +7,7 @@ section {* Nth Roots of Real Numbers *} theory NthRoot -imports Deriv +imports Deriv Binomial begin lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)" @@ -644,6 +644,90 @@ apply auto done +lemma LIMSEQ_root: "(\n. root n n) ----> 1" +proof - + def x \ "\n. root n n - 1" + have "x ----> sqrt 0" + proof (rule tendsto_sandwich[OF _ _ tendsto_const]) + show "(\x. sqrt (2 / x)) ----> sqrt 0" + by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) + (simp_all add: at_infinity_eq_at_top_bot) + { fix n :: nat assume "2 < n" + have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2" + using `2 < n` unfolding gbinomial_def binomial_gbinomial + by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric]) + also have "\ \ (\k\{0, 2}. of_nat (n choose k) * x n^k)" + by (simp add: x_def) + also have "\ \ (\k=0..n. of_nat (n choose k) * x n^k)" + using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) + also have "\ = (x n + 1) ^ n" + by (simp add: binomial_ring) + also have "\ = n" + using `2 < n` by (simp add: x_def) + finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \ real (n - 1) * 1" + by simp + then have "(x n)\<^sup>2 \ 2 / real n" + using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps) + from real_sqrt_le_mono[OF this] have "x n \ sqrt (2 / real n)" + by simp } + then show "eventually (\n. x n \ sqrt (2 / real n)) sequentially" + by (auto intro!: exI[of _ 3] simp: eventually_sequentially) + show "eventually (\n. sqrt 0 \ x n) sequentially" + by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) + qed + from tendsto_add[OF this tendsto_const[of 1]] show ?thesis + by (simp add: x_def) +qed + +lemma LIMSEQ_root_const: + assumes "0 < c" + shows "(\n. root n c) ----> 1" +proof - + { fix c :: real assume "1 \ c" + def x \ "\n. root n c - 1" + have "x ----> 0" + proof (rule tendsto_sandwich[OF _ _ tendsto_const]) + show "(\n. c / n) ----> 0" + by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) + (simp_all add: at_infinity_eq_at_top_bot) + { fix n :: nat assume "1 < n" + have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1" + using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric]) + also have "\ \ (\k\{0, 1}. of_nat (n choose k) * x n^k)" + by (simp add: x_def) + also have "\ \ (\k=0..n. of_nat (n choose k) * x n^k)" + using `1 < n` `1 \ c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) + also have "\ = (x n + 1) ^ n" + by (simp add: binomial_ring) + also have "\ = c" + using `1 < n` `1 \ c` by (simp add: x_def) + finally have "x n \ c / n" + using `1 \ c` `1 < n` by (simp add: field_simps) } + then show "eventually (\n. x n \ c / n) sequentially" + by (auto intro!: exI[of _ 3] simp: eventually_sequentially) + show "eventually (\n. 0 \ x n) sequentially" + using `1 \ c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def) + qed + from tendsto_add[OF this tendsto_const[of 1]] have "(\n. root n c) ----> 1" + by (simp add: x_def) } + note ge_1 = this + + show ?thesis + proof cases + assume "1 \ c" with ge_1 show ?thesis by blast + next + assume "\ 1 \ c" + with `0 < c` have "1 \ 1 / c" + by simp + then have "(\n. 1 / root n (1 / c)) ----> 1 / 1" + by (intro tendsto_divide tendsto_const ge_1 `1 \ 1 / c` one_neq_zero) + then show ?thesis + by (rule filterlim_cong[THEN iffD1, rotated 3]) + (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide) + qed +qed + + text "Legacy theorem names:" lemmas real_root_pos2 = real_root_power_cancel lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le] diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Number_Theory/Fib.thy --- a/src/HOL/Number_Theory/Fib.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Number_Theory/Fib.thy Mon May 25 22:11:43 2015 +0200 @@ -11,11 +11,11 @@ section {* Fib *} theory Fib -imports Main "../GCD" +imports Main "../GCD" "../Binomial" begin -subsection {* Main definitions *} +subsection {* Fibonacci numbers *} fun fib :: "nat \ nat" where @@ -23,7 +23,7 @@ | fib1: "fib (Suc 0) = 1" | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n" -subsection {* Fibonacci numbers *} +subsection {* Basic Properties *} lemma fib_1 [simp]: "fib (1::nat) = 1" by (metis One_nat_def fib1) @@ -41,6 +41,8 @@ lemma fib_neq_0_nat: "n > 0 \ fib n > 0" by (induct n rule: fib.induct) (auto simp add: ) +subsection {* A Few Elementary Results *} + text {* \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is much easier using integers, not natural numbers! @@ -55,7 +57,7 @@ using fib_Cassini_int [of n] by auto -text {* \medskip Toward Law 6.111 of Concrete Mathematics *} +subsection {* Law 6.111 of Concrete Mathematics *} lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))" apply (induct n rule: fib.induct) @@ -67,9 +69,7 @@ apply (simp add: gcd_commute_nat [of "fib m"]) apply (cases m) apply (auto simp add: fib_add) - apply (subst gcd_commute_nat) - apply (subst mult.commute) - apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute) + apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute) done lemma gcd_fib_diff: "m \ n \ @@ -109,5 +109,35 @@ "fib (Suc n) * fib n = (\k \ {..n}. fib k * fib k)" by (induct n rule: nat.induct) (auto simp add: field_simps) +subsection {* Fibonacci and Binomial Coefficients *} + +lemma setsum_drop_zero: "(\k = 0..Suc n. if 0j = 0..n. f j)" + by (induct n) auto + +lemma setsum_choose_drop_zero: + "(\k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\j = 0..n. (n-j) choose j)" + by (rule trans [OF setsum.cong setsum_drop_zero]) auto + +lemma ne_diagonal_fib: + "(\k = 0..n. (n-k) choose k) = fib (Suc n)" +proof (induct n rule: fib.induct) + case 1 show ?case by simp +next + case 2 show ?case by simp +next + case (3 n) + have "(\k = 0..Suc n. Suc (Suc n) - k choose k) = + (\k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))" + by (rule setsum.cong) (simp_all add: choose_reduce_nat) + also have "... = (\k = 0..Suc n. Suc n - k choose k) + + (\k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))" + by (simp add: setsum.distrib) + also have "... = (\k = 0..Suc n. Suc n - k choose k) + + (\j = 0..n. n - j choose j)" + by (metis setsum_choose_drop_zero) + finally show ?case using 3 + by simp +qed + end diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Power.thy Mon May 25 22:11:43 2015 +0200 @@ -131,9 +131,25 @@ end +text{*Extract constant factors from powers*} declare power_mult_distrib [where a = "numeral w" for w, simp] declare power_mult_distrib [where b = "numeral w" for w, simp] +lemma power_add_numeral [simp]: + fixes a :: "'a :: monoid_mult" + shows "a^numeral m * a^numeral n = a^numeral (m + n)" + by (simp add: power_add [symmetric]) + +lemma power_add_numeral2 [simp]: + fixes a :: "'a :: monoid_mult" + shows "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b" + by (simp add: mult.assoc [symmetric]) + +lemma power_mult_numeral [simp]: + fixes a :: "'a :: monoid_mult" + shows"(a^numeral m)^numeral n = a^numeral (m * n)" + by (simp only: numeral_mult power_mult) + context semiring_numeral begin diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Predicate.thy Mon May 25 22:11:43 2015 +0200 @@ -215,50 +215,57 @@ by (auto simp add: is_empty_def) definition singleton :: "(unit \ 'a) \ 'a pred \ 'a" where - "singleton dfault A = (if \!x. eval A x then THE x. eval A x else dfault ())" + "\default. singleton default A = (if \!x. eval A x then THE x. eval A x else default ())" lemma singleton_eqI: - "\!x. eval A x \ eval A x \ singleton dfault A = x" + fixes default + shows "\!x. eval A x \ eval A x \ singleton default A = x" by (auto simp add: singleton_def) lemma eval_singletonI: - "\!x. eval A x \ eval A (singleton dfault A)" + fixes default + shows "\!x. eval A x \ eval A (singleton default A)" proof - assume assm: "\!x. eval A x" then obtain x where x: "eval A x" .. - with assm have "singleton dfault A = x" by (rule singleton_eqI) + with assm have "singleton default A = x" by (rule singleton_eqI) with x show ?thesis by simp qed lemma single_singleton: - "\!x. eval A x \ single (singleton dfault A) = A" + fixes default + shows "\!x. eval A x \ single (singleton default A) = A" proof - assume assm: "\!x. eval A x" - then have "eval A (singleton dfault A)" + then have "eval A (singleton default A)" by (rule eval_singletonI) - moreover from assm have "\x. eval A x \ singleton dfault A = x" + moreover from assm have "\x. eval A x \ singleton default A = x" by (rule singleton_eqI) - ultimately have "eval (single (singleton dfault A)) = eval A" + ultimately have "eval (single (singleton default A)) = eval A" by (simp (no_asm_use) add: single_def fun_eq_iff) blast - then have "\x. eval (single (singleton dfault A)) x = eval A x" + then have "\x. eval (single (singleton default A)) x = eval A x" by simp then show ?thesis by (rule pred_eqI) qed lemma singleton_undefinedI: - "\ (\!x. eval A x) \ singleton dfault A = dfault ()" + fixes default + shows "\ (\!x. eval A x) \ singleton default A = default ()" by (simp add: singleton_def) lemma singleton_bot: - "singleton dfault \ = dfault ()" + fixes default + shows "singleton default \ = default ()" by (auto simp add: bot_pred_def intro: singleton_undefinedI) lemma singleton_single: - "singleton dfault (single x) = x" + fixes default + shows "singleton default (single x) = x" by (auto simp add: intro: singleton_eqI singleI elim: singleE) lemma singleton_sup_single_single: - "singleton dfault (single x \ single y) = (if x = y then x else dfault ())" + fixes default + shows "singleton default (single x \ single y) = (if x = y then x else default ())" proof (cases "x = y") case True then show ?thesis by (simp add: singleton_single) next @@ -268,25 +275,27 @@ by (auto intro: supI1 supI2 singleI) with False have "\ (\!z. eval (single x \ single y) z)" by blast - then have "singleton dfault (single x \ single y) = dfault ()" + then have "singleton default (single x \ single y) = default ()" by (rule singleton_undefinedI) with False show ?thesis by simp qed lemma singleton_sup_aux: - "singleton dfault (A \ B) = (if A = \ then singleton dfault B - else if B = \ then singleton dfault A - else singleton dfault - (single (singleton dfault A) \ single (singleton dfault B)))" + fixes default + shows + "singleton default (A \ B) = (if A = \ then singleton default B + else if B = \ then singleton default A + else singleton default + (single (singleton default A) \ single (singleton default B)))" proof (cases "(\!x. eval A x) \ (\!y. eval B y)") case True then show ?thesis by (simp add: single_singleton) next case False from False have A_or_B: - "singleton dfault A = dfault () \ singleton dfault B = dfault ()" + "singleton default A = default () \ singleton default B = default ()" by (auto intro!: singleton_undefinedI) - then have rhs: "singleton dfault - (single (singleton dfault A) \ single (singleton dfault B)) = dfault ()" + then have rhs: "singleton default + (single (singleton default A) \ single (singleton default B)) = default ()" by (auto simp add: singleton_sup_single_single singleton_single) from False have not_unique: "\ (\!x. eval A x) \ \ (\!y. eval B y)" by simp @@ -296,7 +305,7 @@ by (blast elim: not_bot) with True not_unique have "\ (\!x. eval (A \ B) x)" by (auto simp add: sup_pred_def bot_pred_def) - then have "singleton dfault (A \ B) = dfault ()" by (rule singleton_undefinedI) + then have "singleton default (A \ B) = default ()" by (rule singleton_undefinedI) with True rhs show ?thesis by simp next case False then show ?thesis by auto @@ -304,10 +313,12 @@ qed lemma singleton_sup: - "singleton dfault (A \ B) = (if A = \ then singleton dfault B - else if B = \ then singleton dfault A - else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())" -using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single) + fixes default + shows + "singleton default (A \ B) = (if A = \ then singleton default B + else if B = \ then singleton default A + else if singleton default A = singleton default B then singleton default A else default ())" + using singleton_sup_aux [of default A B] by (simp only: singleton_sup_single_single) subsection {* Derived operations *} @@ -554,28 +565,34 @@ by (simp add: null_is_empty Seq_def) primrec the_only :: "(unit \ 'a) \ 'a seq \ 'a" where - [code del]: "the_only dfault Empty = dfault ()" -| "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())" -| "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P - else let x = singleton dfault P; y = the_only dfault xq in - if x = y then x else dfault ())" + [code del]: "\default. the_only default Empty = default ()" +| "\default. the_only default (Insert x P) = + (if is_empty P then x else let y = singleton default P in if x = y then x else default ())" +| "\default. the_only default (Join P xq) = + (if is_empty P then the_only default xq else if null xq then singleton default P + else let x = singleton default P; y = the_only default xq in + if x = y then x else default ())" lemma the_only_singleton: - "the_only dfault xq = singleton dfault (pred_of_seq xq)" + fixes default + shows "the_only default xq = singleton default (pred_of_seq xq)" by (induct xq) (auto simp add: singleton_bot singleton_single is_empty_def null_is_empty Let_def singleton_sup) lemma singleton_code [code]: - "singleton dfault (Seq f) = (case f () - of Empty \ dfault () + fixes default + shows + "singleton default (Seq f) = + (case f () of + Empty \ default () | Insert x P \ if is_empty P then x - else let y = singleton dfault P in - if x = y then x else dfault () - | Join P xq \ if is_empty P then the_only dfault xq - else if null xq then singleton dfault P - else let x = singleton dfault P; y = the_only dfault xq in - if x = y then x else dfault ())" + else let y = singleton default P in + if x = y then x else default () + | Join P xq \ if is_empty P then the_only default xq + else if null xq then singleton default P + else let x = singleton default P; y = the_only default xq in + if x = y then x else default ())" by (cases "f ()") (auto simp add: Seq_def the_only_singleton is_empty_def null_is_empty singleton_bot singleton_single singleton_sup Let_def) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Mon May 25 22:11:43 2015 +0200 @@ -409,7 +409,7 @@ lemma borel_measurable_lfp[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_linorder, linorder_topology, second_countable_topology})" - assumes "Order_Continuity.continuous F" + assumes "sup_continuous F" assumes *: "\f. f \ borel_measurable M \ F f \ borel_measurable M" shows "lfp F \ borel_measurable M" proof - @@ -420,13 +420,13 @@ also have "(\x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)" by auto also have "(SUP i. (F ^^ i) bot) = lfp F" - by (rule continuous_lfp[symmetric]) fact + by (rule sup_continuous_lfp[symmetric]) fact finally show ?thesis . qed lemma borel_measurable_gfp[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_linorder, linorder_topology, second_countable_topology})" - assumes "Order_Continuity.down_continuous F" + assumes "inf_continuous F" assumes *: "\f. f \ borel_measurable M \ F f \ borel_measurable M" shows "gfp F \ borel_measurable M" proof - @@ -437,7 +437,7 @@ also have "(\x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)" by auto also have "\ = gfp F" - by (rule down_continuous_gfp[symmetric]) fact + by (rule inf_continuous_gfp[symmetric]) fact finally show ?thesis . qed @@ -1345,7 +1345,7 @@ by (intro tendsto_infdist lim) show "\i. (\x. infdist (f i x) A) \ borel_measurable M" by (intro borel_measurable_continuous_on[where f="\x. infdist x A"] - continuous_at_imp_continuous_on ballI continuous_infdist isCont_ident) auto + continuous_at_imp_continuous_on ballI continuous_infdist continuous_ident) auto qed show "g -` A \ space M \ sets M" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Probability/Measurable.thy --- a/src/HOL/Probability/Measurable.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Probability/Measurable.thy Mon May 25 22:11:43 2015 +0200 @@ -7,8 +7,6 @@ "~~/src/HOL/Library/Order_Continuity" begin -hide_const (open) Order_Continuity.continuous - subsection {* Measurability prover *} lemma (in algebra) sets_Collect_finite_All: @@ -425,7 +423,7 @@ lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" assumes "P M" - assumes F: "Order_Continuity.continuous F" + assumes F: "sup_continuous F" assumes *: "\M A. P M \ (\N. P N \ A \ measurable N (count_space UNIV)) \ F A \ measurable M (count_space UNIV)" shows "lfp F \ measurable M (count_space UNIV)" proof - @@ -434,13 +432,13 @@ then have "(\x. SUP i. (F ^^ i) bot x) \ measurable M (count_space UNIV)" by measurable also have "(\x. SUP i. (F ^^ i) bot x) = lfp F" - by (subst continuous_lfp) (auto intro: F) + by (subst sup_continuous_lfp) (auto intro: F) finally show ?thesis . qed lemma measurable_lfp: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" - assumes F: "Order_Continuity.continuous F" + assumes F: "sup_continuous F" assumes *: "\A. A \ measurable M (count_space UNIV) \ F A \ measurable M (count_space UNIV)" shows "lfp F \ measurable M (count_space UNIV)" by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *) @@ -448,7 +446,7 @@ lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" assumes "P M" - assumes F: "Order_Continuity.down_continuous F" + assumes F: "inf_continuous F" assumes *: "\M A. P M \ (\N. P N \ A \ measurable N (count_space UNIV)) \ F A \ measurable M (count_space UNIV)" shows "gfp F \ measurable M (count_space UNIV)" proof - @@ -457,13 +455,13 @@ then have "(\x. INF i. (F ^^ i) top x) \ measurable M (count_space UNIV)" by measurable also have "(\x. INF i. (F ^^ i) top x) = gfp F" - by (subst down_continuous_gfp) (auto intro: F) + by (subst inf_continuous_gfp) (auto intro: F) finally show ?thesis . qed lemma measurable_gfp: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" - assumes F: "Order_Continuity.down_continuous F" + assumes F: "inf_continuous F" assumes *: "\A. A \ measurable M (count_space UNIV) \ F A \ measurable M (count_space UNIV)" shows "gfp F \ measurable M (count_space UNIV)" by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *) @@ -471,7 +469,7 @@ lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]: fixes F :: "('a \ 'c \ 'b) \ ('a \ 'c \ 'b::{complete_lattice, countable})" assumes "P M s" - assumes F: "Order_Continuity.continuous F" + assumes F: "sup_continuous F" assumes *: "\M A s. P M s \ (\N t. P N t \ A t \ measurable N (count_space UNIV)) \ F A s \ measurable M (count_space UNIV)" shows "lfp F s \ measurable M (count_space UNIV)" proof - @@ -480,14 +478,14 @@ then have "(\x. SUP i. (F ^^ i) bot s x) \ measurable M (count_space UNIV)" by measurable also have "(\x. SUP i. (F ^^ i) bot s x) = lfp F s" - by (subst continuous_lfp) (auto simp: F) + by (subst sup_continuous_lfp) (auto simp: F) finally show ?thesis . qed lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]: fixes F :: "('a \ 'c \ 'b) \ ('a \ 'c \ 'b::{complete_lattice, countable})" assumes "P M s" - assumes F: "Order_Continuity.down_continuous F" + assumes F: "inf_continuous F" assumes *: "\M A s. P M s \ (\N t. P N t \ A t \ measurable N (count_space UNIV)) \ F A s \ measurable M (count_space UNIV)" shows "gfp F s \ measurable M (count_space UNIV)" proof - @@ -496,7 +494,7 @@ then have "(\x. INF i. (F ^^ i) top s x) \ measurable M (count_space UNIV)" by measurable also have "(\x. INF i. (F ^^ i) top s x) = gfp F s" - by (subst down_continuous_gfp) (auto simp: F) + by (subst inf_continuous_gfp) (auto simp: F) finally show ?thesis . qed diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Mon May 25 22:11:43 2015 +0200 @@ -389,7 +389,7 @@ ultimately have "(\i. f' (\i. A i) - f' (A i)) ----> 0" by (simp add: zero_ereal_def) then have "(\i. f' (A i)) ----> f' (\i. A i)" - by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const]) + by (rule Lim_transform2[OF tendsto_const]) then show "(\i. f (A i)) ----> f (\i. A i)" using A by (subst (1 2) f') auto qed @@ -550,12 +550,12 @@ lemma emeasure_lfp[consumes 1, case_names cont measurable]: assumes "P M" - assumes cont: "Order_Continuity.continuous F" + assumes cont: "sup_continuous F" assumes *: "\M A. P M \ (\N. P N \ Measurable.pred N A) \ Measurable.pred M (F A)" shows "emeasure M {x\space M. lfp F x} = (SUP i. emeasure M {x\space M. (F ^^ i) (\x. False) x})" proof - have "emeasure M {x\space M. lfp F x} = emeasure M (\i. {x\space M. (F ^^ i) (\x. False) x})" - using continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure]) + using sup_continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure]) moreover { fix i from `P M` have "{x\space M. (F ^^ i) (\x. False) x} \ sets M" by (induct i arbitrary: M) (auto simp add: pred_def[symmetric] intro: *) } moreover have "incseq (\i. {x\space M. (F ^^ i) (\x. False) x})" @@ -565,7 +565,7 @@ proof (induct i) case 0 show ?case by (simp add: le_fun_def) next - case Suc thus ?case using monoD[OF continuous_mono[OF cont] Suc] by auto + case Suc thus ?case using monoD[OF sup_continuous_mono[OF cont] Suc] by auto qed then show "{x \ space M. (F ^^ i) (\x. False) x} \ {x \ space M. (F ^^ Suc i) (\x. False) x}" by auto @@ -1227,7 +1227,7 @@ lemma emeasure_lfp2[consumes 1, case_names cont f measurable]: assumes "P M" - assumes cont: "Order_Continuity.continuous F" + assumes cont: "sup_continuous F" assumes f: "\M. P M \ f \ measurable M' M" assumes *: "\M A. P M \ (\N. P N \ Measurable.pred N A) \ Measurable.pred M (F A)" shows "emeasure M' {x\space M'. lfp F (f x)} = (SUP i. emeasure M' {x\space M'. (F ^^ i) (\x. False) (f x)})" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon May 25 22:11:43 2015 +0200 @@ -838,6 +838,9 @@ "(\x. x \ space M \ u x \ v x) \ integral\<^sup>N M u \ integral\<^sup>N M v" by (auto intro: nn_integral_mono_AE) +lemma mono_nn_integral: "mono F \ mono (\x. integral\<^sup>N M (F x))" + by (auto simp add: mono_def le_fun_def intro!: nn_integral_mono) + lemma nn_integral_cong_AE: "AE x in M. u x = v x \ integral\<^sup>N M u = integral\<^sup>N M v" by (auto simp: eq_iff intro!: nn_integral_mono_AE) @@ -1081,6 +1084,9 @@ "0 \ c \ (\\<^sup>+ x. c \M) = c * (emeasure M) (space M)" by (subst nn_integral_eq_simple_integral) auto +lemma nn_integral_const_nonpos: "c \ 0 \ nn_integral M (\x. c) = 0" + using nn_integral_max_0[of M "\x. c"] by (simp add: max_def split: split_if_asm) + lemma nn_integral_linear: assumes f: "f \ borel_measurable M" "\x. 0 \ f x" and "0 \ a" and g: "g \ borel_measurable M" "\x. 0 \ g x" @@ -1482,6 +1488,89 @@ by (intro Liminf_eq_Limsup) auto qed +lemma nn_integral_monotone_convergence_INF': + assumes f: "decseq f" and [measurable]: "\i. f i \ borel_measurable M" + assumes "(\\<^sup>+ x. f 0 x \M) < \" and nn: "\x i. 0 \ f i x" + shows "(\\<^sup>+ x. (INF i. f i x) \M) = (INF i. integral\<^sup>N M (f i))" +proof (rule LIMSEQ_unique) + show "(\i. integral\<^sup>N M (f i)) ----> (INF i. integral\<^sup>N M (f i))" + using f by (intro LIMSEQ_INF) (auto intro!: nn_integral_mono simp: decseq_def le_fun_def) + show "(\i. integral\<^sup>N M (f i)) ----> \\<^sup>+ x. (INF i. f i x) \M" + proof (rule nn_integral_dominated_convergence) + show "(\\<^sup>+ x. f 0 x \M) < \" "\i. f i \ borel_measurable M" "f 0 \ borel_measurable M" + by fact+ + show "\j. AE x in M. 0 \ f j x" + using nn by auto + show "\j. AE x in M. f j x \ f 0 x" + using f by (auto simp: decseq_def le_fun_def) + show "AE x in M. (\i. f i x) ----> (INF i. f i x)" + using f by (auto intro!: LIMSEQ_INF simp: decseq_def le_fun_def) + show "(\x. INF i. f i x) \ borel_measurable M" + by auto + qed +qed + +lemma nn_integral_monotone_convergence_INF: + assumes f: "decseq f" and [measurable]: "\i. f i \ borel_measurable M" + assumes fin: "(\\<^sup>+ x. f i x \M) < \" + shows "(\\<^sup>+ x. (INF i. f i x) \M) = (INF i. integral\<^sup>N M (f i))" +proof - + { fix f :: "nat \ ereal" and j assume "decseq f" + then have "(INF i. f i) = (INF i. f (i + j))" + apply (intro INF_eq) + apply (rule_tac x="i" in bexI) + apply (auto simp: decseq_def le_fun_def) + done } + note INF_shift = this + + have dec: "\f::nat \ 'a \ ereal. decseq f \ decseq (\j x. max 0 (f (j + i) x))" + by (intro antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def) + + have "(\\<^sup>+ x. max 0 (INF i. f i x) \M) = (\\<^sup>+ x. (INF i. max 0 (f i x)) \M)" + by (intro nn_integral_cong) + (simp add: sup_ereal_def[symmetric] sup_INF del: sup_ereal_def) + also have "\ = (\\<^sup>+ x. (INF j. max 0 (f (j + i) x)) \M)" + using f by (intro nn_integral_cong INF_shift antimonoI le_funI max.mono) + (auto simp: decseq_def le_fun_def) + also have "\ = (INF j. (\\<^sup>+ x. max 0 (f (j + i) x) \M))" + proof (rule nn_integral_monotone_convergence_INF') + show "\j. (\x. max 0 (f (j + i) x)) \ borel_measurable M" + by measurable + show "(\\<^sup>+ x. max 0 (f (0 + i) x) \M) < \" + using fin by (simp add: nn_integral_max_0) + qed (intro max.cobounded1 dec f)+ + also have "\ = (INF j. (\\<^sup>+ x. max 0 (f j x) \M))" + using f by (intro INF_shift[symmetric] nn_integral_mono antimonoI le_funI max.mono) + (auto simp: decseq_def le_fun_def) + finally show ?thesis unfolding nn_integral_max_0 . +qed + +lemma sup_continuous_nn_integral: + assumes f: "\y. sup_continuous (f y)" + assumes [measurable]: "\F x. (\y. f y F x) \ borel_measurable (M x)" + shows "sup_continuous (\F x. (\\<^sup>+y. f y F x \M x))" + unfolding sup_continuous_def +proof safe + fix C :: "nat \ 'b \ ereal" assume C: "incseq C" + then show "(\x. \\<^sup>+ y. f y (SUPREMUM UNIV C) x \M x) = (SUP i. (\x. \\<^sup>+ y. f y (C i) x \M x))" + using sup_continuous_mono[OF f] + by (simp add: sup_continuousD[OF f C] fun_eq_iff nn_integral_monotone_convergence_SUP mono_def le_fun_def) +qed + +lemma inf_continuous_nn_integral: + assumes f: "\y. inf_continuous (f y)" + assumes [measurable]: "\F x. (\y. f y F x) \ borel_measurable (M x)" + assumes bnd: "\x F. (\\<^sup>+ y. f y F x \M x) \ \" + shows "inf_continuous (\F x. (\\<^sup>+y. f y F x \M x))" + unfolding inf_continuous_def +proof safe + fix C :: "nat \ 'b \ ereal" assume C: "decseq C" + then show "(\x. \\<^sup>+ y. f y (INFIMUM UNIV C) x \M x) = (INF i. (\x. \\<^sup>+ y. f y (C i) x \M x))" + using inf_continuous_mono[OF f] + by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def bnd + intro!: nn_integral_monotone_convergence_INF) +qed + lemma nn_integral_null_set: assumes "N \ null_sets M" shows "(\\<^sup>+ x. u x * indicator N x \M) = 0" proof - @@ -1649,6 +1738,124 @@ by (simp add: F_def) qed +lemma nn_integral_lfp: + assumes sets: "\s. sets (M s) = sets N" + assumes f: "sup_continuous f" + assumes meas: "\F. F \ borel_measurable N \ f F \ borel_measurable N" + assumes nonneg: "\F s. 0 \ g F s" + assumes g: "sup_continuous g" + assumes step: "\F s. F \ borel_measurable N \ integral\<^sup>N (M s) (f F) = g (\s. integral\<^sup>N (M s) F) s" + shows "(\\<^sup>+\. lfp f \ \M s) = lfp g s" +proof (rule antisym) + show "lfp g s \ (\\<^sup>+\. lfp f \ \M s)" + proof (induction arbitrary: s rule: lfp_ordinal_induct[OF sup_continuous_mono[OF g]]) + case (1 F) then show ?case + apply (subst lfp_unfold[OF sup_continuous_mono[OF f]]) + apply (subst step) + apply (rule borel_measurable_lfp[OF f]) + apply (rule meas) + apply assumption+ + apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD]) + apply (simp add: le_fun_def) + done + qed (auto intro: SUP_least) + + have lfp_nonneg: "\s. 0 \ lfp g s" + by (subst lfp_unfold[OF sup_continuous_mono[OF g]]) (rule nonneg) + + { fix i have "((f ^^ i) bot) \ borel_measurable N" + by (induction i) (simp_all add: meas) } + + have "(\\<^sup>+\. lfp f \ \M s) = (\\<^sup>+\. (SUP i. (f ^^ i) bot \) \M s)" + by (simp add: sup_continuous_lfp f) + also have "\ = (SUP i. \\<^sup>+\. (f ^^ i) bot \ \M s)" + proof (rule nn_integral_monotone_convergence_SUP) + show "incseq (\i. (f ^^ i) bot)" + using f[THEN sup_continuous_mono] by (rule mono_funpow) + show "\i. ((f ^^ i) bot) \ borel_measurable (M s)" + unfolding measurable_cong_sets[OF sets refl] by fact + qed + also have "\ \ lfp g s" + proof (rule SUP_least) + fix i show "integral\<^sup>N (M s) ((f ^^ i) bot) \ lfp g s" + proof (induction i arbitrary: s) + case 0 then show ?case + by (simp add: nn_integral_const_nonpos lfp_nonneg) + next + case (Suc n) + show ?case + apply (simp del: bot_apply) + apply (subst step) + apply fact + apply (subst lfp_unfold[OF sup_continuous_mono[OF g]]) + apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD]) + apply (rule le_funI) + apply (rule Suc) + done + qed + qed + finally show "(\\<^sup>+\. lfp f \ \M s) \ lfp g s" . +qed + +lemma nn_integral_gfp: + assumes sets: "\s. sets (M s) = sets N" + assumes f: "inf_continuous f" + assumes meas: "\F. F \ borel_measurable N \ f F \ borel_measurable N" + assumes bound: "\F s. (\\<^sup>+x. f F x \M s) < \" + assumes non_zero: "\s. emeasure (M s) (space (M s)) \ 0" + assumes g: "inf_continuous g" + assumes step: "\F s. F \ borel_measurable N \ integral\<^sup>N (M s) (f F) = g (\s. integral\<^sup>N (M s) F) s" + shows "(\\<^sup>+\. gfp f \ \M s) = gfp g s" +proof (rule antisym) + show "(\\<^sup>+\. gfp f \ \M s) \ gfp g s" + proof (induction arbitrary: s rule: gfp_ordinal_induct[OF inf_continuous_mono[OF g]]) + case (1 F) then show ?case + apply (subst gfp_unfold[OF inf_continuous_mono[OF f]]) + apply (subst step) + apply (rule borel_measurable_gfp[OF f]) + apply (rule meas) + apply assumption+ + apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD]) + apply (simp add: le_fun_def) + done + qed (auto intro: INF_greatest) + + { fix i have "((f ^^ i) top) \ borel_measurable N" + by (induction i) (simp_all add: meas) } + + have "(\\<^sup>+\. gfp f \ \M s) = (\\<^sup>+\. (INF i. (f ^^ i) top \) \M s)" + by (simp add: inf_continuous_gfp f) + also have "\ = (INF i. \\<^sup>+\. (f ^^ i) top \ \M s)" + proof (rule nn_integral_monotone_convergence_INF) + show "decseq (\i. (f ^^ i) top)" + using f[THEN inf_continuous_mono] by (rule antimono_funpow) + show "\i. ((f ^^ i) top) \ borel_measurable (M s)" + unfolding measurable_cong_sets[OF sets refl] by fact + show "integral\<^sup>N (M s) ((f ^^ 1) top) < \" + using bound[of s top] by simp + qed + also have "\ \ gfp g s" + proof (rule INF_greatest) + fix i show "gfp g s \ integral\<^sup>N (M s) ((f ^^ i) top)" + proof (induction i arbitrary: s) + case 0 with non_zero[of s] show ?case + by (simp add: top_ereal_def less_le emeasure_nonneg) + next + case (Suc n) + show ?case + apply (simp del: top_apply) + apply (subst step) + apply fact + apply (subst gfp_unfold[OF inf_continuous_mono[OF g]]) + apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD]) + apply (rule le_funI) + apply (rule Suc) + done + qed + qed + finally show "gfp g s \ (\\<^sup>+\. gfp f \ \M s)" . +qed + subsection {* Integral under concrete measures *} lemma nn_integral_empty: diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Probability/Stream_Space.thy --- a/src/HOL/Probability/Stream_Space.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Probability/Stream_Space.thy Mon May 25 22:11:43 2015 +0200 @@ -117,18 +117,18 @@ lemma measurable_alw[measurable]: "Measurable.pred (stream_space M) P \ Measurable.pred (stream_space M) (alw P)" unfolding alw_def - by (coinduction rule: measurable_gfp_coinduct) (auto simp: Order_Continuity.down_continuous_def) + by (coinduction rule: measurable_gfp_coinduct) (auto simp: inf_continuous_def) lemma measurable_ev[measurable]: "Measurable.pred (stream_space M) P \ Measurable.pred (stream_space M) (ev P)" unfolding ev_def - by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def) + by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def) lemma measurable_until: assumes [measurable]: "Measurable.pred (stream_space M) \" "Measurable.pred (stream_space M) \" shows "Measurable.pred (stream_space M) (\ until \)" unfolding UNTIL_def - by (coinduction rule: measurable_gfp_coinduct) (simp_all add: down_continuous_def fun_eq_iff) + by (coinduction rule: measurable_gfp_coinduct) (simp_all add: inf_continuous_def fun_eq_iff) lemma measurable_holds [measurable]: "Measurable.pred M P \ Measurable.pred (stream_space M) (holds P)" unfolding holds.simps[abs_def] @@ -144,7 +144,7 @@ lemma measurable_suntil[measurable]: assumes [measurable]: "Measurable.pred (stream_space M) Q" "Measurable.pred (stream_space M) P" shows "Measurable.pred (stream_space M) (Q suntil P)" - unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def) + unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def) lemma measurable_szip: "(\(\1, \2). szip \1 \2) \ measurable (stream_space M \\<^sub>M stream_space N) (stream_space (M \\<^sub>M N))" @@ -263,7 +263,7 @@ also have "\ \ sets (stream_space M)" apply (intro predE) apply (coinduction rule: measurable_gfp_coinduct) - apply (auto simp: down_continuous_def) + apply (auto simp: inf_continuous_def) done finally show ?thesis . qed diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Proofs/Lambda/WeakNorm.thy --- a/src/HOL/Proofs/Lambda/WeakNorm.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Mon May 25 22:11:43 2015 +0200 @@ -173,7 +173,7 @@ next assume neq: "x \ i" from App have "listall ?R ts" by (iprover dest: listall_conj2) - with TrueI TrueI uNF uT argsT + with uNF uT argsT have "\ts'. \j. Var j \\ map (\t. t[u/i]) ts \\<^sub>\\<^sup>* Var j \\ ts' \ NF (Var j \\ ts')" (is "\ts'. ?ex ts'") by (rule norm_list [of "\t. t", simplified]) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Mon May 25 22:11:43 2015 +0200 @@ -57,9 +57,9 @@ text {* Some fairly large proof: *} ML_val {* - val xml = export_proof @{thm Int.times_int.abs_eq}; + val xml = export_proof @{thm abs_less_iff}; val thm = import_proof thy1 xml; - @{assert} (size (YXML.string_of_body xml) > 50000000); + @{assert} (size (YXML.string_of_body xml) > 1000000); *} end diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Real.thy --- a/src/HOL/Real.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Real.thy Mon May 25 22:11:43 2015 +0200 @@ -757,10 +757,7 @@ "of_nat n < (2::'a::linordered_idom) ^ n" apply (induct n) apply simp -apply (subgoal_tac "(1::'a) \ 2 ^ n") -apply (drule (1) add_le_less_mono, simp) -apply simp -done +by (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc) lemma complete_real: fixes S :: "real set" @@ -807,7 +804,7 @@ have width: "\n. B n - A n = (b - a) / 2^n" apply (simp add: eq_divide_eq) apply (induct_tac n, simp) - apply (simp add: C_def avg_def algebra_simps) + apply (simp add: C_def avg_def power_Suc algebra_simps) done have twos: "\y r :: rat. 0 < r \ \n. y / 2 ^ n < r" @@ -1518,12 +1515,7 @@ by simp lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" -apply (induct "n") -apply (auto simp add: real_of_nat_Suc) -apply (subst mult_2) -apply (erule add_less_le_mono) -apply (rule two_realpow_ge_one) -done + by (simp add: of_nat_less_two_power real_of_nat_def) text {* TODO: no longer real-specific; rename and move elsewhere *} lemma realpow_Suc_le_self: @@ -1535,7 +1527,7 @@ lemma realpow_minus_mult: fixes x :: "'a::monoid_mult" shows "0 < n \ x ^ (n - 1) * x = x ^ n" -by (simp add: power_commutes split add: nat_diff_split) +by (simp add: power_Suc power_commutes split add: nat_diff_split) text {* FIXME: declare this [simp] for all types, or not at all *} lemma real_two_squares_add_zero_iff [simp]: diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Mon May 25 22:11:43 2015 +0200 @@ -316,10 +316,10 @@ lemma of_real_real_of_int_eq [simp]: "of_real (real z) = of_int z" by (simp add: real_of_int_def) -lemma of_real_numeral: "of_real (numeral w) = numeral w" +lemma of_real_numeral [simp]: "of_real (numeral w) = numeral w" using of_real_of_int_eq [of "numeral w"] by simp -lemma of_real_neg_numeral: "of_real (- numeral w) = - numeral w" +lemma of_real_neg_numeral [simp]: "of_real (- numeral w) = - numeral w" using of_real_of_int_eq [of "- numeral w"] by simp text{*Every real algebra has characteristic zero*} diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Series.thy --- a/src/HOL/Series.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Series.thy Mon May 25 22:11:43 2015 +0200 @@ -643,7 +643,7 @@ by (simp only: setsum_diff finite_S1 S2_le_S1) with 1 have "(\n. setsum ?g (?S2 n)) ----> (\k. a k) * (\k. b k)" - by (rule LIMSEQ_diff_approach_zero2) + by (rule Lim_transform2) thus ?thesis by (simp only: sums_def setsum_triangle_reindex) qed diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Set.thy --- a/src/HOL/Set.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Set.thy Mon May 25 22:11:43 2015 +0200 @@ -1623,6 +1623,9 @@ lemma Pow_empty [simp]: "Pow {} = {{}}" by (auto simp add: Pow_def) +lemma Pow_singleton_iff [simp]: "Pow X = {Y} \ X = {} \ Y = {}" +by blast + lemma Pow_insert: "Pow (insert a A) = Pow A \ (insert a ` Pow A)" by (blast intro: image_eqI [where ?x = "u - {a}" for u]) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Set_Interval.thy Mon May 25 22:11:43 2015 +0200 @@ -1298,7 +1298,14 @@ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}" by auto -lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two +lemma ivl_disj_un_two_touch: + "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. {l..m} Un {m.. {l<..m} Un {m..u} = {l<..u}" + "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}" +by auto + +lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch subsubsection {* Disjoint Intersections *} @@ -1498,6 +1505,23 @@ apply (simp_all add: setsum_add_nat_ivl add.commute atLeast0LessThan[symmetric]) done +lemma setsum_triangle_reindex: + fixes n :: nat + shows "(\(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))" + apply (simp add: setsum.Sigma) + apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"]) + apply auto + done + +lemma setsum_triangle_reindex_eq: + fixes n :: nat + shows "(\(i,j)\{(i,j). i+j \ n}. f i j) = (\k\n. \i\k. f i (k - i))" +using setsum_triangle_reindex [of f "Suc n"] +by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost) + +lemma nat_diff_setsum_reindex: "(\ii 0" by simp_all moreover have "(\i 0`) + by (induct n) (simp_all add: power_Suc field_simps `y \ 0`) ultimately show ?thesis by simp qed +lemma diff_power_eq_setsum: + fixes y :: "'a::{comm_ring,monoid_mult}" + shows + "x ^ (Suc n) - y ^ (Suc n) = + (x - y) * (\ppppi 0 \ x^n - 1 = (x - 1) * (\i 0 \ 1 - x^n = (1 - x) * (\i 0 \ 1 - x^n = (1 - x) * (\ix. Q x \ P x \ (\xxxii 'a val strong_co_induct_of: 'a list -> 'a diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Tools/simpdata.ML Mon May 25 22:11:43 2015 +0200 @@ -115,13 +115,8 @@ fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt); -val simp_legacy_precond = - Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false) - fun unsafe_solver_tac ctxt = let - val intros = - if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}] val sol_thms = reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt; fun sol_tac i = @@ -129,7 +124,8 @@ [resolve_tac ctxt sol_thms i, assume_tac ctxt i, eresolve_tac ctxt @{thms FalseE} i] ORELSE - (match_tac ctxt intros THEN_ALL_NEW sol_tac) i + (match_tac ctxt [@{thm conjI}] + THEN_ALL_NEW sol_tac) i in (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac end; diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Topological_Spaces.thy Mon May 25 22:11:43 2015 +0200 @@ -356,6 +356,10 @@ lemma nhds_neq_bot [simp]: "nhds a \ bot" unfolding trivial_limit_def eventually_nhds by simp +lemma (in t1_space) t1_space_nhds: + "x \ y \ (\\<^sub>F x in nhds x. x \ y)" + by (drule t1_space) (auto simp: eventually_nhds) + lemma at_within_eq: "at x within s = (INF S:{S. open S \ x \ S}. principal (S \ s - {x}))" unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib) @@ -1231,7 +1235,7 @@ using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 .. lemma sequentially_imp_eventually_at_left: - fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}" + fixes a :: "'a :: {linorder_topology, first_countable_topology}" assumes b[simp]: "b < a" assumes *: "\f. (\n. b < f n) \ (\n. f n < a) \ incseq f \ f ----> a \ eventually (\n. P (f n)) sequentially" shows "eventually P (at_left a)" @@ -1261,7 +1265,7 @@ qed lemma tendsto_at_left_sequentially: - fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}" + fixes a :: "_ :: {linorder_topology, first_countable_topology}" assumes "b < a" assumes *: "\S. (\n. S n < a) \ (\n. b < S n) \ incseq S \ S ----> a \ (\n. X (S n)) ----> L" shows "(X ---> L) (at_left a)" @@ -1269,7 +1273,7 @@ by (simp add: sequentially_imp_eventually_at_left) lemma sequentially_imp_eventually_at_right: - fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}" + fixes a :: "'a :: {linorder_topology, first_countable_topology}" assumes b[simp]: "a < b" assumes *: "\f. (\n. a < f n) \ (\n. f n < b) \ decseq f \ f ----> a \ eventually (\n. P (f n)) sequentially" shows "eventually P (at_right a)" @@ -1299,7 +1303,7 @@ qed lemma tendsto_at_right_sequentially: - fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}" + fixes a :: "_ :: {linorder_topology, first_countable_topology}" assumes "a < b" assumes *: "\S. (\n. a < S n) \ (\n. S n < b) \ decseq S \ S ----> a \ (\n. X (S n)) ----> L" shows "(X ---> L) (at_right a)" @@ -1479,14 +1483,6 @@ lemma continuous_at_imp_continuous_on: "\x\s. isCont f x \ continuous_on s f" by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within) -lemma isContI_continuous: "continuous (at x within UNIV) f \ isCont f x" - by simp - -lemma isCont_ident[continuous_intros, simp]: "isCont (\x. x) a" - using continuous_ident by (rule isContI_continuous) - -lemmas isCont_const = continuous_const - lemma isCont_o2: "isCont f a \ isCont g (f a) \ isCont (\x. g (f x)) a" unfolding isCont_def by (rule tendsto_compose) diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Transcendental.thy Mon May 25 22:11:43 2015 +0200 @@ -10,6 +10,12 @@ imports Binomial Series Deriv NthRoot begin +lemma reals_Archimedean4: + assumes "0 < y" "0 \ x" + obtains n where "real n * y \ x" "x < real (Suc n) * y" + using floor_correct [of "x/y"] assms + by (auto simp: Real.real_of_nat_Suc field_simps intro: that [of "nat (floor (x/y))"]) + lemma of_real_fact [simp]: "of_real (fact n) = fact n" by (metis of_nat_fact of_real_of_nat_eq) @@ -47,64 +53,22 @@ subsection {* Properties of Power Series *} -lemma lemma_realpow_diff: - fixes y :: "'a::monoid_mult" - shows "p \ n \ y ^ (Suc n - p) = (y ^ (n - p)) * y" +lemma powser_zero: + fixes f :: "nat \ 'a::real_normed_algebra_1" + shows "(\n. f n * 0 ^ n) = f 0" proof - - assume "p \ n" - hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le) - thus ?thesis by (simp add: power_commutes) + have "(\n<1. f n * 0 ^ n) = (\n. f n * 0 ^ n)" + by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) + thus ?thesis unfolding One_nat_def by simp qed -lemma lemma_realpow_diff_sumr2: - fixes y :: "'a::{comm_ring,monoid_mult}" - shows - "x ^ (Suc n) - y ^ (Suc n) = - (x - y) * (\p 'a::real_normed_div_algebra" + shows "(\n. a n * 0^n) sums a 0" + using sums_finite [of "{0}" "\n. a n * 0 ^ n"] by simp - also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)" - by (simp add: algebra_simps) - also have "... = y * ((x - y) * (\pppipp 0 \ x^n - 1 = (x - 1) * (\i 0 \ 1 - x^n = (1 - x) * (\i 0 \ 1 - x^n = (1 - x) * (\iz\ < \x\"}.*} lemma powser_insidea: @@ -167,6 +131,56 @@ summable (\n. f n * (z ^ n))" by (rule powser_insidea [THEN summable_norm_cancel]) +lemma powser_times_n_limit_0: + fixes x :: "'a::{real_normed_div_algebra,banach}" + assumes "norm x < 1" + shows "(\n. of_nat n * x ^ n) ----> 0" +proof - + have "norm x / (1 - norm x) \ 0" + using assms + by (auto simp: divide_simps) + moreover obtain N where N: "norm x / (1 - norm x) < of_int N" + using ex_le_of_int + by (meson ex_less_of_int) + ultimately have N0: "N>0" + by auto + then have *: "real (N + 1) * norm x / real N < 1" + using N assms + by (auto simp: field_simps) + { fix n::nat + assume "N \ int n" + then have "real N * real_of_nat (Suc n) \ real_of_nat n * real (1 + N)" + by (simp add: algebra_simps) + then have "(real N * real_of_nat (Suc n)) * (norm x * norm (x ^ n)) + \ (real_of_nat n * real (1 + N)) * (norm x * norm (x ^ n))" + using N0 mult_mono by fastforce + then have "real N * (norm x * (real_of_nat (Suc n) * norm (x ^ n))) + \ real_of_nat n * (norm x * (real (1 + N) * norm (x ^ n)))" + by (simp add: algebra_simps) + } note ** = this + show ?thesis using * + apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"]) + apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc ** + del: of_nat_Suc real_of_int_add) + done +qed + +corollary lim_n_over_pown: + fixes x :: "'a::{real_normed_field,banach}" + shows "1 < norm x \ ((\n. of_nat n / x^n) ---> 0) sequentially" +using powser_times_n_limit_0 [of "inverse x"] +by (simp add: norm_divide divide_simps) + +lemma lim_1_over_n: "((\n. 1 / of_nat n) ---> (0::'a\real_normed_field)) sequentially" + apply (clarsimp simp: lim_sequentially norm_divide dist_norm divide_simps) + apply (auto simp: mult_ac dest!: ex_less_of_nat_mult [of _ 1]) + by (metis le_eq_less_or_eq less_trans linordered_comm_semiring_strict_class.comm_mult_strict_left_mono + of_nat_less_0_iff of_nat_less_iff zero_less_mult_iff zero_less_one) + +lemma lim_inverse_n: "((\n. inverse(of_nat n)) ---> (0::'a\real_normed_field)) sequentially" + using lim_1_over_n + by (simp add: inverse_eq_divide) + lemma sum_split_even_odd: fixes f :: "nat \ real" shows @@ -462,6 +476,11 @@ "setsum f {..ipp 0" @@ -473,7 +492,7 @@ apply (simp add: right_diff_distrib diff_divide_distrib h) apply (simp add: mult.assoc [symmetric]) apply (cases "n", simp) - apply (simp add: lemma_realpow_diff_sumr2 h + apply (simp add: diff_power_eq_setsum h right_diff_distrib [symmetric] mult.assoc del: power_Suc setsum_lessThan_Suc of_nat_Suc) apply (subst lemma_realpow_rev_sumr) @@ -483,7 +502,7 @@ apply (rule setsum.cong [OF refl]) apply (simp add: less_iff_Suc_add) apply (clarify) - apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps + apply (simp add: setsum_right_distrib diff_power_eq_setsum ac_simps del: setsum_lessThan_Suc power_Suc) apply (subst mult.assoc [symmetric], subst power_add [symmetric]) apply (simp add: ac_simps) @@ -683,6 +702,132 @@ qed qed +subsection {* The Derivative of a Power Series Has the Same Radius of Convergence *} + +lemma termdiff_converges: + fixes x :: "'a::{real_normed_field,banach}" + assumes K: "norm x < K" + and sm: "\x. norm x < K \ summable(\n. c n * x ^ n)" + shows "summable (\n. diffs c n * x ^ n)" +proof (cases "x = 0") + case True then show ?thesis + using powser_sums_zero sums_summable by auto +next + case False + then have "K>0" + using K less_trans zero_less_norm_iff by blast + then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0" + using K False + by (auto simp: abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"]) + have "(\n. of_nat n * (x / of_real r) ^ n) ----> 0" + using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"]) + then obtain N where N: "\n. n\N \ real_of_nat n * norm x ^ n < r ^ n" + using r unfolding LIMSEQ_iff + apply (drule_tac x=1 in spec) + apply (auto simp: norm_divide norm_mult norm_power field_simps) + done + have "summable (\n. (of_nat n * c n) * x ^ n)" + apply (rule summable_comparison_test' [of "\n. norm(c n * (of_real r) ^ n)" N]) + apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]]) + using N r norm_of_real [of "r+K", where 'a = 'a] + apply (auto simp add: norm_divide norm_mult norm_power ) + using less_eq_real_def by fastforce + then have "summable (\n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)" + using summable_iff_shift [of "\n. of_nat n * c n * x ^ n" 1] + by simp + then have "summable (\n. (of_nat (Suc n) * c(Suc n)) * x ^ n)" + using False summable_mult2 [of "\n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"] + by (simp add: mult.assoc) (auto simp: power_Suc mult_ac) + then show ?thesis + by (simp add: diffs_def) +qed + +lemma termdiff_converges_all: + fixes x :: "'a::{real_normed_field,banach}" + assumes "\x. summable (\n. c n * x^n)" + shows "summable (\n. diffs c n * x^n)" + apply (rule termdiff_converges [where K = "1 + norm x"]) + using assms + apply (auto simp: ) + done + +lemma termdiffs_strong: + fixes K x :: "'a::{real_normed_field,banach}" + assumes sm: "summable (\n. c n * K ^ n)" + and K: "norm x < norm K" + shows "DERIV (\x. \n. c n * x^n) x :> (\n. diffs c n * x^n)" +proof - + have [simp]: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K" + using K + apply (auto simp: norm_divide) + apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"]) + apply (auto simp: mult_2_right norm_triangle_mono) + done + have "summable (\n. c n * (of_real (norm x + norm K) / 2) ^ n)" + apply (rule summable_norm_cancel [OF powser_insidea [OF sm]]) + using K + apply (auto simp: algebra_simps) + done + moreover have "\x. norm x < norm K \ summable (\n. diffs c n * x ^ n)" + by (blast intro: sm termdiff_converges powser_inside) + moreover have "\x. norm x < norm K \ summable (\n. diffs(diffs c) n * x ^ n)" + by (blast intro: sm termdiff_converges powser_inside) + ultimately show ?thesis + apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"]) + apply (auto simp: algebra_simps) + using K + apply (simp add: norm_divide) + apply (rule less_le_trans [of _ "of_real (norm K) + of_real (norm x)"]) + apply (simp_all add: of_real_add [symmetric] del: of_real_add) + done +qed + +lemma powser_limit_0: + fixes a :: "nat \ 'a::{real_normed_field,banach}" + assumes s: "0 < s" + and sm: "\x. norm x < s \ (\n. a n * x ^ n) sums (f x)" + shows "(f ---> a 0) (at 0)" +proof - + have "summable (\n. a n * (of_real s / 2) ^ n)" + apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm]) + using s + apply (auto simp: norm_divide) + done + then have "((\x. \n. a n * x ^ n) has_field_derivative (\n. diffs a n * 0 ^ n)) (at 0)" + apply (rule termdiffs_strong) + using s + apply (auto simp: norm_divide) + done + then have "isCont (\x. \n. a n * x ^ n) 0" + by (blast intro: DERIV_continuous) + then have "((\x. \n. a n * x ^ n) ---> a 0) (at 0)" + by (simp add: continuous_within powser_zero) + then show ?thesis + apply (rule Lim_transform) + apply (auto simp add: LIM_eq) + apply (rule_tac x="s" in exI) + using s + apply (auto simp: sm [THEN sums_unique]) + done +qed + +lemma powser_limit_0_strong: + fixes a :: "nat \ 'a::{real_normed_field,banach}" + assumes s: "0 < s" + and sm: "\x. x \ 0 \ norm x < s \ (\n. a n * x ^ n) sums (f x)" + shows "(f ---> a 0) (at 0)" +proof - + have *: "((\x. if x = 0 then a 0 else f x) ---> a 0) (at 0)" + apply (rule powser_limit_0 [OF s]) + apply (case_tac "x=0") + apply (auto simp add: powser_sums_zero sm) + done + show ?thesis + apply (subst LIM_equal [where g = "(\x. if x = 0 then a 0 else f x)"]) + apply (simp_all add: *) + done +qed + subsection {* Derivability of power series *} @@ -846,7 +991,7 @@ proof - have "\f n * x ^ (Suc n) - f n * y ^ (Suc n)\ = (\f n\ * \x-y\) * \\p" - unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult + unfolding right_diff_distrib[symmetric] diff_power_eq_setsum abs_mult by auto also have "\ \ (\f n\ * \x-y\) * (\real (Suc n)\ * \R' ^ n\)" proof (rule mult_left_mono) @@ -946,7 +1091,7 @@ obtain r :: real where r0: "0 < r" and r1: "r < 1" using dense [OF zero_less_one] by fast obtain N :: nat where N: "norm x < real N * r" - using reals_Archimedean3 [OF r0] by fast + using ex_less_of_nat_mult r0 real_of_nat_def by auto from r1 show ?thesis proof (rule summable_ratio_test [rule_format]) fix n :: nat @@ -1044,15 +1189,6 @@ subsubsection {* Properties of the Exponential Function *} -lemma powser_zero: - fixes f :: "nat \ 'a::{real_normed_algebra_1}" - shows "(\n. f n * 0 ^ n) = f 0" -proof - - have "(\n<1. f n * 0 ^ n) = (\n. f n * 0 ^ n)" - by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) - thus ?thesis unfolding One_nat_def by simp -qed - lemma exp_zero [simp]: "exp 0 = 1" unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) @@ -1156,7 +1292,10 @@ lemma exp_of_nat_mult: fixes x :: "'a::{real_normed_field,banach}" shows "exp(of_nat n * x) = exp(x) ^ n" - by (induct n) (auto simp add: distrib_left exp_add mult.commute) + by (induct n) (auto simp add: power_Suc distrib_left exp_add mult.commute) + +corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" + by (simp add: exp_of_nat_mult real_of_nat_def) lemma exp_setsum: "finite I \ exp(setsum f I) = setprod (\x. exp(f x)) I" by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute) @@ -1185,10 +1324,6 @@ lemma abs_exp_cancel [simp]: "\exp x::real\ = exp x" by simp -(*FIXME: superseded by exp_of_nat_mult*) -lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" - by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute) - text {* Strict monotonicity of exponential. *} lemma exp_ge_add_one_self_aux: @@ -1292,6 +1427,9 @@ -- {*exponentation via ln and exp*} where [code del]: "x powr a \ if x = 0 then 0 else exp(a * ln x)" +lemma powr_0 [simp]: "0 powr z = 0" + by (simp add: powr_def) + instantiation real :: ln begin @@ -1790,6 +1928,11 @@ fixes x::real shows "0 < x \ ln x \ x - 1" using exp_ge_add_one_self[of "ln x"] by simp +corollary ln_diff_le: + fixes x::real + shows "0 < x \ 0 < y \ ln x - ln y \ (x - y) / y" + by (simp add: ln_div [symmetric] diff_divide_distrib ln_le_minus_one) + lemma ln_eq_minus_one: fixes x::real assumes "0 < x" "ln x = x - 1" @@ -2164,10 +2307,7 @@ lemma powr_realpow: "0 < x ==> x powr (real n) = x^n" apply (induct n) apply simp - apply (subgoal_tac "real(Suc n) = real n + 1") - apply (erule ssubst) - apply (subst powr_add, simp, simp) - done + by (simp add: add.commute power.simps(2) powr_add real_of_nat_Suc) lemma powr_realpow_numeral: "0 < x \ x powr (numeral n :: real) = x ^ (numeral n)" unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow) @@ -2271,25 +2411,27 @@ using powr_mono by fastforce lemma powr_less_mono2: - fixes x::real shows "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a" + fixes x::real shows "0 < a ==> 0 \ x ==> x < y ==> x powr a < y powr a" by (simp add: powr_def) - lemma powr_less_mono2_neg: fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a" by (simp add: powr_def) lemma powr_mono2: - fixes x::real shows "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a" + fixes x::real shows "0 <= a ==> 0 \ x ==> x <= y ==> x powr a <= y powr a" apply (case_tac "a = 0", simp) apply (case_tac "x = y", simp) - apply (metis less_eq_real_def powr_less_mono2) + apply (metis dual_order.strict_iff_order powr_less_mono2) done lemma powr_inj: fixes x::real shows "0 < a \ a \ 1 \ a powr x = a powr y \ x = y" unfolding powr_def exp_inj_iff by simp +lemma powr_half_sqrt: "0 \ x \ x powr (1/2) = sqrt x" + by (simp add: powr_def root_powr_inverse sqrt_def) + lemma ln_powr_bound: fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a" by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute mult_imp_le_div_pos not_less powr_gt_zero) @@ -2315,28 +2457,15 @@ finally show ?thesis . qed -lemma tendsto_powr [tendsto_intros]: (*FIXME a mess, suggests a general rule about exceptions*) +lemma tendsto_powr [tendsto_intros]: fixes a::real - shows "\(f ---> a) F; (g ---> b) F; a \ 0\ \ ((\x. f x powr g x) ---> a powr b) F" - apply (simp add: powr_def) - apply (simp add: tendsto_def) - apply (simp add: eventually_conj_iff ) - apply safe - apply (case_tac "0 \ S") - apply (auto simp: ) - apply (subgoal_tac "\T. open T & a : T & 0 \ T") - apply clarify - apply (drule_tac x="T" in spec) - apply (simp add: ) - apply (metis (mono_tags, lifting) eventually_mono) - apply (simp add: separation_t1) - apply (subgoal_tac "((\x. exp (g x * ln (f x))) ---> exp (b * ln a)) F") - apply (simp add: tendsto_def) - apply (metis (mono_tags, lifting) eventually_mono) - apply (simp add: tendsto_def [symmetric]) - apply (intro tendsto_intros) - apply (auto simp: ) - done + assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \ 0" + shows "((\x. f x powr g x) ---> a powr b) F" + unfolding powr_def +proof (rule filterlim_If) + from f show "((\x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" + by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds) +qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1) lemma continuous_powr: assumes "continuous F f" @@ -2362,45 +2491,68 @@ shows "continuous_on s (\x. (f x) powr (g x))" using assms unfolding continuous_on_def by (fast intro: tendsto_powr) -(* FIXME: generalize by replacing d by with g x and g ---> d? *) +lemma tendsto_powr2: + fixes a::real + assumes f: "(f ---> a) F" and g: "(g ---> b) F" and f_nonneg: "\\<^sub>F x in F. 0 \ f x" and b: "0 < b" + shows "((\x. f x powr g x) ---> a powr b) F" + unfolding powr_def +proof (rule filterlim_If) + from f show "((\x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" + by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds) +next + { assume "a = 0" + with f f_nonneg have "LIM x inf F (principal {x. f x \ 0}). f x :> at_right 0" + by (auto simp add: filterlim_at eventually_inf_principal le_less + elim: eventually_elim1 intro: tendsto_mono inf_le1) + then have "((\x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \ 0}))" + by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0] + filterlim_tendsto_pos_mult_at_bot[OF _ `0 < b`] + intro: tendsto_mono inf_le1 g) } + then show "((\x. exp (g x * ln (f x))) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \ 0}))" + using f g by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1) +qed + +lemma DERIV_powr: + fixes r::real + assumes g: "DERIV g x :> m" and pos: "g x > 0" and f: "DERIV f x :> r" + shows "DERIV (\x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)" +proof - + have "DERIV (\x. exp (f x * ln (g x))) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)" + using pos + by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff) + then show ?thesis + proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated]) + from DERIV_isCont[OF g] pos have "\\<^sub>F x in at x. 0 < g x" + unfolding isCont_def by (rule order_tendstoD(1)) + with pos show "\\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x" + by (auto simp: eventually_at_filter powr_def elim: eventually_elim1) + qed +qed + +lemma DERIV_fun_powr: + fixes r::real + assumes g: "DERIV g x :> m" and pos: "g x > 0" + shows "DERIV (\x. (g x) powr r) x :> r * (g x) powr (r - of_nat 1) * m" + using DERIV_powr[OF g pos DERIV_const, of r] pos + by (simp add: powr_divide2[symmetric] field_simps) + lemma tendsto_zero_powrI: - assumes "eventually (\x. 0 < f x ) F" and "(f ---> (0::real)) F" - and "0 < d" - shows "((\x. f x powr d) ---> 0) F" -proof (rule tendstoI) - fix e :: real assume "0 < e" - def Z \ "e powr (1 / d)" - with `0 < e` have "0 < Z" by simp - with assms have "eventually (\x. 0 < f x \ dist (f x) 0 < Z) F" - by (intro eventually_conj tendstoD) - moreover - from assms have "\x. 0 < x \ dist x 0 < Z \ x powr d < Z powr d" - by (intro powr_less_mono2) (auto simp: dist_real_def) - with assms `0 < e` have "\x. 0 < x \ dist x 0 < Z \ dist (x powr d) 0 < e" - unfolding dist_real_def Z_def by (auto simp: powr_powr) - ultimately - show "eventually (\x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1) -qed + assumes "(f ---> (0::real)) F" "(g ---> b) F" "\\<^sub>F x in F. 0 \ f x" "0 < b" + shows "((\x. f x powr g x) ---> 0) F" + using tendsto_powr2[OF assms] by simp lemma tendsto_neg_powr: assumes "s < 0" - and "LIM x F. f x :> at_top" + and f: "LIM x F. f x :> at_top" shows "((\x. f x powr s) ---> (0::real)) F" -proof (rule tendstoI) - fix e :: real assume "0 < e" - def Z \ "e powr (1 / s)" - have "Z > 0" - using Z_def `0 < e` by auto - from assms have "eventually (\x. Z < f x) F" - by (simp add: filterlim_at_top_dense) - moreover - from assms have "\x::real. Z < x \ x powr s < Z powr s" - using `Z > 0` - by (auto simp: Z_def intro!: powr_less_mono2_neg) - with assms `0 < e` have "\x. Z < x \ dist (x powr s) 0 < e" - by (simp add: powr_powr Z_def dist_real_def) - ultimately - show "eventually (\x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1) +proof - + have "((\x. exp (s * ln (f x))) ---> (0::real)) F" (is "?X") + by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_top] + filterlim_tendsto_neg_mult_at_bot assms) + also have "?X \ ((\x. f x powr s) ---> (0::real)) F" + using f filterlim_at_top_dense[of f F] + by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_elim1) + finally show ?thesis . qed lemma tendsto_exp_limit_at_right: @@ -2957,7 +3109,7 @@ lemmas realpow_num_eq_if = power_eq_if -lemma sumr_pos_lt_pair: (*FIXME A MESS, BUT THE REAL MESS IS THE NEXT THEOREM*) +lemma sumr_pos_lt_pair: fixes f :: "nat \ real" shows "\summable f; \d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\ @@ -2967,11 +3119,7 @@ apply (drule_tac k=k in summable_ignore_initial_segment) apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp) apply simp -apply (frule sums_unique) -apply (drule sums_summable, simp) -apply (erule suminf_pos) -apply (simp add: ac_simps) -done +by (metis (no_types, lifting) add.commute suminf_pos summable_def sums_unique) lemma cos_two_less_zero [simp]: "cos 2 < (0::real)" @@ -2980,30 +3128,25 @@ from sums_minus [OF cos_paired] have *: "(\n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)" by simp - then have **: "summable (\n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))" + then have sm: "summable (\n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))" by (rule sums_summable) have "0 < (\nnn. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))" + < (\n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))" proof - { fix d - have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) - < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) * - fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))" + let ?six4d = "Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))" + have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))" unfolding real_of_nat_mult by (rule mult_strict_mono) (simp_all add: fact_less_mono) - then have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) - < (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))" - by (simp only: fact.simps(2) [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"] real_of_nat_def of_nat_mult of_nat_fact) - then have "(4::real) * inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))) - < inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))" + then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))" + by (simp only: fact.simps(2) [of "Suc (?six4d)"] real_of_nat_def of_nat_mult of_nat_fact) + then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))" by (simp add: inverse_eq_divide less_divide_eq) - } - note *** = this - have [simp]: "\x y::real. 0 < x - y \ y < x" by arith - from ** show ?thesis by (rule sumr_pos_lt_pair) - (simp add: divide_inverse mult.assoc [symmetric] ***) + } + then show ?thesis + by (force intro!: sumr_pos_lt_pair [OF sm] simp add: power_Suc divide_inverse algebra_simps) qed ultimately have "0 < (\n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))" by (rule order_less_trans) @@ -3349,22 +3492,18 @@ done qed -lemma reals_Archimedean4: - "\0 < y; 0 \ x\ \ \n. real n * y \ x & x < real (Suc n) * y" -apply (auto dest!: reals_Archimedean3) -apply (drule_tac x = x in spec, clarify) -apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y") - prefer 2 apply (erule LeastI) -apply (case_tac "LEAST m::nat. x < real m * y", simp) -apply (rename_tac m) -apply (subgoal_tac "~ x < real m * y") - prefer 2 apply (rule not_less_Least, simp, force) +lemma reals_Archimedean4': + "\0 < y; 0 \ x\ \ \n. real n * y \ x \ x < real (Suc n) * y" +apply (rule_tac x="nat (floor (x/y))" in exI) +using floor_correct [of "x/y"] +apply (auto simp: Real.real_of_nat_Suc field_simps) done lemma cos_zero_lemma: "\0 \ x; cos x = 0\ \ \n::nat. odd n & x = real n * (pi/2)" -apply (drule pi_gt_zero [THEN reals_Archimedean4], safe) +apply (erule reals_Archimedean4 [OF pi_gt_zero]) +apply (auto simp: ) apply (subgoal_tac "0 \ x - real n * pi & (x - real n * pi) \ pi & (cos (x - real n * pi) = 0) ") apply (auto simp: algebra_simps real_of_nat_Suc) @@ -4594,6 +4733,11 @@ using cos_gt_zero_pi [OF 1 2] by (simp add: arctan tan_add) qed +lemma arctan_double: + assumes "\x\ < 1" + shows "2 * arctan x = arctan ((2*x) / (1 - x\<^sup>2))" + by (metis assms arctan_add linear mult_2 not_less power2_eq_square) + theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)" proof - have "\1 / 5\ < (1 :: real)" by auto @@ -4611,6 +4755,35 @@ thus ?thesis unfolding arctan_one by algebra qed +lemma machin_Euler: "5 * arctan(1/7) + 2 * arctan(3/79) = pi/4" +proof - + have 17: "\1/7\ < (1 :: real)" by auto + with arctan_double + have "2 * arctan (1/7) = arctan (7/24)" by auto + moreover + have "\7/24\ < (1 :: real)" by auto + with arctan_double + have "2 * arctan (7/24) = arctan (336/527)" by auto + moreover + have "\336/527\ < (1 :: real)" by auto + from arctan_add[OF less_imp_le[OF 17] this] + have "arctan(1/7) + arctan (336/527) = arctan (2879/3353)" by auto + ultimately have I: "5 * arctan(1/7) = arctan (2879/3353)" by auto + have 379: "\3/79\ < (1 :: real)" by auto + with arctan_double + have II: "2 * arctan (3/79) = arctan (237/3116)" by auto + have *: "\2879/3353\ < (1 :: real)" by auto + have "\237/3116\ < (1 :: real)" by auto + from arctan_add[OF less_imp_le[OF *] this] + have "arctan (2879/3353) + arctan (237/3116) = pi/4" + by (simp add: arctan_one) + then show ?thesis using I II + by auto +qed + +(*But could also prove MACHIN_GAUSS: + 12 * arctan(1/18) + 8 * arctan(1/57) - 5 * arctan(1/239) = pi/4*) + subsection {* Introducing the inverse tangent power series *} @@ -4923,8 +5096,8 @@ hence "\ x \ { 0 <..< 1 }. 0 \ ?a x n - ?diff x n" by auto moreover have "\x. isCont (\ x. ?a x n - ?diff x n) x" unfolding diff_conv_add_uminus divide_inverse - by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan - isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum + by (auto intro!: isCont_add isCont_rabs continuous_ident isCont_minus isCont_arctan + isCont_inverse isCont_mult isCont_power continuous_const isCont_setsum simp del: add_uminus_conv_diff) ultimately have "0 \ ?a 1 n - ?diff 1 n" by (rule LIM_less_bound) @@ -5095,8 +5268,57 @@ qed -subsection{*Basics about polynomial functions: extremal behaviour and root counts*} -(*ALL COULD GO TO COMPLEX_MAIN OR EARLIER*) +subsection{*Basics about polynomial functions: products, extremal behaviour and root counts*} + +lemma pairs_le_eq_Sigma: + fixes m::nat + shows "{(i,j). i+j \ m} = Sigma (atMost m) (\r. atMost (m-r))" +by auto + +lemma setsum_up_index_split: + "(\k\m + n. f k) = (\k\m. f k) + (\k = Suc m..m + n. f k)" + by (metis atLeast0AtMost Suc_eq_plus1 le0 setsum_ub_add_nat) + +lemma Sigma_interval_disjoint: + fixes w :: "'a::order" + shows "(SIGMA i:A. {..v i}) \ (SIGMA i:A.{v i<..w}) = {}" + by auto + +lemma product_atMost_eq_Un: + fixes m :: nat + shows "A \ {..m} = (SIGMA i:A.{..m - i}) \ (SIGMA i:A.{m - i<..m})" + by auto + +lemma polynomial_product: (*with thanks to Chaitanya Mangla*) + fixes x:: "'a :: idom" + assumes m: "\i. i>m \ (a i) = 0" and n: "\j. j>n \ (b j) = 0" + shows "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = + (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" +proof - + have "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = (\i\m. \j\n. (a i * x ^ i) * (b j * x ^ j))" + by (rule setsum_product) + also have "... = (\i\m + n. \j\n + m. a i * x ^ i * (b j * x ^ j))" + using assms by (auto simp: setsum_up_index_split) + also have "... = (\r\m + n. \j\m + n - r. a r * x ^ r * (b j * x ^ j))" + apply (simp add: add_ac setsum.Sigma product_atMost_eq_Un) + apply (clarsimp simp add: setsum_Un Sigma_interval_disjoint intro!: setsum.neutral) + by (metis add_diff_assoc2 add.commute add_lessD1 leD m n nat_le_linear neqE) + also have "... = (\(i,j)\{(i,j). i+j \ m+n}. (a i * x ^ i) * (b j * x ^ j))" + by (auto simp: pairs_le_eq_Sigma setsum.Sigma) + also have "... = (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" + apply (subst setsum_triangle_reindex_eq) + apply (auto simp: algebra_simps setsum_right_distrib intro!: setsum.cong) + by (metis le_add_diff_inverse power_add) + finally show ?thesis . +qed + +lemma polynomial_product_nat: + fixes x:: nat + assumes m: "\i. i>m \ (a i) = 0" and n: "\j. j>n \ (b j) = 0" + shows "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = + (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" + using polynomial_product [of m a n b x] assms + by (simp add: Int.zpower_int Int.zmult_int Int.int_setsum [symmetric]) lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*) fixes x :: "'a::idom" @@ -5170,6 +5392,9 @@ using polyfun_linear_factor [of c n a] assms by auto +(*The material of this section, up until this point, could go into a new theory of polynomials + based on Main alone. The remaining material involves limits, continuity, series, etc.*) + lemma isCont_polynom: fixes c :: "nat \ 'a::real_normed_div_algebra" shows "isCont (\w. \i\n. c i * w^i) a" diff -r 82453d0f49ee -r ff82ba1893c8 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Mon May 25 12:04:43 2015 +0200 +++ b/src/HOL/Wellfounded.thy Mon May 25 22:11:43 2015 +0200 @@ -380,6 +380,35 @@ by (rule wf_union_merge [where S = "{}", simplified]) +subsection {* Well-Foundedness of Composition *} + +text{* Provided by Tjark Weber: *} + +lemma wf_relcomp_compatible: + assumes "wf R" and "R O S \ S O R" + shows "wf (S O R)" +proof (rule wfI_pf) + fix A assume A: "A \ (S O R) `` A" + { + fix n have "(S ^^ n) `` A \ R `` (S ^^ Suc n) `` A" + proof (induction n) + case 0 show ?case using A by (simp add: relcomp_Image) + next + case (Suc n) + then have "S `` (S ^^ n) `` A \ S `` R `` (S ^^ Suc n) `` A" + by (simp add: Image_mono) + also have "\ \ R `` S `` (S ^^ Suc n) `` A" using assms(2) + by (simp add: Image_mono O_assoc relcomp_Image[symmetric] relcomp_mono) + finally show ?case by (simp add: relcomp_Image) + qed + } + then have "(\n. (S ^^ n) `` A) \ R `` (\n. (S ^^ n) `` A)" by blast + then have "(\n. (S ^^ n) `` A) = {}" + using assms(1) by (simp only: wfE_pf) + then show "A = {}" using relpow.simps(1) by blast +qed + + subsection {* Acyclic relations *} lemma wf_acyclic: "wf r ==> acyclic r" diff -r 82453d0f49ee -r ff82ba1893c8 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Mon May 25 12:04:43 2015 +0200 +++ b/src/Pure/raw_simplifier.ML Mon May 25 22:11:43 2015 +0200 @@ -630,10 +630,6 @@ val a = the (cong_name (head_of lhs)) handle Option.Option => raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]); val (xs, weak) = congs; - val _ = - if AList.defined (op =) xs a then - cond_warning ctxt (fn () => "Overwriting congruence rule for " ^ quote (#2 a)) - else (); val xs' = AList.update (op =) (a, thm) xs; val weak' = if is_full_cong thm then weak else a :: weak; in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);