Theory Lambda_Free_RPOs.Lambda_Free_Util
section ‹Utilities for Lambda-Free Orders›
theory Lambda_Free_Util
imports "HOL-Library.Extended_Nat" "HOL-Library.Multiset_Order"
begin
text ‹
This theory gathers various lemmas that likely belong elsewhere in Isabelle or
the \emph{Archive of Formal Proofs}. Most (but certainly not all) of them are
used to formalize orders on ‹λ›-free higher-order terms.
›
subsection ‹Function Power›
lemma funpow_lesseq_iter:
fixes f :: "('a::order) ⇒ 'a"
assumes mono: "⋀k. k ≤ f k" and m_le_n: "m ≤ n"
shows "(f ^^ m) k ≤ (f ^^ n) k"
using m_le_n by (induct n) (fastforce simp: le_Suc_eq intro: mono order_trans)+
lemma funpow_less_iter:
fixes f :: "('a::order) ⇒ 'a"
assumes mono: "⋀k. k < f k" and m_lt_n: "m < n"
shows "(f ^^ m) k < (f ^^ n) k"
using m_lt_n by (induct n) (auto, blast intro: mono less_trans dest: less_antisym)
subsection ‹Least Operator›
lemma Least_eq[simp]: "(LEAST y. y = x) = x" and "(LEAST y. x = y) = x" for x :: "'a::order"
by (blast intro: Least_equality)+
lemma Least_in_nonempty_set_imp_ex:
fixes f :: "'b ⇒ ('a::wellorder)"
assumes
A_nemp: "A ≠ {}" and
P_least: "P (LEAST y. ∃x ∈ A. y = f x)"
shows "∃x ∈ A. P (f x)"
proof -
obtain a where a: "a ∈ A"
using A_nemp by fast
have "∃x. x ∈ A ∧ (LEAST y. ∃x. x ∈ A ∧ y = f x) = f x"
by (rule LeastI[of _ "f a"]) (fast intro: a)
thus ?thesis
by (metis P_least)
qed
lemma Least_eq_0_enat: "P 0 ⟹ (LEAST x :: enat. P x) = 0"
by (simp add: Least_equality)
subsection ‹Antisymmetric Relations›
lemma irrefl_trans_imp_antisym: "irrefl r ⟹ trans r ⟹ antisym r"
unfolding irrefl_def trans_def antisym_def by fast
lemma irreflp_transp_imp_antisymP: "irreflp p ⟹ transp p ⟹ antisymp p"
by (fact irrefl_trans_imp_antisym [to_pred])
subsection ‹Acyclic Relations›
lemma finite_nonempty_ex_succ_imp_cyclic:
assumes
fin: "finite A" and
nemp: "A ≠ {}" and
ex_y: "∀x ∈ A. ∃y ∈ A. (y, x) ∈ r"
shows "¬ acyclic r"
proof -
let ?R = "{(x, y). x ∈ A ∧ y ∈ A ∧ (x, y) ∈ r}"
have R_sub_r: "?R ⊆ r"
by auto
have "?R ⊆ A × A"
by auto
hence fin_R: "finite ?R"
by (auto intro: fin dest!: infinite_super)
have "¬ acyclic ?R"
by (rule notI, drule finite_acyclic_wf[OF fin_R], unfold wf_eq_minimal, drule spec[of _ A],
use ex_y nemp in blast)
thus ?thesis
using R_sub_r acyclic_subset by auto
qed
subsection ‹Reflexive, Transitive Closure›
lemma relcomp_subset_left_imp_relcomp_trancl_subset_left:
assumes sub: "R O S ⊆ R"
shows "R O S⇧* ⊆ R"
proof
fix x
assume "x ∈ R O S⇧*"
then obtain n where "x ∈ R O S ^^ n"
using rtrancl_imp_relpow by fastforce
thus "x ∈ R"
proof (induct n)
case (Suc m)
thus ?case
by (metis (no_types) O_assoc inf_sup_ord(3) le_iff_sup relcomp_distrib2 relpow.simps(2)
relpow_commute sub subsetCE)
qed auto
qed
lemma f_chain_in_rtrancl:
assumes m_le_n: "m ≤ n" and f_chain: "∀i ∈ {m..<n}. (f i, f (Suc i)) ∈ R"
shows "(f m, f n) ∈ R⇧*"
proof (rule relpow_imp_rtrancl, rule relpow_fun_conv[THEN iffD2], intro exI conjI)
let ?g = "λi. f (m + i)"
let ?k = "n - m"
show "?g 0 = f m"
by simp
show "?g ?k = f n"
using m_le_n by force
show "(∀i < ?k. (?g i, ?g (Suc i)) ∈ R)"
by (simp add: f_chain)
qed
lemma f_rev_chain_in_rtrancl:
assumes m_le_n: "m ≤ n" and f_chain: "∀i ∈ {m..<n}. (f (Suc i), f i) ∈ R"
shows "(f n, f m) ∈ R⇧*"
by (rule f_chain_in_rtrancl[OF m_le_n, of "λi. f (n + m - i)", simplified])
(metis f_chain le_add_diff Suc_diff_Suc Suc_leI atLeastLessThan_iff diff_Suc_diff_eq1 diff_less
le_add1 less_le_trans zero_less_Suc)
subsection ‹Well-Founded Relations›
lemma wf_app: "wf r ⟹ wf {(x, y). (f x, f y) ∈ r}"
unfolding wf_eq_minimal by (intro allI, drule spec[of _ "f ` Q" for Q]) fast
lemma wfP_app: "wfP p ⟹ wfP (λx y. p (f x) (f y))"
unfolding wfP_def by (rule wf_app[of "{(x, y). p x y}" f, simplified])
lemma wf_exists_minimal:
assumes wf: "wf r" and Q: "Q x"
shows "∃x. Q x ∧ (∀y. (f y, f x) ∈ r ⟶ ¬ Q y)"
using wf_eq_minimal[THEN iffD1, OF wf_app[OF wf], rule_format, of _ "{x. Q x}", simplified, OF Q]
by blast
lemma wfP_exists_minimal:
assumes wf: "wfP p" and Q: "Q x"
shows "∃x. Q x ∧ (∀y. p (f y) (f x) ⟶ ¬ Q y)"
by (rule wf_exists_minimal[of "{(x, y). p x y}" Q x, OF wf[unfolded wfP_def] Q, simplified])
lemma finite_irrefl_trans_imp_wf: "finite r ⟹ irrefl r ⟹ trans r ⟹ wf r"
by (erule finite_acyclic_wf) (simp add: acyclic_irrefl)
lemma finite_irreflp_transp_imp_wfp:
"finite {(x, y). p x y} ⟹ irreflp p ⟹ transp p ⟹ wfP p"
using finite_irrefl_trans_imp_wf[of "{(x, y). p x y}"]
unfolding wfP_def transp_def irreflp_def trans_def irrefl_def mem_Collect_eq prod.case
by assumption
lemma wf_infinite_down_chain_compatible:
assumes
wf_R: "wf R" and
inf_chain_RS: "∀i. (f (Suc i), f i) ∈ R ∪ S" and
O_subset: "R O S ⊆ R"
shows "∃k. ∀i. (f (Suc (i + k)), f (i + k)) ∈ S"
proof (rule ccontr)
assume "∄k. ∀i. (f (Suc (i + k)), f (i + k)) ∈ S"
hence "∀k. ∃i. (f (Suc (i + k)), f (i + k)) ∉ S"
by blast
hence "∀k. ∃i > k. (f (Suc i), f i) ∉ S"
by (metis add.commute add_Suc less_add_Suc1)
hence "∀k. ∃i > k. (f (Suc i), f i) ∈ R"
using inf_chain_RS by blast
hence "∃i > k. (f (Suc i), f i) ∈ R ∧ (∀j > k. (f (Suc j), f j) ∈ R ⟶ j ≥ i)" for k
using wf_eq_minimal[THEN iffD1, OF wf_less, rule_format,
of _ "{i. i > k ∧ (f (Suc i), f i) ∈ R}", simplified]
by (meson not_less)
then obtain j_of where
j_of_gt: "⋀k. j_of k > k" and
j_of_in_R: "⋀k. (f (Suc (j_of k)), f (j_of k)) ∈ R" and
j_of_min: "⋀k. ∀j > k. (f (Suc j), f j) ∈ R ⟶ j ≥ j_of k"
by moura
have j_of_min_s: "⋀k j. j > k ⟹ j < j_of k ⟹ (f (Suc j), f j) ∈ S"
using j_of_min inf_chain_RS by fastforce
define g :: "nat ⇒ 'a" where "⋀k. g k = f (Suc ((j_of ^^ k) 0))"
have between_g[simplified]: "(f ((j_of ^^ (Suc i)) 0), f (Suc ((j_of ^^ i) 0))) ∈ S⇧*" for i
proof (rule f_rev_chain_in_rtrancl; clarify?)
show "Suc ((j_of ^^ i) 0) ≤ (j_of ^^ Suc i) 0"
using j_of_gt by (simp add: Suc_leI)
next
fix ia
assume ia: "ia ∈ {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0}"
have ia_gt: "ia > (j_of ^^ i) 0"
using ia by auto
have ia_lt: "ia < j_of ((j_of ^^ i) 0)"
using ia by auto
show "(f (Suc ia), f ia) ∈ S"
by (rule j_of_min_s[OF ia_gt ia_lt])
qed
have "⋀i. (g (Suc i), g i) ∈ R"
unfolding g_def funpow.simps comp_def
by (rule subsetD[OF relcomp_subset_left_imp_relcomp_trancl_subset_left[OF O_subset]])
(rule relcompI[OF j_of_in_R between_g])
moreover have "∀f. ∃i. (f (Suc i), f i) ∉ R"
using wf_R[unfolded wf_iff_no_infinite_down_chain] by blast
ultimately show False
by blast
qed
subsection ‹Wellorders›
lemma (in wellorder) exists_minimal:
fixes x :: 'a
assumes "P x"
shows "∃x. P x ∧ (∀y. P y ⟶ y ≥ x)"
using assms by (auto intro: LeastI Least_le)
subsection ‹Lists›
lemma rev_induct2[consumes 1, case_names Nil snoc]:
"length xs = length ys ⟹ P [] [] ⟹
(⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs @ [x]) (ys @ [y])) ⟹ P xs ys"
proof (induct xs arbitrary: ys rule: rev_induct)
case (snoc x xs ys)
thus ?case
by (induct ys rule: rev_induct) simp_all
qed auto
lemma hd_in_set: "length xs ≠ 0 ⟹ hd xs ∈ set xs"
by (cases xs) auto
lemma in_lists_iff_set: "xs ∈ lists A ⟷ set xs ⊆ A"
by fast
lemma butlast_append_Cons[simp]: "butlast (xs @ y # ys) = xs @ butlast (y # ys)"
using butlast_append[of xs "y # ys", simplified] by simp
lemma rev_in_lists[simp]: "rev xs ∈ lists A ⟷ xs ∈ lists A"
by auto
lemma hd_le_sum_list:
fixes xs :: "'a::ordered_ab_semigroup_monoid_add_imp_le list"
assumes "xs ≠ []" and "∀i < length xs. xs ! i ≥ 0"
shows "hd xs ≤ sum_list xs"
using assms
by (induct xs rule: rev_induct, simp_all,
metis add_cancel_right_left add_increasing2 hd_append2 lessI less_SucI list.sel(1) nth_append
nth_append_length order_refl self_append_conv2 sum_list.Nil)
lemma sum_list_ge_length_times:
fixes a :: "'a::{ordered_ab_semigroup_add,semiring_1}"
assumes "∀i < length xs. xs ! i ≥ a"
shows "sum_list xs ≥ of_nat (length xs) * a"
using assms
proof (induct xs)
case (Cons x xs)
note ih = this(1) and xxs_i_ge_a = this(2)
have xs_i_ge_a: "∀i < length xs. xs ! i ≥ a"
using xxs_i_ge_a by auto
have "x ≥ a"
using xxs_i_ge_a by auto
thus ?case
using ih[OF xs_i_ge_a] by (simp add: ring_distribs ordered_ab_semigroup_add_class.add_mono)
qed auto
lemma prod_list_nonneg:
fixes xs :: "('a :: {ordered_semiring_0,linordered_nonzero_semiring}) list"
assumes "⋀x. x ∈ set xs ⟹ x ≥ 0"
shows "prod_list xs ≥ 0"
using assms by (induct xs) auto
lemma zip_append_0_upt:
"zip (xs @ ys) [0..<length xs + length ys] =
zip xs [0..<length xs] @ zip ys [length xs..<length xs + length ys]"
proof (induct ys arbitrary: xs)
case (Cons y ys)
note ih = this
show ?case
using ih[of "xs @ [y]"] by (simp, cases ys, simp, simp add: upt_rec)
qed auto
lemma zip_eq_butlast_last:
assumes len_gt0: "length xs > 0" and len_eq: "length xs = length ys"
shows "zip xs ys = zip (butlast xs) (butlast ys) @ [(last xs, last ys)]"
using len_eq len_gt0 by (induct rule: list_induct2) auto
subsection ‹Extended Natural Numbers›
lemma the_enat_0[simp]: "the_enat 0 = 0"
by (simp add: zero_enat_def)
lemma the_enat_1[simp]: "the_enat 1 = 1"
by (simp add: one_enat_def)
lemma enat_le_minus_1_imp_lt: "m ≤ n - 1 ⟹ n ≠ ∞ ⟹ n ≠ 0 ⟹ m < n" for m n :: enat
by (cases m; cases n; simp add: zero_enat_def one_enat_def)
lemma enat_diff_diff_eq: "k - m - n = k - (m + n)" for k m n :: enat
by (cases k; cases m; cases n) auto
lemma enat_sub_add_same[intro]: "n ≤ m ⟹ m = m - n + n" for m n :: enat
by (cases m; cases n) auto
lemma enat_the_enat_iden[simp]: "n ≠ ∞ ⟹ enat (the_enat n) = n"
by auto
lemma the_enat_minus_nat: "m ≠ ∞ ⟹ the_enat (m - enat n) = the_enat m - n"
by auto
lemma enat_the_enat_le: "enat (the_enat x) ≤ x"
by (cases x; simp)
lemma enat_the_enat_minus_le: "enat (the_enat (x - y)) ≤ x"
by (cases x; cases y; simp)
lemma enat_le_imp_minus_le: "k ≤ m ⟹ k - n ≤ m" for k m n :: enat
by (metis Groups.add_ac(2) enat_diff_diff_eq enat_ord_simps(3) enat_sub_add_same
enat_the_enat_iden enat_the_enat_minus_le idiff_0_right idiff_infinity idiff_infinity_right
order_trans_rules(23) plus_enat_simps(3))
lemma add_diff_assoc2_enat: "m ≥ n ⟹ m - n + p = m + p - n" for m n p :: enat
by (cases m; cases n; cases p; auto)
lemma enat_mult_minus_distrib: "enat x * (y - z) = enat x * y - enat x * z"
by (cases y; cases z; auto simp: enat_0 right_diff_distrib')
subsection ‹Multisets›
declare
filter_eq_replicate_mset [simp]
image_mset_subseteq_mono [intro]
count_gt_imp_in_mset [intro]
end