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.27      by (simp add: eq_fold)
    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.165    by (simp add: eq_fold)
   1.166  
   1.167  lemma empty [simp]:
   1.168 -  "F {} = 1"
   1.169 +  "F {} = \<^bold>1"
   1.170    by (simp add: eq_fold)
   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