now setsum f A = 0 unless A is finite; proved setsum_cong
authorpaulson
Tue Jun 20 11:41:07 2000 +0200 (2000-06-20)
changeset 9086e4592e43e703
parent 9085 5ce73f3cadff
child 9087 12db178a78df
now setsum f A = 0 unless A is finite; proved setsum_cong
src/HOL/Finite.ML
     1.1 --- a/src/HOL/Finite.ML	Fri Jun 16 14:02:41 2000 +0200
     1.2 +++ b/src/HOL/Finite.ML	Tue Jun 20 11:41:07 2000 +0200
     1.3 @@ -679,18 +679,22 @@
     1.4  qed "setsum_insert";
     1.5  Addsimps [setsum_insert];
     1.6  
     1.7 -Goal "finite A ==> setsum (%i. 0) A = 0";
     1.8 +Goal "setsum (%i. 0) A = 0";
     1.9 +by (case_tac "finite A" 1);
    1.10 + by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); 
    1.11  by (etac finite_induct 1);
    1.12  by Auto_tac;
    1.13  qed "setsum_0";
    1.14  
    1.15 -Goal "finite F ==> (setsum f F = 0) = (! a:F. f a = (0::nat))";
    1.16 +Goal "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))";
    1.17  by (etac finite_induct 1);
    1.18  by Auto_tac;
    1.19  qed "setsum_eq_0_iff";
    1.20  Addsimps [setsum_eq_0_iff];
    1.21  
    1.22 -Goal "[| setsum f F = Suc n; finite F |] ==> EX a:F. 0 < f a";
    1.23 +Goal "setsum f A = Suc n ==> EX a:A. 0 < f a";
    1.24 +by (case_tac "finite A" 1);
    1.25 + by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
    1.26  by (etac rev_mp 1);
    1.27  by (etac finite_induct 1);
    1.28  by Auto_tac;
    1.29 @@ -717,7 +721,7 @@
    1.30  by Auto_tac;
    1.31  qed "setsum_Un_disjoint";
    1.32  
    1.33 -Goal "[| finite I |] \
    1.34 +Goal "finite I \
    1.35  \     ==> (ALL i:I. finite (A i)) --> (ALL i:I. ALL j:I. A i Int A j = {}) \
    1.36  \         --> setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; 
    1.37  by (etac finite_induct 1);
    1.38 @@ -725,7 +729,9 @@
    1.39  by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
    1.40  qed_spec_mp "setsum_UN_disjoint";
    1.41  
    1.42 -Goal "finite A ==> setsum (%x. f x + g x) A = setsum f A + setsum g A";
    1.43 +Goal "setsum (%x. f x + g x) A = setsum f A + setsum g A";
    1.44 +by (case_tac "finite A" 1);
    1.45 + by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
    1.46  by (etac finite_induct 1);
    1.47  by Auto_tac;
    1.48  by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1);
    1.49 @@ -740,15 +746,38 @@
    1.50  by Auto_tac;
    1.51  qed "setsum_Un";
    1.52  
    1.53 -Goal "finite F \
    1.54 -\     ==> (setsum f (F-{a}) :: nat) = \
    1.55 -\         (if a:F then setsum f F - f a else setsum f F)";
    1.56 +Goal "(setsum f (A-{a}) :: nat) = \
    1.57 +\     (if a:A then setsum f A - f a else setsum f A)";
    1.58 +by (case_tac "finite A" 1);
    1.59 + by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
    1.60  by (etac finite_induct 1);
    1.61  by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
    1.62  by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
    1.63  by Auto_tac;
    1.64  qed_spec_mp "setsum_diff1";
    1.65  
    1.66 +val prems = Goal
    1.67 +    "[| A = B; !!x. x:B ==> f x = g x|] ==> setsum f A = setsum g B";
    1.68 +by (case_tac "finite B" 1);
    1.69 + by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); 
    1.70 +by (simp_tac (simpset() addsimps prems) 1);
    1.71 +by (subgoal_tac 
    1.72 +    "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C" 1);
    1.73 +by (asm_simp_tac (simpset() addsimps prems) 1); 
    1.74 +by (etac finite_induct 1);
    1.75 + by (simp_tac (simpset() addsimps [subset_empty]) 1);
    1.76 + by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1); 
    1.77 +by (Clarify_tac 1); 
    1.78 +by (subgoal_tac "finite C" 1);
    1.79 + by (blast_tac (claset() addDs [rotate_prems 1 finite_subset]) 2); 
    1.80 +by (subgoal_tac "C = insert x (C-{x})" 1); 
    1.81 + by (Blast_tac 2); 
    1.82 +by (etac ssubst 1); 
    1.83 +by (dtac spec 1); 
    1.84 +by (mp_tac 1);
    1.85 + by (asm_full_simp_tac (simpset() addsimps Ball_def::prems) 1); 
    1.86 +qed "setsum_cong";
    1.87 +
    1.88  
    1.89  (*** Basic theorem about "choose".  By Florian Kammueller, tidied by LCP ***)
    1.90