Search Result: $1

Results of 1 - 1 of about 826 for $1 (0.066 sec.)

Theory Int_ZF_IML (Isabelle2019: June 2019): #score: 5500; @digest: 43d9e29328b1b49384d6b5a5411e0faf; @id: 133953; @mdate: 2019-08-01T18:34:01Z; @size: 312691; @type: text/html; content-type: text/html; charset=utf-8; #keywords: ∈ℤ" (335022), orderedgroup (230730), integerorder (194390), integeraddition (190715), int0 (161323), group3 (157215), lsq (128638), ퟬ\< (105662), zf (81361), lemma (79370), ퟭ" (75563), integermultiplication (75302), ퟭ\< (58809), ∈ℤ. (57109), simp (55127), ퟬ" (52689), theneutralelement (38274), ℤ" (37499), group0 (37166), ퟭ= (31280), assms (30472), induction (30349), qed (25899), assumes (24381), integers (24095), ‹ (24037), proof (23358), inequality (21321), ∈ (21288), \< (16805), ⟩ (16656), nonnegative (15746); Theory Int_ZF_IML theory Int_ZF_IML imports OrderedGroup_ZF_1 Int Nat_ZF_IML (* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2005, 2006 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Integers - introduction› theory Int_ZF_IML imports OrderedGroup_ZF_1 Finite_ZF_1 ZF.Int Nat_ZF_IML begin text ‹This theory file is an interface between the old-style Isabelle (ZF logic) material on integers and the IsarMathLib project. Here we redefine the meta-level operations on integers (addition and multiplication) to convert them to ZF-functions and show that integers form a commutative group with respect to addition and commutative monoid with respect to multiplication. Similarly, we redefine the order on integers as a relation, that is a subset of $Z\times Z$. We show that a subset of intergers is bounded iff it is finite. As we are forced to use standard Isabelle notation with all these dollar signs, sharps etc. to denote "type coercions" (?) the notation is often ugly and difficult to read.› subsection ‹Addition and multiplication as ZF-functions.› text ‹In this section we provide definitions of addition and multiplication as subsets of $(Z\times Z)\times Z$. We use the (higher order) relation defined in the standard ‹Int› theory to define a subset of $Z\times Z$ that constitutes the ZF order relation corresponding to it. We define the set of positive integers using the notion of positive set from the ‹OrderedGroup_ZF› theory.› text ‹Definition of addition of integers as a binary operation on ‹int›. Recall that in standard Isabelle/ZF ‹int› is the set of integers and the sum of integers is denoted by prependig $+$ with a dollar sign.› definition "IntegerAddition ≡ { ⟨ x,c⟩ ∈ (int×int)×int. fst(x) $+ snd(x) = c}" text ‹Definition of multiplication of integers as a binary operation on ‹int›. In standard Isabelle/ZF product of integers is denoted by prepending the dollar sign to ‹*›. › definition "IntegerMultiplication ≡ { ⟨ x,c⟩ ∈ (int×int)×int. fst(x) $* snd(x) = c}" text ‹Definition of natural order on integers as a relation on ‹int›. In the standard Isabelle/ZF the inequality relation on integers is denoted ‹≤› prepended with the dollar sign.› definition "IntegerOrder ≡ {p ∈ int×int. fst(p) $≤ snd(p)}" text ‹This defines the set of positive integers.› definition "PositiveIntegers ≡ PositiveSet(int,IntegerAddition,IntegerOrder)" text ‹IntegerAddition and IntegerMultiplication are functions on ‹int × int›.› lemma Int_ZF_1_L1 : shows "IntegerAddition : int×int → int" "IntegerMultiplication : int×int → int" proof - have "{⟨ x,c⟩ ∈ (int×int)×int. fst(x) $+ snd(x) = c} ∈ int×int→int" "{⟨ x,c⟩ ∈ (int×int)×int. fst(x) $* snd(x) = c} ∈ int×int→int" using func1_1_L11A by auto then show "IntegerAddition : int×int → int" "IntegerMultiplication : int×int → int" using IntegerAddition_def IntegerMultiplication_def by auto qed text ‹The next context (locale) defines notation used for integers. We define ‹ퟬ› to denote the neutral element of addition, ‹ퟭ› as the unit of the multiplicative monoid. We introduce notation ‹m\<lsq>n› for integers and write ‹m..n› to denote the integer interval with endpoints in $m$ and $n$. ‹abs(m)› means the absolute value of $m$. This is a function defined in ‹OrderedGroup› that assigns $x$ to itself if $x$ is positive and assigns the opposite of $x$ if $x\leq 0$. Unforunately we cannot use the $|\cdot|$ notation as in the ‹OrderedGroup› theory as this notation has been hogged by the standard Isabelle's ‹Int› theory. The notation ‹\<sm>A› where $A$ is a subset of integers means the set $\{-m: m\in A\}$. The symbol ‹maxf(f,M)› denotes tha maximum of function $f$ over the set $A$. We also introduce a similar notation for the minimum.› locale int0 = fixes ints ( "ℤ" ) defines ints_def [ simp ] : "ℤ ≡ int" fixes ia ( infixl "\<ra>" 69 ) defines ia_def [ simp ] : "a\<ra>b ≡ IntegerAddition`⟨ a,b⟩" fixes iminus ( "\<rm> _" 72 ) defines rminus_def [ simp ] : "\<rm>a ≡ GroupInv(ℤ,IntegerAddition)`(a)" fixes isub ( infixl "\<rs>" 69 ) defines isub_def [ simp ] : "a\<rs>b ≡ a\<ra> (\<rm> b)" fixes imult ( infixl "⋅" 70 ) defines imult_def [ simp ] : "a⋅b ≡ IntegerMultiplication`⟨ a,b⟩" fixes setneg ( "\<sm> _" 72 ) defines setneg_def [ simp ] : "\<sm>A ≡ GroupInv(ℤ,IntegerAddition)``(A)" fixes izero ( "ퟬ" ) defines izero_def [ simp ] : "ퟬ ≡ TheNeutralElement(ℤ,IntegerAddition)" fixes ione ( "ퟭ" ) defines ione_def [ simp ] : "ퟭ ≡ TheNeutralElement(ℤ,IntegerMultiplication)" fixes itwo ( "ퟮ" ) defines itwo_def [ simp ] : "ퟮ ≡ ퟭ\<ra>ퟭ" fixes ithree ( "ퟯ" ) defines ithree_def [ simp ] : "ퟯ ≡ ퟮ\<ra>ퟭ" fixes nonnegative ( "ℤ ⇧ + " ) defines nonnegative_def [ simp ] : "ℤ ⇧ + ≡ Nonnegative(ℤ,IntegerAddition,IntegerOrder)" fixes positive ( "ℤ ⇩ + " ) defines positive_def [ simp ] : "ℤ ⇩ + ≡ PositiveSet(ℤ,IntegerAddition,IntegerOrder)" fixes abs defines abs_def [ simp ] : "abs(m) ≡ AbsoluteValue(ℤ,IntegerAddition,IntegerOrder)`(m)" fixes lesseq ( infix "\<lsq>" 60 ) defines lesseq_def [ simp ] : "m \<lsq> n ≡ ⟨m,n⟩ ∈ IntegerOrder" fixes interval ( infix ".." 70 ) defines interval_def [ simp ] : "m..n ≡ Interval(IntegerOrder,m,n)" fixes maxf defines maxf_def [ simp ] : "maxf(f,A) ≡ Maximum(IntegerOrder,f``(A))" fixes minf defines minf_def [ simp ] : "minf(f,A) ≡ Minimum(IntegerOrder,f``(A))" text ‹IntegerAddition adds integers and IntegerMultiplication multiplies integers. This states that the ZF functions ‹IntegerAddition› and ‹IntegerMultiplication› give the same results as the higher-order equivalents defined in the standard ‹Int› theory.› lemma ( in int0 ) Int_ZF_1_L2 : assumes A1 : "a ∈ ℤ" "b ∈ ℤ" shows "a\<ra>b = a $+ b" "a⋅b = a $* b" proof - let ?x = "⟨ a,b⟩" let ?c = "a $+ b" let ?d = "a $* b" from A1 have "⟨ ?x,?c⟩ ∈ {⟨ x,c⟩ ∈ (ℤ×ℤ)×ℤ. fst(x) $+ snd(x) = c}" "⟨ ?x,?d⟩ ∈ {⟨ x,d⟩ ∈ (ℤ×ℤ)×ℤ. fst(x) $* snd(x) = d}" by auto then show "a\<ra>b = a $+ b" "a⋅b = a $* b" using IntegerAddition_def IntegerMultiplication_def Int_ZF_1_L1 apply_iff by auto qed text ‹Integer addition and multiplication are associative.› lemma ( in int0 ) Int_ZF_1_L3 : assumes "x∈ℤ" "y∈ℤ" "z∈ℤ" shows "x\<ra>y\<ra>z = x\<ra>(y\<ra>z)" "x⋅y⋅z = x⋅(y⋅z)" using assms Int_ZF_1_L2 zadd_assoc zmult_assoc by auto text ‹Integer addition and multiplication are commutative.› lemma ( in int0 ) Int_ZF_1_L4 : assumes "x∈ℤ" "y∈ℤ" shows "x\<ra>y = y\<ra>x" "x⋅y = y⋅x" using assms Int_ZF_1_L2 zadd_commute zmult_commute by auto text ‹Zero is neutral for addition and one for multiplication.› lemma ( in int0 ) Int_ZF_1_L5 : assumes A1 : "x∈ℤ" shows "($# 0) \<ra> x = x ∧ x \<ra> ($# 0) = x" "($# 1)⋅x = x ∧ x⋅($# 1) = x" proof - from A1 show "($# 0) \<ra> x = x ∧ x \<ra> ($# 0) = x" using Int_ZF_1_L2 zadd_int0 Int_ZF_1_L4 by simp from A1 have "($# 1)⋅x = x" using Int_ZF_1_L2 zmult_int1 by simp with A1 show "($# 1)⋅x = x ∧ x⋅($# 1) = x" using Int_ZF_1_L4 by simp qed text ‹Zero is neutral for addition and one for multiplication.› lemma ( in int0 ) Int_ZF_1_L6 : shows "($# 0)∈ℤ ∧ (∀x∈ℤ. ($# 0)\<ra>x = x ∧ x\<ra>($# 0) = x)" "($# 1)∈ℤ ∧ (∀x∈ℤ. ($# 1)⋅x = x ∧ x⋅($# 1) = x)" using Int_ZF_1_L5 by auto text ‹Integers with addition and integers with multiplication form monoids.› theorem ( in int0 ) Int_ZF_1_T1 : shows "IsAmonoid(ℤ,IntegerAddition)" "IsAmonoid(ℤ,IntegerMultiplication)" proof - have "∃e∈ℤ. ∀x∈ℤ. e\<ra>x = x ∧ x\<ra>e = x" "∃e∈ℤ. ∀x∈ℤ. e⋅x = x ∧ x⋅e = x" using int0.Int_ZF_1_L6 by auto then show "IsAmonoid(ℤ,IntegerAddition)" "IsAmonoid(ℤ,IntegerMultiplication)" using IsAmonoid_def IsAssociative_def Int_ZF_1_L1 Int_ZF_1_L3 by auto qed text ‹Zero is the neutral element of the integers with addition and one is the neutral element of the integers with multiplication.› lemma ( in int0 ) Int_ZF_1_L8 : shows "($# 0) = ퟬ" "($# 1) = ퟭ" proof - have "monoid0(ℤ,IntegerAddition)" using Int_ZF_1_T1 monoid0_def by simp moreover have "($# 0)∈ℤ ∧ (∀x∈ℤ. IntegerAddition`⟨$# 0,x⟩ = x ∧ IntegerAddition`⟨x ,$# 0⟩ = x)" using Int_ZF_1_L6 by auto ultimately have "($# 0) = TheNeutralElement(ℤ,IntegerAddition)" by ( rule monoid0.group0_1_L4 ) then show "($# 0) = ퟬ" by simp have "monoid0(int,IntegerMultiplication)" using Int_ZF_1_T1 monoid0_def by simp moreover have "($# 1) ∈ int ∧ (∀x∈int. IntegerMultiplication`⟨$# 1, x⟩ = x ∧ IntegerMultiplication`⟨x ,$# 1⟩ = x)" using Int_ZF_1_L6 by auto ultimately have "($# 1) = TheNeutralElement(int,IntegerMultiplication)" by ( rule monoid0.group0_1_L4 ) then show "($# 1) = ퟭ" by simp qed text ‹$0$ and $1$, as defined in ‹int0› context, are integers.› lemma ( in int0 ) Int_ZF_1_L8A : shows "ퟬ ∈ ℤ" "ퟭ ∈ ℤ" proof - have "($# 0) ∈ ℤ" "($# 1) ∈ ℤ" by auto then show "ퟬ ∈ ℤ" "ퟭ ∈ ℤ" using Int_ZF_1_L8 by auto qed text ‹Zero is not one.› lemma ( in int0 ) int_zero_not_one : shows "ퟬ ≠ ퟭ" proof - have "($# 0) ≠ ($# 1)" by simp then show "ퟬ ≠ ퟭ" using Int_ZF_1_L8 by simp qed text ‹The set of integers is not empty, of course.› lemma ( in int0 ) int_not_empty : shows "ℤ ≠ 0" using Int_ZF_1_L8A by auto text ‹The set of integers has more than just zero in it.› lemma ( in int0 ) int_not_trivial : shows "ℤ ≠ {ퟬ}" using Int_ZF_1_L8A int_zero_not_one by blast text ‹Each integer has an inverse (in the addition sense).› lemma ( in int0 ) Int_ZF_1_L9 : assumes A1 : "g ∈ ℤ" shows "∃ b∈ℤ. g\<ra>b = ퟬ" proof - from A1 have "g\<ra> $-g = ퟬ" using Int_ZF_1_L2 Int_ZF_1_L8 by simp thus ?thesis by auto qed text ‹Integers with addition form an abelian group. This also shows that we can apply all theorems proven in the proof contexts (locales) that require the assumpion that some pair of sets form a group like locale ‹group0›.› theorem Int_ZF_1_T2 : shows "IsAgroup(int,IntegerAddition)" "IntegerAddition {is commutative on} int" "group0(int,IntegerAddition)" using int0.Int_ZF_1_T1 int0.Int_ZF_1_L9 IsAgroup_def group0_def int0.Int_ZF_1_L4 IsCommutative_def by auto text ‹What is the additive group inverse in the group of integers?› lemma ( in int0 ) Int_ZF_1_L9A : assumes A1 : "m∈ℤ" shows "$-m = \<rm>m" proof - from A1 have "m∈int" "$-m ∈ int" "IntegerAddition`⟨ m,$-m⟩ = TheNeutralElement(int,IntegerAddition)" using zminus_type Int_ZF_1_L2 Int_ZF_1_L8 by auto then have "$-m = GroupInv(int,IntegerAddition)`(m)" using Int_ZF_1_T2 group0.group0_2_L9 by blast then show ?thesis by simp qed text ‹Subtracting integers corresponds to adding the negative.› lemma ( in int0 ) Int_ZF_1_L10 : assumes A1 : "m∈ℤ" "n∈ℤ" shows "m\<rs>n = m $+ $-n" using assms Int_ZF_1_T2 group0.inverse_in_group Int_ZF_1_L9A Int_ZF_1_L2 by simp text ‹Negative of zero is zero.› lemma ( in int0 ) Int_ZF_1_L11 : shows "(\<rm>ퟬ) = ퟬ" using Int_ZF_1_T2 group0.group_inv_of_one by simp text ‹A trivial calculation lemma that allows to subtract and add one.› lemma Int_ZF_1_L12 : assumes "m∈int" shows "m $- $#1 $+ $#1 = m" using assms eq_zdiff_iff by auto text ‹A trivial calculation lemma that allows to subtract and add one, version with ZF-operation.› lemma ( in int0 ) Int_ZF_1_L13 : assumes "m∈ℤ" shows "(m $- $#1) \<ra> ퟭ = m" using assms Int_ZF_1_L8A Int_ZF_1_L2 Int_ZF_1_L8 Int_ZF_1_L12 by simp text ‹Adding or subtracing one changes integers.› lemma ( in int0 ) Int_ZF_1_L14 : assumes A1 : "m∈ℤ" shows "m\<ra>ퟭ ≠ m" "m\<rs>ퟭ ≠ m" proof - { assume "m\<ra>ퟭ = m" with A1 have "group0(ℤ,IntegerAddition)" "m∈ℤ" "ퟭ∈ℤ" "IntegerAddition`⟨m,ퟭ⟩ = m" using Int_ZF_1_T2 Int_ZF_1_L8A by auto then have "ퟭ = TheNeutralElement(ℤ,IntegerAddition)" by ( rule group0.group0_2_L7 ) then have False using int_zero_not_one by simp } then show I : "m\<ra>ퟭ ≠ m" by auto { from A1 have "m \<rs> ퟭ \<ra> ퟭ = m" using Int_ZF_1_L8A Int_ZF_1_T2 group0.inv_cancel_two by simp moreover assume "m\<rs>ퟭ = m" ultimately have "m \<ra> ퟭ = m" by simp with I have False by simp } then show "m\<rs>ퟭ ≠ m" by auto qed text ‹If the difference is zero, the integers are equal.› lemma ( in int0 ) Int_ZF_1_L15 : assumes A1 : "m∈ℤ" "n∈ℤ" and A2 : "m\<rs>n = ퟬ" shows "m=n" proof - let ?G = "ℤ" let ?f = "IntegerAddition" from A1 A2 have "group0(?G, ?f)" "m ∈ ?G" "n ∈ ?G" "?f`⟨m, GroupInv(?G, ?f)`(n)⟩ = TheNeutralElement(?G, ?f)" using Int_ZF_1_T2 by auto then show "m=n" by ( rule group0.group0_2_L11A ) qed subsection ‹Integers as an ordered group› text ‹In this section we define order on integers as a relation, that is a subset of $Z\times Z$ and show that integers form an ordered group.› text ‹The next lemma interprets the order definition one way.› lemma ( in int0 ) Int_ZF_2_L1 : assumes A1 : "m∈ℤ" "n∈ℤ" and A2 : "m $≤ n" shows "m \<lsq> n" proof - from A1 A2 have "⟨ m,n⟩ ∈ {x∈ℤ×ℤ. fst(x) $≤ snd(x)}" by simp then show ?thesis using IntegerOrder_def by simp qed text ‹The next lemma interprets the definition the other way.› lemma ( in int0 ) Int_ZF_2_L1A : assumes A1 : "m \<lsq> n" shows "m $≤ n" "m∈ℤ" "n∈ℤ" proof - from A1 have "⟨ m,n⟩ ∈ {p∈ℤ×ℤ. fst(p) $≤ snd(p)}" using IntegerOrder_def by simp thus "m $≤ n" "m∈ℤ" "n∈ℤ" by auto qed text ‹Integer order is a relation on integers.› lemma Int_ZF_2_L1B : shows "IntegerOrder ⊆ int×int" proof fix x assume "x∈IntegerOrder" then have "x ∈ {p∈int×int. fst(p) $≤ snd(p)}" using IntegerOrder_def by simp then show "x∈int×int" by simp qed text ‹The way we define the notion of being bounded below, its sufficient for the relation to be on integers for all bounded below sets to be subsets of integers.› lemma ( in int0 ) Int_ZF_2_L1C : assumes A1 : "IsBoundedBelow(A,IntegerOrder)" shows "A⊆ℤ" proof - from A1 have "IntegerOrder ⊆ ℤ×ℤ" "IsBoundedBelow(A,IntegerOrder)" using Int_ZF_2_L1B by auto then show "A⊆ℤ" by ( rule Order_ZF_3_L1B ) qed text ‹The order on integers is reflexive.› lemma ( in int0 ) int_ord_is_refl : shows "refl(ℤ,IntegerOrder)" using Int_ZF_2_L1 zle_refl refl_def by auto text ‹The essential condition to show antisymmetry of the order on integers.› lemma ( in int0 ) Int_ZF_2_L3 : assumes A1 : "m \<lsq> n" "n \<lsq> m" shows "m=n" proof - from A1 have "m $≤ n" "n $≤ m" "m∈ℤ" "n∈ℤ" using Int_ZF_2_L1A by auto then show "m=n" using zle_anti_sym by auto qed text ‹The order on integers is antisymmetric.› lemma ( in int0 ) Int_ZF_2_L4 : shows "antisym(IntegerOrder)" proof - have "∀m n. m \<lsq> n ∧ n \<lsq> m ⟶ m=n" using Int_ZF_2_L3 by auto then show ?thesis using imp_conj antisym_def by simp qed text ‹The essential condition to show that the order on integers is transitive.› lemma Int_ZF_2_L5 : assumes A1 : "⟨m,n⟩ ∈ IntegerOrder" "⟨n,k⟩ ∈ IntegerOrder" shows "⟨m,k⟩ ∈ IntegerOrder" proof - from A1 have T1 : "m $≤ n" "n $≤ k" and T2 : "m∈int" "k∈int" using int0.Int_ZF_2_L1A by auto from T1 have "m $≤ k" by ( rule zle_trans ) with T2 show ?thesis using int0.Int_ZF_2_L1 by simp qed text ‹The order on integers is transitive. This version is stated in the ‹int0› context using notation for integers.› lemma ( in int0 ) Int_order_transitive : assumes A1 : "m\<lsq>n" "n\<lsq>k" shows "m\<lsq>k" proof - from A1 have "⟨ m,n⟩ ∈ IntegerOrder" "⟨ n,k⟩ ∈ IntegerOrder" by auto then have "⟨ m,k⟩ ∈ IntegerOrder" by ( rule Int_ZF_2_L5 ) then show "m\<lsq>k" by simp qed text ‹The order on integers is transitive.› lemma Int_ZF_2_L6 : shows "trans(IntegerOrder)" proof - have "∀ m n k. ⟨m, n⟩ ∈ IntegerOrder ∧ ⟨n, k⟩ ∈ IntegerOrder ⟶ ⟨m, k⟩ ∈ IntegerOrder" using Int_ZF_2_L5 by blast then show ?thesis by ( rule Fol1_L2 ) qed text ‹The order on integers is a partial order.› lemma Int_ZF_2_L7 : shows "IsPartOrder(int,IntegerOrder)" using int0.int_ord_is_refl int0.Int_ZF_2_L4 Int_ZF_2_L6 IsPartOrder_def by simp text ‹The essential condition to show that the order on integers is preserved by translations.› lemma ( in int0 ) int_ord_transl_inv : assumes A1 : "k ∈ ℤ" and A2 : "m \<lsq> n" shows "m\<ra>k \<lsq> n\<ra>k " "k\<ra>m\<lsq> k\<ra>n " proof - from A2 have "m $≤ n" and "m∈ℤ" "n∈ℤ" using Int_ZF_2_L1A by auto with A1 show "m\<ra>k \<lsq> n\<ra>k " "k\<ra>m\<lsq> k\<ra>n " using zadd_right_cancel_zle zadd_left_cancel_zle Int_ZF_1_L2 Int_ZF_1_L1 apply_funtype Int_ZF_1_L2 Int_ZF_2_L1 Int_ZF_1_L2 by auto qed text ‹Integers form a linearly ordered group. We can apply all theorems proven in group3 context to integers.› theorem ( in int0 ) Int_ZF_2_T1 : shows "IsAnOrdGroup(ℤ,IntegerAddition,IntegerOrder)" "IntegerOrder {is total on} ℤ" "group3(ℤ,IntegerAddition,IntegerOrder)" "IsLinOrder(ℤ,IntegerOrder)" proof - have "∀k∈ℤ. ∀m n. m \<lsq> n ⟶ m\<ra>k \<lsq> n\<ra>k ∧ k\<ra>m\<lsq> k\<ra>n" using int_ord_transl_inv by simp then show T1 : "IsAnOrdGroup(ℤ,IntegerAddition,IntegerOrder)" using Int_ZF_1_T2 Int_ZF_2_L1B Int_ZF_2_L7 IsAnOrdGroup_def by simp then show "group3(ℤ,IntegerAddition,IntegerOrder)" using group3_def by simp have "∀n∈ℤ. ∀m∈ℤ. n\<lsq>m ∨ m\<lsq>n" using zle_linear Int_ZF_2_L1 by auto then show "IntegerOrder {is total on} ℤ" using IsTotal_def by simp with T1 show "IsLinOrder(ℤ,IntegerOrder)" using IsAnOrdGroup_def IsPartOrder_def IsLinOrder_def by simp qed text ‹If a pair $(i,m)$ belongs to the order relation on integers and $i\neq m$, then $i<m$ in the sense of defined in the standard Isabelle's Int.thy.› lemma ( in int0 ) Int_ZF_2_L9 : assumes A1 : "i \<lsq> m" and A2 : "i≠m" shows "i $< m" proof - from A1 have "i $≤ m" "i∈ℤ" "m∈ℤ" using Int_ZF_2_L1A by auto with A2 show "i $< m" using zle_def by simp qed text ‹This shows how Isabelle's ‹$<› operator translates to IsarMathLib notation.› lemma ( in int0 ) Int_ZF_2_L9AA : assumes A1 : "m∈ℤ" "n∈ℤ" and A2 : "m $< n" shows "m\<lsq>n" "m ≠ n" using assms zle_def Int_ZF_2_L1 by auto text ‹A small technical lemma about putting one on the other side of an inequality.› lemma ( in int0 ) Int_ZF_2_L9A : assumes A1 : "k∈ℤ" and A2 : "m \<lsq> k $- ($# 1)" shows "m\<ra>ퟭ \<lsq> k" proof - from A2 have "m\<ra>ퟭ \<lsq> (k $- ($# 1)) \<ra> ퟭ" using Int_ZF_1_L8A int_ord_transl_inv by simp with A1 show "m\<ra>ퟭ \<lsq> k" using Int_ZF_1_L13 by simp qed text ‹We can put any integer on the other side of an inequality reversing its sign.› lemma ( in int0 ) Int_ZF_2_L9B : assumes "i∈ℤ" "m∈ℤ" "k∈ℤ" shows "i\<ra>m \<lsq> k ⟷ i \<lsq> k\<rs>m" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L9A by simp text ‹A special case of ‹Int_ZF_2_L9B› with weaker assumptions.› lemma ( in int0 ) Int_ZF_2_L9C : assumes "i∈ℤ" "m∈ℤ" and "i\<rs>m \<lsq> k" shows "i \<lsq> k\<ra>m" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L9B by simp text ‹Taking (higher order) minus on both sides of inequality reverses it.› lemma ( in int0 ) Int_ZF_2_L10 : assumes "k \<lsq> i" shows "(\<rm>i) \<lsq> (\<rm>k)" "$-i \<lsq> $-k" using assms Int_ZF_2_L1A Int_ZF_1_L9A Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5 by auto text ‹Taking minus on both sides of inequality reverses it, version with a negative on one side.› lemma ( in int0 ) Int_ZF_2_L10AA : assumes "n∈ℤ" "m\<lsq>(\<rm>n)" shows "n\<lsq>(\<rm>m)" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5AD by simp text ‹We can cancel the same element on on both sides of an inequality, a version with minus on both sides.› lemma ( in int0 ) Int_ZF_2_L10AB : assumes "m∈ℤ" "n∈ℤ" "k∈ℤ" and "m\<rs>n \<lsq> m\<rs>k" shows "k\<lsq>n" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5AF by simp text ‹If an integer is nonpositive, then its opposite is nonnegative.› lemma ( in int0 ) Int_ZF_2_L10A : assumes "k \<lsq> ퟬ" shows "ퟬ\<lsq>(\<rm>k)" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5A by simp text ‹If the opposite of an integers is nonnegative, then the integer is nonpositive.› lemma ( in int0 ) Int_ZF_2_L10B : assumes "k∈ℤ" and "ퟬ\<lsq>(\<rm>k)" shows "k\<lsq>ퟬ" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5AA by simp text ‹Adding one to an integer corresponds to taking a successor for a natural number.› lemma ( in int0 ) Int_ZF_2_L11 : shows "i $+ $# n $+ ($# 1) = i $+ $# succ(n)" proof - have "$# succ(n) = $#1 $+ $# n" using int_succ_int_1 by blast then have "i $+ $# succ(n) = i $+ ($# n $+ $#1)" using zadd_commute by simp then show ?thesis using zadd_assoc by simp qed text ‹Adding a natural number increases integers.› lemma ( in int0 ) Int_ZF_2_L12 : assumes A1 : "i∈ℤ" and A2 : "n∈nat" shows "i \<lsq> i $+ $#n" proof - { assume "n = 0" with A1 have "i \<lsq> i $+ $#n" using zadd_int0 int_ord_is_refl refl_def by simp } moreover { assume "n≠0" with A2 obtain k where "k∈nat" "n = succ(k)" using Nat_ZF_1_L3 by auto with A1 have "i \<lsq> i $+ $#n" using zless_succ_zadd zless_imp_zle Int_ZF_2_L1 by simp } ultimately show ?thesis by blast qed text ‹Adding one increases integers.› lemma ( in int0 ) Int_ZF_2_L12A : assumes A1 : "j\<lsq>k" shows "j \<lsq> k $+ $#1" "j \<lsq> k\<ra>ퟭ" proof - from A1 have T1 : "j∈ℤ" "k∈ℤ" "j $≤ k" using Int_ZF_2_L1A by auto moreover from T1 have "k $≤ k $+ $#1" using Int_ZF_2_L12 Int_ZF_2_L1A by simp ultimately have "j $≤ k $+ $#1" using zle_trans by fast with T1 show "j \<lsq> k $+ $#1" using Int_ZF_2_L1 by simp with T1 have "j\<lsq> k\<ra>$#1" using Int_ZF_1_L2 by simp then show "j \<lsq> k\<ra>ퟭ" using Int_ZF_1_L8 by simp qed text ‹Adding one increases integers, yet one more version.› lemma ( in int0 ) Int_ZF_2_L12B : assumes A1 : "m∈ℤ" shows "m \<lsq> m\<ra>ퟭ" using assms int_ord_is_refl refl_def Int_ZF_2_L12A by simp text ‹If $k+1 = m+n$, where $n$ is a non-zero natural number, then $m\leq k$.› lemma ( in int0 ) Int_ZF_2_L13 : assumes A1 : "k∈ℤ" "m∈ℤ" and A2 : "n∈nat" and A3 : "k $+ ($# 1) = m $+ $# succ(n)" shows "m \<lsq> k" proof - from A1 have "k∈ℤ" "m $+ $# n ∈ ℤ" by auto moreover from assms have "k $+ $# 1 = m $+ $# n $+ $#1" using Int_ZF_2_L11 by simp ultimately have "k = m $+ $# n" using zadd_right_cancel by simp with A1 A2 show ?thesis using Int_ZF_2_L12 by simp qed text ‹The absolute value of an integer is an integer.› lemma ( in int0 ) Int_ZF_2_L14 : assumes A1 : "m∈ℤ" shows "abs(m) ∈ ℤ" proof - have "AbsoluteValue(ℤ,IntegerAddition,IntegerOrder) : ℤ→ℤ" using Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L1 by simp with A1 show ?thesis using apply_funtype by simp qed text ‹If two integers are nonnegative, then the opposite of one is less or equal than the other and the sum is also nonnegative.› lemma ( in int0 ) Int_ZF_2_L14A : assumes "ퟬ\<lsq>m" "ퟬ\<lsq>n" shows "(\<rm>m) \<lsq> n" "ퟬ \<lsq> m \<ra> n" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5AC group3.OrderedGroup_ZF_1_L12 by auto text ‹We can increase components in an estimate.› lemma ( in int0 ) Int_ZF_2_L15 : assumes "b\<lsq>b ⇩ 1 " "c\<lsq>c ⇩ 1 " and "a\<lsq>b\<ra>c" shows "a\<lsq>b ⇩ 1 \<ra>c ⇩ 1 " proof - from assms have "group3(ℤ,IntegerAddition,IntegerOrder)" "⟨a,IntegerAddition`⟨ b,c⟩⟩ ∈ IntegerOrder" "⟨b,b ⇩ 1 ⟩ ∈ IntegerOrder" "⟨c,c ⇩ 1 ⟩ ∈ IntegerOrder" using Int_ZF_2_T1 by auto then have "⟨a,IntegerAddition`⟨ b ⇩ 1 ,c ⇩ 1 ⟩⟩ ∈ IntegerOrder" by ( rule group3.OrderedGroup_ZF_1_L5E ) thus ?thesis by simp qed text ‹We can add or subtract the sides of two inequalities.› lemma ( in int0 ) int_ineq_add_sides : assumes "a\<lsq>b" and "c\<lsq>d" shows "a\<ra>c \<lsq> b\<ra>d" "a\<rs>d \<lsq> b\<rs>c" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5B group3.OrderedGroup_ZF_1_L5I by auto text ‹We can increase the second component in an estimate.› lemma ( in int0 ) Int_ZF_2_L15A : assumes "b∈ℤ" and "a\<lsq>b\<ra>c" and A3 : "c\<lsq>c ⇩ 1 " shows "a\<lsq>b\<ra>c ⇩ 1 " proof - from assms have "group3(ℤ,IntegerAddition,IntegerOrder)" "b ∈ ℤ" "⟨a,IntegerAddition`⟨ b,c⟩⟩ ∈ IntegerOrder" "⟨c,c ⇩ 1 ⟩ ∈ IntegerOrder" using Int_ZF_2_T1 by auto then have "⟨a,IntegerAddition`⟨ b,c ⇩ 1 ⟩⟩ ∈ IntegerOrder" by ( rule group3.OrderedGroup_ZF_1_L5D ) thus ?thesis by simp qed text ‹If we increase the second component in a sum of three integers, the whole sum inceases.› lemma ( in int0 ) Int_ZF_2_L15C : assumes A1 : "m∈ℤ" "n∈ℤ" and A2 : "k \<lsq> L" shows "m\<ra>k\<ra>n \<lsq> m\<ra>L\<ra>n" proof - let ?P = "IntegerAddition" from assms have "group3(int,?P,IntegerOrder)" "m ∈ int" "n ∈ int" "⟨k,L⟩ ∈ IntegerOrder" using Int_ZF_2_T1 by auto then have "⟨?P`⟨?P`⟨ m,k⟩,n⟩, ?P`⟨?P`⟨ m,L⟩,n⟩ ⟩ ∈ IntegerOrder" by ( rule group3.OrderedGroup_ZF_1_L10 ) then show "m\<ra>k\<ra>n \<lsq> m\<ra>L\<ra>n" by simp qed text ‹We don't decrease an integer by adding a nonnegative one.› lemma ( in int0 ) Int_ZF_2_L15D : assumes "ퟬ\<lsq>n" "m∈ℤ" shows "m \<lsq> n\<ra>m" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5F by simp text ‹Some inequalities about the sum of two integers and its absolute value.› lemma ( in int0 ) Int_ZF_2_L15E : assumes "m∈ℤ" "n∈ℤ" shows "m\<ra>n \<lsq> abs(m)\<ra>abs(n)" "m\<rs>n \<lsq> abs(m)\<ra>abs(n)" "(\<rm>m)\<ra>n \<lsq> abs(m)\<ra>abs(n)" "(\<rm>m)\<rs>n \<lsq> abs(m)\<ra>abs(n)" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L6A by auto text ‹We can add a nonnegative integer to the right hand side of an inequality.› lemma ( in int0 ) Int_ZF_2_L15F : assumes "m\<lsq>k" and "ퟬ\<lsq>n" shows "m \<lsq> k\<ra>n" "m \<lsq> n\<ra>k" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L5G by auto text ‹Triangle inequality for integers.› lemma ( in int0 ) Int_triangle_ineq : assumes "m∈ℤ" "n∈ℤ" shows "abs(m\<ra>n)\<lsq>abs(m)\<ra>abs(n)" using assms Int_ZF_1_T2 Int_ZF_2_T1 group3.OrdGroup_triangle_ineq by simp text ‹Taking absolute value does not change nonnegative integers.› lemma ( in int0 ) Int_ZF_2_L16 : assumes "ퟬ\<lsq>m" shows "m∈ℤ ⇧ + " and "abs(m) = m" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L2 group3.OrderedGroup_ZF_3_L2 by auto text ‹$0\leq 1$, so $|1| = 1$.› lemma ( in int0 ) Int_ZF_2_L16A : shows "ퟬ\<lsq>ퟭ" and "abs(ퟭ) = ퟭ" proof - have "($# 0) ∈ ℤ" "($# 1)∈ ℤ" by auto then have "ퟬ\<lsq>ퟬ" and T1 : "ퟭ∈ℤ" using Int_ZF_1_L8 int_ord_is_refl refl_def by auto then have "ퟬ\<lsq>ퟬ\<ra>ퟭ" using Int_ZF_2_L12A by simp with T1 show "ퟬ\<lsq>ퟭ" using Int_ZF_1_T2 group0.group0_2_L2 by simp then show "abs(ퟭ) = ퟭ" using Int_ZF_2_L16 by simp qed text ‹$1\leq 2$.› lemma ( in int0 ) Int_ZF_2_L16B : shows "ퟭ\<lsq>ퟮ" proof - have "($# 1)∈ ℤ" by simp then show "ퟭ\<lsq>ퟮ" using Int_ZF_1_L8 int_ord_is_refl refl_def Int_ZF_2_L12A by simp qed text ‹Integers greater or equal one are greater or equal zero.› lemma ( in int0 ) Int_ZF_2_L16C : assumes A1 : "ퟭ\<lsq>a" shows "ퟬ\<lsq>a" "a≠ퟬ" "ퟮ \<lsq> a\<ra>ퟭ" "ퟭ \<lsq> a\<ra>ퟭ" "ퟬ \<lsq> a\<ra>ퟭ" proof - from A1 have "ퟬ\<lsq>ퟭ" and "ퟭ\<lsq>a" using Int_ZF_2_L16A by auto then show "ퟬ\<lsq>a" by ( rule Int_order_transitive ) have I : "ퟬ\<lsq>ퟭ" using Int_ZF_2_L16A by simp have "ퟭ\<lsq>ퟮ" using Int_ZF_2_L16B by simp moreover from A1 show "ퟮ \<lsq> a\<ra>ퟭ" using Int_ZF_1_L8A int_ord_transl_inv by simp ultimately show "ퟭ \<lsq> a\<ra>ퟭ" by ( rule Int_order_transitive ) with I show "ퟬ \<lsq> a\<ra>ퟭ" by ( rule Int_order_transitive ) from A1 show "a≠ퟬ" using Int_ZF_2_L16A Int_ZF_2_L3 int_zero_not_one by auto qed text ‹Absolute value is the same for an integer and its opposite.› lemma ( in int0 ) Int_ZF_2_L17 : assumes "m∈ℤ" shows "abs(\<rm>m) = abs(m)" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L7A by simp text ‹The absolute value of zero is zero.› lemma ( in int0 ) Int_ZF_2_L18 : shows "abs(ퟬ) = ퟬ" using Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L2A by simp text ‹A different version of the triangle inequality.› lemma ( in int0 ) Int_triangle_ineq1 : assumes A1 : "m∈ℤ" "n∈ℤ" shows "abs(m\<rs>n) \<lsq> abs(n)\<ra>abs(m)" "abs(m\<rs>n) \<lsq> abs(m)\<ra>abs(n)" proof - have "$-n ∈ ℤ" by simp with A1 have "abs(m\<rs>n) \<lsq> abs(m)\<ra>abs(\<rm>n)" using Int_ZF_1_L9A Int_triangle_ineq by simp with A1 show "abs(m\<rs>n) \<lsq> abs(n)\<ra>abs(m)" "abs(m\<rs>n) \<lsq> abs(m)\<ra>abs(n)" using Int_ZF_2_L17 Int_ZF_2_L14 Int_ZF_1_T2 IsCommutative_def by auto qed text ‹Another version of the triangle inequality.› lemma ( in int0 ) Int_triangle_ineq2 : assumes "m∈ℤ" "n∈ℤ" and "abs(m\<rs>n) \<lsq> k" shows "abs(m) \<lsq> abs(n)\<ra>k" "m\<rs>k \<lsq> n" "m \<lsq> n\<ra>k" "n\<rs>k \<lsq> m" using assms Int_ZF_1_T2 Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L7D group3.OrderedGroup_ZF_3_L7E by auto text ‹Triangle inequality with three integers. We could use ‹OrdGroup_triangle_ineq3›, but since simp cannot translate the notation directly, it is simpler to reprove it for integers.› lemma ( in int0 ) Int_triangle_ineq3 : assumes A1 : "m∈ℤ" "n∈ℤ" "k∈ℤ" shows "abs(m\<ra>n\<ra>k) \<lsq> abs(m)\<ra>abs(n)\<ra>abs(k)" proof - from A1 have T : "m\<ra>n ∈ ℤ" "abs(k) ∈ ℤ" using Int_ZF_1_T2 group0.group_op_closed Int_ZF_2_L14 by auto with A1 have "abs(m\<ra>n\<ra>k) \<lsq> abs(m\<ra>n) \<ra> abs(k)" using Int_triangle_ineq by simp moreover from A1 T have "abs(m\<ra>n) \<ra> abs(k) \<lsq> abs(m) \<ra> abs(n) \<ra> abs(k)" using Int_triangle_ineq int_ord_transl_inv by simp ultimately show ?thesis by ( rule Int_order_transitive ) qed text ‹The next lemma shows what happens when one integers is not greater or equal than another.› (* trying to use OrderedGroup_ZF_1_L8 results in a longer proof, simp and auto loop here*) lemma ( in int0 ) Int_ZF_2_L19 : assumes A1 : "m∈ℤ" "n∈ℤ" and A2 : "¬(n\<lsq>m)" shows "m\<lsq>n" "(\<rm>n) \<lsq> (\<rm>m)" "m≠n" proof - from A1 A2 show "m\<lsq>n" using Int_ZF_2_T1 IsTotal_def by auto then show "(\<rm>n) \<lsq> (\<rm>m)" using Int_ZF_2_L10 by simp from A1 have "n \<lsq> n" using int_ord_is_refl refl_def by simp with A2 show "m≠n" by auto qed text ‹If one integer is greater or equal and not equal to another, then it is not smaller or equal.› lemma ( in int0 ) Int_ZF_2_L19AA : assumes A1 : "m\<lsq>n" and A2 : "m≠n" shows "¬(n\<lsq>m)" proof - from A1 A2 have "group3(ℤ, IntegerAddition, IntegerOrder)" "⟨m,n⟩ ∈ IntegerOrder" "m≠n" using Int_ZF_2_T1 by auto then have "⟨n,m⟩ ∉ IntegerOrder" by ( rule group3.OrderedGroup_ZF_1_L8AA ) thus "¬(n\<lsq>m)" by simp qed text ‹The next lemma allows to prove theorems for the case of positive and negative integers separately.› lemma ( in int0 ) Int_ZF_2_L19A : assumes A1 : "m∈ℤ" and A2 : "¬(ퟬ\<lsq>m)" shows "m\<lsq>ퟬ" "ퟬ \<lsq> (\<rm>m)" "m≠ퟬ" proof - from A1 have T : "ퟬ ∈ ℤ" using Int_ZF_1_T2 group0.group0_2_L2 by auto with A1 A2 show "m\<lsq>ퟬ" using Int_ZF_2_L19 by blast from A1 T A2 show "m≠ퟬ" by ( rule Int_ZF_2_L19 ) from A1 T A2 have "(\<rm>ퟬ)\<lsq>(\<rm>m)" by ( rule Int_ZF_2_L19 ) then show "ퟬ \<lsq> (\<rm>m)" using Int_ZF_1_T2 group0.group_inv_of_one by simp qed text ‹We can prove a theorem about integers by proving that it holds for $m=0$, $m\in$‹ℤ ⇩ + › and $-m\in$‹ℤ ⇩ + ›.› lemma ( in int0 ) Int_ZF_2_L19B : assumes "m∈ℤ" and "Q(ퟬ)" and "∀n∈ℤ ⇩ + . Q(n)" and "∀n∈ℤ ⇩ + . Q(\<rm>n)" shows "Q(m)" proof - let ?G = "ℤ" let ?P = "IntegerAddition" let ?r = "IntegerOrder" let ?b = "m" from assms have "group3(?G, ?P, ?r)" "?r {is total on} ?G" "?b ∈ ?G" "Q(TheNeutralElement(?G, ?P))" "∀a∈PositiveSet(?G, ?P, ?r). Q(a)" "∀a∈PositiveSet(?G, ?P, ?r). Q(GroupInv(?G, ?P)`(a))" using Int_ZF_2_T1 by auto then show "Q(?b)" by ( rule group3.OrderedGroup_ZF_1_L18 ) qed text ‹An integer is not greater than its absolute value.› lemma ( in int0 ) Int_ZF_2_L19C : assumes A1 : "m∈ℤ" shows "m \<lsq> abs(m)" "(\<rm>m) \<lsq> abs(m)" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L5 group3.OrderedGroup_ZF_3_L6 by auto text ‹$|m-n| = |n-m|$.› lemma ( in int0 ) Int_ZF_2_L20 : assumes "m∈ℤ" "n∈ℤ" shows "abs(m\<rs>n) = abs(n\<rs>m)" using assms Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L7B by simp text ‹We can add the sides of inequalities with absolute values.› lemma ( in int0 ) Int_ZF_2_L21 : assumes A1 : "m∈ℤ" "n∈ℤ" and A2 : "abs(m) \<lsq> k" "abs(n) \<lsq> l" shows "abs(m\<ra>n) \<lsq> k \<ra> l" "abs(m\<rs>n) \<lsq> k \<ra> l" using assms Int_ZF_1_T2 Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L7C group3.OrderedGroup_ZF_3_L7CA by auto text ‹Absolute value is nonnegative.› lemma ( in int0 ) int_abs_nonneg : assumes A1 : "m∈ℤ" shows "abs(m) ∈ ℤ ⇧ + " "ퟬ \<lsq> abs(m)" proof - have "AbsoluteValue(ℤ,IntegerAddition,IntegerOrder) : ℤ→ℤ ⇧ + " using Int_ZF_2_T1 group3.OrderedGroup_ZF_3_L3C by simp with A1 show "abs(m) ∈ ℤ ⇧ + " using apply_funtype by simp then show "ퟬ \<lsq> abs(m)" using Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L2 by simp qed text ‹If an nonnegative integer is less or equal than another, then so is its absolute value.› lemma ( in int0 ) Int_ZF_2_L23 : assumes "ퟬ\<lsq>m" "m\<lsq>k" shows "abs(m) \<lsq> k" using assms Int_ZF_2_L16 by simp (* this is probably not worth the effort*) subsection ‹Induction on integers.› text ‹In this section we show some induction lemmas for integers. The basic tools are the induction on natural numbers and the fact that integers can be written as a sum of a smaller integer and a natural number. › text ‹An integer can be written a a sum of a smaller integer and a natural number.› lemma ( in int0 ) Int_ZF_3_L2 : assumes A1 : "i \<lsq> m" shows "∃n∈nat. m = i $+ $# n" proof - let ?n = "0" { assume A2 : "i=m" from A1 A2 have "?n ∈ nat" "m = i $+ $# ?n" using Int_ZF_2_L1A zadd_int0_right by auto hence "∃n∈nat. m = i $+ $# n" by blast } moreover { assume A3 : "i≠m" with A1 have "i $< m" "i∈ℤ" "m∈ℤ" using Int_ZF_2_L9 Int_ZF_2_L1A by auto then obtain k where D1 : "k∈nat" "m = i $+ $# succ(k)" using zless_imp_succ_zadd_lemma by auto let ?n = "succ(k)" from D1 have "?n∈nat" "m = i $+ $# ?n" by auto hence "∃n∈nat. m = i $+ $# n" by simp } ultimately show ?thesis by blast qed text ‹Induction for integers, the induction step.› lemma ( in int0 ) Int_ZF_3_L6 : assumes A1 : "i∈ℤ" and A2 : "∀m. i\<lsq>m ∧ Q(m) ⟶ Q(m $+ ($# 1))" shows "∀k∈nat. Q(i $+ ($# k)) ⟶ Q(i $+ ($# succ(k)))" proof fix k assume A3 : "k∈nat" show "Q(i $+ $# k) ⟶ Q(i $+ $# succ(k))" proof assume A4 : "Q(i $+ $# k)" from A1 A3 have "i\<lsq> i $+ ($# k)" using Int_ZF_2_L12 by simp with A4 A2 have "Q(i $+ ($# k) $+ ($# 1))" by simp then show "Q(i $+ ($# succ(k)))" using Int_ZF_2_L11 by simp qed qed text ‹Induction on integers, version with higher-order increment function.› lemma ( in int0 ) Int_ZF_3_L7 : assumes A1 : "i\<lsq>k" and A2 : "Q(i)" and A3 : "∀m. i\<lsq>m ∧ Q(m) ⟶ Q(m $+ ($# 1))" shows "Q(k)" proof - from A1 obtain n where D1 : "n∈nat" and D2 : "k = i $+ $# n" using Int_ZF_3_L2 by auto from A1 have T1 : "i∈ℤ" using Int_ZF_2_L1A by simp note ‹n∈nat› moreover from A1 A2 have "Q(i $+ $#0)" using Int_ZF_2_L1A zadd_int0 by simp moreover from T1 A3 have "∀k∈nat. Q(i $+ ($# k)) ⟶ Q(i $+ ($# succ(k)))" by ( rule Int_ZF_3_L6 ) ultimately have "Q(i $+ ($# n))" by ( rule ind_on_nat ) with D2 show "Q(k)" by simp qed text ‹Induction on integer, implication between two forms of the induction step.› lemma ( in int0 ) Int_ZF_3_L7A : assumes A1 : "∀m. i\<lsq>m ∧ Q(m) ⟶ Q(m\<ra>ퟭ)" shows "∀m. i\<lsq>m ∧ Q(m) ⟶ Q(m $+ ($# 1))" proof - { fix m assume "i\<lsq>m ∧ Q(m)" with A1 have T1 : "m∈ℤ" "Q(m\<ra>ퟭ)" using Int_ZF_2_L1A by auto then have "m\<ra>ퟭ = m\<ra>($# 1)" using Int_ZF_1_L8 by simp with T1 have "Q(m $+ ($# 1))" using Int_ZF_1_L2 by simp } then show ?thesis by simp qed text ‹Induction on integers, version with ZF increment function.› theorem ( in int0 ) Induction_on_int : assumes A1 : "i\<lsq>k" and A2 : "Q(i)" and A3 : "∀m. i\<lsq>m ∧ Q(m) ⟶ Q(m\<ra>ퟭ)" shows "Q(k)" proof - from A3 have "∀m. i\<lsq>m ∧ Q(m) ⟶ Q(m $+ ($# 1))" by ( rule Int_ZF_3_L7A ) with A1 A2 show ?thesis by ( rule Int_ZF_3_L7 ) qed text ‹Another form of induction on integers. This rewrites the basic theorem ‹Int_ZF_3_L7› substituting $P(-k)$ for $Q(k)$.› lemma ( in int0 ) Int_ZF_3_L7B : assumes A1 : "i\<lsq>k" and A2 : "P($-i)" and A3 : "∀m. i\<lsq>m ∧ P($-m) ⟶ P($-(m $+ ($# 1)))" shows "P($-k)" proof - from A1 A2 A3 show "P($-k)" by ( rule Int_ZF_3_L7 ) qed text ‹Another induction on integers. This rewrites Int\_ZF\_3\_L7 substituting $-k$ for $k$ and $-i$ for $i$.› lemma ( in int0 ) Int_ZF_3_L8 : assumes A1 : "k\<lsq>i" and A2 : "P(i)" and A3 : "∀m. $-i\<lsq>m ∧ P($-m) ⟶ P($-(m $+ ($# 1)))" shows "P(k)" proof - from A1 have T1 : "$-i\<lsq>$-k" using Int_ZF_2_L10 by simp from A1 A2 have T2 : "P($- $- i)" using Int_ZF_2_L1A zminus_zminus by simp from T1 T2 A3 have "P($-($-k))" by ( rule Int_ZF_3_L7 ) with A1 show "P(k)" using Int_ZF_2_L1A zminus_zminus by simp qed text ‹An implication between two forms of induction steps.› lemma ( in int0 ) Int_ZF_3_L9 : assumes A1 : "i∈ℤ" and A2 : "∀n. n\<lsq>i ∧ P(n) ⟶ P(n $+ $-($#1))" shows "∀m. $-i\<lsq>m ∧ P($-m) ⟶ P($-(m $+ ($# 1)))" proof fix m show "$-i\<lsq>m ∧ P($-m) ⟶ P($-(m $+ ($# 1)))" proof assume A3 : "$- i \<lsq> m ∧ P($- m)" then have "$- i \<lsq> m" by simp then have "$-m \<lsq> $- ($- i)" by ( rule Int_ZF_2_L10 ) with A1 A2 A3 show "P($-(m $+ ($# 1)))" using zminus_zminus zminus_zadd_distrib by simp qed qed text ‹Backwards induction on integers, version with higher-order decrement function.› lemma ( in int0 ) Int_ZF_3_L9A : assumes A1 : "k\<lsq>i" and A2 : "P(i)" and A3 : "∀n. n\<lsq>i ∧ P(n) ⟶P(n $+ $-($#1)) " shows "P(k)" proof - from A1 have T1 : "i∈ℤ" using Int_ZF_2_L1A by simp from T1 A3 have T2 : "∀m. $-i\<lsq>m ∧ P($-m) ⟶ P($-(m $+ ($# 1)))" by ( rule Int_ZF_3_L9 ) from A1 A2 T2 show "P(k)" by ( rule Int_ZF_3_L8 ) qed text ‹Induction on integers, implication between two forms of the induction step.› lemma ( in int0 ) Int_ZF_3_L10 : assumes A1 : "∀n. n\<lsq>i ∧ P(n) ⟶ P(n\<rs>ퟭ)" shows "∀n. n\<lsq>i ∧ P(n) ⟶ P(n $+ $-($#1))" proof - { fix n assume "n\<lsq>i ∧ P(n)" with A1 have T1 : "n∈ℤ" "P(n\<rs>ퟭ)" using Int_ZF_2_L1A by auto then have "n\<rs>ퟭ = n\<rs>($# 1)" using Int_ZF_1_L8 by simp with T1 have "P(n $+ $-($#1))" using Int_ZF_1_L10 by simp } then show ?thesis by simp qed text ‹Backwards induction on integers.› theorem ( in int0 ) Back_induct_on_int : assumes A1 : "k\<lsq>i" and A2 : "P(i)" and A3 : "∀n. n\<lsq>i ∧ P(n) ⟶ P(n\<rs>ퟭ)" shows "P(k)" proof - from A3 have "∀n. n\<lsq>i ∧ P(n) ⟶ P(n $+ $-($#1))" by ( rule Int_ZF_3_L10 ) with A1 A2 show "P(k)" by ( rule Int_ZF_3_L9A ) qed subsection ‹Bounded vs. finite subsets of integers› text ‹The goal of this section is to establish that a subset of integers is bounded is and only is it is finite. The fact that all finite sets are bounded is already shown for all linearly ordered groups in ‹OrderedGroups_ZF.thy›. To show the other implication we show that all intervals starting at 0 are finite and then use a result from ‹OrderedGroups_ZF.thy›.› text ‹There are no integers between $k$ and $k+1$.› lemma ( in int0 ) Int_ZF_4_L1 : assumes A1 : "k∈ℤ" "m∈ℤ" "n∈nat" and A2 : "k $+ $#1 = m $+ $#n" shows "m = k $+ $#1 ∨ m \<lsq> k" proof - { assume "n=0" with A1 A2 have "m = k $+ $#1 ∨ m \<lsq> k" using zadd_int0 by simp } moreover { assume "n≠0" with A1 obtain j where D1 : "j∈nat" "n = succ(j)" using Nat_ZF_1_L3 by auto with A1 A2 D1 have "m = k $+ $#1 ∨ m \<lsq> k" using Int_ZF_2_L13 by simp } ultimately show ?thesis by blast qed text ‹A trivial calculation lemma that allows to subtract and add one.› lemma Int_ZF_4_L1A : assumes "m∈int" shows "m $- $#1 $+ $#1 = m" using assms eq_zdiff_iff by auto text ‹There are no integers between $k$ and $k+1$, another formulation.› lemma ( in int0 ) Int_ZF_4_L1B : assumes A1 : "m \<lsq> L" shows "m = L ∨ m\<ra>ퟭ \<lsq> L" "m = L ∨ m \<lsq> L\<rs>ퟭ" proof - let ?k = "L $- $#1" from A1 have T1 : "m∈ℤ" "L∈ℤ" "L = ?k $+ $#1" using Int_ZF_2_L1A Int_ZF_4_L1A by auto moreover from A1 obtain n where D1 : "n∈nat" "L = m $+ $# n" using Int_ZF_3_L2 by auto ultimately have "m = L ∨ m \<lsq> ?k" using Int_ZF_4_L1 by simp with T1 show "m = L ∨ m\<ra>ퟭ \<lsq> L" using Int_ZF_2_L9A by auto with T1 show "m = L ∨ m \<lsq> L\<rs>ퟭ" using Int_ZF_1_L8A Int_ZF_2_L9B by simp qed text ‹If $j\in m..k+1$, then $j\in m..n$ or $j=k+1$.› lemma ( in int0 ) Int_ZF_4_L2 : assumes A1 : "k∈ℤ" and A2 : "j ∈ m..(k $+ $#1)" shows "j ∈ m..k ∨ j ∈ {k $+ $#1}" proof - from A2 have T1 : "m\<lsq>j" "j\<lsq>(k $+ $#1)" using Order_ZF_2_L1A by auto then have T2 : "m∈ℤ" "j∈ℤ" using Int_ZF_2_L1A by auto from T1 obtain n where "n∈nat" "k $+ $#1 = j $+ $# n" using Int_ZF_3_L2 by auto with A1 T1 T2 have "(m\<lsq>j ∧ j \<lsq> k) ∨ j ∈ {k $+ $#1}" using Int_ZF_4_L1 by auto then show ?thesis using Order_ZF_2_L1B by auto qed text ‹Extending an integer interval by one is the same as adding the new endpoint.› lemma ( in int0 ) Int_ZF_4_L3 : assumes A1 : "m\<lsq> k" shows "m..(k $+ $#1) = m..k ∪ {k $+ $#1}" proof from A1 have T1 : "m∈ℤ" "k∈ℤ" using Int_ZF_2_L1A by auto then show "m .. (k $+ $# 1) ⊆ m .. k ∪ {k $+ $# 1}" using Int_ZF_4_L2 by auto from T1 have "m\<lsq> m" using Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L3 by simp with T1 A1 have "m .. k ⊆ m .. (k $+ $# 1)" using Int_ZF_2_L12 Int_ZF_2_L6 Order_ZF_2_L3 by simp with T1 A1 show "m..k ∪ {k $+ $#1} ⊆ m..(k $+ $#1)" using Int_ZF_2_L12A int_ord_is_refl Order_ZF_2_L2 by auto qed text ‹Integer intervals are finite - induction step.› lemma ( in int0 ) Int_ZF_4_L4 : assumes A1 : "i\<lsq>m" and A2 : "i..m ∈ Fin(ℤ)" shows "i..(m $+ $#1) ∈ Fin(ℤ)" using assms Int_ZF_4_L3 by simp text ‹Integer intervals are finite.› lemma ( in int0 ) Int_ZF_4_L5 : assumes A1 : "i∈ℤ" "k∈ℤ" shows "i..k ∈ Fin(ℤ)" proof - { assume A2 : "i\<lsq>k" moreover from A1 have "i..i ∈ Fin(ℤ)" using int_ord_is_refl Int_ZF_2_L4 Order_ZF_2_L4 by simp moreover from A2 have "∀m. i\<lsq>m ∧ i..m ∈ Fin(ℤ) ⟶ i..(m $+ $#1) ∈ Fin(ℤ)" using Int_ZF_4_L4 by simp ultimately have "i..k ∈ Fin(ℤ)" by ( rule Int_ZF_3_L7 ) } moreover { assume "¬ i \<lsq> k" then have "i..k ∈ Fin(ℤ)" using Int_ZF_2_L6 Order_ZF_2_L5 by simp } ultimately show ?thesis by blast qed text ‹Bounded integer sets are finite.› lemma ( in int0 ) Int_ZF_4_L6 : assumes A1 : "IsBounded(A,IntegerOrder)" shows "A ∈ Fin(ℤ)" proof - have T1 : "∀m ∈ Nonnegative(ℤ,IntegerAddition,IntegerOrder). $#0..m ∈ Fin(ℤ)" proof fix m assume "m ∈ Nonnegative(ℤ,IntegerAddition,IntegerOrder)" then have "m∈ℤ" using Int_ZF_2_T1 group3.OrderedGroup_ZF_1_L4E by auto then show "$#0..m ∈ Fin(ℤ)" using Int_ZF_4_L5 by simp qed have "group3(ℤ,IntegerAddition,IntegerOrder)" using Int_ZF_2_T1 by simp moreover from T1 have "∀m ∈ Nonnegative(ℤ,IntegerAddition,IntegerOrder). Interval(IntegerOrder,TheNeutralElement(ℤ,IntegerAddition),m) ∈ Fin(ℤ)" using Int_ZF_1_L8 by simp moreover note A1 ultimately show "A ∈ Fin(ℤ)" by ( rule group3.OrderedGroup_ZF_2_T1 ) qed text ‹A subset of integers is bounded iff it is finite.› theorem ( in int0 ) Int_bounded_iff_fin : shows "IsBounded(A,IntegerOrder)⟷ A∈Fin(ℤ)" using Int_ZF_4_L6 Int_ZF_2_T1 group3.ord_group_fin_bounded by blast text ‹The image of an interval by any integer function is finite, hence bounded.› lemma ( in int0 ) Int_ZF_4_L8 : assumes A1 : "i∈ℤ" "k∈ℤ" and A2 : "f:ℤ→ℤ" shows "f``(i..k) ∈ Fin(ℤ)" "IsBounded(f``(i..k),IntegerOrder)" using assms Int_ZF_4_L5 Finite1_L6A Int_bounded_iff_fin by auto text ‹If for every integer we can find one in $A$ that is greater or equal, then $A$ is is not bounded above, hence infinite.› lemma ( in int0 ) Int_ZF_4_L9 : assumes A1 : "∀m∈ℤ. ∃k∈A. m\<lsq>k" shows "¬IsBoundedAbove(A,IntegerOrder)" "A ∉ Fin(ℤ)" proof - have "ℤ ≠ {ퟬ}" using Int_ZF_1_L8A int_zero_not_one by blast with A1 show "¬IsBoundedAbove(A,IntegerOrder)" "A ∉ Fin(ℤ)" using Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L2A by auto qed end ...; http://www.gnu.org/savannah-checkouts/non-gnu/isarmathlib/IsarMathLib/Int_ZF_IML.html - [detail] - [similar]

PREV NEXT