added lemmas and transfer rules

material on finite sets and maps

--HG--
extra : amend_source : ff2581f3f58668d0b07cef46bf45bbd336607dbc

include lemmas generally useful for combinatorial proofs

moved from AFP/Gromov

standardized towards new-style formal comments: isabelle update_comments;

tuned;

tuned proofs;

"split add" -> "split"

misc tuning and modernization;

add lemmas contributed by Peter Gammie

misc tuning and modernization;

more theorems

Moved material from AFP/Randomised_Social_Choice to distribution

eliminated old 'def';
tuned comments;

Refactoring (moving theorems into better locations), plus a bit of new material

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

--HG--
extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9

more canonical names

more uniform treatment of package internals;

abandoned attempt to unify sublocale and interpretation into global theories

sorted out eventually_mono

isabelle update_cartouches -c -t;

modernized

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

option "inductive_defs" controls exposure of def and mono facts;

qualifier is mandatory by default;

Keyword 'rewrites' identifies rewrite morphisms.

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

tuned proofs -- less legacy;

eliminated \<Colon>;

new material for multivariate analysis, etc.

isabelle update_cartouches;

premises in 'show' are treated like 'assume';

tuned whitespace;

New material about paths, and some lemmas

add lema about card and vimage

add more general version of finite_vimageD

New lemmas and a bit of tidying up.

added lemma

modernized header uniformly as section;

added various facts

add lemma

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

--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141

add various lemmas

elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION

normalising simp rules for compound operators

more complete set of lemmas wrt. image and composition

removed theory dependency of BNF_LFP on Datatype

swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)

dissolved 'Fun_More_FP' (a BNF dependency)

prefix disambiguation

prefer ephemeral interpretation over interpretation in proof contexts;
prefer context begin ... end blocks for often-occuring assumptions;
slightly more complete interpretations into abstract algebraic structures for gcd/lcm

set_comprehension_pointfree simproc causes to many surprises if enabled by default

polished some ancient proofs

add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image

killed more "no_atp"s

killed most "no_atp", to make Sledgehammer more complete

added lemmas

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

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

convenient induction rule

--HG--
extra : rebase_source : 06e2fc8106aeb38db30daba81a01bbe09c008945

generalized lemma fold_image thanks to Peter Lammich

more uniform style for interpretation and sublocale declarations

--HG--
extra : rebase_source : 908fa43d5ac738a6c353d74475cb1910f6a318e8

fundamental revision of big operators on sets

locales for abstract orders

added lemma

added some ad-hoc namespace prefixes to avoid duplicate facts;

moving simproc from Finite_Set to more appropriate Product_Type theory

use Set.filter instead of Finite_Set.filter, which is removed then

rename Set.project to Set.filter - more appropriate name

consolidated names of theorems on composition;
generalized former theorem UN_o;
comp_assoc orients to the right, as is more common

congruence rule for Finite_Set.fold

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

prefer ML_file over old uses;

removed junk;

more set operations expressed by Finite_Set.fold

add finiteness lemmas for 'a * 'b and 'a set

tuned proofs -- prefer direct "rotated" instead of old-style COMP;

adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
noting further steps with FIXME

ignore morphism more explicitly;
tuned headers;

Integrated set comprehension pointfree simproc.

--HG--
rename : src/HOL/ex/set_comprehension_pointfree.ML => src/HOL/Tools/set_comprehension_pointfree.ML

remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit

rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'

move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy

--HG--
extra : transplant_source : 4%60%A0%BC%FE%DF%19%27%B6%DB%F9vS%7D%B6hbv%B8%8E

tuned proofs -- eliminated pointless chaining of facts after 'interpret';

incorporated various theorems from theory More_Set into corpus

--HG--
extra : rebase_source : 3382b66ad31349cb7368f064c467aa4a53845dd2

qualified Finite_Set.fold

finite type class instance for `set`

tuned

tune proofs

renamed Complete_Lattices lemmas, removed legacy names

new fastforce replacing fastsimp - less confusing name

added new lemmas

tuned

finite vimage on arbitrary domains

moving UNIV = ... equations to their proper theories

tuned proofs

point-free characterization of operations on finite sets

names of fold_set locales resemble name of characteristic property more closely

use point-free characterization for locale fun_left_comm_idem

use pointfree characterisation for fold_set locale

more uniform naming of lemma

dropped unused lemmas; proper Isar proof

tuned proofs

tuned proof

tuned lemma

added lemmas

moved theorem

restructured theory;
tuned proofs

eliminated global prems;
tuned proofs;

recoded latin1 as utf8;
use textcomp for some text symbols where it appears appropriate;

adding code equation for finiteness of finite types

gave more standard finite set rules simp and intro attribute

new lemma

Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

Replace surj by abbreviation; remove surj_on.

removed assumption

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

import swap prevents strange failure of SML code generator for datatypes

avoid explicit mandatory prefix markers when prefixes are mandatory implicitly

dropped superfluous [code del]s

"prod" and "sum" replace "*" and "+" respectively

added pigeonhole lemmas

avoid if on rhs of default simp rules

locale predicates of classes carry a mandatory "class" prefix

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

simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle

simplify fold_graph proofs

added locales folding_one_(idem); various streamlining and tuning

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

corrected disastrous syntax declarations

moved cardinality to Finite_Set as far as appropriate; added locales for fold_image

split off theory Big_Operators from theory Finite_Set

--HG--
rename : src/HOL/Finite_Set.thy => src/HOL/Big_Operators.thy

Generalized setsum_cases

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

moved remaning class operations from Algebras.thy to Groups.thy

get rid of many duplicate simp rule warnings

Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

added lemmas involving Min, Max, uminus

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

added lemmas

Two new theorems about cardinality

add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff

tuned lattices theory fragements; generlized some lemmas from sets to lattices

tuned

--HG--
extra : rebase_source : e260d697b790839af7519c59bc99073d646fffe9

renamed lemmas "anti_sym" -> "antisym"

fixed order of parameters in induction rules

inv_onto -> inv_into

Inv -> inv_onto, inv abbr. inv_onto UNIV.

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

idempotency case for fold1

inf/sup_absorb are no default simp rules any longer

be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer

inter and union are mere abbreviations for inf and sup

tuned proofs

adapted to localized interpretation of min/max-lattice

More finite set induction rules

refinement of lattice classes

typo

More about gcd/lcm, and some cleaning up

added boolean_algebra type class; tuned lattice duals

recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);

lemma finite_image_set by Jeremy Avigad

Removed unnecessary conditions concerning nonzero divisors

new lemma

finite lemmas

lemmas about basic set operations and Finite_Set.fold

A few finite lemmas

added/moved lemmas by Andreas Lochbihler

lemmas by Andreas Lochbihler

stripped class recpower further

Finite_Set: lemma
IsarRef: attribute arith

added setsum_eq_1_iff

cleaned up setprod_zero-related lemmas

generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs

added strong_setprod_cong[cong] (in analogy with setsum)
added some lemmas

interpretation/interpret: prefixes are mandatory by default;

equalities for Min, Max

Added general theorems for fold_image, setsum and set_prod

reverted to previous version of Finite_Set.thy

No idea what happened here!

dvd and setprod lemmas

added finite_set_choice

more finiteness

more finiteness

more finiteness

more finiteness changes

finiteness 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

handling type classes without parameters

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

Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta

changed import hierarchy

dropped ID

migrated class package to new locale implementation

Conversion of HOL-Main and ZF to new locales.

move lemmas from Numeral_Type.thy to other theories

Added new fold operator and renamed the old oe to fold_image.

tuned unfold_locales invocation

tuned import order

Removed uses of context element includes.

prove lemma finite in context of finite class

remove simp attribute from range_composition

Hid swap

- Deleted code setup for finite and card
- Deleted proof of "instance set :: (finite) finite" and modified proof of
"instance fun :: (finite, finite) finite", which now uses some ideas from
the instance proof for sets
- Instantiated arg_cong rule to avoid problems with HO unification

thms Max_ge, Min_le: dropped superfluous premise

Merged theories about wellfoundedness into one: Wellfounded.thy

only invoke interpret

no "attach UNIV" any more

tuned proofs

locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder

instantiation target rather than legacy instance

instance command as rudimentary class target

deleted card definition as code lemma; authentic syntax for card

renamed lordered_*_* to lordered_*_add_*; further localization

dropped "brown" syntax

went back to >0

global class syntax

explicit parameter for class finite

clarified

added lemmas

proper syntax during class specification

moved Finite_Set before Datatype

code lemmas for cardinality

added lemmas for finiteness

revised blacklisting for ATP linkup

moved ordered_ab_semigroup_add to OrderedGroup.thy

conciliated Inf/Inf_fin

dropped junk

ATP blacklisting is now in theory data, attribute noatp

minimize imports

rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp]

re-eliminated Option.thy

simplified proofs

using interpretation with derived concepts

simplified HOL bootstrap

Renamed inductive2 to inductive.

moved some finite lemmas here

tuned and renamed group_eq_simps and ring_eq_simps

tuned laws for cancellation in divisions for fields.

made divide_self a simp rule

tuned proofs: avoid implicit prems;

generalize class constraints on some lemmas

tuned comments

rudimentary class target implementation

no special treatment in naming of locale predicates stemming form classes

*** empty log message ***

generalize setsum lemmas from semiring_0_cancel to semiring_0

localized Min/Max

generalized type of lemma setsum_product

explizit "type" superclass

added FIXME hints

moved order on functions here

moved instance option :: finite here

added code theorems for UNIV

added class "preorder"

Adapted to new inductive definition package.

Modified lattice locale

generalized type signature of foldSet, fold

tuned proofs;

clarified module dependencies

more robust syntax for definition/abbreviation/notation;

renamed Lattice_Locales to Lattices

made locale partial_order compatible with axclass order

* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
Richer structures do not inherit from semiring_0 anymore, because
anihilation is a theorem there, not an axiom.

* Generalized axclass "recpower" to arbitrary monoid, not just
commutative semirings.

Method intro_locales replaced by intro_locales and unfold_locales.

Restructured locales with predicates: import is now an interpretation.
New method intro_locales.

new results

tuned;

new lemmas concerning finite cardinalities

replaced syntax/translations by abbreviation;
tuned proofs;
tuned;

refined 'abbreviation';

translations -> abbreviations (a cool feature)

Renamed setsum_mult to setsum_right_distrib.

more lemmas

new lemmas

replaced _K by dummy abstraction;

new lemmas

renamed rules to iprover

patterns in setsum and setprod

Lemmas on dvd, power and finite summation added or strengthened.

more simprules now have names

added Brian Hufmann's finite instances

added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy

changed imports due to new GCD.thy

linear arithmetic now takes "&" in assumptions apart.

Added strong_setsum_cong and strong_setprod_cong.

fixed \<Prod> syntax

Subsumption of locale interpretations.

tuning locales

Used locale interpretations everywhere.

fixed presentation

Cleaned up, now uses interpretation.

integrated Jeremy's FiniteLib

added setsum_diff1' which holds in more general cases than setsum_diff1

more setsum tuning

more fine tuniung

comprehensive cleanup, replacing sumr by setsum

tuning

simplified a proof

some stuff is now redundant.

non-inductive fold1Set proofs

simplified a key lemma for foldSet

Subscripts for theorem lists now start at 1.

Extracted generic lattice stuff to new Lattice_Locales.thy

new foldSet proofs

revised fold1 proofs

revised fold1 proofs

cvs merge problem fixed

new treatment of fold1

Fixed lattice defns

*** empty log message ***

fixed latex problems

Added Lattice locale

comment

Added semi-lattice locales and reorganized fold1 lemmas

generalization and tidying

fold and fol1 changes

added [simp]

renamed a few vars, added a lemma

proof simpification

new theorem image_eq_fold

new and stronger lemmas and improved simplification for finite sets

REorganized Finite_Set

First step in reorganizing Finite_Set

Started to clean up and generalize FiniteSet

changed the order of !!-quantifiers in finite set induction.
In Isar you can now write (insert x F) rather than the counterintuitive
(insert F x).

prettier proof of setsum_diff

renamed 2 lemmas

relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring

Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff

generalized lemma

added lemma

More lemmas

simplification tweaks for better arithmetic reasoning

revised simprules for division

import -> imports

New theory header syntax.

Aded a thm.

added some inj_on thms

Modified \<Sum> syntax a little.

redefining sumr to be a translation to setsum

added {0::nat..n(} = {..n(}

ringpower to recpower

strengthened some theorems

moved some cardinality results into main HOL

removed a premise of card_inj_on_le

fixed latex problems

changes made due to new Ring_and_Field theory

tuned notation;

use more symbols in HTML output

new type class abelian_group

new material from Avigad

strengthened the axclass claims

generic theorems about exponentials; general tidying up

new material from Avigad, and simplified treatment of division by 0

re-organized numeric lemmas

*** empty log message ***

misc tidying

new inverse image lemmas

added a few lemmas

HOL-Algebra partially ported to Isar.

Transitive closure is now defined inductively as well.

Proof tidying

less use of x-symbols

Added Mi and Max on sets, hid Min and Pls on numerals.

simplified locale predicates;

accomodate cumulative locale predicates;

ACe_axioms;

adapted to locale defs;

clarified syntax of ``long'' statements: fixes/assumes/shows;

lemmas (in ACe) AC;

qualified exports from locales;

renamed theory Finite to Finite_Set and converted;