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