--- a/src/HOL/Set_Interval.thy Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Set_Interval.thy Sat Jul 02 08:41:05 2016 +0200
@@ -14,7 +14,7 @@
section \<open>Set intervals\<close>
theory Set_Interval
-imports Lattices_Big Nat_Transfer
+imports Lattices_Big Divides Nat_Transfer
begin
context ord
@@ -901,6 +901,16 @@
qed
qed
+corollary image_Suc_lessThan:
+ "Suc ` {..<n} = {1..n}"
+ using image_add_atLeastLessThan [of 1 0 n]
+ by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
+
+corollary image_Suc_atMost:
+ "Suc ` {..n} = {1..Suc n}"
+ using image_add_atLeastLessThan [of 1 0 "Suc n"]
+ by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
+
corollary image_Suc_atLeastAtMost[simp]:
"Suc ` {i..j} = {Suc i..Suc j}"
using image_add_atLeastAtMost[where k="Suc 0"] by simp
@@ -909,6 +919,14 @@
"Suc ` {i..<j} = {Suc i..<Suc j}"
using image_add_atLeastLessThan[where k="Suc 0"] by simp
+lemma atLeast1_lessThan_eq_remove0:
+ "{Suc 0..<n} = {..<n} - {0}"
+ by auto
+
+lemma atLeast1_atMost_eq_remove0:
+ "{Suc 0..n} = {..n} - {0}"
+ by auto
+
lemma image_add_int_atLeastLessThan:
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
apply (auto simp add: image_def)
@@ -1146,6 +1164,12 @@
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
+lemma subset_eq_range_finite:
+ fixes n :: nat
+ assumes "N \<subseteq> {..<n}"
+ shows "finite N"
+ using assms finite_lessThan by (rule finite_subset)
+
lemma ex_bij_betw_nat_finite:
"finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
apply(drule finite_imp_nat_seg_image_inj_on)
@@ -1156,6 +1180,18 @@
"finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
+lemma bij_betw_nat_finite:
+ assumes "finite A"
+ obtains f where "bij_betw f {..<card A} A"
+proof -
+ from assms obtain f where "bij_betw f {0..<card A} A"
+ by (blast dest: ex_bij_betw_nat_finite)
+ also have "{0..<card A} = {..<card A}"
+ by auto
+ finally show thesis using that
+ by blast
+qed
+
lemma finite_same_card_bij:
"finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
apply(drule ex_bij_betw_finite_nat)
@@ -1200,6 +1236,17 @@
ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
qed (insert assms, auto)
+lemma subset_eq_range_card:
+ fixes n :: nat
+ assumes "N \<subseteq> {..<n}"
+ shows "card N \<le> n"
+proof -
+ from assms finite_lessThan have "card N \<le> card {..<n}"
+ using card_mono by blast
+ then show ?thesis by simp
+qed
+
+
subsection \<open>Intervals of integers\<close>
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
@@ -1665,11 +1712,15 @@
"(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
by (induction n) (auto simp: setsum.distrib)
-lemma setsum_zero_power' [simp]:
- fixes c :: "nat \<Rightarrow> 'a::field"
- shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
- using setsum_zero_power [of "\<lambda>i. c i / d i" A]
- by auto
+lemma setsum_atLeast1_atMost_eq:
+ "setsum f {Suc 0..n} = (\<Sum>k<n. f (Suc k))"
+proof -
+ have "setsum f {Suc 0..n} = setsum f (Suc ` {..<n})"
+ by (simp add: image_Suc_lessThan)
+ also have "\<dots> = (\<Sum>k<n. f (Suc k))"
+ by (simp add: setsum.reindex)
+ finally show ?thesis .
+qed
subsection \<open>Telescoping\<close>
@@ -1923,6 +1974,29 @@
qed
+subsection \<open>Division remainder\<close>
+
+lemma range_mod:
+ fixes n :: nat
+ assumes "n > 0"
+ shows "range (\<lambda>m. m mod n) = {0..<n}" (is "?A = ?B")
+proof (rule set_eqI)
+ fix m
+ show "m \<in> ?A \<longleftrightarrow> m \<in> ?B"
+ proof
+ assume "m \<in> ?A"
+ with assms show "m \<in> ?B"
+ by auto
+ next
+ assume "m \<in> ?B"
+ moreover have "m mod n \<in> ?A"
+ by (rule rangeI)
+ ultimately show "m \<in> ?A"
+ by simp
+ qed
+qed
+
+
subsection \<open>Efficient folding over intervals\<close>
function fold_atLeastAtMost_nat where