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