dedicated fact collections for algebraic simplification rules potentially splitting goals

--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6

imported new material mostly due to Sébastien Gouëzel

A couple of new theorems, stolen from AFP entries

new material; rotated premises of Lim_transform_eventually

a few new lemmas and a bit of tidying

moved some theorems into HOL main corpus

Generalisations involving numerals; comparisons should now work for ennreal

Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context

The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale

uniform naming

isabelle update -u control_cartouches;

isabelle update_cartouches -t;

uniform naming of strong congruence rules

removal of more redundancies, and fixes

elimination of near duplication involving Rolle's theorem and the MVT

proper code abbreviation for power on real

--HG--
extra : rebase_source : a05732afe72489a154efb122b87187171d459911

Made simproc for sqrt/root of numeral more robust

de-applying and meta-quantifying

fixes and more de-applying

more de-applying and a fix

more de-applying

de-applying, etc.

De-applying

de-applying, etc.

de-applying

Generalising and renaming some basic results

Rationalisation of complex transcendentals, esp the Arg function

removed some lemma duplicates

--HG--
extra : rebase_source : e56adb958684d57563b0ec467d4b13f1b726b4e0

Some tidying up (mostly regarding summations from 0)

moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

Added hyperbolic functions

added lemmas, avoid 'float_of 0'

standardized towards new-style formal comments: isabelle update_comments;

ran isabelle update_op on all sources

new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product

more symbols;

Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems

tuned

reorganized and added log-related lemmas

tuned proofs

reorganization of tree lemmas; new lemmas

Lemmas about analysis and permutations

Simprocs for roots of numerals

Simplification of some proofs. Also key lemmas using !! rather than ! in premises

Further new material. The simprule status of some exp and ln identities was reverted.

New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;

--HG--
rename : src/HOL/Main.thy => src/HOL/Pre_Main.thy

modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas

added numeral_powr_numeral

Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.

Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion

A few new lemmas and needed adaptations

added simp rule

setprod -> prod

setsum -> sum

left_distrib ~> distrib_right, right_distrib ~> distrib_left

tuned proofs;

Some facts about factorial and binomial coefficients

More analysis lemmas

more accurate cong del;
tuned proofs;

misc tuning and modernization;

tuned proofs -- avoid unstructured calculation;

misc tuning and modernization;

more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
* * *
more rules for setsum, setprod on intervals

simplified definitions of combinatorial functions

more theorems

Facts about HK integration, complex powers, Gamma function

tuned proofs, to allow unfold_abs_def;

isabelle update_cartouches -c -t;

eliminated use of empty "assms";

eliminated old 'def';
tuned comments;

added derivative of scaling in exponential function

lots of new theorems for multivariate analysis

add le_log_of_power and le_log2_of_power by Tobias Nipkow

New and revised material for (multivariate) analysis

more canonical names

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule

add the proof of the central limit theorem

--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b

Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function

more symbols;

more symbols;

more symbols;

prefer symbols for "abs";

prefer symbols for "floor", "ceiling";

Transcendental: use [simp]-canonical form - (pi/2)

--HG--
extra : rebase_source : 16d150606679aa4a47a4ac5769715a911ec5409d

sorted out eventually_mono

isabelle update_cartouches -c -t;

Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.

New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.

Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths

Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer

Rounding function, uniform limits, cotangent, binomial identities

added many small lemmas about setsum/setprod/powr/...

new lemmas about topology, etc., for Cauchy integral formula

real_of_nat_Suc is now a simprule

eliminated \<Colon>;

prefer symbols;

slight cleanup of lemmas

--HG--
extra : rebase_source : 17dbf1b3c59a40c2a2ac93ab58d3e6371773af6c

new material for multivariate analysis, etc.

isabelle update_cartouches;

generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal

avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead

generalized tends over powr; added DERIV rule for powr

--HG--
extra : rebase_source : e5262f95063d694a1b08a65810ad2c515d8583a6

tuned;

tidying some messy proofs

Tidying. Improved simplification for numerals, esp in exponents.

New material about complex transcendental functions (especially Ln, Arg) and polynomials

New material, mostly about limits. Consolidation.

move filters to their own theory

--HG--
rename : src/HOL/NSA/Filter.thy => src/HOL/NSA/Free_Ultrafilter.thy

fix latex in Transcendental

Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

arcsin and arccos lemmas

given up separate type classes demanding `inverse 0 = 0`

rationalised and generalised some theorems concerning abs and x^2.

New material and binomial fix

New material for complex sin, cos, tan, Ln, also some reorganisation

new HOL Light material about exp, sin, cos

Lots of new material on complex-valued functions. Modified simplification of (x/n)^k

The factorial function, "fact", now has type "nat => 'a"

removed junk;

renaming HOL/Fact.thy -> Binomial.thy

--HG--
rename : src/HOL/Fact.thy => src/HOL/Binomial.thy

sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex

clarified Drule.gen_all: observe context more carefully;

The function frac. Various lemmas about limits, series, the exp function, etc.

Removed the obsolete functions "natfloor" and "natceiling"

added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction

code equation for powr

modernized header uniformly as section;

more simp rules concerning dvd and even/odd

--HG--
extra : rebase_source : 895ed3f871c22790e8d199a30828e91bc13bd735

turn even into an abbreviation

add tendsto_const and tendsto_ident_at as simp and intro rules

--HG--
extra : rebase_source : 22eac3c1e90ec123e3d2513334c670b5eb22d7e7

augmented and tuned facts on even/odd and division

prefer generic elimination rules for even/odd over specialized unfold rules for nat

relaxed class constraints for exp

explicit separation of signed and unsigned numerals using existing lexical categories num and xnum

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

fact consolidation

Hypsubst preserves equality hypotheses

Fixes included for various theories affected by this change.

--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0

moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

added lemma

introduce more powerful reindexing rules for big operators

add various lemmas

added lemmas

added divide_nonneg_nonneg and co; made it a simp rule

--HG--
extra : rebase_source : 998eadb7cfbf8720cf961ac2e149ce4537557a47

made mult_pos_pos a simp rule

made divide_pos_pos a simp rule

made mult_nonneg_nonneg a simp rule

--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36

generalize ln/log_powr; add log_base_powr/pow

revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules

removing simprule status for divide_minus_left and divide_minus_right

merged DERIV_intros, has_derivative_intros into derivative_intros

extend continuous_intros; remove continuous_on_intros and isCont_intros

rearranging some deriv theorems

Some rationalisation of basic lemmas

further renaming in Series

cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}

unify syntax for has_derivative and differentiable

tuned proofs

repaired document;

More complex-related lemmas

Lemmas about Reals, norm, etc., and cleaner variants of existing ones

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'

tidied more proofs

cleaned up more messy proofs

cleaned up some messy proofs

eliminiated neg_numeral in favour of - (numeral _)

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

tuned proofs

generalize lemmas

--HG--
extra : rebase_source : 2af44a81e392ceab2d97d9822dbf3392753abfd3

tuned proofs;

more symbols;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

add lemma

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

move Ln.thy and Log.thy to Transcendental.thy

arcsin and arccos are continuous on {0 .. 1} (including the endpoints)

move continuous_on_inv to HOL image (simplifies isCont_inverse_function)

move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)

clean up lemma_nest_unique and renamed to nested_sequence_unique

prove tendsto_power_div_exp_0
* * *
missing rename

--HG--
extra : rebase_source : 2809e8af73b029406c9ce85b75b90c6fbf6cada9

add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2

--HG--
extra : rebase_source : 327fe91b9d9d244286b9a29c61e2f5fe56c9e295

add filterlim rules for exp and ln to infinity

Renamed {left,right}_distrib to distrib_{right,left}.

tuned some proofs;
removed duplicate lemma zero_le_imp_of_nat

merged fork with new numeral representation (see NEWS)

factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero

tendsto lemmas for ln and powr

--HG--
extra : transplant_source : N%CFc4%94f%CF%C9%1D%CFy%7F%EF%9B2%ED%B9%98D%B7

removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]

extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'

simplify proof of tan_half, removing unused assumptions

convert some proofs to Isar-style

add lemmas about arctan;
simplify some proofs about arctan;

convert lemma cos_total to Isar-style proof

convert lemma cos_is_zero to Isar-style

convert lemma sin_gt_zero to Isar style;
remove duplicate lemma sin_gt_zero1;

modify lemma sums_group, and shorten proofs that use it

generalize some lemmas

add lemmas cos_arctan and sin_arctan

remove redundant lemmas about LIMSEQ

discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems

move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs

remove unused lemma DERIV_sin_add

remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong

remove redundant lemma exp_ln_eq in favor of ln_unique

Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.

Transcendental.thy: remove several unused lemmas and simplify some proofs

remove unused lemmas

remove some redundant simp rules

optimize some proofs

remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

use divide instead of inverse for the derivative of ln

generalize infinite sums

eliminated global prems;
tuned proofs;

dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates

diff_minus subsumes diff_def

remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used

remove simp attribute from square_eq_1_iff

fix some linarith_split_limit warnings

move some theorems from RealPow.thy to Transcendental.thy

avoid using real-specific versions of generic lemmas

remove a couple of redundant lemmas; simplify some proofs

get rid of many duplicate simp rule warnings

fix looping call to simplifier

more precise proofs

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

new theory Algebras.thy for generic algebraic structures

A little rationalisation

tuned proofs;

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

Changed fact_Suc_nat back to fact_Suc

Moved factorial lemmas from Binomial.thy to Fact.thy and merged.

use DERIV_intros

Added DERIV_intros

corrected and unified thm names

generalize constants from Lim.thy to class metric_space

add constants sin_coeff, cos_coeff

Cleaned up Parity a little

stripped class recpower further

declare power_Suc [simp]; remove redundant type-specific versions of power_Suc

Merge.

make more proofs work whether or not One_nat_def is a simp rule

Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series

Added real related theorems from Fact.thy

Replaced group_ and ring_simps by algebra_simps;
removed compare_rls - use algebra_simps now

clean up lemmas about ln

clean up lemmas about exp

rearranged subsections; cleaned up some proofs

move theorems about limits from Transcendental.thy to Deriv.thy

cleaned up some proofs; removed redundant simp rules

move sin and cos to their own subsection

clean up some proofs; remove unused lemmas

made repository layout more coherent with logical distribution structure; stripped some $Id$s

--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML