# HG changeset patch
# User paulson
# Date 959187008 -7200
# Node ID 0d4abacae6aacd3ce01ee971012f7eb63b7bc575
# Parent  633e1682455c81076fd732e614957ce86a72af66
setsum is now overloaded on plus_ac0;  lemmas about lessThan, etc.

diff -r 633e1682455c -r 0d4abacae6aa src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed May 24 18:49:05 2000 +0200
+++ b/src/HOL/Finite.ML	Wed May 24 18:50:08 2000 +0200
@@ -213,21 +213,24 @@
 qed "finite_converse";
 AddIffs [finite_converse];
 
+Goal "finite (lessThan (k::nat))";
+by (induct_tac "k" 1);
+by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);
+by Auto_tac;
+qed "finite_lessThan";
+
+Goal "finite (atMost (k::nat))";
+by (induct_tac "k" 1);
+by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
+by Auto_tac;
+qed "finite_atMost";
+
 (* A bounded set of natural numbers is finite *)
-Goal "!N. (!i:N. i<(n::nat)) --> finite N";
-by (induct_tac "n" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
-by (rtac allI 1);
-by (case_tac "n : N" 1);
- by (ftac insert_Diff 1);
- by (etac subst 1);
- by (rtac impI 1);
- by (rtac (finite_insert RS iffD2) 1);
- by (EVERY1[etac allE, etac mp]);
- by (Blast_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "bounded_nat_set_is_finite";
+Goal "(!i:N. i<(n::nat)) ==> finite N";
+by (rtac finite_subset 1);
+ by (rtac finite_lessThan 2);
+by Auto_tac;
+qed "bounded_nat_set_is_finite";
 
 
 section "Finite cardinality -- 'card'";
@@ -800,7 +803,8 @@
 
 Goalw [setsum_def]
  "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
-by (asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
+by (asm_simp_tac (simpset() addsimps [export fold_insert,
+				      thm "plus_ac0_left_commute"]) 1);
 qed "setsum_insert";
 Addsimps [setsum_insert];
 
@@ -814,18 +818,20 @@
 \     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
 by (etac finite_induct 1);
 by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Int_insert_left, insert_absorb,
-					   add_commute]) 1);
+by (asm_full_simp_tac (simpset() addsimps (thms "plus_ac0") @ 
+                                          [Int_insert_left, insert_absorb]) 1);
 qed "setsum_Un_Int";
 
 Goal "[| finite A; finite B |] \
-\     ==> setsum f (A Un B) = setsum f A + setsum f B - setsum f (A Int B)";
+\     ==> (setsum f (A Un B) :: nat) = \
+\         setsum f A + setsum f B - setsum f (A Int B)";
 by (stac (setsum_Un_Int RS sym) 1);
 by Auto_tac;
 qed "setsum_Un";
 
 Goal "finite F \
-\     ==> setsum f (F-{a}) = (if a:F then setsum f F - f a else setsum f F)";
+\     ==> (setsum f (F-{a}) :: nat) = \
+\         (if a:F then setsum f F - f a else setsum f F)";
 by (etac finite_induct 1);
 by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
 by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
@@ -835,6 +841,7 @@
 Goal "finite A ==> setsum (%x. f x + g x) A = setsum f A + setsum g A";
 by (etac finite_induct 1);
 by Auto_tac;
+by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1);
 qed "setsum_addf";