removed unused auxiliary lemmas

strengthened type class for bit operations

slightly more specialized name for type class

More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots

--HG--
extra : amend_source : 3cd58385530e02e27dd013f3706cee7dc704e74c

algebraized more material from theory Divides

--HG--
extra : rebase_source : 3c28e3310e44ad2333f68931aa61b68c0a8f4c0a

isabelle update -u control_cartouches;

clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);

de-applying and simplifying proofs

de-applying

de-applying

avoid overaggressive classical rule

--HG--
extra : rebase_source : 53a1eeba712a12b1da867fa7ecf2289255f06680

grouped material on numeral division

removed some non-essential rules

removed some lemma duplicates

--HG--
extra : rebase_source : e56adb958684d57563b0ec467d4b13f1b726b4e0

eliminiated superfluous class semiring_bits

abstract algebraic bit operations

--HG--
extra : rebase_source : 10402190e8858b0ea47b7ac7f91671a9935921ae

isabelle update_cartouches -c -t;

more simplification rules

--HG--
extra : rebase_source : 2b7704ac9459d132ec9fea4769b865bdcad1548f

more symbols;

new simp rule

added lemmas and tuned proofs

--HG--
extra : rebase_source : 96f42feb3c60e71f2655c97d331ac68baf8b4a63

tuned proofs

--HG--
extra : rebase_source : f75a8a3d183658e5e8f4190946b69265b54c84c9

euclidean rings need no normalization

--HG--
extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05

more fundamental definition of div and mod on int

--HG--
extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800

one uniform type class for parity structures

--HG--
extra : rebase_source : edf12af006cee8d114754f4a1916094166004337

generalized some rules

--HG--
extra : rebase_source : 025e3e1adc961b68e923d241a8e1cb5c2efd0351

generalized simproc

--HG--
extra : rebase_source : 1a484c6a7a8374a73f471204dea8be4ee982845f

elementary definition of division on natural numbers

--HG--
extra : rebase_source : 23767fa1baf28db39b18de60e52d4d7f852e48dd

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

--HG--
extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1

avoid fact name clashes

--HG--
extra : rebase_source : dadb340e6deb1d95749a6828999b5295bffc7702

spelling and tuned whitespace

--HG--
extra : rebase_source : 57fae3b6b07a0d6188e93b76ac6bbc94f6bb6341

speed up proofs slightly

more lemmas

slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization

--HG--
extra : rebase_source : 0d5af77e2a7d66625c22923a19c456b1ca17652e

moved euclidean ring to HOL

--HG--
extra : rebase_source : f98dc2e61ffb3cbd04e533f3c0cffa028129e4a2

more elementary rules about div / mod on int

--HG--
extra : rebase_source : 335ac290cf7449e171b21d6aadc74d1c128a8601

more uniform div/mod relations

emphasize dedicated rewrite rules for congruences

--HG--
extra : rebase_source : 28c5807c3eda548e5ed0637459d63997c46e3ff3

reoriented congruence rules in non-explosive direction

--HG--
extra : rebase_source : 7b0d0d20a7c78db1ac5f12fb0d4ab0d915d0f2a3

more fine-grained type class hierarchy for div and mod

--HG--
extra : rebase_source : fffbeef99e834ca17596f478178e94bed8a014bc

clarified prover-specific rules

eliminated irregular aliasses

clarified theorem names

eliminated irregular aliasses

more standardized theorem names for facts involving the div and mod identity

more standardized names

de-orphanized declaration

separate type class for arbitrary quotient and remainder partitions

--HG--
extra : rebase_source : c803a2a721f660672d64831c56088100891baa86

more lemmas

--HG--
extra : rebase_source : f52072de0fdc0fac0b2505569668d385d1ffe93d

syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div

--HG--
extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4

more lemmas

--HG--
extra : rebase_source : 3446eb0648af16d2212d2a3e40591332dd90c26c

tuned proofs;

Tuned looping simp rules in semiring_div

--HG--
extra : rebase_source : 3b3829fdddfdfffaad7cac785a601ef678dc9b93

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

Various additions to polynomials, FPSs, Gamma function

isabelle update_cartouches -c -t;

eliminated old 'def';
tuned comments;

model characters directly as range 0..255
* * *
operate on syntax terms rather than asts

more canonical names

prefer symbols for "abs";

isabelle update_cartouches -c -t;

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

qualify some names stemming from internal bootstrap constructions

--HG--
extra : rebase_source : 0a98ecf4c3d40ee7459e760b378afbad4bf89ce3

monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime

--HG--
extra : rebase_source : e05d79a48b81d6ffe67aca3743dbab1781bd1e4f

eliminated suspicious unicode;

eliminated \<Colon>;

qualified adjust_*

--HG--
extra : rebase_source : 0e0c41347fcf41a8750a5c6eeed5a7957c43861c

direct bootstrap of integer division from natural division

slight cleanup of lemmas

--HG--
extra : rebase_source : 17dbf1b3c59a40c2a2ac93ab58d3e6371773af6c

isabelle update_cartouches;

tuned facts

moved normalization and unit_factor into Main HOL corpus

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.

separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial

--HG--
extra : rebase_source : 0045d1e39f330613bb1913e52e231f8be282a80a

generalized some theorems about integral domains and moved to HOL theories

--HG--
extra : rebase_source : 2e548495060b9f818a41b1e5333ed921a3b84ac4

uniform _ div _ as infix syntax for ring division

--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9

implicit partial divison operation in integral domains

separate class for division operator, with particular syntax added in more specific classes

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

prefer local fixes;

eliminated technical fact alias

canonical name

added simp lemma

renamed "pairself" to "apply2", in accordance to @{apply 2};

generalized lemmas (particularly concerning dvd) as far as appropriate

import general theorems from AFP/Markov_Models

self-contained simp rules for dvd on numerals

--HG--
extra : rebase_source : 58c009467b675088031714cb7978d38db128ab26

proper oriented equivalence of dvd predicate and mod

--HG--
extra : rebase_source : e7ebe794027e5abe1567181c8cc20badb81feff6

modernized header uniformly as section;

avoid noise (cf. 03ff4d1e6784);

more simp rules concerning dvd and even/odd

--HG--
extra : rebase_source : 895ed3f871c22790e8d199a30828e91bc13bd735

more simp rules;
slight proof tuning

--HG--
extra : rebase_source : d463b58b8b33fbbeadcc0510c471966b813b1179

even further downshift of theory Parity in the hierarchy

--HG--
extra : rebase_source : d3582456671ff992f3d453a0def98065cde7db5a

augmented and tuned facts on even/odd and division

specialized specification: avoid trivial instances

redundant: dropped

--HG--
extra : rebase_source : 11bd474dd732bc6a7d96e95e7435d1a80df215fe

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

Hypsubst preserves equality hypotheses

Fixes included for various theories affected by this change.

--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0

eliminated hard tabs (assuming tab-width=2);

renamed '{prod,sum,bool,unit}_case' to 'case_...'

more direct simplification rules for 1 div/mod numeral;
added simplification rules for (- 1) div/mod numeral

moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain

--HG--
rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy

eliminiated neg_numeral in favour of - (numeral _)

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
tuned presburger

--HG--
extra : rebase_source : 30fe190a27dae1b09024f4fdd70ee005a33e99ba

explicit type class for modelling even/odd parity

--HG--
extra : rebase_source : c21e4a6f9bc2e040f65aec0e592e282e386172d8

more lemmas on division

--HG--
extra : rebase_source : 45547b1ff0044c29b1d6ee9fd444ffdc8ac013fd

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

removed junk;

spelling and typos

execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs

relaxed preconditions

type class for generic division algorithm on numerals

added lemma

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

added lemma

simplifier uses proper Proof.context instead of historic type simpset;

proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);

Sieve of Eratosthenes

avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;

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

prefer ML_file over old uses;

move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used

add simp rules for dvd on negative numerals

removed Nat_Numeral.thy, moving all theorems elsewhere

removed redundant nat-specific copies of theorems

remove more redundant lemmas

tuned proofs

--HG--
extra : transplant_source : /%9B%A4%23%18%3E%90%A4-%E0%0A%E9%A6%A9%C8%1D%83%EE%82s

remove redundant lemmas

generalized lemma zpower_zmod

remove redundant lemma

remove redundant lemma

generalize more div/mod lemmas

generalize some theorems about div/mod

remove redundant lemmas

move int::ring_div instance upward, simplify several proofs

rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names

extend definition of divmod_int_rel to handle denominator=0 case

tuned proofs

shorten a proof

simplify some proofs

rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.

simplify some proofs

merged fork with new numeral representation (see NEWS)

remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)

removing some unnecessary premises from Divides

simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat

--HG--
extra : rebase_source : 7ed52e71daa69142f147737027b94acaef451223

eliminated obsolete "standard";

rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests

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

avoid using legacy theorem names

modernized some simproc setup;

renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics

eliminated global prems;
tuned proofs;

added lemmas

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

dropped superfluous [code del]s

a ring_div is a ring_1_no_zero_divisors

tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)

weakend class ring_div; tuned

transfer: avoid camel case

lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult

get rid of many duplicate simp rule warnings

renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields

--HG--
rename : src/HOL/Ring_and_Field.thy => src/HOL/Fields.thy
rename : src/HOL/OrderedGroup.thy => src/HOL/Groups.thy
rename : src/HOL/Ring_and_Field.thy => src/HOL/Rings.thy

added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick

removed legacy asm_lr

polished Nitpick's binary integer support etc.;
etc. = improve inconsistent scope correction + sort values nicely in output
+ handle "mod" using the characterization "x mod y = x - x div y * y"
(instead of explicit code in Nitpick)
+ introduce KK = Kodkod as abbreviation

added lemma

Fixed splitting of div and mod on integers (split theorem differed from implementation).

Fixed splitting of div and mod on integers (split theorem differed from implementation).

tuned code setup

combined former theories Divides and IntDiv to one theory Divides

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

moved theory Divides after theory Nat_Numeral; tuned some proof texts

moved lemmas for dvd on nat to theories Nat and Power

more antiquotations;

code attributes use common underscore convention

renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int

generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div

move lemma div_power into semiring_div context; class ring_div inherits from idom

dropped reference to class recpower and lemma duplicate

tuned setups of CancelDivMod

tightended specification of class semiring_div

more coherent developement in Divides.thy and IntDiv.thy

added nat_div_gt_0 [simp]

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

interpretation/interpret: prefixes are mandatory by default;

lemma nat_dvd_not_less moved here from Arith_Tools

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

added div lemmas

Merge.

removed and renamed redundant lemmas

added lemmas by Jeremy Avigad

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

move lemma dvd_mod_imp_dvd into class semiring_div

added dvd_div_mult

Removed subsumed lemmas

removed subsumed lemmas

generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power

Cleaned up IntDiv and removed subsumed lemmas.

dvd and setprod lemmas

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

migrated class package to new locale implementation

add class ring_div; generalize mod/diff/minus proofs for class ring_div

generalize zmod_zmod_cancel -> mod_mod_cancel

generalize some div/mod lemmas; remove type-specific proofs

Conversion of HOL-Main and ZF to new locales.

codegen

tuned unfold_locales invocation

`code func` now just `code`

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

(re-)added simp rules for (_ + _) div/mod _

moved op dvd to theory Ring_and_Field; generalized a couple of lemmas

separate class dvd for divisibility predicate

Merged theories about wellfoundedness into one: Wellfounded.thy

removed duplicate lemmas;

using only an relation predicate to construct div and mod

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

more abstract lemmas

tuned proofs;

added class semiring_div

instantiation target rather than legacy instance

went back to >0

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

fixed proofs

global class syntax

class div inherits from class times

proper syntax during class specification

ATP blacklisting is now in theory data, attribute noatp

minimize imports

using class target

introduced (auxiliary) class dvd_mod for more convenient code generation

removed dead code;

uniform module names for code generation

tuned

tuned

changed code generator invocation syntax

added lemmatas

Isar definitions are now added explicitly to code theorem table

tuned proofs;

explizit "type" superclass

Adapted to changes in Transitive_Closure theory.

added OCaml code generation (without dictionaries)

div is now a class

code generator module naming improved

name shifts

explicit divmod algorithm for code generation

lin_arith_prover: splitting reverted because of performance loss

simplified code generator setup

lin_arith_prover splits certain operators (e.g. min, max, abs)

linear arithmetic splits certain operators (e.g. min, max, abs)

simprocs: no theory argument -- use simpset context instead;

substantial improvements in code generator

presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy

add header

Provers/cancel_sums.ML: Simplifier.inherit_bounds;

tuned theory dependencies;

more simprules now have names

classical rules must have names for ATP integration

generlization of some "nat" theorems

linear arithmetic now takes "&" in assumptions apart.

made diff_less a simp rule

converted some induct_tac to induct

import -> imports

New theory header syntax.

new lemmas

some new results

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

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

misc tidying

declarations moved from PreList.thy

New theorems split_div' and mod_div_equality'.

Added div+mod cancelling simproc

Now arith can deal with div/mod arbitrary nat numerals.

Divides.ML -> Divides_lemmas.ML
Converted Divides.thy to Isar.

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

Changed priority of dvd from 70 to 50 as befits a relation.

many new div and mod properties (borrowed from Integ/IntDiv)

*** empty log message ***

*** empty log message ***

installing plus_ac0 for nat

replaced {{ }} by { };

new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m

now div and mod are overloaded; dvd is polymorphic

Moving div and mod from Arith to Divides
Moving dvd from ex/Primes to Divides