Theory Nat_Miscellanea

section‹Auxiliary results on arithmetic›

theory Nat_Miscellanea
  imports
    Delta_System_Lemma.ZF_Library
begin

hide_const (open) Order.pred
notation add (infixl ‹+⇩ω› 65)
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"
  by (simp add: le_iff)

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

lemma succ_ltI : "succ(j) < n ⟹ j < n"
  by (simp add: succ_leE[OF leI])

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"
    using add_diff_inverse2 by simp_all
  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

lemma oadd_lt_mono2 :
  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