de-applying (mostly Set_Interval)

moved lemmas

fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring

lots of new material, ultimately related to measure theory

ran isabelle update_op on all sources

kill old size infrastructure

more symbols;

more induct rules on nat

--HG--
extra : rebase_source : 6cf6194734b5fe2e4195a09814866d229cca60d7

added lemma

--HG--
extra : rebase_source : e435f276e7e9ddfb1136b9ef4088de49a42f9ddc

tuned some proofs and added some lemmas

--HG--
extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be

more fundamental definition of div and mod on int

--HG--
extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800

generalized simproc

--HG--
extra : rebase_source : 1a484c6a7a8374a73f471204dea8be4ee982845f

added lemmas

moved transitive_stepwise_le into Nat, where it belongs

strengthened tactic

tuned names

redefined Greatest

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

generalized types in lemmas

moved some lemmas to appropriate places

--HG--
extra : rebase_source : d3d8537b1c25edc3e07620dda770ad1feb37ea72

dropped slightly outdated comment

--HG--
extra : rebase_source : a1591b23b86abf507eb7098188a636666bfc2ab9

added lemma

clarified lfp/gfp statements and proofs;

"split add" -> "split"

misc tuning and modernization;

add lemmas contributed by Peter Gammie

rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;

--HG--
rename : src/Tools/rat.ML => src/Pure/General/rat.ML

isabelle update_cartouches -c -t;

removed odd cases rule (see also 8cb42cd97579);

tuned document;

misc tuning and modernization;

Moved material from AFP/Randomised_Social_Choice to distribution

eliminated old 'def';
tuned comments;

clarified rule structure;

more theorems on orderings

--HG--
extra : rebase_source : 4e5a14cb68359f057eb65c380c103e23971ad09c

removed junk;

tuned bootstrap order to provide type classes in a more sensible order

--HG--
extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9

generalize more theorems to support enat and ennreal

--HG--
extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d

Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.

--HG--
extra : rebase_source : 54bd3e5fcde04ef38241be91231c48d078b850f2

sorted out some duplicate fact bindings

--HG--
extra : rebase_source : 3431087ca99d182d28ecf04b75f0b422615af1f2

pulled out legacy aliasses and infamous dvd interpretations into theory appendix

allow predicator instead of map function in 'primrec'

Reorganised a huge proof

isabelle update_cartouches -c -t;

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

Rounding function, uniform limits, cotangent, binomial identities

discontinued specific HTML syntax;

tuned proofs -- less legacy;

simplified simproc programming interfaces;

eliminated \<Colon>;

prefer symbols;

isabelle update_cartouches;

add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer

--HG--
extra : rebase_source : b8f67b531a15510b1f468145a6194cf68875d262

Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.

add transfer theorems for fixed points

implicit partial divison operation in integral domains

add lfp/gfp rule for nn_integral

clarified no_zero_devisors: makes only sense in a semiring;
actually turn linorder_semidom into a integral domain

--HG--
extra : rebase_source : 20e224f329987c38e10dba58521b744a19110ced

distributivity of partial minus establishes desired properties of dvd in semirings

--HG--
extra : rebase_source : 99dad957de0410b3a1ca21ff1f8723495b31194f

explicit commutative additive inverse operation;
more explicit focal point for commutative monoids with an inverse operation

--HG--
extra : rebase_source : ed4c155428dd5783c8e0663805a92b15992e85d3

tuned signature -- prefer qualified names;

import general theorems from AFP/Markov_Models

equivalence rules for structures without zero divisors

--HG--
extra : rebase_source : 117d7728292b1473f0416ee8615654859adf7216

modernized header uniformly as section;

modernized setup;

generalized and consolidated some theorems concerning divisibility

more facts about abstract divisibility

made new 'primrec' bootstrapping-capable

moved old 'size' generator together with 'old_datatype'

--HG--
rename : src/HOL/Tools/Function/old_size.ML => src/HOL/Tools/Old_Datatype/old_size.ML

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

added 'plugins' option to control which hooks are enabled

reordered some (co)datatype property names for more consistency

updated to named_theorems;

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

Hypsubst preserves equality hypotheses

Fixes included for various theories affected by this change.

--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0

use 'where' clause for selector default value syntax

got rid of '=:' squiggly

added lemma

fix HOL-NSA; move lemmas

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

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

moved 'primrec' up (for real this time) and removed temporary 'old_primrec'

renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)

aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax

renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)

don't hide constant forever, since it may appear in some 'primcorec'-generated theorems

remove hidden fact about hidden constant from code generator setup

for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'

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'

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt

--HG--
extra : rebase_source : 02e892232f20d46af3dd46c4047e264fc49d378b

stronger inc_induct and dec_induct

restructed

--HG--
extra : rebase_source : 616c48d7ea31bebdcc552b6b49aa376ef8b2934a

generalised lemma

--HG--
extra : rebase_source : 4dadcb70fe7d53997e4493916ca598db52a7e121

killed most "no_atp", to make Sledgehammer more complete

tuned proofs

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

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

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

type class for confined subtraction

turned example into library for comparing growth of functions

--HG--
rename : src/HOL/ex/Landau.thy => src/HOL/Library/Function_Growth.thy

split dense into inner_dense_order and no_top/no_bot

Sieve of Eratosthenes

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

discontinued obsolete typedef (open) syntax;

alternative simplification of ^^ to the righthand side;
lifting of comp_fun_commute to ^^

typeclass formalising bounded subtraction

prefer ML_file over old uses;

replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms

give Nat_Arith simprocs proper name bindings by using simproc_setup

tuned proofs;

tuned some proofs;
removed duplicate lemma zero_le_imp_of_nat

removed Nat_Numeral.thy, moving all theorems elsewhere

move lemmas from Nat_Numeral.thy to Nat.thy

merged fork with new numeral representation (see NEWS)

adding yet another induction rule on natural numbers

moving declarations back to the section they seem to belong to (cf. afffe1f72143)

attribute code_abbrev superseedes code_unfold_post

--HG--
extra : rebase_source : c121dde677a8fb25289c668f8f6a123174fb117d

generalized type signature to permit overloading on `set`

add lemmas

weaken preconditions on lemmas

lemmas about Kleene iteration

prefer typedef without alternative name;

replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

new fastforce replacing fastsimp - less confusing name

remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}

lemmas about +, *, min, max on nat

more uniform formatting of specifications

observe distinction between sets and predicates more properly

modernized some simproc setup;

tuned

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

more concise characterization of of_nat operation and class semiring_char_0

dropped superfluous [code del]s

added lemma funpow_mult

qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

add lemmas Nats_cases and Nats_induct

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

get rid of many duplicate simp rule warnings

tuned import order

hide fact names clashing with fact names from Group.thy

hide fact Nat.add_0_right; make add_0_right from Groups priority

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

more regular axiom of infinity, with no (indirect) reference to overloaded constants

renamed lemmas "anti_sym" -> "antisym"

tuned code setup

moved lemmas for dvd on nat to theories Nat and Power

tuned whitespace

tuned the simp rules for Int involving insert and intervals.

tuned proofs

code attributes use common underscore convention

generalized less_Suc_induct

monomorphic code generation for power operations

tuned interface of Lin_Arith

reimplement reorientation simproc using theory data

some jokes are just too bad to appear in a theory file

funpow and relpow with shared "^^" syntax

avoid local [code]

power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure

moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac

vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement

--HG--
rename : src/HOL/Tools/arith_data.ML => src/HOL/Tools/nat_arith.ML

Merge.

revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)

add lemma diff_Suc_1

make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules

added lemmas

Moved FTA into Lib and cleaned it up a little.

--HG--
rename : src/HOL/Fundamental_Theorem_Algebra.thy => src/HOL/Library/Fundamental_Theorem_Algebra.thy

Deleted the induction rule nat_induct2, which was too weak and not used even once.

new attribute "arith" for facts supplied to arith.

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

nat is a bot instance

no base sort in class import

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

tuned unfold_locales invocation

`code func` now just `code`

tuned of_nat code generation

moved class wellorder to theory Orderings

added lemmas

tuned

simplified proofs

added lemmas

removed obsolete nat_induct_tac -- cannot work without;

added nat_induct_tac (works without context);

rep_datatype command now takes list of constructors as input arguments

Merged theories about wellfoundedness into one: Wellfounded.thy

removed redundant Nat.less_not_sym, Nat.less_asym;
renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;

removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
renamed less_imp_le to less_imp_le_nat;

removed duplicate lemmas;

tuned heading

Added useful general lemmas from the work with the HeapMonad

tuned structures in arith_data.ML

<= and < on nat no longer depend on wellfounded relations

tuned code setup

Renamed *.size to prod.size.

added lemma

instantiation target rather than legacy instance

temporary code generator work arounds

authentic primrec

simplified infrastructure for code generator operational equality

adjustions to due to instance target

instance command as rudimentary class target

dropped implicit assumption proof

tuned specifications of 'notation';

simplified proof

various localizations

went back to >0

random tidying of proofs

dropped superfluous inlining lemmas

More changes from >0 to ~=0::nat

Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.

neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...

localized mono predicate

global class syntax

refined; moved class power to theory Power

added code lemma for 1

datatype interpretators for size and datatype_realizer

added variations on infinite descent

Added infinite_descent

ATP blacklisting is now in theory data, attribute noatp

localized of_nat

split off theory Option for benefit of code generator

added Tools/lin_arith.ML;

arith method setup: proper context;

moved set Nats to Nat.thy

Adapted to new package for inductive sets.

fix looping simp rule

remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int

change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems

add lemma inj_of_nat

add axclass semiring_char_0 for types where of_nat is injective

generalize of_nat and related constants to class semiring_1

tuned boostrap

added induction principles for induction "backwards": P (Suc n) ==> P n

size [nat] is identity

changed code generator invocation syntax

Isar definitions are now added explicitly to code theorem table

tuned proofs;

added instance for lattice

explizit "type" superclass

adjusted code lemmas

simpliefied instance statement

Adapted to new inductive definition package.

min/max lemmas (actually unused!)

Added lemma nat_size[simp]: "size (n::nat) = n"

added aliases for nat_recs/cases;

cleanup

power is now a class

removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);

removed theory NatArith (now part of Nat);

code generator module naming improved

added explicit print translation for nat_case

added code generator names for nat_rec and nat_case

renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes

refinements in codegen serializer

name shifts

added operational equality

simplified code generator setup

cleanup code generation for Numerals

slight adaption for code generator

new results

axiomatization;

substantial improvements in code generator

tidied, and giving theorems names

more finalconsts;

renamed rules to iprover

generlization of some "nat" theorems

linear arithmetic now takes "&" in assumptions apart.

Moved some code lemmas from Main to Nat.

Fixing a problem with lin.arith.

comprehensive cleanup, replacing sumr by setsum

removal of archaic Abs/Rep proofs

converted to Isar script, simplifying some results

More lemmas

converted some induct_tac to induct

import -> imports

New theory header syntax.

fixed latex problems

changes made due to new Ring_and_Field theory

tuned instance statements;

Defining the type class "ringpower" and deleting superseded theorems for
types nat, int, real, hypreal

Ring_and_Field now requires axiom add_left_imp_eq for semirings.
This allows more theorems to be proved for semirings, but
requires a redundant axiom to be proved for rings, etc.

re-organized numeric lemmas

*** empty log message ***

More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
to Isar script.

conversion of integers to use Ring_and_Field;
new lemmas for Ring_and_Field

HOL: installation of Ring_and_Field as the basis for Naturals and Reals

misc tidying

Improved efficiency of code generated for + and -

declarations moved from PreList.thy

modified induct method

Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"

- Converted to new theory format
- Moved NatDef stuff to theory Nat

renamed class "term" to "type" (actually "HOL.type");

partial restructuring to reduce dependence on Axiom of Choice

Inductive definitions are now introduced earlier in the theory hierarchy.

added nat as instance of new wellorder axclass

added axclass power (from HOL.thy);

rearranged setup of arithmetic procedures, avoiding global reference values;

removed DatatypePackage.setup;

Changed syntax of rep_datatype.

updated comments

Declaration of type 'nat' as a datatype (this allows usage of
exhaust_tac and induct_tac on type 'nat'). Moved some proofs
using natE from NatDef.ML to Nat.ML.

Congruence rules use == in premises now.
New class linord.

Replaced ALLNEWSUBGOALS by THEN_ALL_NEW

nat datatype_info moved to Nat.thy;

Overloading of "^" requires new type class "power", with types "nat" and
"set" in that class. The operator itself is declared in Nat.thy

New class "order" and accompanying changes.
In particular reflexivity of <= is now one rewrite rule.

removed \<mu> syntax;

adaptions for symbol font

moved "1", "2" to syntax section;

Changed argument order of nat_rec.

*** empty log message ***

repaired critical proofs depending on the order inside non-confluent SimpSets,
(temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"

*** empty log message ***

Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy

Converted TABs to spaces

Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
Added cardinality to Finite.

expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes

removed quotes from types in consts and syntax sections

removed \...\ inside strings

changed syntax of tuples from <..., ...> to (..., ...)

new version of HOL with curried function application