Theory SetsAndFunctions

(*  Title:      SetsAndFunctions.thy
    Author:     Kevin Donnelly and Jeremy Avigad
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
*)

header {* Operations on sets and functions *}

theory SetsAndFunctions = Complex:

subsection {* Basic definitions *}

instance set :: (times)times;
by intro_classes;

instance fun :: (type,times)times;
by intro_classes;

defs (overloaded)
  func_times: "f * g == (λx. f x * g x)" 
  set_times:"A * B == {c. ∃a∈A. ∃b∈B. c = a * b}";

instance set :: (plus)plus
by intro_classes;

instance fun :: (type,plus)plus;
by intro_classes;

defs (overloaded)
  func_plus: "f + g == (λx. f x + g x)"
  set_plus: "A + B == {c. ∃a∈A. ∃b∈B. c = a + b}";

instance fun :: (type,minus)minus
by intro_classes;

defs (overloaded)
  func_minus: "- f == (λx. - f x)"                 
  func_diff_minus: "(f - g) x == f x - g x";

theorem func_diff_minus2: "((f::'a => 'b::ring) - g) = (f + -g)";
apply(rule ext);
by(auto simp add: func_minus func_diff_minus func_plus diff_minus);

instance fun :: (type,zero)zero;
by intro_classes;

instance set :: (zero)zero;
by(intro_classes);

defs (overloaded)
  func_zero: "0::(('a::type) => ('b::zero)) == λx. 0"
  set_zero: "0::('a::zero)set == {0}";

instance fun :: (type,one)one;
by intro_classes;

instance set :: (one)one;
by intro_classes;

defs (overloaded)
  func_one: "1::(('a::type) => ('b::one)) == λx. 1"
  set_one: "1::('a::one)set == {1}";

constdefs 
  elt_set_plus :: "'a::plus => 'a set => 'a set"    (infixl "+o" 70)
  "a +o B == {c. ∃b∈B. c = a + b}"

  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
  "a *o B == {c. ∃b∈B. c = a * b}"

syntax
  "elt_set_eq" :: "'a => 'a set => bool"      (infix "=o" 50)
  "set_set_eq" :: "'a set => 'a set => bool"  (infix "=s" 50)

translations
  "x =o A" => "x ∈ A"
  "A =s B" => "A ⊆ B"
  
syntax
  "elt_set_eq" :: "'a => 'a set => bool"      (infix "\<elteqo>" 50)
  "set_set_eq" :: "'a set => 'a set => bool"  (infix "\<seteqo>" 50)
  "elt_set_plus" :: "'a => 'a set => 'a set"  (infix "\<pluso>" 70)
  "elt_set_times" :: "'a => 'a set => 'a set" (infix "\<timeso>" 80)

syntax (output)
  "elt_set_plus" :: "'a => 'a set => 'a set"  (infix "+" 70)
  "elt_set_times" :: "'a => 'a set => 'a set" (infix "*" 80)

instance fun :: (type,plus_ac0)plus_ac0;
apply intro_classes;
apply(auto simp add: func_zero func_plus);
apply(rule ext);
apply(auto simp add: plus_ac0.axioms);
apply(rule ext);
by(auto simp add: plus_ac0.axioms plus_ac0_left_commute);

instance set :: (plus_ac0)plus_ac0;
apply intro_classes;
apply (auto simp add: func_plus set_plus plus_ac0);
apply(rule_tac x = "b" in bexI);
apply(rule_tac x = "a" in bexI);
apply(auto simp add: plus_ac0.axioms);
apply(rule_tac x = "b" in bexI);
apply(rule_tac x = "a" in bexI);
apply(auto simp add: plus_ac0.axioms);
apply(rule_tac x = "aa" in bexI);
apply(rule_tac x = "b + ba" in exI);
apply(auto simp add: plus_ac0.axioms);
apply(rule_tac x = "ba" in bexI);
apply(rule_tac x = "b" in bexI);
apply(auto simp add: plus_ac0);
apply(rule_tac x = "a + aa" in exI);
by(auto simp add: plus_ac0 func_zero func_plus set_zero);

instance fun :: (type,ring)ring;
apply intro_classes;
apply(auto simp add: func_plus func_times func_minus func_diff_minus ext 
  func_one func_zero ring.axioms);
apply(rule ext);
apply(simp add: add_ac);
apply(rule ext);
apply(simp add: add_ac);
apply(rule ext);
apply(simp add: mult_ac);
apply(rule ext);
apply(simp add: mult_ac);
apply(simp add: ring_distrib ring.axioms);
apply(frule fun_cong);
apply auto;
apply (rule ext);
apply (simp add: func_diff_minus2 func_plus func_minus);
done;

lemma func_diff: "(%x. (f x)::'a::ring) - (%x. g x) = (%x. f x - g x)";
  by (simp add: diff_minus func_minus func_plus);

subsection {* Basic properties *}

lemma set_plus_intro [intro!]: "[| a ∈ C; b ∈ D|] ==> a + b ∈ C + D"; 
by (auto simp add: set_plus);

lemma set_plus_intro2 [intro!]: "b ∈ C ==> a + b ∈ a \<pluso> C";
by (auto simp add: elt_set_plus_def);

lemma set_plus_rearrange: "((a::'a::plus_ac0) \<pluso> C) + 
  (b \<pluso> D) = (a + b) \<pluso> (C + D)";
apply (auto simp add: elt_set_plus_def set_plus plus_ac0);
apply (rule_tac x = "ba + bb" in exI);
apply (auto simp add: plus_ac0);
apply (rule_tac x = "aa + a" in exI);
by (auto simp add: plus_ac0);

lemma set_plus_rearrange2: "(a::'a::plus_ac0) \<pluso> (b \<pluso> C) = 
  (a + b) \<pluso> C";
by (auto simp add: elt_set_plus_def plus_ac0);

lemma set_plus_rearrange3: "((a::'a::plus_ac0) \<pluso> B) + C = 
  a \<pluso> (B + C)";
apply (auto simp add: elt_set_plus_def set_plus);
apply (blast intro: plus_ac0);
apply (rule_tac x = "a + aa" in exI);
apply (rule conjI);
apply (rule_tac x = "aa" in bexI);
apply auto;
apply (rule_tac x = "ba" in bexI);
by (auto simp add: plus_ac0);

theorem set_plus_rearrange4: "C + ((a::'a::plus_ac0) +o D) = a +o (C + D)"; 
  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus plus_ac0);
  apply (rule_tac x = "aa + ba" in exI);
  by (auto simp add: plus_ac0);

theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
  set_plus_rearrange3 set_plus_rearrange4;

lemma set_plus_mono [intro!]: "C ⊆ D ==> a \<pluso> C ⊆ a \<pluso> D";
by (auto simp add: elt_set_plus_def);

lemma set_plus_mono2 [intro]: "C ⊆ D ==> E ⊆ F ==> C + E ⊆ D + F";
by (auto simp add: set_plus);

lemma set_plus_mono3 [intro]: "a ∈ C ==> a \<pluso> D ⊆ C + D";
by (auto simp add: elt_set_plus_def set_plus);

lemma set_plus_mono4 [intro]: "(a::'a::plus_ac0) ∈ C ==> 
  a \<pluso> D ⊆ D + C"; 
by (auto simp add: elt_set_plus_def set_plus plus_ac0);

lemma set_plus_mono5: "a : C ==> B <= D ==> a +o B <= C + D";
  apply (subgoal_tac "a +o B <= a +o D");
  apply (erule order_trans);
  apply (erule set_plus_mono3);
  apply (erule set_plus_mono);
done;

lemma set_plus_mono_b: "C ⊆ D ==> x ∈ a \<pluso> C 
    ==> x ∈ a \<pluso> D";
  apply (frule set_plus_mono);
  apply auto;
  done;

lemma set_plus_mono2_b: "C ⊆ D ==> E ⊆ F ==> x ∈ C + E ==> 
    x ∈ D + F";
  apply (frule set_plus_mono2);
  prefer 2;
  apply force;
  apply assumption;
  done;

lemma set_plus_mono3_b: "a ∈ C ==> x ∈ a \<pluso> D ==> x ∈ C + D";
  apply (frule set_plus_mono3);
  apply auto;
  done;

lemma set_plus_mono4_b: "(a::'a::plus_ac0) ∈ C ==> 
  x ∈ a \<pluso> D ==> x ∈ D + C"; 
  apply (frule set_plus_mono4);
  apply auto;
  done;

lemma set_zero_plus [simp]: "(0::'a::plus_ac0) \<pluso> C = C";
by (auto simp add: elt_set_plus_def);

lemma set_zero_plus2: "(0::'a::plus_ac0) ∈ A ==> B ⊆ A + B";
apply (auto intro!: subsetI simp add: set_plus);
apply (rule_tac x = 0 in bexI);
apply (rule_tac x = x in bexI);
by (auto simp add: plus_ac0);

lemma set_plus_imp_minus: "(a::'a::ring) ∈ b +o C ==> (a - b) ∈ C";
by (auto simp add: elt_set_plus_def add_ac diff_minus);

lemma set_minus_imp_plus: "(a::'a::ring) - b ∈ C ==> a ∈ b +o C";
apply (auto simp add: elt_set_plus_def add_ac diff_minus);
apply (subgoal_tac "a = (a + - b) + b");
apply (rule bexI, assumption, assumption);
by (auto simp add: add_ac);

lemma set_minus_plus: "((a::'a::ring) - b ∈ C) = (a ∈ b +o C)";
by (rule iffI, rule set_minus_imp_plus, assumption,
  rule set_plus_imp_minus, assumption);

lemma set_times_intro [intro!]: "[| a ∈ C; b ∈ D|] ==> a * b ∈ C * D"; 
by (auto simp add: set_times);

lemma set_times_intro2 [intro!]: "b ∈ C ==> a * b ∈ a \<timeso> C";
by (auto simp add: elt_set_times_def);

lemma set_times_rearrange: "((a::'a::ring) \<timeso> C) * 
  (b \<timeso> D) = (a * b) \<timeso> (C * D)";
apply (auto simp add: elt_set_times_def set_times);
apply (rule_tac x = "ba * bb" in exI);
apply (auto simp add: mult_ac);
apply (rule_tac x = "aa * a" in exI);
by (auto simp add: mult_ac);

lemma set_times_rearrange2: "(a::'a::ring) \<timeso> (b \<timeso> C) = 
  (a * b) \<timeso> C";
by (auto simp add: elt_set_times_def mult_ac);

lemma set_times_rearrange3: "((a::'a::ring) \<timeso> B) * C = 
  a \<timeso> (B * C)";
apply (auto simp add: elt_set_times_def set_times);
apply (blast intro: mult_ac);
apply (rule_tac x = "a * aa" in exI);
apply (rule conjI);
apply (rule_tac x = "aa" in bexI);
apply auto;
apply (rule_tac x = "ba" in bexI);
by (auto simp add: mult_ac);

theorem set_times_rearrange4: "C * ((a::'a::ring) *o D) = a *o (C * D)"; 
  apply (auto intro!: subsetI simp add: elt_set_times_def set_times 
    mult_ac);
  apply (rule_tac x = "aa * ba" in exI);
  by (auto simp add: mult_ac);

theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
  set_times_rearrange3 set_times_rearrange4;

lemma set_times_mono [intro!]: "C ⊆ D ==> a \<timeso> C ⊆ a \<timeso> D";
by (auto simp add: elt_set_times_def);

lemma set_times_mono2 [intro]: "C ⊆ D ==> E ⊆ F ==> C * E ⊆ D * F";
by (auto simp add: set_times);

lemma set_times_mono3 [intro]: "a ∈ C ==> a \<timeso> D ⊆ C * D";
by (auto simp add: elt_set_times_def set_times);

lemma set_times_mono4 [intro]: "(a::'a::times_ac1) ∈ C ==> 
  a \<timeso> D ⊆ D * C"; 
by (auto simp add: elt_set_times_def set_times times_ac1);

lemma set_times_mono5: "a : C ==> B <= D ==> a *o B <= C * D";
  apply (subgoal_tac "a *o B <= a *o D");
  apply (erule order_trans);
  apply (erule set_times_mono3);
  apply (erule set_times_mono);
done;

lemma set_times_mono_b: "C ⊆ D ==> x ∈ a \<timeso> C 
    ==> x ∈ a \<timeso> D";
  apply (frule set_times_mono);
  apply auto;
  done;

lemma set_times_mono2_b: "C ⊆ D ==> E ⊆ F ==> x ∈ C * E ==> 
    x ∈ D * F";
  apply (frule set_times_mono2);
  prefer 2;
  apply force;
  apply assumption;
  done;

lemma set_times_mono3_b: "a ∈ C ==> x ∈ a \<timeso> D ==> x ∈ C * D";
  apply (frule set_times_mono3);
  apply auto;
  done;

lemma set_times_mono4_b: "(a::'a::times_ac1) ∈ C ==> 
  x ∈ a \<timeso> D ==> x ∈ D * C"; 
  apply (frule set_times_mono4);
  apply auto;
  done;

lemma set_one_times [simp]: "(1::'a::ring) \<timeso> C = C";
by (auto simp add: elt_set_times_def);

lemma set_times_plus_distrib: "(a::'a::ring) \<timeso> (b \<pluso> C)= 
  (a * b) \<pluso> (a \<timeso> C)";
by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib);

lemma set_times_plus_distrib2: "(a::'a::ring) \<timeso> (B + C) = 
  (a \<timeso> B) + (a \<timeso> C)";
apply (auto simp add: set_plus elt_set_times_def ring_distrib);
apply blast;
apply (rule_tac x = "b + bb" in exI);
by (auto simp add: ring_distrib);

lemma set_times_plus_distrib3: "((a::'a::ring) \<pluso> C) * D ⊆ 
    a \<timeso> D + C * D";
  apply (auto intro!: subsetI simp add: 
    elt_set_plus_def elt_set_times_def set_times 
    set_plus ring_distrib);
  by auto;

theorems set_times_plus_distribs = set_times_plus_distrib
  set_times_plus_distrib2;

lemma set_neg_intro: "(a::'a::ring) : (- 1) *o C ==> 
    - a : C"; 
  by (auto simp add: elt_set_times_def);

lemma set_neg_intro2: "(a::'a::ring) : C ==>
    - a : (- 1) *o C";
  by (auto simp add: elt_set_times_def);
  

end;