src/HOL/Conditionally_Complete_Lattices.thy
changeset 59452 2538b2c51769
parent 58889 5b7a9633cfa8
child 60172 423273355b55
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jan 26 14:40:13 2015 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Jan 27 16:12:40 2015 +0100
     1.3 @@ -102,15 +102,25 @@
     1.4  lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
     1.5    by (rule bdd_belowI[of _ bot]) simp
     1.6  
     1.7 -lemma bdd_above_uminus[simp]:
     1.8 -  fixes X :: "'a::ordered_ab_group_add set"
     1.9 -  shows "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
    1.10 -  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    1.11 +lemma bdd_above_image_mono: "mono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_above (f`A)"
    1.12 +  by (auto simp: bdd_above_def mono_def)
    1.13 +
    1.14 +lemma bdd_below_image_mono: "mono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_below (f`A)"
    1.15 +  by (auto simp: bdd_below_def mono_def)
    1.16 +  
    1.17 +lemma bdd_above_image_antimono: "antimono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_above (f`A)"
    1.18 +  by (auto simp: bdd_above_def bdd_below_def antimono_def)
    1.19  
    1.20 -lemma bdd_below_uminus[simp]:
    1.21 +lemma bdd_below_image_antimono: "antimono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below (f`A)"
    1.22 +  by (auto simp: bdd_above_def bdd_below_def antimono_def)
    1.23 +
    1.24 +lemma
    1.25    fixes X :: "'a::ordered_ab_group_add set"
    1.26 -  shows"bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
    1.27 -  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    1.28 +  shows bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
    1.29 +    and bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
    1.30 +  using bdd_above_image_antimono[of uminus X] bdd_below_image_antimono[of uminus "uminus`X"]
    1.31 +  using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"]
    1.32 +  by (auto simp: antimono_def image_image)
    1.33  
    1.34  context lattice
    1.35  begin