Theory Nash_Williams.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  xA. yB. 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