Rewrite rules for images of minus of intervals
authorhoelzl
Thu Mar 04 19:43:51 2010 +0100 (2010-03-04)
changeset 355800f74806cab22
parent 35579 cc9a5a0ab5ea
child 35581 a25e51e2d64d
Rewrite rules for images of minus of intervals
src/HOL/Fun.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Mar 04 18:42:39 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Thu Mar 04 19:43:51 2010 +0100
     1.3 @@ -378,6 +378,8 @@
     1.4  apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
     1.5  done
     1.6  
     1.7 +lemma (in ordered_ab_group_add) inj_uminus[iff]: "inj uminus"
     1.8 +  by (auto intro!: inj_onI)
     1.9  
    1.10  subsection{*Function Updating*}
    1.11  
     2.1 --- a/src/HOL/SetInterval.thy	Thu Mar 04 18:42:39 2010 +0100
     2.2 +++ b/src/HOL/SetInterval.thy	Thu Mar 04 19:43:51 2010 +0100
     2.3 @@ -445,6 +445,47 @@
     2.4    apply auto
     2.5    done
     2.6  
     2.7 +context ordered_ab_group_add
     2.8 +begin
     2.9 +
    2.10 +lemma
    2.11 +  fixes x :: 'a
    2.12 +  shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<-x}"
    2.13 +  and image_uminus_atLeast[simp]: "uminus ` {x..} = {..-x}"
    2.14 +proof safe
    2.15 +  fix y assume "y < -x"
    2.16 +  hence *:  "x < -y" using neg_less_iff_less[of "-y" x] by simp
    2.17 +  have "- (-y) \<in> uminus ` {x<..}"
    2.18 +    by (rule imageI) (simp add: *)
    2.19 +  thus "y \<in> uminus ` {x<..}" by simp
    2.20 +next
    2.21 +  fix y assume "y \<le> -x"
    2.22 +  have "- (-y) \<in> uminus ` {x..}"
    2.23 +    by (rule imageI) (insert `y \<le> -x`[THEN le_imp_neg_le], simp)
    2.24 +  thus "y \<in> uminus ` {x..}" by simp
    2.25 +qed simp_all
    2.26 +
    2.27 +lemma
    2.28 +  fixes x :: 'a
    2.29 +  shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {-x<..}"
    2.30 +  and image_uminus_atMost[simp]: "uminus ` {..x} = {-x..}"
    2.31 +proof -
    2.32 +  have "uminus ` {..<x} = uminus ` uminus ` {-x<..}"
    2.33 +    and "uminus ` {..x} = uminus ` uminus ` {-x..}" by simp_all
    2.34 +  thus "uminus ` {..<x} = {-x<..}" and "uminus ` {..x} = {-x..}"
    2.35 +    by (simp_all add: image_image
    2.36 +        del: image_uminus_greaterThan image_uminus_atLeast)
    2.37 +qed
    2.38 +
    2.39 +lemma
    2.40 +  fixes x :: 'a
    2.41 +  shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {-y..-x}"
    2.42 +  and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {-y..<-x}"
    2.43 +  and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {-y<..-x}"
    2.44 +  and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
    2.45 +  by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
    2.46 +      greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
    2.47 +end
    2.48  
    2.49  subsubsection {* Finiteness *}
    2.50