# Theory SetsAndFunctions

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory SetsAndFunctions = Complex:

```(*  Title:      SetsAndFunctions.thy
Author:     Kevin Donnelly and Jeremy Avigad
*)

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;

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;

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;

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);

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;

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(rule ext);
apply(rule ext);

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(rule_tac x = "b" in bexI);
apply(rule_tac x = "a" in bexI);
apply(rule_tac x = "aa" in bexI);
apply(rule_tac x = "b + ba" in exI);
apply(rule_tac x = "ba" in bexI);
apply(rule_tac x = "b" in bexI);
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(rule ext);
apply(rule ext);
apply(rule ext);
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";

lemma set_plus_intro2 [intro!]: "b ∈ C ==> a + b ∈ a \<pluso> C";

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 (rule_tac x = "aa + a" in exI);

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);

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);

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";

lemma set_plus_mono2 [intro]: "C ⊆ D ==> E ⊆ F ==> C + E ⊆ D + F";

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";

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);

lemma set_plus_imp_minus: "(a::'a::ring) ∈ b +o C ==> (a - b) ∈ C";

lemma set_minus_imp_plus: "(a::'a::ring) - b ∈ C ==> a ∈ b +o C";
apply (subgoal_tac "a = (a + - b) + b");
apply (rule bexI, assumption, assumption);

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";

lemma set_times_intro2 [intro!]: "b ∈ C ==> a * b ∈ a \<timeso> C";

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 (rule_tac x = "aa * a" in exI);

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);

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);

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";

lemma set_times_mono2 [intro]: "C ⊆ D ==> E ⊆ F ==> C * E ⊆ D * F";

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";

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);

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";

lemma set_neg_intro2: "(a::'a::ring) : C ==>
- a : (- 1) *o C";

end;
```

### Basic definitions

theorem func_diff_minus2:

`  f - g = f + - g`

lemma func_diff:

`  f - g = (%x. f x - g x)`

### Basic properties

lemma set_plus_intro:

`  [| a ∈ C; b ∈ D |] ==> a + b ∈ C + D`

lemma set_plus_intro2:

`  b ∈ C ==> a + b ∈ a + C`

lemma set_plus_rearrange:

`  a + C + b + D = (a + b) + (C + D)`

lemma set_plus_rearrange2:

`  a + (b + C) = (a + b) + C`

lemma set_plus_rearrange3:

`  a + B + C = a + (B + C)`

theorem set_plus_rearrange4:

`  C + a + D = a + (C + D)`

theorems set_plus_rearranges:

`  a + C + b + D = (a + b) + (C + D)`
`  a + (b + C) = (a + b) + C`
`  a + B + C = a + (B + C)`
`  C + a + D = a + (C + D)`

lemma set_plus_mono:

`  C ⊆ D ==> a + C ⊆ a + D`

lemma set_plus_mono2:

`  [| C ⊆ D; E ⊆ F |] ==> C + E ⊆ D + F`

lemma set_plus_mono3:

`  a ∈ C ==> a + D ⊆ C + D`

lemma set_plus_mono4:

`  a ∈ C ==> a + D ⊆ D + C`

lemma set_plus_mono5:

`  [| a ∈ C; B ⊆ D |] ==> a + B ⊆ C + D`

lemma set_plus_mono_b:

`  [| C ⊆ D; x ∈ a + C |] ==> x ∈ a + D`

lemma set_plus_mono2_b:

`  [| C ⊆ D; E ⊆ F; x ∈ C + E |] ==> x ∈ D + F`

lemma set_plus_mono3_b:

`  [| a ∈ C; x ∈ a + D |] ==> x ∈ C + D`

lemma set_plus_mono4_b:

`  [| a ∈ C; x ∈ a + D |] ==> x ∈ D + C`

lemma set_zero_plus:

`  (0::'a) + C = C`

lemma set_zero_plus2:

`  (0::'a) ∈ A ==> B ⊆ A + B`

lemma set_plus_imp_minus:

`  a ∈ b + C ==> a - b ∈ C`

lemma set_minus_imp_plus:

`  a - b ∈ C ==> a ∈ b + C`

lemma set_minus_plus:

`  (a - b ∈ C) = (a ∈ b + C)`

lemma set_times_intro:

`  [| a ∈ C; b ∈ D |] ==> a * b ∈ C * D`

lemma set_times_intro2:

`  b ∈ C ==> a * b ∈ a * C`

lemma set_times_rearrange:

`  a * C * b * D = (a * b) * (C * D)`

lemma set_times_rearrange2:

`  a * (b * C) = (a * b) * C`

lemma set_times_rearrange3:

`  a * B * C = a * (B * C)`

theorem set_times_rearrange4:

`  C * a * D = a * (C * D)`

theorems set_times_rearranges:

`  a * C * b * D = (a * b) * (C * D)`
`  a * (b * C) = (a * b) * C`
`  a * B * C = a * (B * C)`
`  C * a * D = a * (C * D)`

lemma set_times_mono:

`  C ⊆ D ==> a * C ⊆ a * D`

lemma set_times_mono2:

`  [| C ⊆ D; E ⊆ F |] ==> C * E ⊆ D * F`

lemma set_times_mono3:

`  a ∈ C ==> a * D ⊆ C * D`

lemma set_times_mono4:

`  a ∈ C ==> a * D ⊆ D * C`

lemma set_times_mono5:

`  [| a ∈ C; B ⊆ D |] ==> a * B ⊆ C * D`

lemma set_times_mono_b:

`  [| C ⊆ D; x ∈ a * C |] ==> x ∈ a * D`

lemma set_times_mono2_b:

`  [| C ⊆ D; E ⊆ F; x ∈ C * E |] ==> x ∈ D * F`

lemma set_times_mono3_b:

`  [| a ∈ C; x ∈ a * D |] ==> x ∈ C * D`

lemma set_times_mono4_b:

`  [| a ∈ C; x ∈ a * D |] ==> x ∈ D * C`

lemma set_one_times:

`  (1::'a) * C = C`

lemma set_times_plus_distrib:

`  a * (b + C) = (a * b) + a * C`

lemma set_times_plus_distrib2:

`  a * (B + C) = a * B + a * C`

lemma set_times_plus_distrib3:

`  a + C * D ⊆ a * D + C * D`

theorems set_times_plus_distribs:

`  a * (b + C) = (a * b) + a * C`
`  a * (B + C) = a * B + a * C`

lemma set_neg_intro:

`  a ∈ (- (1::'a)) * C ==> - a ∈ C`

lemma set_neg_intro2:

`  a ∈ C ==> - a ∈ (- (1::'a)) * C`