diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -222,6 +222,10 @@
   "{a..<b} = {a..b} - {b}"
   by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
 
+lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff:
+  "{a<..b} = {a..b} - {a}"
+  by (auto simp add: greaterThanAtMost_def atLeastAtMost_def)
+
 end
 
 subsubsection\<open>Emptyness, singletons, subset\<close>
@@ -869,6 +873,19 @@
 context linordered_semidom
 begin
 
+lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}"
+proof -
+  have "n = k + (n - k)" if "i + k \<le> n" for n
+  proof -
+    have "n = (n - (k + i)) + (k + i)" using that
+      by (metis add_commute le_add_diff_inverse)
+    then show "n = k + (n - k)"
+      by (metis local.add_diff_cancel_left' add_assoc add_commute)
+  qed
+  then show ?thesis
+    by (fastforce simp: add_le_imp_le_diff add.commute)
+qed
+
 lemma image_add_atLeastAtMost [simp]:
   "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
 proof
@@ -911,112 +928,11 @@
   "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
   by (simp add: add.commute [of _ k])
 
+lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}"
+  by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps)
+
 end
 
-lemma image_Suc_atLeastAtMost [simp]:
-  "Suc ` {i..j} = {Suc i..Suc j}"
-  using image_add_atLeastAtMost [of 1 i j]
-    by (simp only: plus_1_eq_Suc) simp
-
-lemma image_Suc_atLeastLessThan [simp]:
-  "Suc ` {i..<j} = {Suc i..<Suc j}"
-  using image_add_atLeastLessThan [of 1 i j]
-    by (simp only: plus_1_eq_Suc) simp
-
-corollary image_Suc_atMost:
-  "Suc ` {..n} = {1..Suc n}"
-  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-
-corollary image_Suc_lessThan:
-  "Suc ` {..<n} = {1..n}"
-  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-  
-lemma image_diff_atLeastAtMost [simp]:
-  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
-  apply auto
-  apply (rule_tac x="d-x" in rev_image_eqI, auto)
-  done
-
-lemma image_mult_atLeastAtMost [simp]:
-  fixes d::"'a::linordered_field"
-  assumes "d>0" shows "(( * ) d ` {a..b}) = {d*a..d*b}"
-  using assms
-  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
-
-lemma image_affinity_atLeastAtMost:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {m*a + c .. m *b + c}
-            else {m*b + c .. m*a + c})"
-  apply (case_tac "m=0", auto simp: mult_le_cancel_left)
-  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
-  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
-  done
-
-lemma image_affinity_atLeastAtMost_diff:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {m*a - c .. m*b - c}
-            else {m*b - c .. m*a - c})"
-  using image_affinity_atLeastAtMost [of m "-c" a b]
-  by simp
-
-lemma image_affinity_atLeastAtMost_div:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {a/m + c .. b/m + c}
-            else {b/m + c .. a/m + c})"
-  using image_affinity_atLeastAtMost [of "inverse m" c a b]
-  by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma image_affinity_atLeastAtMost_div_diff:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {a/m - c .. b/m - c}
-            else {b/m - c .. a/m - c})"
-  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
-  by (simp add: field_class.field_divide_inverse algebra_simps)
-
-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)
-  apply (rule_tac x = "x - l" in bexI)
-  apply auto
-  done
-
-lemma image_minus_const_atLeastLessThan_nat:
-  fixes c :: nat
-  shows "(\<lambda>i. i - c) ` {x ..< y} =
-      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
-    (is "_ = ?right")
-proof safe
-  fix a assume a: "a \<in> ?right"
-  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
-  proof cases
-    assume "c < y" with a show ?thesis
-      by (auto intro!: image_eqI[of _ _ "a + c"])
-  next
-    assume "\<not> c < y" with a show ?thesis
-      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
-  qed
-qed auto
-
-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_atLeastAtMost:
-  "int ` {a..b} = {int a..int b}"
-  by (auto intro!: image_eqI [where x = "nat x" for x])
-
 context ordered_ab_group_add
 begin
 
@@ -1057,8 +973,184 @@
   and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
   by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
       greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
+
+lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}"
+  by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps)
+
 end
 
+lemma image_Suc_atLeastAtMost [simp]:
+  "Suc ` {i..j} = {Suc i..Suc j}"
+  using image_add_atLeastAtMost [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+lemma image_Suc_atLeastLessThan [simp]:
+  "Suc ` {i..<j} = {Suc i..<Suc j}"
+  using image_add_atLeastLessThan [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+corollary image_Suc_atMost:
+  "Suc ` {..n} = {1..Suc n}"
+  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+corollary image_Suc_lessThan:
+  "Suc ` {..<n} = {1..n}"
+  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+lemma image_diff_atLeastAtMost [simp]:
+  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
+  apply auto
+  apply (rule_tac x="d-x" in rev_image_eqI, auto)
+  done
+
+lemma image_diff_atLeastLessThan [simp]:
+  fixes a b c::"'a::linordered_idom"
+  shows "(-) c ` {a..<b} = {c - b<..c - a}"
+proof -
+  have "(-) c ` {a..<b} = (+) c ` uminus ` {a ..<b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b<..c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_greaterThanAtMost_real[simp]:
+  fixes a b c::"'a::linordered_idom"
+  shows "(-) c ` {a<..b} = {c - b..<c - a}"
+proof -
+  have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b..<c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_atLeast_real[simp]:
+  fixes a c::"'a::linordered_idom"
+  shows "(-) c ` {a..} = {..c - a}"
+proof -
+  have "(-) c ` {a..} = (+) c ` uminus ` {a ..}"
+    unfolding image_image by simp
+  also have "\<dots> = {..c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_AtMost_real[simp]:
+  fixes b c::"'a::linordered_idom"
+  shows "(-) c ` {..b} = {c - b..}"
+proof -
+  have "(-) c ` {..b} = (+) c ` uminus ` {..b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b..}" by simp
+  finally show ?thesis by simp
+qed
+
+context linordered_field begin
+
+lemma image_mult_atLeastAtMost [simp]:
+  "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
+  using that
+  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
+
+lemma image_mult_atLeastAtMost_if:
+  "( * ) c ` {x .. y} =
+    (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
+proof -
+  consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
+    using local.antisym_conv3 local.leI by blast
+  then show ?thesis
+  proof cases
+    case 1
+    have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
+      by (simp add: image_image)
+    also have "\<dots> = {c * y .. c * x}"
+      using \<open>c < 0\<close>
+      by simp
+    finally show ?thesis
+      using \<open>c < 0\<close> by auto
+  qed (auto simp: not_le local.mult_less_cancel_left_pos)
+qed
+
+lemma image_mult_atLeastAtMost_if':
+  "(\<lambda>x. x * c) ` {x..y} =
+    (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
+  by (subst mult.commute)
+    (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
+
+lemma image_affinity_atLeastAtMost:
+  "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {m*a + c .. m *b + c}
+            else {m*b + c .. m*a + c})"
+proof -
+  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
+    unfolding image_comp[symmetric]
+    by (simp add: o_def)
+  then show ?thesis
+    by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
+qed
+
+lemma image_affinity_atLeastAtMost_diff:
+  "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {m*a - c .. m*b - c}
+            else {m*b - c .. m*a - c})"
+  using image_affinity_atLeastAtMost [of m "-c" a b]
+  by simp
+
+lemma image_affinity_atLeastAtMost_div:
+  "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {a/m + c .. b/m + c}
+            else {b/m + c .. a/m + c})"
+  using image_affinity_atLeastAtMost [of "inverse m" c a b]
+  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+lemma image_affinity_atLeastAtMost_div_diff:
+  "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {a/m - c .. b/m - c}
+            else {b/m - c .. a/m - c})"
+  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
+  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+end
+
+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)
+  apply (rule_tac x = "x - l" in bexI)
+  apply auto
+  done
+
+lemma image_minus_const_atLeastLessThan_nat:
+  fixes c :: nat
+  shows "(\<lambda>i. i - c) ` {x ..< y} =
+      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
+    (is "_ = ?right")
+proof safe
+  fix a assume a: "a \<in> ?right"
+  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
+  proof cases
+    assume "c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ "a + c"])
+  next
+    assume "\<not> c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
+  qed
+qed auto
+
+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_atLeastAtMost:
+  "int ` {a..b} = {int a..int b}"
+  by (auto intro!: image_eqI [where x = "nat x" for x])
+
+
 subsubsection \<open>Finiteness\<close>
 
 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"