Theory Lower_Set
theory Lower_Set
imports Main
begin
definition is_lower_set_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a set ⇒ bool" where
"transp_on X R ⟹ asymp_on X R ⟹
is_lower_set_wrt R L X ⟷ L ⊆ X ∧ (∀l ∈ L. ∀x ∈ X. R x l ⟶ x ∈ L)"
definition is_strict_lower_set_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a set ⇒ bool" where
"transp_on X R ⟹ asymp_on X R ⟹
is_strict_lower_set_wrt R L X ⟷ L ⊂ X ∧ (∀l ∈ L. ∀x ∈ X. R x l ⟶ x ∈ L)"
lemma is_lower_set_wrt_empty:
fixes X :: "'a set" and R :: "'a ⇒ 'a ⇒ bool"
assumes "transp_on X R" and "asymp_on X R"
shows "is_lower_set_wrt R {} X"
unfolding is_lower_set_wrt_def[OF assms] by simp
lemma is_lower_set_wrt_refl:
fixes X :: "'a set" and R :: "'a ⇒ 'a ⇒ bool"
assumes "transp_on X R" and "asymp_on X R"
shows "is_lower_set_wrt R X X"
unfolding is_lower_set_wrt_def[OF assms] by simp
lemma is_lower_set_wrt_trans:
fixes X Y Z :: "'a set" and R :: "'a ⇒ 'a ⇒ bool"
assumes
"transp_on Z R" and "asymp_on Z R" and
"is_lower_set_wrt R X Y" and "is_lower_set_wrt R Y Z"
shows "is_lower_set_wrt R X Z"
proof -
have "Y ⊆ Z" and Y_lower: "∀l∈Y. ∀x∈Z. R x l ⟶ x ∈ Y"
using ‹is_lower_set_wrt R Y Z›
unfolding is_lower_set_wrt_def[OF ‹transp_on Z R› ‹asymp_on Z R›]
unfolding atomize_conj .
have "transp_on Y R" and "asymp_on Y R"
unfolding atomize_conj
using ‹transp_on Z R› ‹asymp_on Z R› ‹Y ⊆ Z›
by (metis asymp_on_subset transp_on_subset)
have "X ⊆ Y" and X_lower: "∀l∈X. ∀x∈Y. R x l ⟶ x ∈ X"
using ‹is_lower_set_wrt R X Y›
unfolding is_lower_set_wrt_def[OF ‹transp_on Y R› ‹asymp_on Y R›]
unfolding atomize_conj .
have "X ⊆ Z"
using ‹X ⊆ Y› ‹Y ⊆ Z› by order
moreover have "(∀l∈X. ∀x∈Z. R x l ⟶ x ∈ X)"
using ‹X ⊆ Y› X_lower Y_lower by blast
ultimately show ?thesis
unfolding is_lower_set_wrt_def[OF ‹transp_on Z R› ‹asymp_on Z R›] ..
qed
lemma is_lower_set_wrt_antisym:
fixes X Y :: "'a set" and R :: "'a ⇒ 'a ⇒ bool"
assumes
"transp_on Y R" and "asymp_on Y R" and
"is_lower_set_wrt R X Y" and "is_lower_set_wrt R Y X"
shows "X = Y"
proof -
have "X ⊆ Y"
using ‹is_lower_set_wrt R X Y›
unfolding is_lower_set_wrt_def[OF ‹transp_on Y R› ‹asymp_on Y R›] ..
have "transp_on X R" and "asymp_on X R"
unfolding atomize_conj
using ‹transp_on Y R› ‹asymp_on Y R› ‹X ⊆ Y›
by (metis asymp_on_subset transp_on_subset)
have "Y ⊆ X"
using ‹is_lower_set_wrt R Y X›
unfolding is_lower_set_wrt_def[OF ‹transp_on X R› ‹asymp_on X R›] ..
show "X = Y"
using ‹X ⊆ Y› ‹Y ⊆ X› by (metis subset_antisym)
qed
lemma order_is_lower_set_wrt:
fixes R :: "'a ⇒ 'a ⇒ bool"
assumes "transp R" and "asymp R"
shows "class.order (is_lower_set_wrt R) (is_strict_lower_set_wrt R)"
proof unfold_locales
have trans: "⋀A. transp_on A R"
using ‹transp R› by (metis subset_UNIV transp_on_subset)
have asym: "⋀A. asymp_on A R"
using ‹asymp R› by (metis subset_UNIV asymp_on_subset)
show "⋀x y. is_strict_lower_set_wrt R x y = (is_lower_set_wrt R x y ∧ ¬ is_lower_set_wrt R y x)"
unfolding is_lower_set_wrt_def[OF trans asym]
unfolding is_strict_lower_set_wrt_def[OF trans asym]
by (metis order_le_less subset_not_subset_eq)
show "⋀x. is_lower_set_wrt R x x"
using is_lower_set_wrt_refl[OF trans asym] .
show "⋀x y z. is_lower_set_wrt R x y ⟹ is_lower_set_wrt R y z ⟹ is_lower_set_wrt R x z"
using is_lower_set_wrt_trans[OF trans asym] .
show "⋀x y. is_lower_set_wrt R x y ⟹ is_lower_set_wrt R y x ⟹ x = y"
using is_lower_set_wrt_antisym[OF trans asym] .
qed
lemma is_lower_set_wrt_insertI:
assumes "transp_on (insert x X) R" and "asymp_on (insert x X) R" and
"x ∈ X" and "∀w ∈ X. R w x ⟶ w ∈ L" and "is_lower_set_wrt R L X"
shows "is_lower_set_wrt R (insert x L) X"
proof -
have "transp_on X R" and "asymp_on X R"
unfolding atomize_conj
using ‹transp_on (insert x X) R› ‹asymp_on (insert x X) R›
by (metis asymp_on_subset subset_insertI transp_on_subset)
have "is_lower_set_wrt R (insert x L) X ⟷
insert x L ⊆ X ∧ (∀l∈insert x L. ∀xa∈X. R xa l ⟶ xa ∈ insert x L)"
unfolding is_lower_set_wrt_def[OF ‹transp_on X R› ‹asymp_on X R›] ..
also have "… ⟷ x ∈ X ∧ L ⊆ X ∧ (∀l∈insert x L. ∀xa∈X. R xa l ⟶ xa ∈ insert x L)"
by simp
also have "… ⟷ x ∈ X ∧ L ⊆ X ∧ (∀w∈X. R w x ⟶ w ∈ insert x L) ∧
(∀l∈L. ∀xa∈X. R xa l ⟶ xa ∈ insert x L)"
by simp
also have "… ⟷ x ∈ X ∧ L ⊆ X ∧ (∀w∈X. R w x ⟶ w ∈ L) ∧
(∀l∈L. ∀y∈X. R y l ⟶ y ∈ insert x L)"
using ‹asymp_on (insert x X) R› by (smt (verit) asymp_onD insertCI insertE)
also have "… ⟷ x ∈ X ∧ (∀w∈X. R w x ⟶ w ∈ L) ∧ is_lower_set_wrt R L X"
using ‹is_lower_set_wrt R L X›
unfolding is_lower_set_wrt_def[OF ‹transp_on X R› ‹asymp_on X R›]
by blast
finally show ?thesis
using assms(3-) by argo
qed
lemma lower_set_wrt_appendI:
assumes
trans: "transp_on (set (xs @ ys)) R" and
asym: "asymp_on (set (xs @ ys)) R" and
sorted: "sorted_wrt R (xs @ ys)"
shows "is_lower_set_wrt R (set xs) (set (xs @ ys))"
unfolding is_lower_set_wrt_def[OF trans asym]
proof (intro conjI)
show "set xs ⊆ set (xs @ ys)"
by simp
next
show "∀l∈set xs. ∀x∈set (xs @ ys). R x l ⟶ x ∈ set xs"
using sorted
by (metis Un_iff asym asymp_on_def set_append sorted_wrt_append)
qed
lemma sorted_and_lower_set_wrt_appendD_left:
assumes "transp_on A R" and "asymp_on A R" and
"sorted_wrt R (xs @ ys)" and "is_lower_set_wrt R (set (xs @ ys)) A"
shows "sorted_wrt R xs" and "is_lower_set_wrt R (set xs) A"
unfolding atomize_conj
using assms
by (smt (verit) Un_iff asymp_on_def is_lower_set_wrt_def le_sup_iff set_append sorted_wrt_append
subsetD)
lemma sorted_and_lower_set_wrt_appendD_right:
assumes "transp_on A R" and "asymp_on A R" and
"sorted_wrt (λx y. R y x) (xs @ ys)" and "is_lower_set_wrt R (set (xs @ ys)) A"
shows "sorted_wrt (λx y. R y x) ys" and "is_lower_set_wrt R (set ys) A"
unfolding atomize_conj
using assms
by (smt (verit, ccfv_threshold) Un_iff asymp_onD is_lower_set_wrt_def le_sup_iff set_append
sorted_wrt_append subsetD)
lemma not_in_lower_set_wrtI:
fixes R :: "'a ⇒ 'a ⇒ bool"
assumes trans: "transp_on Y R" and asym: "asymp_on Y R"
shows "is_lower_set_wrt R X Y ⟹ y ∉ X ⟹ y ∈ Y ⟹ R y z ⟹ z ∉ X"
unfolding is_lower_set_wrt_def[OF trans asym]
by blast
abbreviation (in preorder) is_lower_set where
"is_lower_set ≡ is_lower_set_wrt (<)"
lemmas (in preorder) is_lower_set_iff =
is_lower_set_wrt_def[OF transp_on_less asymp_on_less]
context linorder begin