# Theory FiniteLib

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

theory FiniteLib = Main:

```(*  Title:      FiniteLib.thy
*)

theory FiniteLib = Main:

syntax
"_qsetsum" :: "idt => bool => 'a => 'a" ("(3∑ _ | _./ _)" [0,0,10] 10)
(*
syntax (xsymbols)
"_qsetsum" :: "idt => bool => 'a => 'a" ("(3∑_ | (_)./ _)" [0,0,10] 10)
*)
syntax (HTML output)
"_qsetsum" :: "idt => bool => 'a => 'a" ("(3∑_ | (_)./ _)" [0,0,10] 10)

translations "∑x|P. t" => "setsum (%x. t) {x. P}"

print_translation {*
let
fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) \$ Abs(y,Ty,P)] =
(if x<>y then raise Match
else let val x' = Syntax.mark_bound x
val t' = subst_bound(x',t)
val P' = subst_bound(x',P)
in Syntax.const "_qsetsum" \$ Syntax.mark_bound x \$ P' \$ t' end) in [("setsum", setsum_tr')] end *}

syntax
"_from_to_setsum" :: "idt => 'a => 'a => 'b => 'b" ("(∑ _ = _.._./ _)" [0,0,0,10] 10)

(*
syntax (xsymbols)
"_from_to_setsum" :: "idt => 'a => 'a => 'b => 'b" ("(3∑_ = _.._./ _)" [0,0,0,10] 10)
*)

syntax (HTML output)
"_from_to_setsum" :: "idt => 'a => 'a => 'b => 'b" ("(3∑_ = _.._./ _)" [0,0,0,10] 10)

translations "∑x=a..b. t" == "setsum (%x. t) {a..b}"

lemma finite_union_finite_subsets: "finite S ==> ALL x:S. (finite x)
==> finite (Union S)";
by (unfold Union_def, auto);

lemma setsum_cong2: "[|!!x. x ∈ A ==> f x = g x|] ==> setsum f A = setsum g A";
by (rule setsum_cong, auto);

lemma setsum_const_times: "setsum (%x. (c::'a::semiring) * f x) A =
c * setsum f A";
apply (case_tac "finite A");
apply (induct set: Finites);
done;

lemma setsum_reindex': "[|finite B; inj_on f B|] ==>
setsum h (f ` B) = setsum (%x. h(f x)) B";
apply (frule setsum_reindex);
apply assumption;
apply (erule ssubst);
apply (unfold o_def);
apply (rule refl);
done;

lemma setsum_reindex_cong': "[|finite A; inj_on f A; B = f ` A;
g = (%x. h (f x))|] ==> setsum h B = setsum g A";
apply (frule setsum_reindex_cong);
apply assumption+;
apply (unfold o_def);
apply assumption+;
done;

lemma setsum_reindex_cong'': "[|finite A; inj_on f A; B = f ` A;
ALL x:A. (g x = h (f x))|] ==> setsum h B = setsum g A";
apply (subgoal_tac "setsum g A = setsum (h o f) A");
apply (subgoal_tac "setsum h B = setsum (h o f) A");
apply simp;
apply (rule setsum_reindex_cong);
apply assumption+;
apply (rule refl);
apply (rule setsum_cong);
done;

lemma setsum_of_nat': "of_nat (setsum f A) = setsum (%x. of_nat(f x)) A";
apply (subst setsum_of_nat);
done;

lemma setsum_of_int': "of_int (setsum f A) = setsum (%x. of_int(f x)) A";
apply (subst setsum_of_int);
done;

lemma interval_singleton [simp]: "{a::'a::order..a} = {a}";
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);

lemma interval_empty [simp]: "b < a ==> {a::'a::order..b} = {}";
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);

lemma interval_plus_one_nat: "(n::nat) <= m ==> {n..m+1} = {n..m} Un {m+1}";
by auto;

lemma setsum_range_plus_one_nat: "(n::nat) <= m ==>
(∑i=n..m+1. f i) = (∑i=n..m. f i) + f(m + 1)";
apply (subst interval_plus_one_nat);
apply assumption;
apply (subst setsum_Un_disjoint);
apply auto;
done;

lemma abs_setsum: "abs(setsum (f::'a=>'b::ordered_ring) A) <=
setsum (%x. abs (f x)) A";
apply (case_tac "finite A");
apply (induct set: Finites);
apply simp;
apply simp;
apply (rule order_trans);
apply (rule abs_triangle_ineq);
apply simp;
done;

lemma setsum_nonneg': "ALL x:A. (0::'a::ordered_ring) <=
f x ==> 0 <= setsum f A";
apply (case_tac "finite A");
apply (erule setsum_nonneg);
apply assumption;
done;

lemma setsum_nonpos: "finite A ==>
ALL x : A. f x <= (0::'a::ordered_semiring) ==>
setsum f A <= 0";
apply (induct set: Finites, auto);
apply (subgoal_tac "f x + setsum f F <= 0 + 0", simp)
done;

lemma setsum_nonpos': "ALL x : A. f x <= (0::'a::ordered_semiring) ==>
setsum f A <= 0";
apply (case_tac "finite A");
apply (erule setsum_nonpos);
apply assumption;
done;

lemma setsum_le_cong [rule_format]:
"(ALL x:A. f x <= ((g x)::'a::ordered_ring)) -->
setsum f A <= setsum g A";
apply (case_tac "finite A");
apply (induct set: Finites);
apply simp;
apply auto;
apply assumption;
done;

lemma setsum_lt_cong: "finite A ==> A ~= {} ==> ALL x:A. (f x < ((g x)::'a::ordered_semiring)) ==> setsum f A < setsum g A";
apply (induct set: Finites);
apply (force);
apply (case_tac "F = {}");
apply force;
done;

lemma setsum_negf': "(∑x:A. - (f::'a=>'b::ring) x) = - setsum f A";
apply (case_tac "finite A");
apply (erule setsum_negf);
done;

lemma nat_interval_Suc: "{1..Suc n} = {1..n} Un {Suc n}";
by auto;

lemma nat_setsum_Suc: "(∑i=1..Suc n. f i) = (∑i=1..n. f i) +
f (Suc n)";
apply (subst nat_interval_Suc);
apply (subst setsum_Un_disjoint);
apply auto;
done;

lemma interval_plus_one_nat': "(n::nat) <= m + 1 ==>
{n..m+1} = {n..m} Un {m+1}";
by auto;

lemma setsum_range_plus_one_nat': "(n::nat) <= m + 1 ==>
(∑i=n..m+1. f i) = (∑i=n..m. f i) + f(m + 1)";
apply (subst interval_plus_one_nat');
apply assumption;
apply (subst setsum_Un_disjoint);
apply auto;
done;

end
```

lemma finite_union_finite_subsets:

`  [| finite S; ∀x∈S. finite x |] ==> finite (Union S)`

lemma setsum_cong2:

`  (!!x. x ∈ A ==> f x = g x) ==> setsum f A = setsum g A`

lemma setsum_const_times:

`  (∑x∈A. c * f x) = c * setsum f A`

lemma setsum_reindex':

`  [| finite B; inj_on f B |] ==> setsum h (f ` B) = (∑x∈B. h (f x))`

lemma setsum_reindex_cong':

```  [| finite A; inj_on f A; B = f ` A; g = (%x. h (f x)) |]
==> setsum h B = setsum g A```

lemma setsum_reindex_cong'':

```  [| finite A; inj_on f A; B = f ` A; ∀x∈A. g x = h (f x) |]
==> setsum h B = setsum g A```

lemma setsum_of_nat':

`  of_nat (setsum f A) = (∑x∈A. of_nat (f x))`

lemma setsum_of_int':

`  of_int (setsum f A) = (∑x∈A. of_int (f x))`

lemma interval_singleton:

`  {a..a} = {a}`

lemma interval_empty:

`  b < a ==> {a..b} = {}`

lemma interval_plus_one_nat:

`  n ≤ m ==> {n..m + 1} = {n..m} ∪ {m + 1}`

lemma setsum_range_plus_one_nat:

`  n ≤ m ==> setsum f {n..m + 1} = setsum f {n..m} + f (m + 1)`

lemma abs_setsum:

`  ¦setsum f A¦ ≤ (∑x∈A. ¦f x¦)`

lemma setsum_nonneg':

`  ∀x∈A. (0::'a) ≤ f x ==> (0::'a) ≤ setsum f A`

lemma setsum_nonpos:

`  [| finite A; ∀x∈A. f x ≤ (0::'a) |] ==> setsum f A ≤ (0::'a)`

lemma setsum_nonpos':

`  ∀x∈A. f x ≤ (0::'a) ==> setsum f A ≤ (0::'a)`

lemma setsum_le_cong:

`  (!!x. x ∈ A ==> f x ≤ g x) ==> setsum f A ≤ setsum g A`

lemma setsum_lt_cong:

`  [| finite A; A ≠ {}; ∀x∈A. f x < g x |] ==> setsum f A < setsum g A`

lemma setsum_negf':

`  (∑x∈A. - f x) = - setsum f A`

lemma nat_interval_Suc:

`  {1..Suc n} = {1..n} ∪ {Suc n}`

lemma nat_setsum_Suc:

`  setsum f {1..Suc n} = setsum f {1..n} + f (Suc n)`

lemma interval_plus_one_nat':

`  n ≤ m + 1 ==> {n..m + 1} = {n..m} ∪ {m + 1}`

lemma setsum_range_plus_one_nat':

`  n ≤ m + 1 ==> setsum f {n..m + 1} = setsum f {n..m} + f (m + 1)`