theory SetsFunctions
imports Main
begin

lemma "A \<union> B = B \<union> A"
  apply (rule equalityI)
  apply (rule subsetI)
  apply (erule UnE)
    apply (rule UnI2)
    apply assumption
   apply (rule UnI1)
   apply assumption
  apply (rule subsetI)
  apply (erule UnE)
   apply (rule UnI2)
   apply assumption
  apply (rule UnI1)
  apply assumption
  done

lemma "A \<union> B = B \<union> A"
proof
  show "A \<union> B \<subseteq> B \<union> A"
  proof
    fix x
    assume "x \<in> A \<union> B"
    thus "x \<in> B \<union> A"
    proof
      assume "x \<in> A"
      thus "x \<in> B \<union> A"
        by auto
    next
      assume "x \<in> B"
      thus "x \<in> B \<union> A"
        by auto
    qed
  qed
next
  show "B \<union> A \<subseteq> A \<union> B"
    by auto
qed

lemma "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
  apply (rule equalityI)
   apply (rule subsetI)
   apply (erule IntE)
   apply (erule UnE)
    apply (rule UnI1)
    apply (rule IntI)
     apply assumption
    apply assumption
   apply (rule UnI2)
   apply (rule IntI)
    apply assumption
   apply assumption
  apply (rule subsetI)
  apply (erule UnE)
   apply (erule IntE)
   apply (rule IntI)
    apply assumption
   apply (rule UnI1)
   apply assumption
  apply (rule IntI)
   apply (erule IntE)
   apply assumption
  apply (erule IntE)
  apply (rule UnI2)
  apply assumption
  done

lemma "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)" (is "?levo = ?desno")
proof
  show "?levo \<subseteq> ?desno"
  proof
    fix x
    assume "x \<in> ?levo"
    thus "x \<in> ?desno"
    proof
      assume "x \<in> A"
      hence "x \<in> A \<union> B" "x \<in> A \<union> C"
        by auto
      thus "x \<in> ?desno"
        by auto
    next
      assume "x \<in> B \<inter> C"
      hence "x \<in> B" "x \<in> C"
        by auto

      from `x \<in> B` have "x \<in> A \<union> B" 
        by auto

      moreover

      from `x \<in> C` have "x \<in> A \<union> C"
        by auto

      ultimately
      
      show "x \<in> ?desno"
        by auto
    qed
  qed
next
  show "?levo \<supseteq> ?desno"
  proof
    fix x
    assume "x \<in> ?desno"
    hence *: "x \<in> (A \<union> B)" "x \<in> (A \<union> C)"
      by auto
    show "x \<in> ?levo"
    proof (cases "x \<in> A")
      case True
      thus ?thesis
        by auto
    next
      case False
      have "x \<in> B" "x \<in> C"
        using False *
        by auto
      hence "x \<in> B \<inter> C"
        by auto
      thus ?thesis
        by auto
    qed
  qed
qed

lemma "- (A \<inter> B) = (-A) \<union> (-B)"
proof
  show "- (A \<inter> B) \<subseteq> (-A) \<union> (-B)"
  proof
    fix x
    assume "x \<in> -(A \<inter> B)" 
    show "x \<in> (-A) \<union> (-B)"
    proof (rule ccontr)
      assume "\<not> ?thesis"
      hence "x \<notin> -A" "x \<notin> -B"
        by auto
      hence "x \<in> A" "x \<in> B"
        by auto
      hence "x \<in> A \<inter> B"
        by auto
      with `x \<in> -(A \<inter> B)`
      show "False"
        by auto
    qed
  qed
next
  show "-A \<union> - B \<subseteq> - (A \<inter> B)"
  proof
    fix x
    assume "x \<in> -A \<union> -B"
    show "x \<in> - (A \<inter> B)"
    proof
      assume "x \<in> A \<inter> B"
      hence "x \<in> A" "x \<in> B"
        by auto
      hence "x \<notin> -A" "x \<notin> -B"
        by auto
      with `x \<in> -A \<union> -B`
      show False
        by auto
    qed
  qed
qed

lemma "A - (B \<inter> C) = (A - B) \<union> (A - C)"
  apply (rule equalityI)
   apply (rule subsetI)
   apply (erule DiffE)
   apply (rule ccontr)
   apply (erule notE)
   apply (rule IntI)
    apply (rule ccontr)
    apply (erule notE)
    apply (rule UnI1)
    apply (rule DiffI)
     apply assumption
    apply assumption
   apply (rule ccontr)
   apply (erule notE)
   apply (rule UnI2)
   apply (rule DiffI)
    apply assumption
   apply assumption
  apply (rule subsetI)
  apply (erule UnE)
   apply (rule DiffI)
    apply (erule DiffE)
  apply assumption
   apply (rule notI)
   apply (erule DiffE)
   apply (erule IntE)
   apply (erule notE)
   apply assumption
  apply (rule DiffI)
   apply (erule DiffE)
   apply assumption
  apply (rule notI)
  apply (erule DiffE)
  apply (erule IntE)
  apply (erule notE)
  apply assumption
  done

lemma "A - (B \<inter> C) = (A - B) \<union> (A - C)"
proof
  show "A - (B \<inter> C) \<subseteq> (A - B) \<union> (A - C)"
  proof
    fix x
    assume "x \<in> A - (B \<inter> C)"
    hence "x \<in> A" "x \<notin> B \<inter> C"
      by auto
    hence "x \<notin> B \<or> x \<notin> C"
      by auto
    hence "x \<in> A - B \<or> x \<in> A - C"
      using `x \<in> A`
      by auto
    thus "x \<in> (A - B) \<union> (A - C)"
      by auto
  qed
next
  show "(A - B) \<union> (A - C) \<subseteq> A - (B \<inter> C)"
  proof
    fix x
    assume "x \<in> (A - B) \<union> (A - C)"
    thus "x \<in> A - (B \<inter> C)"
    proof
      assume "x \<in> A - B"
      hence "x \<in> A" "x \<notin> B"
        by auto
      hence "x \<notin> B \<inter> C"
        by auto
      thus "x \<in> A - (B \<inter> C)"
        using `x \<in> A`
        by auto
    next
      assume "x \<in> A - C"
      hence "x \<in> A" "x \<notin> C"
        by auto
      hence "x \<notin> B \<inter> C"
        by auto
      thus "x \<in> A - (B \<inter> C)"
        using `x \<in> A`
        by auto
    qed
  qed
qed

lemma
  assumes "A \<subseteq> C" "B \<subseteq> C"
  shows "(A \<union> B) \<subseteq> C"
proof
  fix x
  assume "x \<in> A \<union> B"
  hence "x \<in> A \<or> x \<in> B"
    by blast
  show "x \<in> C"
  proof (cases "x \<in> A")
    case True
    thus "x \<in> C"
      using `A \<subseteq> C`
      by blast
  next
    case False
    hence "x \<in> B"
      using `x \<in> A \<or> x \<in> B`
      by blast
    thus "x \<in> C"
      using `B \<subseteq> C`
      by blast
  qed
qed

lemma
  assumes "A \<subseteq> C" "B \<subseteq> C"
  shows "(A \<union> B) \<subseteq> C"
proof
  fix x
  assume "x \<in> A \<union> B"
  thus "x \<in> C"
  proof
    assume "x \<in> A"
    thus "x \<in> C"
      using `A \<subseteq> C`
      by auto
  next
    assume "x \<in> B"
    thus "x \<in> C"
      using `B \<subseteq> C`
      by auto
  qed
qed

lemma
  shows "A \<subseteq> C \<and> B \<subseteq> C \<longrightarrow> (A \<union> B) \<subseteq> C"
  apply (rule impI)
  apply (erule conjE)
  apply (rule subsetI)
  apply (erule UnE)
  find_theorems "\<lbrakk> _ \<subseteq> _; _ \<in> _ \<rbrakk> \<Longrightarrow> _"
   apply (erule subsetD)
   apply assumption
  apply (erule subsetD) back
  apply assumption
  done


lemma "f ` (A \<union> B) = f ` A \<union> f ` B" (is "?l = ?d")
proof
  show "?l \<subseteq> ?d"
  proof
    fix y
    assume "y \<in> ?l"
    then obtain x where "x \<in> A \<union> B" "f x = y"
      by auto
    from `x \<in> A \<union> B` show "y \<in> ?d"
    proof
      assume "x \<in> A"
      hence "f x \<in> f ` A"
        by auto
      hence "y \<in> f ` A"
        using `f x = y`
        by auto
      thus "y \<in> ?d"
        by auto
    next
      assume "x \<in> B"
      hence "f x \<in> f ` B"
        by auto
      hence "y \<in> f ` B"
        using `f x = y`
        by auto
      thus "y \<in> ?d"
        by auto
    qed
  qed
next
  show "?d \<subseteq> ?l"
    by auto
qed

lemma "f ` (f -` B) \<subseteq> B"
proof
  fix y
  assume "y \<in> f ` (f -` B)"
  then obtain x where "x \<in> f -` B" "f x = y"
    by auto
  hence "f x \<in> B"
    by auto
  thus "y \<in> B"
    using `f x = y`
    by auto
qed

lemma "f -` (f ` A) \<supseteq> A"
proof
  fix x
  assume "x \<in> A"
  hence "f x \<in> f ` A"
    by auto
  thus "x \<in> f -` (f ` A)"
    by auto
qed

lemma
  "f -` (- B) = - (f -` B)" (is "?l = ?d")
proof
  show "?l \<subseteq> ?d"
  proof
    fix x
    assume "x \<in> ?l"
    hence "f x \<in> -B"
      by auto
    show "x \<in> ?d"
    proof (rule ccontr)
      assume "x \<notin> ?d"
      hence "x \<in> f -` B"
        by auto
      hence "f x \<in> B"
        by auto
      with `f x \<in> -B`
      show False
        by auto
    qed
  qed
next
  show "?d \<subseteq> ?l"
    by blast
qed

lemma
  assumes "inj f"
  shows "f -` (f ` A) \<subseteq> A"
proof
  fix x
  assume "x \<in> f -` (f ` A)"
  hence "f x \<in> f ` A"
    by auto
  then obtain x' where "x' \<in> A" "f x' = f x"
    by auto
  hence "x = x'"
    using `inj f`
    unfolding inj_def
    by auto
  thus "x \<in> A"
    using `x = x'` `x' \<in> A`
    by auto
qed

lemma 
  assumes "surj f"
  shows "f ` (f -` B) \<supseteq> B"
proof
  fix y
  assume "y \<in> B"
  obtain x where "y = f x"
    using `surj f`
    unfolding surj_def
    by auto
  hence "x \<in> f -` B"
    using `y \<in> B`
    by auto
  hence "f x \<in> f ` (f -` B)"
    by auto
  thus "y \<in> f ` (f -` B)"
    using `y = f x`
    by auto
qed

lemma
  assumes "surj f" "surj g"
  shows "surj (f \<circ> g)"
  unfolding surj_def
proof
  fix z
  obtain y where "z = f y"
    using `surj f`   
    unfolding surj_def
    by auto
  moreover
  obtain x where "y = g x"
    using `surj g`
    unfolding surj_def
    by auto
  ultimately
  have "z = f (g x)"
    by auto
  thus "\<exists> x. z = (f \<circ> g) x"
    by auto
qed

lemma
  assumes "inj f" "inj g"
  shows "inj (f \<circ> g)"
  unfolding inj_def
proof safe
  fix x y
  assume "(f \<circ> g) x = (f \<circ> g) y"
  hence "f (g x) = f (g y)"
    by auto
  hence "g x = g y"
    using `inj f`
    unfolding inj_def
    by auto
  thus "x = y"
    using `inj g`
    unfolding inj_def
    by auto
qed

lemma
  assumes "inj f"
  shows "x \<in> A \<longleftrightarrow> f x \<in> f ` A"
proof
  assume "x \<in> A"
  thus "f x \<in> f ` A"
    by auto
next
  assume "f x \<in> f ` A"
  then obtain x' where "x' \<in> A" "f x = f x'"
    by auto
  hence "x = x'"
    using `inj f`
    unfolding inj_def
    by auto
  thus "x \<in> A"
    using `x' \<in> A`
    by auto
qed

end