Theory Nat_Miscellanea

section‹Auxiliary results on arithmetic›
theory Nat_Miscellanea imports ZF begin

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 =  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 in_succ_in_nat : "m ∈ nat ⟹ n ∈ succ(m) ⟹ n ∈ nat"
  by(auto simp add:in_n_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])

lemma succ_In : "n ∈ nat ⟹ succ(j) ∈ n ⟹ j ∈ n"
  by (rule succ_ltI[THEN ltD], auto intro: ltI)

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)


lemma funcI : "f ∈ A → B ⟹ a ∈ A ⟹ b= f ` a ⟹ ⟨a, b⟩ ∈ f"
  by(simp_all add: apply_Pair)

lemmas natEin = natE [OF lt_nat_in_nat]

lemma succ_in : "succ(x) ≤ y  ⟹ x ∈ y"
  by (auto dest:ltD)

lemmas Un_least_lt_iffn =  Un_least_lt_iff [OF nat_into_Ord nat_into_Ord]

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 pred_le : "n∈ nat ⟹ m ∈ nat ⟹ n ≤ succ(m) ⟹ pred(n) ≤ m"
  by(subgoal_tac "pred(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 pred2_Un: 
  assumes "j ∈ nat" "m ≤ j" "n ≤ j" 
  shows "pred(pred(m ∪ n)) ≤ pred(pred(j))" 
  using assms pred_mono[of "j"] le_in_nat Un_least_lt pred_mono by simp

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

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

lemma nat_un_max : "Ord(i) ⟹ Ord(j) ⟹ i ∪ j = max(i,j)"
  using max_def nat_union_abs1 not_lt_iff_le leI nat_union_abs2
  by auto

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

lemma le_not_lt_nat : "Ord(p) ⟹ Ord(q) ⟹ ¬ p≤ q ⟹ q ≤ p" 
  by (rule ltE,rule not_le_iff_lt[THEN iffD1],auto,drule ltI[of q p],auto,erule leI)

lemmas nat_simp_union = nat_un_max nat_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 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]
    nat_simp_union 
  by auto

lemma Un_le : "p ≤ r ⟹ q ≤ r ⟹
               Ord(p) ⟹ Ord(q) ⟹ Ord(r) ⟹ 
                p ∪ q ≤ r"
  using nat_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 nat_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 ⟹ Arith.pred(succ(x) ∪ y) = x ∪ Arith.pred(y)"
  "x ∈ nat ⟹ y ∈ nat ⟹ Arith.pred(x ∪ succ(y)) = Arith.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 diff_cancel :
  assumes "m ∈ nat" "n∈nat" "m < n"
  shows "m#-n = 0"
  using assms diff_is_0_lemma leI by 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

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)"
  using assms 
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 nat_simp_union(1) nat_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  nat_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 nat_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 nat_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 nat_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 nat_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