(* This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005 - 2009 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\_3.thy}*}

theory Int_ZF_3 imports Int_ZF_2

begin

text{*This theory is a continuation of @{text "Int_ZF_2"}. We consider

here the properties of slopes (almost homomorphisms on integers)

that allow to define the order relation and multiplicative

inverse on real numbers. We also prove theorems that allow to show

completeness of the order relation of real numbers we define in @{text "Real_ZF"}.

*}

section{*Positive slopes*}

text{*This section provides background material for defining the order relation on real numbers.*}

text{*Positive slopes are functions (of course.)*}

lemma (in int1) Int_ZF_2_3_L1: assumes A1: "f∈\<S>⇩_{+}" shows "f:\<int>->\<int>"

using assms AlmostHoms_def PositiveSet_def by simp;

text{*A small technical lemma to simplify the proof of the next theorem.*}

lemma (in int1) Int_ZF_2_3_L1A:

assumes A1: "f∈\<S>⇩_{+}" and A2: "∃n ∈ f``(\<int>⇩_{+}) ∩ \<int>⇩_{+}. a\<lsq>n"

shows "∃M∈\<int>⇩_{+}. a \<lsq> f`(M)"

proof -

from A1 have "f:\<int>->\<int>" "\<int>⇩_{+}⊆ \<int>"

using AlmostHoms_def PositiveSet_def by auto

with A2 show ?thesis using func_imagedef by auto;

qed;

text{*The next lemma is Lemma 3 in the Arthan's paper.*}

lemma (in int1) Arthan_Lem_3:

assumes A1: "f∈\<S>⇩_{+}" and A2: "D ∈ \<int>⇩_{+}"

shows "∃M∈\<int>⇩_{+}. ∀m∈\<int>⇩_{+}. (m\<ra>\<one>)·D \<lsq> f`(m·M)"

proof -

let ?E = "maxδ(f) \<ra> D"

let ?A = "f``(\<int>⇩_{+}) ∩ \<int>⇩_{+}"

from A1 A2 have I: "D\<lsq>?E"

using Int_ZF_1_5_L3 Int_ZF_2_1_L8 Int_ZF_2_L1A Int_ZF_2_L15D

by simp;

from A1 A2 have "?A ⊆ \<int>⇩_{+}" "?A ∉ Fin(\<int>)" "\<two>·?E ∈ \<int>"

using int_two_three_are_int Int_ZF_2_1_L8 PositiveSet_def Int_ZF_1_1_L5

by auto;

with A1 have "∃M∈\<int>⇩_{+}. \<two>·?E \<lsq> f`(M)"

using Int_ZF_1_5_L2A Int_ZF_2_3_L1A by simp;

then obtain M where II: "M∈\<int>⇩_{+}" and III: "\<two>·?E \<lsq> f`(M)"

by auto;

{ fix m assume "m∈\<int>⇩_{+}" then have A4: "\<one>\<lsq>m"

using Int_ZF_1_5_L3 by simp

moreover from II III have "(\<one>\<ra>\<one>) ·?E \<lsq> f`(\<one>·M)"

using PositiveSet_def Int_ZF_1_1_L4 by simp;

moreover have "∀k.

\<one>\<lsq>k ∧ (k\<ra>\<one>)·?E \<lsq> f`(k·M) --> (k\<ra>\<one>\<ra>\<one>)·?E \<lsq> f`((k\<ra>\<one>)·M)"

proof -

{ fix k assume A5: "\<one>\<lsq>k" and A6: "(k\<ra>\<one>)·?E \<lsq> f`(k·M)"

with A1 A2 II have T:

"k∈\<int>" "M∈\<int>" "k\<ra>\<one> ∈ \<int>" "?E∈\<int>" "(k\<ra>\<one>)·?E ∈ \<int>" "\<two>·?E ∈ \<int>"

using Int_ZF_2_L1A PositiveSet_def int_zero_one_are_int

Int_ZF_1_1_L5 Int_ZF_2_1_L8 by auto;

from A1 A2 A5 II have

"δ(f,k·M,M) ∈ \<int>" "abs(δ(f,k·M,M)) \<lsq> maxδ(f)" "\<zero>\<lsq>D"

using Int_ZF_2_L1A PositiveSet_def Int_ZF_1_1_L5

Int_ZF_2_1_L7 Int_ZF_2_L16C by auto;

with III A6 have

"(k\<ra>\<one>)·?E \<ra> (\<two>·?E \<rs> ?E) \<lsq> f`(k·M) \<ra> (f`(M) \<ra> δ(f,k·M,M))"

using Int_ZF_1_3_L19A int_ineq_add_sides by simp;

with A1 T have "(k\<ra>\<one>\<ra>\<one>)·?E \<lsq> f`((k\<ra>\<one>)·M)"

using Int_ZF_1_1_L1 int_zero_one_are_int Int_ZF_1_1_L4

Int_ZF_1_2_L11 Int_ZF_2_1_L13 by simp;

} then show ?thesis by simp;

qed;

ultimately have "(m\<ra>\<one>)·?E \<lsq> f`(m·M)" by (rule Induction_on_int);

with A4 I have "(m\<ra>\<one>)·D \<lsq> f`(m·M)" using Int_ZF_1_3_L13A

by simp;

} then have "∀m∈\<int>⇩_{+}.(m\<ra>\<one>)·D \<lsq> f`(m·M)" by simp;

with II show ?thesis by auto;

qed;

text{*A special case of @{text " Arthan_Lem_3"} when $D=1$.*}

corollary (in int1) Arthan_L_3_spec: assumes A1: "f ∈ \<S>⇩_{+}"

shows "∃M∈\<int>⇩_{+}.∀n∈\<int>⇩_{+}. n\<ra>\<one> \<lsq> f`(n·M)"

proof -

have "∀n∈\<int>⇩_{+}. n\<ra>\<one> ∈ \<int>"

using PositiveSet_def int_zero_one_are_int Int_ZF_1_1_L5

by simp;

then have "∀n∈\<int>⇩_{+}. (n\<ra>\<one>)·\<one> = n\<ra>\<one>"

using Int_ZF_1_1_L4 by simp;

moreover from A1 have "∃M∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. (n\<ra>\<one>)·\<one> \<lsq> f`(n·M)"

using int_one_two_are_pos Arthan_Lem_3 by simp;

ultimately show ?thesis by simp;

qed;

text{*We know from @{text "Group_ZF_3.thy"} that finite range functions are almost homomorphisms.

Besides reminding that fact for slopes the next lemma shows

that finite range functions do not belong to @{text "\<S>⇩_{+}"}.

This is important, because the projection

of the set of finite range functions defines zero in the real number construction in @{text "Real_ZF_x.thy"}

series, while the projection of @{text "\<S>⇩_{+}"} becomes the set of (strictly) positive reals.

We don't want zero to be positive, do we? The next lemma is a part of Lemma 5 in the Arthan's paper

\cite{Arthan2004}.*}

lemma (in int1) Int_ZF_2_3_L1B:

assumes A1: "f ∈ FinRangeFunctions(\<int>,\<int>)"

shows "f∈\<S>" "f ∉ \<S>⇩_{+}"

proof -

from A1 show "f∈\<S>" using Int_ZF_2_1_L1 group1.Group_ZF_3_3_L1

by auto;

have "\<int>⇩_{+}⊆ \<int>" using PositiveSet_def by auto;

with A1 have "f``(\<int>⇩_{+}) ∈ Fin(\<int>)"

using Finite1_L21 by simp;

then have "f``(\<int>⇩_{+}) ∩ \<int>⇩_{+}∈ Fin(\<int>)"

using Fin_subset_lemma by blast;

thus "f ∉ \<S>⇩_{+}" by auto;

qed;

text{*We want to show that if $f$ is a slope and neither $f$ nor $-f$ are in @{text "\<S>⇩_{+}"},

then $f$ is bounded. The next lemma is the first step towards that goal and

shows that if slope is not in @{text "\<S>⇩_{+}"} then $f($@{text "\<int>⇩_{+}"}$)$ is bounded above.*}

lemma (in int1) Int_ZF_2_3_L2: assumes A1: "f∈\<S>" and A2: "f ∉ \<S>⇩_{+}"

shows "IsBoundedAbove(f``(\<int>⇩_{+}), IntegerOrder)"

proof -

from A1 have "f:\<int>->\<int>" using AlmostHoms_def by simp

then have "f``(\<int>⇩_{+}) ⊆ \<int>" using func1_1_L6 by simp;

moreover from A1 A2 have "f``(\<int>⇩_{+}) ∩ \<int>⇩_{+}∈ Fin(\<int>)" by auto;

ultimately show ?thesis using Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L4

by simp;

qed;

text{*If $f$ is a slope and $-f\notin$ @{text "\<S>⇩_{+}"}, then

$f($@{text "\<int>⇩_{+}"}$)$ is bounded below.*}

lemma (in int1) Int_ZF_2_3_L3: assumes A1: "f∈\<S>" and A2: "\<fm>f ∉ \<S>⇩_{+}"

shows "IsBoundedBelow(f``(\<int>⇩_{+}), IntegerOrder)"

proof -

from A1 have T: "f:\<int>->\<int>" using AlmostHoms_def by simp

then have "(\<sm>(f``(\<int>⇩_{+}))) = (\<fm>f)``(\<int>⇩_{+})"

using Int_ZF_1_T2 group0_2_T2 PositiveSet_def func1_1_L15C

by auto;

with A1 A2 T show "IsBoundedBelow(f``(\<int>⇩_{+}), IntegerOrder)"

using Int_ZF_2_1_L12 Int_ZF_2_3_L2 PositiveSet_def func1_1_L6

Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L5 by simp;

qed;

text{* A slope that is bounded on @{text "\<int>⇩_{+}"} is bounded everywhere.*}

lemma (in int1) Int_ZF_2_3_L4:

assumes A1: "f∈\<S>" and A2: "m∈\<int>"

and A3: "∀n∈\<int>⇩_{+}. abs(f`(n)) \<lsq> L"

shows "abs(f`(m)) \<lsq> \<two>·maxδ(f) \<ra> L"

proof -

from A1 A3 have

"\<zero> \<lsq> abs(f`(\<one>))" "abs(f`(\<one>)) \<lsq> L"

using int_zero_one_are_int Int_ZF_2_1_L2B int_abs_nonneg int_one_two_are_pos

by auto;

then have II: "\<zero>\<lsq>L" by (rule Int_order_transitive);

note A2

moreover have "abs(f`(\<zero>)) \<lsq> \<two>·maxδ(f) \<ra> L"

proof -

from A1 have

"abs(f`(\<zero>)) \<lsq> maxδ(f)" "\<zero> \<lsq> maxδ(f)"

and T: "maxδ(f) ∈ \<int>"

using Int_ZF_2_1_L8 by auto;

with II have "abs(f`(\<zero>)) \<lsq> maxδ(f) \<ra> maxδ(f) \<ra> L"

using Int_ZF_2_L15F by simp;

with T show ?thesis using Int_ZF_1_1_L4 by simp;

qed;

moreover from A1 A3 II have

"∀n∈\<int>⇩_{+}. abs(f`(n)) \<lsq> \<two>·maxδ(f) \<ra> L"

using Int_ZF_2_1_L8 Int_ZF_1_3_L5A Int_ZF_2_L15F

by simp;

moreover have "∀n∈\<int>⇩_{+}. abs(f`(\<rm>n)) \<lsq> \<two>·maxδ(f) \<ra> L"

proof;

fix n assume "n∈\<int>⇩_{+}"

with A1 A3 have

"\<two>·maxδ(f) ∈ \<int>"

"abs(f`(\<rm>n)) \<lsq> \<two>·maxδ(f) \<ra> abs(f`(n))"

"abs(f`(n)) \<lsq> L"

using int_two_three_are_int Int_ZF_2_1_L8 Int_ZF_1_1_L5

PositiveSet_def Int_ZF_2_1_L14 by auto;

then show "abs(f`(\<rm>n)) \<lsq> \<two>·maxδ(f) \<ra> L"

using Int_ZF_2_L15A by blast;

qed;

ultimately show ?thesis by (rule Int_ZF_2_L19B);

qed;

text{*A slope whose image of the set of positive integers is bounded

is a finite range function.*}

lemma (in int1) Int_ZF_2_3_L4A:

assumes A1: "f∈\<S>" and A2: "IsBounded(f``(\<int>⇩_{+}), IntegerOrder)"

shows "f ∈ FinRangeFunctions(\<int>,\<int>)"

proof -

have T1: "\<int>⇩_{+}⊆ \<int>" using PositiveSet_def by auto;

from A1 have T2: "f:\<int>->\<int>" using AlmostHoms_def by simp

from A2 obtain L where "∀a∈f``(\<int>⇩_{+}). abs(a) \<lsq> L"

using Int_ZF_1_3_L20A by auto;

with T2 T1 have "∀n∈\<int>⇩_{+}. abs(f`(n)) \<lsq> L"

by (rule func1_1_L15B);

with A1 have "∀m∈\<int>. abs(f`(m)) \<lsq> \<two>·maxδ(f) \<ra> L"

using Int_ZF_2_3_L4 by simp;

with T2 have "f``(\<int>) ∈ Fin(\<int>)"

by (rule Int_ZF_1_3_L20C);

with T2 show "f ∈ FinRangeFunctions(\<int>,\<int>)"

using FinRangeFunctions_def by simp

qed;

text{*A slope whose image of the set of positive integers is bounded

below is a finite range function or a positive slope.*}

lemma (in int1) Int_ZF_2_3_L4B:

assumes "f∈\<S>" and "IsBoundedBelow(f``(\<int>⇩_{+}), IntegerOrder)"

shows "f ∈ FinRangeFunctions(\<int>,\<int>) ∨ f∈\<S>⇩_{+}"

using assms Int_ZF_2_3_L2 IsBounded_def Int_ZF_2_3_L4A

by auto;

text{*If one slope is not greater then another on positive integers,

then they are almost equal or the difference is a positive slope.*}

lemma (in int1) Int_ZF_2_3_L4C: assumes A1: "f∈\<S>" "g∈\<S>" and

A2: "∀n∈\<int>⇩_{+}. f`(n) \<lsq> g`(n)"

shows "f∼g ∨ g \<fp> (\<fm>f) ∈ \<S>⇩_{+}"

proof -

let ?h = "g \<fp> (\<fm>f)"

from A1 have "(\<fm>f) ∈ \<S>" using Int_ZF_2_1_L12

by simp;

with A1 have I: "?h ∈ \<S>" using Int_ZF_2_1_L12C

by simp;

moreover have "IsBoundedBelow(?h``(\<int>⇩_{+}), IntegerOrder)"

proof -

from I have

"?h:\<int>->\<int>" and "\<int>⇩_{+}⊆\<int>" using AlmostHoms_def PositiveSet_def

by auto

moreover from A1 A2 have "∀n∈\<int>⇩_{+}. ⟨\<zero>, ?h`(n)⟩ ∈ IntegerOrder"

using Int_ZF_2_1_L2B PositiveSet_def Int_ZF_1_3_L10A

Int_ZF_2_1_L12 Int_ZF_2_1_L12B Int_ZF_2_1_L12A

by simp;

ultimately show "IsBoundedBelow(?h``(\<int>⇩_{+}), IntegerOrder)"

by (rule func_ZF_8_L1);

qed

ultimately have "?h ∈ FinRangeFunctions(\<int>,\<int>) ∨ ?h∈\<S>⇩_{+}"

using Int_ZF_2_3_L4B by simp

with A1 show "f∼g ∨ g \<fp> (\<fm>f) ∈ \<S>⇩_{+}"

using Int_ZF_2_1_L9C by auto;

qed;

text{*Positive slopes are arbitrarily large for large enough arguments.*}

lemma (in int1) Int_ZF_2_3_L5:

assumes A1: "f∈\<S>⇩_{+}" and A2: "K∈\<int>"

shows "∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> K \<lsq> f`(m)"

proof -

from A1 obtain M where I: "M∈\<int>⇩_{+}" and II: "∀n∈\<int>⇩_{+}. n\<ra>\<one> \<lsq> f`(n·M)"

using Arthan_L_3_spec by auto;

let ?j = "GreaterOf(IntegerOrder,M,K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<rs> \<one>)"

from A1 I have T1:

"minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f) ∈ \<int>" "M∈\<int>"

using Int_ZF_2_1_L15 Int_ZF_2_1_L8 Int_ZF_1_1_L5 PositiveSet_def

by auto;

with A2 I have T2:

"K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) ∈ \<int>"

"K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<rs> \<one> ∈ \<int>"

using Int_ZF_1_1_L5 int_zero_one_are_int by auto;

with T1 have III: "M \<lsq> ?j" and

"K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<rs> \<one> \<lsq> ?j"

using Int_ZF_1_3_L18 by auto;

with A2 T1 T2 have

IV: "K \<lsq> ?j\<ra>\<one> \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f))"

using int_zero_one_are_int Int_ZF_2_L9C by simp;

let ?N = "GreaterOf(IntegerOrder,\<one>,?j·M)"

from T1 III have T3: "?j ∈ \<int>" "?j·M ∈ \<int>"

using Int_ZF_2_L1A Int_ZF_1_1_L5 by auto;

then have V: "?N ∈ \<int>⇩_{+}" and VI: "?j·M \<lsq> ?N"

using int_zero_one_are_int Int_ZF_1_5_L3 Int_ZF_1_3_L18

by auto;

{ fix m

let ?n = "m zdiv M"

let ?k = "m zmod M"

assume "?N\<lsq>m"

with VI have "?j·M \<lsq> m" by (rule Int_order_transitive);

with I III have

VII: "m = ?n·M\<ra>?k"

"?j \<lsq> ?n" and

VIII: "?n ∈ \<int>⇩_{+}" "?k ∈ \<zero>..(M\<rs>\<one>)"

using IntDiv_ZF_1_L5 by auto;

with II have

"?j \<ra> \<one> \<lsq> ?n \<ra> \<one>" "?n\<ra>\<one> \<lsq> f`(?n·M)"

using int_zero_one_are_int int_ord_transl_inv by auto;

then have "?j \<ra> \<one> \<lsq> f`(?n·M)"

by (rule Int_order_transitive);

with T1 have

"?j\<ra>\<one> \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<lsq>

f`(?n·M) \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f))"

using int_ord_transl_inv by simp;

with IV have "K \<lsq> f`(?n·M) \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f))"

by (rule Int_order_transitive);

moreover from A1 I VIII have

"f`(?n·M) \<ra> (minf(f,\<zero>..(M\<rs>\<one>))\<rs> maxδ(f)) \<lsq> f`(?n·M\<ra>?k)"

using PositiveSet_def Int_ZF_2_1_L16 by simp;

ultimately have "K \<lsq> f`(?n·M\<ra>?k)"

by (rule Int_order_transitive);

with VII have "K \<lsq> f`(m)" by simp;

} then have "∀m. ?N\<lsq>m --> K \<lsq> f`(m)"

by simp;

with V show ?thesis by auto;

qed;

text{*Positive slopes are arbitrarily small for small enough arguments.

Kind of dual to @{text "Int_ZF_2_3_L5"}.*}

lemma (in int1) Int_ZF_2_3_L5A: assumes A1: "f∈\<S>⇩_{+}" and A2: "K∈\<int>"

shows "∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> f`(\<rm>m) \<lsq> K"

proof -

from A1 have T1: "abs(f`(\<zero>)) \<ra> maxδ(f) ∈ \<int>"

using Int_ZF_2_1_L8 by auto;

with A2 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K ∈ \<int>"

using Int_ZF_1_1_L5 by simp;

with A1 have

"∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"

using Int_ZF_2_3_L5 by simp;

then obtain N where I: "N∈\<int>⇩_{+}" and II:

"∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"

by auto;

{ fix m assume A3: "N\<lsq>m"

with A1 have

"f`(\<rm>m) \<lsq> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m)"

using Int_ZF_2_L1A Int_ZF_2_1_L14 by simp;

moreover

from II T1 A3 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m) \<lsq>

(abs(f`(\<zero>)) \<ra> maxδ(f)) \<rs>(abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K)"

using Int_ZF_2_L10 int_ord_transl_inv by simp;

with A2 T1 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m) \<lsq> K"

using Int_ZF_1_2_L3 by simp;

ultimately have "f`(\<rm>m) \<lsq> K"

by (rule Int_order_transitive)

} then have "∀m. N\<lsq>m --> f`(\<rm>m) \<lsq> K"

by simp;

with I show ?thesis by auto;

qed;

(*lemma (in int1) Int_ZF_2_3_L5A: assumes A1: "f∈\<S>⇩_{+}" and A2: "K∈\<int>"

shows "∃N∈\<int>⇩_{+}. ∀m. m\<lsq>(\<rm>N) --> f`(m) \<lsq> K"

proof -

from A1 have T1: "abs(f`(\<zero>)) \<ra> maxδ(f) ∈ \<int>"

using Int_ZF_2_1_L8 by auto;

with A2 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K ∈ \<int>"

using Int_ZF_1_1_L5 by simp;

with A1 have

"∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"

using Int_ZF_2_3_L5 by simp;

then obtain N where I: "N∈\<int>⇩_{+}" and II:

"∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"

by auto;

{ fix m assume A3: "m\<lsq>(\<rm>N)"

with A1 have T2: "f`(m) ∈ \<int>"

using Int_ZF_2_L1A Int_ZF_2_1_L2B by simp;

from A1 I II A3 have

"abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(\<rm>m)" and

"f`(\<rm>m) \<lsq> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m)"

using PositiveSet_def Int_ZF_2_L10AA Int_ZF_2_L1A Int_ZF_2_1_L14

by auto;

then have

"abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m)"

by (rule Int_order_transitive)

with T1 A2 T2 have "f`(m) \<lsq> K"

using Int_ZF_2_L10AB by simp;

} then have "∀m. m\<lsq>(\<rm>N) --> f`(m) \<lsq> K"

by simp;

with I show ?thesis by auto;

qed;*)

text{*A special case of @{text "Int_ZF_2_3_L5"} where $K=1$.*}

corollary (in int1) Int_ZF_2_3_L6: assumes "f∈\<S>⇩_{+}"

shows "∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> f`(m) ∈ \<int>⇩_{+}"

using assms int_zero_one_are_int Int_ZF_2_3_L5 Int_ZF_1_5_L3

by simp;

text{*A special case of @{text "Int_ZF_2_3_L5"} where $m=N$.*}

corollary (in int1) Int_ZF_2_3_L6A: assumes "f∈\<S>⇩_{+}" and "K∈\<int>"

shows "∃N∈\<int>⇩_{+}. K \<lsq> f`(N)"

proof -

from assms have "∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> K \<lsq> f`(m)"

using Int_ZF_2_3_L5 by simp;

then obtain N where I: "N ∈ \<int>⇩_{+}" and II: "∀m. N\<lsq>m --> K \<lsq> f`(m)"

by auto;

then show ?thesis using PositiveSet_def int_ord_is_refl refl_def

by auto;

qed;

text{*If values of a slope are not bounded above,

then the slope is positive.*}

lemma (in int1) Int_ZF_2_3_L7: assumes A1: "f∈\<S>"

and A2: "∀K∈\<int>. ∃n∈\<int>⇩_{+}. K \<lsq> f`(n)"

shows "f ∈ \<S>⇩_{+}"

proof -

{ fix K assume "K∈\<int>"

with A2 obtain n where "n∈\<int>⇩_{+}" "K \<lsq> f`(n)"

by auto

moreover from A1 have "\<int>⇩_{+}⊆ \<int>" "f:\<int>->\<int>"

using PositiveSet_def AlmostHoms_def by auto

ultimately have "∃m ∈ f``(\<int>⇩_{+}). K \<lsq> m"

using func1_1_L15D by auto;

} then have "∀K∈\<int>. ∃m ∈ f``(\<int>⇩_{+}). K \<lsq> m" by simp;

with A1 show "f ∈ \<S>⇩_{+}" using Int_ZF_4_L9 Int_ZF_2_3_L2

by auto;

qed;

text{*For unbounded slope $f$ either $f\in$@{text "\<S>⇩_{+}"} of

$-f\in$@{text "\<S>⇩_{+}"}.*}

theorem (in int1) Int_ZF_2_3_L8:

assumes A1: "f∈\<S>" and A2: "f ∉ FinRangeFunctions(\<int>,\<int>)"

shows "(f ∈ \<S>⇩_{+}) Xor ((\<fm>f) ∈ \<S>⇩_{+})"

proof -

have T1: "\<int>⇩_{+}⊆ \<int>" using PositiveSet_def by auto;

from A1 have T2: "f:\<int>->\<int>" using AlmostHoms_def by simp

then have I: "f``(\<int>⇩_{+}) ⊆ \<int>" using func1_1_L6 by auto;

from A1 A2 have "f ∈ \<S>⇩_{+}∨ (\<fm>f) ∈ \<S>⇩_{+}"

using Int_ZF_2_3_L2 Int_ZF_2_3_L3 IsBounded_def Int_ZF_2_3_L4A

by blast;

moreover have "¬(f ∈ \<S>⇩_{+}∧ (\<fm>f) ∈ \<S>⇩_{+})"

proof -

{ assume A3: "f ∈ \<S>⇩_{+}" and A4: "(\<fm>f) ∈ \<S>⇩_{+}"

from A3 obtain N1 where

I: "N1∈\<int>⇩_{+}" and II: "∀m. N1\<lsq>m --> f`(m) ∈ \<int>⇩_{+}"

using Int_ZF_2_3_L6 by auto;

from A4 obtain N2 where

III: "N2∈\<int>⇩_{+}" and IV: "∀m. N2\<lsq>m --> (\<fm>f)`(m) ∈ \<int>⇩_{+}"

using Int_ZF_2_3_L6 by auto;

let ?N = "GreaterOf(IntegerOrder,N1,N2)"

from I III have "N1 \<lsq> ?N" "N2 \<lsq> ?N"

using PositiveSet_def Int_ZF_1_3_L18 by auto;

with A1 II IV have

"f`(?N) ∈ \<int>⇩_{+}" "(\<fm>f)`(?N) ∈ \<int>⇩_{+}" "(\<fm>f)`(?N) = \<rm>(f`(?N))"

using Int_ZF_2_L1A PositiveSet_def Int_ZF_2_1_L12A

by auto;

then have False using Int_ZF_1_5_L8 by simp;

} thus ?thesis by auto

qed;

ultimately show "(f ∈ \<S>⇩_{+}) Xor ((\<fm>f) ∈ \<S>⇩_{+})"

using Xor_def by simp

qed;

text{*The sum of positive slopes is a positive slope.*}

theorem (in int1) sum_of_pos_sls_is_pos_sl:

assumes A1: "f ∈ \<S>⇩_{+}" "g ∈ \<S>⇩_{+}"

shows "f\<fp>g ∈ \<S>⇩_{+}"

proof -

{ fix K assume "K∈\<int>"

with A1 have "∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> K \<lsq> f`(m)"

using Int_ZF_2_3_L5 by simp;

then obtain N where I: "N∈\<int>⇩_{+}" and II: "∀m. N\<lsq>m --> K \<lsq> f`(m)"

by auto;

from A1 have "∃M∈\<int>⇩_{+}. ∀m. M\<lsq>m --> \<zero> \<lsq> g`(m)"

using int_zero_one_are_int Int_ZF_2_3_L5 by simp;

then obtain M where III: "M∈\<int>⇩_{+}" and IV: "∀m. M\<lsq>m --> \<zero> \<lsq> g`(m)"

by auto;

let ?L = "GreaterOf(IntegerOrder,N,M)"

from I III have V: "?L ∈ \<int>⇩_{+}" "\<int>⇩_{+}⊆ \<int>"

using GreaterOf_def PositiveSet_def by auto

moreover from A1 V have "(f\<fp>g)`(?L) = f`(?L) \<ra> g`(?L)"

using Int_ZF_2_1_L12B by auto;

moreover from I II III IV have "K \<lsq> f`(?L) \<ra> g`(?L)"

using PositiveSet_def Int_ZF_1_3_L18 Int_ZF_2_L15F

by simp;

ultimately have "?L ∈ \<int>⇩_{+}" "K \<lsq> (f\<fp>g)`(?L)"

by auto;

then have "∃n ∈\<int>⇩_{+}. K \<lsq> (f\<fp>g)`(n)"

by auto;

} with A1 show "f\<fp>g ∈ \<S>⇩_{+}"

using Int_ZF_2_1_L12C Int_ZF_2_3_L7 by simp;

qed

text{*The composition of positive slopes is a positive slope.*}

theorem (in int1) comp_of_pos_sls_is_pos_sl:

assumes A1: "f ∈ \<S>⇩_{+}" "g ∈ \<S>⇩_{+}"

shows "fog ∈ \<S>⇩_{+}"

proof -

{ fix K assume "K∈\<int>"

with A1 have "∃N∈\<int>⇩_{+}. ∀m. N\<lsq>m --> K \<lsq> f`(m)"

using Int_ZF_2_3_L5 by simp;

then obtain N where "N∈\<int>⇩_{+}" and I: "∀m. N\<lsq>m --> K \<lsq> f`(m)"

by auto;

with A1 have "∃M∈\<int>⇩_{+}. N \<lsq> g`(M)"

using PositiveSet_def Int_ZF_2_3_L6A by simp;

then obtain M where "M∈\<int>⇩_{+}" "N \<lsq> g`(M)"

by auto;

with A1 I have "∃M∈\<int>⇩_{+}. K \<lsq> (fog)`(M)"

using PositiveSet_def Int_ZF_2_1_L10

by auto;

} with A1 show "fog ∈ \<S>⇩_{+}"

using Int_ZF_2_1_L11 Int_ZF_2_3_L7

by simp;

qed;

text{*A slope equivalent to a positive one is positive.*}

lemma (in int1) Int_ZF_2_3_L9:

assumes A1: "f ∈ \<S>⇩_{+}" and A2: "⟨f,g⟩ ∈ AlEqRel" shows "g ∈ \<S>⇩_{+}"

proof -

from A2 have T: "g∈\<S>" and "∃L∈\<int>. ∀m∈\<int>. abs(f`(m)\<rs>g`(m)) \<lsq> L"

using Int_ZF_2_1_L9A by auto;

then obtain L where

I: "L∈\<int>" and II: "∀m∈\<int>. abs(f`(m)\<rs>g`(m)) \<lsq> L"

by auto;

{ fix K assume A3: "K∈\<int>"

with I have "K\<ra>L ∈ \<int>"

using Int_ZF_1_1_L5 by simp;

with A1 obtain M where III: "M∈\<int>⇩_{+}" and IV: "K\<ra>L \<lsq> f`(M)"

using Int_ZF_2_3_L6A by auto;

with A1 A3 I have "K \<lsq> f`(M)\<rs>L"

using PositiveSet_def Int_ZF_2_1_L2B Int_ZF_2_L9B

by simp;

moreover from A1 T II III have

"f`(M)\<rs>L \<lsq> g`(M)"

using PositiveSet_def Int_ZF_2_1_L2B Int_triangle_ineq2

by simp;

ultimately have "K \<lsq> g`(M)"

by (rule Int_order_transitive);

with III have "∃n∈\<int>⇩_{+}. K \<lsq> g`(n)"

by auto;

} with T show "g ∈ \<S>⇩_{+}"

using Int_ZF_2_3_L7 by simp;

qed;

text{* The set of positive slopes is saturated with respect to the relation of

equivalence of slopes.*}

lemma (in int1) pos_slopes_saturated: shows "IsSaturated(AlEqRel,\<S>⇩_{+})"

proof -

have

"equiv(\<S>,AlEqRel)"

"AlEqRel ⊆ \<S> × \<S>"

using Int_ZF_2_1_L9B by auto

moreover have "\<S>⇩_{+}⊆ \<S>" by auto

moreover have "∀f∈\<S>⇩_{+}. ∀g∈\<S>. ⟨f,g⟩ ∈ AlEqRel --> g ∈ \<S>⇩_{+}"

using Int_ZF_2_3_L9 by blast;

ultimately show "IsSaturated(AlEqRel,\<S>⇩_{+})"

by (rule EquivClass_3_L3);

qed;

text{*A technical lemma involving a projection of the set of positive slopes

and a logical epression with exclusive or.*}

lemma (in int1) Int_ZF_2_3_L10:

assumes A1: "f∈\<S>" "g∈\<S>"

and A2: "R = {AlEqRel``{s}. s∈\<S>⇩_{+}}"

and A3: "(f∈\<S>⇩_{+}) Xor (g∈\<S>⇩_{+})"

shows "(AlEqRel``{f} ∈ R) Xor (AlEqRel``{g} ∈ R)"

proof -

from A1 A2 A3 have

"equiv(\<S>,AlEqRel)"

"IsSaturated(AlEqRel,\<S>⇩_{+})"

"\<S>⇩_{+}⊆ \<S>"

"f∈\<S>" "g∈\<S>"

"R = {AlEqRel``{s}. s∈\<S>⇩_{+}}"

"(f∈\<S>⇩_{+}) Xor (g∈\<S>⇩_{+})"

using pos_slopes_saturated Int_ZF_2_1_L9B by auto;

then show ?thesis by (rule EquivClass_3_L7);

qed;

text{*Identity function is a positive slope.*}

lemma (in int1) Int_ZF_2_3_L11: shows "id(\<int>) ∈ \<S>⇩_{+}"

proof -

let ?f = "id(\<int>)"

{ fix K assume "K∈\<int>"

then obtain n where T: "n∈\<int>⇩_{+}" and "K\<lsq>n"

using Int_ZF_1_5_L9 by auto;

moreover from T have "?f`(n) = n"

using PositiveSet_def by simp;

ultimately have "n∈\<int>⇩_{+}" and "K\<lsq>?f`(n)"

by auto;

then have "∃n∈\<int>⇩_{+}. K\<lsq>?f`(n)" by auto;

} then show "?f ∈ \<S>⇩_{+}"

using Int_ZF_2_1_L17 Int_ZF_2_3_L7 by simp;

qed;

text{*The identity function is not almost equal to any bounded function.*}

lemma (in int1) Int_ZF_2_3_L12: assumes A1: "f ∈ FinRangeFunctions(\<int>,\<int>)"

shows "¬(id(\<int>) ∼ f)"

proof -

{ from A1 have "id(\<int>) ∈ \<S>⇩_{+}"

using Int_ZF_2_3_L11 by simp

moreover assume "⟨id(\<int>),f⟩ ∈ AlEqRel"

ultimately have "f ∈ \<S>⇩_{+}"

by (rule Int_ZF_2_3_L9);

with A1 have False using Int_ZF_2_3_L1B

by simp;

} then show "¬(id(\<int>) ∼ f)" by auto;

qed;

section{*Inverting slopes*}

text{*Not every slope is a 1:1 function. However, we can still invert slopes

in the sense that if $f$ is a slope, then we can find a slope $g$ such that

$f\circ g$ is almost equal to the identity function.

The goal of this this section is to establish this fact for positive slopes.

*}

text{*If $f$ is a positive slope, then for every positive integer $p$

the set $\{n\in Z_+: p\leq f(n)\}$ is a nonempty subset of positive integers.

Recall that $f^{-1}(p)$ is the notation for the smallest element of this set.*}

lemma (in int1) Int_ZF_2_4_L1:

assumes A1: "f ∈ \<S>⇩_{+}" and A2: "p∈\<int>⇩_{+}" and A3: "A = {n∈\<int>⇩_{+}. p \<lsq> f`(n)}"

shows

"A ⊆ \<int>⇩_{+}"

"A ≠ 0"

"f¯(p) ∈ A"

"∀m∈A. f¯(p) \<lsq> m"

proof -

from A3 show I: "A ⊆ \<int>⇩_{+}" by auto

from A1 A2 have "∃n∈\<int>⇩_{+}. p \<lsq> f`(n)"

using PositiveSet_def Int_ZF_2_3_L6A by simp;

with A3 show II: "A ≠ 0" by auto;

from A3 I II show

"f¯(p) ∈ A"

"∀m∈A. f¯(p) \<lsq> m"

using Int_ZF_1_5_L1C by auto;

qed;

text{*If $f$ is a positive slope and $p$ is a positive integer $p$, then

$f^{-1}(p)$ (defined as the minimum of the set $\{n\in Z_+: p\leq f(n)\}$ )

is a (well defined) positive integer.*}

lemma (in int1) Int_ZF_2_4_L2:

assumes "f ∈ \<S>⇩_{+}" and "p∈\<int>⇩_{+}"

shows

"f¯(p) ∈ \<int>⇩_{+}"

"p \<lsq> f`(f¯(p))"

using assms Int_ZF_2_4_L1 by auto;

text{*If $f$ is a positive slope and $p$ is a positive integer such

that $n\leq f(p)$, then

$f^{-1}(n) \leq p$.*}

lemma (in int1) Int_ZF_2_4_L3:

assumes "f ∈ \<S>⇩_{+}" and "m∈\<int>⇩_{+}" "p∈\<int>⇩_{+}" and "m \<lsq> f`(p)"

shows "f¯(m) \<lsq> p"

using assms Int_ZF_2_4_L1 by simp;

text{*An upper bound $f(f^{-1}(m) -1)$ for positive slopes.*}

lemma (in int1) Int_ZF_2_4_L4:

assumes A1: "f ∈ \<S>⇩_{+}" and A2: "m∈\<int>⇩_{+}" and A3: "f¯(m)\<rs>\<one> ∈ \<int>⇩_{+}"

shows "f`(f¯(m)\<rs>\<one>) \<lsq> m" "f`(f¯(m)\<rs>\<one>) ≠ m"

proof -

from A1 A2 have T: "f¯(m) ∈ \<int>" using Int_ZF_2_4_L2 PositiveSet_def

by simp;

from A1 A3 have "f:\<int>->\<int>" and "f¯(m)\<rs>\<one> ∈ \<int>"

using Int_ZF_2_3_L1 PositiveSet_def by auto;

with A1 A2 have T1: "f`(f¯(m)\<rs>\<one>) ∈ \<int>" "m∈\<int>"

using apply_funtype PositiveSet_def by auto;

{ assume "m \<lsq> f`(f¯(m)\<rs>\<one>)"

with A1 A2 A3 have "f¯(m) \<lsq> f¯(m)\<rs>\<one>"

by (rule Int_ZF_2_4_L3);

with T have False using Int_ZF_1_2_L3AA

by simp;

} then have I: "¬(m \<lsq> f`(f¯(m)\<rs>\<one>))" by auto;

with T1 show "f`(f¯(m)\<rs>\<one>) \<lsq> m"

by (rule Int_ZF_2_L19);

from T1 I show "f`(f¯(m)\<rs>\<one>) ≠ m"

by (rule Int_ZF_2_L19);

qed;

text{*The (candidate for) the inverse of a positive slope is nondecreasing.*}

lemma (in int1) Int_ZF_2_4_L5:

assumes A1: "f ∈ \<S>⇩_{+}" and A2: "m∈\<int>⇩_{+}" and A3: "m\<lsq>n"

shows "f¯(m) \<lsq> f¯(n)"

proof -

from A2 A3 have T: "n ∈ \<int>⇩_{+}" using Int_ZF_1_5_L7 by blast;

with A1 have "n \<lsq> f`(f¯(n))" using Int_ZF_2_4_L2

by simp;

with A3 have "m \<lsq> f`(f¯(n))" by (rule Int_order_transitive)

with A1 A2 T show "f¯(m) \<lsq> f¯(n)"

using Int_ZF_2_4_L2 Int_ZF_2_4_L3 by simp;

qed;

text{*If $f^{-1}(m)$ is positive and $n$ is a positive integer, then,

then $f^{-1}(m+n)-1$ is positive.*}

lemma (in int1) Int_ZF_2_4_L6:

assumes A1: "f ∈ \<S>⇩_{+}" and A2: "m∈\<int>⇩_{+}" "n∈\<int>⇩_{+}" and

A3: "f¯(m)\<rs>\<one> ∈ \<int>⇩_{+}"

shows "f¯(m\<ra>n)\<rs>\<one> ∈ \<int>⇩_{+}"

proof -

from A1 A2 have "f¯(m)\<rs>\<one> \<lsq> f¯(m\<ra>n) \<rs> \<one>"

using PositiveSet_def Int_ZF_1_5_L7A Int_ZF_2_4_L2

Int_ZF_2_4_L5 int_zero_one_are_int Int_ZF_1_1_L4

int_ord_transl_inv by simp;

with A3 show "f¯(m\<ra>n)\<rs>\<one> ∈ \<int>⇩_{+}" using Int_ZF_1_5_L7

by blast;

qed;

text{*If $f$ is a slope, then $f(f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n))$ is

uniformly bounded above and below. Will it be the messiest IsarMathLib

proof ever? Only time will tell.*}

lemma (in int1) Int_ZF_2_4_L7: assumes A1: "f ∈ \<S>⇩_{+}" and

A2: "∀m∈\<int>⇩_{+}. f¯(m)\<rs>\<one> ∈ \<int>⇩_{+}"

shows

"∃U∈\<int>. ∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"

"∃N∈\<int>. ∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"

proof -

from A1 have "∃L∈\<int>. ∀r∈\<int>. f`(r) \<lsq> f`(r\<rs>\<one>) \<ra> L"

using Int_ZF_2_1_L28 by simp;

then obtain L where

I: "L∈\<int>" and II: "∀r∈\<int>. f`(r) \<lsq> f`(r\<rs>\<one>) \<ra> L"

by auto;

from A1 have

"∃M∈\<int>. ∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r\<rs>p\<rs>q) \<lsq> f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>M"

"∃K∈\<int>. ∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>K \<lsq> f`(r\<rs>p\<rs>q)"

using Int_ZF_2_1_L30 by auto

then obtain M K where III: "M∈\<int>" and

IV: "∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r\<rs>p\<rs>q) \<lsq> f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>M"

and

V: "K∈\<int>" and VI: "∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>K \<lsq> f`(r\<rs>p\<rs>q)"

by auto;

from I III V have

"L\<ra>M ∈ \<int>" "(\<rm>L) \<rs> L \<ra> K ∈ \<int>"

using Int_ZF_1_1_L4 Int_ZF_1_1_L5 by auto;

moreover

{ fix m n

assume A3: "m∈\<int>⇩_{+}" "n∈\<int>⇩_{+}"

have "f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> L\<ra>M ∧

(\<rm>L)\<rs>L\<ra>K \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"

proof -

let ?r = "f¯(m\<ra>n)"

let ?p = "f¯(m)"

let ?q = "f¯(n)"

from A1 A3 have T1:

"?p ∈ \<int>⇩_{+}" "?q ∈ \<int>⇩_{+}" "?r ∈ \<int>⇩_{+}"

using Int_ZF_2_4_L2 pos_int_closed_add_unfolded by auto;

with A3 have T2:

"m ∈ \<int>" "n ∈ \<int>" "?p ∈ \<int>" "?q ∈ \<int>" "?r ∈ \<int>"

using PositiveSet_def by auto;

from A2 A3 have T3:

"?r\<rs>\<one> ∈ \<int>⇩_{+}" "?p\<rs>\<one> ∈ \<int>⇩_{+}" "?q\<rs>\<one> ∈ \<int>⇩_{+}"

using pos_int_closed_add_unfolded by auto;

from A1 A3 have VII:

"m\<ra>n \<lsq> f`(?r)"

"m \<lsq> f`(?p)"

"n \<lsq> f`(?q)"

using Int_ZF_2_4_L2 pos_int_closed_add_unfolded by auto;

from A1 A3 T3 have VIII:

"f`(?r\<rs>\<one>) \<lsq> m\<ra>n"

"f`(?p\<rs>\<one>) \<lsq> m"

"f`(?q\<rs>\<one>) \<lsq> n"

using pos_int_closed_add_unfolded Int_ZF_2_4_L4 by auto;

have "f`(?r\<rs>?p\<rs>?q) \<lsq> L\<ra>M"

proof -

from IV T2 have "f`(?r\<rs>?p\<rs>?q) \<lsq> f`(?r)\<rs>f`(?p)\<rs>f`(?q)\<ra>M"

by simp;

moreover

from I II T2 VIII have

"f`(?r) \<lsq> f`(?r\<rs>\<one>) \<ra> L"

"f`(?r\<rs>\<one>) \<ra> L \<lsq> m\<ra>n\<ra>L"

using int_ord_transl_inv by auto;

then have "f`(?r) \<lsq> m\<ra>n\<ra>L"

by (rule Int_order_transitive);

with VII have "f`(?r) \<rs> f`(?p) \<lsq> m\<ra>n\<ra>L\<rs>m"

using int_ineq_add_sides by simp;

with I T2 VII have "f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<lsq> n\<ra>L\<rs>n"

using Int_ZF_1_2_L9 int_ineq_add_sides by simp;

with I III T2 have "f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<ra> M \<lsq> L\<ra>M"

using Int_ZF_1_2_L3 int_ord_transl_inv by simp;

ultimately show "f`(?r\<rs>?p\<rs>?q) \<lsq> L\<ra>M"

by (rule Int_order_transitive);

qed

moreover have "(\<rm>L)\<rs>L \<ra>K \<lsq> f`(?r\<rs>?p\<rs>?q)"

proof -

from I II T2 VIII have

"f`(?p) \<lsq> f`(?p\<rs>\<one>) \<ra> L"

"f`(?p\<rs>\<one>) \<ra> L \<lsq> m \<ra>L"

using int_ord_transl_inv by auto;

then have "f`(?p) \<lsq> m \<ra>L"

by (rule Int_order_transitive);

with VII have "m\<ra>n \<rs>(m\<ra>L) \<lsq> f`(?r) \<rs> f`(?p)"

using int_ineq_add_sides by simp;

with I T2 have "n \<rs> L \<lsq> f`(?r) \<rs> f`(?p)"

using Int_ZF_1_2_L9 by simp;

moreover

from I II T2 VIII have

"f`(?q) \<lsq> f`(?q\<rs>\<one>) \<ra> L"

"f`(?q\<rs>\<one>) \<ra> L \<lsq> n \<ra>L"

using int_ord_transl_inv by auto;

then have "f`(?q) \<lsq> n \<ra>L"

by (rule Int_order_transitive);

ultimately have

"n \<rs> L \<rs> (n\<ra>L) \<lsq> f`(?r) \<rs> f`(?p) \<rs> f`(?q)"

using int_ineq_add_sides by simp;

with I V T2 have

"(\<rm>L)\<rs>L \<ra>K \<lsq> f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<ra> K"

using Int_ZF_1_2_L3 int_ord_transl_inv by simp;

moreover from VI T2 have

"f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<ra> K \<lsq> f`(?r\<rs>?p\<rs>?q)"

by simp;

ultimately show "(\<rm>L)\<rs>L \<ra>K \<lsq> f`(?r\<rs>?p\<rs>?q)"

by (rule Int_order_transitive);

qed

ultimately show

"f`(?r\<rs>?p\<rs>?q) \<lsq> L\<ra>M ∧

(\<rm>L)\<rs>L\<ra>K \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"

by simp

qed

}

ultimately show

"∃U∈\<int>. ∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"

"∃N∈\<int>. ∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"

by auto;

qed;

text{*The expression $f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n)$ is uniformly bounded

for all pairs $\langle m,n \rangle \in$ @{text "\<int>⇩_{+}×\<int>⇩_{+}"}.

Recall that in the @{text "int1"}

context @{text "ε(f,x)"} is defined so that

$\varepsilon(f,\langle m,n \rangle ) = f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n)$.*}

lemma (in int1) Int_ZF_2_4_L8: assumes A1: "f ∈ \<S>⇩_{+}" and

A2: "∀m∈\<int>⇩_{+}. f¯(m)\<rs>\<one> ∈ \<int>⇩_{+}"

shows "∃M. ∀x∈\<int>⇩_{+}×\<int>⇩_{+}. abs(ε(f,x)) \<lsq> M"

proof -

from A1 A2 have

"∃U∈\<int>. ∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"

"∃N∈\<int>. ∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"

using Int_ZF_2_4_L7 by auto;

then obtain U N where I:

"∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"

"∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"

by auto;

have "\<int>⇩_{+}×\<int>⇩_{+}≠ 0" using int_one_two_are_pos by auto;

moreover from A1 have "f: \<int>->\<int>"

using AlmostHoms_def by simp;

moreover from A1 have

"∀a∈\<int>.∃b∈\<int>⇩_{+}.∀x. b\<lsq>x --> a \<lsq> f`(x)"

using Int_ZF_2_3_L5 by simp;

moreover from A1 have

"∀a∈\<int>.∃b∈\<int>⇩_{+}.∀y. b\<lsq>y --> f`(\<rm>y) \<lsq> a"

using Int_ZF_2_3_L5A by simp;

moreover have

"∀x∈\<int>⇩_{+}×\<int>⇩_{+}. ε(f,x) ∈ \<int> ∧ f`(ε(f,x)) \<lsq> U ∧ N \<lsq> f`(ε(f,x))"

proof -

{ fix x assume A3: "x ∈ \<int>⇩_{+}×\<int>⇩_{+}"

let ?m = "fst(x)"

let ?n = "snd(x)"

from A3 have T: "?m ∈ \<int>⇩_{+}" "?n ∈ \<int>⇩_{+}" "?m\<ra>?n ∈ \<int>⇩_{+}"

using pos_int_closed_add_unfolded by auto;

with A1 have

"f¯(?m\<ra>?n) ∈ \<int>" "f¯(?m) ∈ \<int>" "f¯(?n) ∈ \<int>"

using Int_ZF_2_4_L2 PositiveSet_def by auto;

with I T have

"ε(f,x) ∈ \<int> ∧ f`(ε(f,x)) \<lsq> U ∧ N \<lsq> f`(ε(f,x))"

using Int_ZF_1_1_L5 by auto;

} thus ?thesis by simp;

qed;

ultimately show "∃M.∀x∈\<int>⇩_{+}×\<int>⇩_{+}. abs(ε(f,x)) \<lsq> M"

by (rule Int_ZF_1_6_L4);

qed;

text{*The (candidate for) inverse of a positive slope is a (well defined)

function on @{text "\<int>⇩_{+}"}.*}

lemma (in int1) Int_ZF_2_4_L9:

assumes A1: "f ∈ \<S>⇩_{+}" and A2: "g = {⟨p,f¯(p)⟩. p∈\<int>⇩_{+}}"

shows

"g : \<int>⇩_{+}->\<int>⇩_{+}"

"g : \<int>⇩_{+}->\<int>"

proof -

from A1 have

"∀p∈\<int>⇩_{+}. f¯(p) ∈ \<int>⇩_{+}"

"∀p∈\<int>⇩_{+}. f¯(p) ∈ \<int>"

using Int_ZF_2_4_L2 PositiveSet_def by auto;

with A2 show

"g : \<int>⇩_{+}->\<int>⇩_{+}" and "g : \<int>⇩_{+}->\<int>"

using ZF_fun_from_total by auto;

qed;

text{*What are the values of the (candidate for) the inverse of a positive slope?*}

lemma (in int1) Int_ZF_2_4_L10:

assumes A1: "f ∈ \<S>⇩_{+}" and A2: "g = {⟨p,f¯(p)⟩. p∈\<int>⇩_{+}}" and A3: "p∈\<int>⇩_{+}"

shows "g`(p) = f¯(p)"

proof -

from A1 A2 have "g : \<int>⇩_{+}->\<int>⇩_{+}" using Int_ZF_2_4_L9 by simp;

with A2 A3 show "g`(p) = f¯(p)" using ZF_fun_from_tot_val by simp;

qed;

text{*The (candidate for) the inverse of a positive slope is a slope.*}

lemma (in int1) Int_ZF_2_4_L11: assumes A1: "f ∈ \<S>⇩_{+}" and

A2: "∀m∈\<int>⇩_{+}. f¯(m)\<rs>\<one> ∈ \<int>⇩_{+}" and

A3: "g = {⟨p,f¯(p)⟩. p∈\<int>⇩_{+}}"

shows "OddExtension(\<int>,IntegerAddition,IntegerOrder,g) ∈ \<S>"

proof -

from A1 A2 have "∃L. ∀x∈\<int>⇩_{+}×\<int>⇩_{+}. abs(ε(f,x)) \<lsq> L"

using Int_ZF_2_4_L8 by simp;

then obtain L where I: "∀x∈\<int>⇩_{+}×\<int>⇩_{+}. abs(ε(f,x)) \<lsq> L"

by auto;

from A1 A3 have "g : \<int>⇩_{+}->\<int>" using Int_ZF_2_4_L9

by simp;

moreover have "∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. abs(δ(g,m,n)) \<lsq> L"

proof-

{ fix m n

assume A4: "m∈\<int>⇩_{+}" "n∈\<int>⇩_{+}"

then have "⟨m,n⟩ ∈ \<int>⇩_{+}×\<int>⇩_{+}" by simp

with I have "abs(ε(f,⟨m,n⟩)) \<lsq> L" by simp;

moreover have "ε(f,⟨m,n⟩) = f¯(m\<ra>n) \<rs> f¯(m) \<rs> f¯(n)"

by simp;

moreover from A1 A3 A4 have

"f¯(m\<ra>n) = g`(m\<ra>n)" "f¯(m) = g`(m)" "f¯(n) = g`(n)"

using pos_int_closed_add_unfolded Int_ZF_2_4_L10 by auto;

ultimately have "abs(δ(g,m,n)) \<lsq> L" by simp;

} thus "∀m∈\<int>⇩_{+}. ∀n∈\<int>⇩_{+}. abs(δ(g,m,n)) \<lsq> L" by simp

qed

ultimately show ?thesis by (rule Int_ZF_2_1_L24);

qed;

text{*Every positive slope that is at least $2$ on positive integers

almost has an inverse.*}

lemma (in int1) Int_ZF_2_4_L12: assumes A1: "f ∈ \<S>⇩_{+}" and

A2: "∀m∈\<int>⇩_{+}. f¯(m)\<rs>\<one> ∈ \<int>⇩_{+}"

shows "∃h∈\<S>. foh ∼ id(\<int>)"

proof -

let ?g = "{⟨p,f¯(p)⟩. p∈\<int>⇩_{+}}"

let ?h = "OddExtension(\<int>,IntegerAddition,IntegerOrder,?g)"

from A1 have

"∃M∈\<int>. ∀n∈\<int>. f`(n) \<lsq> f`(n\<rs>\<one>) \<ra> M"

using Int_ZF_2_1_L28 by simp;

then obtain M where

I: "M∈\<int>" and II: "∀n∈\<int>. f`(n) \<lsq> f`(n\<rs>\<one>) \<ra> M"

by auto;

from A1 A2 have T: "?h ∈ \<S>"

using Int_ZF_2_4_L11 by simp

moreover have "fo?h ∼ id(\<int>)"

proof -

from A1 T have "fo?h ∈ \<S>" using Int_ZF_2_1_L11

by simp;

moreover note I

moreover

{ fix m assume A3: "m∈\<int>⇩_{+}"

with A1 have "f¯(m) ∈ \<int>"

using Int_ZF_2_4_L2 PositiveSet_def by simp;

with II have "f`(f¯(m)) \<lsq> f`(f¯(m)\<rs>\<one>) \<ra> M"

by simp;

moreover from A1 A2 I A3 have "f`(f¯(m)\<rs>\<one>) \<ra> M \<lsq> m\<ra>M"

using Int_ZF_2_4_L4 int_ord_transl_inv by simp;

ultimately have "f`(f¯(m)) \<lsq> m\<ra>M"

by (rule Int_order_transitive);

moreover from A1 A3 have "m \<lsq> f`(f¯(m))"

using Int_ZF_2_4_L2 by simp;

moreover from A1 A2 T A3 have "f`(f¯(m)) = (fo?h)`(m)"

using Int_ZF_2_4_L9 Int_ZF_1_5_L11

Int_ZF_2_4_L10 PositiveSet_def Int_ZF_2_1_L10

by simp;

ultimately have "m \<lsq> (fo?h)`(m) ∧ (fo?h)`(m) \<lsq> m\<ra>M"

by simp; }

ultimately show "fo?h ∼ id(\<int>)" using Int_ZF_2_1_L32

by simp

qed

ultimately show "∃h∈\<S>. foh ∼ id(\<int>)"

by auto

qed;

text{* @{text "Int_ZF_2_4_L12"} is almost what we need, except that it has an assumption

that the values of the slope that we get the inverse for are not smaller than $2$ on

positive integers. The Arthan's proof of Theorem 11 has a mistake where he says "note that

for all but finitely many $m,n\in N$ $p=g(m)$ and $q=g(n)$ are both positive". Of course

there may be infinitely many pairs $\langle m,n \rangle$ such that $p,q$ are not both

positive. This is however easy to workaround: we just modify the slope by adding a

constant so that the slope is large enough on positive integers and then look

for the inverse.*}

theorem (in int1) pos_slope_has_inv: assumes A1: "f ∈ \<S>⇩_{+}"

shows "∃g∈\<S>. f∼g ∧ (∃h∈\<S>. goh ∼ id(\<int>))"

proof -

from A1 have "f: \<int>->\<int>" "\<one>∈\<int>" "\<two> ∈ \<int>"

using AlmostHoms_def int_zero_one_are_int int_two_three_are_int

by auto

moreover from A1 have

"∀a∈\<int>.∃b∈\<int>⇩_{+}.∀x. b\<lsq>x --> a \<lsq> f`(x)"

using Int_ZF_2_3_L5 by simp;

ultimately have

"∃c∈\<int>. \<two> \<lsq> Minimum(IntegerOrder,{n∈\<int>⇩_{+}. \<one> \<lsq> f`(n)\<ra>c})"

by (rule Int_ZF_1_6_L7);

then obtain c where I: "c∈\<int>" and

II: "\<two> \<lsq> Minimum(IntegerOrder,{n∈\<int>⇩_{+}. \<one> \<lsq> f`(n)\<ra>c})"

by auto;

let ?g = "{⟨m,f`(m)\<ra>c⟩. m∈\<int>}"

from A1 I have III: "?g∈\<S>" and IV: "f∼?g" using Int_ZF_2_1_L33

by auto

from IV have "⟨f,?g⟩ ∈ AlEqRel" by simp

with A1 have T: "?g ∈ \<S>⇩_{+}" by (rule Int_ZF_2_3_L9);

moreover have "∀m∈\<int>⇩_{+}. ?g¯(m)\<rs>\<one> ∈ \<int>⇩_{+}"

proof

fix m assume A2: "m∈\<int>⇩_{+}"

from A1 I II have V: "\<two> \<lsq> ?g¯(\<one>)"

using Int_ZF_2_1_L33 PositiveSet_def by simp;

moreover from A2 T have "?g¯(\<one>) \<lsq> ?g¯(m)"

using Int_ZF_1_5_L3 int_one_two_are_pos Int_ZF_2_4_L5

by simp;

ultimately have "\<two> \<lsq> ?g¯(m)"

by (rule Int_order_transitive);

then have "\<two>\<rs>\<one> \<lsq> ?g¯(m)\<rs>\<one>"

using int_zero_one_are_int Int_ZF_1_1_L4 int_ord_transl_inv

by simp;

then show "?g¯(m)\<rs>\<one> ∈ \<int>⇩_{+}"

using int_zero_one_are_int Int_ZF_1_2_L3 Int_ZF_1_5_L3

by simp;

qed;

ultimately have "∃h∈\<S>. ?goh ∼ id(\<int>)"

by (rule Int_ZF_2_4_L12);

with III IV show ?thesis by auto;

qed;

section{*Completeness*}

text{*In this section we consider properties of slopes that are

needed for the proof of completeness of real numbers constructred

in @{text "Real_ZF_1.thy"}. In particular we consider properties

of embedding of integers into the set of slopes by the mapping

$m \mapsto m^S$ , where $m^S$ is defined by $m^S(n) = m\cdot n$.*}

text{*If m is an integer, then $m^S$ is a slope whose value

is $m\cdot n$ for every integer.*}

lemma (in int1) Int_ZF_2_5_L1: assumes A1: "m ∈ \<int>"

shows

"∀n ∈ \<int>. (m⇧^{S})`(n) = m·n"

"m⇧^{S}∈ \<S>"

proof -

from A1 have I: "m⇧^{S}:\<int>->\<int>"

using Int_ZF_1_1_L5 ZF_fun_from_total by simp;

then show II: "∀n ∈ \<int>. (m⇧^{S})`(n) = m·n" using ZF_fun_from_tot_val

by simp

{ fix n k

assume A2: "n∈\<int>" "k∈\<int>"

with A1 have T: "m·n ∈ \<int>" "m·k ∈ \<int>"

using Int_ZF_1_1_L5 by auto

from A1 A2 II T have "δ(m⇧^{S},n,k) = m·k \<rs> m·k"

using Int_ZF_1_1_L5 Int_ZF_1_1_L1 Int_ZF_1_2_L3

by simp;

also from T have "… = \<zero>" using Int_ZF_1_1_L4

by simp;

finally have "δ(m⇧^{S},n,k) = \<zero>" by simp;

then have "abs(δ(m⇧^{S},n,k)) \<lsq> \<zero>"

using Int_ZF_2_L18 int_zero_one_are_int int_ord_is_refl refl_def

by simp;

} then have "∀n∈\<int>.∀k∈\<int>. abs(δ(m⇧^{S},n,k)) \<lsq> \<zero>"

by simp

with I show "m⇧^{S}∈ \<S>" by (rule Int_ZF_2_1_L5);

qed;

text{*For any slope $f$ there is an integer $m$ such that there is some slope $g$

that is almost equal to $m^S$ and dominates $f$ in the sense that $f\leq g$

on positive integers (which implies that either $g$ is almost equal to $f$ or

$g-f$ is a positive slope. This will be used in @{text "Real_ZF_1.thy"} to show

that for any real number there is an integer that (whose real embedding)

is greater or equal.*}

lemma (in int1) Int_ZF_2_5_L2: assumes A1: "f ∈ \<S>"

shows "∃m∈\<int>. ∃g∈\<S>. (m⇧^{S}∼g ∧ (f∼g ∨ g\<fp>(\<fm>f) ∈ \<S>⇩_{+}))"

proof -

from A1 have

"∃m k. m∈\<int> ∧ k∈\<int> ∧ (∀p∈\<int>. abs(f`(p)) \<lsq> m·abs(p)\<ra>k)"

using Arthan_Lem_8 by simp;

then obtain m k where I: "m∈\<int>" and II: "k∈\<int>" and

III: "∀p∈\<int>. abs(f`(p)) \<lsq> m·abs(p)\<ra>k"

by auto;

let ?g = "{⟨n,m⇧^{S}`(n) \<ra>k⟩. n∈\<int>}"

from I have IV: "m⇧^{S}∈ \<S>" using Int_ZF_2_5_L1 by simp;

with II have V: "?g∈\<S>" and VI: "m⇧^{S}∼?g" using Int_ZF_2_1_L33

by auto;

{ fix n assume A2: "n∈\<int>⇩_{+}"

with A1 have "f`(n) ∈ \<int>"

using Int_ZF_2_1_L2B PositiveSet_def by simp;

then have "f`(n) \<lsq> abs(f`(n))" using Int_ZF_2_L19C

by simp;

moreover

from III A2 have "abs(f`(n)) \<lsq> m·abs(n) \<ra> k"

using PositiveSet_def by simp;

with A2 have "abs(f`(n)) \<lsq> m·n\<ra>k"

using Int_ZF_1_5_L4A by simp;

ultimately have "f`(n) \<lsq> m·n\<ra>k"

by (rule Int_order_transitive);

moreover

from II IV A2 have "?g`(n) = (m⇧^{S})`(n)\<ra>k"

using Int_ZF_2_1_L33 PositiveSet_def by simp;

with I A2 have "?g`(n) = m·n\<ra>k"

using Int_ZF_2_5_L1 PositiveSet_def by simp;

ultimately have "f`(n) \<lsq> ?g`(n)"

by simp;

} then have "∀n∈\<int>⇩_{+}. f`(n) \<lsq> ?g`(n)"

by simp;

with A1 V have "f∼?g ∨ ?g \<fp> (\<fm>f) ∈ \<S>⇩_{+}"

using Int_ZF_2_3_L4C by simp;

with I V VI show ?thesis by auto;

qed;

text{*The negative of an integer embeds in slopes as a negative of the

orgiginal embedding.*}

lemma (in int1) Int_ZF_2_5_L3: assumes A1: "m ∈ \<int>"

shows "(\<rm>m)⇧^{S}= \<fm>(m⇧^{S})"

proof -

from A1 have "(\<rm>m)⇧^{S}: \<int>->\<int>" and "(\<fm>(m⇧^{S})): \<int>->\<int>"

using Int_ZF_1_1_L4 Int_ZF_2_5_L1 AlmostHoms_def Int_ZF_2_1_L12

by auto;

moreover have "∀n∈\<int>. ((\<rm>m)⇧^{S})`(n) = (\<fm>(m⇧^{S}))`(n)"

proof

fix n assume A2: "n∈\<int>"

with A1 have

"((\<rm>m)⇧^{S})`(n) = (\<rm>m)·n"

"(\<fm>(m⇧^{S}))`(n) = \<rm>(m·n)"

using Int_ZF_1_1_L4 Int_ZF_2_5_L1 Int_ZF_2_1_L12A

by auto;

with A1 A2 show "((\<rm>m)⇧^{S})`(n) = (\<fm>(m⇧^{S}))`(n)"

using Int_ZF_1_1_L5 by simp;

qed

ultimately show "(\<rm>m)⇧^{S}= \<fm>(m⇧^{S})" using fun_extension_iff

by simp;

qed;

text{*The sum of embeddings is the embeding of the sum.*}

lemma (in int1) Int_ZF_2_5_L3A: assumes A1: "m∈\<int>" "k∈\<int>"

shows "(m⇧^{S}) \<fp> (k⇧^{S}) = ((m\<ra>k)⇧^{S})"

proof -

from A1 have T1: "m\<ra>k ∈ \<int>" using Int_ZF_1_1_L5

by simp

with A1 have T2:

"(m⇧^{S}) ∈ \<S>" "(k⇧^{S}) ∈ \<S>"

"(m\<ra>k)⇧^{S}∈ \<S>"

"(m⇧^{S}) \<fp> (k⇧^{S}) ∈ \<S>"

using Int_ZF_2_5_L1 Int_ZF_2_1_L12C by auto;

then have

"(m⇧^{S}) \<fp> (k⇧^{S}) : \<int>->\<int>"

"(m\<ra>k)⇧^{S}: \<int>->\<int>"

using AlmostHoms_def by auto;

moreover have "∀n∈\<int>. ((m⇧^{S}) \<fp> (k⇧^{S}))`(n) = ((m\<ra>k)⇧^{S})`(n)"

proof

fix n assume A2: "n∈\<int>"

with A1 T1 T2 have "((m⇧^{S}) \<fp> (k⇧^{S}))`(n) = (m\<ra>k)·n"

using Int_ZF_2_1_L12B Int_ZF_2_5_L1 Int_ZF_1_1_L1

by simp;

also from T1 A2 have "… = ((m\<ra>k)⇧^{S})`(n)"

using Int_ZF_2_5_L1 by simp;

finally show "((m⇧^{S}) \<fp> (k⇧^{S}))`(n) = ((m\<ra>k)⇧^{S})`(n)"

by simp;

qed;

ultimately show "(m⇧^{S}) \<fp> (k⇧^{S}) = ((m\<ra>k)⇧^{S})"

using fun_extension_iff by simp

qed;

text{*The composition of embeddings is the embeding of the product.*}

lemma (in int1) Int_ZF_2_5_L3B: assumes A1: "m∈\<int>" "k∈\<int>"

shows "(m⇧^{S}) o (k⇧^{S}) = ((m·k)⇧^{S})"

proof -

from A1 have T1: "m·k ∈ \<int>" using Int_ZF_1_1_L5

by simp

with A1 have T2:

"(m⇧^{S}) ∈ \<S>" "(k⇧^{S}) ∈ \<S>"

"(m·k)⇧^{S}∈ \<S>"

"(m⇧^{S}) o (k⇧^{S}) ∈ \<S>"

using Int_ZF_2_5_L1 Int_ZF_2_1_L11 by auto;

then have

"(m⇧^{S}) o (k⇧^{S}) : \<int>->\<int>"

"(m·k)⇧^{S}: \<int>->\<int>"

using AlmostHoms_def by auto;

moreover have "∀n∈\<int>. ((m⇧^{S}) o (k⇧^{S}))`(n) = ((m·k)⇧^{S})`(n)"

proof

fix n assume A2: "n∈\<int>"

with A1 T2 have

"((m⇧^{S}) o (k⇧^{S}))`(n) = (m⇧^{S})`(k·n)"

using Int_ZF_2_1_L10 Int_ZF_2_5_L1 by simp;

moreover

from A1 A2 have "k·n ∈ \<int>" using Int_ZF_1_1_L5

by simp;

with A1 A2 have "(m⇧^{S})`(k·n) = m·k·n"

using Int_ZF_2_5_L1 Int_ZF_1_1_L7 by simp;

ultimately have "((m⇧^{S}) o (k⇧^{S}))`(n) = m·k·n"

by simp;

also from T1 A2 have "m·k·n = ((m·k)⇧^{S})`(n)"

using Int_ZF_2_5_L1 by simp;

finally show "((m⇧^{S}) o (k⇧^{S}))`(n) = ((m·k)⇧^{S})`(n)"

by simp;

qed;

ultimately show "(m⇧^{S}) o (k⇧^{S}) = ((m·k)⇧^{S})"

using fun_extension_iff by simp

qed;

text{*Embedding integers in slopes preserves order.*}

lemma (in int1) Int_ZF_2_5_L4: assumes A1: "m\<lsq>n"

shows "(m⇧^{S}) ∼ (n⇧^{S}) ∨ (n⇧^{S})\<fp>(\<fm>(m⇧^{S})) ∈ \<S>⇩_{+}"

proof -

from A1 have "m⇧^{S}∈ \<S>" and "n⇧^{S}∈ \<S>"

using Int_ZF_2_L1A Int_ZF_2_5_L1 by auto;

moreover from A1 have "∀k∈\<int>⇩_{+}. (m⇧^{S})`(k) \<lsq> (n⇧^{S})`(k)"

using Int_ZF_1_3_L13B Int_ZF_2_L1A PositiveSet_def Int_ZF_2_5_L1

by simp;

ultimately show ?thesis using Int_ZF_2_3_L4C

by simp;

qed;

text{*We aim at showing that $m\mapsto m^S$ is an injection modulo

the relation of almost equality. To do that we first show that if

$m^S$ has finite range, then $m=0$.*}

lemma (in int1) Int_ZF_2_5_L5:

assumes "m∈\<int>" and "m⇧^{S}∈ FinRangeFunctions(\<int>,\<int>)"

shows "m=\<zero>"

using assms FinRangeFunctions_def Int_ZF_2_5_L1 AlmostHoms_def

func_imagedef Int_ZF_1_6_L8 by simp;

text{*Embeddings of two integers are almost equal only if

the integers are equal.*}

lemma (in int1) Int_ZF_2_5_L6:

assumes A1: "m∈\<int>" "k∈\<int>" and A2: "(m⇧^{S}) ∼ (k⇧^{S})"

shows "m=k"

proof -

from A1 have T: "m\<rs>k ∈ \<int>" using Int_ZF_1_1_L5 by simp

from A1 have "(\<fm>(k⇧^{S})) = ((\<rm>k)⇧^{S})"

using Int_ZF_2_5_L3 by simp;

then have "m⇧^{S}\<fp> (\<fm>(k⇧^{S})) = (m⇧^{S}) \<fp> ((\<rm>k)⇧^{S})"

by simp;

with A1 have "m⇧^{S}\<fp> (\<fm>(k⇧^{S})) = ((m\<rs>k)⇧^{S})"

using Int_ZF_1_1_L4 Int_ZF_2_5_L3A by simp;

moreover from A1 A2 have "m⇧^{S}\<fp> (\<fm>(k⇧^{S})) ∈ FinRangeFunctions(\<int>,\<int>)"

using Int_ZF_2_5_L1 Int_ZF_2_1_L9D by simp;

ultimately have "(m\<rs>k)⇧^{S}∈ FinRangeFunctions(\<int>,\<int>)"

by simp;

with T have "m\<rs>k = \<zero>" using Int_ZF_2_5_L5

by simp;

with A1 show "m=k" by (rule Int_ZF_1_L15);

qed;

text{*Embedding of $1$ is the identity slope and embedding of zero is a

finite range function.*}

lemma (in int1) Int_ZF_2_5_L7: shows

"\<one>⇧^{S}= id(\<int>)"

"\<zero>⇧^{S}∈ FinRangeFunctions(\<int>,\<int>)"

proof -

have "id(\<int>) = {⟨x,x⟩. x∈\<int>}"

using id_def by blast;

then show "\<one>⇧^{S}= id(\<int>)" using Int_ZF_1_1_L4 by simp;

have "{\<zero>⇧^{S}`(n). n∈\<int>} = {\<zero>·n. n∈\<int>}"

using int_zero_one_are_int Int_ZF_2_5_L1 by simp;

also have "… = {\<zero>}" using Int_ZF_1_1_L4 int_not_empty

by simp;

finally have "{\<zero>⇧^{S}`(n). n∈\<int>} = {\<zero>}" by simp;

then have "{\<zero>⇧^{S}`(n). n∈\<int>} ∈ Fin(\<int>)"

using int_zero_one_are_int Finite1_L16 by simp;

moreover have "\<zero>⇧^{S}: \<int>->\<int>"

using int_zero_one_are_int Int_ZF_2_5_L1 AlmostHoms_def

by simp;

ultimately show "\<zero>⇧^{S}∈ FinRangeFunctions(\<int>,\<int>)"

using Finite1_L19 by simp;

qed;

text{*A somewhat technical condition for a embedding of an integer

to be "less or equal" (in the sense apriopriate for slopes) than

the composition of a slope and another integer (embedding).*}

lemma (in int1) Int_ZF_2_5_L8:

assumes A1: "f ∈ \<S>" and A2: "N ∈ \<int>" "M ∈ \<int>" and

A3: "∀n∈\<int>⇩_{+}. M·n \<lsq> f`(N·n)"

shows "M⇧^{S}∼ fo(N⇧^{S}) ∨ (fo(N⇧^{S})) \<fp> (\<fm>(M⇧^{S})) ∈ \<S>⇩_{+}"

proof -

from A1 A2 have "M⇧^{S}∈ \<S>" "fo(N⇧^{S}) ∈ \<S>"

using Int_ZF_2_5_L1 Int_ZF_2_1_L11 by auto;

moreover from A1 A2 A3 have "∀n∈\<int>⇩_{+}. (M⇧^{S})`(n) \<lsq> (fo(N⇧^{S}))`(n)"

using Int_ZF_2_5_L1 PositiveSet_def Int_ZF_2_1_L10

by simp;

ultimately show ?thesis using Int_ZF_2_3_L4C

by simp;

qed;

text{*Another technical condition for the composition of a slope and

an integer (embedding) to be "less or equal" (in the sense apriopriate

for slopes) than embedding of another integer.*}

lemma (in int1) Int_ZF_2_5_L9:

assumes A1: "f ∈ \<S>" and A2: "N ∈ \<int>" "M ∈ \<int>" and

A3: "∀n∈\<int>⇩_{+}. f`(N·n) \<lsq> M·n "

shows "fo(N⇧^{S}) ∼ (M⇧^{S}) ∨ (M⇧^{S}) \<fp> (\<fm>(fo(N⇧^{S}))) ∈ \<S>⇩_{+}"

proof -;

from A1 A2 have "fo(N⇧^{S}) ∈ \<S>" "M⇧^{S}∈ \<S>"

using Int_ZF_2_5_L1 Int_ZF_2_1_L11 by auto;

moreover from A1 A2 A3 have "∀n∈\<int>⇩_{+}. (fo(N⇧^{S}))`(n) \<lsq> (M⇧^{S})`(n) "

using Int_ZF_2_5_L1 PositiveSet_def Int_ZF_2_1_L10

by simp;

ultimately show ?thesis using Int_ZF_2_3_L4C

by simp;

qed

end;