Theory Int_ZF_IML

(* 
    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.

*)

section ‹Integers - introduction›

theory Int_ZF_IML imports OrderedGroup_ZF_1 Finite_ZF_1 ZF.Int 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.›

subsection‹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 
  ‹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.›

text‹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 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 ‹int›. In standard Isabelle/ZF product of integers is denoted by
  prepending the dollar sign to ‹*›.  
›

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

text‹Definition of natural order on integers as a relation on ‹int›.
  In the standard Isabelle/ZF the inequality relation on integers
  is denoted ‹≤› 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 
  ‹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 ‹𝟬› to denote the neutral element of addition, 
  ‹𝟭› as the
  unit of the multiplicative monoid. We introduce notation ‹m\<lsq>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 ‹\<sm>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.›

locale int0 =

  fixes ints ("ℤ")
  defines ints_def [simp]: "ℤ ≡ 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(ℤ,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(ℤ,IntegerAddition)``(A)"

  fixes izero ("𝟬")
  defines izero_def [simp]: "𝟬 ≡ TheNeutralElement(ℤ,IntegerAddition)"

  fixes ione ("𝟭")
  defines ione_def [simp]: "𝟭 ≡ TheNeutralElement(ℤ,IntegerMultiplication)"

  fixes itwo ("𝟮")
  defines itwo_def [simp]: "𝟮 ≡ 𝟭\<ra>𝟭"
 
  fixes ithree ("𝟯")
  defines ithree_def [simp]: "𝟯 ≡ 𝟮\<ra>𝟭"
  
  fixes nonnegative ("ℤ⇧+")
  defines nonnegative_def [simp]: 
  "ℤ⇧+ ≡ Nonnegative(ℤ,IntegerAddition,IntegerOrder)"

  fixes positive ("ℤ⇩+")
  defines positive_def [simp]: 
  "ℤ⇩+ ≡ PositiveSet(ℤ,IntegerAddition,IntegerOrder)"

  fixes abs 
  defines abs_def [simp]: 
  "abs(m) ≡ AbsoluteValue(ℤ,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 ‹IntegerAddition› and
  ‹IntegerMultiplication› give the same results as the higher-order
  equivalents defined in the standard ‹Int› theory.›

lemma (in int0) Int_ZF_1_L2: assumes A1: "a ∈ ℤ"  "b ∈ ℤ"
  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⟩ ∈ (ℤ×ℤ)×ℤ. fst(x) $+ snd(x) = c}"
    "⟨ ?x,?d⟩ ∈ {⟨ x,d⟩ ∈ (ℤ×ℤ)×ℤ. 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∈ℤ"  "y∈ℤ"  "z∈ℤ"
  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∈ℤ"  "y∈ℤ"
  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∈ℤ"
  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)∈ℤ ∧ 
  (∀x∈ℤ. ($# 0)\<ra>x = x ∧ x\<ra>($# 0) = x)"
  "($# 1)∈ℤ ∧ 
  (∀x∈ℤ. ($# 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(ℤ,IntegerAddition)"
  "IsAmonoid(ℤ,IntegerMultiplication)"
proof -
   have  
    "∃e∈ℤ. ∀x∈ℤ. e\<ra>x = x ∧ x\<ra>e = x"
     "∃e∈ℤ. ∀x∈ℤ. e⋅x = x ∧ x⋅e = x"
     using int0.Int_ZF_1_L6 by auto
   then show "IsAmonoid(ℤ,IntegerAddition)"
     "IsAmonoid(ℤ,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) = 𝟬"  "($# 1) = 𝟭"
proof -
  have "monoid0(ℤ,IntegerAddition)"
    using Int_ZF_1_T1 monoid0_def by simp
  moreover have 
    "($# 0)∈ℤ ∧
    (∀x∈ℤ. IntegerAddition`⟨$# 0,x⟩ = x ∧ 
    IntegerAddition`⟨x ,$# 0⟩ = x)"
    using Int_ZF_1_L6 by auto
  ultimately have "($# 0) = TheNeutralElement(ℤ,IntegerAddition)"
    by (rule monoid0.group0_1_L4)
  then show "($# 0) = 𝟬" 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) = 𝟭" by simp
qed

text‹$0$  and $1$, as defined in ‹int0› context, are integers.›

lemma (in int0) Int_ZF_1_L8A: shows "𝟬 ∈ ℤ"  "𝟭 ∈ ℤ"
proof -
  have "($# 0) ∈ ℤ"  "($# 1) ∈ ℤ" by auto
  then show "𝟬 ∈ ℤ"  "𝟭 ∈ ℤ" using Int_ZF_1_L8 by auto
qed

text‹Zero is not one.›

lemma (in int0) int_zero_not_one: shows "𝟬 ≠ 𝟭"
proof -
  have "($# 0) ≠ ($# 1)" by simp
  then show "𝟬 ≠ 𝟭" 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 "ℤ ≠ 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 "ℤ ≠ {𝟬}"
  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 ∈ ℤ"
  shows "∃ b∈ℤ. g\<ra>b = 𝟬"
proof -
  from A1 have "g\<ra> $-g = 𝟬"
    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 ‹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∈ℤ" 
  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∈ℤ"  "n∈ℤ"
  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>𝟬) = 𝟬"
  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∈ℤ" 
  shows "(m $- $#1) \<ra> 𝟭 = 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∈ℤ" 
  shows 
  "m\<ra>𝟭 ≠ m"
  "m\<rs>𝟭 ≠ m"
proof -
  { assume "m\<ra>𝟭 = m" 
    with A1 have 
      "group0(ℤ,IntegerAddition)"  
      "m∈ℤ"  "𝟭∈ℤ"
      "IntegerAddition`⟨m,𝟭⟩ = m" 
      using Int_ZF_1_T2 Int_ZF_1_L8A by auto
    then have "𝟭 = TheNeutralElement(ℤ,IntegerAddition)"
      by (rule group0.group0_2_L7)
    then have False using int_zero_not_one by simp
  } then show I: "m\<ra>𝟭 ≠ m" by auto
  { from A1 have "m \<rs> 𝟭 \<ra> 𝟭 = m"
      using Int_ZF_1_L8A Int_ZF_1_T2 group0.inv_cancel_two
      by simp
    moreover assume "m\<rs>𝟭 = m"
    ultimately have "m \<ra> 𝟭 = m" by simp
    with I have False by simp
  } then show "m\<rs>𝟭 ≠ m" by auto
qed

text‹If the difference is zero, the integers are equal.›

lemma (in int0) Int_ZF_1_L15: 
  assumes A1: "m∈ℤ"  "n∈ℤ" and A2: "m\<rs>n = 𝟬"
  shows "m=n" 
proof -
  let ?G = "ℤ"
  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

subsection‹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∈ℤ" "n∈ℤ" and A2: "m $≤ n"
  shows "m \<lsq> n"
proof -
  from A1 A2 have "⟨ m,n⟩ ∈ {x∈ℤ×ℤ. 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∈ℤ" "n∈ℤ"
proof -
  from A1 have "⟨ m,n⟩ ∈ {p∈ℤ×ℤ. fst(p) $≤ snd(p)}"
    using IntegerOrder_def by simp
  thus "m $≤ n"  "m∈ℤ"  "n∈ℤ" 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⊆ℤ"
proof -
  from A1 have 
    "IntegerOrder ⊆ ℤ×ℤ"
    "IsBoundedBelow(A,IntegerOrder)"
    using Int_ZF_2_L1B by auto
  then show "A⊆ℤ" by (rule Order_ZF_3_L1B)
qed

text‹The order on integers is reflexive.›

lemma (in int0) int_ord_is_refl: shows "refl(ℤ,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∈ℤ"  "n∈ℤ"
    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 ‹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 ∈ ℤ" 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∈ℤ" "n∈ℤ" 
    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(ℤ,IntegerAddition,IntegerOrder)"
  "IntegerOrder {is total on} ℤ"
  "group3(ℤ,IntegerAddition,IntegerOrder)"
  "IsLinOrder(ℤ,IntegerOrder)"
proof -
  have "∀k∈ℤ. ∀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(ℤ,IntegerAddition,IntegerOrder)" using
    Int_ZF_1_T2 Int_ZF_2_L1B Int_ZF_2_L7 IsAnOrdGroup_def
    by simp
  then show "group3(ℤ,IntegerAddition,IntegerOrder)"
    using group3_def by simp
  have "∀n∈ℤ. ∀m∈ℤ. n\<lsq>m ∨ m\<lsq>n"
    using zle_linear Int_ZF_2_L1 by auto
  then show "IntegerOrder {is total on} ℤ"
    using IsTotal_def by simp
  with T1 show "IsLinOrder(ℤ,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∈ℤ"  "m∈ℤ" 
    using Int_ZF_2_L1A by auto
  with A2 show "i $< m" using zle_def by simp
qed

text‹This shows how Isabelle's ‹$<› operator translates to IsarMathLib
  notation.›

lemma (in int0) Int_ZF_2_L9AA: assumes A1: "m∈ℤ"  "n∈ℤ"
  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∈ℤ" and A2: "m \<lsq> k $- ($# 1)"
  shows "m\<ra>𝟭 \<lsq> k"
proof -
  from A2 have "m\<ra>𝟭 \<lsq> (k $- ($# 1)) \<ra> 𝟭"
    using Int_ZF_1_L8A int_ord_transl_inv by simp
  with A1 show "m\<ra>𝟭 \<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∈ℤ"  "m∈ℤ"  "k∈ℤ"
  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 ‹Int_ZF_2_L9B› with weaker assumptions.›

lemma (in int0) Int_ZF_2_L9C: 
  assumes "i∈ℤ"  "m∈ℤ" 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∈ℤ"  "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∈ℤ"  "n∈ℤ"  "k∈ℤ" 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> 𝟬"
  shows "𝟬\<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∈ℤ" and "𝟬\<lsq>(\<rm>k)"
  shows "k\<lsq>𝟬"
  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∈ℤ" 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>𝟭"
proof -
  from A1 have T1:"j∈ℤ" "k∈ℤ" "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>𝟭" 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∈ℤ" shows "m \<lsq> m\<ra>𝟭"
  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∈ℤ" "m∈ℤ" and A2: "n∈nat" 
  and A3: "k $+ ($# 1) = m $+ $# succ(n)"
  shows "m \<lsq> k"
proof -
  from A1 have "k∈ℤ" "m $+ $# n ∈ ℤ" 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∈ℤ"
  shows "abs(m) ∈ ℤ"
proof -
  have "AbsoluteValue(ℤ,IntegerAddition,IntegerOrder) : ℤ→ℤ"
    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 "𝟬\<lsq>m"  "𝟬\<lsq>n"
  shows 
  "(\<rm>m) \<lsq> n"
  "𝟬 \<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(ℤ,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∈ℤ" and "a\<lsq>b\<ra>c" and A3: "c\<lsq>c⇩1" 
  shows "a\<lsq>b\<ra>c⇩1"
proof - 
  from assms have 
    "group3(ℤ,IntegerAddition,IntegerOrder)" 
    "b ∈ ℤ"
    "⟨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∈ℤ"  "n∈ℤ" 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 "𝟬\<lsq>n"  "m∈ℤ"
  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∈ℤ"  "n∈ℤ"
  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 "𝟬\<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∈ℤ"  "n∈ℤ"
  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 "𝟬\<lsq>m" shows  "m∈ℤ⇧+" 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 "𝟬\<lsq>𝟭" and "abs(𝟭) = 𝟭"
proof -
  have "($# 0) ∈ ℤ" "($# 1)∈ ℤ" by auto
  then have "𝟬\<lsq>𝟬" and T1: "𝟭∈ℤ" 
    using Int_ZF_1_L8 int_ord_is_refl refl_def by auto
  then have "𝟬\<lsq>𝟬\<ra>𝟭" using Int_ZF_2_L12A by simp
  with T1 show "𝟬\<lsq>𝟭" using Int_ZF_1_T2 group0.group0_2_L2
    by simp
  then show "abs(𝟭) = 𝟭" using Int_ZF_2_L16 by simp
qed

text‹$1\leq 2$.›

lemma (in int0) Int_ZF_2_L16B: shows "𝟭\<lsq>𝟮"
proof -
  have "($# 1)∈ ℤ" by simp
  then show "𝟭\<lsq>𝟮" 
    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: "𝟭\<lsq>a" shows 
  "𝟬\<lsq>a"  "a≠𝟬"
  "𝟮 \<lsq> a\<ra>𝟭"
  "𝟭 \<lsq> a\<ra>𝟭"
  "𝟬 \<lsq> a\<ra>𝟭"
proof -
  from A1 have "𝟬\<lsq>𝟭" and "𝟭\<lsq>a" 
    using Int_ZF_2_L16A by auto
  then show "𝟬\<lsq>a" by (rule Int_order_transitive)
  have I: "𝟬\<lsq>𝟭" using Int_ZF_2_L16A by simp 
  have "𝟭\<lsq>𝟮" using Int_ZF_2_L16B by simp
  moreover from A1 show "𝟮 \<lsq> a\<ra>𝟭"
    using Int_ZF_1_L8A int_ord_transl_inv by simp
  ultimately show "𝟭 \<lsq> a\<ra>𝟭" by (rule Int_order_transitive)
  with I show "𝟬 \<lsq> a\<ra>𝟭" by (rule Int_order_transitive)
  from A1 show "a≠𝟬" 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∈ℤ" 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(𝟬) = 𝟬"
  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∈ℤ"  "n∈ℤ"
  shows 
  "abs(m\<rs>n) \<lsq> abs(n)\<ra>abs(m)"
  "abs(m\<rs>n) \<lsq> abs(m)\<ra>abs(n)"
proof -
  have "$-n ∈ ℤ" 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∈ℤ"  "n∈ℤ"
  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
  ‹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∈ℤ"  "n∈ℤ"  "k∈ℤ"
  shows "abs(m\<ra>n\<ra>k) \<lsq> abs(m)\<ra>abs(n)\<ra>abs(k)"
proof -
  from A1 have T: "m\<ra>n ∈ ℤ"  "abs(k) ∈ ℤ"
    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∈ℤ"  "n∈ℤ" 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(ℤ, 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∈ℤ" and A2: "¬(𝟬\<lsq>m)"
  shows "m\<lsq>𝟬"  "𝟬 \<lsq> (\<rm>m)"  "m≠𝟬"
proof -
  from A1 have T: "𝟬 ∈ ℤ"
    using Int_ZF_1_T2 group0.group0_2_L2 by auto
  with A1 A2 show "m\<lsq>𝟬" using Int_ZF_2_L19 by blast
  from A1 T A2 show "m≠𝟬"  by (rule Int_ZF_2_L19)
  from A1 T A2 have "(\<rm>𝟬)\<lsq>(\<rm>m)" by (rule Int_ZF_2_L19)
  then show "𝟬 \<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$‹ℤ⇩+› and $-m\in$‹ℤ⇩+›.›

lemma (in int0) Int_ZF_2_L19B: 
  assumes "m∈ℤ" and "Q(𝟬)" and "∀n∈ℤ⇩+. Q(n)" and "∀n∈ℤ⇩+. Q(\<rm>n)"
  shows "Q(m)"
proof -
  let ?G = "ℤ"
  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∈ℤ"
  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∈ℤ"  "n∈ℤ"
  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∈ℤ" "n∈ℤ"
  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∈ℤ"
  shows "abs(m) ∈ ℤ⇧+"  "𝟬 \<lsq> abs(m)" 
proof -
  have "AbsoluteValue(ℤ,IntegerAddition,IntegerOrder) : ℤ→ℤ⇧+"
    using Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L3C by simp
  with A1 show "abs(m) ∈ ℤ⇧+" using apply_funtype
    by simp
  then show "𝟬 \<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 "𝟬\<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*)

subsection‹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∈ℤ" "m∈ℤ"   
      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∈ℤ" 
  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∈ℤ" 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>𝟭)"
  shows "∀m. i\<lsq>m ∧ Q(m) ⟶ Q(m $+ ($# 1))"
proof -
  { fix m assume "i\<lsq>m ∧ Q(m)" 
    with A1 have T1: "m∈ℤ" "Q(m\<ra>𝟭)" using Int_ZF_2_L1A by auto
    then have "m\<ra>𝟭 = 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>𝟭)"
  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 
   ‹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∈ℤ"
  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∈ℤ" 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>𝟭)"
  shows "∀n. n\<lsq>i ∧ P(n) ⟶ P(n $+ $-($#1))"
proof -
  { fix n assume "n\<lsq>i ∧ P(n)"
    with A1 have T1: "n∈ℤ" "P(n\<rs>𝟭)" using Int_ZF_2_L1A by auto
    then have "n\<rs>𝟭 = 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>𝟭)"
  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
    
subsection‹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 
  ‹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›.›

text‹There are no integers between $k$ and $k+1$.›

lemma (in int0) Int_ZF_4_L1: 
  assumes A1: "k∈ℤ" "m∈ℤ" "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>𝟭 \<lsq> L"
  "m = L ∨ m \<lsq> L\<rs>𝟭" 
proof -
  let ?k = "L $- $#1"
  from A1 have T1: "m∈ℤ"  "L∈ℤ"  "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>𝟭 \<lsq> L"
    using Int_ZF_2_L9A by auto
  with T1 show "m = L ∨ m \<lsq> L\<rs>𝟭"
    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∈ℤ"
  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∈ℤ" "j∈ℤ" 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∈ℤ" "k∈ℤ" 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(ℤ)"
  shows "i..(m $+ $#1) ∈ Fin(ℤ)"
  using assms Int_ZF_4_L3 by simp

text‹Integer intervals are finite.›

lemma (in int0) Int_ZF_4_L5: assumes A1: "i∈ℤ" "k∈ℤ"
  shows "i..k ∈ Fin(ℤ)"
proof -
  { assume A2: "i\<lsq>k"
    moreover from A1 have "i..i ∈ Fin(ℤ)"
      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(ℤ) ⟶ i..(m $+ $#1) ∈ Fin(ℤ)"
      using Int_ZF_4_L4 by simp
    ultimately have "i..k ∈ Fin(ℤ)" by (rule Int_ZF_3_L7) }
  moreover 
  { assume "¬ i \<lsq> k"
    then have "i..k ∈ Fin(ℤ)" 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(ℤ)"
proof -
  have T1: "∀m ∈ Nonnegative(ℤ,IntegerAddition,IntegerOrder).
    $#0..m ∈ Fin(ℤ)" 
  proof
    fix m assume "m ∈ Nonnegative(ℤ,IntegerAddition,IntegerOrder)"
    then have "m∈ℤ" using Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L4E
      by auto
    then show "$#0..m ∈ Fin(ℤ)" using Int_ZF_4_L5 by simp
  qed
  have "group3(ℤ,IntegerAddition,IntegerOrder)"
    using Int_ZF_2_T1 by simp
  moreover from T1 have "∀m ∈ Nonnegative(ℤ,IntegerAddition,IntegerOrder).
    Interval(IntegerOrder,TheNeutralElement(ℤ,IntegerAddition),m) 
    ∈ Fin(ℤ)" using Int_ZF_1_L8 by simp
  moreover note A1
  ultimately show "A ∈ Fin(ℤ)" 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(ℤ)"
  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∈ℤ"  "k∈ℤ" and A2: "f:ℤ→ℤ"
  shows 
  "f``(i..k) ∈ Fin(ℤ)"
  "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∈ℤ. ∃k∈A. m\<lsq>k"
  shows 
  "¬IsBoundedAbove(A,IntegerOrder)"
  "A ∉ Fin(ℤ)"
proof -
  have "ℤ ≠ {𝟬}"
    using Int_ZF_1_L8A int_zero_not_one by blast
  with A1 show 
    "¬IsBoundedAbove(A,IntegerOrder)"
    "A ∉ Fin(ℤ)"
    using Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L2A
    by auto
qed


end