(*
 * Finite Set lemmas.
 * (C)opyright Peter Gammie, peteg42 at gmail.com, commenced July 2006.
 * License: BSD
 *)

(*<*)
theory FSext

imports Main

begin
(*>*)

(* **************************************** *)

section‹General Lemmas›

subsection‹Extra Finite-Set Lemmas›

text‹Small variant of @{thm [source] "Finite_Set.finite_subset_induct"}:
  assume @{term "F ⊆ A"} in the induction hypothesis.›

lemma finite_subset_induct' [consumes 2, case_names empty insert]:
  assumes "finite F" and "F ⊆ A"
    and empty: "P {}"
    and insert: "∧a F. [finite F; a ∈ A; F ⊆ A; a ∉ F; P F ] ==> P (insert a F)"
  shows "P F"
proof -
  from ‹finite F›
  have "F ⊆ A ==> ?thesis"
  proof induct
    show "P {}" by fact
  next
    fix x F
    assume "finite F" and "x ∉ F" and
      P: "F ⊆ A ==> P F" and i: "insert x F ⊆ A"
    show "P (insert x F)"
    proof (rule insert)
      from i show "x ∈ A" by blast
      from i have "F ⊆ A" by blast
      with P show "P F" .
      show "finite F" by fact
      show "x ∉ F" by fact
      show "F ⊆ A" by fact
    qed
  qed
  with ‹F ⊆ A› show ?thesis by blast
qed

text‹A slight improvement on @{thm [source] "List.finite_list"} - add
 {term "distinct"}.›

lemma finite_list: "finite A ==> ∃l. set l = A ∧ distinct l"
proof(induct rule: finite_induct)
  case (insert x F)
  then obtain l where "set l = F ∧ distinct l" by auto
  with insert have "set (x#l) = insert x F ∧ distinct (x#l)" by auto
  thus ?case by blast
qed auto

subsection‹Extra bijection lemmas›

lemma bij_betw_onto: "bij_betw f A B ==> f ` A = B" unfolding bij_betw_def by simp

lemma inj_on_UnI: "[ inj_on f A; inj_on f B; f ` (A - B) ∩ f ` (B - A) = {} ] ==> inj_on f (A ∪ B)"
  by (auto iff: inj_on_Un)

lemma card_compose_bij:
  assumes bijf: "bij_betw f A A"
  shows "card { a ∈ A. P (f a) } = card { a ∈ A. P a }"
proof -
  from bijf have T: "f ` { a ∈ A. P (f a) } = { a ∈ A. P a }"
    unfolding bij_betw_def by auto
  from bijf have "card { a ∈ A. P (f a) } = card (f ` { a ∈ A. P (f a) })"
    unfolding bij_betw_def by (auto intro: inj_on_subset card_image[symmetric])
  with T show ?thesis by simp
qed

lemma card_eq_bij:
  assumes cardAB: "card A = card B"
      and finiteA: "finite A" and finiteB: "finite B"
  obtains f where "bij_betw f A B"
proof -
  from finiteA obtain g where G: "bij_betw g A {0..<card A}"
    by (blast dest: ex_bij_betw_finite_nat)
  from finiteB obtain h where H: "bij_betw h {0..<card B} B"
    by (blast dest: ex_bij_betw_nat_finite)
  from G H cardAB have I: "inj_on (h ∘ g) A"
    unfolding bij_betw_def by - (rule comp_inj_on, simp_all)
  from G H cardAB have "(h ∘ g) ` A = B"
    unfolding bij_betw_def by auto (metis image_cong image_image)
  with I have "bij_betw (h ∘ g) A B"
    unfolding bij_betw_def by blast
  thus thesis ..
qed

lemma bij_combine:
  assumes ABCD: "A ⊆ B" "C ⊆ D"
      and bijf: "bij_betw f A C"
      and bijg: "bij_betw g (B - A) (D - C)"
  obtains h
    where "bij_betw h B D"
      and "∧x. x ∈ A ==> h x = f x"
      and "∧x. x ∈ B - A ==> h x = g x" 
proof -
  let ?h = "λx. if x ∈ A then f x else g x"
  have "inj_on ?h (A ∪ (B - A))"
  proof(rule inj_on_UnI)
    from bijf show "inj_on ?h A"
      by - (rule inj_onI, auto dest: inj_onD bij_betw_imp_inj_on)
    from bijg show "inj_on ?h (B - A)"
      by - (rule inj_onI, auto dest: inj_onD bij_betw_imp_inj_on)
    from bijf bijg show "?h ` (A - (B - A)) ∩ ?h ` (B - A - A) = {}"
      by (simp, blast dest: bij_betw_onto)
  qed
  with ABCD have "inj_on ?h B" by (auto iff: Un_absorb1)
  moreover
  have "?h ` B = D"
  proof -
    from ABCD have "?h ` B = f ` A ∪ g ` (B - A)" by (auto iff: image_Un Un_absorb1)
    also from ABCD bijf bijg have "… = D" by (blast dest: bij_betw_onto)
    finally show ?thesis .
  qed
  ultimately have "bij_betw ?h B D"
              and "∧x. x ∈ A ==> ?h x = f x"
              and "∧x. x ∈ B - A ==> ?h x = g x"
    unfolding bij_betw_def by auto
  thus thesis ..
qed

lemma bij_complete:
  assumes finiteC: "finite C"
      and ABC: "A ⊆ C" "B ⊆ C"
      and bijf: "bij_betw f A B"
  obtains f' where "bij_betw f' C C"
      and "∧x. x ∈ A ==> f' x = f x"
      and "∧x. x ∈ C - A ==> f' x ∈ C - B"
proof -
  from finiteC ABC bijf have "card B = card A"
    unfolding bij_betw_def
    by (auto iff: inj_on_iff_eq_card [symmetric] intro: finite_subset)
  with finiteC ABC bijf have "card (C - A) = card (C - B)"
    by (auto iff: finite_subset card_Diff_subset)
  with finiteC obtain g where bijg: "bij_betw g (C - A) (C - B)"
    by - (drule card_eq_bij, auto)
  from ABC bijf bijg
  obtain f' where bijf': "bij_betw f' C C"
              and f'f: "∧x. x ∈ A ==> f' x = f x"
              and f'g: "∧x. x ∈ C - A ==> f' x = g x"
    by - (drule bij_combine, auto)
  from f'g bijg have "∧x. x ∈ C - A ==> f' x ∈ C - B"
    by (blast dest: bij_betw_onto)
  with bijf' f'f show thesis ..
qed

lemma card_greater:
  assumes finiteA: "finite A"
      and c: "card { x ∈ A. P x } > card { x ∈ A. Q x }"
  obtains C
    where "card ({ x ∈ A. P x } - C) = card { x ∈ A. Q x }"
      and "C ≠ {}"
      and "C ⊆ { x ∈ A. P x }"
proof -
  let ?PA = "{ x ∈ A . P x }"
  let ?QA = "{ x ∈ A . Q x }"
  from finiteA obtain p where P: "bij_betw p {0..<card ?PA} ?PA"
    using ex_bij_betw_nat_finite[where M="?PA"]
    by (blast intro: finite_subset)
  let ?CN = "{card ?QA..<card ?PA}"
  let ?C = "p ` ?CN"
  have "card ({ x ∈ A. P x } - ?C) = card ?QA"
  proof -
    have nat_add_sub_shuffle: "∧x y z. [ (x::nat) > y; x - y = z ] ==> x - z = y" by simp
    from P have T: "p ` {card ?QA..<card ?PA} ⊆ ?PA"
      unfolding bij_betw_def by auto
    from P have "card ?PA - card ?QA = card ?C"
      unfolding bij_betw_def
      by (auto iff: card_image inj_on_subset[where B="?CN"])
    with c have "card ?PA - card ?C = card ?QA" by (rule nat_add_sub_shuffle)
    with finiteA P T have "card (?PA - ?C) = card ?QA"
      unfolding bij_betw_def by (auto iff: finite_subset card_Diff_subset)
    thus ?thesis .
  qed
  moreover
  from P c have "?C ≠ {}"
    unfolding bij_betw_def by auto
  moreover
  from P have "?C ⊆ { x ∈ A. P x }"
    unfolding bij_betw_def by auto
  ultimately show thesis ..
qed

subsection‹Collections of witnesses: @{term "hasw"}, @{term "has"}›

text ‹

  a set of cardinality at least $n$, we can find up to $n$ distinct
 . The built-in @{term "card"} function unfortunately satisfies:

 begin{center}
 @{thm [source] "Finite_Set.card.infinite"}: @{thm "Finite_Set.card.infinite"
 [no_vars]}
 end{center}

  lemmas handle the infinite case uniformly.

  to Gerwin Klein suggesting this approach.

 ›

definition hasw :: "'a list → 'a set → bool" where
  "hasw xs S ≡ set xs ⊆ S ∧ distinct xs"

definition has :: "nat → 'a set → bool" where
  "has n S ≡ ∃xs. hasw xs S ∧ length xs = n"

declare hasw_def[simp]

lemma hasI[intro]: "hasw xs S ==> has (length xs) S" by (unfold has_def, auto)

lemma card_has:
  assumes cardS: "card S = n"
  shows "has n S"
proof(cases "n = 0")
  case True thus ?thesis by (simp add: has_def)
next
  case False
  with cardS card_eq_0_iff[where A=S] have finiteS: "finite S" by simp
  show ?thesis
  proof(rule ccontr)
    assume nhas: "¬ has n S"
    with distinct_card[symmetric]
    have nxs: "¬ (∃ xs. set xs ⊆ S ∧ distinct xs ∧ card (set xs) = n)"
      by (auto simp add: has_def)
    from finite_list finiteS
    obtain xs where "S = set xs" by blast
    with cardS nxs show False by auto
  qed
qed

lemma card_has_rev:
  assumes finiteS: "finite S"
  shows "has n S ==> card S ≥ n" (is "?lhs ==> ?rhs")
proof -
  assume ?lhs
  then obtain xs
    where "set xs ⊆ S ∧ n = length xs"
      and dxs: "distinct xs" by (unfold has_def hasw_def, blast)
  with card_mono[OF finiteS] distinct_card[OF dxs, symmetric]
  show ?rhs by simp
qed

lemma has_0: "has 0 S" by (simp add: has_def)

lemma has_suc_notempty: "has (Suc n) S ==> {} ≠ S"
  by (clarsimp simp add: has_def)

lemma has_suc_subset: "has (Suc n) S ==> {} ⊂ S"
  by (rule psubsetI, (simp add: has_suc_notempty)+)

lemma has_notempty_1:
  assumes Sne: "S ≠ {}"
  shows "has 1 S"
proof -
  from Sne obtain x where "x ∈ S" by blast
  hence "set [x] ⊆ S ∧ distinct [x] ∧ length [x] = 1" by auto
  thus ?thesis by (unfold has_def hasw_def, blast)
qed

lemma has_le_has:
  assumes h: "has n S"
      and nn': "n' ≤ n"
  shows "has n' S"
proof -
  from h obtain xs where "hasw xs S" "length xs = n" by (unfold has_def, blast)
  with nn' set_take_subset[where n="n'" and xs="xs"]
  have "hasw (take n' xs) S" "length (take n' xs) = n'"
    by (simp_all add: min_def, blast+)
  thus ?thesis by (unfold has_def, blast)
qed

lemma has_ge_has_not:
  assumes h: "¬has n S"
      and nn': "n ≤ n'"
  shows "¬has n' S"
  using h nn' by (blast dest: has_le_has)

lemma has_eq:
  assumes h: "has n S"
      and hn': "¬has (Suc n) S"
  shows "card S = n"
proof -
  from h obtain xs
    where xs: "hasw xs S" and lenxs: "length xs = n" by (unfold has_def, blast)
  have "set xs = S"
  proof
    from xs show "set xs ⊆ S" by simp
  next
    show "S ⊆ set xs"
    proof(rule ccontr)
      assume "¬ S ⊆ set xs"
      then obtain x where "x ∈ S" "x ∉ set xs" by blast
      with lenxs xs have "hasw (x # xs) S" "length (x # xs) = Suc n" by simp_all
      with hn' show False by (unfold has_def, blast)
    qed
  qed
  with xs lenxs distinct_card show "card S = n" by auto
qed

lemma has_extend_witness:
  assumes h: "has n S"
  shows "[ set xs ⊆ S; length xs < n ] ==> set xs ⊂ S"
proof(induct xs)
  case Nil
  with h has_suc_notempty show ?case by (cases n, auto)
next
  case (Cons x xs)
  have "set (x # xs) ≠ S"
  proof
    assume Sxxs: "set (x # xs) = S"
    hence finiteS: "finite S" by auto
    from h obtain xs'
      where Sxs': "set xs' ⊆ S"
        and dlxs': "distinct xs' ∧ length xs' = n"
      by (unfold has_def hasw_def, blast)
    with distinct_card have "card (set xs') = n" by auto
    with finiteS Sxs' card_mono have "card S ≥ n" by auto
    moreover
    from Sxxs Cons card_length[where xs="x # xs"]
    have "card S < n" by auto
    ultimately show False by simp
  qed
  with Cons show ?case by auto
qed

lemma has_extend_witness':
  "[ has n S; hasw xs S; length xs < n ] ==> ∃x. hasw (x # xs) S"
  by (simp, blast dest: has_extend_witness)

lemma has_witness_two:
  assumes hasnS: "has n S"
      and nn': "2 ≤ n"
  shows "∃x y. hasw [x,y] S"
proof -
  have has2S: "has 2 S" by (rule has_le_has[OF hasnS nn'])
  from has_extend_witness'[OF has2S, where xs="[]"]
  obtain x where "x ∈ S" by auto
  with has_extend_witness'[OF has2S, where xs="[x]"]
  show ?thesis by auto
qed

lemma has_witness_three:
  assumes hasnS: "has n S"
      and nn': "3 ≤ n"
  shows "∃x y z. hasw [x,y,z] S"
proof -
  from nn' obtain x y where "hasw [x,y] S"
    using has_witness_two[OF hasnS] by auto
  with nn' show ?thesis
    using has_extend_witness'[OF hasnS, where xs="[x,y]"] by auto
qed

lemma finite_set_singleton_contra:
  assumes finiteS: "finite S"
      and Sne: "S ≠ {}"
      and cardS: "card S > 1 ==> False"
  shows "∃j. S = {j}"
proof -
  from cardS Sne card_0_eq[OF finiteS] have Scard: "card S = 1" by auto
  from has_extend_witness[where xs="[]", OF card_has[OF this]]
  obtain j where "{j} ⊆ S" by auto
  from card_seteq[OF finiteS this] Scard show ?thesis by auto
qed

(*<*)
end
(*>*)