Theory Nash_Extras

section ‹The Pointwise Less-Than Relation Between Two Sets›

theory Nash_Extras
  imports "HOL-Library.Ramsey" "HOL-Library.Countable_Set"

begin

definition less_sets :: "['a::order set, 'a::order set] ⇒ bool" (infixr "≪" 50)
    where "A ≪ B ≡ ∀x∈A. ∀y∈B. x < y"

lemma less_sets_empty[iff]: "S ≪ {}" "{} ≪ T"
  by (auto simp: less_sets_def)

lemma less_setsD: "⟦A ≪ B; a ∈ A; b ∈ B⟧ ⟹ a < b"
  by (auto simp: less_sets_def)

lemma less_sets_irrefl [simp]: "A ≪ A ⟷ A = {}"
  by (auto simp: less_sets_def)

lemma less_sets_trans: "⟦A ≪ B; B ≪ C; B ≠ {}⟧ ⟹ A ≪ C"
  unfolding less_sets_def using less_trans by blast

lemma less_sets_weaken1: "⟦A' ≪ B; A ⊆ A'⟧ ⟹ A ≪ B"
  by (auto simp: less_sets_def)

lemma less_sets_weaken2: "⟦A ≪ B'; B ⊆ B'⟧ ⟹ A ≪ B"
  by (auto simp: less_sets_def)

lemma less_sets_imp_disjnt: "A ≪ B ⟹ disjnt A B"
  by (auto simp: less_sets_def disjnt_def)

lemma less_sets_UN1: "less_sets (⋃𝒜) B ⟷ (∀A∈𝒜. A ≪ B)"
  by (auto simp: less_sets_def)

lemma less_sets_UN2: "less_sets A (⋃ ℬ) ⟷ (∀B∈ℬ. A ≪ B)"
  by (auto simp: less_sets_def)

lemma less_sets_Un1: "less_sets (A ∪ A') B ⟷ A ≪ B ∧ A' ≪ B"
  by (auto simp: less_sets_def)

lemma less_sets_Un2: "less_sets A (B ∪ B') ⟷ A ≪ B ∧ A ≪ B'"
  by (auto simp: less_sets_def)

lemma strict_sorted_imp_less_sets:
  "strict_sorted (as @ bs) ⟹ (list.set as) ≪ (list.set bs)"
  by (simp add: less_sets_def sorted_wrt_append)

lemma Sup_nat_less_sets_singleton:
  fixes n::nat
  assumes "Sup T < n" "finite T"
  shows "less_sets T {n}"
  using assms Max_less_iff
  by (auto simp: Sup_nat_def less_sets_def split: if_split_asm)
  
end