(*

This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005, 2006 Slawomir Kolodynski

This program is free software; Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,

INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A

PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,

INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT

LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR

BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,

STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE

USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

header{*\isaheader{Int\_ZF.thy}*}

theory Int_ZF_IML imports OrderedGroup_ZF_1 Finite_ZF_1 Int_ZF Nat_ZF_IML

begin;

text{*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.*}

section{*Addition and multiplication as ZF-functions.*}

text{*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

@{text "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 @{text "OrderedGroup_ZF"} theory.*}

text{*Definition of addition of integers as a binary operation

on @{text "int"}.

Recall that in standard Isabelle/ZF @{text "int"} is the set of integers

and the sum of integers is denoted by prependig $+$ with a dollar sign.*}

definition

"IntegerAddition ≡ { ⟨ x,c⟩ ∈ (int×int)×int. fst(x) $+ snd(x) = c}"

text{*Definition of multiplication of integers as a binary operation

on @{text "int"}. In standard Isabelle/ZF product of integers is denoted by

prepending the dollar sign to @{text "×"}.

*}

definition

"IntegerMultiplication ≡

{ ⟨ x,c⟩ ∈ (int×int)×int. fst(x) $× snd(x) = c}"

text{*Definition of natural order on integers as a relation on @{text "int"}.

In the standard Isabelle/ZF the inequality relation on integers

is denoted @{text "≤"} prepended with the dollar sign.*}

definition

"IntegerOrder ≡ {p ∈ int×int. fst(p) $≤ snd(p)}"

text{*This defines the set of positive integers.*}

definition

"PositiveIntegers ≡ PositiveSet(int,IntegerAddition,IntegerOrder)";

text{*IntegerAddition and IntegerMultiplication are functions on

@{text "int × int"}. *}

lemma Int_ZF_1_L1: shows

"IntegerAddition : int×int -> int"

"IntegerMultiplication : int×int -> int"

proof -

have

"{⟨ x,c⟩ ∈ (int×int)×int. fst(x) $+ snd(x) = c} ∈ int×int->int"

"{⟨ x,c⟩ ∈ (int×int)×int. fst(x) $× snd(x) = c} ∈ int×int->int"

using func1_1_L11A by auto

then show "IntegerAddition : int×int -> int"

"IntegerMultiplication : int×int -> int"

using IntegerAddition_def IntegerMultiplication_def by auto

qed;

text{*The next context (locale) defines notation used for integers.

We define @{text "\<zero>"} to denote the neutral element of addition,

@{text "\<one>"} as the

unit of the multiplicative monoid. We introduce notation @{text "m\<lsq>n"}

for integers and write @{text "m..n"} to denote the integer interval

with endpoints in $m$ and $n$.

@{text "abs(m)"} means the absolute value of $m$. This is a function

defined in @{text "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 @{text "OrderedGroup"} theory as this

notation has been hogged by the standard Isabelle's @{text "Int"} theory.

The notation @{text "\<sm>A"} where $A$ is a subset of integers means the

set $\{-m: m\in A\}$. The symbol @{text "maxf(f,M)"} denotes tha maximum

of function $f$ over the set $A$. We also introduce a similar notation

for the minimum.*}

locale int0 =

fixes ints ("\<int>")

defines ints_def [simp]: "\<int> ≡ int"

fixes ia (infixl "\<ra>" 69)

defines ia_def [simp]: "a\<ra>b ≡ IntegerAddition`⟨ a,b⟩"

fixes iminus ("\<rm> _" 72)

defines rminus_def [simp]: "\<rm>a ≡ GroupInv(\<int>,IntegerAddition)`(a)"

fixes isub (infixl "\<rs>" 69)

defines isub_def [simp]: "a\<rs>b ≡ a\<ra> (\<rm> b)"

fixes imult (infixl "·" 70)

defines imult_def [simp]: "a·b ≡ IntegerMultiplication`⟨ a,b⟩"

fixes setneg ("\<sm> _" 72)

defines setneg_def [simp]: "\<sm>A ≡ GroupInv(\<int>,IntegerAddition)``(A)"

fixes izero ("\<zero>")

defines izero_def [simp]: "\<zero> ≡ TheNeutralElement(\<int>,IntegerAddition)"

fixes ione ("\<one>")

defines ione_def [simp]: "\<one> ≡ TheNeutralElement(\<int>,IntegerMultiplication)"

fixes itwo ("\<two>")

defines itwo_def [simp]: "\<two> ≡ \<one>\<ra>\<one>"

fixes ithree ("\<three>")

defines ithree_def [simp]: "\<three> ≡ \<two>\<ra>\<one>"

fixes nonnegative ("\<int>⇧^{+}")

defines nonnegative_def [simp]:

"\<int>⇧^{+}≡ Nonnegative(\<int>,IntegerAddition,IntegerOrder)"

fixes positive ("\<int>⇩_{+}")

defines positive_def [simp]:

"\<int>⇩_{+}≡ PositiveSet(\<int>,IntegerAddition,IntegerOrder)"

fixes abs

defines abs_def [simp]:

"abs(m) ≡ AbsoluteValue(\<int>,IntegerAddition,IntegerOrder)`(m)"

fixes lesseq (infix "\<lsq>" 60)

defines lesseq_def [simp]: "m \<lsq> n ≡ ⟨m,n⟩ ∈ IntegerOrder"

fixes interval (infix ".." 70)

defines interval_def [simp]: "m..n ≡ Interval(IntegerOrder,m,n)"

fixes maxf

defines maxf_def [simp]: "maxf(f,A) ≡ Maximum(IntegerOrder,f``(A))"

fixes minf

defines minf_def [simp]: "minf(f,A) ≡ Minimum(IntegerOrder,f``(A))";

text{*IntegerAddition adds integers and IntegerMultiplication multiplies

integers. This states that the ZF functions @{text "IntegerAddition"} and

@{text "IntegerMultiplication"} give the same results as the higher-order

equivalents defined in the standard @{text "Int"} theory.*}

lemma (in int0) Int_ZF_1_L2: assumes A1: "a ∈ \<int>" "b ∈ \<int>"

shows

"a\<ra>b = a $+ b"

"a·b = a $× b"

proof -

let ?x = "⟨ a,b⟩"

let ?c = "a $+ b"

let ?d = "a $× b"

from A1 have

"⟨ ?x,?c⟩ ∈ {⟨ x,c⟩ ∈ (\<int>×\<int>)×\<int>. fst(x) $+ snd(x) = c}"

"⟨ ?x,?d⟩ ∈ {⟨ x,d⟩ ∈ (\<int>×\<int>)×\<int>. fst(x) $× snd(x) = d}"

by auto;

then show "a\<ra>b = a $+ b" "a·b = a $× b"

using IntegerAddition_def IntegerMultiplication_def

Int_ZF_1_L1 apply_iff by auto;

qed;

text{*Integer addition and multiplication are associative.*}

lemma (in int0) Int_ZF_1_L3:

assumes "x∈\<int>" "y∈\<int>" "z∈\<int>"

shows "x\<ra>y\<ra>z = x\<ra>(y\<ra>z)" "x·y·z = x·(y·z)"

using assms Int_ZF_1_L2 zadd_assoc zmult_assoc by auto;

text{*Integer addition and multiplication are commutative.*}

lemma (in int0) Int_ZF_1_L4:

assumes "x∈\<int>" "y∈\<int>"

shows "x\<ra>y = y\<ra>x" "x·y = y·x"

using assms Int_ZF_1_L2 zadd_commute zmult_commute

by auto;

text{*Zero is neutral for addition and one for multiplication.*}

lemma (in int0) Int_ZF_1_L5: assumes A1:"x∈\<int>"

shows "($# 0) \<ra> x = x ∧ x \<ra> ($# 0) = x"

"($# 1)·x = x ∧ x·($# 1) = x"

proof -

from A1 show "($# 0) \<ra> x = x ∧ x \<ra> ($# 0) = x"

using Int_ZF_1_L2 zadd_int0 Int_ZF_1_L4 by simp;

from A1 have "($# 1)·x = x"

using Int_ZF_1_L2 zmult_int1 by simp;

with A1 show "($# 1)·x = x ∧ x·($# 1) = x"

using Int_ZF_1_L4 by simp;

qed;

text{*Zero is neutral for addition and one for multiplication.*}

lemma (in int0) Int_ZF_1_L6: shows "($# 0)∈\<int> ∧

(∀x∈\<int>. ($# 0)\<ra>x = x ∧ x\<ra>($# 0) = x)"

"($# 1)∈\<int> ∧

(∀x∈\<int>. ($# 1)·x = x ∧ x·($# 1) = x)"

using Int_ZF_1_L5 by auto;

text{*Integers with addition and integers with multiplication

form monoids.*}

theorem (in int0) Int_ZF_1_T1: shows

"IsAmonoid(\<int>,IntegerAddition)"

"IsAmonoid(\<int>,IntegerMultiplication)"

proof -

have

"∃e∈\<int>. ∀x∈\<int>. e\<ra>x = x ∧ x\<ra>e = x"

"∃e∈\<int>. ∀x∈\<int>. e·x = x ∧ x·e = x"

using int0.Int_ZF_1_L6 by auto;

then show "IsAmonoid(\<int>,IntegerAddition)"

"IsAmonoid(\<int>,IntegerMultiplication)" using

IsAmonoid_def IsAssociative_def Int_ZF_1_L1 Int_ZF_1_L3

by auto;

qed;

text{*Zero is the neutral element of the integers with addition

and one is the neutral element of the integers with multiplication.*}

lemma (in int0) Int_ZF_1_L8: shows "($# 0) = \<zero>" "($# 1) = \<one>"

proof -;

have "monoid0(\<int>,IntegerAddition)"

using Int_ZF_1_T1 monoid0_def by simp;

moreover have

"($# 0)∈\<int> ∧

(∀x∈\<int>. IntegerAddition`⟨$# 0,x⟩ = x ∧

IntegerAddition`⟨x ,$# 0⟩ = x)"

using Int_ZF_1_L6 by auto;

ultimately have "($# 0) = TheNeutralElement(\<int>,IntegerAddition)"

by (rule monoid0.group0_1_L4);

then show "($# 0) = \<zero>" by simp;

have "monoid0(int,IntegerMultiplication)"

using Int_ZF_1_T1 monoid0_def by simp;

moreover have "($# 1) ∈ int ∧

(∀x∈int. IntegerMultiplication`⟨$# 1, x⟩ = x ∧

IntegerMultiplication`⟨x ,$# 1⟩ = x)"

using Int_ZF_1_L6 by auto;

ultimately have

"($# 1) = TheNeutralElement(int,IntegerMultiplication)"

by (rule monoid0.group0_1_L4)

then show "($# 1) = \<one>" by simp;

qed;

text{* $0$ and $1$, as defined in @{text "int0"} context, are integers.*}

lemma (in int0) Int_ZF_1_L8A: shows "\<zero> ∈ \<int>" "\<one> ∈ \<int>"

proof -

have "($# 0) ∈ \<int>" "($# 1) ∈ \<int>" by auto

then show "\<zero> ∈ \<int>" "\<one> ∈ \<int>" using Int_ZF_1_L8 by auto;

qed;

text{*Zero is not one.*}

lemma (in int0) int_zero_not_one: shows "\<zero> ≠ \<one>"

proof -

have "($# 0) ≠ ($# 1)" by simp

then show "\<zero> ≠ \<one>" using Int_ZF_1_L8 by simp;

qed;

text{*The set of integers is not empty, of course.*}

lemma (in int0) int_not_empty: shows "\<int> ≠ 0"

using Int_ZF_1_L8A by auto;

text{*The set of integers has more than just zero in it.*}

lemma (in int0) int_not_trivial: shows "\<int> ≠ {\<zero>}"

using Int_ZF_1_L8A int_zero_not_one by blast;

text{*Each integer has an inverse (in the addition sense).*}

lemma (in int0) Int_ZF_1_L9: assumes A1: "g ∈ \<int>"

shows "∃ b∈\<int>. g\<ra>b = \<zero>"

proof -

from A1 have "g\<ra> $-g = \<zero>"

using Int_ZF_1_L2 Int_ZF_1_L8 by simp;

thus ?thesis by auto;

qed;

text{*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 @{text "group0"}.*}

theorem Int_ZF_1_T2: shows

"IsAgroup(int,IntegerAddition)"

"IntegerAddition {is commutative on} int"

"group0(int,IntegerAddition)"

using int0.Int_ZF_1_T1 int0.Int_ZF_1_L9 IsAgroup_def

group0_def int0.Int_ZF_1_L4 IsCommutative_def by auto;

text{*What is the additive group inverse in the group of integers?*}

lemma (in int0) Int_ZF_1_L9A: assumes A1: "m∈\<int>"

shows "$-m = \<rm>m"

proof -;

from A1 have "m∈int" "$-m ∈ int" "IntegerAddition`⟨ m,$-m⟩ =

TheNeutralElement(int,IntegerAddition)"

using zminus_type Int_ZF_1_L2 Int_ZF_1_L8 by auto;

then have "$-m = GroupInv(int,IntegerAddition)`(m)"

using Int_ZF_1_T2 group0.group0_2_L9 by blast;

then show ?thesis by simp;

qed;

text{*Subtracting integers corresponds to adding the negative.*}

lemma (in int0) Int_ZF_1_L10: assumes A1: "m∈\<int>" "n∈\<int>"

shows "m\<rs>n = m $+ $-n"

using assms Int_ZF_1_T2 group0.inverse_in_group Int_ZF_1_L9A Int_ZF_1_L2

by simp;

text{*Negative of zero is zero.*}

lemma (in int0) Int_ZF_1_L11: shows "(\<rm>\<zero>) = \<zero>"

using Int_ZF_1_T2 group0.group_inv_of_one by simp;

text{*A trivial calculation lemma that allows to subtract and add one. *}

lemma Int_ZF_1_L12:

assumes "m∈int" shows "m $- $#1 $+ $#1 = m"

using assms eq_zdiff_iff by auto;

text{*A trivial calculation lemma that allows to subtract and add one,

version with ZF-operation.*}

lemma (in int0) Int_ZF_1_L13: assumes "m∈\<int>"

shows "(m $- $#1) \<ra> \<one> = m"

using assms Int_ZF_1_L8A Int_ZF_1_L2 Int_ZF_1_L8 Int_ZF_1_L12

by simp;

text{*Adding or subtracing one changes integers.*}

lemma (in int0) Int_ZF_1_L14: assumes A1: "m∈\<int>"

shows

"m\<ra>\<one> ≠ m"

"m\<rs>\<one> ≠ m"

proof -

{ assume "m\<ra>\<one> = m"

with A1 have

"group0(\<int>,IntegerAddition)"

"m∈\<int>" "\<one>∈\<int>"

"IntegerAddition`⟨m,\<one>⟩ = m"

using Int_ZF_1_T2 Int_ZF_1_L8A by auto;

then have "\<one> = TheNeutralElement(\<int>,IntegerAddition)"

by (rule group0.group0_2_L7);

then have False using int_zero_not_one by simp;

} then show I: "m\<ra>\<one> ≠ m" by auto;

{ from A1 have "m \<rs> \<one> \<ra> \<one> = m"

using Int_ZF_1_L8A Int_ZF_1_T2 group0.inv_cancel_two

by simp;

moreover assume "m\<rs>\<one> = m"

ultimately have "m \<ra> \<one> = m" by simp;

with I have False by simp;

} then show "m\<rs>\<one> ≠ m" by auto;

qed;

text{*If the difference is zero, the integers are equal.*}

lemma (in int0) Int_ZF_1_L15:

assumes A1: "m∈\<int>" "n∈\<int>" and A2: "m\<rs>n = \<zero>"

shows "m=n"

proof -

let ?G = "\<int>"

let ?f = "IntegerAddition"

from A1 A2 have

"group0(?G, ?f)"

"m ∈ ?G" "n ∈ ?G"

"?f`⟨m, GroupInv(?G, ?f)`(n)⟩ = TheNeutralElement(?G, ?f)"

using Int_ZF_1_T2 by auto;

then show "m=n" by (rule group0.group0_2_L11A);

qed;

section{*Integers as an ordered group*}

text{*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.*}

text{*The next lemma interprets the order definition one way. *}

lemma (in int0) Int_ZF_2_L1:

assumes A1: "m∈\<int>" "n∈\<int>" and A2: "m $≤ n"

shows "m \<lsq> n"

proof -

from A1 A2 have "⟨ m,n⟩ ∈ {x∈\<int>×\<int>. fst(x) $≤ snd(x)}"

by simp;

then show ?thesis using IntegerOrder_def by simp;

qed;

text{*The next lemma interprets the definition the other way. *}

lemma (in int0) Int_ZF_2_L1A: assumes A1: "m \<lsq> n"

shows "m $≤ n" "m∈\<int>" "n∈\<int>"

proof -;

from A1 have "⟨ m,n⟩ ∈ {p∈\<int>×\<int>. fst(p) $≤ snd(p)}"

using IntegerOrder_def by simp;

thus "m $≤ n" "m∈\<int>" "n∈\<int>" by auto;

qed;

text{*Integer order is a relation on integers.*}

lemma Int_ZF_2_L1B: shows "IntegerOrder ⊆ int×int"

proof;

fix x assume "x∈IntegerOrder"

then have "x ∈ {p∈int×int. fst(p) $≤ snd(p)}"

using IntegerOrder_def by simp;

then show "x∈int×int" by simp;

qed;

text{*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.*}

lemma (in int0) Int_ZF_2_L1C:

assumes A1: "IsBoundedBelow(A,IntegerOrder)"

shows "A⊆\<int>"

proof -

from A1 have

"IntegerOrder ⊆ \<int>×\<int>"

"IsBoundedBelow(A,IntegerOrder)"

using Int_ZF_2_L1B by auto;

then show "A⊆\<int>" by (rule Order_ZF_3_L1B);

qed;

text{* The order on integers is reflexive.*}

lemma (in int0) int_ord_is_refl: shows "refl(\<int>,IntegerOrder)"

using Int_ZF_2_L1 zle_refl refl_def by auto;

text{*The essential condition to show antisymmetry of the order on integers.*}

lemma (in int0) Int_ZF_2_L3:

assumes A1: "m \<lsq> n" "n \<lsq> m"

shows "m=n"

proof -;

from A1 have "m $≤ n" "n $≤ m" "m∈\<int>" "n∈\<int>"

using Int_ZF_2_L1A by auto;

then show "m=n" using zle_anti_sym by auto;

qed;

text{*The order on integers is antisymmetric.*}

lemma (in int0) Int_ZF_2_L4: shows "antisym(IntegerOrder)"

proof -

have "∀m n. m \<lsq> n ∧ n \<lsq> m --> m=n"

using Int_ZF_2_L3 by auto;

then show ?thesis using imp_conj antisym_def by simp;

qed;

text{*The essential condition to show that the order on integers is

transitive.*}

lemma Int_ZF_2_L5:

assumes A1: "⟨m,n⟩ ∈ IntegerOrder" "⟨n,k⟩ ∈ IntegerOrder"

shows "⟨m,k⟩ ∈ IntegerOrder"

proof -;

from A1 have T1: "m $≤ n" "n $≤ k" and T2: "m∈int" "k∈int"

using int0.Int_ZF_2_L1A by auto;

from T1 have "m $≤ k" by (rule zle_trans);

with T2 show ?thesis using int0.Int_ZF_2_L1 by simp;

qed;

text{*The order on integers is

transitive. This version is stated in the @{text "int0"} context

using notation for integers.*}

lemma (in int0) Int_order_transitive:

assumes A1: "m\<lsq>n" "n\<lsq>k"

shows "m\<lsq>k"

proof -

from A1 have "⟨ m,n⟩ ∈ IntegerOrder" "⟨ n,k⟩ ∈ IntegerOrder"

by auto

then have "⟨ m,k⟩ ∈ IntegerOrder" by (rule Int_ZF_2_L5)

then show "m\<lsq>k" by simp;

qed;

text{*The order on integers is transitive.*}

lemma Int_ZF_2_L6: shows "trans(IntegerOrder)"

proof -;

have "∀ m n k.

⟨m, n⟩ ∈ IntegerOrder ∧ ⟨n, k⟩ ∈ IntegerOrder -->

⟨m, k⟩ ∈ IntegerOrder"

using Int_ZF_2_L5 by blast;

then show ?thesis by (rule Fol1_L2);

qed;

text{*The order on integers is a partial order.*}

lemma Int_ZF_2_L7: shows "IsPartOrder(int,IntegerOrder)"

using int0.int_ord_is_refl int0.Int_ZF_2_L4

Int_ZF_2_L6 IsPartOrder_def by simp;

text{*The essential condition to show that the order on integers is

preserved by translations. *}

lemma (in int0) int_ord_transl_inv:

assumes A1: "k ∈ \<int>" and A2: "m \<lsq> n"

shows "m\<ra>k \<lsq> n\<ra>k " "k\<ra>m\<lsq> k\<ra>n "

proof -;

from A2 have "m $≤ n" and "m∈\<int>" "n∈\<int>"

using Int_ZF_2_L1A by auto;

with A1 show "m\<ra>k \<lsq> n\<ra>k " "k\<ra>m\<lsq> k\<ra>n "

using zadd_right_cancel_zle zadd_left_cancel_zle

Int_ZF_1_L2 Int_ZF_1_L1 apply_funtype

Int_ZF_1_L2 Int_ZF_2_L1 Int_ZF_1_L2 by auto;

qed;

text{*Integers form a linearly ordered group. We can apply all theorems

proven in group3 context to integers. *}

theorem (in int0) Int_ZF_2_T1: shows

"IsAnOrdGroup(\<int>,IntegerAddition,IntegerOrder)"

"IntegerOrder {is total on} \<int>"

"group3(\<int>,IntegerAddition,IntegerOrder)"

"IsLinOrder(\<int>,IntegerOrder)"

proof -;

have "∀k∈\<int>. ∀m n. m \<lsq> n -->

m\<ra>k \<lsq> n\<ra>k ∧ k\<ra>m\<lsq> k\<ra>n"

using int_ord_transl_inv by simp;

then show T1: "IsAnOrdGroup(\<int>,IntegerAddition,IntegerOrder)" using

Int_ZF_1_T2 Int_ZF_2_L1B Int_ZF_2_L7 IsAnOrdGroup_def

by simp;

then show "group3(\<int>,IntegerAddition,IntegerOrder)"

using group3_def by simp;

have "∀n∈\<int>. ∀m∈\<int>. n\<lsq>m ∨ m\<lsq>n"

using zle_linear Int_ZF_2_L1 by auto;

then show "IntegerOrder {is total on} \<int>"

using IsTotal_def by simp;

with T1 show "IsLinOrder(\<int>,IntegerOrder)"

using IsAnOrdGroup_def IsPartOrder_def IsLinOrder_def by simp;

qed;

text{*If a pair $(i,m)$ belongs to the order relation on integers and

$i\neq m$, then $i<m$ in the sense of defined in the standard Isabelle's

Int.thy.*}

lemma (in int0) Int_ZF_2_L9: assumes A1: "i \<lsq> m" and A2: "i≠m"

shows "i $< m"

proof -;

from A1 have "i $≤ m" "i∈\<int>" "m∈\<int>"

using Int_ZF_2_L1A by auto;

with A2 show "i $< m" using zle_def by simp;

qed;

text{*This shows how Isabelle's @{text "$<"} operator translates to IsarMathLib

notation.*}

lemma (in int0) Int_ZF_2_L9AA: assumes A1: "m∈\<int>" "n∈\<int>"

and A2: "m $< n"

shows "m\<lsq>n" "m ≠ n"

using assms zle_def Int_ZF_2_L1 by auto;

text{*A small technical lemma about putting one on the other side

of an inequality.*}

lemma (in int0) Int_ZF_2_L9A:

assumes A1: "k∈\<int>" and A2: "m \<lsq> k $- ($# 1)"

shows "m\<ra>\<one> \<lsq> k"

proof -

from A2 have "m\<ra>\<one> \<lsq> (k $- ($# 1)) \<ra> \<one>"

using Int_ZF_1_L8A int_ord_transl_inv by simp;

with A1 show "m\<ra>\<one> \<lsq> k"

using Int_ZF_1_L13 by simp;

qed;

text{*We can put any integer on the other side of an inequality reversing

its sign.*}

lemma (in int0) Int_ZF_2_L9B: assumes "i∈\<int>" "m∈\<int>" "k∈\<int>"

shows "i\<ra>m \<lsq> k <-> i \<lsq> k\<rs>m"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L9A

by simp;

text{*A special case of @{text "Int_ZF_2_L9B"} with weaker assumptions.*}

lemma (in int0) Int_ZF_2_L9C:

assumes "i∈\<int>" "m∈\<int>" and "i\<rs>m \<lsq> k"

shows "i \<lsq> k\<ra>m"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L9B

by simp;

text{*Taking (higher order) minus on both sides of inequality reverses it.*}

lemma (in int0) Int_ZF_2_L10: assumes "k \<lsq> i"

shows

"(\<rm>i) \<lsq> (\<rm>k)"

"$-i \<lsq> $-k"

using assms Int_ZF_2_L1A Int_ZF_1_L9A Int_ZF_2_T1

group3.OrderedGroup_ZF_1_L5 by auto;

text{*Taking minus on both sides of inequality reverses it,

version with a negative on one side.*}

lemma (in int0) Int_ZF_2_L10AA: assumes "n∈\<int>" "m\<lsq>(\<rm>n)"

shows "n\<lsq>(\<rm>m)"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5AD

by simp;

text{*We can cancel the same element on on both sides of an inequality,

a version with minus on both sides.*}

lemma (in int0) Int_ZF_2_L10AB:

assumes "m∈\<int>" "n∈\<int>" "k∈\<int>" and "m\<rs>n \<lsq> m\<rs>k"

shows "k\<lsq>n"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5AF

by simp;

text{*If an integer is nonpositive, then its opposite is nonnegative.*}

lemma (in int0) Int_ZF_2_L10A: assumes "k \<lsq> \<zero>"

shows "\<zero>\<lsq>(\<rm>k)"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5A by simp;

text{*If the opposite of an integers is nonnegative, then the integer

is nonpositive.*}

lemma (in int0) Int_ZF_2_L10B:

assumes "k∈\<int>" and "\<zero>\<lsq>(\<rm>k)"

shows "k\<lsq>\<zero>"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5AA by simp;

text{*Adding one to an integer corresponds to taking a successor for a natural

number.*}

lemma (in int0) Int_ZF_2_L11:

shows "i $+ $# n $+ ($# 1) = i $+ $# succ(n)"

proof -

have "$# succ(n) = $#1 $+ $# n" using int_succ_int_1 by blast;

then have "i $+ $# succ(n) = i $+ ($# n $+ $#1)"

using zadd_commute by simp;

then show ?thesis using zadd_assoc by simp;

qed;

text{*Adding a natural number increases integers.*}

lemma (in int0) Int_ZF_2_L12: assumes A1: "i∈\<int>" and A2: "n∈nat"

shows "i \<lsq> i $+ $#n"

proof -

{ assume "n = 0"

with A1 have "i \<lsq> i $+ $#n" using zadd_int0 int_ord_is_refl refl_def

by simp }

moreover

{ assume "n≠0"

with A2 obtain k where "k∈nat" "n = succ(k)"

using Nat_ZF_1_L3 by auto;

with A1 have "i \<lsq> i $+ $#n"

using zless_succ_zadd zless_imp_zle Int_ZF_2_L1 by simp }

ultimately show ?thesis by blast

qed;

text{*Adding one increases integers.*}

lemma (in int0) Int_ZF_2_L12A: assumes A1: "j\<lsq>k"

shows "j \<lsq> k $+ $#1" "j \<lsq> k\<ra>\<one>"

proof -;

from A1 have T1:"j∈\<int>" "k∈\<int>" "j $≤ k"

using Int_ZF_2_L1A by auto;

moreover from T1 have "k $≤ k $+ $#1" using Int_ZF_2_L12 Int_ZF_2_L1A

by simp;

ultimately have "j $≤ k $+ $#1" using zle_trans by fast;

with T1 show "j \<lsq> k $+ $#1" using Int_ZF_2_L1 by simp;

with T1 have "j\<lsq> k\<ra>$#1"

using Int_ZF_1_L2 by simp;

then show "j \<lsq> k\<ra>\<one>" using Int_ZF_1_L8 by simp;

qed;

text{*Adding one increases integers, yet one more version.*}

lemma (in int0) Int_ZF_2_L12B: assumes A1: "m∈\<int>" shows "m \<lsq> m\<ra>\<one>"

using assms int_ord_is_refl refl_def Int_ZF_2_L12A by simp;

text{*If $k+1 = m+n$, where $n$ is a non-zero natural number, then

$m\leq k$. *}

lemma (in int0) Int_ZF_2_L13:

assumes A1: "k∈\<int>" "m∈\<int>" and A2: "n∈nat"

and A3: "k $+ ($# 1) = m $+ $# succ(n)"

shows "m \<lsq> k"

proof -;

from A1 have "k∈\<int>" "m $+ $# n ∈ \<int>" by auto;

moreover from assms have "k $+ $# 1 = m $+ $# n $+ $#1"

using Int_ZF_2_L11 by simp;

ultimately have "k = m $+ $# n" using zadd_right_cancel by simp;

with A1 A2 show ?thesis using Int_ZF_2_L12 by simp;

qed;

text{*The absolute value of an integer is an integer.*}

lemma (in int0) Int_ZF_2_L14: assumes A1: "m∈\<int>"

shows "abs(m) ∈ \<int>"

proof -;

have "AbsoluteValue(\<int>,IntegerAddition,IntegerOrder) : \<int>->\<int>"

using Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L1 by simp;

with A1 show ?thesis using apply_funtype by simp;

qed;

text{*If two integers are nonnegative, then the opposite

of one is less or equal than the other and the sum is also nonnegative.*}

lemma (in int0) Int_ZF_2_L14A:

assumes "\<zero>\<lsq>m" "\<zero>\<lsq>n"

shows

"(\<rm>m) \<lsq> n"

"\<zero> \<lsq> m \<ra> n"

using assms Int_ZF_2_T1

group3.OrderedGroup_ZF_1_L5AC group3.OrderedGroup_ZF_1_L12

by auto;

text{*We can increase components in an estimate.*}

lemma (in int0) Int_ZF_2_L15:

assumes "b\<lsq>b⇩_{1}" "c\<lsq>c⇩_{1}" and "a\<lsq>b\<ra>c"

shows "a\<lsq>b⇩_{1}\<ra>c⇩_{1}"

proof -

from assms have "group3(\<int>,IntegerAddition,IntegerOrder)"

"⟨a,IntegerAddition`⟨ b,c⟩⟩ ∈ IntegerOrder"

"⟨b,b⇩_{1}⟩ ∈ IntegerOrder" "⟨c,c⇩_{1}⟩ ∈ IntegerOrder"

using Int_ZF_2_T1 by auto

then have "⟨a,IntegerAddition`⟨ b⇩_{1},c⇩_{1}⟩⟩ ∈ IntegerOrder"

by (rule group3.OrderedGroup_ZF_1_L5E);

thus ?thesis by simp;

qed;

text{*We can add or subtract the sides of two inequalities.*}

lemma (in int0) int_ineq_add_sides:

assumes "a\<lsq>b" and "c\<lsq>d"

shows

"a\<ra>c \<lsq> b\<ra>d"

"a\<rs>d \<lsq> b\<rs>c"

using assms Int_ZF_2_T1

group3.OrderedGroup_ZF_1_L5B group3.OrderedGroup_ZF_1_L5I

by auto;

text{*We can increase the second component in an estimate.*}

lemma (in int0) Int_ZF_2_L15A:

assumes "b∈\<int>" and "a\<lsq>b\<ra>c" and A3: "c\<lsq>c⇩_{1}"

shows "a\<lsq>b\<ra>c⇩_{1}"

proof -

from assms have

"group3(\<int>,IntegerAddition,IntegerOrder)"

"b ∈ \<int>"

"⟨a,IntegerAddition`⟨ b,c⟩⟩ ∈ IntegerOrder"

"⟨c,c⇩_{1}⟩ ∈ IntegerOrder"

using Int_ZF_2_T1 by auto;

then have "⟨a,IntegerAddition`⟨ b,c⇩_{1}⟩⟩ ∈ IntegerOrder"

by (rule group3.OrderedGroup_ZF_1_L5D);

thus ?thesis by simp;

qed;

text{*If we increase the second component in a sum of three

integers, the whole sum inceases.*}

lemma (in int0) Int_ZF_2_L15C:

assumes A1: "m∈\<int>" "n∈\<int>" and A2: "k \<lsq> L"

shows "m\<ra>k\<ra>n \<lsq> m\<ra>L\<ra>n"

proof -

let ?P = "IntegerAddition"

from assms have

"group3(int,?P,IntegerOrder)"

"m ∈ int" "n ∈ int"

"⟨k,L⟩ ∈ IntegerOrder"

using Int_ZF_2_T1 by auto;

then have "⟨?P`⟨?P`⟨ m,k⟩,n⟩, ?P`⟨?P`⟨ m,L⟩,n⟩ ⟩ ∈ IntegerOrder"

by (rule group3.OrderedGroup_ZF_1_L10);

then show "m\<ra>k\<ra>n \<lsq> m\<ra>L\<ra>n" by simp;

qed;

text{*We don't decrease an integer by adding a nonnegative one.*}

lemma (in int0) Int_ZF_2_L15D:

assumes "\<zero>\<lsq>n" "m∈\<int>"

shows "m \<lsq> n\<ra>m"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5F

by simp;

text{*Some inequalities about the sum of two integers

and its absolute value.*}

lemma (in int0) Int_ZF_2_L15E:

assumes "m∈\<int>" "n∈\<int>"

shows

"m\<ra>n \<lsq> abs(m)\<ra>abs(n)"

"m\<rs>n \<lsq> abs(m)\<ra>abs(n)"

"(\<rm>m)\<ra>n \<lsq> abs(m)\<ra>abs(n)"

"(\<rm>m)\<rs>n \<lsq> abs(m)\<ra>abs(n)"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L6A

by auto;

text{*We can add a nonnegative

integer to the right hand side of an inequality.*}

lemma (in int0) Int_ZF_2_L15F: assumes "m\<lsq>k" and "\<zero>\<lsq>n"

shows "m \<lsq> k\<ra>n" "m \<lsq> n\<ra>k"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5G

by auto;

text{*Triangle inequality for integers.*}

lemma (in int0) Int_triangle_ineq:

assumes "m∈\<int>" "n∈\<int>"

shows "abs(m\<ra>n)\<lsq>abs(m)\<ra>abs(n)"

using assms Int_ZF_1_T2 Int_ZF_2_T1 group3.OrdGroup_triangle_ineq

by simp;

text{*Taking absolute value does not change nonnegative integers.*}

lemma (in int0) Int_ZF_2_L16:

assumes "\<zero>\<lsq>m" shows "m∈\<int>⇧^{+}" and "abs(m) = m"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L2

group3.OrderedGroup_ZF_3_L2 by auto;

text{*$0\leq 1$, so $|1| = 1$.*}

lemma (in int0) Int_ZF_2_L16A: shows "\<zero>\<lsq>\<one>" and "abs(\<one>) = \<one>"

proof -

have "($# 0) ∈ \<int>" "($# 1)∈ \<int>" by auto

then have "\<zero>\<lsq>\<zero>" and T1: "\<one>∈\<int>"

using Int_ZF_1_L8 int_ord_is_refl refl_def by auto;

then have "\<zero>\<lsq>\<zero>\<ra>\<one>" using Int_ZF_2_L12A by simp;

with T1 show "\<zero>\<lsq>\<one>" using Int_ZF_1_T2 group0.group0_2_L2

by simp;

then show "abs(\<one>) = \<one>" using Int_ZF_2_L16 by simp

qed;

text{*$1\leq 2$.*}

lemma (in int0) Int_ZF_2_L16B: shows "\<one>\<lsq>\<two>"

proof -

have "($# 1)∈ \<int>" by simp

then show "\<one>\<lsq>\<two>"

using Int_ZF_1_L8 int_ord_is_refl refl_def Int_ZF_2_L12A

by simp;

qed;

text{*Integers greater or equal one are greater or equal zero.*}

lemma (in int0) Int_ZF_2_L16C:

assumes A1: "\<one>\<lsq>a" shows

"\<zero>\<lsq>a" "a≠\<zero>"

"\<two> \<lsq> a\<ra>\<one>"

"\<one> \<lsq> a\<ra>\<one>"

"\<zero> \<lsq> a\<ra>\<one>"

proof -

from A1 have "\<zero>\<lsq>\<one>" and "\<one>\<lsq>a"

using Int_ZF_2_L16A by auto

then show "\<zero>\<lsq>a" by (rule Int_order_transitive);

have I: "\<zero>\<lsq>\<one>" using Int_ZF_2_L16A by simp;

have "\<one>\<lsq>\<two>" using Int_ZF_2_L16B by simp;

moreover from A1 show "\<two> \<lsq> a\<ra>\<one>"

using Int_ZF_1_L8A int_ord_transl_inv by simp;

ultimately show "\<one> \<lsq> a\<ra>\<one>" by (rule Int_order_transitive);

with I show "\<zero> \<lsq> a\<ra>\<one>" by (rule Int_order_transitive);

from A1 show "a≠\<zero>" using

Int_ZF_2_L16A Int_ZF_2_L3 int_zero_not_one by auto;

qed;

text{*Absolute value is the same for an integer and its opposite.*}

lemma (in int0) Int_ZF_2_L17:

assumes "m∈\<int>" shows "abs(\<rm>m) = abs(m)"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L7A by simp;

text{*The absolute value of zero is zero.*}

lemma (in int0) Int_ZF_2_L18: shows "abs(\<zero>) = \<zero>"

using Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L2A by simp;

text{*A different version of the triangle inequality.*}

lemma (in int0) Int_triangle_ineq1:

assumes A1: "m∈\<int>" "n∈\<int>"

shows

"abs(m\<rs>n) \<lsq> abs(n)\<ra>abs(m)"

"abs(m\<rs>n) \<lsq> abs(m)\<ra>abs(n)"

proof -;

have "$-n ∈ \<int>" by simp;

with A1 have "abs(m\<rs>n) \<lsq> abs(m)\<ra>abs(\<rm>n)"

using Int_ZF_1_L9A Int_triangle_ineq by simp;

with A1 show

"abs(m\<rs>n) \<lsq> abs(n)\<ra>abs(m)"

"abs(m\<rs>n) \<lsq> abs(m)\<ra>abs(n)"

using Int_ZF_2_L17 Int_ZF_2_L14 Int_ZF_1_T2 IsCommutative_def

by auto

qed;

text{*Another version of the triangle inequality.*}

lemma (in int0) Int_triangle_ineq2:

assumes "m∈\<int>" "n∈\<int>"

and "abs(m\<rs>n) \<lsq> k"

shows

"abs(m) \<lsq> abs(n)\<ra>k"

"m\<rs>k \<lsq> n"

"m \<lsq> n\<ra>k"

"n\<rs>k \<lsq> m"

using assms Int_ZF_1_T2 Int_ZF_2_T1

group3.OrderedGroup_ZF_3_L7D group3.OrderedGroup_ZF_3_L7E

by auto;

text{*Triangle inequality with three integers. We could use

@{text "OrdGroup_triangle_ineq3"}, but since simp cannot translate

the notation directly, it is simpler to reprove it for integers.*}

lemma (in int0) Int_triangle_ineq3:

assumes A1: "m∈\<int>" "n∈\<int>" "k∈\<int>"

shows "abs(m\<ra>n\<ra>k) \<lsq> abs(m)\<ra>abs(n)\<ra>abs(k)"

proof -

from A1 have T: "m\<ra>n ∈ \<int>" "abs(k) ∈ \<int>"

using Int_ZF_1_T2 group0.group_op_closed Int_ZF_2_L14

by auto;

with A1 have "abs(m\<ra>n\<ra>k) \<lsq> abs(m\<ra>n) \<ra> abs(k)"

using Int_triangle_ineq by simp;

moreover from A1 T have

"abs(m\<ra>n) \<ra> abs(k) \<lsq> abs(m) \<ra> abs(n) \<ra> abs(k)"

using Int_triangle_ineq int_ord_transl_inv by simp;

ultimately show ?thesis by (rule Int_order_transitive);

qed;

text{*The next lemma shows what happens when one integers is not

greater or equal than another.*}

(* trying to use OrderedGroup_ZF_1_L8 results in a longer proof,

simp and auto loop here*)

lemma (in int0) Int_ZF_2_L19:

assumes A1: "m∈\<int>" "n∈\<int>" and A2: "¬(n\<lsq>m)"

shows "m\<lsq>n" "(\<rm>n) \<lsq> (\<rm>m)" "m≠n"

proof -

from A1 A2 show "m\<lsq>n" using Int_ZF_2_T1 IsTotal_def

by auto;

then show "(\<rm>n) \<lsq> (\<rm>m)" using Int_ZF_2_L10

by simp;

from A1 have "n \<lsq> n" using int_ord_is_refl refl_def

by simp;

with A2 show "m≠n" by auto;

qed;

text{*If one integer is greater or equal and not equal to another,

then it is not smaller or equal.*}

lemma (in int0) Int_ZF_2_L19AA: assumes A1: "m\<lsq>n" and A2: "m≠n"

shows "¬(n\<lsq>m)"

proof -

from A1 A2 have

"group3(\<int>, IntegerAddition, IntegerOrder)"

"⟨m,n⟩ ∈ IntegerOrder"

"m≠n"

using Int_ZF_2_T1 by auto;

then have "⟨n,m⟩ ∉ IntegerOrder"

by (rule group3.OrderedGroup_ZF_1_L8AA);

thus "¬(n\<lsq>m)" by simp;

qed;

text{*The next lemma allows to prove theorems for the case of positive and

negative integers separately.*}

lemma (in int0) Int_ZF_2_L19A: assumes A1: "m∈\<int>" and A2: "¬(\<zero>\<lsq>m)"

shows "m\<lsq>\<zero>" "\<zero> \<lsq> (\<rm>m)" "m≠\<zero>"

proof -

from A1 have T: "\<zero> ∈ \<int>"

using Int_ZF_1_T2 group0.group0_2_L2 by auto;

with A1 A2 show "m\<lsq>\<zero>" using Int_ZF_2_L19 by blast;

from A1 T A2 show "m≠\<zero>" by (rule Int_ZF_2_L19);

from A1 T A2 have "(\<rm>\<zero>)\<lsq>(\<rm>m)" by (rule Int_ZF_2_L19);

then show "\<zero> \<lsq> (\<rm>m)"

using Int_ZF_1_T2 group0.group_inv_of_one by simp;

qed;

text{*We can prove a theorem about integers by proving that

it holds for $m=0$, $m\in$@{text "\<int>⇩_{+}"} and $-m\in$@{text "\<int>⇩_{+}"}.*}

lemma (in int0) Int_ZF_2_L19B:

assumes "m∈\<int>" and "Q(\<zero>)" and "∀n∈\<int>⇩_{+}. Q(n)" and "∀n∈\<int>⇩_{+}. Q(\<rm>n)"

shows "Q(m)"

proof -

let ?G = "\<int>"

let ?P = "IntegerAddition"

let ?r = "IntegerOrder"

let ?b = "m"

from assms have

"group3(?G, ?P, ?r)"

"?r {is total on} ?G"

"?b ∈ ?G"

"Q(TheNeutralElement(?G, ?P))"

"∀a∈PositiveSet(?G, ?P, ?r). Q(a)"

"∀a∈PositiveSet(?G, ?P, ?r). Q(GroupInv(?G, ?P)`(a))"

using Int_ZF_2_T1 by auto;

then show "Q(?b)" by (rule group3.OrderedGroup_ZF_1_L18);

qed;

text{*An integer is not greater than its absolute value.*}

lemma (in int0) Int_ZF_2_L19C: assumes A1: "m∈\<int>"

shows

"m \<lsq> abs(m)"

"(\<rm>m) \<lsq> abs(m)"

using assms Int_ZF_2_T1

group3.OrderedGroup_ZF_3_L5 group3.OrderedGroup_ZF_3_L6

by auto;

text{*$|m-n| = |n-m|$.*}

lemma (in int0) Int_ZF_2_L20: assumes "m∈\<int>" "n∈\<int>"

shows "abs(m\<rs>n) = abs(n\<rs>m)"

using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L7B by simp;

text{*We can add the sides of inequalities with absolute values.*}

lemma (in int0) Int_ZF_2_L21:

assumes A1: "m∈\<int>" "n∈\<int>"

and A2: "abs(m) \<lsq> k" "abs(n) \<lsq> l"

shows

"abs(m\<ra>n) \<lsq> k \<ra> l"

"abs(m\<rs>n) \<lsq> k \<ra> l"

using assms Int_ZF_1_T2 Int_ZF_2_T1

group3.OrderedGroup_ZF_3_L7C group3.OrderedGroup_ZF_3_L7CA

by auto;

text{*Absolute value is nonnegative.*}

lemma (in int0) int_abs_nonneg: assumes A1: "m∈\<int>"

shows "abs(m) ∈ \<int>⇧^{+}" "\<zero> \<lsq> abs(m)"

proof -

have "AbsoluteValue(\<int>,IntegerAddition,IntegerOrder) : \<int>->\<int>⇧^{+}"

using Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L3C by simp;

with A1 show "abs(m) ∈ \<int>⇧^{+}" using apply_funtype

by simp;

then show "\<zero> \<lsq> abs(m)"

using Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L2 by simp;

qed;

text{*If an nonnegative integer is less or equal than another,

then so is its absolute value.*}

lemma (in int0) Int_ZF_2_L23:

assumes "\<zero>\<lsq>m" "m\<lsq>k"

shows "abs(m) \<lsq> k"

using assms Int_ZF_2_L16 by simp;(* this is probably not worth the effort*)

section{*Induction on integers.*}

text{*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.

*}

text{*An integer can be written a a sum of a smaller integer and a natural

number.*}

lemma (in int0) Int_ZF_3_L2: assumes A1: "i \<lsq> m"

shows "∃n∈nat. m = i $+ $# n"

proof -

let ?n = "0"

{ assume A2: "i=m"

from A1 A2 have "?n ∈ nat" "m = i $+ $# ?n"

using Int_ZF_2_L1A zadd_int0_right by auto;

hence "∃n∈nat. m = i $+ $# n" by blast }

moreover

{ assume A3: "i≠m"

with A1 have "i $< m" "i∈\<int>" "m∈\<int>"

using Int_ZF_2_L9 Int_ZF_2_L1A by auto;

then obtain k where D1: "k∈nat" "m = i $+ $# succ(k)"

using zless_imp_succ_zadd_lemma by auto;

let ?n = "succ(k)"

from D1 have "?n∈nat" "m = i $+ $# ?n" by auto;

hence "∃n∈nat. m = i $+ $# n" by simp }

ultimately show ?thesis by blast

qed;

text{*Induction for integers, the induction step.*}

lemma (in int0) Int_ZF_3_L6: assumes A1: "i∈\<int>"

and A2: "∀m. i\<lsq>m ∧ Q(m) --> Q(m $+ ($# 1))"

shows "∀k∈nat. Q(i $+ ($# k)) --> Q(i $+ ($# succ(k)))"

proof;

fix k assume A3: "k∈nat" show "Q(i $+ $# k) --> Q(i $+ $# succ(k))"

proof;

assume A4: "Q(i $+ $# k)"

from A1 A3 have "i\<lsq> i $+ ($# k)" using Int_ZF_2_L12

by simp;

with A4 A2 have "Q(i $+ ($# k) $+ ($# 1))" by simp;

then show "Q(i $+ ($# succ(k)))" using Int_ZF_2_L11 by simp;

qed

qed;

text{*Induction on integers, version with higher-order increment function.*}

lemma (in int0) Int_ZF_3_L7:

assumes A1: "i\<lsq>k" and A2: "Q(i)"

and A3: "∀m. i\<lsq>m ∧ Q(m) --> Q(m $+ ($# 1))"

shows "Q(k)"

proof -;

from A1 obtain n where D1: "n∈nat" and D2: "k = i $+ $# n"

using Int_ZF_3_L2 by auto;

from A1 have T1: "i∈\<int>" using Int_ZF_2_L1A by simp;

note `n∈nat`

moreover from A1 A2 have "Q(i $+ $#0)"

using Int_ZF_2_L1A zadd_int0 by simp;

moreover from T1 A3 have

"∀k∈nat. Q(i $+ ($# k)) --> Q(i $+ ($# succ(k)))"

by (rule Int_ZF_3_L6);

ultimately have "Q(i $+ ($# n))" by (rule ind_on_nat);

with D2 show "Q(k)" by simp;

qed;

text{*Induction on integer, implication between two forms of the induction

step.*}

lemma (in int0) Int_ZF_3_L7A: assumes

A1: "∀m. i\<lsq>m ∧ Q(m) --> Q(m\<ra>\<one>)"

shows "∀m. i\<lsq>m ∧ Q(m) --> Q(m $+ ($# 1))"

proof -

{ fix m assume "i\<lsq>m ∧ Q(m)"

with A1 have T1: "m∈\<int>" "Q(m\<ra>\<one>)" using Int_ZF_2_L1A by auto;

then have "m\<ra>\<one> = m\<ra>($# 1)" using Int_ZF_1_L8 by simp;

with T1 have "Q(m $+ ($# 1))" using Int_ZF_1_L2

by simp;

} then show ?thesis by simp;

qed;

text{*Induction on integers, version with ZF increment function.*}

theorem (in int0) Induction_on_int:

assumes A1: "i\<lsq>k" and A2: "Q(i)"

and A3: "∀m. i\<lsq>m ∧ Q(m) --> Q(m\<ra>\<one>)"

shows "Q(k)"

proof -;

from A3 have "∀m. i\<lsq>m ∧ Q(m) --> Q(m $+ ($# 1))"

by (rule Int_ZF_3_L7A);

with A1 A2 show ?thesis by (rule Int_ZF_3_L7);

qed;

text{*Another form of induction on integers. This rewrites the basic theorem

@{text "Int_ZF_3_L7"} substituting $P(-k)$ for $Q(k)$.*};

lemma (in int0) Int_ZF_3_L7B: assumes A1: "i\<lsq>k" and A2: "P($-i)"

and A3: "∀m. i\<lsq>m ∧ P($-m) --> P($-(m $+ ($# 1)))"

shows "P($-k)"

proof -

from A1 A2 A3 show "P($-k)" by (rule Int_ZF_3_L7);

qed;

text{*Another induction on integers. This rewrites Int\_ZF\_3\_L7

substituting $-k$ for $k$ and $-i$ for $i$.*}

lemma (in int0) Int_ZF_3_L8: assumes A1: "k\<lsq>i" and A2: "P(i)"

and A3: "∀m. $-i\<lsq>m ∧ P($-m) --> P($-(m $+ ($# 1)))"

shows "P(k)"

proof -

from A1 have T1: "$-i\<lsq>$-k" using Int_ZF_2_L10 by simp;

from A1 A2 have T2: "P($- $- i)" using Int_ZF_2_L1A zminus_zminus

by simp;

from T1 T2 A3 have "P($-($-k))" by (rule Int_ZF_3_L7);

with A1 show "P(k)" using Int_ZF_2_L1A zminus_zminus by simp;

qed;

text{*An implication between two forms of induction steps.*}

lemma (in int0) Int_ZF_3_L9: assumes A1: "i∈\<int>"

and A2: "∀n. n\<lsq>i ∧ P(n) --> P(n $+ $-($#1))"

shows "∀m. $-i\<lsq>m ∧ P($-m) --> P($-(m $+ ($# 1)))"

proof;

fix m show "$-i\<lsq>m ∧ P($-m) --> P($-(m $+ ($# 1)))"

proof;

assume A3: "$- i \<lsq> m ∧ P($- m)"

then have "$- i \<lsq> m" by simp;

then have "$-m \<lsq> $- ($- i)" by (rule Int_ZF_2_L10);

with A1 A2 A3 show "P($-(m $+ ($# 1)))"

using zminus_zminus zminus_zadd_distrib by simp;

qed;

qed;

text{*Backwards induction on integers, version with higher-order decrement

function.*}

lemma (in int0) Int_ZF_3_L9A: assumes A1: "k\<lsq>i" and A2: "P(i)"

and A3: "∀n. n\<lsq>i ∧ P(n) -->P(n $+ $-($#1)) "

shows "P(k)"

proof -

from A1 have T1: "i∈\<int>" using Int_ZF_2_L1A by simp;

from T1 A3 have T2: "∀m. $-i\<lsq>m ∧ P($-m) --> P($-(m $+ ($# 1)))"

by (rule Int_ZF_3_L9);

from A1 A2 T2 show "P(k)" by (rule Int_ZF_3_L8)

qed;

text{*Induction on integers, implication between two forms of the induction

step.*}

lemma (in int0) Int_ZF_3_L10: assumes

A1: "∀n. n\<lsq>i ∧ P(n) --> P(n\<rs>\<one>)"

shows "∀n. n\<lsq>i ∧ P(n) --> P(n $+ $-($#1))"

proof -;

{ fix n assume "n\<lsq>i ∧ P(n)"

with A1 have T1: "n∈\<int>" "P(n\<rs>\<one>)" using Int_ZF_2_L1A by auto;

then have "n\<rs>\<one> = n\<rs>($# 1)" using Int_ZF_1_L8 by simp;

with T1 have "P(n $+ $-($#1))" using Int_ZF_1_L10 by simp

} then show ?thesis by simp;

qed;

text{*Backwards induction on integers.*}

theorem (in int0) Back_induct_on_int:

assumes A1: "k\<lsq>i" and A2: "P(i)"

and A3: "∀n. n\<lsq>i ∧ P(n) --> P(n\<rs>\<one>)"

shows "P(k)"

proof -;

from A3 have "∀n. n\<lsq>i ∧ P(n) --> P(n $+ $-($#1))"

by (rule Int_ZF_3_L10);

with A1 A2 show "P(k)" by (rule Int_ZF_3_L9A);

qed;

section{*Bounded vs. finite subsets of integers*}

text{*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

@{text "OrderedGroups_ZF.thy"}. To show the other implication we

show that all intervals starting at 0 are finite and then use a result from

@{text "OrderedGroups_ZF.thy"}.*}

text{*There are no integers between $k$ and $k+1$.*}

lemma (in int0) Int_ZF_4_L1:

assumes A1: "k∈\<int>" "m∈\<int>" "n∈nat" and A2: "k $+ $#1 = m $+ $#n"

shows "m = k $+ $#1 ∨ m \<lsq> k"

proof -

{ assume "n=0"

with A1 A2 have "m = k $+ $#1 ∨ m \<lsq> k"

using zadd_int0 by simp }

moreover

{ assume "n≠0"

with A1 obtain j where D1: "j∈nat" "n = succ(j)"

using Nat_ZF_1_L3 by auto;

with A1 A2 D1 have "m = k $+ $#1 ∨ m \<lsq> k"

using Int_ZF_2_L13 by simp }

ultimately show ?thesis by blast

qed;

text{*A trivial calculation lemma that allows to subtract and add one. *}

lemma Int_ZF_4_L1A:

assumes "m∈int" shows "m $- $#1 $+ $#1 = m"

using assms eq_zdiff_iff by auto;

text{*There are no integers between $k$ and $k+1$, another formulation.*}

lemma (in int0) Int_ZF_4_L1B: assumes A1: "m \<lsq> L"

shows

"m = L ∨ m\<ra>\<one> \<lsq> L"

"m = L ∨ m \<lsq> L\<rs>\<one>"

proof -

let ?k = "L $- $#1"

from A1 have T1: "m∈\<int>" "L∈\<int>" "L = ?k $+ $#1"

using Int_ZF_2_L1A Int_ZF_4_L1A by auto;

moreover from A1 obtain n where D1: "n∈nat" "L = m $+ $# n"

using Int_ZF_3_L2 by auto;

ultimately have "m = L ∨ m \<lsq> ?k"

using Int_ZF_4_L1 by simp;

with T1 show "m = L ∨ m\<ra>\<one> \<lsq> L"

using Int_ZF_2_L9A by auto;

with T1 show "m = L ∨ m \<lsq> L\<rs>\<one>"

using Int_ZF_1_L8A Int_ZF_2_L9B by simp;

qed;

text{*If $j\in m..k+1$, then $j\in m..n$ or $j=k+1$.*}

lemma (in int0) Int_ZF_4_L2: assumes A1: "k∈\<int>"

and A2: "j ∈ m..(k $+ $#1)"

shows "j ∈ m..k ∨ j ∈ {k $+ $#1}"

proof -;

from A2 have T1: "m\<lsq>j" "j\<lsq>(k $+ $#1)" using Order_ZF_2_L1A

by auto;

then have T2: "m∈\<int>" "j∈\<int>" using Int_ZF_2_L1A by auto;

from T1 obtain n where "n∈nat" "k $+ $#1 = j $+ $# n"

using Int_ZF_3_L2 by auto;

with A1 T1 T2 have "(m\<lsq>j ∧ j \<lsq> k) ∨ j ∈ {k $+ $#1}"

using Int_ZF_4_L1 by auto;

then show ?thesis using Order_ZF_2_L1B by auto;

qed;

text{*Extending an integer interval by one is the same as adding the new

endpoint.*}

lemma (in int0) Int_ZF_4_L3: assumes A1: "m\<lsq> k"

shows "m..(k $+ $#1) = m..k ∪ {k $+ $#1}"

proof;

from A1 have T1: "m∈\<int>" "k∈\<int>" using Int_ZF_2_L1A by auto;

then show "m .. (k $+ $# 1) ⊆ m .. k ∪ {k $+ $# 1}"

using Int_ZF_4_L2 by auto;

from T1 have "m\<lsq> m" using Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L3

by simp;

with T1 A1 have "m .. k ⊆ m .. (k $+ $# 1)"

using Int_ZF_2_L12 Int_ZF_2_L6 Order_ZF_2_L3 by simp;

with T1 A1 show "m..k ∪ {k $+ $#1} ⊆ m..(k $+ $#1)"

using Int_ZF_2_L12A int_ord_is_refl Order_ZF_2_L2 by auto;

qed;

text{*Integer intervals are finite - induction step.*}

lemma (in int0) Int_ZF_4_L4:

assumes A1: "i\<lsq>m" and A2: "i..m ∈ Fin(\<int>)"

shows "i..(m $+ $#1) ∈ Fin(\<int>)"

using assms Int_ZF_4_L3 by simp;

text{*Integer intervals are finite.*}

lemma (in int0) Int_ZF_4_L5: assumes A1: "i∈\<int>" "k∈\<int>"

shows "i..k ∈ Fin(\<int>)"

proof -

{ assume A2: "i\<lsq>k"

moreover from A1 have "i..i ∈ Fin(\<int>)"

using int_ord_is_refl Int_ZF_2_L4 Order_ZF_2_L4 by simp;

moreover from A2 have

"∀m. i\<lsq>m ∧ i..m ∈ Fin(\<int>) --> i..(m $+ $#1) ∈ Fin(\<int>)"

using Int_ZF_4_L4 by simp;

ultimately have "i..k ∈ Fin(\<int>)" by (rule Int_ZF_3_L7) }

moreover

{ assume "¬ i \<lsq> k"

then have "i..k ∈ Fin(\<int>)" using Int_ZF_2_L6 Order_ZF_2_L5

by simp }

ultimately show ?thesis by blast

qed;

text{*Bounded integer sets are finite.*}

lemma (in int0) Int_ZF_4_L6: assumes A1: "IsBounded(A,IntegerOrder)"

shows "A ∈ Fin(\<int>)"

proof -;

have T1: "∀m ∈ Nonnegative(\<int>,IntegerAddition,IntegerOrder).

$#0..m ∈ Fin(\<int>)"

proof

fix m assume "m ∈ Nonnegative(\<int>,IntegerAddition,IntegerOrder)"

then have "m∈\<int>" using Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L4E

by auto;

then show "$#0..m ∈ Fin(\<int>)" using Int_ZF_4_L5 by simp

qed;

have "group3(\<int>,IntegerAddition,IntegerOrder)"

using Int_ZF_2_T1 by simp;

moreover from T1 have "∀m ∈ Nonnegative(\<int>,IntegerAddition,IntegerOrder).

Interval(IntegerOrder,TheNeutralElement(\<int>,IntegerAddition),m)

∈ Fin(\<int>)" using Int_ZF_1_L8 by simp;

moreover note A1

ultimately show "A ∈ Fin(\<int>)" by (rule group3.OrderedGroup_ZF_2_T1);

qed;

text{*A subset of integers is bounded iff it is finite.*}

theorem (in int0) Int_bounded_iff_fin:

shows "IsBounded(A,IntegerOrder)<-> A∈Fin(\<int>)"

using Int_ZF_4_L6 Int_ZF_2_T1 group3.ord_group_fin_bounded

by blast;

text{*The image of an interval by any integer function is

finite, hence bounded.*}

lemma (in int0) Int_ZF_4_L8:

assumes A1: "i∈\<int>" "k∈\<int>" and A2: "f:\<int>->\<int>"

shows

"f``(i..k) ∈ Fin(\<int>)"

"IsBounded(f``(i..k),IntegerOrder)"

using assms Int_ZF_4_L5 Finite1_L6A Int_bounded_iff_fin

by auto;

text{*If for every integer we can find one in $A$ that is greater or equal,

then $A$ is is not bounded above, hence infinite.*}

lemma (in int0) Int_ZF_4_L9: assumes A1: "∀m∈\<int>. ∃k∈A. m\<lsq>k"

shows

"¬IsBoundedAbove(A,IntegerOrder)"

"A ∉ Fin(\<int>)"

proof -

have "\<int> ≠ {\<zero>}"

using Int_ZF_1_L8A int_zero_not_one by blast

with A1 show

"¬IsBoundedAbove(A,IntegerOrder)"

"A ∉ Fin(\<int>)"

using Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L2A

by auto;

qed;

end