summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Mon, 22 Apr 2013 16:36:02 +0200 | |

changeset 51732 | 4392eb046a97 |

parent 51731 | f27e22880cc3 |

child 51733 | 70abecafe9ac |

NEWS

--- a/NEWS Sun Apr 21 20:08:13 2013 +0200 +++ b/NEWS Mon Apr 22 16:36:02 2013 +0200 @@ -94,9 +94,84 @@ Code_Target_Nat and Code_Target_Numeral. See the tutorial on code generation for details. INCOMPATIBILITY. -* Theory "RealVector" and "Limits": Introduce type class -(lin)order_topology. Allows to generalize theorems about limits and -order. Instances are reals and extended reals. +* Introduce type class "conditional_complete_lattice": Like a complete + lattice but does not assume the existence of the top and bottom elements. + Allows to generalize some lemmas about reals and extended reals. + Removed SupInf and replaced it by the instantiation of + conditional_complete_lattice for real. Renamed lemmas about conditional + complete lattice from Sup_... to cSup_... and from Inf_... to + cInf_... to avoid hidding of similar complete lattice lemmas. +INCOMPATIBILITY. + +* Introduce type classes "no_top" and "no_bot" for orderings without top + and bottom elements. + +* Split dense_linorder into inner_dense_order and no_top, no_bot. + +* Complex_Main: Unify and move various concepts from + HOL-Multivariate_Analysis to HOL-Complex_Main. + + - Introduce type class (lin)order_topology. Allows to generalize theorems + about limits and order. Instances are reals and extended reals. + + - continuous and continuos_on from Multivariate_Analysis: + "continuous" is the continuity of a function at a filter. + "isCont" is now an abbrevitation: "isCont x f == continuous (at _) f". + + Generalized continuity lemmas from isCont to continuous on an arbitrary + filter. + + - compact from Multivariate_Analysis. Use Bolzano's lemma + to prove compactness of closed intervals on reals. Continuous functions + attain infimum and supremum on compact sets. The inverse of a continuous + function is continuous, when the function is continuous on a compact set. + + - connected from Multivariate_Analysis. Use it to prove the + intermediate value theorem. Show connectedness of intervals on order + topologies which are a inner dense, conditional complete linorder. + + - first_countable_topology from Multivariate_Analysis. Is used to + show equivalence of properties on the neighbourhood filter of x and on + all sequences converging to x. + + - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved theorems + from Library/FDERIV.thy to Deriv.thy and base the definition of DERIV on + FDERIV. Add variants of DERIV and FDERIV which are restricted to sets, + i.e. to represent derivatives from left or right. + + - Removed the within-filter. It is replaced by the principal filter: + + F within X = inf F (principal X) + + - Introduce "at x within U" as a single constant, "at x" is now an + abbreviation for "at x within UNIV" + + - Introduce named theorem collections tendsto_intros, continuous_intros, + continuous_on_intros and FDERIV_intros. Theorems in tendsto_intros (or + FDERIV_intros) are also available as tendsto_eq_intros (or + FDERIV_eq_intros) where the right-hand side is replaced by a congruence + rule. This allows to apply them as intro rules and then proving + equivalence by the simplifier. + + - Restructured theories in HOL-Complex_Main: + + + Moved RealDef and RComplete into Real + + + Introduced Topological_Spaces and moved theorems about + topological spaces, filters, limits and continuity to it + + + Renamed RealVector to Real_Vector_Spaces + + + Split Lim, SEQ, Series into Topological_Spaces, Real_Vector_Spaces, and + Limits + + + Moved Ln and Log to Transcendental + + + Moved theorems about continuity from Deriv to Topological_Spaces + + - Remove various auxiliary lemmas. + +INCOMPATIBILITY. * Consolidation of library theories on product orders: