Theory Freiman_Sumset_Basics

theory Freiman_Sumset_Basics
  imports Main
begin

definition sumset :: "('a::comm_monoid_add) set ⇒ 'a set ⇒ 'a set" where
  "sumset A B = {x. ∃a∈A. ∃b∈B. x = a + b}"

lemma sumset_iff:
  "x ∈ sumset A B ⟷ (∃a∈A. ∃b∈B. x = a + b)"
  by (auto simp: sumset_def)

lemma sumsetI [intro]:
  assumes "a ∈ A" "b ∈ B"
  shows "a + b ∈ sumset A B"
  using assms by (auto simp: sumset_def)

lemma sumsetE [elim]:
  assumes "x ∈ sumset A B"
  obtains a b where "a ∈ A" "b ∈ B" "x = a + b"
  using assms by (auto simp: sumset_def)

lemma sumset_as_image:
  "sumset A B = case_prod (+) ` (A × B)"
  by (auto simp: sumset_def)

lemma sumset_commute:
  "sumset A B = sumset B A"
proof
  show "sumset A B ⊆ sumset B A"
  proof
    fix x
    assume "x ∈ sumset A B"
    then obtain a b where "a ∈ A" "b ∈ B" "x = a + b"
      by (auto simp: sumset_def)
    then show "x ∈ sumset B A"
    proof -
      have "b + a ∈ sumset B A"
        using ‹b ∈ B› ‹a ∈ A› by auto
      then show ?thesis
        using ‹x = a + b› by (simp add: add.commute)
    qed
  qed
next
  show "sumset B A ⊆ sumset A B"
  proof
    fix x
    assume "x ∈ sumset B A"
    then obtain b a where "b ∈ B" "a ∈ A" "x = b + a"
      by (auto simp: sumset_def)
    then show "x ∈ sumset A B"
    proof -
      have "a + b ∈ sumset A B"
        using ‹a ∈ A› ‹b ∈ B› by auto
      then show ?thesis
        using ‹x = b + a› by (simp add: add.commute)
    qed
  qed
qed

lemma empty_sumset_left [simp]:
  "sumset {} B = {}"
  by (auto simp: sumset_def)

lemma empty_sumset_right [simp]:
  "sumset A {} = {}"
  by (auto simp: sumset_def)

lemma sumset_assoc:
  fixes A B C :: "('a::comm_monoid_add) set"
  shows "sumset (sumset A B) C = sumset A (sumset B C)"
proof
  show "sumset (sumset A B) C ⊆ sumset A (sumset B C)"
  proof
    fix x
    assume "x ∈ sumset (sumset A B) C"
    then obtain ab c where ab: "ab ∈ sumset A B" and c: "c ∈ C" and x: "x = ab + c"
      by blast
    from ab obtain a b where a: "a ∈ A" and b: "b ∈ B" and ab_eq: "ab = a + b"
      by blast
    have "b + c ∈ sumset B C"
      using b c by auto
    then show "x ∈ sumset A (sumset B C)"
    proof -
      have "a + (b + c) ∈ sumset A (sumset B C)"
        using a ‹b + c ∈ sumset B C› by auto
      then show ?thesis
        using x ab_eq by (simp add: add.assoc)
    qed
  qed
next
  show "sumset A (sumset B C) ⊆ sumset (sumset A B) C"
  proof
    fix x
    assume "x ∈ sumset A (sumset B C)"
    then obtain a bc where a: "a ∈ A" and bc: "bc ∈ sumset B C" and x: "x = a + bc"
      by blast
    from bc obtain b c where b: "b ∈ B" and c: "c ∈ C" and bc_eq: "bc = b + c"
      by blast
    have "a + b ∈ sumset A B"
      using a b by auto
    then show "x ∈ sumset (sumset A B) C"
    proof -
      have "(a + b) + c ∈ sumset (sumset A B) C"
      proof (rule sumsetI)
        show "a + b ∈ sumset A B"
          using ‹a + b ∈ sumset A B› .
        show "c ∈ C"
          using c .
      qed
      then show ?thesis
        using x bc_eq by (simp add: add.assoc)
    qed
  qed
qed

lemma finite_sumset [intro]:
  assumes "finite A" "finite B"
  shows "finite (sumset A B)"
  unfolding sumset_as_image
  using assms by (intro finite_imageI finite_cartesian_product)

end