added auxiliary lemmas for proof tools
authorhaftmann
Sun May 06 21:49:29 2007 +0200 (2007-05-06)
changeset 228426d2fd4e0f984
parent 22841 83b9f2d3fb3c
child 22843 189e214845dd
added auxiliary lemmas for proof tools
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Sun May 06 21:49:27 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sun May 06 21:49:29 2007 +0200
     1.3 @@ -2067,4 +2067,24 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +subsection {* Theorems for proof tools *}
     1.8 +
     1.9 +lemma add_mono_thms_ordered_semiring:
    1.10 +  fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
    1.11 +  shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    1.12 +    and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    1.13 +    and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
    1.14 +    and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
    1.15 +by (rule add_mono, clarify+)+
    1.16 +
    1.17 +lemma add_mono_thms_ordered_field:
    1.18 +  fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
    1.19 +  shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
    1.20 +    and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
    1.21 +    and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
    1.22 +    and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
    1.23 +    and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
    1.24 +by (auto intro: add_strict_right_mono add_strict_left_mono
    1.25 +  add_less_le_mono add_le_less_mono add_strict_mono)
    1.26 +
    1.27  end