Theory Nat_ZF_IML

theory Nat_ZF_IML
imports Arith
(* 
This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005 - 2008 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{Nat\_ZF.thy}*}

theory Nat_ZF_IML imports Arith

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$".
*}


section{*Induction*}

text{*The induction lemmas in the standard Isabelle's Nat.thy file like
for example @{text "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 @{text "succ"}, anyway?*}

lemma succ_explained: shows "succ(n) = n ∪ {n}"
using succ_iff by auto

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{*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 = (\<Union>n ∈ nat. succ(n))"
proof
show "nat ⊆ (\<Union>n ∈ nat. succ(n))" by auto
next
{ fix k assume A2: "k ∈ (\<Union>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 "(\<Union>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) ⊆ (\<Union>n ∈ nat. succ(n))" by auto
then show "succ(n) ⊆ nat" using nat_union_succ by simp
qed

text{*Element of a natural number is a natural number.*}

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{*Element of a natural number is less or equal than
the number. *}

lemma elem_nat_is_Le: assumes A1: "n ∈ nat" and A2: "k∈n"
shows "k ≤ n" and "⟨k,n⟩ ∈ Le"
proof -
from A1 A2 have "k < n"
using elem_nat_is_nat by simp
and "k ∈ nat"
using elem_nat_is_nat by auto*)




text{*The set of natural numbers is the union of its elements.*}

lemma nat_union_nat: shows "nat = \<Union> 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 ⊆ \<Union> nat" by auto
then show "n ⊆ nat" using nat_union_nat by simp
qed

text{*Adding a 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

section{*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. Recall that in standard
Isabelle's @{text "Arith.thy"} the symbol @{text "#+"} is defined
as the sum of natural numbers.*}


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{*Sme 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