Theory Set_Thms

(*
  File: Set_Thms.thy
  Author: Bohua Zhan

  Setup of proof steps related to sets.
*)

section ‹Setup for sets and multisets›

theory Set_Thms
imports Logic_Thms "HOL-Library.Multiset"
begin

subsection ‹Set›

subsubsection ‹Injective functions›

setup ‹add_backward_prfstep @{thm injI}›

subsubsection ‹AC property of intersection and union›

setup ‹fold Auto2_HOL_Extra_Setup.ACUtil.add_ac_data [
  {cfhead = @{cterm inf}, unit = SOME @{cterm inf},
   assoc_th = @{thm inf_assoc}, comm_th = @{thm inf_commute},
   unitl_th = @{thm inf_top_left}, unitr_th = @{thm inf_top_right}},

  {cfhead = @{cterm sup}, unit = SOME @{cterm bot},
   assoc_th = @{thm sup_assoc}, comm_th = @{thm sup_commute},
   unitl_th = @{thm sup_bot_left}, unitr_th = @{thm sup_bot_right}}]
›

subsubsection ‹Collection and bounded quantification›

setup ‹add_rewrite_rule @{thm Set.mem_Collect_eq}›
lemma ball_single [rewrite]: "(∀x∈{x}. P x) = P x" by auto

subsubsection ‹Membership›

setup ‹add_rewrite_rule @{thm Set.singleton_iff}›
setup ‹add_forward_prfstep (equiv_forward_th @{thm Set.empty_iff})›
lemma set_membership_distinct [forward]: "x ∈ s ⟹ y ∉ s ⟹ x ≠ y" by auto
lemma non_empty_exist_elt [backward]: "U ≠ {} ⟹ ∃x. x ∈ U" by blast
lemma non_univ_exist_compl [backward]: "U ≠ UNIV ⟹ ∃x. x ∉ U" by blast
setup ‹add_resolve_prfstep @{thm Set.UNIV_I}›

subsubsection ‹Insert›

setup ‹add_backward_prfstep_cond (equiv_backward_th @{thm Set.insert_iff}) [with_cond "?A ≠ {}"]›
setup ‹add_forward_prfstep_cond (equiv_forward_th @{thm Set.insert_iff})
  [with_score 500, with_cond "?A ≠ {}"]›
setup ‹add_forward_prfstep_cond (equiv_forward_th @{thm Set.insert_subset}) [with_cond "?A ≠ {}"]›
setup ‹add_backward_prfstep_cond (equiv_backward_th @{thm Set.insert_subset})
  [with_score 500, with_cond "?A ≠ {}"]›

subsubsection ‹Extensionality›

lemma set_ext [forward]: "∀a. a ∈ S ⟷ a ∈ T ⟹ S = T" by auto
setup ‹add_backward_prfstep_cond @{thm set_ext} [with_score 500, with_filt (order_filter "S" "T")]›

lemma set_pair_ext [forward]: "∀a b. (a, b) ∈ S ⟷ (a, b) ∈ T ⟹ S = T" by auto

subsubsection ‹Union›

setup ‹add_forward_prfstep_cond (equiv_forward_th @{thm Set.Un_iff}) [with_score 500]›
setup ‹add_backward_prfstep (equiv_backward_th @{thm Set.Un_iff})›

lemma UnD1 [forward]: "c ∈ A ∪ B ⟹ c ∉ A ⟹ c ∈ B" by auto
lemma UnD2 [forward]: "c ∈ A ∪ B ⟹ c ∉ B ⟹ c ∈ A" by auto
lemma UnD1_single [forward]: "c ∈ {a} ∪ B ⟹ c ≠ a ⟹ c ∈ B" by auto
lemma UnD2_single [forward]: "c ∈ A ∪ {b} ⟹ c ≠ b ⟹ c ∈ A" by auto
setup ‹add_forward_prfstep_cond @{thm Set.UnI1} [with_term "?A ∪ ?B"]›
setup ‹add_forward_prfstep_cond @{thm Set.UnI2} [with_term "?A ∪ ?B"]›
lemma UnI1_single: "a ∈ {a} ∪ B" by auto
lemma UnI2_single: "b ∈ A ∪ {b}" by auto
setup ‹add_forward_prfstep_cond @{thm UnI1_single} [with_term "{?a} ∪ ?B"]›
setup ‹add_forward_prfstep_cond @{thm UnI2_single} [with_term "?A ∪ {?b}"]›

lemma union_single_eq [rewrite, backward]: "x ∈ p ⟹ {x} ∪ p = p" by auto

subsubsection ‹Intersection›

setup ‹add_forward_prfstep (equiv_forward_th @{thm Set.Int_iff})›
setup ‹add_backward_prfstep_cond (equiv_backward_th @{thm Set.Int_iff}) [with_score 500]›

setup ‹add_rewrite_rule @{thm Set.Int_empty_left}›
setup ‹add_rewrite_rule @{thm Set.Int_empty_right}›
setup ‹add_rewrite_rule @{thm Set.Int_absorb}›
lemma set_disjoint_mp [forward, backward2]: "A ∩ B = {} ⟹ p ∈ A ⟹ p ∉ B" by auto
lemma set_disjoint_single [rewrite]: "{x} ∩ B = {} ⟷ x ∉ B" by simp

subsubsection ‹subset›

setup ‹add_forward_prfstep @{thm subsetI}›
setup ‹add_backward_prfstep_cond @{thm subsetI} [with_score 500]›

setup ‹add_resolve_prfstep @{thm empty_subsetI}›
setup ‹add_forward_prfstep @{thm subsetD}›
lemma subset_single [rewrite]: "{a} ⊆ B ⟷ a ∈ B" by simp
setup ‹add_resolve_prfstep @{thm Set.basic_monos(1)}›
setup ‹add_resolve_prfstep @{thm Set.Un_upper1}›
setup ‹add_resolve_prfstep @{thm Set.Un_upper2}›
lemma union_is_subset [forward]: "A ∪ B ⊆ C ⟹ A ⊆ C ∧ B ⊆ C" by simp
setup ‹add_backward1_prfstep @{thm Set.Un_least}›
setup ‹add_backward2_prfstep @{thm Set.Un_least}›
lemma subset_union_same1 [backward]: "B ⊆ C ⟹ A ∪ B ⊆ A ∪ C" by auto
lemma subset_union_same2 [backward]: "A ⊆ B ⟹ A ∪ C ⊆ B ∪ C" by auto

subsubsection ‹Diff›

setup ‹add_forward_prfstep (equiv_forward_th @{thm Set.Diff_iff})›
setup ‹add_backward_prfstep_cond (equiv_backward_th @{thm Set.Diff_iff}) [with_score 500]›

setup ‹add_rewrite_rule @{thm Set.empty_Diff}›
lemma mem_diff [rewrite]: "x ∈ A - B ⟷ x ∈ A ∧ x ∉ B" by simp
lemma set_union_minus_same1 [rewrite]: "(A ∪ B) - B = A - B" by auto
lemma set_union_minus_same2 [rewrite]: "(B ∪ A) - B = A - B" by auto
lemma set_union_minus_distinct [rewrite]: "a ≠ c ⟹ {a} ∪ (B - {c}) = {a} ∪ B - {c}" by auto
setup ‹add_forward_prfstep_cond @{thm Set.Diff_subset} [with_term "?A - ?B"]›
lemma union_subtract_elt1 [rewrite]: "x ∉ B ⟹ ({x} ∪ B) - {x} = B" by simp
lemma union_subtract_elt2 [rewrite]: "x ∉ B ⟹ (B ∪ {x}) - {x} = B" by simp
lemma subset_sub1 [backward]: "x ∈ A ⟹ A - {x} ⊂ A" by auto
lemma member_notin [forward]: "x ∈ S - {y} ⟹ x ≠ y" by simp
lemma member_notin_contra: "x ∈ S ⟹ x ≠ y ⟹ x ∈ S - {y}" by simp
setup ‹add_forward_prfstep_cond @{thm member_notin_contra} [with_term "?S - {?y}"]›

subsubsection ‹Results on finite sets›

setup ‹add_resolve_prfstep @{thm Finite_Set.finite.emptyI}›
lemma set_finite_single [resolve]: "finite {x}" by simp
setup ‹add_rewrite_rule @{thm Finite_Set.finite_Un}›
lemma Max_ge' [forward]: "finite A ⟹ x > Max A ⟹ ¬(x ∈ A)" using Max_ge leD by auto
setup ‹add_backward_prfstep @{thm finite_image_set}›
setup ‹add_forward_prfstep @{thm finite_atLeastAtMost}›
setup ‹add_forward_prfstep @{thm rev_finite_subset}›
setup ‹add_backward1_prfstep @{thm rev_finite_subset}›

subsubsection ‹Cardinality›

setup ‹add_rewrite_rule @{thm card.empty}›
lemma card_emptyD [rewrite]: "finite S ⟹ card S = 0 ⟹ S = {}" by simp
lemma card_minus1 [rewrite]: "x ∈ S ⟹ card (S - {x}) = card S - 1" by (simp add: card_Diff_subset)
setup ‹add_forward_prfstep @{thm finite_Diff}›
setup ‹add_resolve_prfstep @{thm card_mono}›

subsubsection ‹Image set›

setup ‹add_rewrite_rule @{thm Set.image_Un}›
setup ‹add_rewrite_rule @{thm image_set_diff}›

subsection ‹Multiset›

subsubsection ‹Basic properties›

lemma mset_member_empty [resolve]: "¬p ∈# {#}" by simp
lemma mem_multiset_single [rewrite]: "x ∈# {#y#} ⟷ x = y" by simp
setup ‹add_backward2_prfstep @{thm subset_mset.antisym}›
setup ‹add_resolve_prfstep @{thm Multiset.empty_le}›
setup ‹add_forward_prfstep @{thm mset_subsetD}›

lemma multi_contain_add_self1 [resolve]: "A ⊂# {#x#} + A" by simp
lemma multi_contain_add_self2 [resolve]: "A ⊂# A + {#x#}" by simp
setup ‹add_forward_prfstep_cond @{thm Multiset.multi_member_this} [with_term "{#?x#} + ?XS"]›
lemma multi_member_this2: "x ∈# XS + {#x#}" by simp
setup ‹add_forward_prfstep_cond @{thm multi_member_this2} [with_term "?XS + {#?x#}"]›
setup ‹add_backward_prfstep @{thm Multiset.subset_mset.add_left_mono}›
setup ‹add_backward_prfstep @{thm Multiset.subset_mset.add_right_mono}›

subsubsection ‹Case checking and induction›

lemma multi_nonempty_split' [resolve]: "M ≠ {#} ⟹ ∃M' m. M = M' + {#m#}"
  using multi_nonempty_split by auto

lemma multi_member_split' [backward]: "x ∈# M ⟹ ∃M'. M = M' + {#x#}"
  by (metis insert_DiffM2)

setup ‹add_strong_induct_rule @{thm full_multiset_induct}›

subsubsection ‹Results on mset›

setup ‹add_rewrite_rule @{thm set_mset_empty}›
setup ‹add_rewrite_rule @{thm set_mset_single}›
setup ‹add_rewrite_rule @{thm set_mset_union}›

setup ‹add_rewrite_rule @{thm image_mset_empty}›
setup ‹add_rewrite_rule @{thm image_mset_single}›
setup ‹add_rewrite_rule @{thm image_mset_union}›

setup ‹add_rewrite_rule @{thm prod_mset_empty}›
setup ‹add_rewrite_rule @{thm prod_mset_singleton}›
setup ‹add_rewrite_rule @{thm prod_mset_Un}›

subsubsection ‹Set interval›

setup ‹add_rewrite_rule @{thm Set_Interval.ord_class.lessThan_iff}›
setup ‹add_rewrite_rule @{thm Set_Interval.ord_class.atLeastAtMost_iff}›

end