--- a/src/HOL/Binomial.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Binomial.thy Sat Jan 13 09:18:54 2018 +0000
@@ -322,7 +322,7 @@
shows "(\<Sum>k=0..m. (n - k) choose (m - k)) = Suc n choose m"
proof -
have "(\<Sum>k=0..m. (n-k) choose (m - k)) = (\<Sum>k=0..m. (n - m + k) choose k)"
- using sum.atLeast_atMost_rev [of "\<lambda>k. (n - k) choose (m - k)" 0 m] assms
+ using sum.atLeastAtMost_rev [of "\<lambda>k. (n - k) choose (m - k)" 0 m] assms
by simp
also have "\<dots> = Suc (n - m + m) choose m"
by (rule sum_choose_lower)
@@ -940,7 +940,7 @@
also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m - k)))"
by (intro sum.cong[OF refl], subst binomial_symmetric) simp_all
also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))"
- using sum.atLeast_atMost_rev [of "\<lambda>k. 2 * m + 1 choose (m - k)" 0 m]
+ using sum.atLeastAtMost_rev [of "\<lambda>k. 2 * m + 1 choose (m - k)" 0 m]
by simp
also have "\<dots> + \<dots> = 2 * \<dots>"
by simp
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sat Jan 13 09:18:54 2018 +0000
@@ -4238,7 +4238,7 @@
apply (simp add: pochhammer_minus field_simps)
using \<open>k \<le> n\<close> apply (simp add: fact_split [of k n])
apply (simp add: pochhammer_prod)
- using prod.atLeast_lessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
+ using prod.atLeastLessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
apply (auto simp add: of_nat_diff field_simps)
done
have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}"
@@ -4247,7 +4247,7 @@
done
have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift)
- using prod.atLeast_atMost_shift_0 [of "m - h" m, where ?'a = 'a]
+ using prod.atLeastAtMost_shift_0 [of "m - h" m, where ?'a = 'a]
apply (auto simp add: of_nat_diff field_simps)
done
have "?m1 n * ?p b n =
--- a/src/HOL/Factorial.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Factorial.thy Sat Jan 13 09:18:54 2018 +0000
@@ -26,7 +26,7 @@
atLeastLessThanSuc_atLeastAtMost)
lemma fact_prod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
- using prod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
+ using prod.atLeastAtMost_rev [of "\<lambda>i. i" 1 n]
by (cases n)
(simp_all add: fact_prod_Suc prod.atLeast_Suc_atMost_Suc_shift
atLeastLessThanSuc_atLeastAtMost)
@@ -191,7 +191,7 @@
where pochhammer_prod: "pochhammer a n = prod (\<lambda>i. a + of_nat i) {0..<n}"
lemma pochhammer_prod_rev: "pochhammer a n = prod (\<lambda>i. a + of_nat (n - i)) {1..n}"
- using prod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
+ using prod.atLeastLessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
by (simp add: pochhammer_prod)
lemma pochhammer_Suc_prod: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat i) {0..n}"
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Sat Jan 13 09:18:54 2018 +0000
@@ -42,7 +42,7 @@
have "(\<Sum>j<k + i. f j) = (\<Sum>j=i..<k + i. f j) + (\<Sum>j=0..<i. f j)"
by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
also have "(\<Sum>j=i..<k + i. f j) = (\<Sum>j\<in>(\<lambda>n. n + i)`{0..<k}. f j)"
- unfolding image_add_atLeast_lessThan by simp
+ unfolding image_add_atLeastLessThan by simp
finally have "(\<Sum>j<k + i. f j) = (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)"
by (auto simp: inj_on_def atLeast0LessThan sum.reindex) }
ultimately have "(\<lambda>k. (\<Sum>n<k + i. f n)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"
--- a/src/HOL/Library/Numeral_Type.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sat Jan 13 09:18:54 2018 +0000
@@ -415,7 +415,7 @@
show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
- by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeast_lessThan)
+ by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
(auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def)
fix P :: "'a bit0 \<Rightarrow> bool"
@@ -439,7 +439,7 @@
show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
- by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeast_lessThan)
+ by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
(auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def)
fix P :: "'a bit1 \<Rightarrow> bool"
--- a/src/HOL/Library/Uprod.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Library/Uprod.thy Sat Jan 13 09:18:54 2018 +0000
@@ -209,7 +209,7 @@
also have "\<dots> = sum Suc {0..<?A}"
by (subst card_SigmaI) simp_all
also have "\<dots> = sum of_nat {Suc 0..?A}"
- using sum.atLeast_lessThan_reindex [symmetric, of Suc 0 ?A id]
+ using sum.atLeastLessThan_reindex [symmetric, of Suc 0 ?A id]
by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
also have "\<dots> = ?A * (?A + 1) div 2"
using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
--- a/src/HOL/Set_Interval.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Set_Interval.thy Sat Jan 13 09:18:54 2018 +0000
@@ -218,7 +218,7 @@
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
by auto
-lemma (in order) atLeast_lessThan_eq_atLeast_atMost_diff:
+lemma (in order) atLeastLessThan_eq_atLeastAtMost_diff:
"{a..<b} = {a..b} - {b}"
by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
@@ -869,7 +869,7 @@
context linordered_semidom
begin
-lemma image_add_atLeast_atMost [simp]:
+lemma image_add_atLeastAtMost [simp]:
"plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
proof
show "?A \<subseteq> ?B"
@@ -899,28 +899,28 @@
qed
qed
-lemma image_add_atLeast_atMost' [simp]:
+lemma image_add_atLeastAtMost' [simp]:
"(\<lambda>n. n + k) ` {i..j} = {i + k..j + k}"
by (simp add: add.commute [of _ k])
-lemma image_add_atLeast_lessThan [simp]:
+lemma image_add_atLeastLessThan [simp]:
"plus k ` {i..<j} = {i + k..<j + k}"
- by (simp add: image_set_diff atLeast_lessThan_eq_atLeast_atMost_diff ac_simps)
-
-lemma image_add_atLeast_lessThan' [simp]:
+ by (simp add: image_set_diff atLeastLessThan_eq_atLeastAtMost_diff ac_simps)
+
+lemma image_add_atLeastLessThan' [simp]:
"(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
by (simp add: add.commute [of _ k])
end
-lemma image_Suc_atLeast_atMost [simp]:
+lemma image_Suc_atLeastAtMost [simp]:
"Suc ` {i..j} = {Suc i..Suc j}"
- using image_add_atLeast_atMost [of 1 i j]
+ using image_add_atLeastAtMost [of 1 i j]
by (simp only: plus_1_eq_Suc) simp
-lemma image_Suc_atLeast_lessThan [simp]:
+lemma image_Suc_atLeastLessThan [simp]:
"Suc ` {i..<j} = {Suc i..<Suc j}"
- using image_add_atLeast_lessThan [of 1 i j]
+ using image_add_atLeastLessThan [of 1 i j]
by (simp only: plus_1_eq_Suc) simp
corollary image_Suc_atMost:
@@ -1009,11 +1009,11 @@
qed
qed auto
-lemma image_int_atLeast_lessThan:
+lemma image_int_atLeastLessThan:
"int ` {a..<b} = {int a..<int b}"
by (auto intro!: image_eqI [where x = "nat x" for x])
-lemma image_int_atLeast_atMost:
+lemma image_int_atLeastAtMost:
"int ` {a..b} = {int a..int b}"
by (auto intro!: image_eqI [where x = "nat x" for x])
@@ -1568,7 +1568,7 @@
context comm_monoid_set
begin
-lemma atLeast_lessThan_reindex:
+lemma atLeastLessThan_reindex:
"F g {h m..<h n} = F (g \<circ> h) {m..<n}"
if "bij_betw h {m..<n} {h m..<h n}" for m n ::nat
proof -
@@ -1578,7 +1578,7 @@
using reindex [of h "{m..<n}" g] by simp
qed
-lemma atLeast_atMost_reindex:
+lemma atLeastAtMost_reindex:
"F g {h m..h n} = F (g \<circ> h) {m..n}"
if "bij_betw h {m..n} {h m..h n}" for m n ::nat
proof -
@@ -1588,37 +1588,37 @@
using reindex [of h "{m..n}" g] by simp
qed
-lemma atLeast_lessThan_shift_bounds:
+lemma atLeastLessThan_shift_bounds:
"F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
for m n k :: nat
- using atLeast_lessThan_reindex [of "plus k" m n g]
+ using atLeastLessThan_reindex [of "plus k" m n g]
by (simp add: ac_simps)
-lemma atLeast_atMost_shift_bounds:
+lemma atLeastAtMost_shift_bounds:
"F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
for m n k :: nat
- using atLeast_atMost_reindex [of "plus k" m n g]
+ using atLeastAtMost_reindex [of "plus k" m n g]
by (simp add: ac_simps)
lemma atLeast_Suc_lessThan_Suc_shift:
"F g {Suc m..<Suc n} = F (g \<circ> Suc) {m..<n}"
- using atLeast_lessThan_shift_bounds [of _ _ 1]
+ using atLeastLessThan_shift_bounds [of _ _ 1]
by (simp add: plus_1_eq_Suc)
lemma atLeast_Suc_atMost_Suc_shift:
"F g {Suc m..Suc n} = F (g \<circ> Suc) {m..n}"
- using atLeast_atMost_shift_bounds [of _ _ 1]
+ using atLeastAtMost_shift_bounds [of _ _ 1]
by (simp add: plus_1_eq_Suc)
lemma atLeast_int_lessThan_int_shift:
"F g {int m..<int n} = F (g \<circ> int) {m..<n}"
- by (rule atLeast_lessThan_reindex)
- (simp add: image_int_atLeast_lessThan)
+ by (rule atLeastLessThan_reindex)
+ (simp add: image_int_atLeastLessThan)
lemma atLeast_int_atMost_int_shift:
"F g {int m..int n} = F (g \<circ> int) {m..n}"
- by (rule atLeast_atMost_reindex)
- (simp add: image_int_atLeast_atMost)
+ by (rule atLeastAtMost_reindex)
+ (simp add: image_int_atLeastAtMost)
lemma atLeast0_lessThan_Suc:
"F g {0..<Suc n} = F g {0..<n} \<^bold>* g n"
@@ -1641,35 +1641,35 @@
\<Longrightarrow> F g {a..<b} = F h {c..<d}"
by (rule cong) simp_all
-lemma atLeast_lessThan_shift_0:
+lemma atLeastLessThan_shift_0:
fixes m n p :: nat
shows "F g {m..<n} = F (g \<circ> plus m) {0..<n - m}"
- using atLeast_lessThan_shift_bounds [of g 0 m "n - m"]
+ using atLeastLessThan_shift_bounds [of g 0 m "n - m"]
by (cases "m \<le> n") simp_all
-lemma atLeast_atMost_shift_0:
+lemma atLeastAtMost_shift_0:
fixes m n p :: nat
assumes "m \<le> n"
shows "F g {m..n} = F (g \<circ> plus m) {0..n - m}"
- using assms atLeast_atMost_shift_bounds [of g 0 m "n - m"] by simp
-
-lemma atLeast_lessThan_concat:
+ using assms atLeastAtMost_shift_bounds [of g 0 m "n - m"] by simp
+
+lemma atLeastLessThan_concat:
fixes m n p :: nat
shows "m \<le> n \<Longrightarrow> n \<le> p \<Longrightarrow> F g {m..<n} \<^bold>* F g {n..<p} = F g {m..<p}"
by (simp add: union_disjoint [symmetric] ivl_disj_un)
-lemma atLeast_lessThan_rev:
+lemma atLeastLessThan_rev:
"F g {n..<m} = F (\<lambda>i. g (m + n - Suc i)) {n..<m}"
by (rule reindex_bij_witness [where i="\<lambda>i. m + n - Suc i" and j="\<lambda>i. m + n - Suc i"], auto)
-lemma atLeast_atMost_rev:
+lemma atLeastAtMost_rev:
fixes n m :: nat
shows "F g {n..m} = F (\<lambda>i. g (m + n - i)) {n..m}"
by (rule reindex_bij_witness [where i="\<lambda>i. m + n - i" and j="\<lambda>i. m + n - i"]) auto
-lemma atLeast_lessThan_rev_at_least_Suc_atMost:
+lemma atLeastLessThan_rev_at_least_Suc_atMost:
"F g {n..<m} = F (\<lambda>i. g (m + n - i)) {Suc n..m}"
- unfolding atLeast_lessThan_rev [of g n m]
+ unfolding atLeastLessThan_rev [of g n m]
by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)
end
@@ -1792,7 +1792,7 @@
atLeastSucAtMost_greaterThanAtMost)
qed
-lemmas sum_add_nat_ivl = sum.atLeast_lessThan_concat
+lemmas sum_add_nat_ivl = sum.atLeastLessThan_concat
lemma sum_diff_nat_ivl:
fixes f :: "nat \<Rightarrow> 'a::ab_group_add"