src/HOL/Conditionally_Complete_Lattices.thy
changeset 56166 9a241bc276cd
parent 54281 b01057e72233
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -275,16 +275,16 @@
     1.4    by (auto intro!: cInf_eq_minimum)
     1.5  
     1.6  lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x"
     1.7 -  unfolding INF_def by (rule cInf_lower) auto
     1.8 +  using cInf_lower [of _ "f ` A"] by simp
     1.9  
    1.10  lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f"
    1.11 -  unfolding INF_def by (rule cInf_greatest) auto
    1.12 +  using cInf_greatest [of "f ` A"] by auto
    1.13  
    1.14  lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f"
    1.15 -  unfolding SUP_def by (rule cSup_upper) auto
    1.16 +  using cSup_upper [of _ "f ` A"] by simp
    1.17  
    1.18  lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M"
    1.19 -  unfolding SUP_def by (rule cSup_least) auto
    1.20 +  using cSup_least [of "f ` A"] by auto
    1.21  
    1.22  lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u"
    1.23    by (auto intro: cINF_lower assms order_trans)
    1.24 @@ -311,16 +311,16 @@
    1.25    by (metis cSUP_upper le_less_trans)
    1.26  
    1.27  lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
    1.28 -  by (metis INF_def cInf_insert assms empty_is_image image_insert)
    1.29 +  by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
    1.30  
    1.31  lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)"
    1.32 -  by (metis SUP_def cSup_insert assms empty_is_image image_insert)
    1.33 +  by (metis cSup_insert Sup_image_eq image_insert image_is_empty)
    1.34  
    1.35  lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFI A f \<le> INFI B g"
    1.36 -  unfolding INF_def by (auto intro: cInf_mono)
    1.37 +  using cInf_mono [of "g ` B" "f ` A"] by auto
    1.38  
    1.39  lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPR A f \<le> SUPR B g"
    1.40 -  unfolding SUP_def by (auto intro: cSup_mono)
    1.41 +  using cSup_mono [of "f ` A" "g ` B"] by auto
    1.42  
    1.43  lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFI B g \<le> INFI A f"
    1.44    by (rule cINF_mono) auto
    1.45 @@ -338,13 +338,13 @@
    1.46    by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
    1.47  
    1.48  lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFI (A \<union> B) f = inf (INFI A f) (INFI B f)"
    1.49 -  unfolding INF_def using assms by (auto simp add: image_Un intro: cInf_union_distrib)
    1.50 +  using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
    1.51  
    1.52  lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
    1.53    by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
    1.54  
    1.55  lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPR (A \<union> B) f = sup (SUPR A f) (SUPR B f)"
    1.56 -  unfolding SUP_def by (auto simp add: image_Un intro: cSup_union_distrib)
    1.57 +  using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
    1.58  
    1.59  lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFI A f) (INFI A g) = (INF a:A. inf (f a) (g a))"
    1.60    by (intro antisym le_infI cINF_greatest cINF_lower2)
    1.61 @@ -388,10 +388,10 @@
    1.62    by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
    1.63  
    1.64  lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
    1.65 -  unfolding INF_def using cInf_less_iff[of "f`A"] by auto
    1.66 +  using cInf_less_iff[of "f`A"] by auto
    1.67  
    1.68  lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
    1.69 -  unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
    1.70 +  using less_cSup_iff[of "f`A"] by auto
    1.71  
    1.72  lemma less_cSupE:
    1.73    assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"