Theory FiniteLib

(*  Title:      FiniteLib.thy
    Author:     Jeremy Avigad
*)

header {* Facts about finite sets, sums, and products *}

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);
  apply (simp_all add: ring_distrib);
  apply (simp add: setsum_def);
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);
  apply (simp_all add: o_def);
done;

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

lemma setsum_of_int': "of_int (setsum f A) = setsum (%x. of_int(f x)) A";
  apply (subst setsum_of_int);
  apply (simp add: o_def);
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;
  apply (simp add: setsum_def);
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;
  apply (simp add: setsum_def);
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)
  apply (blast intro: add_mono);
  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;
  apply (simp add: setsum_def);
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 (erule add_mono);
  apply assumption;
  apply (simp add: setsum_def);
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 (simp add: setsum_insert);
  apply (case_tac "F = {}");
  apply force;
  apply (auto simp add: add_strict_mono);
  done;

lemma setsum_negf': "(∑x:A. - (f::'a=>'b::ring) x) = - setsum f A";
  apply (case_tac "finite A");
  apply (erule setsum_negf);
  apply (simp add: setsum_def);
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