807 else {})" |
807 else {})" |
808 by (simp add: numeral_eq_Suc atLeastLessThanSuc) |
808 by (simp add: numeral_eq_Suc atLeastLessThanSuc) |
809 |
809 |
810 subsubsection \<open>Image\<close> |
810 subsubsection \<open>Image\<close> |
811 |
811 |
812 lemma image_add_atLeastAtMost: |
812 lemma image_add_atLeastAtMost [simp]: |
813 fixes k ::"'a::linordered_semidom" |
813 fixes k ::"'a::linordered_semidom" |
814 shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") |
814 shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") |
815 proof |
815 proof |
816 show "?A \<subseteq> ?B" by auto |
816 show "?A \<subseteq> ?B" by auto |
817 next |
817 next |
830 by (simp add: add.commute) |
830 by (simp add: add.commute) |
831 qed |
831 qed |
832 ultimately show "n : ?A" by blast |
832 ultimately show "n : ?A" by blast |
833 qed |
833 qed |
834 qed |
834 qed |
|
835 |
|
836 lemma image_diff_atLeastAtMost [simp]: |
|
837 fixes d::"'a::linordered_idom" shows "(op - d ` {a..b}) = {d-b..d-a}" |
|
838 apply auto |
|
839 apply (rule_tac x="d-x" in rev_image_eqI, auto) |
|
840 done |
|
841 |
|
842 lemma image_mult_atLeastAtMost [simp]: |
|
843 fixes d::"'a::linordered_field" |
|
844 assumes "d>0" shows "(op * d ` {a..b}) = {d*a..d*b}" |
|
845 using assms |
|
846 by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x]) |
|
847 |
|
848 lemma image_affinity_atLeastAtMost: |
|
849 fixes c :: "'a::linordered_field" |
|
850 shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {} |
|
851 else if 0 \<le> m then {m*a + c .. m *b + c} |
|
852 else {m*b + c .. m*a + c})" |
|
853 apply (case_tac "m=0", auto simp: mult_le_cancel_left) |
|
854 apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps) |
|
855 apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps) |
|
856 done |
|
857 |
|
858 lemma image_affinity_atLeastAtMost_diff: |
|
859 fixes c :: "'a::linordered_field" |
|
860 shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {} |
|
861 else if 0 \<le> m then {m*a - c .. m*b - c} |
|
862 else {m*b - c .. m*a - c})" |
|
863 using image_affinity_atLeastAtMost [of m "-c" a b] |
|
864 by simp |
|
865 |
|
866 lemma image_affinity_atLeastAtMost_div_diff: |
|
867 fixes c :: "'a::linordered_field" |
|
868 shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {} |
|
869 else if 0 \<le> m then {a/m - c .. b/m - c} |
|
870 else {b/m - c .. a/m - c})" |
|
871 using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] |
|
872 by (simp add: field_class.field_divide_inverse algebra_simps) |
835 |
873 |
836 lemma image_add_atLeastLessThan: |
874 lemma image_add_atLeastLessThan: |
837 "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B") |
875 "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B") |
838 proof |
876 proof |
839 show "?A \<subseteq> ?B" by auto |
877 show "?A \<subseteq> ?B" by auto |