integrated Jeremy's FiniteLib
authornipkow
Tue Mar 01 18:48:52 2005 +0100 (2005-03-01)
changeset 1555403d4347b071d
parent 15553 2b3f9c493259
child 15555 9d4dbd18ff2d
integrated Jeremy's FiniteLib
src/HOL/Finite_Set.thy
src/HOL/Integ/IntDef.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 01 05:44:13 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 01 18:48:52 2005 +0100
     1.3 @@ -895,8 +895,11 @@
     1.4    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
     1.5  by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
     1.6  
     1.7 +lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
     1.8 +  by (rule setsum_cong[OF refl], auto);
     1.9 +
    1.10  lemma setsum_reindex_cong:
    1.11 -     "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
    1.12 +     "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
    1.13        ==> setsum h B = setsum g A"
    1.14    by (simp add: setsum_reindex cong: setsum_cong)
    1.15  
    1.16 @@ -1066,6 +1069,17 @@
    1.17      by (simp add: setsum_def)
    1.18  qed
    1.19  
    1.20 +lemma setsum_strict_mono:
    1.21 +fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
    1.22 +assumes fin_ne: "finite A"  "A \<noteq> {}"
    1.23 +shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A"
    1.24 +using fin_ne
    1.25 +proof (induct rule: finite_ne_induct)
    1.26 +  case singleton thus ?case by simp
    1.27 +next
    1.28 +  case insert thus ?case by (auto simp: add_strict_mono)
    1.29 +qed
    1.30 +
    1.31  lemma setsum_negf:
    1.32   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
    1.33  proof (cases "finite A")
     2.1 --- a/src/HOL/Integ/IntDef.thy	Tue Mar 01 05:44:13 2005 +0100
     2.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Mar 01 18:48:52 2005 +0100
     2.3 @@ -764,31 +764,31 @@
     2.4  text{*By Jeremy Avigad*}
     2.5  
     2.6  
     2.7 -lemma setsum_of_nat: "of_nat (setsum f A) = setsum (of_nat \<circ> f) A"
     2.8 +lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
     2.9    apply (case_tac "finite A")
    2.10    apply (erule finite_induct, auto)
    2.11    done
    2.12  
    2.13 -lemma setsum_of_int: "of_int (setsum f A) = setsum (of_int \<circ> f) A"
    2.14 +lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    2.15    apply (case_tac "finite A")
    2.16    apply (erule finite_induct, auto)
    2.17    done
    2.18  
    2.19 -lemma int_setsum: "int (setsum f A) = setsum (int \<circ> f) A"
    2.20 -  by (simp add: int_eq_of_nat setsum_of_nat) 
    2.21 +lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
    2.22 +  by (simp add: int_eq_of_nat of_nat_setsum)
    2.23  
    2.24 -lemma setprod_of_nat: "of_nat (setprod f A) = setprod (of_nat \<circ> f) A"
    2.25 +lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    2.26    apply (case_tac "finite A")
    2.27    apply (erule finite_induct, auto)
    2.28    done
    2.29  
    2.30 -lemma setprod_of_int: "of_int (setprod f A) = setprod (of_int \<circ> f) A"
    2.31 +lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    2.32    apply (case_tac "finite A")
    2.33    apply (erule finite_induct, auto)
    2.34    done
    2.35  
    2.36 -lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
    2.37 -  by (simp add: int_eq_of_nat setprod_of_nat)
    2.38 +lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
    2.39 +  by (simp add: int_eq_of_nat of_nat_setprod)
    2.40  
    2.41  lemma setprod_nonzero_nat:
    2.42      "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
     3.1 --- a/src/HOL/Set.thy	Tue Mar 01 05:44:13 2005 +0100
     3.2 +++ b/src/HOL/Set.thy	Tue Mar 01 18:48:52 2005 +0100
     3.3 @@ -520,6 +520,10 @@
     3.4    apply (rule Collect_mem_eq)
     3.5    done
     3.6  
     3.7 +(* Due to Brian Huffman *)
     3.8 +lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
     3.9 +by(auto intro:set_ext)
    3.10 +
    3.11  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
    3.12    -- {* Anti-symmetry of the subset relation. *}
    3.13    by (rules intro: set_ext subsetD)
     4.1 --- a/src/HOL/SetInterval.thy	Tue Mar 01 05:44:13 2005 +0100
     4.2 +++ b/src/HOL/SetInterval.thy	Tue Mar 01 18:48:52 2005 +0100
     4.3 @@ -168,26 +168,18 @@
     4.4  
     4.5  subsection {*Two-sided intervals*}
     4.6  
     4.7 -text {* @{text greaterThanLessThan} *}
     4.8 -
     4.9  lemma greaterThanLessThan_iff [simp]:
    4.10    "(i : {l<..<u}) = (l < i & i < u)"
    4.11  by (simp add: greaterThanLessThan_def)
    4.12  
    4.13 -text {* @{text atLeastLessThan} *}
    4.14 -
    4.15  lemma atLeastLessThan_iff [simp]:
    4.16    "(i : {l..<u}) = (l <= i & i < u)"
    4.17  by (simp add: atLeastLessThan_def)
    4.18  
    4.19 -text {* @{text greaterThanAtMost} *}
    4.20 -
    4.21  lemma greaterThanAtMost_iff [simp]:
    4.22    "(i : {l<..u}) = (l < i & i <= u)"
    4.23  by (simp add: greaterThanAtMost_def)
    4.24  
    4.25 -text {* @{text atLeastAtMost} *}
    4.26 -
    4.27  lemma atLeastAtMost_iff [simp]:
    4.28    "(i : {l..u}) = (l <= i & i <= u)"
    4.29  by (simp add: atLeastAtMost_def)
    4.30 @@ -196,6 +188,16 @@
    4.31    If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
    4.32    seems to take forever (more than one hour). *}
    4.33  
    4.34 +subsubsection{* Emptyness and singletons *}
    4.35 +
    4.36 +lemma atLeastAtMost_empty [simp]: "n < m ==> {m::'a::order..n} = {}";
    4.37 +  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
    4.38 +
    4.39 +lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n::'a::order} = {}"
    4.40 +by (auto simp add: atLeastLessThan_def)
    4.41 +
    4.42 +lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}";
    4.43 +  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
    4.44  
    4.45  subsection {* Intervals of natural numbers *}
    4.46  
    4.47 @@ -268,12 +270,6 @@
    4.48  lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
    4.49  by (simp add: atLeastLessThan_def)
    4.50  
    4.51 -lemma atLeastLessThan_self [simp]: "{n::'a::order..<n} = {}"
    4.52 -by (auto simp add: atLeastLessThan_def)
    4.53 -
    4.54 -lemma atLeastLessThan_empty: "n \<le> m ==> {m..<n::'a::order} = {}"
    4.55 -by (auto simp add: atLeastLessThan_def)
    4.56 -
    4.57  subsubsection {* Intervals of nats with @{term Suc} *}
    4.58  
    4.59  text{*Not a simprule because the RHS is too messy.*}
    4.60 @@ -301,6 +297,9 @@
    4.61    by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
    4.62      greaterThanLessThan_def)
    4.63  
    4.64 +lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
    4.65 +by (auto simp add: atLeastAtMost_def)
    4.66 +
    4.67  subsubsection {* Finiteness *}
    4.68  
    4.69  lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
    4.70 @@ -389,8 +388,6 @@
    4.71    apply (subst image_atLeastZeroLessThan_int, assumption)
    4.72    apply (rule finite_imageI)
    4.73    apply auto
    4.74 -  apply (subgoal_tac "{0..<u} = {}")
    4.75 -  apply auto
    4.76    done
    4.77  
    4.78  lemma image_atLeastLessThan_int_shift:
    4.79 @@ -615,8 +612,14 @@
    4.80   setsum f {a..<b} = setsum g {c..<d}"
    4.81  by(rule setsum_cong, simp_all)
    4.82  
    4.83 +lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
    4.84 +    (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
    4.85 +by (auto simp:add_ac atLeastAtMostSuc_conv)
    4.86 +
    4.87 +(* FIXME delete
    4.88  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    4.89  by (simp add:lessThan_Suc)
    4.90 +*)
    4.91  
    4.92  lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    4.93    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"