# HG changeset patch
# User paulson
# Date 1080207141 -3600
# Node ID ea2707645af8633f6a09f9be6e5d7592164906ce
# Parent  ef8c7c5eb01b78a873559323ce09992d1f1121bf
new material from Avigad

diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Finite_Set.ML
--- a/src/HOL/Finite_Set.ML	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Finite_Set.ML	Thu Mar 25 10:32:21 2004 +0100
@@ -32,7 +32,6 @@
 end;
 
 val Diff1_foldSet = thm "Diff1_foldSet";
-val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
 val cardR_SucD = thm "cardR_SucD";
 val cardR_determ = thm "cardR_determ";
 val cardR_emptyE = thm "cardR_emptyE";
@@ -83,7 +82,6 @@
 val finite_UN_I = thm "finite_UN_I";
 val finite_Un = thm "finite_Un";
 val finite_UnI = thm "finite_UnI";
-val finite_atMost = thm "finite_atMost";
 val finite_converse = thm "finite_converse";
 val finite_empty_induct = thm "finite_empty_induct";
 val finite_imageD = thm "finite_imageD";
@@ -92,7 +90,6 @@
 val finite_imp_foldSet = thm "finite_imp_foldSet";
 val finite_induct = thm "finite_induct";
 val finite_insert = thm "finite_insert";
-val finite_lessThan = thm "finite_lessThan";
 val finite_range_imageI = thm "finite_range_imageI";
 val finite_subset = thm "finite_subset";
 val finite_subset_induct = thm "finite_subset_induct";
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -7,7 +7,7 @@
 
 header {* Finite sets *}
 
-theory Finite_Set = Divides + Power + Inductive + SetInterval:
+theory Finite_Set = Divides + Power + Inductive:
 
 subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
 
@@ -34,9 +34,9 @@
 proof qed (rule add_commute add_assoc almost_semiring.add_0)+
 
 axclass times_ac1 < times, one
-  commute: "x * y = y * x"
-  assoc:   "(x * y) * z = x * (y * z)"
-  one:    "1 * x = x"
+  commute:     "x * y = y * x"
+  assoc:       "(x * y) * z = x * (y * z)"
+  one [simp]:  "1 * x = x"
 
 theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
   y * (x * z)"
@@ -50,7 +50,7 @@
   finally show ?thesis .
 qed
 
-theorem times_ac1_one_right: "(x::'a::times_ac1) * 1 = x"
+theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"
 proof -
   have "x * 1 = 1 * x"
     by (rule times_ac1.commute)
@@ -347,38 +347,6 @@
   done
 
 
-subsubsection {* Intervals of nats *}
-
-lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
-  by (induct k) (simp_all add: lessThan_Suc)
-
-lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
-  by (induct k) (simp_all add: atMost_Suc)
-
-lemma finite_greaterThanLessThan [iff]:
-  fixes l :: nat shows "finite {)l..u(}"
-by (simp add: greaterThanLessThan_def)
-
-lemma finite_atLeastLessThan [iff]:
-  fixes l :: nat shows "finite {l..u(}"
-by (simp add: atLeastLessThan_def)
-
-lemma finite_greaterThanAtMost [iff]:
-  fixes l :: nat shows "finite {)l..u}"
-by (simp add: greaterThanAtMost_def)
-
-lemma finite_atLeastAtMost [iff]:
-  fixes l :: nat shows "finite {l..u}"
-by (simp add: atLeastAtMost_def)
-
-lemma bounded_nat_set_is_finite:
-    "(ALL i:N. i < (n::nat)) ==> finite N"
-  -- {* A bounded set of natural numbers is finite. *}
-  apply (rule finite_subset)
-   apply (rule_tac [2] finite_lessThan, auto)
-  done
-
-
 subsubsection {* Finiteness of transitive closure *}
 
 text {* (Thanks to Sidi Ehmety) *}
@@ -849,63 +817,24 @@
   by (simp add: setsum_def
     LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
 
-lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: setsum_def)
-  apply (erule finite_induct, auto)
-  done
-
-lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: setsum_def)
-  apply (erule rev_mp)
-  apply (erule finite_induct, auto)
-  done
-
-lemma card_eq_setsum: "finite A ==> card A = setsum (\<lambda>x. 1) A"
-  -- {* Could allow many @{text "card"} proofs to be simplified. *}
-  by (induct set: Finites) auto
-
-lemma setsum_Un_Int: "finite A ==> finite B
-    ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
-  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-  apply (induct set: Finites, simp)
-  apply (simp add: plus_ac0 Int_insert_left insert_absorb)
-  done
-
-lemma setsum_Un_disjoint: "finite A ==> finite B
-  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
-  apply (subst setsum_Un_Int [symmetric], auto)
+lemma setsum_reindex [rule_format]: "finite B ==>
+                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setsum_insert)
+apply (simp add: inj_on_def)
   done
 
-lemma setsum_UN_disjoint:
-  fixes f :: "'a => 'b::plus_ac0"
-  shows
-    "finite I ==> (ALL i:I. finite (A i)) ==>
-        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
-      setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
-  apply (induct set: Finites, simp, atomize)
-  apply (subgoal_tac "ALL i:F. x \<noteq> i")
-   prefer 2 apply blast
-  apply (subgoal_tac "A x Int UNION F A = {}")
-   prefer 2 apply blast
-  apply (simp add: setsum_Un_disjoint)
-  done
+lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
+    setsum f B = setsum id (f ` B)"
+by (auto simp add: setsum_reindex id_o)
 
-lemma setsum_Union_disjoint:
-  "finite C ==> (ALL A:C. finite A) ==>
-        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
-      setsum f (Union C) = setsum (setsum f) C"
-  apply (frule setsum_UN_disjoint [of C id f])
-  apply (unfold Union_def id_def, assumption+)
-  done
-
-lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: setsum_def)
-  apply (erule finite_induct, auto)
-  apply (simp add: plus_ac0)
-  done
+lemma setsum_reindex_cong: "finite A ==> inj_on f A ==> 
+    B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
+  by (frule setsum_reindex, assumption, simp)
 
 lemma setsum_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
@@ -925,28 +854,10 @@
   apply (simp add: Ball_def del:insert_Diff_single)
   done
 
-lemma card_UN_disjoint:
-  fixes f :: "'a => 'b::plus_ac0"
-  shows
-    "finite I ==> (ALL i:I. finite (A i)) ==>
-        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
-      card (UNION I A) = setsum (\<lambda>i. card (A i)) I"
-  apply (subst card_eq_setsum)
-  apply (subst finite_UN, assumption+)
-  apply (subgoal_tac "setsum (\<lambda>i. card (A i)) I =
-      setsum (%i. (setsum (%x. 1) (A i))) I")
-  apply (erule ssubst)
-  apply (erule setsum_UN_disjoint, assumption+)
-  apply (rule setsum_cong)
-  apply (simp, simp add: card_eq_setsum)
-  done
-
-lemma card_Union_disjoint:
-  "finite C ==> (ALL A:C. finite A) ==>
-        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
-      card (Union C) = setsum card C"
-  apply (frule card_UN_disjoint [of C id])
-  apply (unfold Union_def id_def, assumption+)
+lemma setsum_0: "setsum (%i. 0) A = 0"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setsum_def)
+  apply (erule finite_induct, auto)
   done
 
 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
@@ -955,32 +866,85 @@
   apply (rule setsum_cong, auto)
   done
 
+lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A"
+  -- {* Could allow many @{text "card"} proofs to be simplified. *}
+  by (induct set: Finites) auto
 
-subsubsection {* Reindexing sums *}
+lemma setsum_Un_Int: "finite A ==> finite B
+    ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
+  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
+  apply (induct set: Finites, simp)
+  apply (simp add: plus_ac0 Int_insert_left insert_absorb)
+  done
+
+lemma setsum_Un_disjoint: "finite A ==> finite B
+  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
+  apply (subst setsum_Un_Int [symmetric], auto)
+  done
 
-lemma setsum_reindex [rule_format]: "finite B ==>
-                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
-apply (rule finite_induct, assumption, force)
-apply (rule impI, auto)
-apply (simp add: inj_on_def)
-apply (subgoal_tac "f x \<notin> f ` F")
-apply (subgoal_tac "finite (f ` F)")
-apply (auto simp add: setsum_insert)
-apply (simp add: inj_on_def)
+lemma setsum_UN_disjoint:
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
+  apply (induct set: Finites, simp, atomize)
+  apply (subgoal_tac "ALL i:F. x \<noteq> i")
+   prefer 2 apply blast
+  apply (subgoal_tac "A x Int UNION F A = {}")
+   prefer 2 apply blast
+  apply (simp add: setsum_Un_disjoint)
+  done
+
+lemma setsum_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      setsum f (Union C) = setsum (setsum f) C"
+  apply (frule setsum_UN_disjoint [of C id f])
+  apply (unfold Union_def id_def, assumption+)
   done
 
-lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
-    setsum f B = setsum id (f ` B)"
-by (auto simp add: setsum_reindex id_o)
+lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
+    (\<Sum> x:A. (\<Sum> y:B x. f x y)) = 
+    (\<Sum> z:(SIGMA x:A. B x). f (fst z) (snd z))"
+  apply (subst Sigma_def)
+  apply (subst setsum_UN_disjoint)
+  apply assumption
+  apply (rule ballI)
+  apply (drule_tac x = i in bspec, assumption)
+  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
+  apply (rule finite_surj)
+  apply auto
+  apply (rule setsum_cong, rule refl)
+  apply (subst setsum_UN_disjoint)
+  apply (erule bspec, assumption)
+  apply auto
+  done
 
+lemma setsum_cartesian_product: "finite A ==> finite B ==>
+    (\<Sum> x:A. (\<Sum> y:B. f x y)) = 
+    (\<Sum> z:A <*> B. f (fst z) (snd z))"
+  by (erule setsum_Sigma, auto);
+
+lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setsum_def)
+  apply (erule finite_induct, auto)
+  apply (simp add: plus_ac0)
+  done
 
 subsubsection {* Properties in more restricted classes of structures *}
 
+lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setsum_def)
+  apply (erule rev_mp)
+  apply (erule finite_induct, auto)
+  done
+
 lemma setsum_eq_0_iff [simp]:
     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   by (induct set: Finites) auto
 
-lemma setsum_constant_nat:
+lemma setsum_constant_nat [simp]:
     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
   -- {* Later generalized to any semiring. *}
   by (erule finite_induct, auto)
@@ -1022,13 +986,35 @@
   apply (blast intro: add_mono)
   done
 
-subsubsection {* Cardinality of Sigma and Cartesian product *}
+subsubsection {* Cardinality of unions and Sigma sets *}
+
+lemma card_UN_disjoint:
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      card (UNION I A) = setsum (%i. card (A i)) I"
+  apply (subst card_eq_setsum)
+  apply (subst finite_UN, assumption+)
+  apply (subgoal_tac "setsum (%i. card (A i)) I =
+      setsum (%i. (setsum (%x. 1) (A i))) I")
+  apply (erule ssubst)
+  apply (erule setsum_UN_disjoint, assumption+)
+  apply (rule setsum_cong)
+  apply simp+
+  done
+
+lemma card_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      card (Union C) = setsum card C"
+  apply (frule card_UN_disjoint [of C id])
+  apply (unfold Union_def id_def, assumption+)
+  done
 
 lemma SigmaI_insert: "y \<notin> A ==>
   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
   by auto
 
-lemma card_cartesian_product_singleton [simp]: "finite A ==>
+lemma card_cartesian_product_singleton: "finite A ==>
     card({x} <*> A) = card(A)"
   apply (subgoal_tac "inj_on (%y .(x,y)) A")
   apply (frule card_image, assumption)
@@ -1042,14 +1028,12 @@
   apply (erule finite_induct, auto)
   apply (subst SigmaI_insert, assumption)
   apply (subst card_Un_disjoint)
-  apply (auto intro: finite_SigmaI)
+  apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
   done
 
-lemma card_cartesian_product [simp]: "[| finite A; finite B |] ==>
+lemma card_cartesian_product: "[| finite A; finite B |] ==>
   card (A <*> B) = card(A) * card(B)"
-  apply (subst card_SigmaI, assumption+)
-  apply (simp add: setsum_constant_nat)
-  done
+  by simp
 
 
 subsection {* Generalized product over a set *}
@@ -1077,54 +1061,24 @@
   by (auto simp add: setprod_def LC_def LC.fold_insert
       times_ac1_left_commute)
 
-lemma setprod_1: "setprod (\<lambda>i. 1) A = 1"
-  apply (case_tac "finite A")
-  apply (erule finite_induct, auto simp add: times_ac1)
-  apply (simp add: setprod_def)
-  done
-
-lemma setprod_Un_Int: "finite A ==> finite B
-    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
-  apply (induct set: Finites, simp)
-  apply (simp add: times_ac1 insert_absorb)
-  apply (simp add: times_ac1 Int_insert_left insert_absorb)
-  done
-
-lemma setprod_Un_disjoint: "finite A ==> finite B
-  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
-  apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
+lemma setprod_reindex [rule_format]: "finite B ==>
+                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setprod_insert)
+apply (simp add: inj_on_def)
   done
 
-lemma setprod_UN_disjoint:
-  fixes f :: "'a => 'b::times_ac1"
-  shows
-    "finite I ==> (ALL i:I. finite (A i)) ==>
-        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
-      setprod f (UNION I A) = setprod (\<lambda>i. setprod f (A i)) I"
-  apply (induct set: Finites, simp, atomize)
-  apply (subgoal_tac "ALL i:F. x \<noteq> i")
-   prefer 2 apply blast
-  apply (subgoal_tac "A x Int UNION F A = {}")
-   prefer 2 apply blast
-  apply (simp add: setprod_Un_disjoint)
-  done
+lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
+    setprod f B = setprod id (f ` B)"
+by (auto simp add: setprod_reindex id_o)
 
-lemma setprod_Union_disjoint:
-  "finite C ==> (ALL A:C. finite A) ==>
-        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
-      setprod f (Union C) = setprod (setprod f) C"
-  apply (frule setprod_UN_disjoint [of C id f])
-  apply (unfold Union_def id_def, assumption+)
-  done
-
-lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A =
-    (setprod f A * setprod g A)"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: setprod_def times_ac1)
-  apply (erule finite_induct, auto)
-  apply (simp add: times_ac1)
-  apply (simp add: times_ac1)
-  done
+lemma setprod_reindex_cong: "finite A ==> inj_on f A ==> 
+    B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
+  by (frule setprod_reindex, assumption, simp)
 
 lemma setprod_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
@@ -1144,30 +1098,79 @@
   apply (simp add: Ball_def del:insert_Diff_single)
   done
 
+lemma setprod_1: "setprod (%i. 1) A = 1"
+  apply (case_tac "finite A")
+  apply (erule finite_induct, auto simp add: times_ac1)
+  apply (simp add: setprod_def)
+  done
+
 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
   apply (erule ssubst, rule setprod_1)
   apply (rule setprod_cong, auto)
   done
 
-
-subsubsection {* Reindexing products *}
+lemma setprod_Un_Int: "finite A ==> finite B
+    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
+  apply (induct set: Finites, simp)
+  apply (simp add: times_ac1 insert_absorb)
+  apply (simp add: times_ac1 Int_insert_left insert_absorb)
+  done
 
-lemma setprod_reindex [rule_format]: "finite B ==>
-                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
-apply (rule finite_induct, assumption, force)
-apply (rule impI, auto)
-apply (simp add: inj_on_def)
-apply (subgoal_tac "f x \<notin> f ` F")
-apply (subgoal_tac "finite (f ` F)")
-apply (auto simp add: setprod_insert)
-apply (simp add: inj_on_def)
+lemma setprod_Un_disjoint: "finite A ==> finite B
+  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
+  apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
+  done
+
+lemma setprod_UN_disjoint:
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
+  apply (induct set: Finites, simp, atomize)
+  apply (subgoal_tac "ALL i:F. x \<noteq> i")
+   prefer 2 apply blast
+  apply (subgoal_tac "A x Int UNION F A = {}")
+   prefer 2 apply blast
+  apply (simp add: setprod_Un_disjoint)
   done
 
-lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
-    setprod f B = setprod id (f ` B)"
-by (auto simp add: setprod_reindex id_o)
+lemma setprod_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      setprod f (Union C) = setprod (setprod f) C"
+  apply (frule setprod_UN_disjoint [of C id f])
+  apply (unfold Union_def id_def, assumption+)
+  done
 
+lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
+    (\<Prod> x:A. (\<Prod> y: B x. f x y)) = 
+    (\<Prod> z:(SIGMA x:A. B x). f (fst z) (snd z))"
+  apply (subst Sigma_def)
+  apply (subst setprod_UN_disjoint)
+  apply assumption
+  apply (rule ballI)
+  apply (drule_tac x = i in bspec, assumption)
+  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
+  apply (rule finite_surj)
+  apply auto
+  apply (rule setprod_cong, rule refl)
+  apply (subst setprod_UN_disjoint)
+  apply (erule bspec, assumption)
+  apply auto
+  done
+
+lemma setprod_cartesian_product: "finite A ==> finite B ==> 
+    (\<Prod> x:A. (\<Prod> y: B. f x y)) = 
+    (\<Prod> z:(A <*> B). f (fst z) (snd z))"
+  by (erule setprod_Sigma, auto)
+
+lemma setprod_timesf: "setprod (%x. f x * g x) A =
+    (setprod f A * setprod g A)"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setprod_def times_ac1)
+  apply (erule finite_induct, auto)
+  apply (simp add: times_ac1)
+  done
 
 subsubsection {* Properties in more restricted classes of structures *}
 
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Infinite_Set.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -5,7 +5,7 @@
 
 header {* Infnite Sets and Related Concepts*}
 
-theory Infinite_Set = Hilbert_Choice + Finite_Set:
+theory Infinite_Set = Hilbert_Choice + Finite_Set + SetInterval:
 
 subsection "Infinite Sets"
 
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -37,7 +37,7 @@
   One_int_def:   "1 == int 1"
 
   minus_int_def:
-    "- z ==  contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
+    "- z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
 
   add_int_def:
    "z + w ==
@@ -82,13 +82,8 @@
 declare inj_on_Abs_Integ [THEN inj_on_iff, simp]
         Abs_Integ_inverse [simp]
 
-lemma inj_Rep_Integ: "inj(Rep_Integ)"
-apply (rule inj_on_inverseI)
-apply (rule Rep_Integ_inverse)
-done
-
 text{*Case analysis on the representation of an integer as an equivalence
-      class.*}
+      class of pairs of naturals.*}
 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
      "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
 apply (rule Rep_Integ [of z, unfolded Integ_def, THEN quotientE])
@@ -952,7 +947,6 @@
 val equiv_intrel_iff = thm "equiv_intrel_iff";
 val intrel_in_integ = thm "intrel_in_integ";
 val inj_on_Abs_Integ = thm "inj_on_Abs_Integ";
-val inj_Rep_Integ = thm "inj_Rep_Integ";
 val inj_int = thm "inj_int";
 val zminus_zminus = thm "zminus_zminus";
 val zminus_0 = thm "zminus_0";
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Integ/Presburger.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -7,7 +7,7 @@
 generation for Cooper Algorithm  
 *)
 
-theory Presburger = NatSimprocs
+theory Presburger = NatSimprocs + SetInterval
 files
   ("cooper_dec.ML")
   ("cooper_proof.ML")
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/NumberTheory/Euler.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -138,7 +138,7 @@
     also have "... = int(setsum (%x.2) (SetS a p))";
       apply (insert prems)
       apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
-        card_setsum_aux)
+        card_setsum_aux simp del: setsum_constant_nat)
     done
     also have "... = 2 * int(card( SetS a p))";
       by (auto simp add: prems SetS_finite setsum_const2)
@@ -342,4 +342,4 @@
   apply (frule Euler_part1, auto simp add: zcong_sym)
 done
 
-end;
\ No newline at end of file
+end
\ No newline at end of file
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -342,7 +342,7 @@
 apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
 apply (auto simp only: card_eq_setsum)
 apply (erule setsum_same_function)
-by (auto simp add: card_eq_setsum)
+by auto;
 
 lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
     ((\<forall>x \<in> A. finite (g x)) & 
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Presburger.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -7,7 +7,7 @@
 generation for Cooper Algorithm  
 *)
 
-theory Presburger = NatSimprocs
+theory Presburger = NatSimprocs + SetInterval
 files
   ("cooper_dec.ML")
   ("cooper_proof.ML")
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/SetInterval.ML
--- a/src/HOL/SetInterval.ML	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/SetInterval.ML	Thu Mar 25 10:32:21 2004 +0100
@@ -49,3 +49,7 @@
 val lessThan_def     = thm "lessThan_def";
 val lessThan_iff = thm "lessThan_iff";
 val single_Diff_lessThan = thm "single_Diff_lessThan";
+
+val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
+val finite_atMost = thm "finite_atMost";
+val finite_lessThan = thm "finite_lessThan";
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/SetInterval.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -1,12 +1,13 @@
 (*  Title:      HOL/SetInterval.thy
     ID:         $Id$
     Author:     Tobias Nipkow and Clemens Ballarin
+                Additions by Jeremy Avigad in March 2004
     Copyright   2000  TU Muenchen
 
 lessThan, greaterThan, atLeast, atMost and two-sided intervals
 *)
 
-theory SetInterval = NatArith:
+theory SetInterval = IntArith:
 
 constdefs
   lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
@@ -58,23 +59,11 @@
   "INT i<n. A"  == "INT i:{..n(}. A"
 
 
-subsection {*lessThan*}
+subsection {* Various equivalences *}
 
 lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
 by (simp add: lessThan_def)
 
-lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
-by (simp add: lessThan_def)
-
-lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
-by (simp add: lessThan_def less_Suc_eq, blast)
-
-lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
-by (simp add: lessThan_def atMost_def less_Suc_eq_le)
-
-lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
-by blast
-
 lemma Compl_lessThan [simp]: 
     "!!k:: 'a::linorder. -lessThan k = atLeast k"
 apply (auto simp add: lessThan_def atLeast_def)
@@ -83,24 +72,9 @@
 lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
 by auto
 
-subsection {*greaterThan*}
-
 lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
 by (simp add: greaterThan_def)
 
-lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
-apply (simp add: greaterThan_def)
-apply (blast dest: gr0_conv_Suc [THEN iffD1])
-done
-
-lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
-apply (simp add: greaterThan_def)
-apply (auto elim: linorder_neqE)
-done
-
-lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
-by blast
-
 lemma Compl_greaterThan [simp]: 
     "!!k:: 'a::linorder. -greaterThan k = atMost k"
 apply (simp add: greaterThan_def atMost_def le_def, auto)
@@ -111,48 +85,22 @@
 apply (rule double_complement) 
 done
 
-
-subsection {*atLeast*}
-
 lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
 by (simp add: atLeast_def)
 
-lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
-by (unfold atLeast_def UNIV_def, simp)
-
-lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
-apply (simp add: atLeast_def)
-apply (simp add: Suc_le_eq)
-apply (simp add: order_le_less, blast)
-done
-
-lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
-by blast
-
 lemma Compl_atLeast [simp]: 
     "!!k:: 'a::linorder. -atLeast k = lessThan k"
 apply (simp add: lessThan_def atLeast_def le_def, auto)
 done
 
-
-subsection {*atMost*}
-
 lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)"
 by (simp add: atMost_def)
 
-lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
-by (simp add: atMost_def)
-
-lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
-apply (simp add: atMost_def)
-apply (simp add: less_Suc_eq order_le_less, blast)
-done
-
-lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
-by blast
+lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
+by (blast intro: order_antisym)
 
 
-subsection {*Logical Equivalences for Set Inclusion and Equality*}
+subsection {* Logical Equivalences for Set Inclusion and Equality *}
 
 lemma atLeast_subset_iff [iff]:
      "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
@@ -195,11 +143,6 @@
 done
 
 
-subsection {*Combined properties*}
-
-lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
-by (blast intro: order_antisym)
-
 subsection {*Two-sided intervals*}
 
 (* greaterThanLessThan *)
@@ -208,25 +151,12 @@
   "(i : {)l..u(}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
-lemma greaterThanLessThan_0 [simp]: "{)l..0::nat(} == {}"
-by (simp add: greaterThanLessThan_def)
-
-lemma greaterThanLessThan_Suc_greaterThanAtMost:
-  "{)l..Suc n(} = {)l..n}"
-by (auto simp add: greaterThanLessThan_def greaterThanAtMost_def)
-
 (* atLeastLessThan *)
 
 lemma atLeastLessThan_iff [simp]:
   "(i : {l..u(}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
-lemma atLeastLessThan_0 [simp]: "{l..0::nat(} == {}"
-by (simp add: atLeastLessThan_def)
-
-lemma atLeastLessThan_Suc_atLeastAtMost: "{l..Suc n(} = {l..n}"
-by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
-
 (* greaterThanAtMost *)
 
 lemma greaterThanAtMost_iff [simp]:
@@ -239,11 +169,226 @@
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
-
 (* The above four lemmas could be declared as iffs.
    If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
    seems to take forever (more than one hour). *)
 
+
+subsection {* Intervals of natural numbers *}
+
+lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
+by (simp add: lessThan_def)
+
+lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
+by (simp add: lessThan_def less_Suc_eq, blast)
+
+lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
+by (simp add: lessThan_def atMost_def less_Suc_eq_le)
+
+lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
+by blast
+
+lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
+apply (simp add: greaterThan_def)
+apply (blast dest: gr0_conv_Suc [THEN iffD1])
+done
+
+lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
+apply (simp add: greaterThan_def)
+apply (auto elim: linorder_neqE)
+done
+
+lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
+by blast
+
+lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
+by (unfold atLeast_def UNIV_def, simp)
+
+lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
+apply (simp add: atLeast_def)
+apply (simp add: Suc_le_eq)
+apply (simp add: order_le_less, blast)
+done
+
+lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
+  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
+
+lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
+by blast
+
+lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
+by (simp add: atMost_def)
+
+lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
+apply (simp add: atMost_def)
+apply (simp add: less_Suc_eq order_le_less, blast)
+done
+
+lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
+by blast
+
+(* Intervals of nats with Suc *)
+
+lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
+  by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
+
+lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}"  
+  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
+    greaterThanAtMost_def)
+
+lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}"  
+  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
+    greaterThanLessThan_def)
+
+subsubsection {* Finiteness *}
+
+lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
+  by (induct k) (simp_all add: lessThan_Suc)
+
+lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
+  by (induct k) (simp_all add: atMost_Suc)
+
+lemma finite_greaterThanLessThan [iff]:
+  fixes l :: nat shows "finite {)l..u(}"
+by (simp add: greaterThanLessThan_def)
+
+lemma finite_atLeastLessThan [iff]:
+  fixes l :: nat shows "finite {l..u(}"
+by (simp add: atLeastLessThan_def)
+
+lemma finite_greaterThanAtMost [iff]:
+  fixes l :: nat shows "finite {)l..u}"
+by (simp add: greaterThanAtMost_def)
+
+lemma finite_atLeastAtMost [iff]:
+  fixes l :: nat shows "finite {l..u}"
+by (simp add: atLeastAtMost_def)
+
+lemma bounded_nat_set_is_finite:
+    "(ALL i:N. i < (n::nat)) ==> finite N"
+  -- {* A bounded set of natural numbers is finite. *}
+  apply (rule finite_subset)
+   apply (rule_tac [2] finite_lessThan, auto)
+  done
+
+subsubsection {* Cardinality *}
+
+lemma card_lessThan [simp]: "card {..u(} = u"
+  by (induct_tac u, simp_all add: lessThan_Suc)
+
+lemma card_atMost [simp]: "card {..u} = Suc u"
+  by (simp add: lessThan_Suc_atMost [THEN sym])
+
+lemma card_atLeastLessThan [simp]: "card {l..u(} = u - l"
+  apply (subgoal_tac "card {l..u(} = card {..u-l(}")
+  apply (erule ssubst, rule card_lessThan)
+  apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {l..u(}")
+  apply (erule subst)
+  apply (rule card_image)
+  apply (rule finite_lessThan)
+  apply (simp add: inj_on_def)
+  apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
+  apply arith
+  apply (rule_tac x = "x - l" in exI)
+  apply arith
+  done
+
+lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
+  by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
+
+lemma card_greaterThanAtMost [simp]: "card {)l..u} = u - l" 
+  by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
+
+lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u - Suc l"
+  by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
+
+subsection {* Intervals of integers *}
+
+lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}"
+  by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
+
+lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}"  
+  by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
+
+lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
+    "{l+1..u(} = {)l..(u::int)(}"  
+  by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
+
+subsubsection {* Finiteness *}
+
+lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
+    {(0::int)..u(} = int ` {..nat u(}"
+  apply (unfold image_def lessThan_def)
+  apply auto
+  apply (rule_tac x = "nat x" in exI)
+  apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
+  done
+
+lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}"
+  apply (case_tac "0 \<le> u")
+  apply (subst image_atLeastZeroLessThan_int, assumption)
+  apply (rule finite_imageI)
+  apply auto
+  apply (subgoal_tac "{0..u(} = {}")
+  apply auto
+  done
+
+lemma image_atLeastLessThan_int_shift: 
+    "(%x. x + (l::int)) ` {0..u-l(} = {l..u(}"
+  apply (auto simp add: image_def atLeastLessThan_iff)
+  apply (rule_tac x = "x - l" in bexI)
+  apply auto
+  done
+
+lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}"
+  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+  apply (erule subst)
+  apply (rule finite_imageI)
+  apply (rule finite_atLeastZeroLessThan_int)
+  apply (rule image_atLeastLessThan_int_shift)
+  done
+
+lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
+  by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
+
+lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}" 
+  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
+
+lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}" 
+  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
+
+subsubsection {* Cardinality *}
+
+lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u"
+  apply (case_tac "0 \<le> u")
+  apply (subst image_atLeastZeroLessThan_int, assumption)
+  apply (subst card_image)
+  apply (auto simp add: inj_on_def)
+  done
+
+lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u - l)"
+  apply (subgoal_tac "card {l..u(} = card {0..u-l(}")
+  apply (erule ssubst, rule card_atLeastZeroLessThan_int)
+  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+  apply (erule subst)
+  apply (rule card_image)
+  apply (rule finite_atLeastZeroLessThan_int)
+  apply (simp add: inj_on_def)
+  apply (rule image_atLeastLessThan_int_shift)
+  done
+
+lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
+  apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
+  apply (auto simp add: compare_rls)
+  done
+
+lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u - l)" 
+  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
+
+lemma card_greaterThanLessThan_int [simp]: "card {)l..u(} = nat (u - (l + 1))"
+  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
+
+
 subsection {*Lemmas useful with the summation operator setsum*}
 
 (* For examples, see Algebra/poly/UnivPoly.thy *)