IsarMathLib

This theory file is an interface between the old-style Isabelle (ZF logic) material on integers and the IsarMathLib project. Here we redefine the meta-level operations on integers (addition and multiplication) to convert them to ZF-functions and show that integers form a commutative group with respect to addition and commutative monoid with respect to multiplication. Similarly, we redefine the order on integers as a relation, that is a subset of \(Z\times Z\). We show that a subset of intergers is bounded iff it is finite. As we are forced to use standard Isabelle notation with all these dollar signs, sharps etc. to denote "type coercions" (?) the notation is often ugly and difficult to read.

In this section we provide definitions of addition and multiplication as subsets of \((Z\times Z)\times Z\). We use the (higher order) relation defined in the standard Int theory to define a subset of \(Z\times Z\) that constitutes the ZF order relation corresponding to it. We define the set of positive integers using the notion of positive set from the OrderedGroup_ZF theory.

Definition of addition of integers as a binary operation on int. Recall that in standard Isabelle/ZF int is the set of integers and the sum of integers is denoted by prepending \(+\) with a dollar sign.

Definition of multiplication of integers as a binary operation on int. In standard Isabelle/ZF product of integers is denoted by prepending the dollar sign to \( * \).

Definition of natural order on integers as a relation on int. In the standard Isabelle/ZF the inequality relation on integers is denoted \( \leq \) prepended with the dollar sign.

This defines the set of positive integers.

IntegerAddition and IntegerMultiplication are functions on \( int \times int \).

The next context (locale) defines notation used for integers. We define \( 0 \) to denote the neutral element of addition, \( 1 \) as the unit of the multiplicative monoid. We introduce notation \( m\leq n \) for integers and write m..n to denote the integer interval with endpoints in \(m\) and \(n\). \( abs(m) \) means the absolute value of \(m\). This is a function defined in OrderedGroup that assigns \(x\) to itself if \(x\) is positive and assigns the opposite of \(x\) if \(x\leq 0\). Unforunately we cannot use the \(|\cdot|\) notation as in the OrderedGroup theory as this notation has been hogged by the standard Isabelle's Int theory. The notation \( -A \) where \(A\) is a subset of integers means the set \(\{-m: m\in A\}\). The symbol \( maxf(f,M) \) denotes tha maximum of function \(f\) over the set \(A\). We also introduce a similar notation for the minimum.

IntegerAddition adds integers and IntegerMultiplication multiplies integers. This states that the ZF functions IntegerAddition and IntegerMultiplication give the same results as the higher-order equivalents defined in the standard Int theory.

Integer addition and multiplication are associative.

Integer addition and multiplication are commutative.

Zero is neutral for addition and one for multiplication.

Zero is neutral for addition and one for multiplication.

Integers with addition and integers with multiplication form monoids.

Zero is the neutral element of the integers with addition and one is the neutral element of the integers with multiplication.

\(0\) and \(1\), as defined in int0 context, are integers.

Zero is not one.

The set of integers is not empty, of course.

The set of integers has more than just zero in it.

Each integer has an inverse (in the addition sense).

Integers with addition form an abelian group. This also shows that we can apply all theorems proven in the proof contexts (locales) that require the assumpion that some pair of sets form a group like locale group0.

Negative of an integer is an integer.

Taking a negative twice we get back the same integer.

What is the additive group inverse in the group of integers?

Subtracting integers corresponds to adding the negative.

Negative of zero is zero.

A trivial calculation lemma that allows to subtract and add one.

A trivial calculation lemma that allows to subtract and add one, version with ZF-operation.

Adding or subtracing one changes integers, but subtracting zero does not. .

If the difference is zero, the integers are equal.

In this section we define order on integers as a relation, that is a subset of \(Z\times Z\) and show that integers form an ordered group.

The next lemma interprets the order definition one way.

The next lemma interprets the definition the other way.

Integer order is a relation on integers.

The way we define the notion of being bounded below, its sufficient for the relation to be on integers for all bounded below sets to be subsets of integers.

The order on integers is reflexive.

A more explicit version of "integer order is reflexive" claim

The essential condition to show antisymmetry of the order on integers.

The order on integers is antisymmetric.

The essential condition to show that the order on integers is transitive.

The order on integers is transitive. This version is stated in the int0 context using notation for integers.

The order on integers is transitive.

The order on integers is a partial order.

The essential condition to show that the order on integers is preserved by translations.

Integers form a linearly ordered group. We can apply all theorems proven in group3 context to integers.

Another way of stating that we can apply theorems proven in the group3 context (defined OrderedGroup_ZF theory) to the ordered group of integers.

Negative numbers are not nonnegative. This is a special case of ls_not_leq from OrderedGroup_ZF theory.

Negative of a positive integer is negative.

Negative of a negative integer is positive.

An integer is nonnegative or negative. This is a special case of OrdGroup_2cases from OrderedGroup_ZF theory and useful for splitting proofs into cases.

Slightly weaker assertion than int_nonneg_or_neg with overlap at zero: an integer is nonnegative or nonpositive.

Another variant of splitting into cases: an integer is positive, zero or negative.

If a pair \((i,m)\) belongs to the order relation on integers and \(i\neq m\), then \(i\) is smaller that \(m\) in the sense of defined in the standard Isabelle's Int.thy.

This shows how Isabelle's \( $ \lt \) operator translates to IsarMathLib notation.

A small technical lemma about putting one on the other side of an inequality.

We can put any integer on the other side of an inequality reversing its sign.

A special case of Int_ZF_2_L9B with weaker assumptions.

Taking (higher order) minus on both sides of inequality reverses it.

Taking minus on both sides of inequality reverses it, version with a negative on one side.

We can cancel the same element on on both sides of an inequality, a version with minus on both sides.

If an integer is nonpositive, then its opposite is nonnegative.

If the opposite of an integers is nonnegative, then the integer is nonpositive.

Adding one to an integer corresponds to taking a successor for a natural number.

Adding a natural number increases integers.

Adding one increases integers.

Adding one increases integers, yet one more version.

If \(k+1 = m+n\), where \(n\) is a non-zero natural number, then \(m\leq k\).

The absolute value of an integer is an integer.

If two integers are nonnegative, then the opposite of one is less or equal than the other and the sum is also nonnegative.

We can increase components in an estimate.

We can add or subtract the sides of two inequalities.

We can increase the second component in an estimate.

If we increase the second component in a sum of three integers, the whole sum inceases.

We don't decrease an integer by adding a nonnegative one.

Some inequalities about the sum of two integers and its absolute value.

We can add a nonnegative integer to the right hand side of an inequality.

Triangle inequality for integers.

Taking absolute value does not change nonnegative integers.

\(0\leq 1\), so \(|1| = 1\).

Negative one is smaller than zero.

\(1\leq 2\).

Assume an integer is greater or equal one. Then it is greater or equal than zero, is not equal zero, if we add one to it then it is greater or equal one, two and zero. Two is .

If we add one to a nonnegative integer, the result is greater than zero.

Absolute value is the same for an integer and its opposite.

The absolute value of zero is zero.

A different version of the triangle inequality.

Another version of the triangle inequality.

Triangle inequality with three integers. We could use OrdGroup_triangle_ineq3, but since simp cannot translate the notation directly, it is simpler to reprove it for integers.

The next lemma shows what happens when one integers is not greater or equal than another.

If one integer is greater or equal and not equal to another, then it is not smaller or equal.

The next lemma allows to prove theorems for the case of positive and negative integers separately.

We can prove a theorem about integers by proving that it holds for \(m=0\), \(m\in\)\( \mathbb{Z} _+ \) and \(-m\in\)\( \mathbb{Z} _+ \).

An integer is not greater than its absolute value.

\(|m-n| = |n-m|\).

We can add the sides of inequalities with absolute values.

Absolute value is nonnegative.

If an nonnegative integer is less or equal than another, then so is its absolute value.

The standard Isabelle/ZF defined znegative predicate on integers. The next lemma expresses that in terms of the order relation on integers.

A nonnegative integer (i.e. \(0\leq z\)) is not negative in the sense of znegative predicate. We also use the opportunity to mention that such a nonnegative integer is an integer.

A nonnegative integer (i.e. one that belongs to \(\mathbb{Z}^+\)) is not negative in the sense of znegative predicate. We also use the opportunity to mention that a nonnegative integer is an integer.

A negative integer is znegative.

An integer that is not znegative is nonegative.

An integers that is not znegative is greater or equal than zero..

In this section we show some induction lemmas for integers. The basic tools are the induction on natural numbers and the fact that integers can be written as a sum of a smaller integer and a natural number.

An integer can be written a a sum of a smaller integer and a natural number.

Induction for integers, the induction step.

Induction on integers, version with higher-order increment function.

Induction on integer, implication between two forms of the induction step.

Induction on integers, version with ZF increment function.

Another form of induction on integers. This rewrites the basic theorem Int_ZF_3_L7 substituting \(P(-k)\) for \(Q(k)\).

Another induction on integers. This rewrites Int\_ZF\_3\_L7 substituting \(-k\) for \(k\) and \(-i\) for \(i\).

An implication between two forms of induction steps.

Backwards induction on integers, version with higher-order decrement function.

Induction on integers, implication between two forms of the induction step.

Backwards induction on integers.

The goal of this section is to establish that a subset of integers is bounded is and only is it is finite. The fact that all finite sets are bounded is already shown for all linearly ordered groups in OrderedGroups_ZF.thy. To show the other implication we show that all intervals starting at 0 are finite and then use a result from OrderedGroups_ZF.thy.

There are no integers between \(k\) and \(k+1\).

A trivial calculation lemma that allows to subtract and add one.

There are no integers between \(k\) and \(k+1\), another formulation.

If \(j\in m..k+1\), then \(j\in m..n\) or \(j=k+1\).

Extending an integer interval by one is the same as adding the new endpoint.

Integer intervals are finite - induction step.

Integer intervals are finite.

Bounded integer sets are finite.

A subset of integers is bounded iff it is finite.

The image of an interval by any integer function is finite, hence bounded.

If for every integer we can find one in \(A\) that is greater or equal, then \(A\) is is not bounded above, hence infinite.

In standard (informal) mathematics natural numbers form a subset of integers. In ZF that is not true as integers are defined as certain classes of pairs of natural numbers. As a result, addition on natural numbers is not a special case of addition on integers. The standard Isabelle/ZF's Int theory defines the notion of zmagnitude i.e. the magnitude of an integer. If \(z\) is an integer then \( | z|_N \) is its absolute value, interpreted as a natural number. The goal of this section is to provide facts about zmagnitude that are missing from the standard Isabelle/ZF's Int library and formulae that express addition of integers in terms of addition of their magnitudes.

The next lemma shows that zmagnitude of an integer is the same as zmagnitude of its opposite.

The magnitude of zero (the integer) is zero (the natural number) and the magnitude of one (the integer) is one (the natural number).

If \(z_1,z_1\) is a pair of integers then (at least) one of the following six cases holds: 1. Both integers are nonnegative.

2. Both integers are negative.

3. \(z_1\) is nonnegative, \(z_2\) is negative and magnitude of \(z_2\) is less or equal than magnitude of \(z_1\).

4. \(z_1\) is nonnegative, \(z_2\) is negative and magnitude of \(z_1\) is (strictly) smaller than magnitude of \(z_2\).

5. \(z_1\) is negative, \(z_2\) is nonnegative and magnitude of \(z_1\) is less or equal than magnitude of \(z_2\).

6. \(z_1\) is negative, \(z_2\) is nonnegative and magnitude of \(z_2\) is (strictly) less than magnitude of \(z_1\).

Sum of nonnegative integers in nonnegative. The magnitude of the sum of such integers is the sum of their magnitudes. We can add nonnegative integers by adding their magnitudes and converting the result to an integer. zmagnitude (defined in standard Isabelle/ZF's Int theory) is the natural number corresponding to the absolute value of an integer number.

Sum of negative integers is negative. The magnitude of the sum of such integers is the sum of their magnitudes. We can calculate the sum of negative integers by taking the sum of their magnitudes, converting that to an integer and taking negative of the result.

If \(z_1\) is a nonegative integer and \(z_2\) is a negative integer with a less or equal magnitude, then their sum is nonnegative and its magnitude is the difference between magnitudes of \(z_1\) and \(z_2\).

If \(z_1\) is a nonegative integer and \(z_2\) is a negative integer with a greater magnitude, then their sum is negative and its magnitude is the difference between magnitudes of \(z_2\) and \(z_1\).

If \(z_1\) is a negative integer and \(z_2\) is a nonnegative integer with a greater or equal magnitude, then their sum is nonnegative and its magnitude is the difference between magnitudes of \(z_2\) and \(z_1\). This is essentially add_nonneg_neg1 with \(z_1\) and \(z_2\) swapped.

If \(z_1\) is a negative integer and \(z_2\) is a nonnegative integer with a smaller magnitude, the their sum is negative and its magnitude is the difference between magnitudes of \(z_1\) and \(z_2\). This is essentially add_nonneg_neg2 with \(z_1\) and \(z_2\) swapped.