src/HOL/Lattices_Big.thy
changeset 58467 6a3da58f7233
parent 57800 84748234de9d
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Lattices_Big.thy	Fri Sep 26 19:38:26 2014 +0200
     1.2 +++ b/src/HOL/Lattices_Big.thy	Sun Sep 28 20:27:46 2014 +0200
     1.3 @@ -560,6 +560,30 @@
     1.4    shows "Max A \<in> A"
     1.5    using assms by (auto simp add: max_def Max.closed)
     1.6  
     1.7 +lemma Min_insert2:
     1.8 +  assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
     1.9 +  shows "Min (insert a A) = a"
    1.10 +proof (cases "A = {}")
    1.11 +  case True then show ?thesis by simp
    1.12 +next
    1.13 +  case False with `finite A` have "Min (insert a A) = min a (Min A)"
    1.14 +    by simp
    1.15 +  moreover from `finite A` `A \<noteq> {}` min have "a \<le> Min A" by simp
    1.16 +  ultimately show ?thesis by (simp add: min.absorb1)
    1.17 +qed
    1.18 +
    1.19 +lemma Max_insert2:
    1.20 +  assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
    1.21 +  shows "Max (insert a A) = a"
    1.22 +proof (cases "A = {}")
    1.23 +  case True then show ?thesis by simp
    1.24 +next
    1.25 +  case False with `finite A` have "Max (insert a A) = max a (Max A)"
    1.26 +    by simp
    1.27 +  moreover from `finite A` `A \<noteq> {}` max have "Max A \<le> a" by simp
    1.28 +  ultimately show ?thesis by (simp add: max.absorb1)
    1.29 +qed
    1.30 +
    1.31  lemma Min_le [simp]:
    1.32    assumes "finite A" and "x \<in> A"
    1.33    shows "Min A \<le> x"