# Theory Nat_Miscellanea

```section‹Auxiliary results on arithmetic›

theory Nat_Miscellanea
imports
Delta_System_Lemma.ZF_Library
begin

hide_const (open) Order.pred
notation diff (infixl ‹-⇩ω› 65)

text‹Most of these results will get used at some point for the
calculation of arities.›

lemmas nat_succI =  Ord_succ_mem_iff [THEN iffD2,OF nat_into_Ord]

lemma nat_succD : "m ∈ nat ⟹  succ(n) ∈ succ(m) ⟹ n ∈ m"
by (drule_tac j="succ(m)" in ltI,auto elim:ltD)

lemmas zero_in_succ = ltD [OF nat_0_le]

lemma in_n_in_nat :  "m ∈ nat ⟹ n ∈ m ⟹ n ∈ nat"
by(drule ltI[of "n"],auto simp add: lt_nat_in_nat)

lemma ltI_neg : "x ∈ nat ⟹ j ≤ x ⟹ j ≠ x ⟹ j < x"

lemma succ_pred_eq  :  "m ∈ nat ⟹ m ≠ 0  ⟹ succ(pred(m)) = m"
by (auto elim: natE)

lemma succ_ltI : "succ(j) < n ⟹ j < n"

lemmas succ_leD = succ_leE[OF leI]

lemma succpred_leI : "n ∈ nat ⟹  n ≤ succ(pred(n))"
by (auto elim: natE)

lemma succpred_n0 : "succ(n) ∈ p ⟹ p≠0"
by (auto)

lemmas natEin = natE [OF lt_nat_in_nat]

lemmas Un_least_lt_iffn =  Un_least_lt_iff [OF nat_into_Ord nat_into_Ord]

lemma pred_type : "m ∈ nat ⟹ n ≤ m ⟹ n∈nat"
by (rule leE,auto simp:in_n_in_nat ltD)

lemma pred_le : "m ∈ nat ⟹ n ≤ succ(m) ⟹ pred(n) ≤ m"
by(rule_tac n="n" in natE,auto simp add:pred_type[of "succ(m)"])

lemma pred_le2 : "n∈ nat ⟹ m ∈ nat ⟹ pred(n) ≤ m ⟹ n ≤ succ(m)"
by(subgoal_tac "n∈nat",rule_tac n="n" in natE,auto)

lemma Un_leD1 : "Ord(i)⟹ Ord(j)⟹ Ord(k)⟹  i ∪ j ≤ k ⟹ i ≤ k"
by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)

lemma Un_leD2 : "Ord(i)⟹ Ord(j)⟹ Ord(k)⟹  i ∪ j ≤k ⟹ j ≤ k"
by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)

lemma gt1 : "n ∈ nat ⟹ i ∈ n ⟹ i ≠ 0 ⟹ i ≠ 1 ⟹ 1<i"
by(rule_tac n="i" in natE,erule in_n_in_nat,auto intro: Ord_0_lt)

lemma pred_mono : "m ∈ nat ⟹ n ≤ m ⟹ pred(n) ≤ pred(m)"
by(rule_tac n="n" in natE,auto simp add:le_in_nat,erule_tac n="m" in natE,auto)

lemma succ_mono : "m ∈ nat ⟹ n ≤ m ⟹ succ(n) ≤ succ(m)"
by auto

lemma union_abs1 :
"⟦ i ≤ j ⟧ ⟹ i ∪ j = j"
by (rule Un_absorb1,erule le_imp_subset)

lemma union_abs2 :
"⟦ i ≤ j ⟧ ⟹ j ∪ i = j"
by (rule Un_absorb2,erule le_imp_subset)

lemma ord_un_max : "Ord(i) ⟹ Ord(j) ⟹ i ∪ j = max(i,j)"
using max_def union_abs1 not_lt_iff_le leI union_abs2
by auto

lemma ord_max_ty : "Ord(i) ⟹Ord(j) ⟹ Ord(max(i,j))"
unfolding max_def by simp

lemmas ord_simp_union = ord_un_max ord_max_ty max_def

lemma le_succ : "x∈nat ⟹ x≤succ(x)" by simp

lemma le_pred : "x∈nat ⟹ pred(x)≤x"
using pred_le[OF _ le_succ] pred_succ_eq
by simp

lemma not_le_anti_sym : "x∈nat ⟹ y ∈ nat ⟹ ¬ x≤y ⟹ ¬y≤x ⟹ y=x"
using Ord_linear not_le_iff_lt ltD lt_trans
by auto

lemma Un_le_compat : "o ≤ p ⟹ q ≤ r ⟹ Ord(o) ⟹ Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹ o ∪ q ≤ p ∪ r"
using le_trans[of q r "p∪r",OF _ Un_upper2_le] le_trans[of o p "p∪r",OF _ Un_upper1_le]
ord_simp_union
by auto

lemma Un_le : "p ≤ r ⟹ q ≤ r ⟹
Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹
p ∪ q ≤ r"
using ord_simp_union by auto

lemma Un_leI3 : "o ≤ r ⟹ p ≤ r ⟹ q ≤ r ⟹
Ord(o) ⟹ Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹
o ∪ p ∪ q ≤ r"
using ord_simp_union by auto

lemma diff_mono :
assumes "m ∈ nat" "n∈nat" "p ∈ nat" "m < n" "p≤m"
shows "m#-p < n#-p"
proof -
from assms
have "m#-p ∈ nat" "m#-p +⇩ωp = m"
with assms
show ?thesis
using less_diff_conv[of n p "m #- p",THEN iffD2] by simp
qed

lemma pred_Un:
"x ∈ nat ⟹ y ∈ nat ⟹ pred(succ(x) ∪ y) = x ∪ pred(y)"
"x ∈ nat ⟹ y ∈ nat ⟹ pred(x ∪ succ(y)) = pred(x) ∪ y"
using pred_Un_distrib pred_succ_eq by simp_all

lemma le_natI : "j ≤ n ⟹ n ∈ nat ⟹ j∈nat"
by(drule ltD,rule in_n_in_nat,rule nat_succ_iff[THEN iffD2,of n],simp_all)

lemma le_natE : "n∈nat ⟹ j < n ⟹  j∈n"
by(rule ltE[of j n],simp+)

lemma leD : assumes "n∈nat" "j ≤ n"
shows "j < n | j = n"
using leE[OF ‹j≤n›,of "j<n | j = n"] by auto

lemma pred_nat_eq :
assumes "n∈nat"
shows "pred(n) = ⋃ n"
using assms
proof(induct)
case 0
then show ?case by simp
next
case (succ x)
then show ?case using pred_succ_eq Ord_Union_succ_eq
by simp
qed

subsection‹Some results in ordinal arithmetic›
text‹The following results are auxiliary to the proof of
wellfoundedness of the relation \<^term>‹frecR››

lemma max_cong :
assumes "x ≤ y" "Ord(y)" "Ord(z)"
shows "max(x,y) ≤ max(y,z)"
proof (cases "y ≤ z")
case True
then show ?thesis
unfolding max_def using assms by simp
next
case False
then have "z ≤ y"  using assms not_le_iff_lt leI by simp
then show ?thesis
unfolding max_def using assms by simp
qed

lemma max_commutes :
assumes "Ord(x)" "Ord(y)"
shows "max(x,y) = max(y,x)"
using assms Un_commute ord_simp_union(1) ord_simp_union(1)[symmetric] by auto

lemma max_cong2 :
assumes "x ≤ y" "Ord(y)" "Ord(z)" "Ord(x)"
shows "max(x,z) ≤ max(y,z)"
proof -
from assms
have " x ∪ z ≤ y ∪ z"
using lt_Ord Ord_Un Un_mono[OF  le_imp_subset[OF ‹x≤y›]]  subset_imp_le by auto
then show ?thesis
using  ord_simp_union ‹Ord(x)› ‹Ord(z)› ‹Ord(y)› by simp
qed

lemma max_D1 :
assumes "x = y" "w < z"  "Ord(x)"  "Ord(w)" "Ord(z)" "max(x,w) = max(y,z)"
shows "z≤y"
proof -
from assms
have "w <  x ∪ w" using Un_upper2_lt[OF ‹w<z›] assms ord_simp_union by simp
then
have "w < x" using assms lt_Un_iff[of x w w] lt_not_refl by auto
then
have "y = y ∪ z" using assms max_commutes ord_simp_union assms leI by simp
then
show ?thesis using Un_leD2 assms by simp
qed

lemma max_D2 :
assumes "w = y ∨ w = z" "x < y"  "Ord(x)"  "Ord(w)" "Ord(y)" "Ord(z)" "max(x,w) = max(y,z)"
shows "x<w"
proof -
from assms
have "x < z ∪ y" using Un_upper2_lt[OF ‹x<y›] by simp
then
consider (a) "x < y" | (b) "x < w"
using assms ord_simp_union by simp
then show ?thesis proof (cases)
case a
consider (c) "w = y" | (d) "w = z"
using assms by auto
then show ?thesis proof (cases)
case c
with a show ?thesis by simp
next
case d
with a
show ?thesis
proof (cases "y <w")
case True
then show ?thesis using lt_trans[OF ‹x<y›] by simp
next
case False
then
have "w ≤ y"
using not_lt_iff_le[OF assms(5) assms(4)] by simp
with ‹w=z›
have "max(z,y) = y"  unfolding max_def using assms by simp
with assms
have "... = x ∪ w" using ord_simp_union max_commutes  by simp
then show ?thesis using le_Un_iff assms by blast
qed
qed
next
case b
then show ?thesis .
qed
qed

assumes  "Ord(n)" "Ord(α)" "Ord(β)" "α < β" "x < n" "y < n" "0 <n"
shows "n ** α + x < n **β + y"
proof -
consider (0) "β=0" | (s) γ where  "Ord(γ)" "β = succ(γ)" | (l) "Limit(β)"
using Ord_cases[OF ‹Ord(β)›,of ?thesis] by force
then show ?thesis
proof cases
case 0
then show ?thesis using ‹α<β› by auto
next
case s
then
have "α≤γ" using ‹α<β› using leI by auto
then
have "n ** α ≤ n ** γ" using omult_le_mono[OF _ ‹α≤γ›] ‹Ord(n)› by simp
then
have "n ** α + x < n ** γ + n" using oadd_lt_mono[OF _ ‹x<n›] by simp
also
have "... = n ** β" using ‹β=succ(_)› omult_succ ‹Ord(β)› ‹Ord(n)› by simp
finally
have "n ** α + x < n ** β" by auto
then
show ?thesis using oadd_le_self ‹Ord(β)› lt_trans2 ‹Ord(n)› by auto
next
case l
have "Ord(x)" using ‹x<n› lt_Ord by simp
with l
have "succ(α) < β" using Limit_has_succ ‹α<β› by simp
have "n ** α + x < n ** α + n"
using oadd_lt_mono[OF le_refl[OF Ord_omult[OF _ ‹Ord(α)›]] ‹x<n›] ‹Ord(n)› by simp
also
have "... = n ** succ(α)" using omult_succ ‹Ord(α)› ‹Ord(n)› by simp
finally
have "n ** α + x < n ** succ(α)" by simp
with ‹succ(α) < β›
have "n ** α + x < n ** β" using lt_trans omult_lt_mono ‹Ord(n)› ‹0<n›  by auto
then show ?thesis using oadd_le_self ‹Ord(β)› lt_trans2 ‹Ord(n)› by auto
qed
qed
end
```