theory Nat_ZF_IML imports ZF.ArithSimp
begin
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\)".
Induction
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) \)proof note A1, A2
moreover {
}
ultimately show \( P(n) \) by (rule nat_induct )
qed
fix \( x \)
assume \( x\in nat \), \( P(x) \)
with A3 have \( P(succ(x)) \)
A 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) \)proof from A1 have \( n \in \{0\} \cup \{succ(k).\ k\in nat\} \) using nat_unfold
with A2 show \( thesis \)
qed
What is succ, anyway? It's a union with the singleton of the set.
lemma succ_explained:
shows \( succ(n) = n \cup \{n\} \) using succ_iffThe singleton containing the empty set is a natural number.
lemma one_is_nat:
shows \( \{0\} \in nat \), \( \{0\} = succ(0) \), \( \{0\} = 1 \)proof show \( \{0\} = succ(0) \) using succ_explained
then show \( \{0\} \in nat \)
show \( \{0\}=1 \)
qed
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\in succ(n) \), \( k\neq n \)
shows \( k\in n \) using assms, succ_explainedEmpty 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) \)proof note A1
moreover
}
qed
have \( 0 \in succ(0) \)
moreover {
fix \( k \)
assume \( k \in nat \) and A2: \( 0 \in succ(k) \)
then have \( succ(k) \subseteq succ(succ(k)) \)
with A2 have \( 0 \in succ(succ(k)) \)
then have \( \forall k \in nat.\ 0 \in succ(k) \longrightarrow 0 \in succ(succ(k)) \)
ultimately show \( 0 \in succ(n) \) by (rule ind_on_nat )
Various forms of saying that for natural numbers taking the successor is the same as adding one.
lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \)proof from assms show \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( succ(n) \in nat \)
moreover
from assms have \( \{0\} = 1 \) and \( n + 1 = 1 + n \)
ultimately show \( \{0\} + n = succ(n) \) and \( n + \{0\} = succ(n) \)
from assms, \( n + 1 = succ(n) \) show \( 0 \in n + 1 \) using empty_in_every_succ
from assms, \( n + 1 = succ(n) \) show \( n \subseteq n + 1 \) using succ_explained
qed
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\in nat \), \( n\neq 0 \)
shows \( 0\in n \) using assms, Nat_ZF_1_L3, empty_in_every_succIf 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) \)proof note A1
moreover
}
}
qed
have \( \forall k \in 0.\ succ(k) \in succ(0) \)
moreover {
fix \( k \)
assume A2: \( \forall i\in k.\ succ(i) \in succ(k) \)
{
fix \( i \)
assume \( i \in succ(k) \)
then have \( i \in k \vee i = k \)
moreover {
}
moreover {
}
ultimately have \( succ(i) \in succ(succ(k)) \)
assume \( i\in k \)
with A2 have \( succ(i) \in succ(k) \)
hence \( succ(i) \in succ(succ(k)) \)
assume \( i = k \)
then have \( succ(i) \in succ(succ(k)) \)
then have \( \forall i \in succ(k).\ succ(i) \in succ(succ(k)) \)
then have \( \forall k \in nat.\ \)
\( ( (\forall i\in k.\ succ(i) \in succ(k)) \longrightarrow (\forall i \in succ(k).\ succ(i) \in succ(succ(k))) ) \)
ultimately show \( \forall i \in n.\ succ(i) \in succ(n) \) by (rule ind_on_nat )
For 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) \)proof from A1 have T: \( Ord(k) \) and \( Ord(n) \) using nat_into_Ord
with A2 have \( succ(k) \leq succ(n) \) using subset_imp_le
then show \( succ(k) \subseteq succ(n) \) using le_imp_subset
qed
For 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 \)proof from A1 have T: \( Ord(i) \), \( Ord(j) \) using nat_into_Ord
then have \( i\in j \vee i=j \vee j\in i \) using Ord_linear
moreover {
}
moreover {
}
moreover {
}
ultimately show \( i \subseteq j \vee j \subseteq i \)
qed
assume \( i\in j \)
with T have \( i\subseteq j \vee j\subseteq i \) using lt_def, leI, le_imp_subset
assume \( i=j \)
then have \( i\subseteq j \vee j\subseteq i \)
assume \( j\in i \)
with T have \( i\subseteq j \vee j\subseteq i \) using lt_def, leI, le_imp_subset
The 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)) \)proof show \( nat \subseteq (\bigcup n \in nat.\ succ(n)) \)
next
{
fix \( k \)
assume A2: \( k \in (\bigcup n \in nat.\ succ(n)) \)
then obtain \( n \) where T: \( n \in nat \) and I: \( k \in succ(n) \)
then have \( k \leq n \) using nat_into_Ord, lt_def
with T have \( k \in nat \) using le_in_nat
then show \( (\bigcup n \in nat.\ succ(n)) \subseteq nat \)
qed
Successors 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 \)proof from A1 have \( succ(n) \subseteq (\bigcup n \in nat.\ succ(n)) \)
then show \( succ(n) \subseteq nat \) using nat_union_succ
qed
Element \(k\) of a natural number \(n\) is a natural number that is smaller than \(n\).
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 \)proof from A1, A2 show \( k \lt n \) using nat_into_Ord, lt_def
with A1 show \( k \in nat \) using lt_nat_in_nat
from \( k \lt n \) show \( k \leq n \) using leI
with A1, \( k \in nat \) show \( \langle k,n\rangle \in Le \) using Le_def
qed
A version of succ_ineq without a quantifier, with additional assertion using the \( n + 1 \) notation.
lemma succ_ineq1:
assumes \( n \in nat \), \( i\in n \)
shows \( succ(i) \in succ(n) \), \( i + 1 \in n + 1 \), \( i \in n + 1 \) using assms, succ_ineq, succ_add_one(1,7), elem_nat_is_nat(2)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\in nat \)
shows \( k \lt n \longleftrightarrow k\in n \) and \( k\leq n \longleftrightarrow k \in succ(n) \) using assms, nat_into_Ord, Ord_mem_iff_ltIf \(n\) is a natural number and \(k\leq n\), then k is a natural number.
lemma leq_nat_is_nat:
assumes \( n\in nat \), \( k\leq n \)
shows \( k\in nat \) using assms, nat_mem_lt, elem_nat_is_nat(2)The term \(k \leq n\) is the same as \(k < \textrm{succ}(n)\).
lemma leq_mem_succ:
shows \( k\leq n \longleftrightarrow k \lt succ(n) \)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 \in nat \), \( succ(k) \in succ(n) \)
shows \( k\in n \) using assms, elem_nat_is_nat(1), succ_leE, nat_into_Ord unfolding lt_defThe 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 \)proof from A1 have \( n \subseteq \bigcup nat \)
then show \( n \subseteq nat \) using nat_union_nat
qed
Adding 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 + k \), \( n \subseteq n + k \), \( n \subseteq k + n \)proof from A1, A2 have \( n \leq n \), \( 0 \leq k \), \( n \in nat \), \( k \in nat \) using nat_le_refl, nat_0_le
then have \( n + 0 \leq n + k \) by (rule add_le_mono )
with A1 show \( n \leq n + k \) using add_0_right
then show \( n \subseteq n + k \) using le_imp_subset
then show \( n \subseteq k + n \) using add_commute
qed
Result 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 + j) \lt (n + k) \), \( (n + j) \in (n + k) \)proof from assms have \( j \lt k \) using elem_nat_is_nat
moreover
qed
note \( k \in nat \)
ultimately show \( (n + j) \lt (n + k) \), \( (n + j) \in (n + k) \) using add_lt_mono2, ltD
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 \in nat \) and A2: \( m \in nat \)
shows \( \forall i \in m + n.\ i \in m \vee (\exists j \in n.\ i = m + j) \)proof note A1
moreover
qed
from A2 have \( \forall i \in m + 0.\ i \in m \vee (\exists j \in 0.\ i = m + j) \) using add_0_right
moreover have \( \forall k\in nat.\ \)
\( (\forall i \in m + k.\ i \in m \vee (\exists j \in k.\ i = m + j)) \longrightarrow \)
\( (\forall i \in m + succ(k).\ i \in m \vee (\exists j \in succ(k).\ i = m + j)) \)proof
ultimately show \( \forall i \in m + n.\ i \in m \vee (\exists j \in n.\ i = m + j) \) by (rule ind_on_nat )
{
}
}
}
fix \( k \)
assume A3: \( k \in nat \)
{
assume A4: \( \forall i \in m + k.\ i \in m \vee (\exists j \in k.\ i = m + j) \)
{
fix \( i \)
assume \( i \in m + succ(k) \)
then have \( i \in m + k \vee i = m + k \) using add_succ_right
moreover
from A4, A3 have \( i \in m + k \longrightarrow i \in m \vee (\exists j \in succ(k).\ i = m + j) \)
ultimately have \( i \in m \vee (\exists j \in succ(k).\ i = m + j) \)
then have \( \forall i \in m + succ(k).\ i \in m \vee (\exists j \in succ(k).\ i = m + j) \)
then have \( (\forall i \in m + k.\ i \in m \vee (\exists j \in k.\ i = m + j)) \longrightarrow \)
\( (\forall i \in m + succ(k).\ i \in m \vee (\exists j \in succ(k).\ i = m + j)) \)
then show \( thesis \)
qed
A 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) \)proof from A2 have \( k \in n \vee k=n \)
with A1 have \( k \in nat \) using elem_nat_is_nat
moreover
qed
from A3 have \( 0 \in succ(n) \longrightarrow P(0) \)
moreover from A1, A4 have \( \forall k \in nat.\ (k \in succ(n) \longrightarrow P(k)) \longrightarrow (succ(k) \in succ(n) \longrightarrow P(succ(k))) \) using nat_into_Ord, Ord_succ_mem_iff
ultimately have \( k \in succ(n) \longrightarrow P(k) \) by (rule ind_on_nat )
with A2 show \( P(k) \)
Some properties of positive natural numbers.
lemma succ_plus:
assumes \( n \in nat \), \( k \in nat \)
shows \( succ(n + j) \in nat \), \( succ(n) + succ(j) = succ(succ(n + j)) \) using assmsIf \(k\) is in the successor of \(n\), then the predecessor of \(k\) is in \(n\).
lemma pred_succ_mem:
assumes \( n\in nat \), \( n\neq 0 \), \( k\in succ(n) \)
shows \( pred(k)\in n \)proof from assms(1,3) have \( k\in nat \) using succnat_subset_nat
{
assume \( k\neq 0 \)
with \( k\in nat \) obtain \( j \) where \( j\in nat \) and \( k=succ(j) \) using Nat_ZF_1_L3
with assms(1,3) have \( pred(k)\in n \) using succ_mem, pred_succ_eq
moreover {
}
ultimately show \( thesis \)
qed
assume \( k=0 \)
with assms(1,2) have \( pred(k)\in n \) using pred_0, empty_in_non_empty
For non-zero natural numbers \(\textrm{pred}(n) = n-1\).
lemma pred_minus_one:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( n - 1 = pred(n) \)proof from assms obtain \( k \) where \( n=succ(k) \) using Nat_ZF_1_L3
with assms show \( thesis \) using pred_succ_eq, eq_succ_imp_eq_m1
qed
For natural numbers if \(j\in n\) then \(j+1 \subseteq n\).
lemma mem_add_one_subset:
assumes \( n \in nat \), \( k\in n \)
shows \( k + 1 \subseteq n \)proof from assms have \( k + 1 \in succ(n) \) using elem_nat_is_nat(2), succ_ineq1, succ_add_one(1)
with assms(1) show \( k + 1 \subseteq n \) using nat_mem_lt(2), le_imp_subset
qed
For a natural \(n\) if \(k\in n+1\) then \(k+1\leq n+1\).
lemma succ_ineq2:
assumes \( n \in nat \), \( k \in n + 1 \)
shows \( k + 1 \leq n + 1 \) and \( k\leq n \)proof from assms show \( k\leq n \) using succ_add_one(1), nat_mem_lt(2)
with assms(1) show \( k + 1 \leq n + 1 \) using add_le_mono1
qed
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\in nat \), \( n\neq 0 \)
shows \( \exists m\in nat.\ n = m + 1 \) using assms, Nat_ZF_1_L3, succ_add_one(1)A version of induction on natural numbers that uses the \(n+1\) notation instead of \( succ(n) \).
lemma ind_on_nat1:
assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(k + 1) \)
shows \( P(n) \) using assms, succ_add_one(1), ind_on_natA version of induction for finite sequences using the \(n+1\) notation instead of \( succ(n) \):
lemma fin_nat_ind1:
assumes \( n\in nat \) and \( P(0) \) and \( \forall j\in n.\ P(j)\longrightarrow P(j + 1) \)
shows \( \forall k\in n + 1.\ P(k) \) and \( P(n) \)proof{
}
fix \( k \)
assume \( k\in n + 1 \)
with assms have \( n\in nat \), \( k\in succ(n) \), \( P(0) \), \( \forall j\in n.\ P(j) \longrightarrow P(succ(j)) \) using succ_add_one(1), elem_nat_is_nat(2)
then have \( P(k) \) by (rule fin_nat_ind )
thus \( \forall k\in n + 1.\ P(k) \)
with assms(1) show \( P(n) \)
qed
Simplification rules for addition and subtraction of natural numbers
This section collects useful simplification rules involving addition and subtraction of natural numbers that we couldn't find in standard Isabelle's ArithSimp theory.
Adding and subtracting a natural number cancel each other.
lemma add_subtract:
assumes \( m\in nat \)
shows \( (m + n) - n = m \) using assms, diff_add_inverse2A simplification rule for natural numbers: if \(k < n\) then \(n-(k+1)+1 = n-k\):
lemma nat_subtr_simpl0:
assumes \( n\in nat \), \( k\in n \)
shows \( n - (k + 1) + 1 = n - k \)proof from assms obtain \( m \) where \( m\in nat \) and \( n = m + 1 \) using nat_not0_succ
with assms have \( succ(m) = m + 1 \), \( succ(m - k) = m - k + 1 \) using elem_nat_is_nat(2), succ_add_one
moreover
qed
from assms(2), \( m\in nat \), \( n = m + 1 \) have \( succ(m) - k = succ(m - k) \) using diff_succ, succ_ineq2(2)
ultimately have \( m - k + 1 = m + 1 - k \)
with \( n = m + 1 \) show \( thesis \) using diff_cancel2
If \(k\) is a natural number then \(n+k = n + ((n+k) \#- n))\).
lemma nat_subtr_simpl1:
assumes \( k\in nat \)
shows \( n + ((n + k) - n) = n + k \) using assms, diff_add_inverseIntervals
In 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.
definition
\( \text{NatInterval}(n,k) \equiv \{n + 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 \text{NatInterval}(n,k) \)
shows \( i - n \in k \)proof from A2 obtain \( j \) where I: \( i = n + j \) and II: \( j \in k \) using NatInterval_def
from A1, II have \( j \in nat \) using elem_nat_is_nat
moreover
qed
from I have \( i - n = \text{natify}(j) \) using diff_add_inverse
ultimately have \( i - n = j \)
with II show \( thesis \)
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 \in nat \), \( k \in nat \)
shows \( n \cap \text{NatInterval}(n,k) = 0 \), \( n \cup \text{NatInterval}(n,k) = n + k \)proof{
}
fix \( i \)
assume A2: \( i \in n \) and \( i \in \text{NatInterval}(n,k) \)
then obtain \( j \) where I: \( i = n + j \) and II: \( j \in k \) using NatInterval_def
from A1 have \( k \in nat \) using elem_nat_is_nat
with II have \( j \in nat \) using elem_nat_is_nat
with A1, I have \( n \leq i \) using add_nat_le
moreover
from A1, A2 have \( i \lt n \) using elem_nat_is_nat
ultimately have \( False \) using le_imp_not_lt
thus \( n \cap \text{NatInterval}(n,k) = 0 \)
from A1 have \( n \subseteq n + k \) using add_nat_le
moreover {
}
ultimately have \( n \cup \text{NatInterval}(n,k) \subseteq n + k \)
fix \( i \)
assume \( i \in \text{NatInterval}(n,k) \)
then obtain \( j \) where III: \( i = n + j \) and IV: \( j \in k \) using NatInterval_def
with A1 have \( j \lt k \) using elem_nat_is_nat
with A1, III have \( i \in n + k \) using add_lt_mono2, ltD
moreover
qed
from A1 have \( n + k \subseteq n \cup \text{NatInterval}(n,k) \) using nat_sum_decomp, NatInterval_def
ultimately show \( n \cup \text{NatInterval}(n,k) = n + k \)
Some properties of three adjacent intervals.
lemma adjacent_intervals3:
assumes \( n \in nat \), \( k \in nat \), \( m \in nat \)
shows \( n + k + m = (n + k) \cup \text{NatInterval}(n + k,m) \), \( n + k + m = n \cup \text{NatInterval}(n,k + m) \), \( n + k + m = n \cup \text{NatInterval}(n,k) \cup \text{NatInterval}(n + k,m) \) using assms, add_assoc, length_start_decomp end
lemma succ_explained: shows \( succ(n) = n \cup \{n\} \)
theorem ind_on_nat:
assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(succ(k)) \)
shows \( P(n) \) lemma empty_in_every_succ:
assumes \( n \in nat \)
shows \( 0 \in succ(n) \) lemma Nat_ZF_1_L3:
assumes \( n \in nat \) and \( n\neq 0 \)
shows \( \exists k\in nat.\ n = succ(k) \) lemma nat_union_succ: shows \( nat = (\bigcup n \in nat.\ succ(n)) \)
lemma succ_ineq:
assumes \( n \in nat \)
shows \( \forall i \in n.\ succ(i) \in succ(n) \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) lemma elem_nat_is_nat:
assumes \( n \in nat \) and \( k\in n \)
shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \) lemma nat_mem_lt:
assumes \( n\in nat \)
shows \( k \lt n \longleftrightarrow k\in n \) and \( k\leq n \longleftrightarrow k \in succ(n) \) lemma elem_nat_is_nat:
assumes \( n \in nat \) and \( k\in n \)
shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \) lemma elem_nat_is_nat:
assumes \( n \in nat \) and \( k\in n \)
shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \) lemma nat_union_nat: shows \( nat = \bigcup nat \)
lemma succnat_subset_nat:
assumes \( n \in nat \)
shows \( succ(n) \subseteq nat \) lemma succ_mem:
assumes \( n \in nat \), \( succ(k) \in succ(n) \)
shows \( k\in n \) lemma empty_in_non_empty:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( 0\in n \) lemma succ_ineq1:
assumes \( n \in nat \), \( i\in n \)
shows \( succ(i) \in succ(n) \), \( i + 1 \in n + 1 \), \( i \in n + 1 \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) lemma nat_mem_lt:
assumes \( n\in nat \)
shows \( k \lt n \longleftrightarrow k\in n \) and \( k\leq n \longleftrightarrow k \in succ(n) \) lemma fin_nat_ind:
assumes \( n \in nat \) and \( k \in succ(n) \) and \( P(0) \) and \( \forall j\in n.\ P(j) \longrightarrow P(succ(j)) \)
shows \( P(k) \) lemma nat_not0_succ:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( \exists m\in nat.\ n = m + 1 \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) lemma succ_ineq2:
assumes \( n \in nat \), \( k \in n + 1 \)
shows \( k + 1 \leq n + 1 \) and \( k\leq n \)Definition of NatInterval:
\( \text{NatInterval}(n,k) \equiv \{n + j.\ j\in k\} \)
lemma add_nat_le:
assumes \( n \in nat \) and \( k \in nat \)
shows \( n \leq n + k \), \( n \subseteq n + k \), \( n \subseteq k + n \) lemma nat_sum_decomp:
assumes \( n \in nat \) and \( m \in nat \)
shows \( \forall i \in m + n.\ i \in m \vee (\exists j \in n.\ i = m + j) \) lemma length_start_decomp:
assumes \( n \in nat \), \( k \in nat \)
shows \( n \cap \text{NatInterval}(n,k) = 0 \), \( n \cup \text{NatInterval}(n,k) = n + k \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8