remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
authorhuffman
Thu Sep 08 18:47:23 2011 -0700 (2011-09-08)
changeset 44848f4d0b060c7ca
parent 44847 b93d17a52217
child 44849 41fddafe20d5
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
src/HOL/Groups.thy
src/HOL/Library/Saturated.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Groups.thy	Thu Sep 08 18:13:48 2011 -0700
     1.2 +++ b/src/HOL/Groups.thy	Thu Sep 08 18:47:23 2011 -0700
     1.3 @@ -596,6 +596,14 @@
     1.4    "min x y + z = min (x + z) (y + z)"
     1.5    unfolding min_def by auto
     1.6  
     1.7 +lemma max_add_distrib_right:
     1.8 +  "x + max y z = max (x + y) (x + z)"
     1.9 +  unfolding max_def by auto
    1.10 +
    1.11 +lemma min_add_distrib_right:
    1.12 +  "x + min y z = min (x + y) (x + z)"
    1.13 +  unfolding min_def by auto
    1.14 +
    1.15  end
    1.16  
    1.17  subsection {* Support for reasoning about signs *}
     2.1 --- a/src/HOL/Library/Saturated.thy	Thu Sep 08 18:13:48 2011 -0700
     2.2 +++ b/src/HOL/Library/Saturated.thy	Thu Sep 08 18:47:23 2011 -0700
     2.3 @@ -131,7 +131,7 @@
     2.4      case True thus ?thesis by (simp add: sat_eq_iff)
     2.5    next
     2.6      case False thus ?thesis
     2.7 -      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib nat_add_min_left nat_add_min_right min_max.inf_assoc min_max.inf_absorb2)
     2.8 +      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2)
     2.9    qed
    2.10  qed (simp_all add: sat_eq_iff mult.commute)
    2.11  
     3.1 --- a/src/HOL/Nat.thy	Thu Sep 08 18:13:48 2011 -0700
     3.2 +++ b/src/HOL/Nat.thy	Thu Sep 08 18:47:23 2011 -0700
     3.3 @@ -753,16 +753,6 @@
     3.4     "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
     3.5  by (simp split: nat.split)
     3.6  
     3.7 -lemma nat_add_min_left:
     3.8 -  fixes m n q :: nat
     3.9 -  shows "min m n + q = min (m + q) (n + q)"
    3.10 -  by (simp add: min_def)
    3.11 -
    3.12 -lemma nat_add_min_right:
    3.13 -  fixes m n q :: nat
    3.14 -  shows "m + min n q = min (m + n) (m + q)"
    3.15 -  by (simp add: min_def)
    3.16 -
    3.17  lemma nat_mult_min_left:
    3.18    fixes m n q :: nat
    3.19    shows "min m n * q = min (m * q) (n * q)"