section ‹Constructing Minimal Bad Sequences›
theory Minimal_Bad_Sequences
imports
Almost_Full
Minimal_Elements
begin
text ‹
A locale capturing the construction of minimal bad sequences over values from @{term "A"}. Where
minimality is to be understood w.r.t.\ @{term size} of an element.
›
locale mbs =
fixes A :: "('a :: size) set"
begin
text ‹
Since the @{term size} is a well-founded measure, whenever some element satisfies a property
@{term P}, then there is a size-minimal such element.
›
lemma minimal:
assumes "x ∈ A" and "P x"
shows "∃y ∈ A. size y ≤ size x ∧ P y ∧ (∀z ∈ A. size z < size y ⟶ ¬ P z)"
using assms
proof (induction x taking: size rule: measure_induct)
case (1 x)
then show ?case
proof (cases "∀y ∈ A. size y < size x ⟶ ¬ P y")
case True
with 1 show ?thesis by blast
next
case False
then obtain y where "y ∈ A" and "size y < size x" and "P y" by blast
with "1.IH" show ?thesis by (fastforce elim!: order_trans)
qed
qed
lemma less_not_eq [simp]:
"x ∈ A ⟹ size x < size y ⟹ x = y ⟹ False"
by simp
text ‹
The set of all bad sequences over @{term A}.
›
definition "BAD P = {f ∈ SEQ A. bad P f}"
lemma BAD_iff [iff]:
"f ∈ BAD P ⟷ (∀i. f i ∈ A) ∧ bad P f"
by (auto simp: BAD_def)
text ‹
A partial order on infinite bad sequences.
›
definition geseq :: "((nat ⇒ 'a) × (nat ⇒ 'a)) set"
where
"geseq =
{(f, g). f ∈ SEQ A ∧ g ∈ SEQ A ∧ (f = g ∨ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j)))}"
text ‹
The strict part of the above order.
›
definition gseq :: "((nat ⇒ 'a) × (nat ⇒ 'a)) set" where
"gseq = {(f, g). f ∈ SEQ A ∧ g ∈ SEQ A ∧ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j))}"
lemma geseq_iff:
"(f, g) ∈ geseq ⟷
f ∈ SEQ A ∧ g ∈ SEQ A ∧ (f = g ∨ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j)))"
by (auto simp: geseq_def)
lemma gseq_iff:
"(f, g) ∈ gseq ⟷ f ∈ SEQ A ∧ g ∈ SEQ A ∧ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j))"
by (auto simp: gseq_def)
lemma geseqE:
assumes "(f, g) ∈ geseq"
and "⟦∀i. f i ∈ A; ∀i. g i ∈ A; f = g⟧ ⟹ Q"
and "⋀i. ⟦∀i. f i ∈ A; ∀i. g i ∈ A; size (g i) < size (f i); ∀j < i. f j = g j⟧ ⟹ Q"
shows "Q"
using assms by (auto simp: geseq_iff)
lemma gseqE:
assumes "(f, g) ∈ gseq"
and "⋀i. ⟦∀i. f i ∈ A; ∀i. g i ∈ A; size (g i) < size (f i); ∀j < i. f j = g j⟧ ⟹ Q"
shows "Q"
using assms by (auto simp: gseq_iff)
sublocale min_elt_size?: minimal_element "measure_on size UNIV" A
rewrites "measure_on size UNIV ≡ λx y. size x < size y"
apply (unfold_locales)
apply (auto simp: po_on_def irreflp_on_def transp_on_def simp del: wfp_on_UNIV intro: wfp_on_subset)
apply (auto simp: measure_on_def inv_image_betw_def)
done
context
fixes P :: "'a ⇒ 'a ⇒ bool"
begin
text ‹
A lower bound to all sequences in a set of sequences @{term B}.
›
abbreviation "lb ≡ lexmin (BAD P)"
lemma eq_upto_BAD_mem:
assumes "f ∈ eq_upto (BAD P) g i"
shows "f j ∈ A"
using assms by (auto)
text ‹
Assume that there is some infinite bad sequence @{term h}.
›
context
fixes h :: "nat ⇒ 'a"
assumes BAD_ex: "h ∈ BAD P"
begin
text ‹
When there is a bad sequence, then filtering @{term "BAD P"} w.r.t.~positions in @{term lb} never
yields an empty set of sequences.
›
lemma eq_upto_BAD_non_empty:
"eq_upto (BAD P) lb i ≠ {}"
using eq_upto_lexmin_non_empty [of "BAD P"] and BAD_ex by auto
lemma non_empty_ith:
shows "ith (eq_upto (BAD P) lb i) i ⊆ A"
and "ith (eq_upto (BAD P) lb i) i ≠ {}"
using eq_upto_BAD_non_empty [of i] by auto
lemmas
lb_minimal = min_elt_minimal [OF non_empty_ith, folded lexmin] and
lb_mem = min_elt_mem [OF non_empty_ith, folded lexmin]
text ‹
@{term "lb"} is a infinite bad sequence.
›
lemma lb_BAD:
"lb ∈ BAD P"
proof -
have *: "⋀j. lb j ∈ ith (eq_upto (BAD P) lb j) j" by (rule lb_mem)
then have "∀i. lb i ∈ A" by (auto simp: ith_conv) (metis eq_upto_BAD_mem)
moreover
{ assume "good P lb"
then obtain i j where "i < j" and "P (lb i) (lb j)" by (auto simp: good_def)
from * have "lb j ∈ ith (eq_upto (BAD P) lb j) j" by (auto)
then obtain g where "g ∈ eq_upto (BAD P) lb j" and "g j = lb j" by force
then have "∀k ≤ j. g k = lb k" by (auto simp: order_le_less)
with ‹i < j› and ‹P (lb i) (lb j)› have "P (g i) (g j)" by auto
with ‹i < j› have "good P g" by (auto simp: good_def)
with ‹g ∈ eq_upto (BAD P) lb j› have False by auto }
ultimately show ?thesis by blast
qed
text ‹
There is no infinite bad sequence that is strictly smaller than @{term lb}.
›
lemma lb_lower_bound:
"∀g. (lb, g) ∈ gseq ⟶ g ∉ BAD P"
proof (intro allI impI)
fix g
assume "(lb, g) ∈ gseq"
then obtain i where "g i ∈ A" and "size (g i) < size (lb i)"
and "∀j < i. lb j = g j" by (auto simp: gseq_iff)
moreover with lb_minimal
have "g i ∉ ith (eq_upto (BAD P) lb i) i" by auto
ultimately show "g ∉ BAD P" by blast
qed
text ‹
If there is at least one bad sequence, then there is also a minimal one.
›
lemma lower_bound_ex:
"∃f ∈ BAD P. ∀g. (f, g) ∈ gseq ⟶ g ∉ BAD P"
using lb_BAD and lb_lower_bound by blast
lemma gseq_conv:
"(f, g) ∈ gseq ⟷ f ≠ g ∧ (f, g) ∈ geseq"
by (auto simp: gseq_def geseq_def dest: less_not_eq)
text ‹There is a minimal bad sequence.›
lemma mbs:
"∃f ∈ BAD P. ∀g. (f, g) ∈ gseq ⟶ good P g"
using lower_bound_ex by (auto simp: gseq_conv geseq_iff)
end
end
end
end