# Theory CZH_Sets_Nat

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Further properties of natural numbers›
theory CZH_Sets_Nat
imports CZH_Sets_Sets
begin

subsection‹Background›

text‹
The section exposes certain fundamental properties of natural numbers and
provides convenience utilities for doing arithmetic within the type \<^typ>‹V›.

Many of the results that are presented in this sections were carried over
(with amendments) from the theory ‹Nat› that can be found in the main
library of Isabelle/HOL.
›

notation ord_of_nat (‹_⇩ℕ› [999] 999)

named_theorems nat_omega_simps

declare One_nat_def[simp del]

abbreviation (input) vpfst where "vpfst a ≡ a⦇0⦈"
abbreviation (input) vpsnd where "vpsnd a ≡ a⦇1⇩ℕ⦈"
abbreviation (input) vpthrd where "vpthrd a ≡ a⦇2⇩ℕ⦈"

subsection‹Conversion between \<^typ>‹V› and ‹nat››

subsubsection‹Primitive arithmetic›

lemma ord_of_nat_plus[nat_omega_simps]: "a⇩ℕ + b⇩ℕ = (a + b)⇩ℕ"
by (induct b) (simp_all add: plus_V_succ_right)

lemma ord_of_nat_times[nat_omega_simps]: "a⇩ℕ * b⇩ℕ = (a * b)⇩ℕ"
by (induct b) (simp_all add: mult_succ nat_omega_simps)

lemma ord_of_nat_succ[nat_omega_simps]: "succ (a⇩ℕ) = (Suc a)⇩ℕ" by auto

lemmas [nat_omega_simps] = nat_cadd_eq_add

lemma ord_of_nat_csucc[nat_omega_simps]: "csucc (a⇩ℕ) = succ (a⇩ℕ)"
using finite_csucc by blast

lemma ord_of_nat_succ_vempty[nat_omega_simps]: "succ 0 = 1⇩ℕ" by auto

lemma ord_of_nat_vone[nat_omega_simps]: "1 = 1⇩ℕ" by auto

subsubsection‹Transfer›

definition cr_omega :: "V ⇒ nat ⇒ bool"
where "cr_omega a b ⟷ (a = ord_of_nat b)"

text‹Transfer setup.›

lemma cr_omega_right_total[transfer_rule]: "right_total cr_omega"
unfolding cr_omega_def right_total_def by simp

lemma cr_omega_bi_unqie[transfer_rule]: "bi_unique cr_omega"
unfolding cr_omega_def bi_unique_def
by (simp add: inj_eq inj_ord_of_nat)

lemma omega_transfer_domain_rule[transfer_domain_rule]:
"Domainp cr_omega = (λx. x ∈⇩∘ ω)"
unfolding cr_omega_def by (auto simp: elts_ω)

lemma omega_transfer[transfer_rule]:
"(rel_set cr_omega) (elts ω) (UNIV::nat set)"
unfolding cr_omega_def rel_set_def by (simp add: elts_ω)

lemma omega_of_real_transfer[transfer_rule]: "cr_omega (ord_of_nat a) a"
unfolding cr_omega_def by auto

text‹Operations.›

lemma omega_succ_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_omega ===> cr_omega) succ Suc"
proof(intro rel_funI, unfold cr_omega_def)
fix x y assume prems: "x = y⇩ℕ"
show "succ x = Suc y⇩ℕ" unfolding prems ord_of_nat_succ[symmetric] ..
qed

lemma omega_plus_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_omega ===> cr_omega ===> cr_omega) (+) (+)"
by (intro rel_funI, unfold cr_omega_def) (simp add: nat_omega_simps)

lemma omega_mult_transfer[transfer_rule]:
includes lifting_syntax
shows "(cr_omega ===> cr_omega ===> cr_omega) (*) (*)"
by (intro rel_funI, unfold cr_omega_def) (simp add: nat_omega_simps)

lemma ord_of_nat_card_transfer[transfer_rule]:
includes lifting_syntax
shows "(rel_set (=) ===> cr_omega) (λx. ord_of_nat (card x)) card"
by (intro rel_funI) (simp add: cr_omega_def rel_set_eq)

lemma ord_of_nat_transfer[transfer_rule]:
"(rel_fun cr_omega (=)) id ord_of_nat"
unfolding cr_omega_def by auto

subsection‹Elementary results›

lemma ord_of_nat_vempty: "0 = 0⇩ℕ" by auto

lemma set_vzero_eq_ord_of_nat_vone: "set {0} = 1⇩ℕ"
by (metis elts_1 set_of_elts ord_of_nat_vone)

lemma vone_in_omega[simp]: "1 ∈⇩∘ ω" unfolding ω_def by force

lemma nat_of_omega:
assumes "n ∈⇩∘ ω"
obtains m where "n = m⇩ℕ"
using assms unfolding ω_def by clarsimp

lemma omega_prev:
assumes "n ∈⇩∘ ω" and "0 ∈⇩∘ n"
obtains k where "n = succ k"
proof-
from assms nat_of_omega obtain m where "n = m⇩ℕ" by auto
with assms(2) obtain m' where "m = Suc m'"
unfolding less_V_def by (auto dest: gr0_implies_Suc)
with that show ?thesis unfolding ‹n = m⇩ℕ› using ord_of_nat.simps(2) by blast
qed

lemma omega_vplus_commutative:
assumes "a ∈⇩∘ ω" and "b ∈⇩∘ ω"
shows "a + b = b + a"
using assms by (metis Groups.add_ac(2) nat_of_omega ord_of_nat_plus)

lemma omega_vinetrsection[intro]:
assumes "m ∈⇩∘ ω" and "n ∈⇩∘ ω"
shows "m ∩⇩∘ n ∈⇩∘ ω"
proof-
from nat_into_Ord[OF assms(1)] nat_into_Ord[OF assms(2)] Ord_linear_le
consider "m ⊆⇩∘ n" | "n ⊆⇩∘ m"
by auto
then show ?thesis by cases (simp_all add: assms inf.absorb1 inf.absorb2)
qed

subsection‹Induction›

lemma omega_induct_all[consumes 1, case_names step]:
assumes "n ∈⇩∘ ω" and "⋀x. ⟦x ∈⇩∘ ω; ⋀y. y ∈⇩∘ x ⟹ P y⟧ ⟹ P x"
shows "P n"
using assms by (metis Ord_ω Ord_induct Ord_linear Ord_trans nat_into_Ord)

lemma omega_induct[consumes 1, case_names 0 succ]:
assumes "n ∈⇩∘ ω" and "P 0" and "⋀n. ⟦ n ∈⇩∘ ω; P n ⟧ ⟹ P (succ n)"
shows "P n"
using assms(1,3)
proof(induct rule: omega_induct_all)
case (step x) show ?case
proof(cases ‹x = 0›)
case True with assms(2) show ?thesis by simp
next
case False
with step(1) have "0 ∈⇩∘ x" by (simp add: mem_0_Ord)
with ‹x ∈⇩∘ ω› obtain y where x_def: "x = succ y" by (elim omega_prev)
with elts_succ step.hyps(1) have "y ∈⇩∘ ω" by (blast intro: Ord_trans)
have "y ∈⇩∘ x" by (simp add: ‹x = succ y›)
have "P y" by (auto intro: step.prems step.hyps(2)[OF ‹y ∈⇩∘ x›])
from step.prems[OF ‹y ∈⇩∘ ω› ‹P y›, folded x_def] show "P x" .
qed
qed

subsection‹Methods›

text‹
The following methods provide an infrastructure for working with goals of the
form ‹a ∈⇩∘ n⇩ℕ ⟹ P a›.
›

lemma in_succE:
assumes "a ∈⇩∘ succ n" and "⋀a. a ∈⇩∘ n ⟹ P a" and "P n"
shows "P a"
using assms by auto

method Suc_of_numeral =
(
unfold numeral.simps add.assoc,
use nothing in ‹unfold Suc_eq_plus1_left[symmetric], unfold One_nat_def›
)

method succ_of_numeral =
(
Suc_of_numeral,
use nothing in ‹unfold ord_of_nat_succ[symmetric] ord_of_nat_zero›
)

method numeral_of_succ =
(
unfold nat_omega_simps,
use nothing in
‹
unfold numeral.simps[symmetric] Suc_numeral add_num_simps,
(unfold numerals(1))?
›
)

method elim_in_succ =
(
(
elim in_succE;
use nothing in ‹(unfold triv_forall_equality)?; (numeral_of_succ)?›
),
simp
)

method elim_in_numeral = (succ_of_numeral, use nothing in ‹elim_in_succ›)

subsection‹Auxiliary›

lemma one: "1⇩ℕ = set {0}" by auto

lemma two: "2⇩ℕ = set {0, 1⇩ℕ}" by force

lemma three: "3⇩ℕ = set {0, 1⇩ℕ, 2⇩ℕ}" by force

lemma four: "4⇩ℕ = set {0, 1⇩ℕ, 2⇩ℕ, 3⇩ℕ}" by force

lemma two_vdiff_zero[simp]: "set {0, 1⇩ℕ} -⇩∘ set {0} = set {1⇩ℕ}" by auto
lemma two_vdiff_one[simp]: "set {0, 1⇩ℕ} -⇩∘ set {1⇩ℕ} = set {0}" by auto

text‹\newpage›

end```