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

src/HOL/Lattices_Big.thy

changeset 60758 | d8d85a8172b5 |

parent 59000 | 6eb0725503fc |

child 61169 | 4de9ff3ea29a |

1.1 --- a/src/HOL/Lattices_Big.thy Sat Jul 18 21:44:18 2015 +0200 1.2 +++ b/src/HOL/Lattices_Big.thy Sat Jul 18 22:58:50 2015 +0200 1.3 @@ -3,19 +3,19 @@ 1.4 with contributions by Jeremy Avigad 1.5 *) 1.6 1.7 -section {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *} 1.8 +section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close> 1.9 1.10 theory Lattices_Big 1.11 imports Finite_Set Option 1.12 begin 1.13 1.14 -subsection {* Generic lattice operations over a set *} 1.15 +subsection \<open>Generic lattice operations over a set\<close> 1.16 1.17 no_notation times (infixl "*" 70) 1.18 no_notation Groups.one ("1") 1.19 1.20 1.21 -subsubsection {* Without neutral element *} 1.22 +subsubsection \<open>Without neutral element\<close> 1.23 1.24 locale semilattice_set = semilattice 1.25 begin 1.26 @@ -50,9 +50,9 @@ 1.27 assumes "finite A" and "x \<notin> A" and "A \<noteq> {}" 1.28 shows "F (insert x A) = x * F A" 1.29 proof - 1.30 - from `A \<noteq> {}` obtain b where "b \<in> A" by blast 1.31 + from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast 1.32 then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert) 1.33 - with `finite A` and `x \<notin> A` 1.34 + with \<open>finite A\<close> and \<open>x \<notin> A\<close> 1.35 have "finite (insert x B)" and "b \<notin> insert x B" by auto 1.36 then have "F (insert b (insert x B)) = x * F (insert b B)" 1.37 by (simp add: eq_fold) 1.38 @@ -64,7 +64,7 @@ 1.39 shows "x * F A = F A" 1.40 proof - 1.41 from assms have "A \<noteq> {}" by auto 1.42 - with `finite A` show ?thesis using `x \<in> A` 1.43 + with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close> 1.44 by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem) 1.45 qed 1.46 1.47 @@ -102,7 +102,7 @@ 1.48 lemma closed: 1.49 assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}" 1.50 shows "F A \<in> A" 1.51 -using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct) 1.52 +using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct) 1.53 case singleton then show ?case by simp 1.54 next 1.55 case insert with elem show ?case by force 1.56 @@ -156,7 +156,7 @@ 1.57 shows "F A \<preceq> a" 1.58 proof - 1.59 from assms have "A \<noteq> {}" by auto 1.60 - from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis 1.61 + from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis 1.62 proof (induct rule: finite_ne_induct) 1.63 case singleton thus ?case by (simp add: refl) 1.64 next 1.65 @@ -173,7 +173,7 @@ 1.66 case True then show ?thesis by (simp add: refl) 1.67 next 1.68 case False 1.69 - have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast 1.70 + have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast 1.71 then have "F B = F (A \<union> (B - A))" by simp 1.72 also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset) 1.73 also have "\<dots> \<preceq> F A" by simp 1.74 @@ -183,7 +183,7 @@ 1.75 end 1.76 1.77 1.78 -subsubsection {* With neutral element *} 1.79 +subsubsection \<open>With neutral element\<close> 1.80 1.81 locale semilattice_neutr_set = semilattice_neutr 1.82 begin 1.83 @@ -213,7 +213,7 @@ 1.84 shows "x * F A = F A" 1.85 proof - 1.86 from assms have "A \<noteq> {}" by auto 1.87 - with `finite A` show ?thesis using `x \<in> A` 1.88 + with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close> 1.89 by (induct A rule: finite_ne_induct) (auto simp add: ac_simps) 1.90 qed 1.91 1.92 @@ -246,7 +246,7 @@ 1.93 lemma closed: 1.94 assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}" 1.95 shows "F A \<in> A" 1.96 -using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct) 1.97 +using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct) 1.98 case singleton then show ?case by simp 1.99 next 1.100 case insert with elem show ?case by force 1.101 @@ -279,7 +279,7 @@ 1.102 shows "F A \<preceq> a" 1.103 proof - 1.104 from assms have "A \<noteq> {}" by auto 1.105 - from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis 1.106 + from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis 1.107 proof (induct rule: finite_ne_induct) 1.108 case singleton thus ?case by (simp add: refl) 1.109 next 1.110 @@ -296,7 +296,7 @@ 1.111 case True then show ?thesis by (simp add: refl) 1.112 next 1.113 case False 1.114 - have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast 1.115 + have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast 1.116 then have "F B = F (A \<union> (B - A))" by simp 1.117 also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset) 1.118 also have "\<dots> \<preceq> F A" by simp 1.119 @@ -309,7 +309,7 @@ 1.120 notation Groups.one ("1") 1.121 1.122 1.123 -subsection {* Lattice operations on finite sets *} 1.124 +subsection \<open>Lattice operations on finite sets\<close> 1.125 1.126 context semilattice_inf 1.127 begin 1.128 @@ -348,7 +348,7 @@ 1.129 end 1.130 1.131 1.132 -subsection {* Infimum and Supremum over non-empty sets *} 1.133 +subsection \<open>Infimum and Supremum over non-empty sets\<close> 1.134 1.135 context lattice 1.136 begin 1.137 @@ -357,9 +357,9 @@ 1.138 assumes "finite A" and "A \<noteq> {}" 1.139 shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" 1.140 proof - 1.141 - from `A \<noteq> {}` obtain a where "a \<in> A" by blast 1.142 - with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI) 1.143 - moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI) 1.144 + from \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" by blast 1.145 + with \<open>finite A\<close> have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI) 1.146 + moreover from \<open>finite A\<close> \<open>a \<in> A\<close> have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI) 1.147 ultimately show ?thesis by (rule order_trans) 1.148 qed 1.149 1.150 @@ -477,7 +477,7 @@ 1.151 end 1.152 1.153 1.154 -subsection {* Minimum and Maximum over non-empty sets *} 1.155 +subsection \<open>Minimum and Maximum over non-empty sets\<close> 1.156 1.157 context linorder 1.158 begin 1.159 @@ -506,7 +506,7 @@ 1.160 1.161 end 1.162 1.163 -text {* An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *} 1.164 +text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close> 1.165 1.166 lemma Inf_fin_Min: 1.167 "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)" 1.168 @@ -566,9 +566,9 @@ 1.169 proof (cases "A = {}") 1.170 case True then show ?thesis by simp 1.171 next 1.172 - case False with `finite A` have "Min (insert a A) = min a (Min A)" 1.173 + case False with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)" 1.174 by simp 1.175 - moreover from `finite A` `A \<noteq> {}` min have "a \<le> Min A" by simp 1.176 + moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp 1.177 ultimately show ?thesis by (simp add: min.absorb1) 1.178 qed 1.179 1.180 @@ -578,9 +578,9 @@ 1.181 proof (cases "A = {}") 1.182 case True then show ?thesis by simp 1.183 next 1.184 - case False with `finite A` have "Max (insert a A) = max a (Max A)" 1.185 + case False with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)" 1.186 by simp 1.187 - moreover from `finite A` `A \<noteq> {}` max have "Max A \<le> a" by simp 1.188 + moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp 1.189 ultimately show ?thesis by (simp add: max.absorb1) 1.190 qed 1.191 1.192 @@ -600,7 +600,7 @@ 1.193 and "x \<in> A" 1.194 shows "Min A = x" 1.195 proof (rule antisym) 1.196 - from `x \<in> A` have "A \<noteq> {}" by auto 1.197 + from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto 1.198 with assms show "Min A \<ge> x" by simp 1.199 next 1.200 from assms show "x \<ge> Min A" by simp 1.201 @@ -612,7 +612,7 @@ 1.202 and "x \<in> A" 1.203 shows "Max A = x" 1.204 proof (rule antisym) 1.205 - from `x \<in> A` have "A \<noteq> {}" by auto 1.206 + from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto 1.207 with assms show "Max A \<le> x" by simp 1.208 next 1.209 from assms show "x \<le> Max A" by simp 1.210 @@ -687,14 +687,14 @@ 1.211 assumes "finite A" and "A \<noteq> {}" 1.212 shows "f (Min A) = Min (f ` A)" 1.213 proof (rule linorder_class.Min_eqI [symmetric]) 1.214 - from `finite A` show "finite (f ` A)" by simp 1.215 + from \<open>finite A\<close> show "finite (f ` A)" by simp 1.216 from assms show "f (Min A) \<in> f ` A" by simp 1.217 fix x 1.218 assume "x \<in> f ` A" 1.219 then obtain y where "y \<in> A" and "x = f y" .. 1.220 with assms have "Min A \<le> y" by auto 1.221 - with `mono f` have "f (Min A) \<le> f y" by (rule monoE) 1.222 - with `x = f y` show "f (Min A) \<le> x" by simp 1.223 + with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE) 1.224 + with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp 1.225 qed 1.226 1.227 lemma mono_Max_commute: 1.228 @@ -702,14 +702,14 @@ 1.229 assumes "finite A" and "A \<noteq> {}" 1.230 shows "f (Max A) = Max (f ` A)" 1.231 proof (rule linorder_class.Max_eqI [symmetric]) 1.232 - from `finite A` show "finite (f ` A)" by simp 1.233 + from \<open>finite A\<close> show "finite (f ` A)" by simp 1.234 from assms show "f (Max A) \<in> f ` A" by simp 1.235 fix x 1.236 assume "x \<in> f ` A" 1.237 then obtain y where "y \<in> A" and "x = f y" .. 1.238 with assms have "y \<le> Max A" by auto 1.239 - with `mono f` have "f y \<le> f (Max A)" by (rule monoE) 1.240 - with `x = f y` show "x \<le> f (Max A)" by simp 1.241 + with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE) 1.242 + with \<open>x = f y\<close> show "x \<le> f (Max A)" by simp 1.243 qed 1.244 1.245 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]: 1.246 @@ -727,18 +727,18 @@ 1.247 show "P A" 1.248 proof (cases "A = {}") 1.249 assume "A = {}" 1.250 - then show "P A" using `P {}` by simp 1.251 + then show "P A" using \<open>P {}\<close> by simp 1.252 next 1.253 let ?B = "A - {Max A}" 1.254 let ?A = "insert (Max A) ?B" 1.255 - have "finite ?B" using `finite A` by simp 1.256 + have "finite ?B" using \<open>finite A\<close> by simp 1.257 assume "A \<noteq> {}" 1.258 - with `finite A` have "Max A : A" by auto 1.259 + with \<open>finite A\<close> have "Max A : A" by auto 1.260 then have A: "?A = A" using insert_Diff_single insert_absorb by auto 1.261 - then have "P ?B" using `P {}` step IH [of ?B] by blast 1.262 + then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast 1.263 moreover 1.264 - have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce 1.265 - ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce 1.266 + have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF \<open>finite A\<close>] by fastforce 1.267 + ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce 1.268 qed 1.269 qed 1.270 1.271 @@ -770,7 +770,7 @@ 1.272 shows "\<not> finite X" 1.273 proof 1.274 assume "finite X" 1.275 - with `X \<noteq> {}` have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X" 1.276 + with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X" 1.277 by auto 1.278 with *[of "Max X"] show False 1.279 by auto