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"
```