Theory Infinite_Chain
section ‹Infinite (Non-Well-Founded) Chains›
theory Infinite_Chain
imports Lambda_Free_Util
begin
text ‹
This theory defines the concept of a minimal bad (or non-well-founded)
infinite chain, as found in the term rewriting literature to prove the
well-foundedness of syntactic term orders.
›
context
fixes p :: "'a ⇒ 'a ⇒ bool"
begin
definition inf_chain :: "(nat ⇒ 'a) ⇒ bool" where
"inf_chain f ⟷ (∀i. p (f i) (f (Suc i)))"
lemma wfP_iff_no_inf_chain: "wfP (λx y. p y x) ⟷ (∄f. inf_chain f)"
unfolding wfP_def wf_iff_no_infinite_down_chain inf_chain_def by simp
lemma inf_chain_offset: "inf_chain f ⟹ inf_chain (λj. f (j + i))"
unfolding inf_chain_def by simp
definition bad :: "'a ⇒ bool" where
"bad x ⟷ (∃f. inf_chain f ∧ f 0 = x)"
lemma inf_chain_bad:
assumes bad_f: "inf_chain f"
shows "bad (f i)"
unfolding bad_def by (rule exI[of _ "λj. f (j + i)"]) (simp add: inf_chain_offset[OF bad_f])
context
fixes gt :: "'a ⇒ 'a ⇒ bool"
assumes wf: "wf {(x, y). gt y x}"
begin
primrec worst_chain :: "nat ⇒ 'a" where
"worst_chain 0 = (SOME x. bad x ∧ (∀y. bad y ⟶ ¬ gt x y))"
| "worst_chain (Suc i) = (SOME x. bad x ∧ p (worst_chain i) x ∧
(∀y. bad y ∧ p (worst_chain i) y ⟶ ¬ gt x y))"
declare worst_chain.simps[simp del]
context
fixes x :: 'a
assumes x_bad: "bad x"
begin
lemma
bad_worst_chain_0: "bad (worst_chain 0)" and
min_worst_chain_0: "¬ gt (worst_chain 0) x"
proof -
obtain y where "bad y ∧ (∀z. bad z ⟶ ¬ gt y z)"
using wf_exists_minimal[OF wf, of bad, OF x_bad] by force
hence "bad (worst_chain 0) ∧ (∀z. bad z ⟶ ¬ gt (worst_chain 0) z)"
unfolding worst_chain.simps by (rule someI)
thus "bad (worst_chain 0)" and "¬ gt (worst_chain 0) x"
using x_bad by blast+
qed
lemma
bad_worst_chain_Suc: "bad (worst_chain (Suc i))" and
worst_chain_pred: "p (worst_chain i) (worst_chain (Suc i))" and
min_worst_chain_Suc: "p (worst_chain i) x ⟹ ¬ gt (worst_chain (Suc i)) x"
proof (induct i rule: less_induct)
case (less i)
have "bad (worst_chain i)"
proof (cases i)
case 0
thus ?thesis
using bad_worst_chain_0 by simp
next
case (Suc j)
thus ?thesis
using less(1) by blast
qed
then obtain fa where fa_bad: "inf_chain fa" and fa_0: "fa 0 = worst_chain i"
unfolding bad_def by blast
have "∃s0. bad s0 ∧ p (worst_chain i) s0"
proof (intro exI conjI)
let ?y0 = "fa (Suc 0)"
show "bad ?y0"
unfolding bad_def by (auto intro: exI[of _ "λi. fa (Suc i)"] inf_chain_offset[OF fa_bad])
show "p (worst_chain i) ?y0"
using fa_bad[unfolded inf_chain_def] fa_0 by metis
qed
then obtain y0 where y0: "bad y0 ∧ p (worst_chain i) y0"
by blast
obtain y1 where
y1: "bad y1 ∧ p (worst_chain i) y1 ∧ (∀z. bad z ∧ p (worst_chain i) z ⟶ ¬ gt y1 z)"
using wf_exists_minimal[OF wf, of "λy. bad y ∧ p (worst_chain i) y", OF y0] by force
let ?y = "worst_chain (Suc i)"
have conj: "bad ?y ∧ p (worst_chain i) ?y ∧ (∀z. bad z ∧ p (worst_chain i) z ⟶ ¬ gt ?y z)"
unfolding worst_chain.simps using y1 by (rule someI)
show "bad ?y"
by (rule conj[THEN conjunct1])
show "p (worst_chain i) ?y"
by (rule conj[THEN conjunct2, THEN conjunct1])
show "p (worst_chain i) x ⟹ ¬ gt ?y x"
using x_bad conj[THEN conjunct2, THEN conjunct2, rule_format] by meson
qed
lemma bad_worst_chain: "bad (worst_chain i)"
by (cases i) (auto intro: bad_worst_chain_0 bad_worst_chain_Suc)
lemma worst_chain_bad: "inf_chain worst_chain"
unfolding inf_chain_def using worst_chain_pred by metis
end
context
fixes x :: 'a
assumes
x_bad: "bad x" and
p_trans: "⋀z y x. p z y ⟹ p y x ⟹ p z x"
begin
lemma worst_chain_not_gt: "¬ gt (worst_chain i) (worst_chain (Suc i))" for i
proof (cases i)
case 0
show ?thesis
unfolding 0 by (rule min_worst_chain_0[OF inf_chain_bad[OF worst_chain_bad[OF x_bad]]])
next
case Suc
show ?thesis
unfolding Suc
by (rule min_worst_chain_Suc[OF inf_chain_bad[OF worst_chain_bad[OF x_bad]]])
(rule p_trans[OF worst_chain_pred[OF x_bad] worst_chain_pred[OF x_bad]])
qed
end
end
end
lemma inf_chain_subset: "inf_chain p f ⟹ p ≤ q ⟹ inf_chain q f"
unfolding inf_chain_def by blast
hide_fact (open) bad_worst_chain_0 bad_worst_chain_Suc
end