(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2005 - 2023 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 ‹Natural numbers in IsarMathLib› theory Nat_ZF_IML imports ZF.ArithSimp begin text‹The ZF set theory constructs natural numbers from the empty set and the notion of a one-element set. Namely, zero of natural numbers is defined as the empty set. For each natural number $n$ the next natural number is defined as $n\cup \{n\}$. With this definition for every non-zero natural number we get the identity $n = \{0,1,2,..,n-1\}$. It is good to remember that when we see an expression like $f: n \rightarrow X$. Also, with this definition the relation "less or equal than" becomes "$\subseteq$" and the relation "less than" becomes "$\in$". › subsection‹Induction› text‹The induction lemmas in the standard Isabelle's Nat.thy file like for example ‹nat_induct› require the induction step to be a higher order statement (the one that uses the $\Longrightarrow$ sign). I found it difficult to apply from Isar, which is perhaps more of an indication of my Isar skills than anything else. Anyway, here we provide a first order version that is easier to reference in Isar declarative style proofs.› text‹The next theorem is a version of induction on natural numbers that I was thought in school.› theorem ind_on_nat: assumes A1: "n∈nat" and A2: "P(0)" and A3: "∀k∈nat. P(k)⟶P(succ(k))" shows "P(n)" proof - note A1 A2 moreover { fix x assume "x∈nat" "P(x)" with A3 have "P(succ(x))" by simp } ultimately show "P(n)" by (rule nat_induct) qed text‹A nonzero natural number has a predecessor.› lemma Nat_ZF_1_L3: assumes A1: "n ∈ nat" and A2: "n≠0" shows "∃k∈nat. n = succ(k)" proof - from A1 have "n ∈ {0} ∪ {succ(k). k∈nat}" using nat_unfold by simp with A2 show ?thesis by simp qed text‹What is ‹succ›, anyway? It's a union with the singleton of the set.› lemma succ_explained: shows "succ(n) = n ∪ {n}" using succ_iff by auto text‹The singleton containing the empty set is a natural number.› lemma one_is_nat: shows "{0} ∈ nat" "{0} = succ(0)" "{0} = 1" proof - show "{0} = succ(0)" using succ_explained by simp then show "{0} ∈ nat" by simp show "{0}=1" by blast qed text‹If $k$ is a member of $succ(n)$ but is not $n$, then it must be the member of $n$.› lemma mem_succ_not_eq: assumes "k∈succ(n)" "k≠n" shows "k∈n" using assms succ_explained by simp text‹Empty set is an element of every natural number which is not zero.› lemma empty_in_every_succ: assumes A1: "n ∈ nat" shows "0 ∈ succ(n)" proof - note A1 moreover have "0 ∈ succ(0)" by simp moreover { fix k assume "k ∈ nat" and A2: "0 ∈ succ(k)" then have "succ(k) ⊆ succ(succ(k))" by auto with A2 have "0 ∈ succ(succ(k))" by auto } then have "∀k ∈ nat. 0 ∈ succ(k) ⟶ 0 ∈ succ(succ(k))" by simp ultimately show "0 ∈ succ(n)" by (rule ind_on_nat) qed text‹Various forms of saying that for natural numbers taking the successor is the same as adding one. › lemma succ_add_one: assumes "n∈nat" shows "n #+ 1 = succ(n)" "n #+ 1 ∈ nat" "{0} #+ n = succ(n)" "n #+ {0} = succ(n)" "succ(n) ∈ nat" "0 ∈ n #+ 1" "n ⊆ n #+ 1" proof - from assms show "n #+ 1 = succ(n)" "n #+ 1 ∈ nat" "succ(n) ∈ nat" by simp_all moreover from assms have "{0} = 1" and "n #+ 1 = 1 #+ n" by auto ultimately show "{0} #+ n = succ(n)" and "n #+ {0} = succ(n)" by simp_all from assms ‹n #+ 1 = succ(n)› show "0 ∈ n #+ 1" using empty_in_every_succ by simp from assms ‹n #+ 1 = succ(n)› show "n ⊆ n #+ 1" using succ_explained by auto qed text‹A more direct way of stating that empty set is an element of every non-zero natural number:› lemma empty_in_non_empty: assumes "n∈nat" "n≠0" shows "0∈n" using assms Nat_ZF_1_L3 empty_in_every_succ by auto text‹If one natural number is less than another then their successors are in the same relation.› lemma succ_ineq: assumes A1: "n ∈ nat" shows "∀i ∈ n. succ(i) ∈ succ(n)" proof - note A1 moreover have "∀k ∈ 0. succ(k) ∈ succ(0)" by simp moreover { fix k assume A2: "∀i∈k. succ(i) ∈ succ(k)" { fix i assume "i ∈ succ(k)" then have "i ∈ k ∨ i = k" by auto moreover { assume "i∈k" with A2 have "succ(i) ∈ succ(k)" by simp hence "succ(i) ∈ succ(succ(k))" by auto } moreover { assume "i = k" then have "succ(i) ∈ succ(succ(k))" by auto } ultimately have "succ(i) ∈ succ(succ(k))" by auto } then have "∀i ∈ succ(k). succ(i) ∈ succ(succ(k))" by simp } then have "∀k ∈ nat. ( (∀i∈k. succ(i) ∈ succ(k)) ⟶ (∀i ∈ succ(k). succ(i) ∈ succ(succ(k))) )" by simp ultimately show "∀i ∈ n. succ(i) ∈ succ(n)" by (rule ind_on_nat) qed text‹For natural numbers if $k\subseteq n$ the similar holds for their successors.› lemma succ_subset: assumes A1: "k ∈ nat" "n ∈ nat" and A2: "k⊆n" shows "succ(k) ⊆ succ(n)" proof - from A1 have T: "Ord(k)" and "Ord(n)" using nat_into_Ord by auto with A2 have "succ(k) ≤ succ(n)" using subset_imp_le by simp then show "succ(k) ⊆ succ(n)" using le_imp_subset by simp qed text‹For any two natural numbers one of them is contained in the other.› lemma nat_incl_total: assumes A1: "i ∈ nat" "j ∈ nat" shows "i ⊆ j ∨ j ⊆ i" proof - from A1 have T: "Ord(i)" "Ord(j)" using nat_into_Ord by auto then have "i∈j ∨ i=j ∨ j∈i" using Ord_linear by simp moreover { assume "i∈j" with T have "i⊆j ∨ j⊆i" using lt_def leI le_imp_subset by simp } moreover { assume "i=j" then have "i⊆j ∨ j⊆i" by simp } moreover { assume "j∈i" with T have "i⊆j ∨ j⊆i" using lt_def leI le_imp_subset by simp } ultimately show "i ⊆ j ∨ j ⊆ i" by auto qed text‹The set of natural numbers is the union of all successors of natural numbers.› lemma nat_union_succ: shows "nat = (⋃n ∈ nat. succ(n))" proof show "nat ⊆ (⋃n ∈ nat. succ(n))" by auto next { fix k assume A2: "k ∈ (⋃n ∈ nat. succ(n))" then obtain n where T: "n ∈ nat" and I: "k ∈ succ(n)" by auto then have "k ≤ n" using nat_into_Ord lt_def by simp with T have "k ∈ nat" using le_in_nat by simp } then show "(⋃n ∈ nat. succ(n)) ⊆ nat" by auto qed text‹Successors of natural numbers are subsets of the set of natural numbers.› lemma succnat_subset_nat: assumes A1: "n ∈ nat" shows "succ(n) ⊆ nat" proof - from A1 have "succ(n) ⊆ (⋃n ∈ nat. succ(n))" by auto then show "succ(n) ⊆ nat" using nat_union_succ by simp qed text‹Element $k$ of a natural number $n$ is a natural number that is smaller than $n$.› lemma elem_nat_is_nat: assumes A1: "n ∈ nat" and A2: "k∈n" shows "k < n" "k ∈ nat" "k ≤ n" "⟨k,n⟩ ∈ Le" proof - from A1 A2 show "k < n" using nat_into_Ord lt_def by simp with A1 show "k ∈ nat" using lt_nat_in_nat by simp from ‹k < n› show "k ≤ n" using leI by simp with A1 ‹k ∈ nat› show "⟨k,n⟩ ∈ Le" using Le_def by simp qed text‹A version of ‹succ_ineq› without a quantifier, with additional assertion using the ‹n #+ 1› notation.› lemma succ_ineq1: assumes "n ∈ nat" "i∈n" shows "succ(i) ∈ succ(n)" "i #+ 1 ∈ n #+ 1" "i ∈ n #+ 1" using assms succ_ineq succ_add_one(1,7) elem_nat_is_nat(2) by auto text‹For natural numbers membership and inequality are the same and $k \leq n$ is the same as $k \in \textrm{succ}(n)$. The proof relies on lemmas in the standard Isabelle's ‹Nat› and ‹Ordinal› theories. › lemma nat_mem_lt: assumes "n∈nat" shows "k<n ⟷ k∈n" and "k≤n ⟷ k ∈ succ(n)" using assms nat_into_Ord Ord_mem_iff_lt by auto text‹The term $k \leq n$ is the same as $k < \textrm{succ}(n)$. › lemma leq_mem_succ: shows "k≤n ⟷ k < succ(n)" by simp text‹If the successor of a natural number $k$ is an element of the successor of $n$ then a similar relations holds for the numbers themselves.› lemma succ_mem: assumes "n ∈ nat" "succ(k) ∈ succ(n)" shows "k∈n" using assms elem_nat_is_nat(1) succ_leE nat_into_Ord unfolding lt_def by blast text‹The set of natural numbers is the union of its elements.› lemma nat_union_nat: shows "nat = ⋃ nat" using elem_nat_is_nat by blast text‹A natural number is a subset of the set of natural numbers.› lemma nat_subset_nat: assumes A1: "n ∈ nat" shows "n ⊆ nat" proof - from A1 have "n ⊆ ⋃ nat" by auto then show "n ⊆ nat" using nat_union_nat by simp qed text‹Adding natural numbers does not decrease what we add to.› lemma add_nat_le: assumes A1: "n ∈ nat" and A2: "k ∈ nat" shows "n ≤ n #+ k" "n ⊆ n #+ k" "n ⊆ k #+ n" proof - from A1 A2 have "n ≤ n" "0 ≤ k" "n ∈ nat" "k ∈ nat" using nat_le_refl nat_0_le by auto then have "n #+ 0 ≤ n #+ k" by (rule add_le_mono) with A1 show "n ≤ n #+ k" using add_0_right by simp then show "n ⊆ n #+ k" using le_imp_subset by simp then show "n ⊆ k #+ n" using add_commute by simp qed text‹Result of adding an element of $k$ is smaller than of adding $k$.› lemma add_lt_mono: assumes "k ∈ nat" and "j∈k" shows "(n #+ j) < (n #+ k)" "(n #+ j) ∈ (n #+ k)" proof - from assms have "j < k" using elem_nat_is_nat by blast moreover note ‹k ∈ nat› ultimately show "(n #+ j) < (n #+ k)" "(n #+ j) ∈ (n #+ k)" using add_lt_mono2 ltD by auto qed text‹A technical lemma about a decomposition of a sum of two natural numbers: if a number $i$ is from $m + n$ then it is either from $m$ or can be written as a sum of $m$ and a number from $n$. The proof by induction w.r.t. to $m$ seems to be a bit heavy-handed, but I could not figure out how to do this directly from results from standard Isabelle/ZF.› lemma nat_sum_decomp: assumes A1: "n ∈ nat" and A2: "m ∈ nat" shows "∀i ∈ m #+ n. i ∈ m ∨ (∃j ∈ n. i = m #+ j)" proof - note A1 moreover from A2 have "∀i ∈ m #+ 0. i ∈ m ∨ (∃j ∈ 0. i = m #+ j)" using add_0_right by simp moreover have "∀k∈nat. (∀i ∈ m #+ k. i ∈ m ∨ (∃j ∈ k. i = m #+ j)) ⟶ (∀i ∈ m #+ succ(k). i ∈ m ∨ (∃j ∈ succ(k). i = m #+ j))" proof - { fix k assume A3: "k ∈ nat" { assume A4: "∀i ∈ m #+ k. i ∈ m ∨ (∃j ∈ k. i = m #+ j)" { fix i assume "i ∈ m #+ succ(k)" then have "i ∈ m #+ k ∨ i = m #+ k" using add_succ_right by auto moreover from A4 A3 have "i ∈ m #+ k ⟶ i ∈ m ∨ (∃j ∈ succ(k). i = m #+ j)" by auto ultimately have "i ∈ m ∨ (∃j ∈ succ(k). i = m #+ j)" by auto } then have "∀i ∈ m #+ succ(k). i ∈ m ∨ (∃j ∈ succ(k). i = m #+ j)" by simp } then have "(∀i ∈ m #+ k. i ∈ m ∨ (∃j ∈ k. i = m #+ j)) ⟶ (∀i ∈ m #+ succ(k). i ∈ m ∨ (∃j ∈ succ(k). i = m #+ j))" by simp } then show ?thesis by simp qed ultimately show "∀i ∈ m #+ n. i ∈ m ∨ (∃j ∈ n. i = m #+ j)" by (rule ind_on_nat) qed text‹A variant of induction useful for finite sequences.› lemma fin_nat_ind: assumes A1: "n ∈ nat" and A2: "k ∈ succ(n)" and A3: "P(0)" and A4: "∀j∈n. P(j) ⟶ P(succ(j))" shows "P(k)" proof - from A2 have "k ∈ n ∨ k=n" by auto with A1 have "k ∈ nat" using elem_nat_is_nat by blast moreover from A3 have "0 ∈ succ(n) ⟶ P(0)" by simp moreover from A1 A4 have "∀k ∈ nat. (k ∈ succ(n) ⟶ P(k)) ⟶ (succ(k) ∈ succ(n) ⟶ P(succ(k)))" using nat_into_Ord Ord_succ_mem_iff by auto ultimately have "k ∈ succ(n) ⟶ P(k)" by (rule ind_on_nat) with A2 show "P(k)" by simp qed text‹Some properties of positive natural numbers.› lemma succ_plus: assumes "n ∈ nat" "k ∈ nat" shows "succ(n #+ j) ∈ nat" "succ(n) #+ succ(j) = succ(succ(n #+ j))" using assms by auto text‹If $k$ is in the successor of $n$, then the predecessor of $k$ is in $n$.› lemma pred_succ_mem: assumes "n∈nat" "n≠0" "k∈succ(n)" shows "pred(k)∈n" proof - from assms(1,3) have "k∈nat" using succnat_subset_nat by blast { assume "k≠0" with ‹k∈nat› obtain j where "j∈nat" and "k=succ(j)" using Nat_ZF_1_L3 by auto with assms(1,3) have "pred(k)∈n" using succ_mem pred_succ_eq by simp } moreover { assume "k=0" with assms(1,2) have "pred(k)∈n" using pred_0 empty_in_non_empty by simp } ultimately show ?thesis by blast qed text‹For non-zero natural numbers $\textrm{pred}(n) = n-1$.› lemma pred_minus_one: assumes "n∈nat" "n≠0" shows "n #- 1 = pred(n)" proof - from assms obtain k where "n=succ(k)" using Nat_ZF_1_L3 by blast with assms show ?thesis using pred_succ_eq eq_succ_imp_eq_m1 by simp qed text‹For natural numbers if $j\in n$ then $j+1 \subseteq n$.› lemma mem_add_one_subset: assumes "n ∈ nat" "k∈n" shows "k #+ 1 ⊆ n" proof - from assms have "k #+ 1 ∈ succ(n)" using elem_nat_is_nat(2) succ_ineq1 succ_add_one(1) by simp with assms(1) show "k #+ 1 ⊆ n" using nat_mem_lt(2) le_imp_subset by blast qed text‹For a natural $n$ if $k\in n+1$ then $k+1\leq n+1$.› lemma succ_ineq2: assumes "n ∈ nat" "k ∈ n #+ 1" shows "k #+ 1 ≤ n #+ 1" and "k≤n" proof - from assms show "k≤n" using succ_add_one(1) nat_mem_lt(2) by simp with assms(1) show "k #+ 1 ≤ n #+ 1" using add_le_mono1 by blast qed text‹A nonzero natural number is of the form $n=m+1$ for some natural number $m$. This is very similar to ‹Nat_ZF_1_L3› except that we use $n+1$ instead of ‹succ(n)›. › lemma nat_not0_succ: assumes "n∈nat" "n≠0" shows "∃m∈nat. n = m #+1" using assms Nat_ZF_1_L3 succ_add_one(1) by simp text‹Adding and subtracting a natural number cancel each other.› lemma add_subctract: assumes "m∈nat" shows "(m #+ n) #- n = m" using assms diff_add_inverse2 by simp text‹A version of induction on natural numbers that uses the $n+1$ notation instead of $‹succ(n)›$.› lemma ind_on_nat1: assumes "n∈nat" and "P(0)" and "∀k∈nat. P(k)⟶P(k #+ 1)" shows "P(n)" using assms succ_add_one(1) ind_on_nat by simp text‹A version of induction for finite sequences using the $n+1$ notation instead of ‹succ(n)›:› lemma fin_nat_ind1: assumes "n∈nat" and "P(0)" and "∀j∈n. P(j)⟶P(j #+ 1)" shows "∀k∈n #+ 1. P(k)" and "P(n)" proof - { fix k assume "k∈n #+ 1" with assms have "n∈nat" "k∈succ(n)" "P(0)" "∀j∈n. P(j) ⟶ P(succ(j))" using succ_add_one(1) elem_nat_is_nat(2) by simp_all then have "P(k)" by (rule fin_nat_ind) } thus "∀k∈n #+ 1. P(k)" by simp with assms(1) show "P(n)" by simp qed text‹A simplification rule for natural numbers: if $k<n$ then $n-(k+1)+1 = n-k$: › lemma nat_subtr_simpl0: assumes "n∈nat" "k∈n" shows "n #- (k #+ 1) #+ 1 = n #- k" proof - from assms obtain m where "m∈nat" and "n = m #+1" using nat_not0_succ by blast with assms have "succ(m) = m #+ 1" "succ(m #- k) = m #- k #+ 1" using elem_nat_is_nat(2) succ_add_one by simp_all moreover from assms(2) ‹m∈nat› ‹n = m #+1› have "succ(m) #- k = succ(m #- k)" using diff_succ succ_ineq2(2) by simp ultimately have "m #- k #+ 1 = m #+ 1 #- k" by simp with ‹n = m #+1› show ?thesis using diff_cancel2 by simp qed subsection‹Intervals› text‹In this section we consider intervals of natural numbers i.e. sets of the form $\{n+j : j \in 0..k-1\}$.› text‹The interval is determined by two parameters: starting point and length.› definition "NatInterval(n,k) ≡ {n #+ j. j∈k}" text‹Subtracting the beginning af the interval results in a number from the length of the interval. It may sound weird, but note that the length of such interval is a natural number, hence a set.› lemma inter_diff_in_len: assumes A1: "k ∈ nat" and A2: "i ∈ NatInterval(n,k)" shows "i #- n ∈ k" proof - from A2 obtain j where I: "i = n #+ j" and II: "j ∈ k" using NatInterval_def by auto from A1 II have "j ∈ nat" using elem_nat_is_nat by blast moreover from I have "i #- n = natify(j)" using diff_add_inverse by simp ultimately have "i #- n = j" by simp with II show ?thesis by simp qed text‹Intervals don't overlap with their starting point and the union of an interval with its starting point is the sum of the starting point and the length of the interval.› lemma length_start_decomp: assumes A1: "n ∈ nat" "k ∈ nat" shows "n ∩ NatInterval(n,k) = 0" "n ∪ NatInterval(n,k) = n #+ k" proof - { fix i assume A2: "i ∈ n" and "i ∈ NatInterval(n,k)" then obtain j where I: "i = n #+ j" and II: "j ∈ k" using NatInterval_def by auto from A1 have "k ∈ nat" using elem_nat_is_nat by blast with II have "j ∈ nat" using elem_nat_is_nat by blast with A1 I have "n ≤ i" using add_nat_le by simp moreover from A1 A2 have "i < n" using elem_nat_is_nat by blast ultimately have False using le_imp_not_lt by blast } thus "n ∩ NatInterval(n,k) = 0" by auto from A1 have "n ⊆ n #+ k" using add_nat_le by simp moreover { fix i assume "i ∈ NatInterval(n,k)" then obtain j where III: "i = n #+ j" and IV: "j ∈ k" using NatInterval_def by auto with A1 have "j < k" using elem_nat_is_nat by blast with A1 III have "i ∈ n #+ k" using add_lt_mono2 ltD by simp } ultimately have "n ∪ NatInterval(n,k) ⊆ n #+ k" by auto moreover from A1 have "n #+ k ⊆ n ∪ NatInterval(n,k)" using nat_sum_decomp NatInterval_def by auto ultimately show "n ∪ NatInterval(n,k) = n #+ k" by auto qed text‹Some properties of three adjacent intervals.› lemma adjacent_intervals3: assumes "n ∈ nat" "k ∈ nat" "m ∈ nat" shows "n #+ k #+ m = (n #+ k) ∪ NatInterval(n #+ k,m)" "n #+ k #+ m = n ∪ NatInterval(n,k #+ m)" "n #+ k #+ m = n ∪ NatInterval(n,k) ∪ NatInterval(n #+ k,m)" using assms add_assoc length_start_decomp by auto end