Incorporating new/strengthened proofs from Library and AFP entries

infinite product material

tidying and reorganisation around Cauchy Integral Theorem

type class generalisations; some work on infinite products

tuned some proofs

--HG--
extra : transplant_source : %15%0D%CE%FC%93%A6k%C6%C4%E2%25id%1E%17%FBJg%19%2A

Added some simple facts about limits

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

Unified the order of zeros and poles; improved reasoning around non-essential singularites

--HG--
extra : amend_source : 528e99138923389ffcb3b2021c959a3c9f20de52

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

more elementary proof of connected_Times, earlier

moved t3/t4 space from AFP/Gromov to here.

more automation

tuned op's

isabelle update_cartouches -c -t;

prefer control symbol antiquotations;

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

Replaced subseq with strict_mono

Contravariant map on filters

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

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

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

Simplified Gamma_Function

Advanced topology

Many new theorems, and more tidying

A few new lemmas and needed adaptations

more new material

HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory

--HG--
extra : rebase_source : 081106cd39425dcfe6a04e687466bbb9ffedb25e

HOL-Probability: move conditional expectation from AFP/Ergodic_Theory

--HG--
extra : rebase_source : 55f4bbfc342a2532835d5bd35b92dd5cf39bc512

HOL-Probability: more about probability, prepare for Markov processes in the AFP

--HG--
extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14

new material connected with HOL Light measure theory, plus more rationalisation

Tuned L'Hospital

proper latex;

misc tuning and modernization;

Various additions to polynomials, FPSs, Gamma function

move open_Collect_eq/less to HOL

--HG--
extra : rebase_source : 96094aa6a000ee330467c05cc87a0888c8c05297

new results about topology

Facts about HK integration, complex powers, Gamma function

tuned proofs;

tuned proofs, to allow unfold_abs_def;

eliminated use of empty "assms";

eliminated old 'def';
tuned comments;

new theorems about convex hulls, etc.; also, renamed some theorems

Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results

new material to Blochj's theorem, as well as supporting lemmas

Substantial new material for multivariate analysis. Also removal of some duplicates.

New and revised material for (multivariate) analysis

instantiate topologies for nat, int and enat

--HG--
extra : rebase_source : 2320da44d4913f441c671ef425945fac6d4381c9

move product topology to HOL-Complex_Main

--HG--
extra : rebase_source : 80e22139dd7e4e8ac20bba89047fdda51008fbef

prefer abbreviations for compound operators INFIMUM and SUPREMUM

Reorganised a huge proof

isabelle update_cartouches -c -t;

setup code generation for filters as suggested by Florian

fix code generation for uniformity: uniformity is a non-computable pure data.

add uniform spaces

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;

Liouville theorem, Fundamental Theorem of Algebra, etc.

sorted out eventually_mono

Cauchy's integral formula for circles. Starting to fix eventually_mono.

isabelle update_cartouches -c -t;

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

Rounding function, uniform limits, cotangent, binomial identities

Cauchy's integral formula, required lemmas, and a bit of reorganisation

new material on path_component_sets, inside, outside, etc. And more default simprules

isabelle update_cartouches;

New theorems about connected sets. And pairwise moved to Set.thy.

prove Liminf_inverse_ereal

--HG--
extra : rebase_source : 7d8a9342e5dbe92c85b912b98c1ce573397ea836

New lemmas

new lemmas and movement of lemmas into place

tuned proofs -- less legacy;

new material for multivariate analysis, etc.

isabelle update_cartouches;

add continuous_onI_mono

tuned whitespace;

generalized tends over powr; added DERIV rule for powr

--HG--
extra : rebase_source : e5262f95063d694a1b08a65810ad2c515d8583a6

rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity

--HG--
extra : rebase_source : 6c7faec3b6fc45b9da856e08add46f99a0b483b7

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

move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter

move filters to their own theory

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

more standard access to goal state;

tuned signature;

proper context for Object_Logic operations;

tuned signature -- prefer qualified names;

ereal: tuned proofs concerning continuity and suprema

--HG--
extra : rebase_source : 88d9ba24758ab75b76f4b7e10f1fc85b74642f63

instance bool and enat as topologies

modernized header uniformly as section;

add tendsto_const and tendsto_ident_at as simp and intro rules

--HG--
extra : rebase_source : 22eac3c1e90ec123e3d2513334c670b5eb22d7e7

updated to named_theorems;

more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

--HG--
extra : rebase_source : 8664c1d86ed72607199cc8197a480070514ae330

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141

filters are easier to define with INF on filters.

--HG--
extra : rebase_source : 5626307315d6be224d16a97b9160690f09c8e0d4

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

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

add various lemmas

clean up Lebesgue integration

setup for Transfer and Lifting from BNF; tuned thm names

--HG--
rename : src/HOL/Tools/transfer.ML => src/HOL/Tools/Transfer/transfer.ML

left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)

extend continuous_intros; remove continuous_on_intros and isCont_intros

add connected_local_const

Some useful lemmas

enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;

normalising simp rules for compound operators

introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices

--HG--
rename : src/HOL/Library/Continuity.thy => src/HOL/Library/Order_Continuity.thy
extra : rebase_source : d8ac7002419cf6199ad52baea5d24cbc0e1a47e7

renamed 'fun_rel' to 'rel_fun'

renamed 'filter_rel' to 'rel_filter'

renamed 'set_rel' to 'rel_set'

A bit of tidying up

More complex-related lemmas

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

delete or move now not necessary reflexivity rules due to 1726f46d2aa8

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'

renamed 'nat_{case,rec}' to '{case,rec}_nat'

modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property

use bdd_above and bdd_below for conditionally complete lattices

add relator for 'a filter and parametricity theorems

factor out new lemma

replace lemma with more general simp rule

tuned proofs -- less guessing;

tuned proofs -- clarified flow of facts wrt. calculation;

renamed typeclass dense_linorder to unbounded_dense_linorder

--HG--
extra : rebase_source : 1aec1d46ec989f6555ab53f40d6db74ef5536fe0

factored syntactic type classes for bot and top (by Alessandro Coglio)

tuned headers;

revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space

renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)

--HG--
extra : rebase_source : 63f5230a997c030fcaa8377e299f12c9d6ec02a6

spell conditional_ly_-complete lattices correct

--HG--
rename : src/HOL/Conditional_Complete_Lattices.thy => src/HOL/Conditionally_Complete_Lattices.thy
extra : rebase_source : fe25f4dff8edab189f8c7a631785ba3cc5a19aa2

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

separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef

--HG--
rename : src/HOL/SupInf.thy => src/HOL/Conditional_Complete_Lattices.thy

move continuous_on_inv to HOL image (simplifies isCont_inverse_function)

move connected to HOL image; used to show intermediate value theorem

move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets

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)

generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

move first_countable_topology to the HOL image

move topological_space to its own theory