Theory Partial_Order_Reduction.Set_Extensions

section ‹Sets›

theory Set_Extensions
imports
  "HOL-Library.Infinite_Set"
begin

  declare finite_subset[intro]

  lemma set_not_emptyI[intro 0]: "x  S  S  {}" by auto
  lemma sets_empty_iffI[intro 0]:
    assumes " a. a  A   b. b  B"
    assumes " b. b  B   a. a  A"
    shows "A = {}  B = {}"
    using assms by auto
  lemma disjointI[intro 0]:
    assumes " x. x  A  x  B  False"
    shows "A  B = {}"
    using assms by auto
  lemma range_subsetI[intro 0]:
    assumes " x. f x  S"
    shows "range f  S"
    using assms by blast

  lemma finite_imageI_range:
    assumes "finite (range f)"
    shows "finite (f ` A)"
    using finite_subset image_mono subset_UNIV assms by metis

  lemma inf_img_fin_domE':
    assumes "infinite A"
    assumes "finite (f ` A)"
    obtains y
    where "y  f ` A" "infinite (A  f -` {y})"
  proof (rule ccontr)
    assume 1: "¬ thesis"
    have 2: "finite ( y  f ` A. A  f -` {y})"
    proof (rule finite_UN_I)
      show "finite (f ` A)" using assms(2) by this
      show " y. y  f ` A  finite (A  f -` {y})" using that 1 by blast
    qed
    have 3: "A  ( y  f ` A. A  f -` {y})" by blast
    show False using assms(1) 2 3 by blast
  qed

  lemma vimage_singleton[simp]: "f -` {y} = {x. f x = y}" unfolding vimage_def by simp

  lemma these_alt_def: "Option.these S = Some -` S" unfolding Option.these_def by force
  lemma the_vimage_subset: "the -` {a}  {None, Some a}" by auto

  lemma finite_induct_reverse[consumes 1, case_names remove]:
    assumes "finite S"
    assumes " S. finite S  ( x. x  S  P (S - {x}))  P S"
    shows "P S"
  using assms(1)
  proof (induct rule: finite_psubset_induct)
    case (psubset S)
    show ?case
    proof (rule assms(2))
      show "finite S" using psubset(1) by this
    next
      fix x
      assume 0: "x  S"
      show "P (S - {x})"
      proof (rule psubset(2))
        show "S - {x}  S" using 0 by auto
      qed
    qed
  qed

  lemma zero_not_in_Suc_image[simp]: "0  Suc ` A" by auto

  lemma Collect_split_Suc:
    "¬ P 0  {i. P i} = Suc ` {i. P (Suc i)}"
    "P 0  {i. P i} = {0}  Suc ` {i. P (Suc i)}"
  proof -
    assume "¬ P 0"
    thus "{i. P i} = Suc ` {i. P (Suc i)}"
      by (auto, metis image_eqI mem_Collect_eq nat.exhaust)
  next
    assume "P 0"
    thus "{i. P i} = {0}  Suc ` {i. P (Suc i)}"
      by (auto, metis imageI mem_Collect_eq not0_implies_Suc)
  qed

  lemma Collect_subsume[simp]:
    assumes " x. x  A  P x"
    shows "{x  A. P x} = A"
    using assms unfolding simp_implies_def by auto

  lemma Max_ge':
    assumes "finite A" "A  {}"
    assumes "b  A" "a  b"
    shows "a  Max A"
    using assms Max_ge_iff by auto

  abbreviation "least A  LEAST k. k  A"

  lemma least_contains[intro?, simp]:
    fixes A :: "'a :: wellorder set"
    assumes "k  A"
    shows "least A  A"
    using assms by (metis LeastI)
  lemma least_contains'[intro?, simp]:
    fixes A :: "'a :: wellorder set"
    assumes "A  {}"
    shows "least A  A"
    using assms by (metis LeastI equals0I)
  lemma least_least[intro?, simp]:
    fixes A :: "'a :: wellorder set"
    assumes "k  A"
    shows "least A  k"
    using assms by (metis Least_le)
  lemma least_unique:
    fixes A :: "'a :: wellorder set"
    assumes "k  A" "k  least A"
    shows "k = least A"
    using assms by (metis Least_le antisym)
  lemma least_not_less:
    fixes A :: "'a :: wellorder set"
    assumes "k < least A"
    shows "k  A"
    using assms by (metis not_less_Least)
  lemma leastI2_order[simp]:
    fixes A :: "'a :: wellorder set"
    assumes "A  {}" " k. k  A  ( l. l  A  k  l)  P k"
    shows "P (least A)"
  proof (rule LeastI2_order)
    show "least A  A" using assms(1) by rule
  next
    fix k
    assume 1: "k  A"
    show "least A  k" using 1 by rule
  next
    fix k
    assume 1: "k  A" " l. l  A  k  l"
    show "P k" using assms(2) 1 by auto
  qed

  lemma least_singleton[simp]:
    fixes a :: "'a :: wellorder"
    shows "least {a} = a"
    by (metis insert_not_empty least_contains' singletonD)

  lemma least_image[simp]:
    fixes f :: "'a :: wellorder  'b :: wellorder"
    assumes "A  {}" " k l. k  A  l  A  k  l  f k  f l"
    shows "least (f ` A) = f (least A)"
  proof (rule leastI2_order)
    show "A  {}" using assms(1) by this
  next
    fix k
    assume 1: "k  A" " i. i  A  k  i"
    show "least (f ` A) = f k"
    proof (rule leastI2_order)
      show "f ` A  {}" using assms(1) by simp
    next
      fix l
      assume 2: "l  f ` A" " i. i  f ` A  l  i"
      show "l = f k" using assms(2) 1 2 by force
    qed
  qed

  lemma least_le:
    fixes A B :: "'a :: wellorder set"
    assumes "B  {}"
    assumes " i. i  least A  i  least B  i  B  i  A"
    shows "least A  least B"
  proof (rule ccontr)
    assume 1: "¬ least A  least B"
    have 2: "least B  A" using assms(1, 2) 1 by simp
    have 3: "least A  least B" using 2 by rule
    show False using 1 3 by rule
  qed
  lemma least_eq:
    fixes A B :: "'a :: wellorder set"
    assumes "A  {}" "B  {}"
    assumes " i. i  least A  i  least B  i  A  i  B"
    shows "least A = least B"
    using assms by (auto intro: antisym least_le)

  lemma least_Suc[simp]:
    assumes "A  {}"
    shows "least (Suc ` A) = Suc (least A)"
  proof (rule antisym)
    obtain k where 10: "k  A" using assms by blast
    have 11: "Suc k  Suc ` A" using 10 by auto
    have 20: "least A  A" using 10 LeastI by metis
    have 21: "least (Suc ` A)  Suc ` A" using 11 LeastI by metis
    have 30: " l. l  A  least A  l" using 10 Least_le by metis
    have 31: " l. l  Suc ` A  least (Suc ` A)  l" using 11 Least_le by metis
    show "least (Suc ` A)  Suc (least A)" using 20 31 by auto
    show "Suc (least A)  least (Suc ` A)" using 21 30 by auto
  qed

  lemma least_Suc_diff[simp]: "Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})"
  proof (cases "A = {}")
    case True
    show ?thesis unfolding True by simp
  next
    case False
    have "Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}" using False by simp
    also have " = Suc ` A - Suc ` {least A}" by simp
    also have " = Suc ` (A - {least A})" by blast
    finally show ?thesis by this
  qed

  lemma Max_diff_least[simp]:
    fixes A :: "'a :: wellorder set"
    assumes "finite A" "A - {least A}  {}"
    shows "Max (A - {least A}) = Max A"
  proof -
    have 1: "least A  A" using assms(2) by auto
    obtain a where 2: "a  A - {least A}" using assms(2) by blast
    have "Max A = Max (insert (least A) (A - {least A}))" using insert_absorb 1 by force
    also have " = max (least A) (Max (A - {least A}))"
    proof (rule Max_insert)
      show "finite (A - {least A})" using assms(1) by auto
      show "A - {least A}  {}" using assms(2) by this
    qed
    also have " = Max (A - {least A})"
    proof (rule max_absorb2, rule Max_ge')
      show "finite (A - {least A})" using assms(1) by auto
      show "A - {least A}  {}" using assms(2) by this
      show "a  A - {least A}" using 2 by this
      show "least A  a" using 2 by simp
    qed
    finally show ?thesis by rule
  qed

  lemma nat_set_card_equality_less:
    fixes A :: "nat set"
    assumes "x  A" "y  A" "card {z  A. z < x} = card {z  A. z < y}"
    shows "x = y"
  proof (cases x y rule: linorder_cases)
    case less
    have 0: "finite {z  A. z < y}" by simp
    have 1: "{z  A. z < x}  {z  A. z < y}" using assms(1, 2) less by force
    have 2: "card {z  A. z < x} < card {z  A. z < y}" using psubset_card_mono 0 1 by this
    show ?thesis using assms(3) 2 by simp
  next
    case equal
    show ?thesis using equal by this
  next
    case greater
    have 0: "finite {z  A. z < x}" by simp
    have 1: "{z  A. z < y}  {z  A. z < x}" using assms(1, 2) greater by force
    have 2: "card {z  A. z < y} < card {z  A. z < x}" using psubset_card_mono 0 1 by this
    show ?thesis using assms(3) 2 by simp
  qed

  lemma nat_set_card_equality_le:
    fixes A :: "nat set"
    assumes "x  A" "y  A" "card {z  A. z  x} = card {z  A. z  y}"
    shows "x = y"
  proof (cases x y rule: linorder_cases)
    case less
    have 0: "finite {z  A. z  y}" by simp
    have 1: "{z  A. z  x}  {z  A. z  y}" using assms(1, 2) less by force
    have 2: "card {z  A. z  x} < card {z  A. z  y}" using psubset_card_mono 0 1 by this
    show ?thesis using assms(3) 2 by simp
  next
    case equal
    show ?thesis using equal by this
  next
    case greater
    have 0: "finite {z  A. z  x}" by simp
    have 1: "{z  A. z  y}  {z  A. z  x}" using assms(1, 2) greater by force
    have 2: "card {z  A. z  y} < card {z  A. z  x}" using psubset_card_mono 0 1 by this
    show ?thesis using assms(3) 2 by simp
  qed

  lemma nat_set_card_mono[simp]:
    fixes A :: "nat set"
    assumes "x  A"
    shows "card {z  A. z < x} < card {z  A. z < y}  x < y"
  proof
    assume 1: "card {z  A. z < x} < card {z  A. z < y}"
    show "x < y"
    proof (rule ccontr)
      assume 2: "¬ x < y"
      have 3: "card {z  A. z < y}  card {z  A. z < x}" using 2 by (auto intro: card_mono)
      show "False" using 1 3 by simp
    qed
  next
    assume 1: "x < y"
    show "card {z  A. z < x} < card {z  A. z < y}"
    proof (intro psubset_card_mono psubsetI)
      show "finite {z  A. z < y}" by simp
      show "{z  A. z < x}  {z  A. z < y}" using 1 by auto
      show "{z  A. z < x}  {z  A. z < y}" using assms 1 by blast
    qed
  qed

  lemma card_one[elim]:
    assumes "card A = 1"
    obtains a
    where "A = {a}"
    using assms by (metis One_nat_def card_Suc_eq)

  lemma image_alt_def: "f ` A = {f x |x. x  A}" by auto

  lemma supset_mono_inductive[mono]:
    assumes " x. x  B  x  C"
    shows "A  B  A  C"
    using assms by auto
  lemma Collect_mono_inductive[mono]:
    assumes " x. P x  Q x"
    shows "x  {x. P x}  x  {x. Q x}"
    using assms by auto

  lemma image_union_split:
    assumes "f ` (A  B) = g ` C"
    obtains D E
    where "f ` A = g ` D" "f ` B = g ` E" "D  C" "E  C"
    using assms unfolding image_Un
    by (metis (erased, lifting) inf_sup_ord(3) inf_sup_ord(4) subset_imageE)
  lemma image_insert_split:
    assumes "inj g" "f ` insert a B = g ` C"
    obtains d E
    where "f a = g d" "f ` B = g ` E" "d  C" "E  C"
  proof -
    have 1: "f ` ({a}  B) = g ` C" using assms(2) by simp
    obtain D E where 2: "f ` {a} = g ` D" "f ` B = g ` E" "D  C" "E  C"
      using image_union_split 1 by this
    obtain d where 3: "D = {d}" using assms(1) 2(1) by (auto, metis (erased, opaque_lifting) imageE
      image_empty image_insert inj_image_eq_iff singletonI)
    show ?thesis using that 2 unfolding 3 by simp
  qed

end