moved auxiliary lemmas to more appropriate places
authorhaftmann
Mon Feb 08 14:06:54 2010 +0100 (2010-02-08)
changeset 35037748f0bc3f7ca
parent 35036 b8c8d01cc20d
child 35038 a1d93ce94235
moved auxiliary lemmas to more appropriate places
src/HOL/SupInf.thy
     1.1 --- a/src/HOL/SupInf.thy	Mon Feb 08 14:06:51 2010 +0100
     1.2 +++ b/src/HOL/SupInf.thy	Mon Feb 08 14:06:54 2010 +0100
     1.3 @@ -6,38 +6,6 @@
     1.4  imports RComplete
     1.5  begin
     1.6  
     1.7 -lemma minus_max_eq_min:
     1.8 -  fixes x :: "'a::{lattice_ab_group_add, linorder}"
     1.9 -  shows "- (max x y) = min (-x) (-y)"
    1.10 -by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
    1.11 -
    1.12 -lemma minus_min_eq_max:
    1.13 -  fixes x :: "'a::{lattice_ab_group_add, linorder}"
    1.14 -  shows "- (min x y) = max (-x) (-y)"
    1.15 -by (metis minus_max_eq_min minus_minus)
    1.16 -
    1.17 -lemma minus_Max_eq_Min [simp]:
    1.18 -  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
    1.19 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
    1.20 -proof (induct S rule: finite_ne_induct)
    1.21 -  case (singleton x)
    1.22 -  thus ?case by simp
    1.23 -next
    1.24 -  case (insert x S)
    1.25 -  thus ?case by (simp add: minus_max_eq_min) 
    1.26 -qed
    1.27 -
    1.28 -lemma minus_Min_eq_Max [simp]:
    1.29 -  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
    1.30 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
    1.31 -proof (induct S rule: finite_ne_induct)
    1.32 -  case (singleton x)
    1.33 -  thus ?case by simp
    1.34 -next
    1.35 -  case (insert x S)
    1.36 -  thus ?case by (simp add: minus_min_eq_max) 
    1.37 -qed
    1.38 -
    1.39  instantiation real :: Sup 
    1.40  begin
    1.41  definition