(* 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{OrderedGroup\_ZF\_1.thy}*}

theory OrderedGroup_ZF_1 imports OrderedGroup_ZF

begin

text{*In this theory we continue the @{text "OrderedGroup_ZF"}

theory development.*}

section{*Absolute value and the triangle inequality*};

text{*The goal of this section is to prove the triangle inequality for

ordered groups.*};

text{*Absolute value maps $G$ into $G$.*}

lemma (in group3) OrderedGroup_ZF_3_L1:

shows "AbsoluteValue(G,P,r) : G->G"

proof -;

let ?f = "id(G⇧^{+})"

let ?g = "restrict(GroupInv(G,P),G-G⇧^{+})"

have "?f : G⇧^{+}->G⇧^{+}" using id_type by simp;

then have "?f : G⇧^{+}->G" using OrderedGroup_ZF_1_L4E fun_weaken_type

by blast;

moreover have "?g : G-G⇧^{+}->G"

proof -;

from ordGroupAssum have "GroupInv(G,P) : G->G"

using IsAnOrdGroup_def group0_2_T2 by simp;

moreover have "G-G⇧^{+}⊆ G" by auto;

ultimately show ?thesis using restrict_type2 by simp;

qed;

moreover have "G⇧^{+}∩(G-G⇧^{+}) = 0" by blast;

ultimately have "?f ∪ ?g : G⇧^{+}∪(G-G⇧^{+})->G∪G"

by (rule fun_disjoint_Un);

moreover have "G⇧^{+}∪(G-G⇧^{+}) = G" using OrderedGroup_ZF_1_L4E

by auto;

ultimately show "AbsoluteValue(G,P,r) : G->G"

using AbsoluteValue_def by simp;

qed;

text{*If $a\in G^+$, then $|a| = a$.*}

lemma (in group3) OrderedGroup_ZF_3_L2:

assumes A1: "a∈G⇧^{+}" shows "|a| = a"

proof -

from ordGroupAssum have "GroupInv(G,P) : G->G"

using IsAnOrdGroup_def group0_2_T2 by simp;

with A1 show ?thesis using

func1_1_L1 OrderedGroup_ZF_1_L4E fun_disjoint_apply1

AbsoluteValue_def id_conv by simp;

qed;

text{*The absolute value of the unit is the unit. In the

additive totation that would be $|0| = 0$.*}

lemma (in group3) OrderedGroup_ZF_3_L2A:

shows "|\<one>| = \<one>" using OrderedGroup_ZF_1_L3A OrderedGroup_ZF_3_L2

by simp;

text{*If $a$ is positive, then $|a| = a$.*}

lemma (in group3) OrderedGroup_ZF_3_L2B:

assumes "a∈G⇩_{+}" shows "|a| = a"

using assms PositiveSet_def Nonnegative_def OrderedGroup_ZF_3_L2

by auto;

text{*If $a\in G\setminus G^+$, then $|a| = a^{-1}$.*}

lemma (in group3) OrderedGroup_ZF_3_L3:

assumes A1: "a ∈ G-G⇧^{+}" shows "|a| = a¯"

proof -

have "domain(id(G⇧^{+})) = G⇧^{+}"

using id_type func1_1_L1 by auto;

with A1 show ?thesis using fun_disjoint_apply2 AbsoluteValue_def

restrict by simp;

qed;

text{*For elements that not greater than the unit, the absolute value is

the inverse.*}

lemma (in group3) OrderedGroup_ZF_3_L3A:

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

shows "|a| = a¯"

proof -

{ assume "a=\<one>" then have "|a| = a¯"

using OrderedGroup_ZF_3_L2A OrderedGroup_ZF_1_L1 group0.group_inv_of_one

by simp }

moreover

{ assume "a≠\<one>"

with A1 have "|a| = a¯" using OrderedGroup_ZF_1_L4C OrderedGroup_ZF_3_L3

by simp }

ultimately show "|a| = a¯" by blast

qed;

text{*In linearly ordered groups the absolute value of any element

is in $G^+$.*}

lemma (in group3) OrderedGroup_ZF_3_L3B:

assumes A1: "r {is total on} G" and A2: "a∈G"

shows "|a| ∈ G⇧^{+}"

proof -

{ assume "a ∈ G⇧^{+}" then have "|a| ∈ G⇧^{+}"

using OrderedGroup_ZF_3_L2 by simp }

moreover

{ assume "a ∉ G⇧^{+}"

with A1 A2 have "|a| ∈ G⇧^{+}" using OrderedGroup_ZF_3_L3

OrderedGroup_ZF_1_L6 by simp }

ultimately show "|a| ∈ G⇧^{+}" by blast

qed;

text{*For linearly ordered groups (where the order is total), the absolute

value maps the group into the positive set.*}

lemma (in group3) OrderedGroup_ZF_3_L3C:

assumes A1: "r {is total on} G"

shows "AbsoluteValue(G,P,r) : G->G⇧^{+}"

proof-;

have "AbsoluteValue(G,P,r) : G->G" using OrderedGroup_ZF_3_L1

by simp;

moreover from A1 have T2:

"∀g∈G. AbsoluteValue(G,P,r)`(g) ∈ G⇧^{+}"

using OrderedGroup_ZF_3_L3B by simp;

ultimately show ?thesis by (rule func1_1_L1A);

qed;

text{*If the absolute value is the unit, then the elemnent is the unit.*}

lemma (in group3) OrderedGroup_ZF_3_L3D:

assumes A1: "a∈G" and A2: "|a| = \<one>"

shows "a = \<one>"

proof -

{ assume "a ∈ G⇧^{+}"

with A2 have "a = \<one>" using OrderedGroup_ZF_3_L2 by simp }

moreover

{ assume "a ∉ G⇧^{+}"

with A1 A2 have "a = \<one>" using

OrderedGroup_ZF_3_L3 OrderedGroup_ZF_1_L1 group0.group0_2_L8A

by auto }

ultimately show "a = \<one>" by blast

qed;

text{*In linearly ordered groups the unit is not greater than the absolute

value of any element.*}

lemma (in group3) OrderedGroup_ZF_3_L3E:

assumes "r {is total on} G" and "a∈G"

shows "\<one> \<lsq> |a|"

using assms OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L2 by simp;

text{*If $b$ is greater than both $a$ and $a^{-1}$, then $b$ is greater than

$|a|$.*}

lemma (in group3) OrderedGroup_ZF_3_L4:

assumes A1: "a\<lsq>b" and A2: "a¯\<lsq> b"

shows "|a|\<lsq> b"

proof -

{ assume "a∈G⇧^{+}"

with A1 have "|a|\<lsq> b" using OrderedGroup_ZF_3_L2 by simp }

moreover

{ assume "a∉G⇧^{+}"

with A1 A2 have "|a|\<lsq> b"

using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_3_L3 by simp }

ultimately show "|a|\<lsq> b" by blast

qed;

text{*In linearly ordered groups $a\leq |a|$.*}

lemma (in group3) OrderedGroup_ZF_3_L5:

assumes A1: "r {is total on} G" and A2: "a∈G"

shows "a \<lsq> |a|"

proof -

{ assume "a ∈ G⇧^{+}"

with A2 have "a \<lsq> |a|"

using OrderedGroup_ZF_3_L2 OrderedGroup_ZF_1_L3 by simp }

moreover

{ assume "a ∉ G⇧^{+}"

with A1 A2 have "a \<lsq> |a|"

using OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L4B by simp }

ultimately show "a \<lsq> |a|" by blast

qed;

text{* $a^{-1}\leq |a|$ (in additive notation it would be $-a\leq |a|$.*}

lemma (in group3) OrderedGroup_ZF_3_L6:

assumes A1: "a∈G" shows "a¯ \<lsq> |a|"

proof -

{ assume "a ∈ G⇧^{+}"

then have T1: "\<one>\<lsq>a" and T2: "|a| = a" using OrderedGroup_ZF_1_L2

OrderedGroup_ZF_3_L2 by auto;

then have "a¯\<lsq>\<one>¯" using OrderedGroup_ZF_1_L5 by simp;

then have T3: "a¯\<lsq>\<one>"

using OrderedGroup_ZF_1_L1 group0.group_inv_of_one by simp;

from T3 T1 have "a¯\<lsq>a" by (rule Group_order_transitive);

with T2 have "a¯ \<lsq> |a|" by simp }

moreover

{ assume A2: "a ∉ G⇧^{+}"

from A1 have "|a| ∈ G"

using OrderedGroup_ZF_3_L1 apply_funtype by auto;

with ordGroupAssum have "|a| \<lsq> |a|"

using IsAnOrdGroup_def IsPartOrder_def refl_def by simp;

with A1 A2 have "a¯ \<lsq> |a|" using OrderedGroup_ZF_3_L3 by simp }

ultimately show "a¯ \<lsq> |a|" by blast

qed;

text{*Some inequalities about the product of two elements of a linearly

ordered group and its absolute value.*}

lemma (in group3) OrderedGroup_ZF_3_L6A:

assumes "r {is total on} G" and "a∈G" "b∈G"

shows

"a·b \<lsq>|a|·|b|"

"a·b¯ \<lsq>|a|·|b|"

"a¯·b \<lsq>|a|·|b|"

"a¯·b¯ \<lsq>|a|·|b|"

using assms OrderedGroup_ZF_3_L5 OrderedGroup_ZF_3_L6

OrderedGroup_ZF_1_L5B by auto;

text{* $|a^{-1}|\leq |a|$.*}

lemma (in group3) OrderedGroup_ZF_3_L7:

assumes "r {is total on} G" and "a∈G"

shows "|a¯|\<lsq>|a|"

using assms OrderedGroup_ZF_3_L5 OrderedGroup_ZF_1_L1 group0.group_inv_of_inv

OrderedGroup_ZF_3_L6 OrderedGroup_ZF_3_L4 by simp;

text{* $|a^{-1}| = |a|$.*}

lemma (in group3) OrderedGroup_ZF_3_L7A:

assumes A1: "r {is total on} G" and A2: "a∈G"

shows "|a¯| = |a|"

proof -

from A2 have "a¯∈G" using OrderedGroup_ZF_1_L1 group0.inverse_in_group

by simp;

with A1 have "|(a¯)¯| \<lsq> |a¯|" using OrderedGroup_ZF_3_L7 by simp;

with A1 A2 have "|a¯| \<lsq> |a|" "|a| \<lsq> |a¯|"

using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv OrderedGroup_ZF_3_L7

by auto;

then show ?thesis by (rule group_order_antisym);

qed;

text{* $|a\cdot b^{-1}| = |b\cdot a^{-1}|$. It doesn't look so strange in the

additive notation: $|a-b| = |b-a|$. *}

lemma (in group3) OrderedGroup_ZF_3_L7B:

assumes A1: "r {is total on} G" and A2: "a∈G" "b∈G"

shows "|a·b¯| = |b·a¯|"

proof -

from A1 A2 have "|(a·b¯)¯| = |a·b¯|" using

OrderedGroup_ZF_1_L1 group0.inverse_in_group group0.group0_2_L1

monoid0.group0_1_L1 OrderedGroup_ZF_3_L7A by simp;

moreover from A2 have "(a·b¯)¯ = b·a¯"

using OrderedGroup_ZF_1_L1 group0.group0_2_L12 by simp;

ultimately show ?thesis by simp;

qed;

text{*Triangle inequality for linearly ordered abelian groups.

It would be nice to drop commutativity or give an example that shows we

can't do that.*}

theorem (in group3) OrdGroup_triangle_ineq:

assumes A1: "P {is commutative on} G"

and A2: "r {is total on} G" and A3: "a∈G" "b∈G"

shows "|a·b| \<lsq> |a|·|b|"

proof -;

from A1 A2 A3 have

"a \<lsq> |a|" "b \<lsq> |b|" "a¯ \<lsq> |a|" "b¯ \<lsq> |b|"

using OrderedGroup_ZF_3_L5 OrderedGroup_ZF_3_L6 by auto;

then have "a·b \<lsq> |a|·|b|" "a¯·b¯ \<lsq> |a|·|b|"

using OrderedGroup_ZF_1_L5B by auto;

with A1 A3 show "|a·b| \<lsq> |a|·|b|"

using OrderedGroup_ZF_1_L1 group0.group_inv_of_two IsCommutative_def

OrderedGroup_ZF_3_L4 by simp;

qed;

text{*We can multiply the sides of an inequality with absolute value.*}

lemma (in group3) OrderedGroup_ZF_3_L7C:

assumes A1: "P {is commutative on} G"

and A2: "r {is total on} G" and A3: "a∈G" "b∈G"

and A4: "|a| \<lsq> c" "|b| \<lsq> d"

shows "|a·b| \<lsq> c·d"

proof -

from A1 A2 A3 A4 have "|a·b| \<lsq> |a|·|b|"

using OrderedGroup_ZF_1_L4 OrdGroup_triangle_ineq

by simp;

moreover from A4 have "|a|·|b| \<lsq> c·d"

using OrderedGroup_ZF_1_L5B by simp

ultimately show ?thesis by (rule Group_order_transitive);

qed;

text{*A version of the @{text "OrderedGroup_ZF_3_L7C"}

but with multiplying by the inverse.*}

lemma (in group3) OrderedGroup_ZF_3_L7CA:

assumes "P {is commutative on} G"

and "r {is total on} G" and "a∈G" "b∈G"

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

shows "|a·b¯| \<lsq> c·d"

using assms OrderedGroup_ZF_1_L1 group0.inverse_in_group

OrderedGroup_ZF_3_L7A OrderedGroup_ZF_3_L7C by simp;

text{*Triangle inequality with three integers.*}

lemma (in group3) OrdGroup_triangle_ineq3:

assumes A1: "P {is commutative on} G"

and A2: "r {is total on} G" and A3: "a∈G" "b∈G" "c∈G"

shows "|a·b·c| \<lsq> |a|·|b|·|c|"

proof -

from A3 have T: "a·b ∈ G" "|c| ∈ G"

using OrderedGroup_ZF_1_L1 group0.group_op_closed

OrderedGroup_ZF_3_L1 apply_funtype by auto;

with A1 A2 A3 have "|a·b·c| \<lsq> |a·b|·|c|"

using OrdGroup_triangle_ineq by simp;

moreover from ordGroupAssum A1 A2 A3 T have

"|a·b|·|c| \<lsq> |a|·|b|·|c|"

using OrdGroup_triangle_ineq IsAnOrdGroup_def by simp;

ultimately show "|a·b·c| \<lsq> |a|·|b|·|c|"

by (rule Group_order_transitive);

qed;

text{*Some variants of the triangle inequality.*}

lemma (in group3) OrderedGroup_ZF_3_L7D:

assumes A1: "P {is commutative on} G"

and A2: "r {is total on} G" and A3: "a∈G" "b∈G"

and A4: "|a·b¯| \<lsq> c"

shows

"|a| \<lsq> c·|b|"

"|a| \<lsq> |b|·c"

"c¯·a \<lsq> b"

"a·c¯ \<lsq> b"

"a \<lsq> b·c"

proof -

from A3 A4 have

T: "a·b¯ ∈ G" "|b| ∈ G" "c∈G" "c¯ ∈ G"

using OrderedGroup_ZF_1_L1

group0.inverse_in_group group0.group0_2_L1 monoid0.group0_1_L1

OrderedGroup_ZF_3_L1 apply_funtype OrderedGroup_ZF_1_L4

by auto;

from A3 have "|a| = |a·b¯·b|"

using OrderedGroup_ZF_1_L1 group0.inv_cancel_two

by simp;

with A1 A2 A3 T have "|a| \<lsq> |a·b¯|·|b|"

using OrdGroup_triangle_ineq by simp;

with T A4 show "|a| \<lsq> c·|b|" using OrderedGroup_ZF_1_L5C

by blast

with T A1 show "|a| \<lsq> |b|·c"

using IsCommutative_def by simp;

from A2 T have "a·b¯ \<lsq> |a·b¯|"

using OrderedGroup_ZF_3_L5 by simp

moreover note A4

ultimately have I: "a·b¯ \<lsq> c"

by (rule Group_order_transitive)

with A3 show "c¯·a \<lsq> b"

using OrderedGroup_ZF_1_L5H by simp;

with A1 A3 T show "a·c¯ \<lsq> b"

using IsCommutative_def by simp;

from A1 A3 T I show "a \<lsq> b·c"

using OrderedGroup_ZF_1_L5H IsCommutative_def

by auto;

qed;

text{*Some more variants of the triangle inequality.*}

lemma (in group3) OrderedGroup_ZF_3_L7E:

assumes A1: "P {is commutative on} G"

and A2: "r {is total on} G" and A3: "a∈G" "b∈G"

and A4: "|a·b¯| \<lsq> c"

shows "b·c¯ \<lsq> a"

proof -

from A3 have "a·b¯ ∈ G"

using OrderedGroup_ZF_1_L1

group0.inverse_in_group group0.group_op_closed

by auto

with A2 have "|(a·b¯)¯| = |a·b¯|"

using OrderedGroup_ZF_3_L7A by simp

moreover from A3 have "(a·b¯)¯ = b·a¯"

using OrderedGroup_ZF_1_L1 group0.group0_2_L12

by simp;

ultimately have "|b·a¯| = |a·b¯|"

by simp

with A1 A2 A3 A4 show "b·c¯ \<lsq> a"

using OrderedGroup_ZF_3_L7D by simp;

qed;

text{*An application of the triangle inequality with four group

elements.*}

lemma (in group3) OrderedGroup_ZF_3_L7F:

assumes A1: "P {is commutative on} G"

and A2: "r {is total on} G" and

A3: "a∈G" "b∈G" "c∈G" "d∈G"

shows "|a·c¯| \<lsq> |a·b|·|c·d|·|b·d¯|"

proof -

from A3 have T:

"a·c¯ ∈ G" "a·b ∈ G" "c·d ∈ G" "b·d¯ ∈ G"

"(c·d)¯ ∈ G" "(b·d¯)¯ ∈ G"

using OrderedGroup_ZF_1_L1

group0.inverse_in_group group0.group_op_closed

by auto;

with A1 A2 have "|(a·b)·(c·d)¯·(b·d¯)¯| \<lsq> |a·b|·|(c·d)¯|·|(b·d¯)¯|"

using OrdGroup_triangle_ineq3 by simp;

moreover from A2 T have "|(c·d)¯| =|c·d|" and "|(b·d¯)¯| = |b·d¯|"

using OrderedGroup_ZF_3_L7A by auto;

moreover from A1 A3 have "(a·b)·(c·d)¯·(b·d¯)¯ = a·c¯"

using OrderedGroup_ZF_1_L1 group0.group0_4_L8

by simp;

ultimately show "|a·c¯| \<lsq> |a·b|·|c·d|·|b·d¯|"

by simp;

qed;

text{* $|a|\leq L$ implies $L^{-1} \leq a$

(it would be $-L \leq a$ in the additive notation).*}

lemma (in group3) OrderedGroup_ZF_3_L8:

assumes A1: "a∈G" and A2: "|a|\<lsq>L"

shows

"L¯\<lsq>a"

proof -

from A1 have I: "a¯ \<lsq> |a|" using OrderedGroup_ZF_3_L6 by simp;

from I A2 have "a¯ \<lsq> L" by (rule Group_order_transitive);

then have "L¯\<lsq>(a¯)¯" using OrderedGroup_ZF_1_L5 by simp;

with A1 show "L¯\<lsq>a" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv

by simp

qed;

text{*In linearly ordered groups $|a|\leq L$ implies $a \leq L$

(it would be $a \leq L$ in the additive notation).*}

lemma (in group3) OrderedGroup_ZF_3_L8A:

assumes A1: "r {is total on} G"

and A2: "a∈G" and A3: "|a|\<lsq>L"

shows

"a\<lsq>L"

"\<one>\<lsq>L"

proof -;

from A1 A2 have I: "a \<lsq> |a|" using OrderedGroup_ZF_3_L5 by simp;

from I A3 show "a\<lsq>L" by (rule Group_order_transitive);

from A1 A2 A3 have "\<one> \<lsq> |a|" "|a|\<lsq>L"

using OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L2 by auto;

then show "\<one>\<lsq>L" by (rule Group_order_transitive);

qed;

text{*A somewhat generalized version of the above lemma.*}

lemma (in group3) OrderedGroup_ZF_3_L8B:

assumes A1: "a∈G" and A2: "|a|\<lsq>L" and A3: "\<one>\<lsq>c"

shows "(L·c)¯ \<lsq> a"

proof -

from A1 A2 A3 have "c¯·L¯ \<lsq> \<one>·a"

using OrderedGroup_ZF_3_L8 OrderedGroup_ZF_1_L5AB

OrderedGroup_ZF_1_L5B by simp;

with A1 A2 A3 show "(L·c)¯ \<lsq> a"

using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1

group0.group_inv_of_two group0.group0_2_L2

by simp;

qed;

text{*If $b$ is between $a$ and $a\cdot c$, then $b\cdot a^{-1}\leq c$.*}

lemma (in group3) OrderedGroup_ZF_3_L8C:

assumes A1: "a\<lsq>b" and A2: "c∈G" and A3: "b\<lsq>c·a"

shows "|b·a¯| \<lsq> c"

proof -

from A1 A2 A3 have "b·a¯ \<lsq> c"

using OrderedGroup_ZF_1_L9C OrderedGroup_ZF_1_L4

by simp;

moreover have "(b·a¯)¯ \<lsq> c"

proof -

from A1 have T: "a∈G" "b∈G"

using OrderedGroup_ZF_1_L4 by auto;

with A1 have "a·b¯ \<lsq> \<one>"

using OrderedGroup_ZF_1_L9 by blast;

moreover

from A1 A3 have "a\<lsq>c·a"

by (rule Group_order_transitive);

with ordGroupAssum T have "a·a¯ \<lsq> c·a·a¯"

using OrderedGroup_ZF_1_L1 group0.inverse_in_group

IsAnOrdGroup_def by simp;

with T A2 have "\<one> \<lsq> c"

using OrderedGroup_ZF_1_L1

group0.group0_2_L6 group0.inv_cancel_two

by simp;

ultimately have "a·b¯ \<lsq> c"

by (rule Group_order_transitive);

with T show "(b·a¯)¯ \<lsq> c"

using OrderedGroup_ZF_1_L1 group0.group0_2_L12

by simp;

qed;

ultimately show "|b·a¯| \<lsq> c"

using OrderedGroup_ZF_3_L4 by simp;

qed;

text{*For linearly ordered groups if the absolute values of elements in a set

are bounded, then the set is bounded.*}

lemma (in group3) OrderedGroup_ZF_3_L9:

assumes A1: "r {is total on} G"

and A2: "A⊆G" and A3: "∀a∈A. |a| \<lsq> L"

shows "IsBounded(A,r)"

proof -;

from A1 A2 A3 have

"∀a∈A. a\<lsq>L" "∀a∈A. L¯\<lsq>a"

using OrderedGroup_ZF_3_L8 OrderedGroup_ZF_3_L8A by auto;

then show "IsBounded(A,r)" using

IsBoundedAbove_def IsBoundedBelow_def IsBounded_def

by auto;

qed;

text{* A slightly more general version of the previous lemma, stating the same

fact for a set defined by separation.*}

lemma (in group3) OrderedGroup_ZF_3_L9A:

assumes A1: "r {is total on} G"

and A2: "∀x∈X. b(x)∈G ∧ |b(x)|\<lsq>L"

shows "IsBounded({b(x). x∈X},r)"

proof -

from A2 have "{b(x). x∈X} ⊆ G" "∀a∈{b(x). x∈X}. |a| \<lsq> L"

by auto;

with A1 show ?thesis using OrderedGroup_ZF_3_L9 by blast;

qed;

text{*A special form of the previous lemma stating a similar fact for an

image of a set by a function with values in a linearly ordered group.*}

lemma (in group3) OrderedGroup_ZF_3_L9B:

assumes A1: "r {is total on} G"

and A2: "f:X->G" and A3: "A⊆X"

and A4: "∀x∈A. |f`(x)| \<lsq> L"

shows "IsBounded(f``(A),r)"

proof -

from A2 A3 A4 have "∀x∈A. f`(x) ∈ G ∧ |f`(x)| \<lsq> L"

using apply_funtype by auto;

with A1 have "IsBounded({f`(x). x∈A},r)"

by (rule OrderedGroup_ZF_3_L9A);

with A2 A3 show "IsBounded(f``(A),r)"

using func_imagedef by simp;

qed;

text{*For linearly ordered groups if $l\leq a\leq u$ then

$|a|$ is smaller than the greater of $|l|,|u|$.*}

lemma (in group3) OrderedGroup_ZF_3_L10:

assumes A1: "r {is total on} G"

and A2: "l\<lsq>a" "a\<lsq>u"

shows

"|a| \<lsq> GreaterOf(r,|l|,|u|)"

proof -

from A2 have T1: "|l| ∈ G" "|a| ∈ G" "|u| ∈ G"

using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_3_L1 apply_funtype

by auto;

{ assume A3: "a∈G⇧^{+}"

with A2 have "\<one>\<lsq>a" "a\<lsq>u"

using OrderedGroup_ZF_1_L2 by auto;

then have "\<one>\<lsq>u" by (rule Group_order_transitive)

with A2 A3 have "|a|\<lsq>|u|"

using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_3_L2 by simp;

moreover from A1 T1 have "|u| \<lsq> GreaterOf(r,|l|,|u|)"

using Order_ZF_3_L2 by simp;

ultimately have "|a| \<lsq> GreaterOf(r,|l|,|u|)"

by (rule Group_order_transitive) }

moreover

{ assume A4: "a∉G⇧^{+}"

with A2 have T2:

"l∈G" "|l| ∈ G" "|a| ∈ G" "|u| ∈ G" "a ∈ G-G⇧^{+}"

using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_3_L1 apply_funtype

by auto;

with A2 have "l ∈ G-G⇧^{+}" using OrderedGroup_ZF_1_L4D by fast;

with T2 A2 have "|a| \<lsq> |l|"

using OrderedGroup_ZF_3_L3 OrderedGroup_ZF_1_L5

by simp;

moreover from A1 T2 have "|l| \<lsq> GreaterOf(r,|l|,|u|)"

using Order_ZF_3_L2 by simp;

ultimately have "|a| \<lsq> GreaterOf(r,|l|,|u|)"

by (rule Group_order_transitive) }

ultimately show ?thesis by blast

qed;

text{*For linearly ordered groups if a set is bounded then the absolute

values are bounded.*}

lemma (in group3) OrderedGroup_ZF_3_L10A:

assumes A1: "r {is total on} G"

and A2: "IsBounded(A,r)"

shows "∃L. ∀a∈A. |a| \<lsq> L"

proof -

{ assume "A = 0" then have ?thesis by auto; }

moreover

{ assume A3: "A≠0"

with A2 have "∃u. ∀g∈A. g\<lsq>u" and "∃l.∀g∈A. l\<lsq>g"

using IsBounded_def IsBoundedAbove_def IsBoundedBelow_def

by auto;

then obtain u l where "∀g∈A. l\<lsq>g ∧ g\<lsq>u"

by auto;

with A1 have "∀a∈A. |a| \<lsq> GreaterOf(r,|l|,|u|)"

using OrderedGroup_ZF_3_L10 by simp;

then have ?thesis by auto }

ultimately show ?thesis by blast

qed;

text{* A slightly more general version of the previous lemma, stating the same

fact for a set defined by separation.*}

lemma (in group3) OrderedGroup_ZF_3_L11:

assumes "r {is total on} G"

and "IsBounded({b(x).x∈X},r)"

shows "∃L. ∀x∈X. |b(x)| \<lsq> L"

using assms OrderedGroup_ZF_3_L10A by blast;

text{*Absolute values of elements of a finite image of a nonempty set are

bounded by an element of the group.*}

lemma (in group3) OrderedGroup_ZF_3_L11A:

assumes A1: "r {is total on} G"

and A2: "X≠0" and A3: "{b(x). x∈X} ∈ Fin(G)"

shows "∃L∈G. ∀x∈X. |b(x)| \<lsq> L"

proof -

from A1 A3 have "∃L. ∀x∈X. |b(x)| \<lsq> L"

using ord_group_fin_bounded OrderedGroup_ZF_3_L11

by simp;

then obtain L where I: "∀x∈X. |b(x)| \<lsq> L"

using OrderedGroup_ZF_3_L11 by auto;

from A2 obtain x where "x∈X" by auto;

with I show ?thesis using OrderedGroup_ZF_1_L4

by blast;

qed;

text{*In totally oredered groups the absolute value of a

nonunit element is in @{text "G⇩_{+}"}.*}

lemma (in group3) OrderedGroup_ZF_3_L12:

assumes A1: "r {is total on} G"

and A2: "a∈G" and A3: "a≠\<one>"

shows "|a| ∈ G⇩_{+}"

proof -

from A1 A2 have "|a| ∈ G" "\<one> \<lsq> |a|"

using OrderedGroup_ZF_3_L1 apply_funtype

OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L2

by auto;

moreover from A2 A3 have "|a| ≠ \<one>"

using OrderedGroup_ZF_3_L3D by auto;

ultimately show "|a| ∈ G⇩_{+}"

using PositiveSet_def by auto;

qed;

section{*Maximum absolute value of a set *}

text{* Quite often when considering inequalities we prefer to talk about

the absolute values instead of raw elements of a set. This section formalizes

some material that is useful for that. *}

text{*If a set has a maximum and minimum, then the greater of the

absolute value of the maximum and minimum belongs to the image of the set

by the absolute value function. *}

lemma (in group3) OrderedGroup_ZF_4_L1:

assumes "A ⊆ G"

and "HasAmaximum(r,A)" "HasAminimum(r,A)"

and "M = GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"

shows "M ∈ AbsoluteValue(G,P,r)``(A)"

using ordGroupAssum assms IsAnOrdGroup_def IsPartOrder_def

Order_ZF_4_L3 Order_ZF_4_L4 OrderedGroup_ZF_3_L1

func_imagedef GreaterOf_def by auto;

text{*If a set has a maximum and minimum, then the greater of the

absolute value of the maximum and minimum bounds absolute values of all

elements of the set. *}

lemma (in group3) OrderedGroup_ZF_4_L2:

assumes A1: "r {is total on} G"

and A2: "HasAmaximum(r,A)" "HasAminimum(r,A)"

and A3: "a∈A"

shows "|a|\<lsq> GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"

proof -;

from ordGroupAssum A2 A3 have

"Minimum(r,A)\<lsq> a" "a\<lsq> Maximum(r,A)"

using IsAnOrdGroup_def IsPartOrder_def Order_ZF_4_L3 Order_ZF_4_L4

by auto;

with A1 show ?thesis by (rule OrderedGroup_ZF_3_L10);

qed;

text{*If a set has a maximum and minimum, then the greater of the

absolute value of the maximum and minimum bounds absolute values of all

elements of the set. In this lemma the absolute values of ekements of a

set are represented as the elements of the image of the set by the absolute

value function.*}

lemma (in group3) OrderedGroup_ZF_4_L3:

assumes "r {is total on} G" and "A ⊆ G"

and "HasAmaximum(r,A)" "HasAminimum(r,A)"

and "b ∈ AbsoluteValue(G,P,r)``(A)"

shows "b\<lsq> GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"

using assms OrderedGroup_ZF_3_L1 func_imagedef OrderedGroup_ZF_4_L2

by auto;

text{*If a set has a maximum and minimum, then the set of absolute values

also has a maximum.*}

lemma (in group3) OrderedGroup_ZF_4_L4:

assumes A1: "r {is total on} G" and A2: "A ⊆ G"

and A3: "HasAmaximum(r,A)" "HasAminimum(r,A)"

shows "HasAmaximum(r,AbsoluteValue(G,P,r)``(A))"

proof -;

let ?M = "GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"

from A2 A3 have "?M ∈ AbsoluteValue(G,P,r)``(A)"

using OrderedGroup_ZF_4_L1 by simp;

moreover from A1 A2 A3 have

"∀b ∈ AbsoluteValue(G,P,r)``(A). b \<lsq> ?M"

using OrderedGroup_ZF_4_L3 by simp;

ultimately show ?thesis using HasAmaximum_def by auto;

qed;

text{*If a set has a maximum and a minimum, then all absolute values are

bounded by the maximum of the set of absolute values.*}

lemma (in group3) OrderedGroup_ZF_4_L5:

assumes A1: "r {is total on} G" and A2: "A ⊆ G"

and A3: "HasAmaximum(r,A)" "HasAminimum(r,A)"

and A4: "a∈A"

shows "|a| \<lsq> Maximum(r,AbsoluteValue(G,P,r)``(A))"

proof -;

from A2 A4 have "|a| ∈ AbsoluteValue(G,P,r)``(A)"

using OrderedGroup_ZF_3_L1 func_imagedef by auto;

with ordGroupAssum A1 A2 A3 show ?thesis using

IsAnOrdGroup_def IsPartOrder_def OrderedGroup_ZF_4_L4

Order_ZF_4_L3 by simp;

qed;

section{*Alternative definitions*}

text{*Sometimes it is usful to define the order by prescibing the set

of positive or nonnegative elements. This section deals with two such

definitions. One takes a subset $H$ of $G$ that is closed under the group

operation, $1\notin H$ and for every $a\in H$ we have either $a\in H$ or

$a^{-1}\in H$. Then the order is defined as $a\leq b$ iff $a=b$ or

$a^{-1}b \in H$. For abelian groups this makes a linearly ordered group.

We will refer to order defined this way in the comments as the order

defined by a positive set. The context used in this section is the

@{text "group0"} context defined in @{text "Group_ZF"} theory. Recall that

@{text "f"} in that context denotes the group operation (unlike in the

previous sections where the group operation was denoted @{text "P"}.*}

text{*The order defined by a positive set is the same as the order defined by

a nonnegative set.*}

lemma (in group0) OrderedGroup_ZF_5_L1:

assumes A1: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"

shows "⟨a,b⟩ ∈ r <-> a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"

proof;

assume "⟨a,b⟩ ∈ r"

with A1 show "a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"

using group0_2_L6 by auto;

next assume "a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"

then have "a∈G ∧ b∈G ∧ b=(a¯)¯ ∨ a∈G ∧ b∈G ∧ a¯·b ∈ H"

using inverse_in_group group0_2_L9 by auto;

with A1 show "⟨a,b⟩ ∈ r" using group_inv_of_inv

by auto;

qed;

text{*The relation defined by a positive set is antisymmetric.*}

lemma (in group0) OrderedGroup_ZF_5_L2:

assumes A1: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"

and A2: "∀a∈G. a≠\<one> --> (a∈H) Xor (a¯∈H)"

shows "antisym(r)"

proof -

{ fix a b assume A3: "⟨a,b⟩ ∈ r" "⟨b,a⟩ ∈ r"

with A1 have T: "a∈G" "b∈G" by auto;

{ assume A4: "a≠b"

with A1 A3 have "a¯·b ∈ G" "a¯·b ∈ H" "(a¯·b)¯ ∈ H"

using inverse_in_group group0_2_L1 monoid0.group0_1_L1 group0_2_L12

by auto;

with A2 have "a¯·b = \<one>" using Xor_def by auto;

with T A4 have False using group0_2_L11 by auto;

} then have "a=b" by auto;

} then show "antisym(r)" by (rule antisymI);

qed;

text{*The relation defined by a positive set is transitive.*}

lemma (in group0) OrderedGroup_ZF_5_L3:

assumes A1: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"

and A2: "H⊆G" "H {is closed under} P"

shows "trans(r)"

proof -

{ fix a b c assume "⟨a,b⟩ ∈ r" "⟨b,c⟩ ∈ r"

with A1 have

"a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"

"b∈G ∧ c∈G ∧ b¯·c ∈ H ∪ {\<one>}"

using OrderedGroup_ZF_5_L1 by auto;

with A2 have

I: "a∈G" "b∈G" "c∈G"

and "(a¯·b)·(b¯·c) ∈ H ∪ {\<one>}"

using inverse_in_group group0_2_L17 IsOpClosed_def

by auto

moreover from I have "a¯·c = (a¯·b)·(b¯·c)"

by (rule group0_2_L14A);

ultimately have "⟨a,c⟩ ∈ G×G" "a¯·c ∈ H ∪ {\<one>}"

by auto;

with A1 have "⟨a,c⟩ ∈ r" using OrderedGroup_ZF_5_L1

by auto;

} then have "∀ a b c. ⟨a, b⟩ ∈ r ∧ ⟨b, c⟩ ∈ r --> ⟨a, c⟩ ∈ r"

by blast;

then show "trans(r)" by (rule Fol1_L2);

qed;

text{*The relation defined by a positive set is translation invariant.

With our definition this step requires the group to be abelian. *}

lemma (in group0) OrderedGroup_ZF_5_L4:

assumes A1: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"

and A2: "P {is commutative on} G"

and A3: "⟨a,b⟩ ∈ r" and A4: "c∈G"

shows "⟨a·c,b·c⟩ ∈ r ∧ ⟨c·a,c·b⟩ ∈ r"

proof

from A1 A3 A4 have

I: "a∈G" "b∈G" "a·c ∈ G" "b·c ∈ G"

and II: "a¯·b ∈ H ∪ {\<one>}"

using OrderedGroup_ZF_5_L1 group_op_closed

by auto;

with A2 A4 have "(a·c)¯·(b·c) ∈ H ∪ {\<one>}"

using group0_4_L6D by simp;

with A1 I show "⟨a·c,b·c⟩ ∈ r" using OrderedGroup_ZF_5_L1

by auto;

with A2 A4 I show "⟨c·a,c·b⟩ ∈ r"

using IsCommutative_def by simp;

qed;

text{*If $H\subseteq G$ is closed under the group operation

$1\notin H$ and for every $a\in H$ we have either $a\in H$ or

$a^{-1}\in H$, then the relation "$\leq$" defined by

$a\leq b \Leftrightarrow a^{-1}b \in H$ orders the group $G$.

In such order $H$ may be the set of positive or nonnegative

elements.*}

lemma (in group0) OrderedGroup_ZF_5_L5:

assumes A1: "P {is commutative on} G"

and A2: "H⊆G" "H {is closed under} P"

and A3: "∀a∈G. a≠\<one> --> (a∈H) Xor (a¯∈H)"

and A4: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"

shows

"IsAnOrdGroup(G,P,r)"

"r {is total on} G"

"Nonnegative(G,P,r) = PositiveSet(G,P,r) ∪ {\<one>}"

proof -

from groupAssum A2 A3 A4 have

"IsAgroup(G,P)" "r ⊆ G×G" "IsPartOrder(G,r)"

using refl_def OrderedGroup_ZF_5_L2 OrderedGroup_ZF_5_L3

IsPartOrder_def by auto

moreover from A1 A4 have

"∀g∈G. ∀a b. ⟨ a,b⟩ ∈ r --> ⟨a·g,b·g⟩ ∈ r ∧ ⟨g·a,g·b⟩ ∈ r"

using OrderedGroup_ZF_5_L4 by blast;

ultimately show "IsAnOrdGroup(G,P,r)"

using IsAnOrdGroup_def by simp;

then show "Nonnegative(G,P,r) = PositiveSet(G,P,r) ∪ {\<one>}"

using group3_def group3.OrderedGroup_ZF_1_L24

by simp;

{ fix a b

assume T: "a∈G" "b∈G"

then have T1: "a¯·b ∈ G"

using inverse_in_group group_op_closed by simp;

{ assume "⟨ a,b⟩ ∉ r"

with A4 T have I: "a≠b" and II: "a¯·b ∉ H"

by auto;

from A3 T T1 I have "(a¯·b ∈ H) Xor ((a¯·b)¯ ∈ H)"

using group0_2_L11 by auto;

with A4 T II have "⟨ b,a⟩ ∈ r"

using Xor_def group0_2_L12 by simp;

} then have "⟨ a,b⟩ ∈ r ∨ ⟨ b,a⟩ ∈ r" by auto;

} then show "r {is total on} G" using IsTotal_def

by simp;

qed;

text{*If the set defined as in @{text "OrderedGroup_ZF_5_L4"} does not

contain the neutral element, then it is the positive set for the resulting

order.*}

lemma (in group0) OrderedGroup_ZF_5_L6:

assumes "P {is commutative on} G"

and "H⊆G" and "\<one> ∉ H"

and "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"

shows "PositiveSet(G,P,r) = H"

using assms group_inv_of_one group0_2_L2 PositiveSet_def

by auto;

text{*The next definition describes how we construct an order relation

from the prescribed set of positive elements.*}

definition

"OrderFromPosSet(G,P,H) ≡

{p ∈ G×G. fst(p) = snd(p) ∨ P`⟨GroupInv(G,P)`(fst(p)),snd(p)⟩ ∈ H }"

text{*The next theorem rephrases lemmas

@{text "OrderedGroup_ZF_5_L5"} and @{text "OrderedGroup_ZF_5_L6"}

using the definition of the order from the positive set

@{text "OrderFromPosSet"}. To summarize, this is what it says:

Suppose that $H\subseteq G$ is a set closed under that group operation

such that $1\notin H$ and for every nonunit group element $a$ either $a\in H$

or $a^{-1}\in H$. Define the order as $a\leq b$ iff $a=b$ or

$a^{-1}\cdot b \in H$. Then this order makes $G$ into a linearly ordered

group such $H$ is the set of positive elements (and then of course

$H \cup \{1\}$ is the set of nonnegative elements).*}

theorem (in group0) Group_ord_by_positive_set:

assumes "P {is commutative on} G"

and "H⊆G" "H {is closed under} P" "\<one> ∉ H"

and "∀a∈G. a≠\<one> --> (a∈H) Xor (a¯∈H)"

shows

"IsAnOrdGroup(G,P,OrderFromPosSet(G,P,H))"

"OrderFromPosSet(G,P,H) {is total on} G"

"PositiveSet(G,P,OrderFromPosSet(G,P,H)) = H"

"Nonnegative(G,P,OrderFromPosSet(G,P,H)) = H ∪ {\<one>}"

using assms OrderFromPosSet_def OrderedGroup_ZF_5_L5 OrderedGroup_ZF_5_L6

by auto;

section{*Odd Extensions*}

text{*In this section we verify properties of odd extensions of functions

defined on $G_+$. An odd extension of a function $f: G_+ \rightarrow G$

is a function $f^\circ : G\rightarrow G$ defined by $f^\circ (x) = f(x)$

if $x\in G_+$, $f(1) = 1$ and $f^\circ (x) = (f(x^{-1}))^{-1}$ for $x < 1$.

Such function is the unique odd function that is equal to $f$ when

restricted to $G_+$.*}

text{*The next lemma is just to see the definition of the odd extension

in the notation used in the @{text "group1"} context.*}

lemma (in group3) OrderedGroup_ZF_6_L1:

shows "f° = f ∪ {⟨a, (f`(a¯))¯⟩. a ∈ \<sm>G⇩_{+}} ∪ {⟨\<one>,\<one>⟩}"

using OddExtension_def by simp;

text{*A technical lemma that states that from a function defined on

@{text "G⇩_{+}"} with values in $G$ we have $(f(a^{-1}))^{-1}\in G$.*}

lemma (in group3) OrderedGroup_ZF_6_L2:

assumes "f: G⇩_{+}->G" and "a∈\<sm>G⇩_{+}"

shows

"f`(a¯) ∈ G"

"(f`(a¯))¯ ∈ G"

using assms OrderedGroup_ZF_1_L27 apply_funtype

OrderedGroup_ZF_1_L1 group0.inverse_in_group

by auto;

text{*The main theorem about odd extensions. It basically says that the odd

extension of a function is what we want to to be.*}

lemma (in group3) odd_ext_props:

assumes A1: "r {is total on} G" and A2: "f: G⇩_{+}->G"

shows

"f° : G -> G"

"∀a∈G⇩_{+}. (f°)`(a) = f`(a)"

"∀a∈(\<sm>G⇩_{+}). (f°)`(a) = (f`(a¯))¯"

"(f°)`(\<one>) = \<one>"

proof -

from A1 A2 have I:

"f: G⇩_{+}->G"

"∀a∈\<sm>G⇩_{+}. (f`(a¯))¯ ∈ G"

"G⇩_{+}∩(\<sm>G⇩_{+}) = 0"

"\<one> ∉ G⇩_{+}∪(\<sm>G⇩_{+})"

"f° = f ∪ {⟨a, (f`(a¯))¯⟩. a ∈ \<sm>G⇩_{+}} ∪ {⟨\<one>,\<one>⟩}"

using OrderedGroup_ZF_6_L2 OrdGroup_decomp2 OrderedGroup_ZF_6_L1

by auto;

then have "f°: G⇩_{+}∪ (\<sm>G⇩_{+}) ∪ {\<one>} ->G∪G∪{\<one>}"

by (rule func1_1_L11E);

moreover from A1 have

"G⇩_{+}∪ (\<sm>G⇩_{+}) ∪ {\<one>} = G"

"G∪G∪{\<one>} = G"

using OrdGroup_decomp2 OrderedGroup_ZF_1_L1 group0.group0_2_L2

by auto;

ultimately show "f° : G -> G" by simp;

from I show "∀a∈G⇩_{+}. (f°)`(a) = f`(a)"

by (rule func1_1_L11E);

from I show "∀a∈(\<sm>G⇩_{+}). (f°)`(a) = (f`(a¯))¯"

by (rule func1_1_L11E);

from I show "(f°)`(\<one>) = \<one>"

by (rule func1_1_L11E);

qed;

text{*Odd extensions are odd, of course.*}

lemma (in group3) oddext_is_odd:

assumes A1: "r {is total on} G" and A2: "f: G⇩_{+}->G"

and A3: "a∈G"

shows "(f°)`(a¯) = ((f°)`(a))¯"

proof -

from A1 A3 have "a∈G⇩_{+}∨ a ∈ (\<sm>G⇩_{+}) ∨ a=\<one>"

using OrdGroup_decomp2 by blast;

moreover

{ assume "a∈G⇩_{+}"

with A1 A2 have "a¯ ∈ \<sm>G⇩_{+}" and "(f°)`(a) = f`(a)"

using OrderedGroup_ZF_1_L25 odd_ext_props by auto;

with A1 A2 have

"(f°)`(a¯) = (f`((a¯)¯))¯" and "(f`(a))¯ = ((f°)`(a))¯"

using odd_ext_props by auto;

with A3 have "(f°)`(a¯) = ((f°)`(a))¯"

using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv

by simp }

moreover

{ assume A4: "a ∈ \<sm>G⇩_{+}"

with A1 A2 have "a¯ ∈ G⇩_{+}" and "(f°)`(a) = (f`(a¯))¯"

using OrderedGroup_ZF_1_L27 odd_ext_props

by auto;

with A1 A2 A4 have "(f°)`(a¯) = ((f°)`(a))¯"

using odd_ext_props OrderedGroup_ZF_6_L2

OrderedGroup_ZF_1_L1 group0.group_inv_of_inv

by simp; }

moreover

{ assume "a = \<one>"

with A1 A2 have "(f°)`(a¯) = ((f°)`(a))¯"

using OrderedGroup_ZF_1_L1 group0.group_inv_of_one

odd_ext_props by simp;

}

ultimately show "(f°)`(a¯) = ((f°)`(a))¯"

by auto;

qed;

text{*Another way of saying that odd extensions are odd.*}

lemma (in group3) oddext_is_odd_alt:

assumes A1: "r {is total on} G" and A2: "f: G⇩_{+}->G"

and A3: "a∈G"

shows "((f°)`(a¯))¯ = (f°)`(a)"

proof -

from A1 A2 have

"f° : G -> G"

"∀a∈G. (f°)`(a¯) = ((f°)`(a))¯"

using odd_ext_props oddext_is_odd by auto

then have "∀a∈G. ((f°)`(a¯))¯ = (f°)`(a)"

using OrderedGroup_ZF_1_L1 group0.group0_6_L2 by simp;

with A3 show "((f°)`(a¯))¯ = (f°)`(a)" by simp;

qed;

section{*Functions with infinite limits*}

text{*In this section we consider functions $f: G\rightarrow G$ with the

property that for $f(x)$ is arbitrarily large for large enough $x$.

More precisely, for every $a\in G$ there exist $b\in G_+$ such that

for every $x\geq b$ we have $f(x)\geq a$. In a sense this means that

$\lim_{x\rightarrow \infty}f(x) = \infty$, hence the title of this section.

We also prove dual statements for functions such that

$\lim_{x\rightarrow -\infty}f(x) = -\infty$.

*}

text{*If an image of a set by a function with infinite positive limit

is bounded above, then the set itself is bounded above.*}

lemma (in group3) OrderedGroup_ZF_7_L1:

assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}" and

A3: "f:G->G" and

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

A5: "A⊆G" and

A6: "IsBoundedAbove(f``(A),r)"

shows "IsBoundedAbove(A,r)"

proof -

{ assume "¬IsBoundedAbove(A,r)"

then have I: "∀u. ∃x∈A. ¬(x\<lsq>u)"

using IsBoundedAbove_def by auto;

have "∀a∈G. ∃y∈f``(A). a\<lsq>y"

proof -

{ fix a assume "a∈G"

with A4 obtain b where

II: "b∈G⇩_{+}" and III: "∀x. b\<lsq>x --> a \<lsq> f`(x)"

by auto;

from I obtain x where IV: "x∈A" and "¬(x\<lsq>b)"

by auto;

with A1 A5 II have

"r {is total on} G"

"x∈G" "b∈G" "¬(x\<lsq>b)"

using PositiveSet_def by auto;

with III have "a \<lsq> f`(x)"

using OrderedGroup_ZF_1_L8 by blast;

with A3 A5 IV have "∃y∈f``(A). a\<lsq>y"

using func_imagedef by auto;

} thus ?thesis by simp

qed

with A1 A2 A6 have False using OrderedGroup_ZF_2_L2A

by simp;

} thus ?thesis by auto;

qed;

text{*If an image of a set defined by separation

by a function with infinite positive limit

is bounded above, then the set itself is bounded above.*}

lemma (in group3) OrderedGroup_ZF_7_L2:

assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}" and

A3: "X≠0" and A4: "f:G->G" and

A5: "∀a∈G.∃b∈G⇩_{+}.∀y. b\<lsq>y --> a \<lsq> f`(y)" and

A6: "∀x∈X. b(x) ∈ G ∧ f`(b(x)) \<lsq> U"

shows "∃u.∀x∈X. b(x) \<lsq> u"

proof -

let ?A = "{b(x). x∈X}"

from A6 have I: "?A⊆G" by auto;

moreover note assms

moreover have "IsBoundedAbove(f``(?A),r)"

proof -

from A4 A6 I have "∀z∈f``(?A). ⟨z,U⟩ ∈ r"

using func_imagedef by simp;

then show "IsBoundedAbove(f``(?A),r)"

by (rule Order_ZF_3_L10);

qed;

ultimately have "IsBoundedAbove(?A,r)" using OrderedGroup_ZF_7_L1

by simp;

with A3 have "∃u.∀y∈?A. y \<lsq> u"

using IsBoundedAbove_def by simp;

then show "∃u.∀x∈X. b(x) \<lsq> u" by auto;

qed;

text{*If the image of a set defined by separation

by a function with infinite negative limit

is bounded below, then the set itself is bounded above.

This is dual to @{text "OrderedGroup_ZF_7_L2"}.*}

lemma (in group3) OrderedGroup_ZF_7_L3:

assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}" and

A3: "X≠0" and A4: "f:G->G" and

A5: "∀a∈G.∃b∈G⇩_{+}.∀y. b\<lsq>y --> f`(y¯) \<lsq> a" and

A6: "∀x∈X. b(x) ∈ G ∧ L \<lsq> f`(b(x))"

shows "∃l.∀x∈X. l \<lsq> b(x)"

proof -

let ?g = "GroupInv(G,P) O f O GroupInv(G,P)"

from ordGroupAssum have I: "GroupInv(G,P) : G->G"

using IsAnOrdGroup_def group0_2_T2 by simp;

with A4 have II: "∀x∈G. ?g`(x) = (f`(x¯))¯"

using func1_1_L18 by simp;

note A1 A2 A3

moreover from A4 I have "?g : G->G"

using comp_fun by blast;

moreover have "∀a∈G.∃b∈G⇩_{+}.∀y. b\<lsq>y --> a \<lsq> ?g`(y)"

proof -

{ fix a assume A7: "a∈G"

then have "a¯ ∈ G"

using OrderedGroup_ZF_1_L1 group0.inverse_in_group

by simp;

with A5 obtain b where

III: "b∈G⇩_{+}" and "∀y. b\<lsq>y --> f`(y¯) \<lsq> a¯"

by auto;

with II A7 have "∀y. b\<lsq>y --> a \<lsq> ?g`(y)"

using OrderedGroup_ZF_1_L5AD OrderedGroup_ZF_1_L4

by simp;

with III have "∃b∈G⇩_{+}.∀y. b\<lsq>y --> a \<lsq> ?g`(y)"

by auto;

} then show "∀a∈G.∃b∈G⇩_{+}.∀y. b\<lsq>y --> a \<lsq> ?g`(y)"

by simp;

qed;

moreover have "∀x∈X. b(x)¯ ∈ G ∧ ?g`(b(x)¯) \<lsq> L¯"

proof-

{ fix x assume "x∈X"

with A6 have

T: "b(x) ∈ G" "b(x)¯ ∈ G" and "L \<lsq> f`(b(x))"

using OrderedGroup_ZF_1_L1 group0.inverse_in_group

by auto;

then have "(f`(b(x)))¯ \<lsq> L¯"

using OrderedGroup_ZF_1_L5 by simp;

moreover from II T have "(f`(b(x)))¯ = ?g`(b(x)¯)"

using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv

by simp;

ultimately have "?g`(b(x)¯) \<lsq> L¯" by simp;

with T have "b(x)¯ ∈ G ∧ ?g`(b(x)¯) \<lsq> L¯"

by simp;

} then show "∀x∈X. b(x)¯ ∈ G ∧ ?g`(b(x)¯) \<lsq> L¯"

by simp;

qed;

ultimately have "∃u.∀x∈X. (b(x))¯ \<lsq> u"

by (rule OrderedGroup_ZF_7_L2);

then have "∃u.∀x∈X. u¯ \<lsq> (b(x)¯)¯"

using OrderedGroup_ZF_1_L5 by auto;

with A6 show "∃l.∀x∈X. l \<lsq> b(x)"

using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv

by auto;

qed;

text{*The next lemma combines @{text "OrderedGroup_ZF_7_L2"} and

@{text "OrderedGroup_ZF_7_L3"} to show that if an image of a set

defined by separation by a function with infinite limits is bounded,

then the set itself i bounded.*}

lemma (in group3) OrderedGroup_ZF_7_L4:

assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}" and

A3: "X≠0" and A4: "f:G->G" and

A5: "∀a∈G.∃b∈G⇩_{+}.∀y. b\<lsq>y --> a \<lsq> f`(y)" and

A6: "∀a∈G.∃b∈G⇩_{+}.∀y. b\<lsq>y --> f`(y¯) \<lsq> a" and

A7: "∀x∈X. b(x) ∈ G ∧ L \<lsq> f`(b(x)) ∧ f`(b(x)) \<lsq> U"

shows "∃M.∀x∈X. |b(x)| \<lsq> M"

proof -

from A7 have

I: "∀x∈X. b(x) ∈ G ∧ f`(b(x)) \<lsq> U" and

II: "∀x∈X. b(x) ∈ G ∧ L \<lsq> f`(b(x))"

by auto;

from A1 A2 A3 A4 A5 I have "∃u.∀x∈X. b(x) \<lsq> u"

by (rule OrderedGroup_ZF_7_L2);

moreover from A1 A2 A3 A4 A6 II have "∃l.∀x∈X. l \<lsq> b(x)"

by (rule OrderedGroup_ZF_7_L3);

ultimately have "∃u l. ∀x∈X. l\<lsq>b(x) ∧ b(x) \<lsq> u"

by auto;

with A1 have "∃u l.∀x∈X. |b(x)| \<lsq> GreaterOf(r,|l|,|u|)"

using OrderedGroup_ZF_3_L10 by blast;

then show "∃M.∀x∈X. |b(x)| \<lsq> M"

by auto;

qed;

end