new material from Avigad
authorpaulson
Thu Mar 25 10:32:21 2004 +0100 (2004-03-25)
changeset 14485ea2707645af8
parent 14484 ef8c7c5eb01b
child 14486 74c053a25513
new material from Avigad
src/HOL/Finite_Set.ML
src/HOL/Finite_Set.thy
src/HOL/Infinite_Set.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/Presburger.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/Finite2.thy
src/HOL/Presburger.thy
src/HOL/SetInterval.ML
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Finite_Set.ML	Thu Mar 25 10:31:25 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.ML	Thu Mar 25 10:32:21 2004 +0100
     1.3 @@ -32,7 +32,6 @@
     1.4  end;
     1.5  
     1.6  val Diff1_foldSet = thm "Diff1_foldSet";
     1.7 -val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
     1.8  val cardR_SucD = thm "cardR_SucD";
     1.9  val cardR_determ = thm "cardR_determ";
    1.10  val cardR_emptyE = thm "cardR_emptyE";
    1.11 @@ -83,7 +82,6 @@
    1.12  val finite_UN_I = thm "finite_UN_I";
    1.13  val finite_Un = thm "finite_Un";
    1.14  val finite_UnI = thm "finite_UnI";
    1.15 -val finite_atMost = thm "finite_atMost";
    1.16  val finite_converse = thm "finite_converse";
    1.17  val finite_empty_induct = thm "finite_empty_induct";
    1.18  val finite_imageD = thm "finite_imageD";
    1.19 @@ -92,7 +90,6 @@
    1.20  val finite_imp_foldSet = thm "finite_imp_foldSet";
    1.21  val finite_induct = thm "finite_induct";
    1.22  val finite_insert = thm "finite_insert";
    1.23 -val finite_lessThan = thm "finite_lessThan";
    1.24  val finite_range_imageI = thm "finite_range_imageI";
    1.25  val finite_subset = thm "finite_subset";
    1.26  val finite_subset_induct = thm "finite_subset_induct";
     2.1 --- a/src/HOL/Finite_Set.thy	Thu Mar 25 10:31:25 2004 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Thu Mar 25 10:32:21 2004 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  header {* Finite sets *}
     2.6  
     2.7 -theory Finite_Set = Divides + Power + Inductive + SetInterval:
     2.8 +theory Finite_Set = Divides + Power + Inductive:
     2.9  
    2.10  subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
    2.11  
    2.12 @@ -34,9 +34,9 @@
    2.13  proof qed (rule add_commute add_assoc almost_semiring.add_0)+
    2.14  
    2.15  axclass times_ac1 < times, one
    2.16 -  commute: "x * y = y * x"
    2.17 -  assoc:   "(x * y) * z = x * (y * z)"
    2.18 -  one:    "1 * x = x"
    2.19 +  commute:     "x * y = y * x"
    2.20 +  assoc:       "(x * y) * z = x * (y * z)"
    2.21 +  one [simp]:  "1 * x = x"
    2.22  
    2.23  theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
    2.24    y * (x * z)"
    2.25 @@ -50,7 +50,7 @@
    2.26    finally show ?thesis .
    2.27  qed
    2.28  
    2.29 -theorem times_ac1_one_right: "(x::'a::times_ac1) * 1 = x"
    2.30 +theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"
    2.31  proof -
    2.32    have "x * 1 = 1 * x"
    2.33      by (rule times_ac1.commute)
    2.34 @@ -347,38 +347,6 @@
    2.35    done
    2.36  
    2.37  
    2.38 -subsubsection {* Intervals of nats *}
    2.39 -
    2.40 -lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
    2.41 -  by (induct k) (simp_all add: lessThan_Suc)
    2.42 -
    2.43 -lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
    2.44 -  by (induct k) (simp_all add: atMost_Suc)
    2.45 -
    2.46 -lemma finite_greaterThanLessThan [iff]:
    2.47 -  fixes l :: nat shows "finite {)l..u(}"
    2.48 -by (simp add: greaterThanLessThan_def)
    2.49 -
    2.50 -lemma finite_atLeastLessThan [iff]:
    2.51 -  fixes l :: nat shows "finite {l..u(}"
    2.52 -by (simp add: atLeastLessThan_def)
    2.53 -
    2.54 -lemma finite_greaterThanAtMost [iff]:
    2.55 -  fixes l :: nat shows "finite {)l..u}"
    2.56 -by (simp add: greaterThanAtMost_def)
    2.57 -
    2.58 -lemma finite_atLeastAtMost [iff]:
    2.59 -  fixes l :: nat shows "finite {l..u}"
    2.60 -by (simp add: atLeastAtMost_def)
    2.61 -
    2.62 -lemma bounded_nat_set_is_finite:
    2.63 -    "(ALL i:N. i < (n::nat)) ==> finite N"
    2.64 -  -- {* A bounded set of natural numbers is finite. *}
    2.65 -  apply (rule finite_subset)
    2.66 -   apply (rule_tac [2] finite_lessThan, auto)
    2.67 -  done
    2.68 -
    2.69 -
    2.70  subsubsection {* Finiteness of transitive closure *}
    2.71  
    2.72  text {* (Thanks to Sidi Ehmety) *}
    2.73 @@ -849,63 +817,24 @@
    2.74    by (simp add: setsum_def
    2.75      LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
    2.76  
    2.77 -lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
    2.78 -  apply (case_tac "finite A")
    2.79 -   prefer 2 apply (simp add: setsum_def)
    2.80 -  apply (erule finite_induct, auto)
    2.81 -  done
    2.82 -
    2.83 -lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
    2.84 -  apply (case_tac "finite A")
    2.85 -   prefer 2 apply (simp add: setsum_def)
    2.86 -  apply (erule rev_mp)
    2.87 -  apply (erule finite_induct, auto)
    2.88 -  done
    2.89 -
    2.90 -lemma card_eq_setsum: "finite A ==> card A = setsum (\<lambda>x. 1) A"
    2.91 -  -- {* Could allow many @{text "card"} proofs to be simplified. *}
    2.92 -  by (induct set: Finites) auto
    2.93 -
    2.94 -lemma setsum_Un_Int: "finite A ==> finite B
    2.95 -    ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
    2.96 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    2.97 -  apply (induct set: Finites, simp)
    2.98 -  apply (simp add: plus_ac0 Int_insert_left insert_absorb)
    2.99 -  done
   2.100 -
   2.101 -lemma setsum_Un_disjoint: "finite A ==> finite B
   2.102 -  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   2.103 -  apply (subst setsum_Un_Int [symmetric], auto)
   2.104 +lemma setsum_reindex [rule_format]: "finite B ==>
   2.105 +                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   2.106 +apply (rule finite_induct, assumption, force)
   2.107 +apply (rule impI, auto)
   2.108 +apply (simp add: inj_on_def)
   2.109 +apply (subgoal_tac "f x \<notin> f ` F")
   2.110 +apply (subgoal_tac "finite (f ` F)")
   2.111 +apply (auto simp add: setsum_insert)
   2.112 +apply (simp add: inj_on_def)
   2.113    done
   2.114  
   2.115 -lemma setsum_UN_disjoint:
   2.116 -  fixes f :: "'a => 'b::plus_ac0"
   2.117 -  shows
   2.118 -    "finite I ==> (ALL i:I. finite (A i)) ==>
   2.119 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.120 -      setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
   2.121 -  apply (induct set: Finites, simp, atomize)
   2.122 -  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.123 -   prefer 2 apply blast
   2.124 -  apply (subgoal_tac "A x Int UNION F A = {}")
   2.125 -   prefer 2 apply blast
   2.126 -  apply (simp add: setsum_Un_disjoint)
   2.127 -  done
   2.128 +lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
   2.129 +    setsum f B = setsum id (f ` B)"
   2.130 +by (auto simp add: setsum_reindex id_o)
   2.131  
   2.132 -lemma setsum_Union_disjoint:
   2.133 -  "finite C ==> (ALL A:C. finite A) ==>
   2.134 -        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   2.135 -      setsum f (Union C) = setsum (setsum f) C"
   2.136 -  apply (frule setsum_UN_disjoint [of C id f])
   2.137 -  apply (unfold Union_def id_def, assumption+)
   2.138 -  done
   2.139 -
   2.140 -lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
   2.141 -  apply (case_tac "finite A")
   2.142 -   prefer 2 apply (simp add: setsum_def)
   2.143 -  apply (erule finite_induct, auto)
   2.144 -  apply (simp add: plus_ac0)
   2.145 -  done
   2.146 +lemma setsum_reindex_cong: "finite A ==> inj_on f A ==> 
   2.147 +    B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
   2.148 +  by (frule setsum_reindex, assumption, simp)
   2.149  
   2.150  lemma setsum_cong:
   2.151    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   2.152 @@ -925,28 +854,10 @@
   2.153    apply (simp add: Ball_def del:insert_Diff_single)
   2.154    done
   2.155  
   2.156 -lemma card_UN_disjoint:
   2.157 -  fixes f :: "'a => 'b::plus_ac0"
   2.158 -  shows
   2.159 -    "finite I ==> (ALL i:I. finite (A i)) ==>
   2.160 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.161 -      card (UNION I A) = setsum (\<lambda>i. card (A i)) I"
   2.162 -  apply (subst card_eq_setsum)
   2.163 -  apply (subst finite_UN, assumption+)
   2.164 -  apply (subgoal_tac "setsum (\<lambda>i. card (A i)) I =
   2.165 -      setsum (%i. (setsum (%x. 1) (A i))) I")
   2.166 -  apply (erule ssubst)
   2.167 -  apply (erule setsum_UN_disjoint, assumption+)
   2.168 -  apply (rule setsum_cong)
   2.169 -  apply (simp, simp add: card_eq_setsum)
   2.170 -  done
   2.171 -
   2.172 -lemma card_Union_disjoint:
   2.173 -  "finite C ==> (ALL A:C. finite A) ==>
   2.174 -        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   2.175 -      card (Union C) = setsum card C"
   2.176 -  apply (frule card_UN_disjoint [of C id])
   2.177 -  apply (unfold Union_def id_def, assumption+)
   2.178 +lemma setsum_0: "setsum (%i. 0) A = 0"
   2.179 +  apply (case_tac "finite A")
   2.180 +   prefer 2 apply (simp add: setsum_def)
   2.181 +  apply (erule finite_induct, auto)
   2.182    done
   2.183  
   2.184  lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
   2.185 @@ -955,32 +866,85 @@
   2.186    apply (rule setsum_cong, auto)
   2.187    done
   2.188  
   2.189 +lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A"
   2.190 +  -- {* Could allow many @{text "card"} proofs to be simplified. *}
   2.191 +  by (induct set: Finites) auto
   2.192  
   2.193 -subsubsection {* Reindexing sums *}
   2.194 +lemma setsum_Un_Int: "finite A ==> finite B
   2.195 +    ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   2.196 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   2.197 +  apply (induct set: Finites, simp)
   2.198 +  apply (simp add: plus_ac0 Int_insert_left insert_absorb)
   2.199 +  done
   2.200 +
   2.201 +lemma setsum_Un_disjoint: "finite A ==> finite B
   2.202 +  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   2.203 +  apply (subst setsum_Un_Int [symmetric], auto)
   2.204 +  done
   2.205  
   2.206 -lemma setsum_reindex [rule_format]: "finite B ==>
   2.207 -                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   2.208 -apply (rule finite_induct, assumption, force)
   2.209 -apply (rule impI, auto)
   2.210 -apply (simp add: inj_on_def)
   2.211 -apply (subgoal_tac "f x \<notin> f ` F")
   2.212 -apply (subgoal_tac "finite (f ` F)")
   2.213 -apply (auto simp add: setsum_insert)
   2.214 -apply (simp add: inj_on_def)
   2.215 +lemma setsum_UN_disjoint:
   2.216 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   2.217 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.218 +      setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
   2.219 +  apply (induct set: Finites, simp, atomize)
   2.220 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.221 +   prefer 2 apply blast
   2.222 +  apply (subgoal_tac "A x Int UNION F A = {}")
   2.223 +   prefer 2 apply blast
   2.224 +  apply (simp add: setsum_Un_disjoint)
   2.225 +  done
   2.226 +
   2.227 +lemma setsum_Union_disjoint:
   2.228 +  "finite C ==> (ALL A:C. finite A) ==>
   2.229 +        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   2.230 +      setsum f (Union C) = setsum (setsum f) C"
   2.231 +  apply (frule setsum_UN_disjoint [of C id f])
   2.232 +  apply (unfold Union_def id_def, assumption+)
   2.233    done
   2.234  
   2.235 -lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
   2.236 -    setsum f B = setsum id (f ` B)"
   2.237 -by (auto simp add: setsum_reindex id_o)
   2.238 +lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
   2.239 +    (\<Sum> x:A. (\<Sum> y:B x. f x y)) = 
   2.240 +    (\<Sum> z:(SIGMA x:A. B x). f (fst z) (snd z))"
   2.241 +  apply (subst Sigma_def)
   2.242 +  apply (subst setsum_UN_disjoint)
   2.243 +  apply assumption
   2.244 +  apply (rule ballI)
   2.245 +  apply (drule_tac x = i in bspec, assumption)
   2.246 +  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
   2.247 +  apply (rule finite_surj)
   2.248 +  apply auto
   2.249 +  apply (rule setsum_cong, rule refl)
   2.250 +  apply (subst setsum_UN_disjoint)
   2.251 +  apply (erule bspec, assumption)
   2.252 +  apply auto
   2.253 +  done
   2.254  
   2.255 +lemma setsum_cartesian_product: "finite A ==> finite B ==>
   2.256 +    (\<Sum> x:A. (\<Sum> y:B. f x y)) = 
   2.257 +    (\<Sum> z:A <*> B. f (fst z) (snd z))"
   2.258 +  by (erule setsum_Sigma, auto);
   2.259 +
   2.260 +lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   2.261 +  apply (case_tac "finite A")
   2.262 +   prefer 2 apply (simp add: setsum_def)
   2.263 +  apply (erule finite_induct, auto)
   2.264 +  apply (simp add: plus_ac0)
   2.265 +  done
   2.266  
   2.267  subsubsection {* Properties in more restricted classes of structures *}
   2.268  
   2.269 +lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   2.270 +  apply (case_tac "finite A")
   2.271 +   prefer 2 apply (simp add: setsum_def)
   2.272 +  apply (erule rev_mp)
   2.273 +  apply (erule finite_induct, auto)
   2.274 +  done
   2.275 +
   2.276  lemma setsum_eq_0_iff [simp]:
   2.277      "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   2.278    by (induct set: Finites) auto
   2.279  
   2.280 -lemma setsum_constant_nat:
   2.281 +lemma setsum_constant_nat [simp]:
   2.282      "finite A ==> (\<Sum>x: A. y) = (card A) * y"
   2.283    -- {* Later generalized to any semiring. *}
   2.284    by (erule finite_induct, auto)
   2.285 @@ -1022,13 +986,35 @@
   2.286    apply (blast intro: add_mono)
   2.287    done
   2.288  
   2.289 -subsubsection {* Cardinality of Sigma and Cartesian product *}
   2.290 +subsubsection {* Cardinality of unions and Sigma sets *}
   2.291 +
   2.292 +lemma card_UN_disjoint:
   2.293 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   2.294 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.295 +      card (UNION I A) = setsum (%i. card (A i)) I"
   2.296 +  apply (subst card_eq_setsum)
   2.297 +  apply (subst finite_UN, assumption+)
   2.298 +  apply (subgoal_tac "setsum (%i. card (A i)) I =
   2.299 +      setsum (%i. (setsum (%x. 1) (A i))) I")
   2.300 +  apply (erule ssubst)
   2.301 +  apply (erule setsum_UN_disjoint, assumption+)
   2.302 +  apply (rule setsum_cong)
   2.303 +  apply simp+
   2.304 +  done
   2.305 +
   2.306 +lemma card_Union_disjoint:
   2.307 +  "finite C ==> (ALL A:C. finite A) ==>
   2.308 +        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   2.309 +      card (Union C) = setsum card C"
   2.310 +  apply (frule card_UN_disjoint [of C id])
   2.311 +  apply (unfold Union_def id_def, assumption+)
   2.312 +  done
   2.313  
   2.314  lemma SigmaI_insert: "y \<notin> A ==>
   2.315    (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
   2.316    by auto
   2.317  
   2.318 -lemma card_cartesian_product_singleton [simp]: "finite A ==>
   2.319 +lemma card_cartesian_product_singleton: "finite A ==>
   2.320      card({x} <*> A) = card(A)"
   2.321    apply (subgoal_tac "inj_on (%y .(x,y)) A")
   2.322    apply (frule card_image, assumption)
   2.323 @@ -1042,14 +1028,12 @@
   2.324    apply (erule finite_induct, auto)
   2.325    apply (subst SigmaI_insert, assumption)
   2.326    apply (subst card_Un_disjoint)
   2.327 -  apply (auto intro: finite_SigmaI)
   2.328 +  apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
   2.329    done
   2.330  
   2.331 -lemma card_cartesian_product [simp]: "[| finite A; finite B |] ==>
   2.332 +lemma card_cartesian_product: "[| finite A; finite B |] ==>
   2.333    card (A <*> B) = card(A) * card(B)"
   2.334 -  apply (subst card_SigmaI, assumption+)
   2.335 -  apply (simp add: setsum_constant_nat)
   2.336 -  done
   2.337 +  by simp
   2.338  
   2.339  
   2.340  subsection {* Generalized product over a set *}
   2.341 @@ -1077,54 +1061,24 @@
   2.342    by (auto simp add: setprod_def LC_def LC.fold_insert
   2.343        times_ac1_left_commute)
   2.344  
   2.345 -lemma setprod_1: "setprod (\<lambda>i. 1) A = 1"
   2.346 -  apply (case_tac "finite A")
   2.347 -  apply (erule finite_induct, auto simp add: times_ac1)
   2.348 -  apply (simp add: setprod_def)
   2.349 -  done
   2.350 -
   2.351 -lemma setprod_Un_Int: "finite A ==> finite B
   2.352 -    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
   2.353 -  apply (induct set: Finites, simp)
   2.354 -  apply (simp add: times_ac1 insert_absorb)
   2.355 -  apply (simp add: times_ac1 Int_insert_left insert_absorb)
   2.356 -  done
   2.357 -
   2.358 -lemma setprod_Un_disjoint: "finite A ==> finite B
   2.359 -  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
   2.360 -  apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
   2.361 +lemma setprod_reindex [rule_format]: "finite B ==>
   2.362 +                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
   2.363 +apply (rule finite_induct, assumption, force)
   2.364 +apply (rule impI, auto)
   2.365 +apply (simp add: inj_on_def)
   2.366 +apply (subgoal_tac "f x \<notin> f ` F")
   2.367 +apply (subgoal_tac "finite (f ` F)")
   2.368 +apply (auto simp add: setprod_insert)
   2.369 +apply (simp add: inj_on_def)
   2.370    done
   2.371  
   2.372 -lemma setprod_UN_disjoint:
   2.373 -  fixes f :: "'a => 'b::times_ac1"
   2.374 -  shows
   2.375 -    "finite I ==> (ALL i:I. finite (A i)) ==>
   2.376 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.377 -      setprod f (UNION I A) = setprod (\<lambda>i. setprod f (A i)) I"
   2.378 -  apply (induct set: Finites, simp, atomize)
   2.379 -  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.380 -   prefer 2 apply blast
   2.381 -  apply (subgoal_tac "A x Int UNION F A = {}")
   2.382 -   prefer 2 apply blast
   2.383 -  apply (simp add: setprod_Un_disjoint)
   2.384 -  done
   2.385 +lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
   2.386 +    setprod f B = setprod id (f ` B)"
   2.387 +by (auto simp add: setprod_reindex id_o)
   2.388  
   2.389 -lemma setprod_Union_disjoint:
   2.390 -  "finite C ==> (ALL A:C. finite A) ==>
   2.391 -        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   2.392 -      setprod f (Union C) = setprod (setprod f) C"
   2.393 -  apply (frule setprod_UN_disjoint [of C id f])
   2.394 -  apply (unfold Union_def id_def, assumption+)
   2.395 -  done
   2.396 -
   2.397 -lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A =
   2.398 -    (setprod f A * setprod g A)"
   2.399 -  apply (case_tac "finite A")
   2.400 -   prefer 2 apply (simp add: setprod_def times_ac1)
   2.401 -  apply (erule finite_induct, auto)
   2.402 -  apply (simp add: times_ac1)
   2.403 -  apply (simp add: times_ac1)
   2.404 -  done
   2.405 +lemma setprod_reindex_cong: "finite A ==> inj_on f A ==> 
   2.406 +    B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
   2.407 +  by (frule setprod_reindex, assumption, simp)
   2.408  
   2.409  lemma setprod_cong:
   2.410    "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
   2.411 @@ -1144,30 +1098,79 @@
   2.412    apply (simp add: Ball_def del:insert_Diff_single)
   2.413    done
   2.414  
   2.415 +lemma setprod_1: "setprod (%i. 1) A = 1"
   2.416 +  apply (case_tac "finite A")
   2.417 +  apply (erule finite_induct, auto simp add: times_ac1)
   2.418 +  apply (simp add: setprod_def)
   2.419 +  done
   2.420 +
   2.421  lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
   2.422    apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
   2.423    apply (erule ssubst, rule setprod_1)
   2.424    apply (rule setprod_cong, auto)
   2.425    done
   2.426  
   2.427 -
   2.428 -subsubsection {* Reindexing products *}
   2.429 +lemma setprod_Un_Int: "finite A ==> finite B
   2.430 +    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
   2.431 +  apply (induct set: Finites, simp)
   2.432 +  apply (simp add: times_ac1 insert_absorb)
   2.433 +  apply (simp add: times_ac1 Int_insert_left insert_absorb)
   2.434 +  done
   2.435  
   2.436 -lemma setprod_reindex [rule_format]: "finite B ==>
   2.437 -                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
   2.438 -apply (rule finite_induct, assumption, force)
   2.439 -apply (rule impI, auto)
   2.440 -apply (simp add: inj_on_def)
   2.441 -apply (subgoal_tac "f x \<notin> f ` F")
   2.442 -apply (subgoal_tac "finite (f ` F)")
   2.443 -apply (auto simp add: setprod_insert)
   2.444 -apply (simp add: inj_on_def)
   2.445 +lemma setprod_Un_disjoint: "finite A ==> finite B
   2.446 +  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
   2.447 +  apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
   2.448 +  done
   2.449 +
   2.450 +lemma setprod_UN_disjoint:
   2.451 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   2.452 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.453 +      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
   2.454 +  apply (induct set: Finites, simp, atomize)
   2.455 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.456 +   prefer 2 apply blast
   2.457 +  apply (subgoal_tac "A x Int UNION F A = {}")
   2.458 +   prefer 2 apply blast
   2.459 +  apply (simp add: setprod_Un_disjoint)
   2.460    done
   2.461  
   2.462 -lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
   2.463 -    setprod f B = setprod id (f ` B)"
   2.464 -by (auto simp add: setprod_reindex id_o)
   2.465 +lemma setprod_Union_disjoint:
   2.466 +  "finite C ==> (ALL A:C. finite A) ==>
   2.467 +        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   2.468 +      setprod f (Union C) = setprod (setprod f) C"
   2.469 +  apply (frule setprod_UN_disjoint [of C id f])
   2.470 +  apply (unfold Union_def id_def, assumption+)
   2.471 +  done
   2.472  
   2.473 +lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
   2.474 +    (\<Prod> x:A. (\<Prod> y: B x. f x y)) = 
   2.475 +    (\<Prod> z:(SIGMA x:A. B x). f (fst z) (snd z))"
   2.476 +  apply (subst Sigma_def)
   2.477 +  apply (subst setprod_UN_disjoint)
   2.478 +  apply assumption
   2.479 +  apply (rule ballI)
   2.480 +  apply (drule_tac x = i in bspec, assumption)
   2.481 +  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
   2.482 +  apply (rule finite_surj)
   2.483 +  apply auto
   2.484 +  apply (rule setprod_cong, rule refl)
   2.485 +  apply (subst setprod_UN_disjoint)
   2.486 +  apply (erule bspec, assumption)
   2.487 +  apply auto
   2.488 +  done
   2.489 +
   2.490 +lemma setprod_cartesian_product: "finite A ==> finite B ==> 
   2.491 +    (\<Prod> x:A. (\<Prod> y: B. f x y)) = 
   2.492 +    (\<Prod> z:(A <*> B). f (fst z) (snd z))"
   2.493 +  by (erule setprod_Sigma, auto)
   2.494 +
   2.495 +lemma setprod_timesf: "setprod (%x. f x * g x) A =
   2.496 +    (setprod f A * setprod g A)"
   2.497 +  apply (case_tac "finite A")
   2.498 +   prefer 2 apply (simp add: setprod_def times_ac1)
   2.499 +  apply (erule finite_induct, auto)
   2.500 +  apply (simp add: times_ac1)
   2.501 +  done
   2.502  
   2.503  subsubsection {* Properties in more restricted classes of structures *}
   2.504  
     3.1 --- a/src/HOL/Infinite_Set.thy	Thu Mar 25 10:31:25 2004 +0100
     3.2 +++ b/src/HOL/Infinite_Set.thy	Thu Mar 25 10:32:21 2004 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  
     3.5  header {* Infnite Sets and Related Concepts*}
     3.6  
     3.7 -theory Infinite_Set = Hilbert_Choice + Finite_Set:
     3.8 +theory Infinite_Set = Hilbert_Choice + Finite_Set + SetInterval:
     3.9  
    3.10  subsection "Infinite Sets"
    3.11  
     4.1 --- a/src/HOL/Integ/IntDef.thy	Thu Mar 25 10:31:25 2004 +0100
     4.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Mar 25 10:32:21 2004 +0100
     4.3 @@ -37,7 +37,7 @@
     4.4    One_int_def:   "1 == int 1"
     4.5  
     4.6    minus_int_def:
     4.7 -    "- z ==  contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
     4.8 +    "- z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
     4.9  
    4.10    add_int_def:
    4.11     "z + w ==
    4.12 @@ -82,13 +82,8 @@
    4.13  declare inj_on_Abs_Integ [THEN inj_on_iff, simp]
    4.14          Abs_Integ_inverse [simp]
    4.15  
    4.16 -lemma inj_Rep_Integ: "inj(Rep_Integ)"
    4.17 -apply (rule inj_on_inverseI)
    4.18 -apply (rule Rep_Integ_inverse)
    4.19 -done
    4.20 -
    4.21  text{*Case analysis on the representation of an integer as an equivalence
    4.22 -      class.*}
    4.23 +      class of pairs of naturals.*}
    4.24  lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
    4.25       "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
    4.26  apply (rule Rep_Integ [of z, unfolded Integ_def, THEN quotientE])
    4.27 @@ -952,7 +947,6 @@
    4.28  val equiv_intrel_iff = thm "equiv_intrel_iff";
    4.29  val intrel_in_integ = thm "intrel_in_integ";
    4.30  val inj_on_Abs_Integ = thm "inj_on_Abs_Integ";
    4.31 -val inj_Rep_Integ = thm "inj_Rep_Integ";
    4.32  val inj_int = thm "inj_int";
    4.33  val zminus_zminus = thm "zminus_zminus";
    4.34  val zminus_0 = thm "zminus_0";
     5.1 --- a/src/HOL/Integ/Presburger.thy	Thu Mar 25 10:31:25 2004 +0100
     5.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Mar 25 10:32:21 2004 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  generation for Cooper Algorithm  
     5.5  *)
     5.6  
     5.7 -theory Presburger = NatSimprocs
     5.8 +theory Presburger = NatSimprocs + SetInterval
     5.9  files
    5.10    ("cooper_dec.ML")
    5.11    ("cooper_proof.ML")
     6.1 --- a/src/HOL/NumberTheory/Euler.thy	Thu Mar 25 10:31:25 2004 +0100
     6.2 +++ b/src/HOL/NumberTheory/Euler.thy	Thu Mar 25 10:32:21 2004 +0100
     6.3 @@ -138,7 +138,7 @@
     6.4      also have "... = int(setsum (%x.2) (SetS a p))";
     6.5        apply (insert prems)
     6.6        apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
     6.7 -        card_setsum_aux)
     6.8 +        card_setsum_aux simp del: setsum_constant_nat)
     6.9      done
    6.10      also have "... = 2 * int(card( SetS a p))";
    6.11        by (auto simp add: prems SetS_finite setsum_const2)
    6.12 @@ -342,4 +342,4 @@
    6.13    apply (frule Euler_part1, auto simp add: zcong_sym)
    6.14  done
    6.15  
    6.16 -end;
    6.17 \ No newline at end of file
    6.18 +end
    6.19 \ No newline at end of file
     7.1 --- a/src/HOL/NumberTheory/Finite2.thy	Thu Mar 25 10:31:25 2004 +0100
     7.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Thu Mar 25 10:32:21 2004 +0100
     7.3 @@ -342,7 +342,7 @@
     7.4  apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
     7.5  apply (auto simp only: card_eq_setsum)
     7.6  apply (erule setsum_same_function)
     7.7 -by (auto simp add: card_eq_setsum)
     7.8 +by auto;
     7.9  
    7.10  lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
    7.11      ((\<forall>x \<in> A. finite (g x)) & 
     8.1 --- a/src/HOL/Presburger.thy	Thu Mar 25 10:31:25 2004 +0100
     8.2 +++ b/src/HOL/Presburger.thy	Thu Mar 25 10:32:21 2004 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  generation for Cooper Algorithm  
     8.5  *)
     8.6  
     8.7 -theory Presburger = NatSimprocs
     8.8 +theory Presburger = NatSimprocs + SetInterval
     8.9  files
    8.10    ("cooper_dec.ML")
    8.11    ("cooper_proof.ML")
     9.1 --- a/src/HOL/SetInterval.ML	Thu Mar 25 10:31:25 2004 +0100
     9.2 +++ b/src/HOL/SetInterval.ML	Thu Mar 25 10:32:21 2004 +0100
     9.3 @@ -49,3 +49,7 @@
     9.4  val lessThan_def     = thm "lessThan_def";
     9.5  val lessThan_iff = thm "lessThan_iff";
     9.6  val single_Diff_lessThan = thm "single_Diff_lessThan";
     9.7 +
     9.8 +val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
     9.9 +val finite_atMost = thm "finite_atMost";
    9.10 +val finite_lessThan = thm "finite_lessThan";
    10.1 --- a/src/HOL/SetInterval.thy	Thu Mar 25 10:31:25 2004 +0100
    10.2 +++ b/src/HOL/SetInterval.thy	Thu Mar 25 10:32:21 2004 +0100
    10.3 @@ -1,12 +1,13 @@
    10.4  (*  Title:      HOL/SetInterval.thy
    10.5      ID:         $Id$
    10.6      Author:     Tobias Nipkow and Clemens Ballarin
    10.7 +                Additions by Jeremy Avigad in March 2004
    10.8      Copyright   2000  TU Muenchen
    10.9  
   10.10  lessThan, greaterThan, atLeast, atMost and two-sided intervals
   10.11  *)
   10.12  
   10.13 -theory SetInterval = NatArith:
   10.14 +theory SetInterval = IntArith:
   10.15  
   10.16  constdefs
   10.17    lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
   10.18 @@ -58,23 +59,11 @@
   10.19    "INT i<n. A"  == "INT i:{..n(}. A"
   10.20  
   10.21  
   10.22 -subsection {*lessThan*}
   10.23 +subsection {* Various equivalences *}
   10.24  
   10.25  lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
   10.26  by (simp add: lessThan_def)
   10.27  
   10.28 -lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
   10.29 -by (simp add: lessThan_def)
   10.30 -
   10.31 -lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
   10.32 -by (simp add: lessThan_def less_Suc_eq, blast)
   10.33 -
   10.34 -lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
   10.35 -by (simp add: lessThan_def atMost_def less_Suc_eq_le)
   10.36 -
   10.37 -lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
   10.38 -by blast
   10.39 -
   10.40  lemma Compl_lessThan [simp]: 
   10.41      "!!k:: 'a::linorder. -lessThan k = atLeast k"
   10.42  apply (auto simp add: lessThan_def atLeast_def)
   10.43 @@ -83,24 +72,9 @@
   10.44  lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
   10.45  by auto
   10.46  
   10.47 -subsection {*greaterThan*}
   10.48 -
   10.49  lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
   10.50  by (simp add: greaterThan_def)
   10.51  
   10.52 -lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
   10.53 -apply (simp add: greaterThan_def)
   10.54 -apply (blast dest: gr0_conv_Suc [THEN iffD1])
   10.55 -done
   10.56 -
   10.57 -lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
   10.58 -apply (simp add: greaterThan_def)
   10.59 -apply (auto elim: linorder_neqE)
   10.60 -done
   10.61 -
   10.62 -lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
   10.63 -by blast
   10.64 -
   10.65  lemma Compl_greaterThan [simp]: 
   10.66      "!!k:: 'a::linorder. -greaterThan k = atMost k"
   10.67  apply (simp add: greaterThan_def atMost_def le_def, auto)
   10.68 @@ -111,48 +85,22 @@
   10.69  apply (rule double_complement) 
   10.70  done
   10.71  
   10.72 -
   10.73 -subsection {*atLeast*}
   10.74 -
   10.75  lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
   10.76  by (simp add: atLeast_def)
   10.77  
   10.78 -lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
   10.79 -by (unfold atLeast_def UNIV_def, simp)
   10.80 -
   10.81 -lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
   10.82 -apply (simp add: atLeast_def)
   10.83 -apply (simp add: Suc_le_eq)
   10.84 -apply (simp add: order_le_less, blast)
   10.85 -done
   10.86 -
   10.87 -lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
   10.88 -by blast
   10.89 -
   10.90  lemma Compl_atLeast [simp]: 
   10.91      "!!k:: 'a::linorder. -atLeast k = lessThan k"
   10.92  apply (simp add: lessThan_def atLeast_def le_def, auto)
   10.93  done
   10.94  
   10.95 -
   10.96 -subsection {*atMost*}
   10.97 -
   10.98  lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)"
   10.99  by (simp add: atMost_def)
  10.100  
  10.101 -lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
  10.102 -by (simp add: atMost_def)
  10.103 -
  10.104 -lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
  10.105 -apply (simp add: atMost_def)
  10.106 -apply (simp add: less_Suc_eq order_le_less, blast)
  10.107 -done
  10.108 -
  10.109 -lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
  10.110 -by blast
  10.111 +lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
  10.112 +by (blast intro: order_antisym)
  10.113  
  10.114  
  10.115 -subsection {*Logical Equivalences for Set Inclusion and Equality*}
  10.116 +subsection {* Logical Equivalences for Set Inclusion and Equality *}
  10.117  
  10.118  lemma atLeast_subset_iff [iff]:
  10.119       "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
  10.120 @@ -195,11 +143,6 @@
  10.121  done
  10.122  
  10.123  
  10.124 -subsection {*Combined properties*}
  10.125 -
  10.126 -lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
  10.127 -by (blast intro: order_antisym)
  10.128 -
  10.129  subsection {*Two-sided intervals*}
  10.130  
  10.131  (* greaterThanLessThan *)
  10.132 @@ -208,25 +151,12 @@
  10.133    "(i : {)l..u(}) = (l < i & i < u)"
  10.134  by (simp add: greaterThanLessThan_def)
  10.135  
  10.136 -lemma greaterThanLessThan_0 [simp]: "{)l..0::nat(} == {}"
  10.137 -by (simp add: greaterThanLessThan_def)
  10.138 -
  10.139 -lemma greaterThanLessThan_Suc_greaterThanAtMost:
  10.140 -  "{)l..Suc n(} = {)l..n}"
  10.141 -by (auto simp add: greaterThanLessThan_def greaterThanAtMost_def)
  10.142 -
  10.143  (* atLeastLessThan *)
  10.144  
  10.145  lemma atLeastLessThan_iff [simp]:
  10.146    "(i : {l..u(}) = (l <= i & i < u)"
  10.147  by (simp add: atLeastLessThan_def)
  10.148  
  10.149 -lemma atLeastLessThan_0 [simp]: "{l..0::nat(} == {}"
  10.150 -by (simp add: atLeastLessThan_def)
  10.151 -
  10.152 -lemma atLeastLessThan_Suc_atLeastAtMost: "{l..Suc n(} = {l..n}"
  10.153 -by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
  10.154 -
  10.155  (* greaterThanAtMost *)
  10.156  
  10.157  lemma greaterThanAtMost_iff [simp]:
  10.158 @@ -239,11 +169,226 @@
  10.159    "(i : {l..u}) = (l <= i & i <= u)"
  10.160  by (simp add: atLeastAtMost_def)
  10.161  
  10.162 -
  10.163  (* The above four lemmas could be declared as iffs.
  10.164     If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
  10.165     seems to take forever (more than one hour). *)
  10.166  
  10.167 +
  10.168 +subsection {* Intervals of natural numbers *}
  10.169 +
  10.170 +lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
  10.171 +by (simp add: lessThan_def)
  10.172 +
  10.173 +lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
  10.174 +by (simp add: lessThan_def less_Suc_eq, blast)
  10.175 +
  10.176 +lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
  10.177 +by (simp add: lessThan_def atMost_def less_Suc_eq_le)
  10.178 +
  10.179 +lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
  10.180 +by blast
  10.181 +
  10.182 +lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
  10.183 +apply (simp add: greaterThan_def)
  10.184 +apply (blast dest: gr0_conv_Suc [THEN iffD1])
  10.185 +done
  10.186 +
  10.187 +lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
  10.188 +apply (simp add: greaterThan_def)
  10.189 +apply (auto elim: linorder_neqE)
  10.190 +done
  10.191 +
  10.192 +lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
  10.193 +by blast
  10.194 +
  10.195 +lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
  10.196 +by (unfold atLeast_def UNIV_def, simp)
  10.197 +
  10.198 +lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
  10.199 +apply (simp add: atLeast_def)
  10.200 +apply (simp add: Suc_le_eq)
  10.201 +apply (simp add: order_le_less, blast)
  10.202 +done
  10.203 +
  10.204 +lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
  10.205 +  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
  10.206 +
  10.207 +lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
  10.208 +by blast
  10.209 +
  10.210 +lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
  10.211 +by (simp add: atMost_def)
  10.212 +
  10.213 +lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
  10.214 +apply (simp add: atMost_def)
  10.215 +apply (simp add: less_Suc_eq order_le_less, blast)
  10.216 +done
  10.217 +
  10.218 +lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
  10.219 +by blast
  10.220 +
  10.221 +(* Intervals of nats with Suc *)
  10.222 +
  10.223 +lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
  10.224 +  by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
  10.225 +
  10.226 +lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}"  
  10.227 +  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
  10.228 +    greaterThanAtMost_def)
  10.229 +
  10.230 +lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}"  
  10.231 +  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
  10.232 +    greaterThanLessThan_def)
  10.233 +
  10.234 +subsubsection {* Finiteness *}
  10.235 +
  10.236 +lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
  10.237 +  by (induct k) (simp_all add: lessThan_Suc)
  10.238 +
  10.239 +lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
  10.240 +  by (induct k) (simp_all add: atMost_Suc)
  10.241 +
  10.242 +lemma finite_greaterThanLessThan [iff]:
  10.243 +  fixes l :: nat shows "finite {)l..u(}"
  10.244 +by (simp add: greaterThanLessThan_def)
  10.245 +
  10.246 +lemma finite_atLeastLessThan [iff]:
  10.247 +  fixes l :: nat shows "finite {l..u(}"
  10.248 +by (simp add: atLeastLessThan_def)
  10.249 +
  10.250 +lemma finite_greaterThanAtMost [iff]:
  10.251 +  fixes l :: nat shows "finite {)l..u}"
  10.252 +by (simp add: greaterThanAtMost_def)
  10.253 +
  10.254 +lemma finite_atLeastAtMost [iff]:
  10.255 +  fixes l :: nat shows "finite {l..u}"
  10.256 +by (simp add: atLeastAtMost_def)
  10.257 +
  10.258 +lemma bounded_nat_set_is_finite:
  10.259 +    "(ALL i:N. i < (n::nat)) ==> finite N"
  10.260 +  -- {* A bounded set of natural numbers is finite. *}
  10.261 +  apply (rule finite_subset)
  10.262 +   apply (rule_tac [2] finite_lessThan, auto)
  10.263 +  done
  10.264 +
  10.265 +subsubsection {* Cardinality *}
  10.266 +
  10.267 +lemma card_lessThan [simp]: "card {..u(} = u"
  10.268 +  by (induct_tac u, simp_all add: lessThan_Suc)
  10.269 +
  10.270 +lemma card_atMost [simp]: "card {..u} = Suc u"
  10.271 +  by (simp add: lessThan_Suc_atMost [THEN sym])
  10.272 +
  10.273 +lemma card_atLeastLessThan [simp]: "card {l..u(} = u - l"
  10.274 +  apply (subgoal_tac "card {l..u(} = card {..u-l(}")
  10.275 +  apply (erule ssubst, rule card_lessThan)
  10.276 +  apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {l..u(}")
  10.277 +  apply (erule subst)
  10.278 +  apply (rule card_image)
  10.279 +  apply (rule finite_lessThan)
  10.280 +  apply (simp add: inj_on_def)
  10.281 +  apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
  10.282 +  apply arith
  10.283 +  apply (rule_tac x = "x - l" in exI)
  10.284 +  apply arith
  10.285 +  done
  10.286 +
  10.287 +lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
  10.288 +  by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
  10.289 +
  10.290 +lemma card_greaterThanAtMost [simp]: "card {)l..u} = u - l" 
  10.291 +  by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
  10.292 +
  10.293 +lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u - Suc l"
  10.294 +  by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
  10.295 +
  10.296 +subsection {* Intervals of integers *}
  10.297 +
  10.298 +lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}"
  10.299 +  by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
  10.300 +
  10.301 +lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}"  
  10.302 +  by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
  10.303 +
  10.304 +lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
  10.305 +    "{l+1..u(} = {)l..(u::int)(}"  
  10.306 +  by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
  10.307 +
  10.308 +subsubsection {* Finiteness *}
  10.309 +
  10.310 +lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
  10.311 +    {(0::int)..u(} = int ` {..nat u(}"
  10.312 +  apply (unfold image_def lessThan_def)
  10.313 +  apply auto
  10.314 +  apply (rule_tac x = "nat x" in exI)
  10.315 +  apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
  10.316 +  done
  10.317 +
  10.318 +lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}"
  10.319 +  apply (case_tac "0 \<le> u")
  10.320 +  apply (subst image_atLeastZeroLessThan_int, assumption)
  10.321 +  apply (rule finite_imageI)
  10.322 +  apply auto
  10.323 +  apply (subgoal_tac "{0..u(} = {}")
  10.324 +  apply auto
  10.325 +  done
  10.326 +
  10.327 +lemma image_atLeastLessThan_int_shift: 
  10.328 +    "(%x. x + (l::int)) ` {0..u-l(} = {l..u(}"
  10.329 +  apply (auto simp add: image_def atLeastLessThan_iff)
  10.330 +  apply (rule_tac x = "x - l" in bexI)
  10.331 +  apply auto
  10.332 +  done
  10.333 +
  10.334 +lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}"
  10.335 +  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
  10.336 +  apply (erule subst)
  10.337 +  apply (rule finite_imageI)
  10.338 +  apply (rule finite_atLeastZeroLessThan_int)
  10.339 +  apply (rule image_atLeastLessThan_int_shift)
  10.340 +  done
  10.341 +
  10.342 +lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
  10.343 +  by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
  10.344 +
  10.345 +lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}" 
  10.346 +  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
  10.347 +
  10.348 +lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}" 
  10.349 +  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
  10.350 +
  10.351 +subsubsection {* Cardinality *}
  10.352 +
  10.353 +lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u"
  10.354 +  apply (case_tac "0 \<le> u")
  10.355 +  apply (subst image_atLeastZeroLessThan_int, assumption)
  10.356 +  apply (subst card_image)
  10.357 +  apply (auto simp add: inj_on_def)
  10.358 +  done
  10.359 +
  10.360 +lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u - l)"
  10.361 +  apply (subgoal_tac "card {l..u(} = card {0..u-l(}")
  10.362 +  apply (erule ssubst, rule card_atLeastZeroLessThan_int)
  10.363 +  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
  10.364 +  apply (erule subst)
  10.365 +  apply (rule card_image)
  10.366 +  apply (rule finite_atLeastZeroLessThan_int)
  10.367 +  apply (simp add: inj_on_def)
  10.368 +  apply (rule image_atLeastLessThan_int_shift)
  10.369 +  done
  10.370 +
  10.371 +lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
  10.372 +  apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
  10.373 +  apply (auto simp add: compare_rls)
  10.374 +  done
  10.375 +
  10.376 +lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u - l)" 
  10.377 +  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
  10.378 +
  10.379 +lemma card_greaterThanLessThan_int [simp]: "card {)l..u(} = nat (u - (l + 1))"
  10.380 +  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
  10.381 +
  10.382 +
  10.383  subsection {*Lemmas useful with the summation operator setsum*}
  10.384  
  10.385  (* For examples, see Algebra/poly/UnivPoly.thy *)