Theory MLSSmf_HF_Extras

theory MLSSmf_HF_Extras
  imports HereditarilyFinite.HF
begin

lemma union_hunion: "finite a ⟹ finite b ⟹ HF (a ∪ b) = HF a ⊔ HF b"
  by (standard, standard, standard) auto

lemma inter_hinter: "finite a ⟹ finite b ⟹ HF (a ∩ b) = HF a ⊓ HF b"
  by (standard, standard, standard) auto

lemma hdisjoint_iff[iff]: "A ⊓ B = 0 ⟷ (∀x. x ❙∈ A ⟶ x ❙∉ B)"
  apply standard
   apply (metis hinter_iff hmem_hempty)
  apply blast
  done

lemma hcard_0E: "hcard s = 0 ⟹ s = 0"
proof (rule ccontr)
  assume "s ≠ 0" "hcard s = 0"
  then have "hcard s > 0"
    using hcard_hinsert_if hcard_hdiff1_less by fastforce
  with ‹hcard s = 0› show False by simp
qed

lemma hcard_1E: "hcard s = 1 ⟹ ∃c. s = 0 ◃ c"
proof (rule ccontr)
  assume "hcard s = 1" "∄c. s = 0 ◃ c"
  then obtain s' c where "s = s' ◃ c" "s' ≠ 0" "c ❙∉ s'"
    by (metis hcard_0 hf_cases zero_neq_one) 
  then have "hcard s = Suc (hcard s')"
    using hcard_hinsert_if by auto
  moreover
  from ‹s' ≠ 0› have "hcard s' > 0"
    using hcard_0E by blast
  ultimately
  have "hcard s > 1" by simp
  with ‹hcard s = 1› show False by presburger
qed

lemma singleton_nonempty_subset:
  assumes "s = HF {c}"
      and "t ≤ s"
      and "t ≠ 0"
    shows "t = HF {c}"
proof -
  from ‹t ≤ s› ‹s = HF {c}› have "c' = c" if "c' ❙∈ t" for c'
    using that by force
  with ‹t ≠ 0› show ?thesis by force
qed

lemma hsubset_hunion:
  "s ≤ t ∨ s ≤ u ⟹ s ≤ t ⊔ u"
  by (cases "s ≤ t") auto

lemma mem_hsubset_HUnion:
  "finite S ⟹ s ∈ S ⟹ s ≤ ⨆HF S"
  by auto

lemma hinter_hdiff_hempty: "s ≤ B ⟹ s ⊓ (A - B) = 0"
  by blast

lemma Hunion_nonempty: "finite S ⟹ ⨆HF S = ⨆HF {s ∈ S. s ≠ 0}"
  by force

lemma hcard_Hunion_singletons:
  assumes "finite s"
      and f_s_singletons: "∀x ∈ s. hcard (f x) = 1"
    shows "hcard (⨆HF (f ` s)) ≤ card s"
  using assms
proof (induction s)
  case empty
  then show ?case using Zero_hf_def by auto
next
  case (insert x F)
  then have IH': "hcard (⨆HF (f ` F)) ≤ card F" by blast
  from ‹∀x∈insert x F. hcard (f x) = 1› obtain a where "f x = HF {a}"
    using hcard_1E by fastforce
  then have Hunion_insert_a: "⨆HF (f ` insert x F) = ⨆HF (insert (HF {a}) (f ` F))"
    by simp
  have "HF (insert (HF {a}) (f ` F)) = (HF (f ` F)) ◃ (HF {a})"
    by (simp add: hinsert_def insert.hyps(1))
  also have "⨆... = HF {a} ⊔ (⨆HF (f ` F))" by blast
  also have "... = (⨆HF (f ` F)) ◃ a" by force
  finally have "⨆HF (insert (HF {a}) (f ` F)) = ⨆HF (f ` F) ◃ a" .
  with Hunion_insert_a have insert_hinsert:
    "⨆HF (f ` insert x F) = ⨆HF (f ` F) ◃ a"
    by argo
  
  have Suc_hcard_le: "hcard (⨆HF (f ` F) ◃ a) ≤ Suc (hcard (⨆HF (f ` F)))"
    apply (cases "a ❙∈ ⨆HF (f ` F)")
    by (simp add: hcard_hinsert_if)+

  from ‹x ∉ F› have Suc_card: "card (insert x F) = Suc (card F)"
    by (simp add: insert.hyps(1))

  from insert_hinsert Suc_hcard_le Suc_card IH'
  show ?case by presburger
qed

lemma hcard_Hunion_distinct_singletons:
  assumes "finite s"
      and f_distinct: "∀x ∈ s. ∀y ∈ s. x ≠ y ⟶ f x ≠ f y"
      and f_s_singletons: "∀x ∈ s. hcard (f x) = 1"
    shows "hcard (⨆HF (f ` s)) = card s"
  using assms
proof (induction s)
  case empty
  then show ?case using Zero_hf_def by auto
next
  case (insert x F)
  then have IH': "hcard (⨆HF (f ` F)) = card F" by blast
  from ‹∀x∈insert x F. hcard (f x) = 1› obtain a where "f x = HF {a}"
    using hcard_1E by fastforce
  then have Hunion_insert_a: "⨆HF (f ` insert x F) = ⨆HF (insert (HF {a}) (f ` F))"
    by simp
  have "HF (insert (HF {a}) (f ` F)) = (HF (f ` F)) ◃ (HF {a})"
    by (simp add: hinsert_def insert.hyps(1))
  also have "⨆... = HF {a} ⊔ (⨆HF (f ` F))" by blast
  also have "... = (⨆HF (f ` F)) ◃ a" by force
  finally have "⨆HF (insert (HF {a}) (f ` F)) = ⨆HF (f ` F) ◃ a" .
  with Hunion_insert_a have insert_hinsert:
    "⨆HF (f ` insert x F) = ⨆HF (f ` F) ◃ a"
    by argo
  
  have "b ≠ a" if "b ❙∈ ⨆HF (f ` F)" for b
  proof -
    from that obtain y where "y ∈ F" "b ❙∈ f y" by auto
    with insert.prems(2) have "f y = HF {b}"
      using hcard_1E by force
    from ‹y ∈ F› ‹x ∉ F› insert.prems(1) have "f x ≠ f y" by auto
    with ‹f x = HF {a}› ‹f y = HF {b}›
    show "b ≠ a" by auto
  qed
  then have Suc_hcard: "hcard (⨆HF (f ` F) ◃ a) = Suc (hcard (⨆HF (f ` F)))"
    by (metis hcard_hinsert_if)

  from ‹x ∉ F› have Suc_card: "card (insert x F) = Suc (card F)"
    by (simp add: insert.hyps(1))

  from insert_hinsert Suc_hcard Suc_card IH'
  show ?case by presburger
qed

lemma singleton_mem_eq:
  assumes "HF {a} = HF {b}"
    shows "a = b"
  using assms
  by (metis HF_hfset hfset_0 hfset_hinsert singleton_insert_inj_eq') 

lemma hinter_HUnion_if_image_pairwise_disjoint:
  assumes "finite U"
      and "S ⊆ U"
      and "T ⊆ U"
      and image_pairwise_disjoint: "∀x ∈ U. ∀y ∈ U. x ≠ y ⟶ f x ⊓ f y = 0"
    shows "⨆HF (f ` S) ⊓ ⨆HF (f ` T) = ⨆HF (f ` (S ∩ T))"
proof (standard; standard)
  fix c assume "c ❙∈ ⨆HF (f ` S) ⊓ ⨆HF (f ` T)"
  from assms have "finite S" "finite T"
    using finite_subset by blast+
  from ‹c ❙∈ ⨆HF (f ` S) ⊓ ⨆HF (f ` T)›
  have "c ❙∈ ⨆HF (f ` S)" "c ❙∈ ⨆HF (f ` T)" by blast+
  then obtain x y where "x ∈ S" "c ❙∈ f x" "y ∈ T" "c ❙∈ f y"
    using ‹finite S› ‹finite T› by fastforce+
  with image_pairwise_disjoint have "x = y"
    using ‹S ⊆ U› ‹T ⊆ U› by blast
  with ‹x ∈ S› ‹y ∈ T› have "x ∈ S ∩ T" by blast
  with ‹c ❙∈ f x› show "c ❙∈ ⨆HF (f ` (S ∩ T))"
    using ‹finite S› by auto
next
  fix c assume "c ❙∈ ⨆HF (f ` (S ∩ T))"
  then obtain x where "x ∈ S ∩ T" "c ❙∈ f x"
    by auto
  then have "x ∈ S" "x ∈ T" by blast+
  from assms have "finite S" "finite T"
    using finite_subset by blast+
  from ‹x ∈ S› ‹c ❙∈ f x› have "c ❙∈ ⨆HF (f ` S)" 
    using ‹finite S› by auto
  moreover
  from ‹x ∈ T› ‹c ❙∈ f x› have "c ❙∈ ⨆HF (f ` T)" 
    using ‹finite T› by auto
  ultimately
  show "c ❙∈ ⨆HF (f ` S) ⊓ ⨆HF (f ` T)" by blast
qed

lemma HUnion_hdiff_if_image_pairwise_disjoint:
  assumes "finite U"
      and "S ⊆ U"
      and "T ⊆ U"
      and image_pairwise_disjoint: "∀x ∈ U. ∀y ∈ U. x ≠ y ⟶ f x ⊓ f y = 0"
    shows "⨆HF (f ` (S - T)) = ⨆HF (f ` S) - ⨆HF (f ` T)"
proof (standard; standard)
  fix c assume "c ❙∈ ⨆HF (f ` (S - T))"
  then obtain x where "x ∈ S - T" "c ❙∈ f x"
    by auto
  then have "x ∈ S" "x ∉ T" by blast+
  from assms have "finite S" "finite T"
    using finite_subset by blast+
  from ‹x ∈ S› ‹c ❙∈ f x› have "c ❙∈ ⨆HF (f ` S)" 
    using ‹finite S› by auto
  from image_pairwise_disjoint ‹c ❙∈ f x›
  have "∀y ∈ U. y ≠ x ⟶ c ❙∉ f y"
    using ‹x ∈ S› ‹S ⊆ U› by auto
  with ‹x ∉ T› have "∀y ∈ T. c ❙∉ f y"
    using ‹T ⊆ U› by fast
  then have "c ❙∉ ⨆HF (f ` T)"
    using ‹finite T› by simp
  with ‹c ❙∈ ⨆HF (f ` S)› show "c ❙∈ ⨆HF (f ` S) - ⨆HF (f ` T)"
    by blast
next
  fix c assume "c ❙∈ ⨆HF (f ` S) - ⨆HF (f ` T)"
  from assms have "finite S" "finite T"
    using finite_subset by blast+
  from ‹c ❙∈ ⨆HF (f ` S) - ⨆HF (f ` T)›
  have "c ❙∈ ⨆HF (f ` S)" "c ❙∉ ⨆HF (f ` T)" by blast+
  then obtain x where "x ∈ S" "x ∉ T" "c ❙∈ f x"
    using ‹finite T› by fastforce
  then show "c ❙∈ ⨆HF (f ` (S - T))"
    using ‹finite S› by auto
qed

lemma hsubset_hcard:
  assumes "S ≤ T"
  shows "hcard S ≤ hcard T"
  using assms
  apply (induction T arbitrary: S)
   apply simp
  apply (smt (verit) hcard_hinsert_if less_eq_insert2_iff linorder_le_cases not_less_eq_eq)
  done

lemma HInter_singleton: "⨅HF {x} = x"
  unfolding HInter_def by auto

lemma HF_nonempty: "finite S ⟹ S ≠ {} ⟹ HF S ≠ 0"
  using hfset_HF by fastforce

lemma HF_insert_hinsert: "finite S ⟹ HF (insert x S) = HF S ◃ x"
  unfolding hinsert_def by simp

lemma HUnion_empty: "∀s ∈ S. f s = 0 ⟹ ⨆HF (f ` S) = 0"
  by fastforce

lemma HUnion_eq: "∀x ∈ S. f x = g x ⟹ ⨆HF (f ` S) = ⨆HF (g ` S)"
  by auto

end