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