weaken preconditions on lemmas
authornoschinl
Mon Dec 19 14:41:08 2011 +0100 (2011-12-19)
changeset 4593199cf6e470816
parent 45930 2a882ef2cd73
child 45932 6f08f8fe9752
weaken preconditions on lemmas
src/HOL/Nat.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.3 @@ -721,10 +721,10 @@
     1.4  by (rule monoI) simp
     1.5  
     1.6  lemma min_0L [simp]: "min 0 n = (0::nat)"
     1.7 -by (rule min_leastL) simp
     1.8 +by (rule min_absorb1) simp
     1.9  
    1.10  lemma min_0R [simp]: "min n 0 = (0::nat)"
    1.11 -by (rule min_leastR) simp
    1.12 +by (rule min_absorb2) simp
    1.13  
    1.14  lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
    1.15  by (simp add: mono_Suc min_of_mono)
    1.16 @@ -738,10 +738,10 @@
    1.17  by (simp split: nat.split)
    1.18  
    1.19  lemma max_0L [simp]: "max 0 n = (n::nat)"
    1.20 -by (rule max_leastL) simp
    1.21 +by (rule max_absorb2) simp
    1.22  
    1.23  lemma max_0R [simp]: "max n 0 = (n::nat)"
    1.24 -by (rule max_leastR) simp
    1.25 +by (rule max_absorb1) simp
    1.26  
    1.27  lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
    1.28  by (simp add: mono_Suc max_of_mono)
     2.1 --- a/src/HOL/Orderings.thy	Mon Dec 19 14:41:08 2011 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Mon Dec 19 14:41:08 2011 +0100
     2.3 @@ -1050,33 +1050,20 @@
     2.4  
     2.5  end
     2.6  
     2.7 -lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
     2.8 +lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x"
     2.9  by (simp add: min_def)
    2.10  
    2.11 -lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
    2.12 +lemma max_absorb2: "x \<le> y ==> max x y = y"
    2.13  by (simp add: max_def)
    2.14  
    2.15 -lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
    2.16 -by (simp add: min_def) (blast intro: antisym)
    2.17 -
    2.18 -lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
    2.19 -by (simp add: max_def) (blast intro: antisym)
    2.20 -
    2.21 -lemma min_greatestL: "(\<And>x::'a::order. x \<le> greatest) \<Longrightarrow> min greatest x = x"
    2.22 -by (simp add: min_def) (blast intro: antisym)
    2.23 +lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"
    2.24 +by (simp add:min_def)
    2.25  
    2.26 -lemma max_greatestL: "(\<And>x::'a::order. x \<le> greatest) \<Longrightarrow> max greatest x = greatest"
    2.27 -by (simp add: max_def) (blast intro: antisym)
    2.28 -
    2.29 -lemma min_greatestR: "(\<And>x. x \<le> greatest) \<Longrightarrow> min x greatest = x"
    2.30 -by (simp add: min_def)
    2.31 -
    2.32 -lemma max_greatestR: "(\<And>x. x \<le> greatest) \<Longrightarrow> max x greatest = greatest"
    2.33 +lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x"
    2.34  by (simp add: max_def)
    2.35  
    2.36  
    2.37  
    2.38 -
    2.39  subsection {* (Unique) top and bottom elements *}
    2.40  
    2.41  class bot = order +