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\)".
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.
The next theorem is a version of induction on natural numbers that I was thought in school.
theorem ind_on_nat:
assumes A1: \( n\in nat \) and A2: \( P(0) \) and A3: \( \forall k\in nat.\ P(k)\longrightarrow P(succ(k)) \)
shows \( P(n) \)proofA nonzero natural number has a predecessor.
lemma Nat_ZF_1_L3:
assumes A1: \( n \in nat \) and A2: \( n\neq 0 \)
shows \( \exists k\in nat.\ n = succ(k) \)proofWhat is succ, anyway?
lemma succ_explained:
shows \( succ(n) = n \cup \{n\} \) using succ_iffEmpty set is an element of every natural number which is not zero.
lemma empty_in_every_succ:
assumes A1: \( n \in nat \)
shows \( 0 \in succ(n) \)proofIf one natural number is less than another then their successors are in the same relation.
lemma succ_ineq:
assumes A1: \( n \in nat \)
shows \( \forall i \in n.\ succ(i) \in succ(n) \)proofFor natural numbers if \(k\subseteq n\) the similar holds for their successors.
lemma succ_subset:
assumes A1: \( k \in nat \), \( n \in nat \) and A2: \( k\subseteq n \)
shows \( succ(k) \subseteq succ(n) \)proofFor any two natural numbers one of them is contained in the other.
lemma nat_incl_total:
assumes A1: \( i \in nat \), \( j \in nat \)
shows \( i \subseteq j \vee j \subseteq i \)proofThe set of natural numbers is the union of all successors of natural numbers.
lemma nat_union_succ:
shows \( nat = (\bigcup n \in nat.\ succ(n)) \)proofSuccessors of natural numbers are subsets of the set of natural numbers.
lemma succnat_subset_nat:
assumes A1: \( n \in nat \)
shows \( succ(n) \subseteq nat \)proofElement of a natural number is a natural number.
lemma elem_nat_is_nat:
assumes A1: \( n \in nat \) and A2: \( k\in n \)
shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \)proofThe set of natural numbers is the union of its elements.
lemma nat_union_nat:
shows \( nat = \bigcup nat \) using elem_nat_is_natA natural number is a subset of the set of natural numbers.
lemma nat_subset_nat:
assumes A1: \( n \in nat \)
shows \( n \subseteq nat \)proofAdding natural numbers does not decrease what we add to.
lemma add_nat_le:
assumes A1: \( n \in nat \) and A2: \( k \in nat \)
shows \( n \leq n \ \sharp + k \), \( n \subseteq n \ \sharp + k \), \( n \subseteq k \ \sharp + n \)proofResult of adding an element of \(k\) is smaller than of adding \(k\).
lemma add_lt_mono:
assumes \( k \in nat \) and \( j\in k \)
shows \( (n \ \sharp + j) \lt (n \ \sharp + k) \), \( (n \ \sharp + j) \in (n \ \sharp + k) \)proofA 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 \in nat \) and A2: \( m \in nat \)
shows \( \forall i \in m \ \sharp + n.\ i \in m \vee (\exists j \in n.\ i = m \ \sharp + j) \)proofA variant of induction useful for finite sequences.
lemma fin_nat_ind:
assumes A1: \( n \in nat \) and A2: \( k \in succ(n) \) and A3: \( P(0) \) and A4: \( \forall j\in n.\ P(j) \longrightarrow P(succ(j)) \)
shows \( P(k) \)proofSome properties of positive natural numbers.
lemma succ_plus:
assumes \( n \in nat \), \( k \in nat \)
shows \( succ(n \ \sharp + j) \in nat \), \( succ(n) \ \sharp + succ(j) = succ(succ(n \ \sharp + j)) \) using assmsIn this section we consider intervals of natural numbers i.e. sets of the form \(\{n+j : j \in 0..k-1\}\).
The interval is determined by two parameters: starting point and length. Recall that in standard Isabelle's Arith.thy the symbol \( \ \sharp + \) is defined as the sum of natural numbers.
Definition
\( Nat \text{Interval}(n,k) \equiv \{n \ \sharp + j.\ j\in k\} \)
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 \in nat \) and A2: \( i \in Nat \text{Interval}(n,k) \)
shows \( i \ \sharp - n \in k \)proofIntervals 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 \in nat \), \( k \in nat \)
shows \( n \cap Nat \text{Interval}(n,k) = 0 \), \( n \cup Nat \text{Interval}(n,k) = n \ \sharp + k \)proofSme properties of three adjacent intervals.
lemma adjacent_intervals3:
assumes \( n \in nat \), \( k \in nat \), \( m \in nat \)
shows \( n \ \sharp + k \ \sharp + m = (n \ \sharp + k) \cup Nat \text{Interval}(n \ \sharp + k,m) \), \( n \ \sharp + k \ \sharp + m = n \cup Nat \text{Interval}(n,k \ \sharp + m) \), \( n \ \sharp + k \ \sharp + m = n \cup Nat \text{Interval}(n,k) \cup Nat \text{Interval}(n \ \sharp + k,m) \) using assms , add_assoc , length_start_decompassumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(succ(k)) \)
shows \( P(n) \)assumes \( n \in nat \) and \( k\in n \)
shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \)assumes \( n \in nat \) and \( k \in nat \)
shows \( n \leq n \ \sharp + k \), \( n \subseteq n \ \sharp + k \), \( n \subseteq k \ \sharp + n \)assumes \( n \in nat \) and \( m \in nat \)
shows \( \forall i \in m \ \sharp + n.\ i \in m \vee (\exists j \in n.\ i = m \ \sharp + j) \)assumes \( n \in nat \), \( k \in nat \)
shows \( n \cap Nat \text{Interval}(n,k) = 0 \), \( n \cup Nat \text{Interval}(n,k) = n \ \sharp + k \)