Theory SetUtils

theory SetUtils
  imports Main
begin

― ‹TODO use Inf instead of Min where necessary.›

― ‹TODO can be replaced by @{term "card_Un_disjoint (⟦finite A; finite B; A ∩ B = {}⟧ 
  ⟹ card (A ∪ B) = card A + card B)"} ?›
lemma card_union': "(finite s) ∧ (finite t) ∧ (disjnt s t) ⟹ (card (s ∪ t) = card s + card t)"
  by (simp add: card_Un_disjoint disjnt_def)

lemma CARD_INJ_IMAGE_2: 
  fixes f s
  assumes "finite s" "(∀x y. ((x ∈ s) ∧ (y ∈ s)) ⟶ ((f x = f y) ⟷ (x = y)))"
  shows "(card (f ` s) = card s)"
proof -
  {
    fix x y
    assume "x ∈ s" "y ∈ s" 
    then have "f x = f y ⟶ x = y"
      using assms(2)
      by blast
  }
  then have "inj_on f s"
    by (simp add: inj_onI)
  then show ?thesis
    using assms(1) inj_on_iff_eq_card
    by blast
qed

lemma scc_main_lemma_x: "⋀s t x. (x ∈ s) ∧ ¬(x ∈ t) ⟹ ¬(s = t)"
  by blast

lemma neq_funs_neq_images:
  fixes s 
  assumes "∀x. x ∈ s ⟶ (∀y. y ∈ s ⟶ f1 x ≠ f2 y)" "∃x. x ∈ s" 
  shows "f1 ` s ≠ f2 ` s"
  using assms 
  by blast 

subsection "Sets of Numbers"

― ‹TODO 
  Is '<=' natural number lte or overloaded? 
  If it's overloaded for reals, this might be wrong (e.g. the real set s = [0; 1] is not finite even 
though @{term "∀ x ∈ s. x ≤ 1"} holds).›
lemma mems_le_finite_i: 
  fixes s :: "nat set" and k :: nat
  shows "(∀ x. x ∈ s ⟶ x ≤ k) ⟹ finite s"
proof -
  assume P: "(∀ x. x ∈ s ⟶ x ≤ k)"
  let ?f = "id :: nat ⇒ nat"
  let ?S = "{i. i ≤ k}"
  have "s ⊆ ?S" using P by blast
  moreover have "?f ` ?S = ?S" by auto
  moreover have "finite ?S" using nat_seg_image_imp_finite by auto
  moreover have "finite s" using calculation finite_subset by auto
  ultimately show ?thesis by auto
qed
lemma mems_le_finite: 
  fixes s :: "nat set" and k :: nat
  shows "⋀(s :: nat set) k. (∀ x. x ∈ s ⟶ x ≤ k) ⟹ finite s"  
  using mems_le_finite_i by auto

― ‹NOTE translated `s` to `nat set` (more generality wasn't required.).› 
lemma mem_le_imp_MIN_le: 
  fixes s :: "nat set" and k :: nat 
  assumes "∃x. (x ∈ s) ∧ (x ≤ k)" 
  shows "(Inf s ≤ k)" 
proof -
  from assms obtain x where 1: "x ∈ s" "x ≤ k"
    by blast
  {
    assume C: "Inf s > k"
    then have "Inf s > x" using 1(2)
      by fastforce
    then have False 
      using 1(1) cInf_lower leD
      by fast
  }
  then show ?thesis
    by fastforce
qed

― ‹NOTE 
  nat --> bool is the type of a HOL4 set and was translated to 'nat set'.›
― ‹NOTE 
  We cannot use 'Min' instead of 'Inf' because there is no indication that '{n. s n}' will be
finite. Without that @{term "Min {n. s n} ∈ {n. s n}"} is not necessarily true.›
lemma mem_lt_imp_MIN_lt: 
  fixes s :: "nat set" and k :: nat
  assumes "(∃x. x ∈ s ∧ x < k)"
  shows "(Inf s) < k" 
proof -
  obtain x where 1: "x ∈ s" "x < k"
    using assms
    by blast
  then have 2: "s ≠ {}" 
    by blast
  then have "Inf s ∈ s" 
    using Inf_nat_def LeastI
    by force
  moreover have "∀x∈s. Inf s ≤ x"
    by (simp add: cInf_lower)
  ultimately show "(Inf s) < k"
    using assms leD 
    by force
qed

― ‹NOTE type for 'k' had to be fixed (type unordered error; also not true for e.g. real sets).›
lemma bound_child_parent_neq_mems_state_set_neq_len: 
  fixes s and k :: nat
  assumes "(∀x. x ∈ s ⟶ x < k)"
  shows "finite s"
  using assms bounded_nat_set_is_finite 
  by blast 

lemma bound_main_lemma_2: "⋀(s :: nat set) k. (s ≠ {}) ∧ (∀x. x ∈ s ⟶ x ≤ k) ⟹ Sup s ≤ k"
proof -
  fix s :: "nat set" and k
  {
    assume P1: "s ≠ {}"
    assume P2: "(∀x. x ∈ s ⟶ x ≤ k)"
    have "finite s" using P2 mems_le_finite by auto
    moreover have "Max s ∈ s" using P1 calculation Max_in by auto
    moreover have "Max s ≤ k" using P2 calculation by auto 
  }
  then show "(s ≠ {}) ∧ (∀x. x ∈ s ⟶ x ≤ k) ⟹ Sup s ≤ k"
    by (simp add: Sup_nat_def)
qed

― ‹NOTE type of 'k' fixed to nat to be able to use 'bound\_child\_parent\_neq\_mems\_state\_set\_neq\_len'.›
lemma bound_child_parent_not_eq_last_diff_paths: "⋀s (k :: nat).
  (s ≠ {}) 
  ⟹ (∀x. x ∈ s ⟶ x < k) 
  ⟹ Sup s < k
"
  by (simp add: Sup_nat_def bound_child_parent_neq_mems_state_set_neq_len)

lemma FINITE_ALL_DISTINCT_LISTS_i:
  fixes P
  assumes "finite P"
  shows "
    {p. distinct p ∧ set p ⊆ P} 
    = {[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))"
proof -
  let ?A="{p. distinct p ∧ set p ⊆ P }"
  let ?B="{[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))"
  {
    {
      fix a
      assume P: "a ∈ ?A"
      then have "a ∈ ?B" 
      proof (cases a)
        text ‹ The empty list is distinct and its corresponding set is the empty set which is a 
            trivial subset of `?B`. The `Nil` case can therefore be derived by automation. ›
        case (Cons h list)
        {
          let ?b'="h"
          {
            from P have "set a ⊆ P"
              by simp
            then have "set list ⊆ (P - {h})"
              using P dual_order.trans local.Cons 
              by auto
          }
          moreover from P Cons 
          have "distinct list"
            by force
          ultimately have "a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ?b')"
            using Cons
            by blast
          moreover {
            from P Cons have "?b' ∈ set a"
              by simp
            moreover from P have "set a ⊆ P"
              by simp
            ultimately have "?b' ∈ P" 
              by auto
          }
          ultimately have 
            "∃b' ∈ P. a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) b')"
            by meson 
        }
        then obtain b' where
          "b' ∈ P" "a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) b')"
          by blast
        then show ?thesis 
          by blast
      qed blast
    }
    then have "?A ⊆ ?B"
      by auto
  }
  moreover {
    {
      fix b
      assume P: "b ∈ ?B"
      have "b ∈ ?A" 
        text ‹ The empty list is in `?B` by construction. The `Nil` case can therefore be derived  
          straightforwardly.›
      proof (cases b)
        case (Cons a list)
        from P Cons obtain b' where a: 
          "b' ∈ P" "b ∈ {b' # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {b'})}"
          by fast
        then obtain p0 where b: "b = b' # p0" "distinct p0" "set p0 ⊆ (P - {b'})"
          by blast
        then have "distinct (b' # p0)"
          by (simp add: subset_Diff_insert)
        moreover have "set (b' # p0) ⊆ P"
          using a(1) b(3)
          by auto
        ultimately show ?thesis 
          using b(1)
          by fast
      qed simp
    }
    then have "?B ⊆ ?A"
      by blast
  }
  ultimately show ?thesis
    using set_eq_subset 
    by blast
qed

lemma FINITE_ALL_DISTINCT_LISTS:
  fixes P
  assumes "finite P"
  shows "finite {p. distinct p ∧ set p ⊆ P}"
  using assms 
proof (induction "card P" arbitrary: P)
  case 0
  then have "P = {}"
    by force
  then show ?case 
    using 0
    by simp
next
  case (Suc x)
  {
    text ‹ Proof the finiteness of the union by proving both sets of the union are finite. The 
      singleton set `{[]}` is trivially finite. ›
    {
      {
        fix e
        assume P: "e ∈ P" 
        have "
          {e # p0 | p0. distinct p0 ∧ set p0 ⊆ P - {e}} 
          = (λp. e # p) ` { p. distinct p ∧ set p ⊆ P - {e}}" 
          by blast
        moreover {
          let ?P'="P - {e}"
          from Suc.prems 
          have "finite ?P'"
            by blast
          text ‹ The finiteness can now be shown using the induction hypothesis. However `e` might
            already be contained in `?P`, so we have to split cases first. ›
          have "finite ((λp. e # p) ` {p. distinct p ∧ set p ⊆ ?P'})" 
          proof (cases "e ∈ P")
            case True
            then have "x = card ?P'" using Suc.prems Suc(2) 
              by fastforce
            moreover from Suc.prems 
            have "finite ?P'" 
              by blast
            ultimately show ?thesis 
              using Suc(1) 
              by blast
          next
            case False
            then have "?P' = P" 
              by simp
            then have "finite {p. distinct p ∧ set p ⊆ ?P'}"
              using False P by linarith 
            then show ?thesis
              using finite_imageI
              by blast
          qed
        }
        ultimately have "finite {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}"
          by argo
      }
      then have "finite (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))"
        using Suc.prems
        by blast
    }
    then have 
      "finite ({[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P)))" 
      using finite_Un
      by blast    
  }
  then show ?case 
    using FINITE_ALL_DISTINCT_LISTS_i[OF Suc.prems]
    by force
qed

lemma subset_inter_diff_empty: 
  assumes "s ⊆ t" 
  shows "(s ∩ (u - t) = {})" 
  using assms
  by auto

end