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