summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Lattices_Big.thy

changeset 63915 | bab633745c7f |

parent 63290 | 9ac558ab0906 |

child 65817 | 8ee1799fb076 |

1.1 --- a/src/HOL/Lattices_Big.thy Sun Sep 18 17:59:28 2016 +0200 1.2 +++ b/src/HOL/Lattices_Big.thy Sun Sep 18 20:33:48 2016 +0200 1.3 @@ -522,9 +522,11 @@ 1.4 assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b" 1.5 shows "Min (insert a A) = a" 1.6 proof (cases "A = {}") 1.7 - case True then show ?thesis by simp 1.8 + case True 1.9 + then show ?thesis by simp 1.10 next 1.11 - case False with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)" 1.12 + case False 1.13 + with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)" 1.14 by simp 1.15 moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp 1.16 ultimately show ?thesis by (simp add: min.absorb1) 1.17 @@ -534,9 +536,11 @@ 1.18 assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a" 1.19 shows "Max (insert a A) = a" 1.20 proof (cases "A = {}") 1.21 - case True then show ?thesis by simp 1.22 + case True 1.23 + then show ?thesis by simp 1.24 next 1.25 - case False with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)" 1.26 + case False 1.27 + with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)" 1.28 by simp 1.29 moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp 1.30 ultimately show ?thesis by (simp add: max.absorb1)