src/HOL/Lattices_Big.thy
 changeset 63290 9ac558ab0906 parent 61776 57bb7da5c867 child 63915 bab633745c7f
```     1.1 --- a/src/HOL/Lattices_Big.thy	Sat Jun 11 17:40:52 2016 +0200
1.2 +++ b/src/HOL/Lattices_Big.thy	Sat Jun 11 16:22:42 2016 +0200
1.3 @@ -11,10 +11,6 @@
1.4
1.5  subsection \<open>Generic lattice operations over a set\<close>
1.6
1.7 -no_notation times (infixl "*" 70)
1.8 -no_notation Groups.one ("1")
1.9 -
1.10 -
1.11  subsubsection \<open>Without neutral element\<close>
1.12
1.13  locale semilattice_set = semilattice
1.14 @@ -48,20 +44,20 @@
1.15
1.16  lemma insert_not_elem:
1.17    assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
1.18 -  shows "F (insert x A) = x * F A"
1.19 +  shows "F (insert x A) = x \<^bold>* F A"
1.20  proof -
1.21    from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
1.22    then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
1.23    with \<open>finite A\<close> and \<open>x \<notin> A\<close>
1.24      have "finite (insert x B)" and "b \<notin> insert x B" by auto
1.25 -  then have "F (insert b (insert x B)) = x * F (insert b B)"
1.26 +  then have "F (insert b (insert x B)) = x \<^bold>* F (insert b B)"
1.28    then show ?thesis by (simp add: * insert_commute)
1.29  qed
1.30
1.31  lemma in_idem:
1.32    assumes "finite A" and "x \<in> A"
1.33 -  shows "x * F A = F A"
1.34 +  shows "x \<^bold>* F A = F A"
1.35  proof -
1.36    from assms have "A \<noteq> {}" by auto
1.37    with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
1.38 @@ -70,17 +66,17 @@
1.39
1.40  lemma insert [simp]:
1.41    assumes "finite A" and "A \<noteq> {}"
1.42 -  shows "F (insert x A) = x * F A"
1.43 +  shows "F (insert x A) = x \<^bold>* F A"
1.44    using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
1.45
1.46  lemma union:
1.47    assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
1.48 -  shows "F (A \<union> B) = F A * F B"
1.49 +  shows "F (A \<union> B) = F A \<^bold>* F B"
1.50    using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
1.51
1.52  lemma remove:
1.53    assumes "finite A" and "x \<in> A"
1.54 -  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
1.55 +  shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
1.56  proof -
1.57    from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
1.58    with assms show ?thesis by simp
1.59 @@ -88,19 +84,19 @@
1.60
1.61  lemma insert_remove:
1.62    assumes "finite A"
1.63 -  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
1.64 +  shows "F (insert x A) = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
1.65    using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
1.66
1.67  lemma subset:
1.68    assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
1.69 -  shows "F B * F A = F A"
1.70 +  shows "F B \<^bold>* F A = F A"
1.71  proof -
1.72    from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
1.73    with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
1.74  qed
1.75
1.76  lemma closed:
1.77 -  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
1.78 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
1.79    shows "F A \<in> A"
1.80  using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
1.81    case singleton then show ?case by simp
1.82 @@ -109,17 +105,17 @@
1.83  qed
1.84
1.85  lemma hom_commute:
1.86 -  assumes hom: "\<And>x y. h (x * y) = h x * h y"
1.87 +  assumes hom: "\<And>x y. h (x \<^bold>* y) = h x \<^bold>* h y"
1.88    and N: "finite N" "N \<noteq> {}"
1.89    shows "h (F N) = F (h ` N)"
1.90  using N proof (induct rule: finite_ne_induct)
1.91    case singleton thus ?case by simp
1.92  next
1.93    case (insert n N)
1.94 -  then have "h (F (insert n N)) = h (n * F N)" by simp
1.95 -  also have "\<dots> = h n * h (F N)" by (rule hom)
1.96 +  then have "h (F (insert n N)) = h (n \<^bold>* F N)" by simp
1.97 +  also have "\<dots> = h n \<^bold>* h (F N)" by (rule hom)
1.98    also have "h (F N) = F (h ` N)" by (rule insert)
1.99 -  also have "h n * \<dots> = F (insert (h n) (h ` N))"
1.100 +  also have "h n \<^bold>* \<dots> = F (insert (h n) (h ` N))"
1.101      using insert by simp
1.102    also have "insert (h n) (h ` N) = h ` insert n N" by simp
1.103    finally show ?case .
1.104 @@ -135,25 +131,25 @@
1.105
1.106  lemma bounded_iff:
1.107    assumes "finite A" and "A \<noteq> {}"
1.108 -  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
1.109 +  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
1.110    using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
1.111
1.112  lemma boundedI:
1.113    assumes "finite A"
1.114    assumes "A \<noteq> {}"
1.115 -  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
1.116 -  shows "x \<preceq> F A"
1.117 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
1.118 +  shows "x \<^bold>\<le> F A"
1.119    using assms by (simp add: bounded_iff)
1.120
1.121  lemma boundedE:
1.122 -  assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
1.123 -  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
1.124 +  assumes "finite A" and "A \<noteq> {}" and "x \<^bold>\<le> F A"
1.125 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
1.126    using assms by (simp add: bounded_iff)
1.127
1.128  lemma coboundedI:
1.129    assumes "finite A"
1.130      and "a \<in> A"
1.131 -  shows "F A \<preceq> a"
1.132 +  shows "F A \<^bold>\<le> a"
1.133  proof -
1.134    from assms have "A \<noteq> {}" by auto
1.135    from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
1.136 @@ -168,15 +164,15 @@
1.137
1.138  lemma antimono:
1.139    assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
1.140 -  shows "F B \<preceq> F A"
1.141 +  shows "F B \<^bold>\<le> F A"
1.142  proof (cases "A = B")
1.143    case True then show ?thesis by (simp add: refl)
1.144  next
1.145    case False
1.146    have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
1.147    then have "F B = F (A \<union> (B - A))" by simp
1.148 -  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
1.149 -  also have "\<dots> \<preceq> F A" by simp
1.150 +  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
1.151 +  also have "\<dots> \<^bold>\<le> F A" by simp
1.152    finally show ?thesis .
1.153  qed
1.154
1.155 @@ -193,24 +189,24 @@
1.156
1.157  definition F :: "'a set \<Rightarrow> 'a"
1.158  where
1.159 -  eq_fold: "F A = Finite_Set.fold f 1 A"
1.160 +  eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"
1.161
1.162  lemma infinite [simp]:
1.163 -  "\<not> finite A \<Longrightarrow> F A = 1"
1.164 +  "\<not> finite A \<Longrightarrow> F A = \<^bold>1"
1.166
1.167  lemma empty [simp]:
1.168 -  "F {} = 1"
1.169 +  "F {} = \<^bold>1"
1.171
1.172  lemma insert [simp]:
1.173    assumes "finite A"
1.174 -  shows "F (insert x A) = x * F A"
1.175 +  shows "F (insert x A) = x \<^bold>* F A"
1.176    using assms by (simp add: eq_fold)
1.177
1.178  lemma in_idem:
1.179    assumes "finite A" and "x \<in> A"
1.180 -  shows "x * F A = F A"
1.181 +  shows "x \<^bold>* F A = F A"
1.182  proof -
1.183    from assms have "A \<noteq> {}" by auto
1.184    with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
1.185 @@ -219,12 +215,12 @@
1.186
1.187  lemma union:
1.188    assumes "finite A" and "finite B"
1.189 -  shows "F (A \<union> B) = F A * F B"
1.190 +  shows "F (A \<union> B) = F A \<^bold>* F B"
1.191    using assms by (induct A) (simp_all add: ac_simps)
1.192
1.193  lemma remove:
1.194    assumes "finite A" and "x \<in> A"
1.195 -  shows "F A = x * F (A - {x})"
1.196 +  shows "F A = x \<^bold>* F (A - {x})"
1.197  proof -
1.198    from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
1.199    with assms show ?thesis by simp
1.200 @@ -232,19 +228,19 @@
1.201
1.202  lemma insert_remove:
1.203    assumes "finite A"
1.204 -  shows "F (insert x A) = x * F (A - {x})"
1.205 +  shows "F (insert x A) = x \<^bold>* F (A - {x})"
1.206    using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
1.207
1.208  lemma subset:
1.209    assumes "finite A" and "B \<subseteq> A"
1.210 -  shows "F B * F A = F A"
1.211 +  shows "F B \<^bold>* F A = F A"
1.212  proof -
1.213    from assms have "finite B" by (auto dest: finite_subset)
1.214    with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
1.215  qed
1.216
1.217  lemma closed:
1.218 -  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
1.219 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
1.220    shows "F A \<in> A"
1.221  using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
1.222    case singleton then show ?case by simp
1.223 @@ -259,24 +255,24 @@
1.224
1.225  lemma bounded_iff:
1.226    assumes "finite A"
1.227 -  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
1.228 +  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
1.229    using assms by (induct A) (simp_all add: bounded_iff)
1.230
1.231  lemma boundedI:
1.232    assumes "finite A"
1.233 -  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
1.234 -  shows "x \<preceq> F A"
1.235 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
1.236 +  shows "x \<^bold>\<le> F A"
1.237    using assms by (simp add: bounded_iff)
1.238
1.239  lemma boundedE:
1.240 -  assumes "finite A" and "x \<preceq> F A"
1.241 -  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
1.242 +  assumes "finite A" and "x \<^bold>\<le> F A"
1.243 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
1.244    using assms by (simp add: bounded_iff)
1.245
1.246  lemma coboundedI:
1.247    assumes "finite A"
1.248      and "a \<in> A"
1.249 -  shows "F A \<preceq> a"
1.250 +  shows "F A \<^bold>\<le> a"
1.251  proof -
1.252    from assms have "A \<noteq> {}" by auto
1.253    from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
1.254 @@ -291,23 +287,20 @@
1.255
1.256  lemma antimono:
1.257    assumes "A \<subseteq> B" and "finite B"
1.258 -  shows "F B \<preceq> F A"
1.259 +  shows "F B \<^bold>\<le> F A"
1.260  proof (cases "A = B")
1.261    case True then show ?thesis by (simp add: refl)
1.262  next
1.263    case False
1.264    have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
1.265    then have "F B = F (A \<union> (B - A))" by simp
1.266 -  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
1.267 -  also have "\<dots> \<preceq> F A" by simp
1.268 +  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
1.269 +  also have "\<dots> \<^bold>\<le> F A" by simp
1.270    finally show ?thesis .
1.271  qed
1.272
1.273  end
1.274
1.275 -notation times (infixl "*" 70)
1.276 -notation Groups.one ("1")
1.277 -
1.278
1.279  subsection \<open>Lattice operations on finite sets\<close>
1.280
```