Theory Int_ZF

(* 
    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 imports OrderedGroup_ZF Finite_ZF_1 Int Nat_ZF 

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

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 $\$\leq $ (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 positive integers using the notion of 
  positive set from the @{text "OrderedGroup"} theory.*}

constdefs

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

  "IntegerMultiplication ≡ 
    { <x,c> ∈ (int×int)×int. fst(x) $× snd(x) = c}"

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

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

text{*IntegerAddition and IntegerMultiplication are functions on 
  int$\times$int. *}

lemma Int_ZF_1_L1: 
  "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 :: "i=>i" ("\<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 :: "i=>i" ("\<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 itwo_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
  @{text "$+"} and @{text "$×"} 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 prems 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 prems 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: "($# 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 prems 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 prems 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 prems 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.group0_2_L16
      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: "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: "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: "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;
  show "IntegerOrder {is total on} \<int>"
    using IsTotal_def zle_linear Int_ZF_2_L1 by auto;
  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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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: "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 (cases "n = 0");
  assume "n = 0" 
  with A1 show "i \<lsq> i $+ $#n" using zadd_int0 int_ord_is_refl refl_def
    by simp;
next;
  assume "n≠0" 
  with A2 obtain k where "k∈nat" "n = succ(k)" 
    using Nat_ZF_1_L3 by auto;
  with A1 show "i \<lsq> i $+ $#n"
    using zless_succ_zadd zless_imp_zle Int_ZF_2_L1 by simp;
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 prems 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 A2 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 prems 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>b1" "c\<lsq>c1" and "a\<lsq>b\<ra>c"
  shows "a\<lsq>b1\<ra>c1"
proof -
  from prems have "group3(\<int>,IntegerAddition,IntegerOrder)" 
    "⟨a,IntegerAddition`<b,c>⟩ ∈ IntegerOrder" 
    "⟨b,b1⟩ ∈ IntegerOrder" "⟨c,c1⟩ ∈ IntegerOrder"
    using Int_ZF_2_T1 by auto
  then have "⟨a,IntegerAddition`<b1,c1>⟩ ∈ 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 prems 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>c1" 
  shows "a\<lsq>b\<ra>c1"
proof - 
  from prems have 
    "group3(\<int>,IntegerAddition,IntegerOrder)" 
    "b ∈ \<int>"
    "⟨a,IntegerAddition`<b,c>⟩ ∈ IntegerOrder" 
    "⟨c,c1⟩ ∈ IntegerOrder"
    using Int_ZF_2_T1 by auto;
  then have "⟨a,IntegerAddition`<b,c1>⟩ ∈ 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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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 T1: "\<zero> ∈ \<int>" 
    using Int_ZF_1_T2 group0.group0_2_L2 by auto;
  with A1 show "m\<lsq>\<zero>" by (rule Int_ZF_2_L19);
  from A1 T1 show "m≠\<zero>"  by (rule Int_ZF_2_L19);
  from A1 T1 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 prems 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 prems 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 prems 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 prems 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 prems 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 (cases "i=m");
  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;
  thus "∃n∈nat. m = i $+ $# n" by blast;
next
  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;
  thus "∃n∈nat. m = i $+ $# n" by simp;
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;
  from D1 have "n∈nat" .
  moreover from A1 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 Nat_ZF_1_L2); 
  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 (cases "n=0");
  assume "n=0" 
  with A1 A2 show "m =  k $+ $#1 ∨ m \<lsq> k" 
    using zadd_int0 by simp;
next 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 show "m =  k $+ $#1 ∨ m \<lsq> k" 
    using Int_ZF_2_L13 by simp;
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 prems 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 prems 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 (cases "i\<lsq> k");
  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 show "i..k ∈ Fin(\<int>)" by (rule Int_ZF_3_L7);
next assume "¬ i \<lsq> k"
  then show "i..k ∈ Fin(\<int>)" using Int_ZF_2_L6 Order_ZF_2_L5
    by simp;
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 from A1 have "IsBounded(A,IntegerOrder)" .;
  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{*If $A\cap Z_+$ is finite, then $A$ is bounded above.*}

lemma (in int0) Int_ZF_4_L7: 
  assumes "A⊆\<int>" and "A ∩ \<int>+ ∈ Fin(\<int>)"
  shows "IsBoundedAbove(A,IntegerOrder)"
  using prems Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L4
  by simp;*)

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 prems 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