Knaster-Tarski fixed point theorem and Galois Connections.
authorballarin
Thu Mar 02 21:16:02 2017 +0100 (2017-03-02)
changeset 6509930d0b2f1df76
parent 65098 b47ba1778e44
child 65108 5a290f1819e5
child 65109 a79c1080f1e9
Knaster-Tarski fixed point theorem and Galois Connections.
CONTRIBUTORS
NEWS
src/HOL/Algebra/Complete_Lattice.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Galois_Connection.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Order.thy
src/HOL/ROOT
     1.1 --- a/CONTRIBUTORS	Fri Mar 03 23:21:24 2017 +0100
     1.2 +++ b/CONTRIBUTORS	Thu Mar 02 21:16:02 2017 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* March 2017: Alasdair Armstrong and Simon Foster, University of York
     1.8 +  Fixed-point theory and Galois Connections in HOL-Algebra.
     1.9 +
    1.10  * February 2017: Florian Haftmann, TUM
    1.11    Statically embedded computations implemented by generated code.
    1.12  
     2.1 --- a/NEWS	Fri Mar 03 23:21:24 2017 +0100
     2.2 +++ b/NEWS	Thu Mar 02 21:16:02 2017 +0100
     2.3 @@ -108,6 +108,9 @@
     2.4      with type class annotations. As a result, the tactic that derives
     2.5      it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
     2.6  
     2.7 +* Session HOL-Algebra extended by additional lattice theory: the
     2.8 +Knaster-Tarski fixed point theorem and Galois Connections.
     2.9 +
    2.10  * Session HOL-Analysis: more material involving arcs, paths, covering
    2.11  spaces, innessential maps, retracts. Major results include the Jordan
    2.12  Curve Theorem and the Great Picard Theorem.
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy	Thu Mar 02 21:16:02 2017 +0100
     3.3 @@ -0,0 +1,1191 @@
     3.4 +(*  Title:      HOL/Algebra/Complete_Lattice.thy
     3.5 +    Author:     Clemens Ballarin, started 7 November 2003
     3.6 +    Copyright:  Clemens Ballarin
     3.7 +
     3.8 +Most congruence rules by Stephan Hohe.
     3.9 +With additional contributions from Alasdair Armstrong and Simon Foster.
    3.10 +*)
    3.11 +
    3.12 +theory Complete_Lattice
    3.13 +imports Lattice
    3.14 +begin
    3.15 +
    3.16 +section \<open>Complete Lattices\<close>
    3.17 +
    3.18 +locale weak_complete_lattice = weak_partial_order +
    3.19 +  assumes sup_exists:
    3.20 +    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
    3.21 +    and inf_exists:
    3.22 +    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    3.23 +
    3.24 +sublocale weak_complete_lattice \<subseteq> weak_lattice
    3.25 +proof
    3.26 +  fix x y
    3.27 +  assume a: "x \<in> carrier L" "y \<in> carrier L"
    3.28 +  thus "\<exists>s. is_lub L s {x, y}"
    3.29 +    by (rule_tac sup_exists[of "{x, y}"], auto)
    3.30 +  from a show "\<exists>s. is_glb L s {x, y}"
    3.31 +    by (rule_tac inf_exists[of "{x, y}"], auto)
    3.32 +qed
    3.33 +
    3.34 +text \<open>Introduction rule: the usual definition of complete lattice\<close>
    3.35 +
    3.36 +lemma (in weak_partial_order) weak_complete_latticeI:
    3.37 +  assumes sup_exists:
    3.38 +    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
    3.39 +    and inf_exists:
    3.40 +    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    3.41 +  shows "weak_complete_lattice L"
    3.42 +  by standard (auto intro: sup_exists inf_exists)
    3.43 +
    3.44 +lemma (in weak_complete_lattice) dual_weak_complete_lattice:
    3.45 +  "weak_complete_lattice (inv_gorder L)"
    3.46 +proof -
    3.47 +  interpret dual: weak_lattice "inv_gorder L"
    3.48 +    by (metis dual_weak_lattice)
    3.49 +
    3.50 +  show ?thesis
    3.51 +    apply (unfold_locales)
    3.52 +    apply (simp_all add:inf_exists sup_exists)
    3.53 +  done
    3.54 +qed
    3.55 +
    3.56 +lemma (in weak_complete_lattice) supI:
    3.57 +  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
    3.58 +  ==> P (\<Squnion>A)"
    3.59 +proof (unfold sup_def)
    3.60 +  assume L: "A \<subseteq> carrier L"
    3.61 +    and P: "!!l. least L l (Upper L A) ==> P l"
    3.62 +  with sup_exists obtain s where "least L s (Upper L A)" by blast
    3.63 +  with L show "P (SOME l. least L l (Upper L A))"
    3.64 +  by (fast intro: someI2 weak_least_unique P)
    3.65 +qed
    3.66 +
    3.67 +lemma (in weak_complete_lattice) sup_closed [simp]:
    3.68 +  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
    3.69 +  by (rule supI) simp_all
    3.70 +
    3.71 +lemma (in weak_complete_lattice) sup_cong:
    3.72 +  assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"
    3.73 +  shows "\<Squnion> A .= \<Squnion> B"
    3.74 +proof -
    3.75 +  have "\<And> x. is_lub L x A \<longleftrightarrow> is_lub L x B"
    3.76 +    by (rule least_Upper_cong_r, simp_all add: assms)
    3.77 +  moreover have "\<Squnion> B \<in> carrier L"
    3.78 +    by (simp add: assms(2))
    3.79 +  ultimately show ?thesis
    3.80 +    by (simp add: sup_def)
    3.81 +qed
    3.82 +
    3.83 +sublocale weak_complete_lattice \<subseteq> weak_bounded_lattice
    3.84 +  apply (unfold_locales)
    3.85 +  apply (metis Upper_empty empty_subsetI sup_exists)
    3.86 +  apply (metis Lower_empty empty_subsetI inf_exists)
    3.87 +done
    3.88 +
    3.89 +lemma (in weak_complete_lattice) infI:
    3.90 +  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
    3.91 +  ==> P (\<Sqinter>A)"
    3.92 +proof (unfold inf_def)
    3.93 +  assume L: "A \<subseteq> carrier L"
    3.94 +    and P: "!!l. greatest L l (Lower L A) ==> P l"
    3.95 +  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
    3.96 +  with L show "P (SOME l. greatest L l (Lower L A))"
    3.97 +  by (fast intro: someI2 weak_greatest_unique P)
    3.98 +qed
    3.99 +
   3.100 +lemma (in weak_complete_lattice) inf_closed [simp]:
   3.101 +  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
   3.102 +  by (rule infI) simp_all
   3.103 +
   3.104 +lemma (in weak_complete_lattice) inf_cong:
   3.105 +  assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"
   3.106 +  shows "\<Sqinter> A .= \<Sqinter> B"
   3.107 +proof -
   3.108 +  have "\<And> x. is_glb L x A \<longleftrightarrow> is_glb L x B"
   3.109 +    by (rule greatest_Lower_cong_r, simp_all add: assms)
   3.110 +  moreover have "\<Sqinter> B \<in> carrier L"
   3.111 +    by (simp add: assms(2))
   3.112 +  ultimately show ?thesis
   3.113 +    by (simp add: inf_def)
   3.114 +qed
   3.115 +
   3.116 +theorem (in weak_partial_order) weak_complete_lattice_criterion1:
   3.117 +  assumes top_exists: "EX g. greatest L g (carrier L)"
   3.118 +    and inf_exists:
   3.119 +      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
   3.120 +  shows "weak_complete_lattice L"
   3.121 +proof (rule weak_complete_latticeI)
   3.122 +  from top_exists obtain top where top: "greatest L top (carrier L)" ..
   3.123 +  fix A
   3.124 +  assume L: "A \<subseteq> carrier L"
   3.125 +  let ?B = "Upper L A"
   3.126 +  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
   3.127 +  then have B_non_empty: "?B ~= {}" by fast
   3.128 +  have B_L: "?B \<subseteq> carrier L" by simp
   3.129 +  from inf_exists [OF B_L B_non_empty]
   3.130 +  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
   3.131 +  have "least L b (Upper L A)"
   3.132 +apply (rule least_UpperI)
   3.133 +   apply (rule greatest_le [where A = "Lower L ?B"])
   3.134 +    apply (rule b_inf_B)
   3.135 +   apply (rule Lower_memI)
   3.136 +    apply (erule Upper_memD [THEN conjunct1])
   3.137 +     apply assumption
   3.138 +    apply (rule L)
   3.139 +   apply (fast intro: L [THEN subsetD])
   3.140 +  apply (erule greatest_Lower_below [OF b_inf_B])
   3.141 +  apply simp
   3.142 + apply (rule L)
   3.143 +apply (rule greatest_closed [OF b_inf_B])
   3.144 +done
   3.145 +  then show "EX s. least L s (Upper L A)" ..
   3.146 +next
   3.147 +  fix A
   3.148 +  assume L: "A \<subseteq> carrier L"
   3.149 +  show "EX i. greatest L i (Lower L A)"
   3.150 +  proof (cases "A = {}")
   3.151 +    case True then show ?thesis
   3.152 +      by (simp add: top_exists)
   3.153 +  next
   3.154 +    case False with L show ?thesis
   3.155 +      by (rule inf_exists)
   3.156 +  qed
   3.157 +qed
   3.158 +
   3.159 +
   3.160 +text \<open>Supremum\<close>
   3.161 +
   3.162 +declare (in partial_order) weak_sup_of_singleton [simp del]
   3.163 +
   3.164 +lemma (in partial_order) sup_of_singleton [simp]:
   3.165 +  "x \<in> carrier L ==> \<Squnion>{x} = x"
   3.166 +  using weak_sup_of_singleton unfolding eq_is_equal .
   3.167 +
   3.168 +lemma (in upper_semilattice) join_assoc_lemma:
   3.169 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.170 +  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
   3.171 +  using weak_join_assoc_lemma L unfolding eq_is_equal .
   3.172 +
   3.173 +lemma (in upper_semilattice) join_assoc:
   3.174 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.175 +  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   3.176 +  using weak_join_assoc L unfolding eq_is_equal .
   3.177 +
   3.178 +
   3.179 +text \<open>Infimum\<close>
   3.180 +
   3.181 +declare (in partial_order) weak_inf_of_singleton [simp del]
   3.182 +
   3.183 +lemma (in partial_order) inf_of_singleton [simp]:
   3.184 +  "x \<in> carrier L ==> \<Sqinter>{x} = x"
   3.185 +  using weak_inf_of_singleton unfolding eq_is_equal .
   3.186 +
   3.187 +text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
   3.188 +
   3.189 +lemma (in lower_semilattice) meet_assoc_lemma:
   3.190 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.191 +  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
   3.192 +  using weak_meet_assoc_lemma L unfolding eq_is_equal .
   3.193 +
   3.194 +lemma (in lower_semilattice) meet_assoc:
   3.195 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.196 +  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   3.197 +  using weak_meet_assoc L unfolding eq_is_equal .
   3.198 +
   3.199 +
   3.200 +subsection \<open>Infimum Laws\<close>
   3.201 +
   3.202 +context weak_complete_lattice
   3.203 +begin
   3.204 +
   3.205 +lemma inf_glb: 
   3.206 +  assumes "A \<subseteq> carrier L"
   3.207 +  shows "greatest L (\<Sqinter>A) (Lower L A)"
   3.208 +proof -
   3.209 +  obtain i where "greatest L i (Lower L A)"
   3.210 +    by (metis assms inf_exists)
   3.211 +
   3.212 +  thus ?thesis
   3.213 +    apply (simp add: inf_def)
   3.214 +    apply (rule someI2[of _ "i"])
   3.215 +    apply (auto)
   3.216 +  done
   3.217 +qed
   3.218 +
   3.219 +lemma inf_lower:
   3.220 +  assumes "A \<subseteq> carrier L" "x \<in> A"
   3.221 +  shows "\<Sqinter>A \<sqsubseteq> x"
   3.222 +  by (metis assms greatest_Lower_below inf_glb)
   3.223 +
   3.224 +lemma inf_greatest: 
   3.225 +  assumes "A \<subseteq> carrier L" "z \<in> carrier L" 
   3.226 +          "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x)"
   3.227 +  shows "z \<sqsubseteq> \<Sqinter>A"
   3.228 +  by (metis Lower_memI assms greatest_le inf_glb)
   3.229 +
   3.230 +lemma weak_inf_empty [simp]: "\<Sqinter>{} .= \<top>"
   3.231 +  by (metis Lower_empty empty_subsetI inf_glb top_greatest weak_greatest_unique)
   3.232 +
   3.233 +lemma weak_inf_carrier [simp]: "\<Sqinter>carrier L .= \<bottom>"
   3.234 +  by (metis bottom_weak_eq inf_closed inf_lower subset_refl)
   3.235 +
   3.236 +lemma weak_inf_insert [simp]: 
   3.237 +  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
   3.238 +  apply (rule weak_le_antisym)
   3.239 +  apply (force intro: meet_le inf_greatest inf_lower inf_closed)
   3.240 +  apply (rule inf_greatest)
   3.241 +  apply (force)
   3.242 +  apply (force intro: inf_closed)
   3.243 +  apply (auto)
   3.244 +  apply (metis inf_closed meet_left)
   3.245 +  apply (force intro: le_trans inf_closed meet_right meet_left inf_lower)
   3.246 +done
   3.247 +
   3.248 +
   3.249 +subsection \<open>Supremum Laws\<close>
   3.250 +
   3.251 +lemma sup_lub: 
   3.252 +  assumes "A \<subseteq> carrier L"
   3.253 +  shows "least L (\<Squnion>A) (Upper L A)"
   3.254 +    by (metis Upper_is_closed assms least_closed least_cong supI sup_closed sup_exists weak_least_unique)
   3.255 +
   3.256 +lemma sup_upper: 
   3.257 +  assumes "A \<subseteq> carrier L" "x \<in> A"
   3.258 +  shows "x \<sqsubseteq> \<Squnion>A"
   3.259 +  by (metis assms least_Upper_above supI)
   3.260 +
   3.261 +lemma sup_least:
   3.262 +  assumes "A \<subseteq> carrier L" "z \<in> carrier L" 
   3.263 +          "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z)" 
   3.264 +  shows "\<Squnion>A \<sqsubseteq> z"
   3.265 +  by (metis Upper_memI assms least_le sup_lub)
   3.266 +
   3.267 +lemma weak_sup_empty [simp]: "\<Squnion>{} .= \<bottom>"
   3.268 +  by (metis Upper_empty bottom_least empty_subsetI sup_lub weak_least_unique)
   3.269 +
   3.270 +lemma weak_sup_carrier [simp]: "\<Squnion>carrier L .= \<top>"
   3.271 +  by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)
   3.272 +
   3.273 +lemma weak_sup_insert [simp]: 
   3.274 +  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Squnion>insert a A .= a \<squnion> \<Squnion>A"
   3.275 +  apply (rule weak_le_antisym)
   3.276 +  apply (rule sup_least)
   3.277 +  apply (auto)
   3.278 +  apply (metis join_left sup_closed)
   3.279 +  apply (rule le_trans) defer
   3.280 +  apply (rule join_right)
   3.281 +  apply (auto)
   3.282 +  apply (rule join_le)
   3.283 +  apply (auto intro: sup_upper sup_least sup_closed)
   3.284 +done
   3.285 +
   3.286 +end
   3.287 +
   3.288 +
   3.289 +subsection \<open>Fixed points of a lattice\<close>
   3.290 +
   3.291 +definition "fps L f = {x \<in> carrier L. f x .=\<^bsub>L\<^esub> x}"
   3.292 +
   3.293 +abbreviation "fpl L f \<equiv> L\<lparr>carrier := fps L f\<rparr>"
   3.294 +
   3.295 +lemma (in weak_partial_order) 
   3.296 +  use_fps: "x \<in> fps L f \<Longrightarrow> f x .= x"
   3.297 +  by (simp add: fps_def)
   3.298 +
   3.299 +lemma fps_carrier [simp]:
   3.300 +  "fps L f \<subseteq> carrier L"
   3.301 +  by (auto simp add: fps_def)
   3.302 +
   3.303 +lemma (in weak_complete_lattice) fps_sup_image: 
   3.304 +  assumes "f \<in> carrier L \<rightarrow> carrier L" "A \<subseteq> fps L f" 
   3.305 +  shows "\<Squnion> (f ` A) .= \<Squnion> A"
   3.306 +proof -
   3.307 +  from assms(2) have AL: "A \<subseteq> carrier L"
   3.308 +    by (auto simp add: fps_def)
   3.309 +  
   3.310 +  show ?thesis
   3.311 +  proof (rule sup_cong, simp_all add: AL)
   3.312 +    from assms(1) AL show "f ` A \<subseteq> carrier L"
   3.313 +      by (auto)
   3.314 +    from assms(2) show "f ` A {.=} A"
   3.315 +      apply (auto simp add: fps_def)
   3.316 +      apply (rule set_eqI2)
   3.317 +      apply blast
   3.318 +      apply (rename_tac b)
   3.319 +      apply (rule_tac x="f b" in bexI)
   3.320 +      apply (metis (mono_tags, lifting) Ball_Collect assms(1) Pi_iff local.sym)
   3.321 +      apply (auto)
   3.322 +    done
   3.323 +  qed
   3.324 +qed
   3.325 +
   3.326 +lemma (in weak_complete_lattice) fps_idem:
   3.327 +  "\<lbrakk> f \<in> carrier L \<rightarrow> carrier L; Idem f \<rbrakk> \<Longrightarrow> fps L f {.=} f ` carrier L"
   3.328 +  apply (rule set_eqI2)
   3.329 +  apply (auto simp add: idempotent_def fps_def)
   3.330 +  apply (metis Pi_iff local.sym)
   3.331 +  apply force
   3.332 +done
   3.333 +
   3.334 +context weak_complete_lattice
   3.335 +begin
   3.336 +
   3.337 +lemma weak_sup_pre_fixed_point: 
   3.338 +  assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"
   3.339 +  shows "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"
   3.340 +proof (rule sup_least)
   3.341 +  from assms(3) show AL: "A \<subseteq> carrier L"
   3.342 +    by (auto simp add: fps_def)
   3.343 +  thus fA: "f (\<Squnion>A) \<in> carrier L"
   3.344 +    by (simp add: assms funcset_carrier[of f L L])
   3.345 +  fix x
   3.346 +  assume xA: "x \<in> A"
   3.347 +  hence "x \<in> fps L f"
   3.348 +    using assms subsetCE by blast
   3.349 +  hence "f x .=\<^bsub>L\<^esub> x"
   3.350 +    by (auto simp add: fps_def)
   3.351 +  moreover have "f x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
   3.352 +    by (meson AL assms(2) subsetCE sup_closed sup_upper use_iso1 xA)
   3.353 +  ultimately show "x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
   3.354 +    by (meson AL fA assms(1) funcset_carrier le_cong local.refl subsetCE xA)
   3.355 +qed
   3.356 +
   3.357 +lemma weak_sup_post_fixed_point: 
   3.358 +  assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"
   3.359 +  shows "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"
   3.360 +proof (rule inf_greatest)
   3.361 +  from assms(3) show AL: "A \<subseteq> carrier L"
   3.362 +    by (auto simp add: fps_def)
   3.363 +  thus fA: "f (\<Sqinter>A) \<in> carrier L"
   3.364 +    by (simp add: assms funcset_carrier[of f L L])
   3.365 +  fix x
   3.366 +  assume xA: "x \<in> A"
   3.367 +  hence "x \<in> fps L f"
   3.368 +    using assms subsetCE by blast
   3.369 +  hence "f x .=\<^bsub>L\<^esub> x"
   3.370 +    by (auto simp add: fps_def)
   3.371 +  moreover have "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f x"
   3.372 +    by (meson AL assms(2) inf_closed inf_lower subsetCE use_iso1 xA)   
   3.373 +  ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> x"
   3.374 +    by (meson AL assms(1) fA funcset_carrier le_cong_r subsetCE xA)
   3.375 +qed
   3.376 +
   3.377 +
   3.378 +subsubsection \<open>Least fixed points\<close>
   3.379 +
   3.380 +lemma LFP_closed [intro, simp]:
   3.381 +  "\<mu> f \<in> carrier L"
   3.382 +  by (metis (lifting) LFP_def inf_closed mem_Collect_eq subsetI)
   3.383 +
   3.384 +lemma LFP_lowerbound: 
   3.385 +  assumes "x \<in> carrier L" "f x \<sqsubseteq> x" 
   3.386 +  shows "\<mu> f \<sqsubseteq> x"
   3.387 +  by (auto intro:inf_lower assms simp add:LFP_def)
   3.388 +
   3.389 +lemma LFP_greatest: 
   3.390 +  assumes "x \<in> carrier L" 
   3.391 +          "(\<And>u. \<lbrakk> u \<in> carrier L; f u \<sqsubseteq> u \<rbrakk> \<Longrightarrow> x \<sqsubseteq> u)"
   3.392 +  shows "x \<sqsubseteq> \<mu> f"
   3.393 +  by (auto simp add:LFP_def intro:inf_greatest assms)
   3.394 +
   3.395 +lemma LFP_lemma2: 
   3.396 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   3.397 +  shows "f (\<mu> f) \<sqsubseteq> \<mu> f"
   3.398 +  using assms
   3.399 +  apply (auto simp add:Pi_def)
   3.400 +  apply (rule LFP_greatest)
   3.401 +  apply (metis LFP_closed)
   3.402 +  apply (metis LFP_closed LFP_lowerbound le_trans use_iso1)
   3.403 +done
   3.404 +
   3.405 +lemma LFP_lemma3: 
   3.406 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   3.407 +  shows "\<mu> f \<sqsubseteq> f (\<mu> f)"
   3.408 +  using assms
   3.409 +  apply (auto simp add:Pi_def)
   3.410 +  apply (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
   3.411 +done
   3.412 +
   3.413 +lemma LFP_weak_unfold: 
   3.414 +  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<mu> f .= f (\<mu> f)"
   3.415 +  by (auto intro: LFP_lemma2 LFP_lemma3 funcset_mem)
   3.416 +
   3.417 +lemma LFP_fixed_point [intro]:
   3.418 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   3.419 +  shows "\<mu> f \<in> fps L f"
   3.420 +proof -
   3.421 +  have "f (\<mu> f) \<in> carrier L"
   3.422 +    using assms(2) by blast
   3.423 +  with assms show ?thesis
   3.424 +    by (simp add: LFP_weak_unfold fps_def local.sym)
   3.425 +qed
   3.426 +
   3.427 +lemma LFP_least_fixed_point:
   3.428 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
   3.429 +  shows "\<mu> f \<sqsubseteq> x"
   3.430 +  using assms by (force intro: LFP_lowerbound simp add: fps_def)
   3.431 +  
   3.432 +lemma LFP_idem: 
   3.433 +  assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
   3.434 +  shows "\<mu> f .= (f \<bottom>)"
   3.435 +proof (rule weak_le_antisym)
   3.436 +  from assms(1) show fb: "f \<bottom> \<in> carrier L"
   3.437 +    by (rule funcset_mem, simp)
   3.438 +  from assms show mf: "\<mu> f \<in> carrier L"
   3.439 +    by blast
   3.440 +  show "\<mu> f \<sqsubseteq> f \<bottom>"
   3.441 +  proof -
   3.442 +    have "f (f \<bottom>) .= f \<bottom>"
   3.443 +      by (auto simp add: fps_def fb assms(3) idempotent)
   3.444 +    moreover have "f (f \<bottom>) \<in> carrier L"
   3.445 +      by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
   3.446 +    ultimately show ?thesis
   3.447 +      by (auto intro: LFP_lowerbound simp add: fb)
   3.448 +  qed
   3.449 +  show "f \<bottom> \<sqsubseteq> \<mu> f"
   3.450 +  proof -
   3.451 +    have "f \<bottom> \<sqsubseteq> f (\<mu> f)"
   3.452 +      by (auto intro: use_iso1[of _ f] simp add: assms)
   3.453 +    moreover have "... .= \<mu> f"
   3.454 +      using assms(1) assms(2) fps_def by force
   3.455 +    moreover from assms(1) have "f (\<mu> f) \<in> carrier L"
   3.456 +      by (auto)
   3.457 +    ultimately show ?thesis
   3.458 +      using fb by blast
   3.459 +  qed
   3.460 +qed
   3.461 +
   3.462 +
   3.463 +subsubsection \<open>Greatest fixed points\<close>
   3.464 +  
   3.465 +lemma GFP_closed [intro, simp]:
   3.466 +  "\<nu> f \<in> carrier L"
   3.467 +  by (auto intro:sup_closed simp add:GFP_def)
   3.468 +  
   3.469 +lemma GFP_upperbound:
   3.470 +  assumes "x \<in> carrier L" "x \<sqsubseteq> f x"
   3.471 +  shows "x \<sqsubseteq> \<nu> f"
   3.472 +  by (auto intro:sup_upper assms simp add:GFP_def)
   3.473 +
   3.474 +lemma GFP_least: 
   3.475 +  assumes "x \<in> carrier L" 
   3.476 +          "(\<And>u. \<lbrakk> u \<in> carrier L; u \<sqsubseteq> f u \<rbrakk> \<Longrightarrow> u \<sqsubseteq> x)"
   3.477 +  shows "\<nu> f \<sqsubseteq> x"
   3.478 +  by (auto simp add:GFP_def intro:sup_least assms)
   3.479 +
   3.480 +lemma GFP_lemma2:
   3.481 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   3.482 +  shows "\<nu> f \<sqsubseteq> f (\<nu> f)"
   3.483 +  using assms
   3.484 +  apply (auto simp add:Pi_def)
   3.485 +  apply (rule GFP_least)
   3.486 +  apply (metis GFP_closed)
   3.487 +  apply (metis GFP_closed GFP_upperbound le_trans use_iso2)
   3.488 +done
   3.489 +
   3.490 +lemma GFP_lemma3:
   3.491 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   3.492 +  shows "f (\<nu> f) \<sqsubseteq> \<nu> f"
   3.493 +  by (metis GFP_closed GFP_lemma2 GFP_upperbound assms funcset_mem use_iso2)
   3.494 +  
   3.495 +lemma GFP_weak_unfold: 
   3.496 +  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<nu> f .= f (\<nu> f)"
   3.497 +  by (auto intro: GFP_lemma2 GFP_lemma3 funcset_mem)
   3.498 +
   3.499 +lemma (in weak_complete_lattice) GFP_fixed_point [intro]:
   3.500 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   3.501 +  shows "\<nu> f \<in> fps L f"
   3.502 +  using assms
   3.503 +proof -
   3.504 +  have "f (\<nu> f) \<in> carrier L"
   3.505 +    using assms(2) by blast
   3.506 +  with assms show ?thesis
   3.507 +    by (simp add: GFP_weak_unfold fps_def local.sym)
   3.508 +qed
   3.509 +
   3.510 +lemma GFP_greatest_fixed_point:
   3.511 +  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
   3.512 +  shows "x \<sqsubseteq> \<nu> f"
   3.513 +  using assms 
   3.514 +  by (rule_tac GFP_upperbound, auto simp add: fps_def, meson PiE local.sym weak_refl)
   3.515 +    
   3.516 +lemma GFP_idem: 
   3.517 +  assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
   3.518 +  shows "\<nu> f .= (f \<top>)"
   3.519 +proof (rule weak_le_antisym)
   3.520 +  from assms(1) show fb: "f \<top> \<in> carrier L"
   3.521 +    by (rule funcset_mem, simp)
   3.522 +  from assms show mf: "\<nu> f \<in> carrier L"
   3.523 +    by blast
   3.524 +  show "f \<top> \<sqsubseteq> \<nu> f"
   3.525 +  proof -
   3.526 +    have "f (f \<top>) .= f \<top>"
   3.527 +      by (auto simp add: fps_def fb assms(3) idempotent)
   3.528 +    moreover have "f (f \<top>) \<in> carrier L"
   3.529 +      by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
   3.530 +    ultimately show ?thesis
   3.531 +      by (rule_tac GFP_upperbound, simp_all add: fb local.sym)
   3.532 +  qed
   3.533 +  show "\<nu> f \<sqsubseteq> f \<top>"
   3.534 +  proof -
   3.535 +    have "\<nu> f \<sqsubseteq> f (\<nu> f)"
   3.536 +      by (simp add: GFP_lemma2 assms(1) assms(2))
   3.537 +    moreover have "... \<sqsubseteq> f \<top>"
   3.538 +      by (auto intro: use_iso1[of _ f] simp add: assms)
   3.539 +    moreover from assms(1) have "f (\<nu> f) \<in> carrier L"
   3.540 +      by (auto)
   3.541 +    ultimately show ?thesis
   3.542 +      using fb local.le_trans by blast
   3.543 +  qed
   3.544 +qed
   3.545 +
   3.546 +end
   3.547 +
   3.548 +
   3.549 +subsection \<open>Complete lattices where @{text eq} is the Equality\<close>
   3.550 +
   3.551 +locale complete_lattice = partial_order +
   3.552 +  assumes sup_exists:
   3.553 +    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   3.554 +    and inf_exists:
   3.555 +    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   3.556 +
   3.557 +sublocale complete_lattice \<subseteq> lattice
   3.558 +proof
   3.559 +  fix x y
   3.560 +  assume a: "x \<in> carrier L" "y \<in> carrier L"
   3.561 +  thus "\<exists>s. is_lub L s {x, y}"
   3.562 +    by (rule_tac sup_exists[of "{x, y}"], auto)
   3.563 +  from a show "\<exists>s. is_glb L s {x, y}"
   3.564 +    by (rule_tac inf_exists[of "{x, y}"], auto)
   3.565 +qed
   3.566 +
   3.567 +sublocale complete_lattice \<subseteq> weak?: weak_complete_lattice
   3.568 +  by standard (auto intro: sup_exists inf_exists)
   3.569 +
   3.570 +lemma complete_lattice_lattice [simp]: 
   3.571 +  assumes "complete_lattice X"
   3.572 +  shows "lattice X"
   3.573 +proof -
   3.574 +  interpret c: complete_lattice X
   3.575 +    by (simp add: assms)
   3.576 +  show ?thesis
   3.577 +    by (unfold_locales)
   3.578 +qed
   3.579 +
   3.580 +text \<open>Introduction rule: the usual definition of complete lattice\<close>
   3.581 +
   3.582 +lemma (in partial_order) complete_latticeI:
   3.583 +  assumes sup_exists:
   3.584 +    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   3.585 +    and inf_exists:
   3.586 +    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   3.587 +  shows "complete_lattice L"
   3.588 +  by standard (auto intro: sup_exists inf_exists)
   3.589 +
   3.590 +theorem (in partial_order) complete_lattice_criterion1:
   3.591 +  assumes top_exists: "EX g. greatest L g (carrier L)"
   3.592 +    and inf_exists:
   3.593 +      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
   3.594 +  shows "complete_lattice L"
   3.595 +proof (rule complete_latticeI)
   3.596 +  from top_exists obtain top where top: "greatest L top (carrier L)" ..
   3.597 +  fix A
   3.598 +  assume L: "A \<subseteq> carrier L"
   3.599 +  let ?B = "Upper L A"
   3.600 +  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
   3.601 +  then have B_non_empty: "?B ~= {}" by fast
   3.602 +  have B_L: "?B \<subseteq> carrier L" by simp
   3.603 +  from inf_exists [OF B_L B_non_empty]
   3.604 +  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
   3.605 +  have "least L b (Upper L A)"
   3.606 +apply (rule least_UpperI)
   3.607 +   apply (rule greatest_le [where A = "Lower L ?B"])
   3.608 +    apply (rule b_inf_B)
   3.609 +   apply (rule Lower_memI)
   3.610 +    apply (erule Upper_memD [THEN conjunct1])
   3.611 +     apply assumption
   3.612 +    apply (rule L)
   3.613 +   apply (fast intro: L [THEN subsetD])
   3.614 +  apply (erule greatest_Lower_below [OF b_inf_B])
   3.615 +  apply simp
   3.616 + apply (rule L)
   3.617 +apply (rule greatest_closed [OF b_inf_B])
   3.618 +done
   3.619 +  then show "EX s. least L s (Upper L A)" ..
   3.620 +next
   3.621 +  fix A
   3.622 +  assume L: "A \<subseteq> carrier L"
   3.623 +  show "EX i. greatest L i (Lower L A)"
   3.624 +  proof (cases "A = {}")
   3.625 +    case True then show ?thesis
   3.626 +      by (simp add: top_exists)
   3.627 +  next
   3.628 +    case False with L show ?thesis
   3.629 +      by (rule inf_exists)
   3.630 +  qed
   3.631 +qed
   3.632 +
   3.633 +(* TODO: prove dual version *)
   3.634 +
   3.635 +subsection \<open>Fixed points\<close>
   3.636 +
   3.637 +context complete_lattice
   3.638 +begin
   3.639 +
   3.640 +lemma LFP_unfold: 
   3.641 +  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<mu> f = f (\<mu> f)"
   3.642 +  using eq_is_equal weak.LFP_weak_unfold by auto
   3.643 +
   3.644 +lemma LFP_const:
   3.645 +  "t \<in> carrier L \<Longrightarrow> \<mu> (\<lambda> x. t) = t"
   3.646 +  by (simp add: local.le_antisym weak.LFP_greatest weak.LFP_lowerbound)
   3.647 +
   3.648 +lemma LFP_id:
   3.649 +  "\<mu> id = \<bottom>"
   3.650 +  by (simp add: local.le_antisym weak.LFP_lowerbound)
   3.651 +
   3.652 +lemma GFP_unfold:
   3.653 +  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<nu> f = f (\<nu> f)"
   3.654 +  using eq_is_equal weak.GFP_weak_unfold by auto
   3.655 +
   3.656 +lemma GFP_const:
   3.657 +  "t \<in> carrier L \<Longrightarrow> \<nu> (\<lambda> x. t) = t"
   3.658 +  by (simp add: local.le_antisym weak.GFP_least weak.GFP_upperbound)
   3.659 +
   3.660 +lemma GFP_id:
   3.661 +  "\<nu> id = \<top>"
   3.662 +  using weak.GFP_upperbound by auto
   3.663 +
   3.664 +end
   3.665 +
   3.666 +
   3.667 +subsection \<open>Interval complete lattices\<close>
   3.668 +  
   3.669 +context weak_complete_lattice
   3.670 +begin
   3.671 +
   3.672 +  lemma at_least_at_most_Sup:
   3.673 +    "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"
   3.674 +    apply (rule weak_le_antisym)
   3.675 +    apply (rule sup_least)
   3.676 +    apply (auto simp add: at_least_at_most_closed)
   3.677 +    apply (rule sup_upper)
   3.678 +    apply (auto simp add: at_least_at_most_closed)
   3.679 +  done
   3.680 +
   3.681 +  lemma at_least_at_most_Inf:
   3.682 +    "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"
   3.683 +    apply (rule weak_le_antisym)
   3.684 +    apply (rule inf_lower)
   3.685 +    apply (auto simp add: at_least_at_most_closed)
   3.686 +    apply (rule inf_greatest)
   3.687 +    apply (auto simp add: at_least_at_most_closed)
   3.688 +  done
   3.689 +
   3.690 +end
   3.691 +
   3.692 +lemma weak_complete_lattice_interval:
   3.693 +  assumes "weak_complete_lattice L" "a \<in> carrier L" "b \<in> carrier L" "a \<sqsubseteq>\<^bsub>L\<^esub> b"
   3.694 +  shows "weak_complete_lattice (L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>)"
   3.695 +proof -
   3.696 +  interpret L: weak_complete_lattice L
   3.697 +    by (simp add: assms)
   3.698 +  interpret weak_partial_order "L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>"
   3.699 +  proof -
   3.700 +    have "\<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<subseteq> carrier L"
   3.701 +      by (auto, simp add: at_least_at_most_def)
   3.702 +    thus "weak_partial_order (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
   3.703 +      by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
   3.704 +  qed
   3.705 +
   3.706 +  show ?thesis
   3.707 +  proof
   3.708 +    fix A
   3.709 +    assume a: "A \<subseteq> carrier (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
   3.710 +    show "\<exists>s. is_lub (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
   3.711 +    proof (cases "A = {}")
   3.712 +      case True
   3.713 +      thus ?thesis
   3.714 +        by (rule_tac x="a" in exI, auto simp add: least_def assms)
   3.715 +    next
   3.716 +      case False
   3.717 +      show ?thesis
   3.718 +      proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)
   3.719 +        show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
   3.720 +          using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
   3.721 +        show "\<And>y. y \<in> Upper (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
   3.722 +          using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
   3.723 +        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
   3.724 +          by (auto)
   3.725 +        from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
   3.726 +          apply (rule_tac L.at_least_at_most_member)
   3.727 +          apply (auto)
   3.728 +          apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)
   3.729 +          apply (meson False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed b all_not_in_conv assms(2) contra_subsetD subset_trans)
   3.730 +          apply (rule L.sup_least)
   3.731 +          apply (auto simp add: assms)
   3.732 +          using L.at_least_at_most_closed apply blast
   3.733 +        done
   3.734 +      qed
   3.735 +    qed
   3.736 +    show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
   3.737 +    proof (cases "A = {}")
   3.738 +      case True
   3.739 +      thus ?thesis
   3.740 +        by (rule_tac x="b" in exI, auto simp add: greatest_def assms)
   3.741 +    next
   3.742 +      case False
   3.743 +      show ?thesis
   3.744 +      proof (rule_tac x="\<Sqinter>\<^bsub>L\<^esub> A" in exI, rule greatest_LowerI, simp_all)
   3.745 +        show b:"\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"
   3.746 +          using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
   3.747 +        show "\<And>y. y \<in> Lower (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> y \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
   3.748 +           using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
   3.749 +        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
   3.750 +          by (auto)
   3.751 +        from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
   3.752 +          apply (rule_tac L.at_least_at_most_member)
   3.753 +          apply (auto)
   3.754 +          apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)
   3.755 +          apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans)
   3.756 +          apply (meson False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.le_trans b all_not_in_conv assms(3) contra_subsetD subset_trans)            
   3.757 +        done
   3.758 +      qed
   3.759 +    qed
   3.760 +  qed
   3.761 +qed
   3.762 +
   3.763 +
   3.764 +subsection \<open>Knaster-Tarski theorem and variants\<close>
   3.765 +  
   3.766 +text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>
   3.767 +
   3.768 +theorem Knaster_Tarski:
   3.769 +  assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"
   3.770 +  shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
   3.771 +proof -
   3.772 +  interpret L: weak_complete_lattice L
   3.773 +    by (simp add: assms)
   3.774 +  interpret weak_partial_order ?L'
   3.775 +  proof -
   3.776 +    have "{x \<in> carrier L. f x .=\<^bsub>L\<^esub> x} \<subseteq> carrier L"
   3.777 +      by (auto)
   3.778 +    thus "weak_partial_order ?L'"
   3.779 +      by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
   3.780 +  qed
   3.781 +  show ?thesis
   3.782 +  proof (unfold_locales, simp_all)
   3.783 +    fix A
   3.784 +    assume A: "A \<subseteq> fps L f"
   3.785 +    show "\<exists>s. is_lub (fpl L f) s A"
   3.786 +    proof
   3.787 +      from A have AL: "A \<subseteq> carrier L"
   3.788 +        by (meson fps_carrier subset_eq)
   3.789 +
   3.790 +      let ?w = "\<Squnion>\<^bsub>L\<^esub> A"
   3.791 +      have w: "f (\<Squnion>\<^bsub>L\<^esub>A) \<in> carrier L"
   3.792 +        by (rule funcset_mem[of f "carrier L"], simp_all add: AL assms(2))
   3.793 +
   3.794 +      have pf_w: "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"
   3.795 +        by (simp add: A L.weak_sup_pre_fixed_point assms(2) assms(3))
   3.796 +
   3.797 +      have f_top_chain: "f ` \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<subseteq> \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
   3.798 +      proof (auto simp add: at_least_at_most_def)
   3.799 +        fix x
   3.800 +        assume b: "x \<in> carrier L" "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"
   3.801 +        from b show fx: "f x \<in> carrier L"
   3.802 +          using assms(2) by blast
   3.803 +        show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f x"
   3.804 +        proof -
   3.805 +          have "?w \<sqsubseteq>\<^bsub>L\<^esub> f ?w"
   3.806 +          proof (rule_tac L.sup_least, simp_all add: AL w)
   3.807 +            fix y
   3.808 +            assume c: "y \<in> A" 
   3.809 +            hence y: "y \<in> fps L f"
   3.810 +              using A subsetCE by blast
   3.811 +            with assms have "y .=\<^bsub>L\<^esub> f y"
   3.812 +            proof -
   3.813 +              from y have "y \<in> carrier L"
   3.814 +                by (simp add: fps_def)
   3.815 +              moreover hence "f y \<in> carrier L"
   3.816 +                by (rule_tac funcset_mem[of f "carrier L"], simp_all add: assms)
   3.817 +              ultimately show ?thesis using y
   3.818 +                by (rule_tac L.sym, simp_all add: L.use_fps)
   3.819 +            qed              
   3.820 +            moreover have "y \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
   3.821 +              by (simp add: AL L.sup_upper c(1))
   3.822 +            ultimately show "y \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
   3.823 +              by (meson fps_def AL funcset_mem L.refl L.weak_complete_lattice_axioms assms(2) assms(3) c(1) isotone_def rev_subsetD weak_complete_lattice.sup_closed weak_partial_order.le_cong)
   3.824 +          qed
   3.825 +          thus ?thesis
   3.826 +            by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) b(1) b(2) use_iso2)
   3.827 +        qed
   3.828 +   
   3.829 +        show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>L\<^esub>"
   3.830 +          by (simp add: fx)
   3.831 +      qed
   3.832 +  
   3.833 +      let ?L' = "L\<lparr> carrier := \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rparr>"
   3.834 +
   3.835 +      interpret L': weak_complete_lattice ?L'
   3.836 +        by (auto intro: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
   3.837 +
   3.838 +      let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
   3.839 +
   3.840 +      show "is_lub ?L'' (\<mu>\<^bsub>?L'\<^esub> f) A"
   3.841 +      proof (rule least_UpperI, simp_all)
   3.842 +        fix x
   3.843 +        assume "x \<in> Upper ?L'' A"
   3.844 +        hence "\<mu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
   3.845 +          apply (rule_tac L'.LFP_lowerbound)
   3.846 +          apply (auto simp add: Upper_def)
   3.847 +          apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)          
   3.848 +          apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)
   3.849 +          apply (auto)
   3.850 +          apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
   3.851 +        done
   3.852 +        thus " \<mu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
   3.853 +          by (simp)
   3.854 +      next
   3.855 +        fix x
   3.856 +        assume xA: "x \<in> A"
   3.857 +        show "x \<sqsubseteq>\<^bsub>L\<^esub> \<mu>\<^bsub>?L'\<^esub> f"
   3.858 +        proof -
   3.859 +          have "\<mu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
   3.860 +            by blast
   3.861 +          thus ?thesis
   3.862 +            by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed L.sup_upper xA subsetCE)
   3.863 +        qed
   3.864 +      next
   3.865 +        show "A \<subseteq> fps L f"
   3.866 +          by (simp add: A)
   3.867 +      next
   3.868 +        show "\<mu>\<^bsub>?L'\<^esub> f \<in> fps L f"
   3.869 +        proof (auto simp add: fps_def)
   3.870 +          have "\<mu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
   3.871 +            by (rule L'.LFP_closed)
   3.872 +          thus c:"\<mu>\<^bsub>?L'\<^esub> f \<in> carrier L"
   3.873 +             by (auto simp add: at_least_at_most_def)
   3.874 +          have "\<mu>\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (\<mu>\<^bsub>?L'\<^esub> f)"
   3.875 +          proof (rule "L'.LFP_weak_unfold", simp_all)
   3.876 +            show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
   3.877 +              apply (auto simp add: Pi_def at_least_at_most_def)
   3.878 +              using assms(2) apply blast
   3.879 +              apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
   3.880 +              using assms(2) apply blast
   3.881 +            done
   3.882 +            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
   3.883 +              apply (auto simp add: isotone_def)
   3.884 +              using L'.weak_partial_order_axioms apply blast
   3.885 +              apply (meson L.at_least_at_most_closed subsetCE)
   3.886 +            done
   3.887 +          qed
   3.888 +          thus "f (\<mu>\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> \<mu>\<^bsub>?L'\<^esub> f"
   3.889 +            by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
   3.890 +        qed
   3.891 +      qed
   3.892 +    qed
   3.893 +    show "\<exists>i. is_glb (L\<lparr>carrier := fps L f\<rparr>) i A"
   3.894 +    proof
   3.895 +      from A have AL: "A \<subseteq> carrier L"
   3.896 +        by (meson fps_carrier subset_eq)
   3.897 +
   3.898 +      let ?w = "\<Sqinter>\<^bsub>L\<^esub> A"
   3.899 +      have w: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> carrier L"
   3.900 +        by (simp add: AL funcset_carrier' assms(2))
   3.901 +
   3.902 +      have pf_w: "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"
   3.903 +        by (simp add: A L.weak_sup_post_fixed_point assms(2) assms(3))
   3.904 +
   3.905 +      have f_bot_chain: "f ` \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<subseteq> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
   3.906 +      proof (auto simp add: at_least_at_most_def)
   3.907 +        fix x
   3.908 +        assume b: "x \<in> carrier L" "x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
   3.909 +        from b show fx: "f x \<in> carrier L"
   3.910 +          using assms(2) by blast
   3.911 +        show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
   3.912 +        proof -
   3.913 +          have "f ?w \<sqsubseteq>\<^bsub>L\<^esub> ?w"
   3.914 +          proof (rule_tac L.inf_greatest, simp_all add: AL w)
   3.915 +            fix y
   3.916 +            assume c: "y \<in> A" 
   3.917 +            with assms have "y .=\<^bsub>L\<^esub> f y"
   3.918 +              by (metis (no_types, lifting) A funcset_carrier'[OF assms(2)] L.sym fps_def mem_Collect_eq subset_eq)
   3.919 +            moreover have "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
   3.920 +              by (simp add: AL L.inf_lower c)
   3.921 +            ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> y"
   3.922 +              by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w)
   3.923 +          qed
   3.924 +          thus ?thesis
   3.925 +            by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
   3.926 +        qed
   3.927 +   
   3.928 +        show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"
   3.929 +          by (simp add: fx)
   3.930 +      qed
   3.931 +  
   3.932 +      let ?L' = "L\<lparr> carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rparr>"
   3.933 +
   3.934 +      interpret L': weak_complete_lattice ?L'
   3.935 +        by (auto intro!: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
   3.936 +
   3.937 +      let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
   3.938 +
   3.939 +      show "is_glb ?L'' (\<nu>\<^bsub>?L'\<^esub> f) A"
   3.940 +      proof (rule greatest_LowerI, simp_all)
   3.941 +        fix x
   3.942 +        assume "x \<in> Lower ?L'' A"
   3.943 +        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
   3.944 +          apply (rule_tac L'.GFP_upperbound)
   3.945 +          apply (auto simp add: Lower_def)
   3.946 +          apply (meson A AL L.at_least_at_most_member L.bottom_lower L.weak_complete_lattice_axioms fps_carrier subsetCE weak_complete_lattice.inf_greatest)
   3.947 +          apply (simp add: funcset_carrier' L.sym assms(2) fps_def)          
   3.948 +        done
   3.949 +        thus "x \<sqsubseteq>\<^bsub>L\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
   3.950 +          by (simp)
   3.951 +      next
   3.952 +        fix x
   3.953 +        assume xA: "x \<in> A"
   3.954 +        show "\<nu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
   3.955 +        proof -
   3.956 +          have "\<nu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
   3.957 +            by blast
   3.958 +          thus ?thesis
   3.959 +            by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.inf_lower L.le_trans subsetCE xA)     
   3.960 +        qed
   3.961 +      next
   3.962 +        show "A \<subseteq> fps L f"
   3.963 +          by (simp add: A)
   3.964 +      next
   3.965 +        show "\<nu>\<^bsub>?L'\<^esub> f \<in> fps L f"
   3.966 +        proof (auto simp add: fps_def)
   3.967 +          have "\<nu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
   3.968 +            by (rule L'.GFP_closed)
   3.969 +          thus c:"\<nu>\<^bsub>?L'\<^esub> f \<in> carrier L"
   3.970 +             by (auto simp add: at_least_at_most_def)
   3.971 +          have "\<nu>\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (\<nu>\<^bsub>?L'\<^esub> f)"
   3.972 +          proof (rule "L'.GFP_weak_unfold", simp_all)
   3.973 +            show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
   3.974 +              apply (auto simp add: Pi_def at_least_at_most_def)
   3.975 +              using assms(2) apply blast
   3.976 +              apply (simp add: funcset_carrier' assms(2))
   3.977 +              apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
   3.978 +            done
   3.979 +            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
   3.980 +              apply (auto simp add: isotone_def)
   3.981 +              using L'.weak_partial_order_axioms apply blast
   3.982 +              using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
   3.983 +            done
   3.984 +          qed
   3.985 +          thus "f (\<nu>\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
   3.986 +            by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
   3.987 +        qed
   3.988 +      qed
   3.989 +    qed
   3.990 +  qed
   3.991 +qed
   3.992 +
   3.993 +theorem Knaster_Tarski_top:
   3.994 +  assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
   3.995 +  shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> \<nu>\<^bsub>L\<^esub> f"
   3.996 +proof -
   3.997 +  interpret L: weak_complete_lattice L
   3.998 +    by (simp add: assms)
   3.999 +  interpret L': weak_complete_lattice "fpl L f"
  3.1000 +    by (rule Knaster_Tarski, simp_all add: assms)
  3.1001 +  show ?thesis
  3.1002 +  proof (rule L.weak_le_antisym, simp_all)
  3.1003 +    show "\<top>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> \<nu>\<^bsub>L\<^esub> f"
  3.1004 +      by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified])
  3.1005 +    show "\<nu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
  3.1006 +    proof -
  3.1007 +      have "\<nu>\<^bsub>L\<^esub> f \<in> fps L f"
  3.1008 +        by (rule L.GFP_fixed_point, simp_all add: assms)
  3.1009 +      hence "\<nu>\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
  3.1010 +        by simp
  3.1011 +      hence "\<nu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
  3.1012 +        by (rule L'.top_higher)
  3.1013 +      thus ?thesis
  3.1014 +        by simp
  3.1015 +    qed
  3.1016 +    show "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"
  3.1017 +    proof -
  3.1018 +      have "carrier (fpl L f) \<subseteq> carrier L"
  3.1019 +        by (auto simp add: fps_def)
  3.1020 +      with L'.top_closed show ?thesis
  3.1021 +        by blast
  3.1022 +    qed
  3.1023 +  qed
  3.1024 +qed
  3.1025 +
  3.1026 +theorem Knaster_Tarski_bottom:
  3.1027 +  assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
  3.1028 +  shows "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> \<mu>\<^bsub>L\<^esub> f"
  3.1029 +proof -
  3.1030 +  interpret L: weak_complete_lattice L
  3.1031 +    by (simp add: assms)
  3.1032 +  interpret L': weak_complete_lattice "fpl L f"
  3.1033 +    by (rule Knaster_Tarski, simp_all add: assms)
  3.1034 +  show ?thesis
  3.1035 +  proof (rule L.weak_le_antisym, simp_all)
  3.1036 +    show "\<mu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<bottom>\<^bsub>fpl L f\<^esub>"
  3.1037 +      by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified])
  3.1038 +    show "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> \<mu>\<^bsub>L\<^esub> f"
  3.1039 +    proof -
  3.1040 +      have "\<mu>\<^bsub>L\<^esub> f \<in> fps L f"
  3.1041 +        by (rule L.LFP_fixed_point, simp_all add: assms)
  3.1042 +      hence "\<mu>\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
  3.1043 +        by simp
  3.1044 +      hence "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<mu>\<^bsub>L\<^esub> f"
  3.1045 +        by (rule L'.bottom_lower)
  3.1046 +      thus ?thesis
  3.1047 +        by simp
  3.1048 +    qed
  3.1049 +    show "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"
  3.1050 +    proof -
  3.1051 +      have "carrier (fpl L f) \<subseteq> carrier L"
  3.1052 +        by (auto simp add: fps_def)
  3.1053 +      with L'.bottom_closed show ?thesis
  3.1054 +        by blast
  3.1055 +    qed
  3.1056 +  qed
  3.1057 +qed
  3.1058 +
  3.1059 +text \<open>If a function is both idempotent and isotone then the image of the function forms a complete lattice\<close>
  3.1060 +  
  3.1061 +theorem Knaster_Tarski_idem:
  3.1062 +  assumes "complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "idempotent L f"
  3.1063 +  shows "complete_lattice (L\<lparr>carrier := f ` carrier L\<rparr>)"
  3.1064 +proof -
  3.1065 +  interpret L: complete_lattice L
  3.1066 +    by (simp add: assms)
  3.1067 +  have "fps L f = f ` carrier L"
  3.1068 +    using L.weak.fps_idem[OF assms(2) assms(4)]
  3.1069 +    by (simp add: L.set_eq_is_eq)
  3.1070 +  then interpret L': weak_complete_lattice "(L\<lparr>carrier := f ` carrier L\<rparr>)"
  3.1071 +    by (metis Knaster_Tarski L.weak.weak_complete_lattice_axioms assms(2) assms(3))
  3.1072 +  show ?thesis
  3.1073 +    using L'.sup_exists L'.inf_exists
  3.1074 +    by (unfold_locales, auto simp add: L.eq_is_equal)
  3.1075 +qed
  3.1076 +
  3.1077 +theorem Knaster_Tarski_idem_extremes:
  3.1078 +  assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \<in> carrier L \<rightarrow> carrier L"
  3.1079 +  shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<top>\<^bsub>L\<^esub>)" "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<bottom>\<^bsub>L\<^esub>)"
  3.1080 +proof -
  3.1081 +  interpret L: weak_complete_lattice "L"
  3.1082 +    by (simp_all add: assms)
  3.1083 +  interpret L': weak_complete_lattice "fpl L f"
  3.1084 +    by (rule Knaster_Tarski, simp_all add: assms)
  3.1085 +  have FA: "fps L f \<subseteq> carrier L"
  3.1086 +    by (auto simp add: fps_def)
  3.1087 +  show "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<top>\<^bsub>L\<^esub>)"
  3.1088 +  proof -
  3.1089 +    from FA have "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"
  3.1090 +    proof -
  3.1091 +      have "\<top>\<^bsub>fpl L f\<^esub> \<in> fps L f"
  3.1092 +        using L'.top_closed by auto
  3.1093 +      thus ?thesis
  3.1094 +        using FA by blast
  3.1095 +    qed
  3.1096 +    moreover with assms have "f \<top>\<^bsub>L\<^esub> \<in> carrier L"
  3.1097 +      by (auto)
  3.1098 +
  3.1099 +    ultimately show ?thesis
  3.1100 +      using L.trans[OF Knaster_Tarski_top[of L f] L.GFP_idem[of f]]
  3.1101 +      by (simp_all add: assms)
  3.1102 +  qed
  3.1103 +  show "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<bottom>\<^bsub>L\<^esub>)"
  3.1104 +  proof -
  3.1105 +    from FA have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"
  3.1106 +    proof -
  3.1107 +      have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> fps L f"
  3.1108 +        using L'.bottom_closed by auto
  3.1109 +      thus ?thesis
  3.1110 +        using FA by blast
  3.1111 +    qed
  3.1112 +    moreover with assms have "f \<bottom>\<^bsub>L\<^esub> \<in> carrier L"
  3.1113 +      by (auto)
  3.1114 +
  3.1115 +    ultimately show ?thesis
  3.1116 +      using L.trans[OF Knaster_Tarski_bottom[of L f] L.LFP_idem[of f]]
  3.1117 +      by (simp_all add: assms)
  3.1118 +  qed
  3.1119 +qed
  3.1120 +
  3.1121 +
  3.1122 +subsection \<open>Examples\<close>
  3.1123 +
  3.1124 +subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
  3.1125 +
  3.1126 +theorem powerset_is_complete_lattice:
  3.1127 +  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
  3.1128 +  (is "complete_lattice ?L")
  3.1129 +proof (rule partial_order.complete_latticeI)
  3.1130 +  show "partial_order ?L"
  3.1131 +    by standard auto
  3.1132 +next
  3.1133 +  fix B
  3.1134 +  assume "B \<subseteq> carrier ?L"
  3.1135 +  then have "least ?L (\<Union> B) (Upper ?L B)"
  3.1136 +    by (fastforce intro!: least_UpperI simp: Upper_def)
  3.1137 +  then show "EX s. least ?L s (Upper ?L B)" ..
  3.1138 +next
  3.1139 +  fix B
  3.1140 +  assume "B \<subseteq> carrier ?L"
  3.1141 +  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
  3.1142 +    txt \<open>@{term "\<Inter> B"} is not the infimum of @{term B}:
  3.1143 +      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! \<close>
  3.1144 +    by (fastforce intro!: greatest_LowerI simp: Lower_def)
  3.1145 +  then show "EX i. greatest ?L i (Lower ?L B)" ..
  3.1146 +qed
  3.1147 +
  3.1148 +text \<open>Another example, that of the lattice of subgroups of a group,
  3.1149 +  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
  3.1150 +
  3.1151 +
  3.1152 +subsection \<open>Limit preserving functions\<close>
  3.1153 +
  3.1154 +definition weak_sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
  3.1155 +"weak_sup_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. A \<noteq> {} \<longrightarrow> f (\<Squnion>\<^bsub>X\<^esub> A) = (\<Squnion>\<^bsub>Y\<^esub> (f ` A)))"
  3.1156 +
  3.1157 +definition sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
  3.1158 +"sup_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. f (\<Squnion>\<^bsub>X\<^esub> A) = (\<Squnion>\<^bsub>Y\<^esub> (f ` A)))"
  3.1159 +
  3.1160 +definition weak_inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
  3.1161 +"weak_inf_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. A \<noteq> {} \<longrightarrow> f (\<Sqinter>\<^bsub>X\<^esub> A) = (\<Sqinter>\<^bsub>Y\<^esub> (f ` A)))"
  3.1162 +
  3.1163 +definition inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
  3.1164 +"inf_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. f (\<Sqinter>\<^bsub>X\<^esub> A) = (\<Sqinter>\<^bsub>Y\<^esub> (f ` A)))"
  3.1165 +
  3.1166 +lemma weak_sup_pres:
  3.1167 +  "sup_pres X Y f \<Longrightarrow> weak_sup_pres X Y f"
  3.1168 +  by (simp add: sup_pres_def weak_sup_pres_def)
  3.1169 +
  3.1170 +lemma weak_inf_pres:
  3.1171 +  "inf_pres X Y f \<Longrightarrow> weak_inf_pres X Y f"
  3.1172 +  by (simp add: inf_pres_def weak_inf_pres_def)
  3.1173 +
  3.1174 +lemma sup_pres_is_join_pres:
  3.1175 +  assumes "weak_sup_pres X Y f"
  3.1176 +  shows "join_pres X Y f"
  3.1177 +  using assms
  3.1178 +  apply (simp add: join_pres_def weak_sup_pres_def, safe)
  3.1179 +  apply (rename_tac x y)
  3.1180 +  apply (drule_tac x="{x, y}" in spec)
  3.1181 +  apply (auto simp add: join_def)
  3.1182 +done
  3.1183 +
  3.1184 +lemma inf_pres_is_meet_pres:
  3.1185 +  assumes "weak_inf_pres X Y f"
  3.1186 +  shows "meet_pres X Y f"
  3.1187 +  using assms
  3.1188 +  apply (simp add: meet_pres_def weak_inf_pres_def, safe)
  3.1189 +  apply (rename_tac x y)
  3.1190 +  apply (drule_tac x="{x, y}" in spec)
  3.1191 +  apply (auto simp add: meet_def)
  3.1192 +done
  3.1193 +
  3.1194 +end
     4.1 --- a/src/HOL/Algebra/Congruence.thy	Fri Mar 03 23:21:24 2017 +0100
     4.2 +++ b/src/HOL/Algebra/Congruence.thy	Thu Mar 02 21:16:02 2017 +0100
     4.3 @@ -4,7 +4,9 @@
     4.4  *)
     4.5  
     4.6  theory Congruence
     4.7 -imports Main
     4.8 +imports 
     4.9 +  Main
    4.10 +  "~~/src/HOL/Library/FuncSet"
    4.11  begin
    4.12  
    4.13  section \<open>Objects\<close>
    4.14 @@ -14,6 +16,14 @@
    4.15  record 'a partial_object =
    4.16    carrier :: "'a set"
    4.17  
    4.18 +lemma funcset_carrier:
    4.19 +  "\<lbrakk> f \<in> carrier X \<rightarrow> carrier Y; x \<in> carrier X \<rbrakk> \<Longrightarrow> f x \<in> carrier Y"
    4.20 +  by (fact funcset_mem)
    4.21 +
    4.22 +lemma funcset_carrier':
    4.23 +  "\<lbrakk> f \<in> carrier A \<rightarrow> carrier A; x \<in> carrier A \<rbrakk> \<Longrightarrow> f x \<in> carrier A"
    4.24 +  by (fact funcset_mem)
    4.25 +
    4.26  
    4.27  subsection \<open>Structure with Carrier and Equivalence Relation \<open>eq\<close>\<close>
    4.28  
    4.29 @@ -413,4 +423,14 @@
    4.30  by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
    4.31  *)
    4.32  
    4.33 +lemma equivalence_subset:
    4.34 +  assumes "equivalence L" "A \<subseteq> carrier L"
    4.35 +  shows "equivalence (L\<lparr> carrier := A \<rparr>)"
    4.36 +proof -
    4.37 +  interpret L: equivalence L
    4.38 +    by (simp add: assms)
    4.39 +  show ?thesis
    4.40 +    by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD)
    4.41 +qed
    4.42 +  
    4.43  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Algebra/Galois_Connection.thy	Thu Mar 02 21:16:02 2017 +0100
     5.3 @@ -0,0 +1,422 @@
     5.4 +(*  Title:      HOL/Algebra/Galois_Connection.thy
     5.5 +    Author:     Alasdair Armstrong and Simon Foster
     5.6 +    Copyright:  Alasdair Armstrong and Simon Foster
     5.7 +*)
     5.8 +
     5.9 +theory Galois_Connection
    5.10 +  imports Complete_Lattice
    5.11 +begin
    5.12 +
    5.13 +section \<open>Galois connections\<close>
    5.14 +
    5.15 +subsection \<open>Definition and basic properties\<close>
    5.16 +
    5.17 +record ('a, 'b, 'c, 'd) galcon =
    5.18 +  orderA :: "('a, 'c) gorder_scheme" ("\<X>\<index>")
    5.19 +  orderB :: "('b, 'd) gorder_scheme" ("\<Y>\<index>")
    5.20 +  lower  :: "'a \<Rightarrow> 'b" ("\<pi>\<^sup>*\<index>")
    5.21 +  upper  :: "'b \<Rightarrow> 'a" ("\<pi>\<^sub>*\<index>")
    5.22 +
    5.23 +type_synonym ('a, 'b) galois = "('a, 'b, unit, unit) galcon"
    5.24 +
    5.25 +abbreviation "inv_galcon G \<equiv> \<lparr> orderA = inv_gorder \<Y>\<^bsub>G\<^esub>, orderB = inv_gorder \<X>\<^bsub>G\<^esub>, lower = upper G, upper = lower G \<rparr>"
    5.26 +
    5.27 +definition comp_galcon :: "('b, 'c) galois \<Rightarrow> ('a, 'b) galois \<Rightarrow> ('a, 'c) galois" (infixr "\<circ>\<^sub>g" 85)
    5.28 +  where "G \<circ>\<^sub>g F = \<lparr> orderA = orderA F, orderB = orderB G, lower = lower G \<circ> lower F, upper = upper F \<circ> upper G \<rparr>"
    5.29 +
    5.30 +definition id_galcon :: "'a gorder \<Rightarrow> ('a, 'a) galois" ("I\<^sub>g") where
    5.31 +"I\<^sub>g(A) = \<lparr> orderA = A, orderB = A, lower = id, upper = id \<rparr>"
    5.32 +
    5.33 +
    5.34 +subsection \<open>Well-typed connections\<close>
    5.35 +
    5.36 +locale connection =
    5.37 +  fixes G (structure)
    5.38 +  assumes is_order_A: "partial_order \<X>"
    5.39 +  and is_order_B: "partial_order \<Y>"
    5.40 +  and lower_closure: "\<pi>\<^sup>* \<in> carrier \<X> \<rightarrow> carrier \<Y>"
    5.41 +  and upper_closure: "\<pi>\<^sub>* \<in> carrier \<Y> \<rightarrow> carrier \<X>"
    5.42 +begin
    5.43 +
    5.44 +  lemma lower_closed: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* x \<in> carrier \<Y>"
    5.45 +    using lower_closure by auto
    5.46 +
    5.47 +  lemma upper_closed: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* y \<in> carrier \<X>"
    5.48 +    using upper_closure by auto
    5.49 +
    5.50 +end
    5.51 +
    5.52 +
    5.53 +subsection \<open>Galois connections\<close>
    5.54 +  
    5.55 +locale galois_connection = connection +
    5.56 +  assumes galois_property: "\<lbrakk>x \<in> carrier \<X>; y \<in> carrier \<Y>\<rbrakk> \<Longrightarrow> \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
    5.57 +begin
    5.58 +
    5.59 +  lemma is_weak_order_A: "weak_partial_order \<X>"
    5.60 +  proof -
    5.61 +    interpret po: partial_order \<X>
    5.62 +      by (metis is_order_A)
    5.63 +    show ?thesis ..
    5.64 +  qed
    5.65 +
    5.66 +  lemma is_weak_order_B: "weak_partial_order \<Y>"
    5.67 +  proof -
    5.68 +    interpret po: partial_order \<Y>
    5.69 +      by (metis is_order_B)
    5.70 +    show ?thesis ..
    5.71 +  qed
    5.72 +
    5.73 +  lemma right: "\<lbrakk>x \<in> carrier \<X>; y \<in> carrier \<Y>; \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
    5.74 +    by (metis galois_property)
    5.75 +
    5.76 +  lemma left: "\<lbrakk>x \<in> carrier \<X>; y \<in> carrier \<Y>; x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y\<rbrakk> \<Longrightarrow> \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
    5.77 +    by (metis galois_property)
    5.78 +
    5.79 +  lemma deflation: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
    5.80 +    by (metis Pi_iff is_weak_order_A left upper_closure weak_partial_order.le_refl)
    5.81 +
    5.82 +  lemma inflation: "x \<in> carrier \<X> \<Longrightarrow> x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* x)"
    5.83 +    by (metis (no_types, lifting) PiE galois_connection.right galois_connection_axioms is_weak_order_B lower_closure weak_partial_order.le_refl)
    5.84 +
    5.85 +  lemma lower_iso: "isotone \<X> \<Y> \<pi>\<^sup>*"
    5.86 +  proof (auto simp add:isotone_def)
    5.87 +    show "weak_partial_order \<X>"
    5.88 +      by (metis is_weak_order_A)
    5.89 +    show "weak_partial_order \<Y>"
    5.90 +      by (metis is_weak_order_B)
    5.91 +    fix x y
    5.92 +    assume a: "x \<in> carrier \<X>" "y \<in> carrier \<X>" "x \<sqsubseteq>\<^bsub>\<X>\<^esub> y"
    5.93 +    have b: "\<pi>\<^sup>* y \<in> carrier \<Y>"
    5.94 +      using a(2) lower_closure by blast
    5.95 +    then have "\<pi>\<^sub>* (\<pi>\<^sup>* y) \<in> carrier \<X>"
    5.96 +      using upper_closure by blast
    5.97 +    then have "x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* y)"
    5.98 +      by (meson a inflation is_weak_order_A weak_partial_order.le_trans)
    5.99 +    thus "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* y"
   5.100 +      by (meson b a(1) Pi_iff galois_property lower_closure upper_closure)
   5.101 +  qed
   5.102 +
   5.103 +  lemma upper_iso: "isotone \<Y> \<X> \<pi>\<^sub>*"
   5.104 +    apply (auto simp add:isotone_def)
   5.105 +    apply (metis is_weak_order_B)
   5.106 +    apply (metis is_weak_order_A)
   5.107 +    apply (metis (no_types, lifting) Pi_mem deflation is_weak_order_B lower_closure right upper_closure weak_partial_order.le_trans)
   5.108 +  done
   5.109 +
   5.110 +  lemma lower_comp: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* (\<pi>\<^sup>* x)) = \<pi>\<^sup>* x"
   5.111 +    by (meson deflation funcset_mem inflation is_order_B lower_closure lower_iso partial_order.le_antisym upper_closure use_iso2)
   5.112 +
   5.113 +  lemma lower_comp': "x \<in> carrier \<X> \<Longrightarrow> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>* \<circ> \<pi>\<^sup>*) x = \<pi>\<^sup>* x"
   5.114 +    by (simp add: lower_comp)
   5.115 +
   5.116 +  lemma upper_comp: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) = \<pi>\<^sub>* y"
   5.117 +  proof -
   5.118 +    assume a1: "y \<in> carrier \<Y>"
   5.119 +    hence f1: "\<pi>\<^sub>* y \<in> carrier \<X>" using upper_closure by blast 
   5.120 +    have f2: "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y" using a1 deflation by blast
   5.121 +    have f3: "\<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) \<in> carrier \<X>"
   5.122 +      using f1 lower_closure upper_closure by auto 
   5.123 +    have "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<in> carrier \<Y>" using f1 lower_closure by blast   
   5.124 +    thus "\<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) = \<pi>\<^sub>* y"
   5.125 +      by (meson a1 f1 f2 f3 inflation is_order_A partial_order.le_antisym upper_iso use_iso2) 
   5.126 +  qed
   5.127 +
   5.128 +  lemma upper_comp': "y \<in> carrier \<Y> \<Longrightarrow> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>* \<circ> \<pi>\<^sub>*) y = \<pi>\<^sub>* y"
   5.129 +    by (simp add: upper_comp)
   5.130 +
   5.131 +  lemma adjoint_idem1: "idempotent \<Y> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>*)"
   5.132 +    by (simp add: idempotent_def is_order_B partial_order.eq_is_equal upper_comp)
   5.133 +
   5.134 +  lemma adjoint_idem2: "idempotent \<X> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>*)"
   5.135 +    by (simp add: idempotent_def is_order_A partial_order.eq_is_equal lower_comp)
   5.136 +
   5.137 +  lemma fg_iso: "isotone \<Y> \<Y> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>*)"
   5.138 +    by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)
   5.139 +
   5.140 +  lemma gf_iso: "isotone \<X> \<X> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>*)"
   5.141 +    by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)
   5.142 +
   5.143 +  lemma semi_inverse1: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* x = \<pi>\<^sup>* (\<pi>\<^sub>* (\<pi>\<^sup>* x))"
   5.144 +    by (metis lower_comp)
   5.145 +
   5.146 +  lemma semi_inverse2: "x \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* x = \<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* x))"
   5.147 +    by (metis upper_comp)
   5.148 +
   5.149 +  theorem lower_by_complete_lattice:
   5.150 +    assumes "complete_lattice \<Y>" "x \<in> carrier \<X>"
   5.151 +    shows "\<pi>\<^sup>*(x) = \<Sqinter>\<^bsub>\<Y>\<^esub> { y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>*(y) }"
   5.152 +  proof -
   5.153 +    interpret Y: complete_lattice \<Y>
   5.154 +      by (simp add: assms)
   5.155 +
   5.156 +    show ?thesis
   5.157 +    proof (rule Y.le_antisym)
   5.158 +      show x: "\<pi>\<^sup>* x \<in> carrier \<Y>"
   5.159 +        using assms(2) lower_closure by blast
   5.160 +      show "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}"
   5.161 +      proof (rule Y.weak.inf_greatest)
   5.162 +        show "{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<subseteq> carrier \<Y>"
   5.163 +          by auto
   5.164 +        show "\<pi>\<^sup>* x \<in> carrier \<Y>" by (fact x)
   5.165 +        fix z
   5.166 +        assume "z \<in> {y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}" 
   5.167 +        thus "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> z"
   5.168 +          using assms(2) left by auto
   5.169 +      qed
   5.170 +      show "\<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* x"
   5.171 +      proof (rule Y.weak.inf_lower)
   5.172 +        show "{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<subseteq> carrier \<Y>"
   5.173 +          by auto
   5.174 +        show "\<pi>\<^sup>* x \<in> {y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}"
   5.175 +        proof (auto)
   5.176 +          show "\<pi>\<^sup>* x \<in> carrier \<Y>" by (fact x)
   5.177 +          show "x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* x)"
   5.178 +            using assms(2) inflation by blast
   5.179 +        qed
   5.180 +      qed
   5.181 +      show "\<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<in> carrier \<Y>"
   5.182 +       by (auto intro: Y.weak.inf_closed)
   5.183 +    qed
   5.184 +  qed
   5.185 +
   5.186 +  theorem upper_by_complete_lattice:
   5.187 +    assumes "complete_lattice \<X>" "y \<in> carrier \<Y>"
   5.188 +    shows "\<pi>\<^sub>*(y) = \<Squnion>\<^bsub>\<X>\<^esub> { x \<in> carrier \<X>. \<pi>\<^sup>*(x) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y }"
   5.189 +  proof -
   5.190 +    interpret X: complete_lattice \<X>
   5.191 +      by (simp add: assms)
   5.192 +    show ?thesis
   5.193 +    proof (rule X.le_antisym)
   5.194 +      show y: "\<pi>\<^sub>* y \<in> carrier \<X>"
   5.195 +        using assms(2) upper_closure by blast
   5.196 +      show "\<pi>\<^sub>* y \<sqsubseteq>\<^bsub>\<X>\<^esub> \<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}"
   5.197 +      proof (rule X.weak.sup_upper)
   5.198 +        show "{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<subseteq> carrier \<X>"
   5.199 +          by auto
   5.200 +        show "\<pi>\<^sub>* y \<in> {x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}"
   5.201 +        proof (auto)
   5.202 +          show "\<pi>\<^sub>* y \<in> carrier \<X>" by (fact y)
   5.203 +          show "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
   5.204 +            by (simp add: assms(2) deflation)
   5.205 +        qed
   5.206 +      qed
   5.207 +      show "\<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
   5.208 +      proof (rule X.weak.sup_least)
   5.209 +        show "{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<subseteq> carrier \<X>"
   5.210 +          by auto
   5.211 +        show "\<pi>\<^sub>* y \<in> carrier \<X>" by (fact y)
   5.212 +        fix z
   5.213 +        assume "z \<in> {x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}" 
   5.214 +        thus "z \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
   5.215 +          by (simp add: assms(2) right)
   5.216 +      qed
   5.217 +      show "\<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<in> carrier \<X>"
   5.218 +       by (auto intro: X.weak.sup_closed)
   5.219 +    qed
   5.220 +  qed
   5.221 +
   5.222 +end
   5.223 +
   5.224 +lemma dual_galois [simp]: " galois_connection \<lparr> orderA = inv_gorder B, orderB = inv_gorder A, lower = f, upper = g \<rparr> 
   5.225 +                          = galois_connection \<lparr> orderA = A, orderB = B, lower = g, upper = f \<rparr>"
   5.226 +  by (auto simp add: galois_connection_def galois_connection_axioms_def connection_def dual_order_iff)
   5.227 +
   5.228 +definition lower_adjoint :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   5.229 +  "lower_adjoint A B f \<equiv> \<exists>g. galois_connection \<lparr> orderA = A, orderB = B, lower = f, upper = g \<rparr>"
   5.230 +
   5.231 +definition upper_adjoint :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool" where
   5.232 +  "upper_adjoint A B g \<equiv> \<exists>f. galois_connection \<lparr> orderA = A, orderB = B, lower = f, upper = g \<rparr>"
   5.233 +
   5.234 +lemma lower_adjoint_dual [simp]: "lower_adjoint (inv_gorder A) (inv_gorder B) f = upper_adjoint B A f"
   5.235 +  by (simp add: lower_adjoint_def upper_adjoint_def)
   5.236 +
   5.237 +lemma upper_adjoint_dual [simp]: "upper_adjoint (inv_gorder A) (inv_gorder B) f = lower_adjoint B A f"
   5.238 +  by (simp add: lower_adjoint_def upper_adjoint_def)
   5.239 +
   5.240 +lemma lower_type: "lower_adjoint A B f \<Longrightarrow> f \<in> carrier A \<rightarrow> carrier B"
   5.241 +  by (auto simp add:lower_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)
   5.242 +
   5.243 +lemma upper_type: "upper_adjoint A B g \<Longrightarrow> g \<in> carrier B \<rightarrow> carrier A"
   5.244 +  by (auto simp add:upper_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)
   5.245 +
   5.246 +
   5.247 +subsection \<open>Composition of Galois connections\<close>
   5.248 +
   5.249 +lemma id_galois: "partial_order A \<Longrightarrow> galois_connection (I\<^sub>g(A))"
   5.250 +  by (simp add: id_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
   5.251 +
   5.252 +lemma comp_galcon_closed:
   5.253 +  assumes "galois_connection G" "galois_connection F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
   5.254 +  shows "galois_connection (G \<circ>\<^sub>g F)"
   5.255 +proof -
   5.256 +  interpret F: galois_connection F
   5.257 +    by (simp add: assms)
   5.258 +  interpret G: galois_connection G
   5.259 +    by (simp add: assms)
   5.260 +  
   5.261 +  have "partial_order \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.262 +    by (simp add: F.is_order_A comp_galcon_def)
   5.263 +  moreover have "partial_order \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.264 +    by (simp add: G.is_order_B comp_galcon_def)
   5.265 +  moreover have "\<pi>\<^sup>*\<^bsub>G\<^esub> \<circ> \<pi>\<^sup>*\<^bsub>F\<^esub> \<in> carrier \<X>\<^bsub>F\<^esub> \<rightarrow> carrier \<Y>\<^bsub>G\<^esub>"
   5.266 +    using F.lower_closure G.lower_closure assms(3) by auto
   5.267 +  moreover have "\<pi>\<^sub>*\<^bsub>F\<^esub> \<circ> \<pi>\<^sub>*\<^bsub>G\<^esub> \<in> carrier \<Y>\<^bsub>G\<^esub> \<rightarrow> carrier \<X>\<^bsub>F\<^esub>"
   5.268 +    using F.upper_closure G.upper_closure assms(3) by auto
   5.269 +  moreover 
   5.270 +  have "\<And> x y. \<lbrakk>x \<in> carrier \<X>\<^bsub>F\<^esub>; y \<in> carrier \<Y>\<^bsub>G\<^esub> \<rbrakk> \<Longrightarrow> 
   5.271 +               (\<pi>\<^sup>*\<^bsub>G\<^esub> (\<pi>\<^sup>*\<^bsub>F\<^esub> x) \<sqsubseteq>\<^bsub>\<Y>\<^bsub>G\<^esub>\<^esub> y) = (x \<sqsubseteq>\<^bsub>\<X>\<^bsub>F\<^esub>\<^esub> \<pi>\<^sub>*\<^bsub>F\<^esub> (\<pi>\<^sub>*\<^bsub>G\<^esub> y))"
   5.272 +    by (metis F.galois_property F.lower_closure G.galois_property G.upper_closure assms(3) Pi_iff)
   5.273 +  ultimately show ?thesis
   5.274 +    by (simp add: comp_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
   5.275 +qed
   5.276 +
   5.277 +lemma comp_galcon_right_unit [simp]: "F \<circ>\<^sub>g I\<^sub>g(\<X>\<^bsub>F\<^esub>) = F"
   5.278 +  by (simp add: comp_galcon_def id_galcon_def)
   5.279 +
   5.280 +lemma comp_galcon_left_unit [simp]: "I\<^sub>g(\<Y>\<^bsub>F\<^esub>) \<circ>\<^sub>g F = F"
   5.281 +  by (simp add: comp_galcon_def id_galcon_def)
   5.282 +
   5.283 +lemma galois_connectionI:
   5.284 +  assumes
   5.285 +    "partial_order A" "partial_order B"
   5.286 +    "L \<in> carrier A \<rightarrow> carrier B" "R \<in> carrier B \<rightarrow> carrier A"
   5.287 +    "isotone A B L" "isotone B A R" 
   5.288 +    "\<And> x y. \<lbrakk> x \<in> carrier A; y \<in> carrier B \<rbrakk> \<Longrightarrow> L x \<sqsubseteq>\<^bsub>B\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>A\<^esub> R y"
   5.289 +  shows "galois_connection \<lparr> orderA = A, orderB = B, lower = L, upper = R \<rparr>"
   5.290 +  using assms by (simp add: galois_connection_def connection_def galois_connection_axioms_def)
   5.291 +
   5.292 +lemma galois_connectionI':
   5.293 +  assumes
   5.294 +    "partial_order A" "partial_order B"
   5.295 +    "L \<in> carrier A \<rightarrow> carrier B" "R \<in> carrier B \<rightarrow> carrier A"
   5.296 +    "isotone A B L" "isotone B A R" 
   5.297 +    "\<And> X. X \<in> carrier(B) \<Longrightarrow> L(R(X)) \<sqsubseteq>\<^bsub>B\<^esub> X"
   5.298 +    "\<And> X. X \<in> carrier(A) \<Longrightarrow> X \<sqsubseteq>\<^bsub>A\<^esub> R(L(X))"
   5.299 +  shows "galois_connection \<lparr> orderA = A, orderB = B, lower = L, upper = R \<rparr>"
   5.300 +  using assms
   5.301 +  by (auto simp add: galois_connection_def connection_def galois_connection_axioms_def, (meson PiE isotone_def weak_partial_order.le_trans)+)
   5.302 +
   5.303 +
   5.304 +subsection \<open>Retracts\<close>
   5.305 +
   5.306 +locale retract = galois_connection +
   5.307 +  assumes retract_property: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) \<sqsubseteq>\<^bsub>\<X>\<^esub> x"
   5.308 +begin
   5.309 +  lemma retract_inverse: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) = x"
   5.310 +    by (meson funcset_mem inflation is_order_A lower_closure partial_order.le_antisym retract_axioms retract_axioms_def retract_def upper_closure)
   5.311 +
   5.312 +  lemma retract_injective: "inj_on \<pi>\<^sup>* (carrier \<X>)"
   5.313 +    by (metis inj_onI retract_inverse)
   5.314 +end  
   5.315 +
   5.316 +theorem comp_retract_closed:
   5.317 +  assumes "retract G" "retract F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
   5.318 +  shows "retract (G \<circ>\<^sub>g F)"
   5.319 +proof -
   5.320 +  interpret f: retract F
   5.321 +    by (simp add: assms)
   5.322 +  interpret g: retract G
   5.323 +    by (simp add: assms)
   5.324 +  interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
   5.325 +    by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed retract.axioms(1))
   5.326 +  show ?thesis
   5.327 +  proof
   5.328 +    fix x
   5.329 +    assume "x \<in> carrier \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.330 +    thus "le \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> x)) x"
   5.331 +      using assms(3) f.inflation f.lower_closed f.retract_inverse g.retract_inverse by (auto simp add: comp_galcon_def)
   5.332 +  qed
   5.333 +qed
   5.334 +
   5.335 +
   5.336 +subsection \<open>Coretracts\<close>
   5.337 +  
   5.338 +locale coretract = galois_connection +
   5.339 +  assumes coretract_property: "y \<in> carrier \<Y> \<Longrightarrow> y \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* (\<pi>\<^sub>* y)"
   5.340 +begin
   5.341 +  lemma coretract_inverse: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) = y"
   5.342 +    by (meson coretract_axioms coretract_axioms_def coretract_def deflation funcset_mem is_order_B lower_closure partial_order.le_antisym upper_closure)
   5.343 + 
   5.344 +  lemma retract_injective: "inj_on \<pi>\<^sub>* (carrier \<Y>)"
   5.345 +    by (metis coretract_inverse inj_onI)
   5.346 +end  
   5.347 +
   5.348 +theorem comp_coretract_closed:
   5.349 +  assumes "coretract G" "coretract F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
   5.350 +  shows "coretract (G \<circ>\<^sub>g F)"
   5.351 +proof -
   5.352 +  interpret f: coretract F
   5.353 +    by (simp add: assms)
   5.354 +  interpret g: coretract G
   5.355 +    by (simp add: assms)
   5.356 +  interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
   5.357 +    by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed coretract.axioms(1))
   5.358 +  show ?thesis
   5.359 +  proof
   5.360 +    fix y
   5.361 +    assume "y \<in> carrier \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.362 +    thus "le \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub> y (\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> y))"
   5.363 +      by (simp add: comp_galcon_def assms(3) f.coretract_inverse g.coretract_property g.upper_closed)
   5.364 +  qed
   5.365 +qed
   5.366 +
   5.367 +
   5.368 +subsection \<open>Galois Bijections\<close>
   5.369 +  
   5.370 +locale galois_bijection = connection +
   5.371 +  assumes lower_iso: "isotone \<X> \<Y> \<pi>\<^sup>*" 
   5.372 +  and upper_iso: "isotone \<Y> \<X> \<pi>\<^sub>*"
   5.373 +  and lower_inv_eq: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) = x"
   5.374 +  and upper_inv_eq: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) = y"
   5.375 +begin
   5.376 +
   5.377 +  lemma lower_bij: "bij_betw \<pi>\<^sup>* (carrier \<X>) (carrier \<Y>)"
   5.378 +    by (rule bij_betwI[where g="\<pi>\<^sub>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)  
   5.379 +
   5.380 +  lemma upper_bij: "bij_betw \<pi>\<^sub>* (carrier \<Y>) (carrier \<X>)"
   5.381 +    by (rule bij_betwI[where g="\<pi>\<^sup>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)  
   5.382 +
   5.383 +sublocale gal_bij_conn: galois_connection
   5.384 +  apply (unfold_locales, auto)
   5.385 +  using lower_closed lower_inv_eq upper_iso use_iso2 apply fastforce
   5.386 +  using lower_iso upper_closed upper_inv_eq use_iso2 apply fastforce
   5.387 +done
   5.388 +
   5.389 +sublocale gal_bij_ret: retract
   5.390 +  by (unfold_locales, simp add: gal_bij_conn.is_weak_order_A lower_inv_eq weak_partial_order.le_refl)
   5.391 +
   5.392 +sublocale gal_bij_coret: coretract
   5.393 +  by (unfold_locales, simp add: gal_bij_conn.is_weak_order_B upper_inv_eq weak_partial_order.le_refl)
   5.394 +
   5.395 +end
   5.396 +
   5.397 +theorem comp_galois_bijection_closed:
   5.398 +  assumes "galois_bijection G" "galois_bijection F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
   5.399 +  shows "galois_bijection (G \<circ>\<^sub>g F)"
   5.400 +proof -
   5.401 +  interpret f: galois_bijection F
   5.402 +    by (simp add: assms)
   5.403 +  interpret g: galois_bijection G
   5.404 +    by (simp add: assms)
   5.405 +  interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
   5.406 +    by (simp add: assms(3) comp_galcon_closed f.gal_bij_conn.galois_connection_axioms g.gal_bij_conn.galois_connection_axioms galois_connection.axioms(1))
   5.407 +  show ?thesis
   5.408 +  proof
   5.409 +    show "isotone \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.410 +      by (simp add: comp_galcon_def, metis comp_galcon_def galcon.select_convs(1) galcon.select_convs(2) galcon.select_convs(3) gf.lower_iso)
   5.411 +    show "isotone \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub> \<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.412 +      by (simp add: gf.upper_iso)
   5.413 +    fix x
   5.414 +    assume "x \<in> carrier \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.415 +    thus "\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> x) = x"
   5.416 +      using assms(3) f.lower_closed f.lower_inv_eq g.lower_inv_eq by (auto simp add: comp_galcon_def)
   5.417 +  next
   5.418 +    fix y
   5.419 +    assume "y \<in> carrier \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
   5.420 +    thus "\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> y) = y"
   5.421 +      by (simp add: comp_galcon_def assms(3) f.upper_inv_eq g.upper_closed g.upper_inv_eq)
   5.422 +  qed
   5.423 +qed
   5.424 +
   5.425 +end
     6.1 --- a/src/HOL/Algebra/Group.thy	Fri Mar 03 23:21:24 2017 +0100
     6.2 +++ b/src/HOL/Algebra/Group.thy	Thu Mar 02 21:16:02 2017 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  *)
     6.5  
     6.6  theory Group
     6.7 -imports Lattice "~~/src/HOL/Library/FuncSet"
     6.8 +imports Complete_Lattice "~~/src/HOL/Library/FuncSet"
     6.9  begin
    6.10  
    6.11  section \<open>Monoids and Groups\<close>
     7.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Mar 03 23:21:24 2017 +0100
     7.2 +++ b/src/HOL/Algebra/Lattice.thy	Thu Mar 02 21:16:02 2017 +0100
     7.3 @@ -3,406 +3,16 @@
     7.4      Copyright:  Clemens Ballarin
     7.5  
     7.6  Most congruence rules by Stephan Hohe.
     7.7 +With additional contributions from Alasdair Armstrong and Simon Foster.
     7.8  *)
     7.9  
    7.10  theory Lattice
    7.11 -imports Congruence
    7.12 -begin
    7.13 -
    7.14 -section \<open>Orders and Lattices\<close>
    7.15 -
    7.16 -subsection \<open>Partial Orders\<close>
    7.17 -
    7.18 -record 'a gorder = "'a eq_object" +
    7.19 -  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    7.20 -
    7.21 -locale weak_partial_order = equivalence L for L (structure) +
    7.22 -  assumes le_refl [intro, simp]:
    7.23 -      "x \<in> carrier L ==> x \<sqsubseteq> x"
    7.24 -    and weak_le_antisym [intro]:
    7.25 -      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
    7.26 -    and le_trans [trans]:
    7.27 -      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    7.28 -    and le_cong:
    7.29 -      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
    7.30 -      x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
    7.31 -
    7.32 -definition
    7.33 -  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    7.34 -  where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
    7.35 -
    7.36 -
    7.37 -subsubsection \<open>The order relation\<close>
    7.38 -
    7.39 -context weak_partial_order
    7.40 +imports Order
    7.41  begin
    7.42  
    7.43 -lemma le_cong_l [intro, trans]:
    7.44 -  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    7.45 -  by (auto intro: le_cong [THEN iffD2])
    7.46 -
    7.47 -lemma le_cong_r [intro, trans]:
    7.48 -  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    7.49 -  by (auto intro: le_cong [THEN iffD1])
    7.50 -
    7.51 -lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
    7.52 -  by (simp add: le_cong_l)
    7.53 -
    7.54 -end
    7.55 -
    7.56 -lemma weak_llessI:
    7.57 -  fixes R (structure)
    7.58 -  assumes "x \<sqsubseteq> y" and "~(x .= y)"
    7.59 -  shows "x \<sqsubset> y"
    7.60 -  using assms unfolding lless_def by simp
    7.61 -
    7.62 -lemma lless_imp_le:
    7.63 -  fixes R (structure)
    7.64 -  assumes "x \<sqsubset> y"
    7.65 -  shows "x \<sqsubseteq> y"
    7.66 -  using assms unfolding lless_def by simp
    7.67 -
    7.68 -lemma weak_lless_imp_not_eq:
    7.69 -  fixes R (structure)
    7.70 -  assumes "x \<sqsubset> y"
    7.71 -  shows "\<not> (x .= y)"
    7.72 -  using assms unfolding lless_def by simp
    7.73 -
    7.74 -lemma weak_llessE:
    7.75 -  fixes R (structure)
    7.76 -  assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
    7.77 -  shows "P"
    7.78 -  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
    7.79 -
    7.80 -lemma (in weak_partial_order) lless_cong_l [trans]:
    7.81 -  assumes xx': "x .= x'"
    7.82 -    and xy: "x' \<sqsubset> y"
    7.83 -    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
    7.84 -  shows "x \<sqsubset> y"
    7.85 -  using assms unfolding lless_def by (auto intro: trans sym)
    7.86 -
    7.87 -lemma (in weak_partial_order) lless_cong_r [trans]:
    7.88 -  assumes xy: "x \<sqsubset> y"
    7.89 -    and  yy': "y .= y'"
    7.90 -    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
    7.91 -  shows "x \<sqsubset> y'"
    7.92 -  using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
    7.93 -
    7.94 -
    7.95 -lemma (in weak_partial_order) lless_antisym:
    7.96 -  assumes "a \<in> carrier L" "b \<in> carrier L"
    7.97 -    and "a \<sqsubset> b" "b \<sqsubset> a"
    7.98 -  shows "P"
    7.99 -  using assms
   7.100 -  by (elim weak_llessE) auto
   7.101 -
   7.102 -lemma (in weak_partial_order) lless_trans [trans]:
   7.103 -  assumes "a \<sqsubset> b" "b \<sqsubset> c"
   7.104 -    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
   7.105 -  shows "a \<sqsubset> c"
   7.106 -  using assms unfolding lless_def by (blast dest: le_trans intro: sym)
   7.107 -
   7.108 -
   7.109 -subsubsection \<open>Upper and lower bounds of a set\<close>
   7.110 -
   7.111 -definition
   7.112 -  Upper :: "[_, 'a set] => 'a set"
   7.113 -  where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
   7.114 -
   7.115 -definition
   7.116 -  Lower :: "[_, 'a set] => 'a set"
   7.117 -  where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
   7.118 -
   7.119 -lemma Upper_closed [intro!, simp]:
   7.120 -  "Upper L A \<subseteq> carrier L"
   7.121 -  by (unfold Upper_def) clarify
   7.122 -
   7.123 -lemma Upper_memD [dest]:
   7.124 -  fixes L (structure)
   7.125 -  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
   7.126 -  by (unfold Upper_def) blast
   7.127 -
   7.128 -lemma (in weak_partial_order) Upper_elemD [dest]:
   7.129 -  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   7.130 -  unfolding Upper_def elem_def
   7.131 -  by (blast dest: sym)
   7.132 -
   7.133 -lemma Upper_memI:
   7.134 -  fixes L (structure)
   7.135 -  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   7.136 -  by (unfold Upper_def) blast
   7.137 -
   7.138 -lemma (in weak_partial_order) Upper_elemI:
   7.139 -  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
   7.140 -  unfolding Upper_def by blast
   7.141 -
   7.142 -lemma Upper_antimono:
   7.143 -  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   7.144 -  by (unfold Upper_def) blast
   7.145 -
   7.146 -lemma (in weak_partial_order) Upper_is_closed [simp]:
   7.147 -  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
   7.148 -  by (rule is_closedI) (blast intro: Upper_memI)+
   7.149 -
   7.150 -lemma (in weak_partial_order) Upper_mem_cong:
   7.151 -  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   7.152 -    and aa': "a .= a'"
   7.153 -    and aelem: "a \<in> Upper L A"
   7.154 -  shows "a' \<in> Upper L A"
   7.155 -proof (rule Upper_memI[OF _ a'carr])
   7.156 -  fix y
   7.157 -  assume yA: "y \<in> A"
   7.158 -  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
   7.159 -  also note aa'
   7.160 -  finally
   7.161 -      show "y \<sqsubseteq> a'"
   7.162 -      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
   7.163 -qed
   7.164 -
   7.165 -lemma (in weak_partial_order) Upper_cong:
   7.166 -  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   7.167 -    and AA': "A {.=} A'"
   7.168 -  shows "Upper L A = Upper L A'"
   7.169 -unfolding Upper_def
   7.170 -apply rule
   7.171 - apply (rule, clarsimp) defer 1
   7.172 - apply (rule, clarsimp) defer 1
   7.173 -proof -
   7.174 -  fix x a'
   7.175 -  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   7.176 -    and a'A': "a' \<in> A'"
   7.177 -  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
   7.178 -
   7.179 -  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   7.180 -  from this obtain a
   7.181 -      where aA: "a \<in> A"
   7.182 -      and a'a: "a' .= a"
   7.183 -      by auto
   7.184 -  note [simp] = subsetD[OF Acarr aA] carr
   7.185 -
   7.186 -  note a'a
   7.187 -  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
   7.188 -  finally show "a' \<sqsubseteq> x" by simp
   7.189 -next
   7.190 -  fix x a
   7.191 -  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   7.192 -    and aA: "a \<in> A"
   7.193 -  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
   7.194 -
   7.195 -  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   7.196 -  from this obtain a'
   7.197 -      where a'A': "a' \<in> A'"
   7.198 -      and aa': "a .= a'"
   7.199 -      by auto
   7.200 -  note [simp] = subsetD[OF A'carr a'A'] carr
   7.201 -
   7.202 -  note aa'
   7.203 -  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
   7.204 -  finally show "a \<sqsubseteq> x" by simp
   7.205 -qed
   7.206 -
   7.207 -lemma Lower_closed [intro!, simp]:
   7.208 -  "Lower L A \<subseteq> carrier L"
   7.209 -  by (unfold Lower_def) clarify
   7.210 -
   7.211 -lemma Lower_memD [dest]:
   7.212 -  fixes L (structure)
   7.213 -  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
   7.214 -  by (unfold Lower_def) blast
   7.215 -
   7.216 -lemma Lower_memI:
   7.217 -  fixes L (structure)
   7.218 -  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   7.219 -  by (unfold Lower_def) blast
   7.220 -
   7.221 -lemma Lower_antimono:
   7.222 -  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   7.223 -  by (unfold Lower_def) blast
   7.224 -
   7.225 -lemma (in weak_partial_order) Lower_is_closed [simp]:
   7.226 -  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
   7.227 -  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
   7.228 -
   7.229 -lemma (in weak_partial_order) Lower_mem_cong:
   7.230 -  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   7.231 -    and aa': "a .= a'"
   7.232 -    and aelem: "a \<in> Lower L A"
   7.233 -  shows "a' \<in> Lower L A"
   7.234 -using assms Lower_closed[of L A]
   7.235 -by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
   7.236 -
   7.237 -lemma (in weak_partial_order) Lower_cong:
   7.238 -  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   7.239 -    and AA': "A {.=} A'"
   7.240 -  shows "Lower L A = Lower L A'"
   7.241 -unfolding Lower_def
   7.242 -apply rule
   7.243 - apply clarsimp defer 1
   7.244 - apply clarsimp defer 1
   7.245 -proof -
   7.246 -  fix x a'
   7.247 -  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   7.248 -    and a'A': "a' \<in> A'"
   7.249 -  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
   7.250 -  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
   7.251 -
   7.252 -  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   7.253 -  from this obtain a
   7.254 -      where aA: "a \<in> A"
   7.255 -      and a'a: "a' .= a"
   7.256 -      by auto
   7.257 -
   7.258 -  from aA and subsetD[OF Acarr aA]
   7.259 -      have "x \<sqsubseteq> a" by (rule aLxCond)
   7.260 -  also note a'a[symmetric]
   7.261 -  finally
   7.262 -      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
   7.263 -next
   7.264 -  fix x a
   7.265 -  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   7.266 -    and aA: "a \<in> A"
   7.267 -  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
   7.268 -  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
   7.269 -
   7.270 -  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   7.271 -  from this obtain a'
   7.272 -      where a'A': "a' \<in> A'"
   7.273 -      and aa': "a .= a'"
   7.274 -      by auto
   7.275 -  from a'A' and subsetD[OF A'carr a'A']
   7.276 -      have "x \<sqsubseteq> a'" by (rule a'LxCond)
   7.277 -  also note aa'[symmetric]
   7.278 -  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
   7.279 -qed
   7.280 -
   7.281 -
   7.282 -subsubsection \<open>Least and greatest, as predicate\<close>
   7.283 -
   7.284 -definition
   7.285 -  least :: "[_, 'a, 'a set] => bool"
   7.286 -  where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
   7.287 -
   7.288 -definition
   7.289 -  greatest :: "[_, 'a, 'a set] => bool"
   7.290 -  where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
   7.291 -
   7.292 -text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
   7.293 -  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
   7.294 -
   7.295 -lemma least_closed [intro, simp]:
   7.296 -  "least L l A ==> l \<in> carrier L"
   7.297 -  by (unfold least_def) fast
   7.298 -
   7.299 -lemma least_mem:
   7.300 -  "least L l A ==> l \<in> A"
   7.301 -  by (unfold least_def) fast
   7.302 -
   7.303 -lemma (in weak_partial_order) weak_least_unique:
   7.304 -  "[| least L x A; least L y A |] ==> x .= y"
   7.305 -  by (unfold least_def) blast
   7.306 -
   7.307 -lemma least_le:
   7.308 -  fixes L (structure)
   7.309 -  shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   7.310 -  by (unfold least_def) fast
   7.311 -
   7.312 -lemma (in weak_partial_order) least_cong:
   7.313 -  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
   7.314 -  by (unfold least_def) (auto dest: sym)
   7.315 -
   7.316 -text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for 
   7.317 -  @{term "A {.=} A'"}\<close>
   7.318 -
   7.319 -lemma (in weak_partial_order) least_Upper_cong_l:
   7.320 -  assumes "x .= x'"
   7.321 -    and "x \<in> carrier L" "x' \<in> carrier L"
   7.322 -    and "A \<subseteq> carrier L"
   7.323 -  shows "least L x (Upper L A) = least L x' (Upper L A)"
   7.324 -  apply (rule least_cong) using assms by auto
   7.325 -
   7.326 -lemma (in weak_partial_order) least_Upper_cong_r:
   7.327 -  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
   7.328 -    and AA': "A {.=} A'"
   7.329 -  shows "least L x (Upper L A) = least L x (Upper L A')"
   7.330 -apply (subgoal_tac "Upper L A = Upper L A'", simp)
   7.331 -by (rule Upper_cong) fact+
   7.332 -
   7.333 -lemma least_UpperI:
   7.334 -  fixes L (structure)
   7.335 -  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   7.336 -    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   7.337 -    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   7.338 -  shows "least L s (Upper L A)"
   7.339 -proof -
   7.340 -  have "Upper L A \<subseteq> carrier L" by simp
   7.341 -  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   7.342 -  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   7.343 -  ultimately show ?thesis by (simp add: least_def)
   7.344 -qed
   7.345 -
   7.346 -lemma least_Upper_above:
   7.347 -  fixes L (structure)
   7.348 -  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   7.349 -  by (unfold least_def) blast
   7.350 -
   7.351 -lemma greatest_closed [intro, simp]:
   7.352 -  "greatest L l A ==> l \<in> carrier L"
   7.353 -  by (unfold greatest_def) fast
   7.354 -
   7.355 -lemma greatest_mem:
   7.356 -  "greatest L l A ==> l \<in> A"
   7.357 -  by (unfold greatest_def) fast
   7.358 -
   7.359 -lemma (in weak_partial_order) weak_greatest_unique:
   7.360 -  "[| greatest L x A; greatest L y A |] ==> x .= y"
   7.361 -  by (unfold greatest_def) blast
   7.362 -
   7.363 -lemma greatest_le:
   7.364 -  fixes L (structure)
   7.365 -  shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   7.366 -  by (unfold greatest_def) fast
   7.367 -
   7.368 -lemma (in weak_partial_order) greatest_cong:
   7.369 -  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
   7.370 -  greatest L x A = greatest L x' A"
   7.371 -  by (unfold greatest_def) (auto dest: sym)
   7.372 -
   7.373 -text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for 
   7.374 -  @{term "A {.=} A'"}\<close>
   7.375 -
   7.376 -lemma (in weak_partial_order) greatest_Lower_cong_l:
   7.377 -  assumes "x .= x'"
   7.378 -    and "x \<in> carrier L" "x' \<in> carrier L"
   7.379 -    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
   7.380 -  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
   7.381 -  apply (rule greatest_cong) using assms by auto
   7.382 -
   7.383 -lemma (in weak_partial_order) greatest_Lower_cong_r:
   7.384 -  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
   7.385 -    and AA': "A {.=} A'"
   7.386 -  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
   7.387 -apply (subgoal_tac "Lower L A = Lower L A'", simp)
   7.388 -by (rule Lower_cong) fact+
   7.389 -
   7.390 -lemma greatest_LowerI:
   7.391 -  fixes L (structure)
   7.392 -  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   7.393 -    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   7.394 -    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   7.395 -  shows "greatest L i (Lower L A)"
   7.396 -proof -
   7.397 -  have "Lower L A \<subseteq> carrier L" by simp
   7.398 -  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   7.399 -  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   7.400 -  ultimately show ?thesis by (simp add: greatest_def)
   7.401 -qed
   7.402 -
   7.403 -lemma greatest_Lower_below:
   7.404 -  fixes L (structure)
   7.405 -  shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   7.406 -  by (unfold greatest_def) blast
   7.407 -
   7.408 -text \<open>Supremum and infimum\<close>
   7.409 +section \<open>Lattices\<close>
   7.410 +  
   7.411 +subsection \<open>Supremum and infimum\<close>
   7.412  
   7.413  definition
   7.414    sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   7.415 @@ -412,6 +22,26 @@
   7.416    inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   7.417    where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
   7.418  
   7.419 +definition supr :: 
   7.420 +  "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
   7.421 +  where "supr L A f = \<Squnion>\<^bsub>L\<^esub>(f ` A)"
   7.422 +
   7.423 +definition infi :: 
   7.424 +  "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
   7.425 +  where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
   7.426 +
   7.427 +syntax
   7.428 +  "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _./ _)" [0, 10] 10)
   7.429 +  "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3IINF\<index> _:_./ _)" [0, 0, 10] 10)
   7.430 +  "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
   7.431 +  "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
   7.432 +
   7.433 +translations
   7.434 +  "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
   7.435 +  "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
   7.436 +  "SSUP\<^bsub>L\<^esub> x. B"     == "CONST supr L CONST UNIV (%x. B)"
   7.437 +  "SSUP\<^bsub>L\<^esub> x:A. B"   == "CONST supr L A (%x. B)"
   7.438 +
   7.439  definition
   7.440    join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   7.441    where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
   7.442 @@ -420,6 +50,49 @@
   7.443    meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   7.444    where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
   7.445  
   7.446 +definition
   7.447 +  LFP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<mu>\<index>") where
   7.448 +  "LFP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
   7.449 +
   7.450 +definition
   7.451 +  GFP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<nu>\<index>") where
   7.452 +  "GFP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
   7.453 +
   7.454 +
   7.455 +subsection \<open>Dual operators\<close>
   7.456 +
   7.457 +lemma sup_dual [simp]: 
   7.458 +  "\<Squnion>\<^bsub>inv_gorder L\<^esub>A = \<Sqinter>\<^bsub>L\<^esub>A"
   7.459 +  by (simp add: sup_def inf_def)
   7.460 +
   7.461 +lemma inf_dual [simp]: 
   7.462 +  "\<Sqinter>\<^bsub>inv_gorder L\<^esub>A = \<Squnion>\<^bsub>L\<^esub>A"
   7.463 +  by (simp add: sup_def inf_def)
   7.464 +
   7.465 +lemma join_dual [simp]:
   7.466 +  "p \<squnion>\<^bsub>inv_gorder L\<^esub> q = p \<sqinter>\<^bsub>L\<^esub> q"
   7.467 +  by (simp add:join_def meet_def)
   7.468 +
   7.469 +lemma meet_dual [simp]:
   7.470 +  "p \<sqinter>\<^bsub>inv_gorder L\<^esub> q = p \<squnion>\<^bsub>L\<^esub> q"
   7.471 +  by (simp add:join_def meet_def)
   7.472 +
   7.473 +lemma top_dual [simp]:
   7.474 +  "\<top>\<^bsub>inv_gorder L\<^esub> = \<bottom>\<^bsub>L\<^esub>"
   7.475 +  by (simp add: top_def bottom_def)
   7.476 +
   7.477 +lemma bottom_dual [simp]:
   7.478 +  "\<bottom>\<^bsub>inv_gorder L\<^esub> = \<top>\<^bsub>L\<^esub>"
   7.479 +  by (simp add: top_def bottom_def)
   7.480 +
   7.481 +lemma LFP_dual [simp]:
   7.482 +  "LFP (inv_gorder L) f = GFP L f"
   7.483 +  by (simp add:LFP_def GFP_def)
   7.484 +
   7.485 +lemma GFP_dual [simp]:
   7.486 +  "GFP (inv_gorder L) f = LFP L f"
   7.487 +  by (simp add:LFP_def GFP_def)
   7.488 +
   7.489  
   7.490  subsection \<open>Lattices\<close>
   7.491  
   7.492 @@ -433,6 +106,18 @@
   7.493  
   7.494  locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
   7.495  
   7.496 +lemma (in weak_lattice) dual_weak_lattice:
   7.497 +  "weak_lattice (inv_gorder L)"
   7.498 +proof -
   7.499 +  interpret dual: weak_partial_order "inv_gorder L"
   7.500 +    by (metis dual_weak_order)
   7.501 +
   7.502 +  show ?thesis
   7.503 +    apply (unfold_locales)
   7.504 +    apply (simp_all add: inf_of_two_exists sup_of_two_exists)
   7.505 +  done
   7.506 +qed
   7.507 +
   7.508  
   7.509  subsubsection \<open>Supremum\<close>
   7.510  
   7.511 @@ -589,7 +274,7 @@
   7.512  lemma (in weak_upper_semilattice) finite_sup_insertI:
   7.513    assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   7.514      and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   7.515 -  shows "P (\<Squnion>(insert x A))"
   7.516 +  shows "P (\<Squnion> (insert x A))"
   7.517  proof (cases "A = {}")
   7.518    case True with P and xA show ?thesis
   7.519      by (simp add: finite_sup_least)
   7.520 @@ -634,6 +319,11 @@
   7.521    with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   7.522  qed
   7.523  
   7.524 +lemma (in weak_lattice) weak_le_iff_meet:
   7.525 +  assumes "x \<in> carrier L" "y \<in> carrier L"
   7.526 +  shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) .= y"
   7.527 +  by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym)
   7.528 +  
   7.529  lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
   7.530    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   7.531    shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
   7.532 @@ -828,7 +518,7 @@
   7.533  lemma (in weak_lower_semilattice) finite_inf_insertI:
   7.534    assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   7.535      and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   7.536 -  shows "P (\<Sqinter>(insert x A))"
   7.537 +  shows "P (\<Sqinter> (insert x A))"
   7.538  proof (cases "A = {}")
   7.539    case True with P and xA show ?thesis
   7.540      by (simp add: finite_inf_greatest)
   7.541 @@ -875,6 +565,11 @@
   7.542    with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
   7.543  qed
   7.544  
   7.545 +lemma (in weak_lattice) weak_le_iff_join:
   7.546 +  assumes "x \<in> carrier L" "y \<in> carrier L"
   7.547 +  shows "x \<sqsubseteq> y \<longleftrightarrow> x .= (x \<sqinter> y)"
   7.548 +  by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl)
   7.549 +  
   7.550  lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
   7.551    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   7.552    shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
   7.553 @@ -904,28 +599,15 @@
   7.554  proof -
   7.555    (* FIXME: improved simp, see weak_join_assoc above *)
   7.556    have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
   7.557 -  also from L have "... .= \<Sqinter>{z, x, y}" by (simp add: weak_meet_assoc_lemma)
   7.558 -  also from L have "... = \<Sqinter>{x, y, z}" by (simp add: insert_commute)
   7.559 +  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
   7.560 +  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
   7.561    also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
   7.562    finally show ?thesis by (simp add: L)
   7.563  qed
   7.564  
   7.565 -
   7.566 -subsection \<open>Total Orders\<close>
   7.567 -
   7.568 -locale weak_total_order = weak_partial_order +
   7.569 -  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   7.570 -
   7.571 -text \<open>Introduction rule: the usual definition of total order\<close>
   7.572 -
   7.573 -lemma (in weak_partial_order) weak_total_orderI:
   7.574 -  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   7.575 -  shows "weak_total_order L"
   7.576 -  by standard (rule total)
   7.577 -
   7.578  text \<open>Total orders are lattices.\<close>
   7.579  
   7.580 -sublocale weak_total_order < weak?: weak_lattice
   7.581 +sublocale weak_total_order \<subseteq> weak?: weak_lattice
   7.582  proof
   7.583    fix x y
   7.584    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   7.585 @@ -969,337 +651,136 @@
   7.586  qed
   7.587  
   7.588  
   7.589 -subsection \<open>Complete Lattices\<close>
   7.590 -
   7.591 -locale weak_complete_lattice = weak_lattice +
   7.592 -  assumes sup_exists:
   7.593 -    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   7.594 -    and inf_exists:
   7.595 -    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   7.596 -
   7.597 -text \<open>Introduction rule: the usual definition of complete lattice\<close>
   7.598 -
   7.599 -lemma (in weak_partial_order) weak_complete_latticeI:
   7.600 -  assumes sup_exists:
   7.601 -    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   7.602 -    and inf_exists:
   7.603 -    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   7.604 -  shows "weak_complete_lattice L"
   7.605 -  by standard (auto intro: sup_exists inf_exists)
   7.606 -
   7.607 -definition
   7.608 -  top :: "_ => 'a" ("\<top>\<index>")
   7.609 -  where "\<top>\<^bsub>L\<^esub> = sup L (carrier L)"
   7.610 -
   7.611 -definition
   7.612 -  bottom :: "_ => 'a" ("\<bottom>\<index>")
   7.613 -  where "\<bottom>\<^bsub>L\<^esub> = inf L (carrier L)"
   7.614 -
   7.615 -
   7.616 -lemma (in weak_complete_lattice) supI:
   7.617 -  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   7.618 -  ==> P (\<Squnion>A)"
   7.619 -proof (unfold sup_def)
   7.620 -  assume L: "A \<subseteq> carrier L"
   7.621 -    and P: "!!l. least L l (Upper L A) ==> P l"
   7.622 -  with sup_exists obtain s where "least L s (Upper L A)" by blast
   7.623 -  with L show "P (SOME l. least L l (Upper L A))"
   7.624 -  by (fast intro: someI2 weak_least_unique P)
   7.625 -qed
   7.626 -
   7.627 -lemma (in weak_complete_lattice) sup_closed [simp]:
   7.628 -  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
   7.629 -  by (rule supI) simp_all
   7.630 -
   7.631 -lemma (in weak_complete_lattice) top_closed [simp, intro]:
   7.632 -  "\<top> \<in> carrier L"
   7.633 -  by (unfold top_def) simp
   7.634 -
   7.635 -lemma (in weak_complete_lattice) infI:
   7.636 -  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
   7.637 -  ==> P (\<Sqinter>A)"
   7.638 -proof (unfold inf_def)
   7.639 -  assume L: "A \<subseteq> carrier L"
   7.640 -    and P: "!!l. greatest L l (Lower L A) ==> P l"
   7.641 -  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
   7.642 -  with L show "P (SOME l. greatest L l (Lower L A))"
   7.643 -  by (fast intro: someI2 weak_greatest_unique P)
   7.644 -qed
   7.645 -
   7.646 -lemma (in weak_complete_lattice) inf_closed [simp]:
   7.647 -  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
   7.648 -  by (rule infI) simp_all
   7.649 +subsection \<open>Weak Bounded Lattices\<close>
   7.650  
   7.651 -lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
   7.652 -  "\<bottom> \<in> carrier L"
   7.653 -  by (unfold bottom_def) simp
   7.654 -
   7.655 -text \<open>Jacobson: Theorem 8.1\<close>
   7.656 -
   7.657 -lemma Lower_empty [simp]:
   7.658 -  "Lower L {} = carrier L"
   7.659 -  by (unfold Lower_def) simp
   7.660 -
   7.661 -lemma Upper_empty [simp]:
   7.662 -  "Upper L {} = carrier L"
   7.663 -  by (unfold Upper_def) simp
   7.664 -
   7.665 -theorem (in weak_partial_order) weak_complete_lattice_criterion1:
   7.666 -  assumes top_exists: "EX g. greatest L g (carrier L)"
   7.667 -    and inf_exists:
   7.668 -      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
   7.669 -  shows "weak_complete_lattice L"
   7.670 -proof (rule weak_complete_latticeI)
   7.671 -  from top_exists obtain top where top: "greatest L top (carrier L)" ..
   7.672 -  fix A
   7.673 -  assume L: "A \<subseteq> carrier L"
   7.674 -  let ?B = "Upper L A"
   7.675 -  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
   7.676 -  then have B_non_empty: "?B ~= {}" by fast
   7.677 -  have B_L: "?B \<subseteq> carrier L" by simp
   7.678 -  from inf_exists [OF B_L B_non_empty]
   7.679 -  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
   7.680 -  have "least L b (Upper L A)"
   7.681 -apply (rule least_UpperI)
   7.682 -   apply (rule greatest_le [where A = "Lower L ?B"])
   7.683 -    apply (rule b_inf_B)
   7.684 -   apply (rule Lower_memI)
   7.685 -    apply (erule Upper_memD [THEN conjunct1])
   7.686 -     apply assumption
   7.687 -    apply (rule L)
   7.688 -   apply (fast intro: L [THEN subsetD])
   7.689 -  apply (erule greatest_Lower_below [OF b_inf_B])
   7.690 -  apply simp
   7.691 - apply (rule L)
   7.692 -apply (rule greatest_closed [OF b_inf_B])
   7.693 -done
   7.694 -  then show "EX s. least L s (Upper L A)" ..
   7.695 -next
   7.696 -  fix A
   7.697 -  assume L: "A \<subseteq> carrier L"
   7.698 -  show "EX i. greatest L i (Lower L A)"
   7.699 -  proof (cases "A = {}")
   7.700 -    case True then show ?thesis
   7.701 -      by (simp add: top_exists)
   7.702 -  next
   7.703 -    case False with L show ?thesis
   7.704 -      by (rule inf_exists)
   7.705 -  qed
   7.706 -qed
   7.707 -
   7.708 -(* TODO: prove dual version *)
   7.709 -
   7.710 -
   7.711 -subsection \<open>Orders and Lattices where \<open>eq\<close> is the Equality\<close>
   7.712 -
   7.713 -locale partial_order = weak_partial_order +
   7.714 -  assumes eq_is_equal: "op .= = op ="
   7.715 +locale weak_bounded_lattice = 
   7.716 +  weak_lattice + 
   7.717 +  weak_partial_order_bottom + 
   7.718 +  weak_partial_order_top
   7.719  begin
   7.720  
   7.721 -declare weak_le_antisym [rule del]
   7.722 +lemma bottom_meet: "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqinter> x .= \<bottom>"
   7.723 +  by (metis bottom_least least_def meet_closed meet_left weak_le_antisym)
   7.724  
   7.725 -lemma le_antisym [intro]:
   7.726 -  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
   7.727 -  using weak_le_antisym unfolding eq_is_equal .
   7.728 +lemma bottom_join: "x \<in> carrier L \<Longrightarrow> \<bottom> \<squnion> x .= x"
   7.729 +  by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym)
   7.730  
   7.731 -lemma lless_eq:
   7.732 -  "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
   7.733 -  unfolding lless_def by (simp add: eq_is_equal)
   7.734 +lemma bottom_weak_eq:
   7.735 +  "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b .= \<bottom>"
   7.736 +  by (metis bottom_closed bottom_lower weak_le_antisym)
   7.737  
   7.738 -lemma lless_asym:
   7.739 -  assumes "a \<in> carrier L" "b \<in> carrier L"
   7.740 -    and "a \<sqsubset> b" "b \<sqsubset> a"
   7.741 -  shows "P"
   7.742 -  using assms unfolding lless_eq by auto
   7.743 +lemma top_join: "x \<in> carrier L \<Longrightarrow> \<top> \<squnion> x .= \<top>"
   7.744 +  by (metis join_closed join_left top_closed top_higher weak_le_antisym)
   7.745 +
   7.746 +lemma top_meet: "x \<in> carrier L \<Longrightarrow> \<top> \<sqinter> x .= x"
   7.747 +  by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym)
   7.748 +
   7.749 +lemma top_weak_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t .= \<top>"
   7.750 +  by (metis top_closed top_higher weak_le_antisym)
   7.751  
   7.752  end
   7.753  
   7.754 -
   7.755 -text \<open>Least and greatest, as predicate\<close>
   7.756 -
   7.757 -lemma (in partial_order) least_unique:
   7.758 -  "[| least L x A; least L y A |] ==> x = y"
   7.759 -  using weak_least_unique unfolding eq_is_equal .
   7.760 -
   7.761 -lemma (in partial_order) greatest_unique:
   7.762 -  "[| greatest L x A; greatest L y A |] ==> x = y"
   7.763 -  using weak_greatest_unique unfolding eq_is_equal .
   7.764 +sublocale weak_bounded_lattice \<subseteq> weak_partial_order ..
   7.765  
   7.766  
   7.767 -text \<open>Lattices\<close>
   7.768 +subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close>
   7.769  
   7.770  locale upper_semilattice = partial_order +
   7.771    assumes sup_of_two_exists:
   7.772      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   7.773  
   7.774 -sublocale upper_semilattice < weak?: weak_upper_semilattice
   7.775 -  by standard (rule sup_of_two_exists)
   7.776 +sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice
   7.777 +  by unfold_locales (rule sup_of_two_exists)
   7.778  
   7.779  locale lower_semilattice = partial_order +
   7.780    assumes inf_of_two_exists:
   7.781      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   7.782  
   7.783 -sublocale lower_semilattice < weak?: weak_lower_semilattice
   7.784 -  by standard (rule inf_of_two_exists)
   7.785 +sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice
   7.786 +  by unfold_locales (rule inf_of_two_exists)
   7.787  
   7.788  locale lattice = upper_semilattice + lower_semilattice
   7.789  
   7.790 -
   7.791 -text \<open>Supremum\<close>
   7.792 -
   7.793 -declare (in partial_order) weak_sup_of_singleton [simp del]
   7.794 +sublocale lattice \<subseteq> weak_lattice ..
   7.795  
   7.796 -lemma (in partial_order) sup_of_singleton [simp]:
   7.797 -  "x \<in> carrier L ==> \<Squnion>{x} = x"
   7.798 -  using weak_sup_of_singleton unfolding eq_is_equal .
   7.799 -
   7.800 -lemma (in upper_semilattice) join_assoc_lemma:
   7.801 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   7.802 -  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
   7.803 -  using weak_join_assoc_lemma L unfolding eq_is_equal .
   7.804 +lemma (in lattice) dual_lattice:
   7.805 +  "lattice (inv_gorder L)"
   7.806 +proof -
   7.807 +  interpret dual: weak_lattice "inv_gorder L"
   7.808 +    by (metis dual_weak_lattice)
   7.809  
   7.810 -lemma (in upper_semilattice) join_assoc:
   7.811 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   7.812 -  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   7.813 -  using weak_join_assoc L unfolding eq_is_equal .
   7.814 -
   7.815 -
   7.816 -text \<open>Infimum\<close>
   7.817 +  show ?thesis
   7.818 +    apply (unfold_locales)
   7.819 +    apply (simp_all add: inf_of_two_exists sup_of_two_exists)
   7.820 +    apply (simp add:eq_is_equal)
   7.821 +  done
   7.822 +qed
   7.823 +  
   7.824 +lemma (in lattice) le_iff_join:
   7.825 +  assumes "x \<in> carrier L" "y \<in> carrier L"
   7.826 +  shows "x \<sqsubseteq> y \<longleftrightarrow> x = (x \<sqinter> y)"
   7.827 +  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join)
   7.828  
   7.829 -declare (in partial_order) weak_inf_of_singleton [simp del]
   7.830 +lemma (in lattice) le_iff_meet:
   7.831 +  assumes "x \<in> carrier L" "y \<in> carrier L"
   7.832 +  shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) = y"
   7.833 +  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet)
   7.834  
   7.835 -lemma (in partial_order) inf_of_singleton [simp]:
   7.836 -  "x \<in> carrier L ==> \<Sqinter>{x} = x"
   7.837 -  using weak_inf_of_singleton unfolding eq_is_equal .
   7.838 -
   7.839 -text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
   7.840 +text \<open> Total orders are lattices. \<close>
   7.841  
   7.842 -lemma (in lower_semilattice) meet_assoc_lemma:
   7.843 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   7.844 -  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
   7.845 -  using weak_meet_assoc_lemma L unfolding eq_is_equal .
   7.846 +sublocale total_order \<subseteq> weak?: lattice
   7.847 +  by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists)
   7.848 +    
   7.849 +text \<open>Functions that preserve joins and meets\<close>
   7.850 +  
   7.851 +definition join_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   7.852 +"join_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<squnion>\<^bsub>X\<^esub> y) = f x \<squnion>\<^bsub>Y\<^esub> f y)"
   7.853  
   7.854 -lemma (in lower_semilattice) meet_assoc:
   7.855 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   7.856 -  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   7.857 -  using weak_meet_assoc L unfolding eq_is_equal .
   7.858 -
   7.859 -
   7.860 -text \<open>Total Orders\<close>
   7.861 +definition meet_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   7.862 +"meet_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<sqinter>\<^bsub>X\<^esub> y) = f x \<sqinter>\<^bsub>Y\<^esub> f y)"
   7.863  
   7.864 -locale total_order = partial_order +
   7.865 -  assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   7.866 -
   7.867 -sublocale total_order < weak?: weak_total_order
   7.868 -  by standard (rule total_order_total)
   7.869 -
   7.870 -text \<open>Introduction rule: the usual definition of total order\<close>
   7.871 +lemma join_pres_isotone:
   7.872 +  assumes "f \<in> carrier X \<rightarrow> carrier Y" "join_pres X Y f"
   7.873 +  shows "isotone X Y f"
   7.874 +  using assms
   7.875 +  apply (rule_tac isotoneI)
   7.876 +  apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier)
   7.877 +  using lattice_def partial_order_def upper_semilattice_def apply blast
   7.878 +  using lattice_def partial_order_def upper_semilattice_def apply blast
   7.879 +  apply fastforce
   7.880 +done
   7.881  
   7.882 -lemma (in partial_order) total_orderI:
   7.883 -  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   7.884 -  shows "total_order L"
   7.885 -  by standard (rule total)
   7.886 -
   7.887 -text \<open>Total orders are lattices.\<close>
   7.888 -
   7.889 -sublocale total_order < weak?: lattice
   7.890 -  by standard (auto intro: sup_of_two_exists inf_of_two_exists)
   7.891 +lemma meet_pres_isotone:
   7.892 +  assumes "f \<in> carrier X \<rightarrow> carrier Y" "meet_pres X Y f"
   7.893 +  shows "isotone X Y f"
   7.894 +  using assms
   7.895 +  apply (rule_tac isotoneI)
   7.896 +  apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier)
   7.897 +  using lattice_def partial_order_def upper_semilattice_def apply blast
   7.898 +  using lattice_def partial_order_def upper_semilattice_def apply blast
   7.899 +  apply fastforce
   7.900 +done
   7.901  
   7.902  
   7.903 -text \<open>Complete lattices\<close>
   7.904 -
   7.905 -locale complete_lattice = lattice +
   7.906 -  assumes sup_exists:
   7.907 -    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   7.908 -    and inf_exists:
   7.909 -    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   7.910 +subsection \<open>Bounded Lattices\<close>
   7.911  
   7.912 -sublocale complete_lattice < weak?: weak_complete_lattice
   7.913 -  by standard (auto intro: sup_exists inf_exists)
   7.914 -
   7.915 -text \<open>Introduction rule: the usual definition of complete lattice\<close>
   7.916 +locale bounded_lattice = 
   7.917 +  lattice + 
   7.918 +  weak_partial_order_bottom + 
   7.919 +  weak_partial_order_top
   7.920  
   7.921 -lemma (in partial_order) complete_latticeI:
   7.922 -  assumes sup_exists:
   7.923 -    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   7.924 -    and inf_exists:
   7.925 -    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   7.926 -  shows "complete_lattice L"
   7.927 -  by standard (auto intro: sup_exists inf_exists)
   7.928 +sublocale bounded_lattice \<subseteq> weak_bounded_lattice ..
   7.929  
   7.930 -theorem (in partial_order) complete_lattice_criterion1:
   7.931 -  assumes top_exists: "EX g. greatest L g (carrier L)"
   7.932 -    and inf_exists:
   7.933 -      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
   7.934 -  shows "complete_lattice L"
   7.935 -proof (rule complete_latticeI)
   7.936 -  from top_exists obtain top where top: "greatest L top (carrier L)" ..
   7.937 -  fix A
   7.938 -  assume L: "A \<subseteq> carrier L"
   7.939 -  let ?B = "Upper L A"
   7.940 -  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
   7.941 -  then have B_non_empty: "?B ~= {}" by fast
   7.942 -  have B_L: "?B \<subseteq> carrier L" by simp
   7.943 -  from inf_exists [OF B_L B_non_empty]
   7.944 -  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
   7.945 -  have "least L b (Upper L A)"
   7.946 -apply (rule least_UpperI)
   7.947 -   apply (rule greatest_le [where A = "Lower L ?B"])
   7.948 -    apply (rule b_inf_B)
   7.949 -   apply (rule Lower_memI)
   7.950 -    apply (erule Upper_memD [THEN conjunct1])
   7.951 -     apply assumption
   7.952 -    apply (rule L)
   7.953 -   apply (fast intro: L [THEN subsetD])
   7.954 -  apply (erule greatest_Lower_below [OF b_inf_B])
   7.955 -  apply simp
   7.956 - apply (rule L)
   7.957 -apply (rule greatest_closed [OF b_inf_B])
   7.958 -done
   7.959 -  then show "EX s. least L s (Upper L A)" ..
   7.960 -next
   7.961 -  fix A
   7.962 -  assume L: "A \<subseteq> carrier L"
   7.963 -  show "EX i. greatest L i (Lower L A)"
   7.964 -  proof (cases "A = {}")
   7.965 -    case True then show ?thesis
   7.966 -      by (simp add: top_exists)
   7.967 -  next
   7.968 -    case False with L show ?thesis
   7.969 -      by (rule inf_exists)
   7.970 -  qed
   7.971 -qed
   7.972 +context bounded_lattice
   7.973 +begin
   7.974  
   7.975 -(* TODO: prove dual version *)
   7.976 -
   7.977 -
   7.978 -subsection \<open>Examples\<close>
   7.979 -
   7.980 -subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
   7.981 +lemma bottom_eq:  
   7.982 +  "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b = \<bottom>"
   7.983 +  by (metis bottom_closed bottom_lower le_antisym)
   7.984  
   7.985 -theorem powerset_is_complete_lattice:
   7.986 -  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
   7.987 -  (is "complete_lattice ?L")
   7.988 -proof (rule partial_order.complete_latticeI)
   7.989 -  show "partial_order ?L"
   7.990 -    by standard auto
   7.991 -next
   7.992 -  fix B
   7.993 -  assume "B \<subseteq> carrier ?L"
   7.994 -  then have "least ?L (\<Union>B) (Upper ?L B)"
   7.995 -    by (fastforce intro!: least_UpperI simp: Upper_def)
   7.996 -  then show "EX s. least ?L s (Upper ?L B)" ..
   7.997 -next
   7.998 -  fix B
   7.999 -  assume "B \<subseteq> carrier ?L"
  7.1000 -  then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
  7.1001 -    txt \<open>@{term "\<Inter>B"} is not the infimum of @{term B}:
  7.1002 -      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}!\<close>
  7.1003 -    by (fastforce intro!: greatest_LowerI simp: Lower_def)
  7.1004 -  then show "EX i. greatest ?L i (Lower ?L B)" ..
  7.1005 -qed
  7.1006 -
  7.1007 -text \<open>An other example, that of the lattice of subgroups of a group,
  7.1008 -  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
  7.1009 +lemma top_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>"
  7.1010 +  by (metis le_antisym top_closed top_higher)
  7.1011  
  7.1012  end
  7.1013 +
  7.1014 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Algebra/Order.thy	Thu Mar 02 21:16:02 2017 +0100
     8.3 @@ -0,0 +1,738 @@
     8.4 +(*  Title:      HOL/Algebra/Order.thy
     8.5 +    Author:     Clemens Ballarin, started 7 November 2003
     8.6 +    Copyright:  Clemens Ballarin
     8.7 +
     8.8 +Most congruence rules by Stephan Hohe.
     8.9 +With additional contributions from Alasdair Armstrong and Simon Foster.
    8.10 +*)
    8.11 +
    8.12 +theory Order
    8.13 +imports 
    8.14 +  "~~/src/HOL/Library/FuncSet"
    8.15 +  Congruence
    8.16 +begin
    8.17 +
    8.18 +section \<open>Orders\<close>
    8.19 +
    8.20 +subsection \<open>Partial Orders\<close>
    8.21 +
    8.22 +record 'a gorder = "'a eq_object" +
    8.23 +  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    8.24 +
    8.25 +abbreviation inv_gorder :: "_ \<Rightarrow> 'a gorder" where
    8.26 +  "inv_gorder L \<equiv>
    8.27 +   \<lparr> carrier = carrier L,
    8.28 +     eq = op .=\<^bsub>L\<^esub>,
    8.29 +     le = (\<lambda> x y. y \<sqsubseteq>\<^bsub>L \<^esub>x) \<rparr>"
    8.30 +
    8.31 +lemma inv_gorder_inv:
    8.32 +  "inv_gorder (inv_gorder L) = L"
    8.33 +  by simp
    8.34 +
    8.35 +locale weak_partial_order = equivalence L for L (structure) +
    8.36 +  assumes le_refl [intro, simp]:
    8.37 +      "x \<in> carrier L ==> x \<sqsubseteq> x"
    8.38 +    and weak_le_antisym [intro]:
    8.39 +      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
    8.40 +    and le_trans [trans]:
    8.41 +      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    8.42 +    and le_cong:
    8.43 +      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
    8.44 +      x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
    8.45 +
    8.46 +definition
    8.47 +  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    8.48 +  where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
    8.49 +
    8.50 +
    8.51 +subsubsection \<open>The order relation\<close>
    8.52 +
    8.53 +context weak_partial_order
    8.54 +begin
    8.55 +
    8.56 +lemma le_cong_l [intro, trans]:
    8.57 +  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    8.58 +  by (auto intro: le_cong [THEN iffD2])
    8.59 +
    8.60 +lemma le_cong_r [intro, trans]:
    8.61 +  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    8.62 +  by (auto intro: le_cong [THEN iffD1])
    8.63 +
    8.64 +lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
    8.65 +  by (simp add: le_cong_l)
    8.66 +
    8.67 +end
    8.68 +
    8.69 +lemma weak_llessI:
    8.70 +  fixes R (structure)
    8.71 +  assumes "x \<sqsubseteq> y" and "~(x .= y)"
    8.72 +  shows "x \<sqsubset> y"
    8.73 +  using assms unfolding lless_def by simp
    8.74 +
    8.75 +lemma lless_imp_le:
    8.76 +  fixes R (structure)
    8.77 +  assumes "x \<sqsubset> y"
    8.78 +  shows "x \<sqsubseteq> y"
    8.79 +  using assms unfolding lless_def by simp
    8.80 +
    8.81 +lemma weak_lless_imp_not_eq:
    8.82 +  fixes R (structure)
    8.83 +  assumes "x \<sqsubset> y"
    8.84 +  shows "\<not> (x .= y)"
    8.85 +  using assms unfolding lless_def by simp
    8.86 +
    8.87 +lemma weak_llessE:
    8.88 +  fixes R (structure)
    8.89 +  assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
    8.90 +  shows "P"
    8.91 +  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
    8.92 +
    8.93 +lemma (in weak_partial_order) lless_cong_l [trans]:
    8.94 +  assumes xx': "x .= x'"
    8.95 +    and xy: "x' \<sqsubset> y"
    8.96 +    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
    8.97 +  shows "x \<sqsubset> y"
    8.98 +  using assms unfolding lless_def by (auto intro: trans sym)
    8.99 +
   8.100 +lemma (in weak_partial_order) lless_cong_r [trans]:
   8.101 +  assumes xy: "x \<sqsubset> y"
   8.102 +    and  yy': "y .= y'"
   8.103 +    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   8.104 +  shows "x \<sqsubset> y'"
   8.105 +  using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
   8.106 +
   8.107 +
   8.108 +lemma (in weak_partial_order) lless_antisym:
   8.109 +  assumes "a \<in> carrier L" "b \<in> carrier L"
   8.110 +    and "a \<sqsubset> b" "b \<sqsubset> a"
   8.111 +  shows "P"
   8.112 +  using assms
   8.113 +  by (elim weak_llessE) auto
   8.114 +
   8.115 +lemma (in weak_partial_order) lless_trans [trans]:
   8.116 +  assumes "a \<sqsubset> b" "b \<sqsubset> c"
   8.117 +    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
   8.118 +  shows "a \<sqsubset> c"
   8.119 +  using assms unfolding lless_def by (blast dest: le_trans intro: sym)
   8.120 +
   8.121 +lemma weak_partial_order_subset:
   8.122 +  assumes "weak_partial_order L" "A \<subseteq> carrier L"
   8.123 +  shows "weak_partial_order (L\<lparr> carrier := A \<rparr>)"
   8.124 +proof -
   8.125 +  interpret L: weak_partial_order L
   8.126 +    by (simp add: assms)
   8.127 +  interpret equivalence "(L\<lparr> carrier := A \<rparr>)"
   8.128 +    by (simp add: L.equivalence_axioms assms(2) equivalence_subset)
   8.129 +  show ?thesis
   8.130 +    apply (unfold_locales, simp_all)
   8.131 +    using assms(2) apply auto[1]
   8.132 +    using assms(2) apply auto[1]
   8.133 +    apply (meson L.le_trans assms(2) contra_subsetD)
   8.134 +    apply (meson L.le_cong assms(2) subsetCE)
   8.135 +  done
   8.136 +qed
   8.137 +
   8.138 +
   8.139 +subsubsection \<open>Upper and lower bounds of a set\<close>
   8.140 +
   8.141 +definition
   8.142 +  Upper :: "[_, 'a set] => 'a set"
   8.143 +  where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
   8.144 +
   8.145 +definition
   8.146 +  Lower :: "[_, 'a set] => 'a set"
   8.147 +  where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
   8.148 +
   8.149 +lemma Upper_closed [intro!, simp]:
   8.150 +  "Upper L A \<subseteq> carrier L"
   8.151 +  by (unfold Upper_def) clarify
   8.152 +
   8.153 +lemma Upper_memD [dest]:
   8.154 +  fixes L (structure)
   8.155 +  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
   8.156 +  by (unfold Upper_def) blast
   8.157 +
   8.158 +lemma (in weak_partial_order) Upper_elemD [dest]:
   8.159 +  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   8.160 +  unfolding Upper_def elem_def
   8.161 +  by (blast dest: sym)
   8.162 +
   8.163 +lemma Upper_memI:
   8.164 +  fixes L (structure)
   8.165 +  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   8.166 +  by (unfold Upper_def) blast
   8.167 +
   8.168 +lemma (in weak_partial_order) Upper_elemI:
   8.169 +  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
   8.170 +  unfolding Upper_def by blast
   8.171 +
   8.172 +lemma Upper_antimono:
   8.173 +  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   8.174 +  by (unfold Upper_def) blast
   8.175 +
   8.176 +lemma (in weak_partial_order) Upper_is_closed [simp]:
   8.177 +  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
   8.178 +  by (rule is_closedI) (blast intro: Upper_memI)+
   8.179 +
   8.180 +lemma (in weak_partial_order) Upper_mem_cong:
   8.181 +  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   8.182 +    and aa': "a .= a'"
   8.183 +    and aelem: "a \<in> Upper L A"
   8.184 +  shows "a' \<in> Upper L A"
   8.185 +proof (rule Upper_memI[OF _ a'carr])
   8.186 +  fix y
   8.187 +  assume yA: "y \<in> A"
   8.188 +  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
   8.189 +  also note aa'
   8.190 +  finally
   8.191 +      show "y \<sqsubseteq> a'"
   8.192 +      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
   8.193 +qed
   8.194 +
   8.195 +lemma (in weak_partial_order) Upper_cong:
   8.196 +  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   8.197 +    and AA': "A {.=} A'"
   8.198 +  shows "Upper L A = Upper L A'"
   8.199 +unfolding Upper_def
   8.200 +apply rule
   8.201 + apply (rule, clarsimp) defer 1
   8.202 + apply (rule, clarsimp) defer 1
   8.203 +proof -
   8.204 +  fix x a'
   8.205 +  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   8.206 +    and a'A': "a' \<in> A'"
   8.207 +  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
   8.208 +
   8.209 +  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   8.210 +  from this obtain a
   8.211 +      where aA: "a \<in> A"
   8.212 +      and a'a: "a' .= a"
   8.213 +      by auto
   8.214 +  note [simp] = subsetD[OF Acarr aA] carr
   8.215 +
   8.216 +  note a'a
   8.217 +  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
   8.218 +  finally show "a' \<sqsubseteq> x" by simp
   8.219 +next
   8.220 +  fix x a
   8.221 +  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   8.222 +    and aA: "a \<in> A"
   8.223 +  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
   8.224 +
   8.225 +  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   8.226 +  from this obtain a'
   8.227 +      where a'A': "a' \<in> A'"
   8.228 +      and aa': "a .= a'"
   8.229 +      by auto
   8.230 +  note [simp] = subsetD[OF A'carr a'A'] carr
   8.231 +
   8.232 +  note aa'
   8.233 +  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
   8.234 +  finally show "a \<sqsubseteq> x" by simp
   8.235 +qed
   8.236 +
   8.237 +lemma Lower_closed [intro!, simp]:
   8.238 +  "Lower L A \<subseteq> carrier L"
   8.239 +  by (unfold Lower_def) clarify
   8.240 +
   8.241 +lemma Lower_memD [dest]:
   8.242 +  fixes L (structure)
   8.243 +  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
   8.244 +  by (unfold Lower_def) blast
   8.245 +
   8.246 +lemma Lower_memI:
   8.247 +  fixes L (structure)
   8.248 +  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   8.249 +  by (unfold Lower_def) blast
   8.250 +
   8.251 +lemma Lower_antimono:
   8.252 +  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   8.253 +  by (unfold Lower_def) blast
   8.254 +
   8.255 +lemma (in weak_partial_order) Lower_is_closed [simp]:
   8.256 +  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
   8.257 +  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
   8.258 +
   8.259 +lemma (in weak_partial_order) Lower_mem_cong:
   8.260 +  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   8.261 +    and aa': "a .= a'"
   8.262 +    and aelem: "a \<in> Lower L A"
   8.263 +  shows "a' \<in> Lower L A"
   8.264 +using assms Lower_closed[of L A]
   8.265 +by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
   8.266 +
   8.267 +lemma (in weak_partial_order) Lower_cong:
   8.268 +  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   8.269 +    and AA': "A {.=} A'"
   8.270 +  shows "Lower L A = Lower L A'"
   8.271 +unfolding Lower_def
   8.272 +apply rule
   8.273 + apply clarsimp defer 1
   8.274 + apply clarsimp defer 1
   8.275 +proof -
   8.276 +  fix x a'
   8.277 +  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   8.278 +    and a'A': "a' \<in> A'"
   8.279 +  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
   8.280 +  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
   8.281 +
   8.282 +  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   8.283 +  from this obtain a
   8.284 +      where aA: "a \<in> A"
   8.285 +      and a'a: "a' .= a"
   8.286 +      by auto
   8.287 +
   8.288 +  from aA and subsetD[OF Acarr aA]
   8.289 +      have "x \<sqsubseteq> a" by (rule aLxCond)
   8.290 +  also note a'a[symmetric]
   8.291 +  finally
   8.292 +      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
   8.293 +next
   8.294 +  fix x a
   8.295 +  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   8.296 +    and aA: "a \<in> A"
   8.297 +  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
   8.298 +  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
   8.299 +
   8.300 +  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   8.301 +  from this obtain a'
   8.302 +      where a'A': "a' \<in> A'"
   8.303 +      and aa': "a .= a'"
   8.304 +      by auto
   8.305 +  from a'A' and subsetD[OF A'carr a'A']
   8.306 +      have "x \<sqsubseteq> a'" by (rule a'LxCond)
   8.307 +  also note aa'[symmetric]
   8.308 +  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
   8.309 +qed
   8.310 +
   8.311 +text \<open>Jacobson: Theorem 8.1\<close>
   8.312 +
   8.313 +lemma Lower_empty [simp]:
   8.314 +  "Lower L {} = carrier L"
   8.315 +  by (unfold Lower_def) simp
   8.316 +
   8.317 +lemma Upper_empty [simp]:
   8.318 +  "Upper L {} = carrier L"
   8.319 +  by (unfold Upper_def) simp
   8.320 +
   8.321 +
   8.322 +subsubsection \<open>Least and greatest, as predicate\<close>
   8.323 +
   8.324 +definition
   8.325 +  least :: "[_, 'a, 'a set] => bool"
   8.326 +  where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
   8.327 +
   8.328 +definition
   8.329 +  greatest :: "[_, 'a, 'a set] => bool"
   8.330 +  where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
   8.331 +
   8.332 +text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
   8.333 +  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
   8.334 +
   8.335 +lemma least_closed [intro, simp]:
   8.336 +  "least L l A ==> l \<in> carrier L"
   8.337 +  by (unfold least_def) fast
   8.338 +
   8.339 +lemma least_mem:
   8.340 +  "least L l A ==> l \<in> A"
   8.341 +  by (unfold least_def) fast
   8.342 +
   8.343 +lemma (in weak_partial_order) weak_least_unique:
   8.344 +  "[| least L x A; least L y A |] ==> x .= y"
   8.345 +  by (unfold least_def) blast
   8.346 +
   8.347 +lemma least_le:
   8.348 +  fixes L (structure)
   8.349 +  shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   8.350 +  by (unfold least_def) fast
   8.351 +
   8.352 +lemma (in weak_partial_order) least_cong:
   8.353 +  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
   8.354 +  by (unfold least_def) (auto dest: sym)
   8.355 +
   8.356 +abbreviation is_lub :: "[_, 'a, 'a set] => bool"
   8.357 +where "is_lub L x A \<equiv> least L x (Upper L A)"
   8.358 +
   8.359 +text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for
   8.360 +  @{term "A {.=} A'"}\<close>
   8.361 +
   8.362 +lemma (in weak_partial_order) least_Upper_cong_l:
   8.363 +  assumes "x .= x'"
   8.364 +    and "x \<in> carrier L" "x' \<in> carrier L"
   8.365 +    and "A \<subseteq> carrier L"
   8.366 +  shows "least L x (Upper L A) = least L x' (Upper L A)"
   8.367 +  apply (rule least_cong) using assms by auto
   8.368 +
   8.369 +lemma (in weak_partial_order) least_Upper_cong_r:
   8.370 +  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
   8.371 +    and AA': "A {.=} A'"
   8.372 +  shows "least L x (Upper L A) = least L x (Upper L A')"
   8.373 +apply (subgoal_tac "Upper L A = Upper L A'", simp)
   8.374 +by (rule Upper_cong) fact+
   8.375 +
   8.376 +lemma least_UpperI:
   8.377 +  fixes L (structure)
   8.378 +  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   8.379 +    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   8.380 +    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   8.381 +  shows "least L s (Upper L A)"
   8.382 +proof -
   8.383 +  have "Upper L A \<subseteq> carrier L" by simp
   8.384 +  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   8.385 +  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   8.386 +  ultimately show ?thesis by (simp add: least_def)
   8.387 +qed
   8.388 +
   8.389 +lemma least_Upper_above:
   8.390 +  fixes L (structure)
   8.391 +  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   8.392 +  by (unfold least_def) blast
   8.393 +
   8.394 +lemma greatest_closed [intro, simp]:
   8.395 +  "greatest L l A ==> l \<in> carrier L"
   8.396 +  by (unfold greatest_def) fast
   8.397 +
   8.398 +lemma greatest_mem:
   8.399 +  "greatest L l A ==> l \<in> A"
   8.400 +  by (unfold greatest_def) fast
   8.401 +
   8.402 +lemma (in weak_partial_order) weak_greatest_unique:
   8.403 +  "[| greatest L x A; greatest L y A |] ==> x .= y"
   8.404 +  by (unfold greatest_def) blast
   8.405 +
   8.406 +lemma greatest_le:
   8.407 +  fixes L (structure)
   8.408 +  shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   8.409 +  by (unfold greatest_def) fast
   8.410 +
   8.411 +lemma (in weak_partial_order) greatest_cong:
   8.412 +  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
   8.413 +  greatest L x A = greatest L x' A"
   8.414 +  by (unfold greatest_def) (auto dest: sym)
   8.415 +
   8.416 +abbreviation is_glb :: "[_, 'a, 'a set] => bool"
   8.417 +where "is_glb L x A \<equiv> greatest L x (Lower L A)"
   8.418 +
   8.419 +text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for
   8.420 +  @{term "A {.=} A'"} \<close>
   8.421 +
   8.422 +lemma (in weak_partial_order) greatest_Lower_cong_l:
   8.423 +  assumes "x .= x'"
   8.424 +    and "x \<in> carrier L" "x' \<in> carrier L"
   8.425 +    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
   8.426 +  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
   8.427 +  apply (rule greatest_cong) using assms by auto
   8.428 +
   8.429 +lemma (in weak_partial_order) greatest_Lower_cong_r:
   8.430 +  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
   8.431 +    and AA': "A {.=} A'"
   8.432 +  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
   8.433 +apply (subgoal_tac "Lower L A = Lower L A'", simp)
   8.434 +by (rule Lower_cong) fact+
   8.435 +
   8.436 +lemma greatest_LowerI:
   8.437 +  fixes L (structure)
   8.438 +  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   8.439 +    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   8.440 +    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   8.441 +  shows "greatest L i (Lower L A)"
   8.442 +proof -
   8.443 +  have "Lower L A \<subseteq> carrier L" by simp
   8.444 +  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   8.445 +  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   8.446 +  ultimately show ?thesis by (simp add: greatest_def)
   8.447 +qed
   8.448 +
   8.449 +lemma greatest_Lower_below:
   8.450 +  fixes L (structure)
   8.451 +  shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   8.452 +  by (unfold greatest_def) blast
   8.453 +
   8.454 +lemma Lower_dual [simp]:
   8.455 +  "Lower (inv_gorder L) A = Upper L A"
   8.456 +  by (simp add:Upper_def Lower_def)
   8.457 +
   8.458 +lemma Upper_dual [simp]:
   8.459 +  "Upper (inv_gorder L) A = Lower L A"
   8.460 +  by (simp add:Upper_def Lower_def)
   8.461 +
   8.462 +lemma least_dual [simp]:
   8.463 +  "least (inv_gorder L) x A = greatest L x A"
   8.464 +  by (simp add:least_def greatest_def)
   8.465 +
   8.466 +lemma greatest_dual [simp]:
   8.467 +  "greatest (inv_gorder L) x A = least L x A"
   8.468 +  by (simp add:least_def greatest_def)
   8.469 +
   8.470 +lemma (in weak_partial_order) dual_weak_order:
   8.471 +  "weak_partial_order (inv_gorder L)"
   8.472 +  apply (unfold_locales)
   8.473 +  apply (simp_all)
   8.474 +  apply (metis sym)
   8.475 +  apply (metis trans)
   8.476 +  apply (metis weak_le_antisym)
   8.477 +  apply (metis le_trans)
   8.478 +  apply (metis le_cong_l le_cong_r sym)
   8.479 +done
   8.480 +
   8.481 +lemma dual_weak_order_iff:
   8.482 +  "weak_partial_order (inv_gorder A) \<longleftrightarrow> weak_partial_order A"
   8.483 +proof
   8.484 +  assume "weak_partial_order (inv_gorder A)"
   8.485 +  then interpret dpo: weak_partial_order "inv_gorder A"
   8.486 +  rewrites "carrier (inv_gorder A) = carrier A"
   8.487 +  and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
   8.488 +  and   "eq (inv_gorder A)      = eq A"
   8.489 +    by (simp_all)
   8.490 +  show "weak_partial_order A"
   8.491 +    by (unfold_locales, auto intro: dpo.sym dpo.trans dpo.le_trans)
   8.492 +next
   8.493 +  assume "weak_partial_order A"
   8.494 +  thus "weak_partial_order (inv_gorder A)"
   8.495 +    by (metis weak_partial_order.dual_weak_order)
   8.496 +qed
   8.497 +
   8.498 +
   8.499 +subsubsection \<open>Intervals\<close>
   8.500 +
   8.501 +definition
   8.502 +  at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set" ("(1\<lbrace>_.._\<rbrace>\<index>)")
   8.503 +  where "\<lbrace>l..u\<rbrace>\<^bsub>A\<^esub> = {x \<in> carrier A. l \<sqsubseteq>\<^bsub>A\<^esub> x \<and> x \<sqsubseteq>\<^bsub>A\<^esub> u}"
   8.504 +
   8.505 +context weak_partial_order
   8.506 +begin
   8.507 +  
   8.508 +  lemma at_least_at_most_upper [dest]:
   8.509 +    "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> x \<sqsubseteq> b"
   8.510 +    by (simp add: at_least_at_most_def)
   8.511 +
   8.512 +  lemma at_least_at_most_lower [dest]:
   8.513 +    "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> a \<sqsubseteq> x"
   8.514 +    by (simp add: at_least_at_most_def)
   8.515 +
   8.516 +  lemma at_least_at_most_closed: "\<lbrace>a..b\<rbrace> \<subseteq> carrier L"
   8.517 +    by (auto simp add: at_least_at_most_def)
   8.518 +
   8.519 +  lemma at_least_at_most_member [intro]: 
   8.520 +    "\<lbrakk> x \<in> carrier L; a \<sqsubseteq> x; x \<sqsubseteq> b \<rbrakk> \<Longrightarrow> x \<in> \<lbrace>a..b\<rbrace>"
   8.521 +    by (simp add: at_least_at_most_def)
   8.522 +
   8.523 +end
   8.524 +
   8.525 +
   8.526 +subsubsection \<open>Isotone functions\<close>
   8.527 +
   8.528 +definition isotone :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   8.529 +  where
   8.530 +  "isotone A B f \<equiv>
   8.531 +   weak_partial_order A \<and> weak_partial_order B \<and>
   8.532 +   (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. x \<sqsubseteq>\<^bsub>A\<^esub> y \<longrightarrow> f x \<sqsubseteq>\<^bsub>B\<^esub> f y)"
   8.533 +
   8.534 +lemma isotoneI [intro?]:
   8.535 +  fixes f :: "'a \<Rightarrow> 'b"
   8.536 +  assumes "weak_partial_order L1"
   8.537 +          "weak_partial_order L2"
   8.538 +          "(\<And>x y. \<lbrakk> x \<in> carrier L1; y \<in> carrier L1; x \<sqsubseteq>\<^bsub>L1\<^esub> y \<rbrakk> 
   8.539 +                   \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L2\<^esub> f y)"
   8.540 +  shows "isotone L1 L2 f"
   8.541 +  using assms by (auto simp add:isotone_def)
   8.542 +
   8.543 +abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Mono\<index>")
   8.544 +  where "Monotone L f \<equiv> isotone L L f"
   8.545 +
   8.546 +lemma use_iso1:
   8.547 +  "\<lbrakk>isotone A A f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
   8.548 +   f x \<sqsubseteq>\<^bsub>A\<^esub> f y"
   8.549 +  by (simp add: isotone_def)
   8.550 +
   8.551 +lemma use_iso2:
   8.552 +  "\<lbrakk>isotone A B f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
   8.553 +   f x \<sqsubseteq>\<^bsub>B\<^esub> f y"
   8.554 +  by (simp add: isotone_def)
   8.555 +
   8.556 +lemma iso_compose:
   8.557 +  "\<lbrakk>f \<in> carrier A \<rightarrow> carrier B; isotone A B f; g \<in> carrier B \<rightarrow> carrier C; isotone B C g\<rbrakk> \<Longrightarrow>
   8.558 +   isotone A C (g \<circ> f)"
   8.559 +  by (simp add: isotone_def, safe, metis Pi_iff)
   8.560 +
   8.561 +lemma (in weak_partial_order) inv_isotone [simp]: 
   8.562 +  "isotone (inv_gorder A) (inv_gorder B) f = isotone A B f"
   8.563 +  by (auto simp add:isotone_def dual_weak_order dual_weak_order_iff)
   8.564 +
   8.565 +
   8.566 +subsubsection \<open>Idempotent functions\<close>
   8.567 +
   8.568 +definition idempotent :: 
   8.569 +  "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Idem\<index>") where
   8.570 +  "idempotent L f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
   8.571 +
   8.572 +lemma (in weak_partial_order) idempotent:
   8.573 +  "\<lbrakk> Idem f; x \<in> carrier L \<rbrakk> \<Longrightarrow> f (f x) .= f x"
   8.574 +  by (auto simp add: idempotent_def)
   8.575 +
   8.576 +
   8.577 +subsubsection \<open>Order embeddings\<close>
   8.578 +
   8.579 +definition order_emb :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   8.580 +  where
   8.581 +  "order_emb A B f \<equiv> weak_partial_order A 
   8.582 +                   \<and> weak_partial_order B 
   8.583 +                   \<and> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f x \<sqsubseteq>\<^bsub>B\<^esub> f y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>A\<^esub> y )"
   8.584 +
   8.585 +lemma order_emb_isotone: "order_emb A B f \<Longrightarrow> isotone A B f"
   8.586 +  by (auto simp add: isotone_def order_emb_def)
   8.587 +
   8.588 +
   8.589 +subsubsection \<open>Commuting functions\<close>
   8.590 +    
   8.591 +definition commuting :: "('a, 'c) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
   8.592 +"commuting A f g = (\<forall>x\<in>carrier A. (f \<circ> g) x .=\<^bsub>A\<^esub> (g \<circ> f) x)"
   8.593 +
   8.594 +subsection \<open>Partial orders where \<open>eq\<close> is the Equality\<close>
   8.595 +
   8.596 +locale partial_order = weak_partial_order +
   8.597 +  assumes eq_is_equal: "op .= = op ="
   8.598 +begin
   8.599 +
   8.600 +declare weak_le_antisym [rule del]
   8.601 +
   8.602 +lemma le_antisym [intro]:
   8.603 +  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
   8.604 +  using weak_le_antisym unfolding eq_is_equal .
   8.605 +
   8.606 +lemma lless_eq:
   8.607 +  "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
   8.608 +  unfolding lless_def by (simp add: eq_is_equal)
   8.609 +
   8.610 +lemma set_eq_is_eq: "A {.=} B \<longleftrightarrow> A = B"
   8.611 +  by (auto simp add: set_eq_def elem_def eq_is_equal)
   8.612 +
   8.613 +end
   8.614 +
   8.615 +lemma (in partial_order) dual_order:
   8.616 +  "partial_order (inv_gorder L)"
   8.617 +proof -
   8.618 +  interpret dwo: weak_partial_order "inv_gorder L"
   8.619 +    by (metis dual_weak_order)
   8.620 +  show ?thesis
   8.621 +    by (unfold_locales, simp add:eq_is_equal)
   8.622 +qed
   8.623 +
   8.624 +lemma dual_order_iff:
   8.625 +  "partial_order (inv_gorder A) \<longleftrightarrow> partial_order A"
   8.626 +proof
   8.627 +  assume assm:"partial_order (inv_gorder A)"
   8.628 +  then interpret po: partial_order "inv_gorder A"
   8.629 +  rewrites "carrier (inv_gorder A) = carrier A"
   8.630 +  and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
   8.631 +  and   "eq (inv_gorder A)      = eq A"
   8.632 +    by (simp_all)
   8.633 +  show "partial_order A"
   8.634 +    apply (unfold_locales, simp_all)
   8.635 +    apply (metis po.sym, metis po.trans)
   8.636 +    apply (metis po.weak_le_antisym, metis po.le_trans)
   8.637 +    apply (metis (full_types) po.eq_is_equal, metis po.eq_is_equal)
   8.638 +  done
   8.639 +next
   8.640 +  assume "partial_order A"
   8.641 +  thus "partial_order (inv_gorder A)"
   8.642 +    by (metis partial_order.dual_order)
   8.643 +qed
   8.644 +
   8.645 +text \<open>Least and greatest, as predicate\<close>
   8.646 +
   8.647 +lemma (in partial_order) least_unique:
   8.648 +  "[| least L x A; least L y A |] ==> x = y"
   8.649 +  using weak_least_unique unfolding eq_is_equal .
   8.650 +
   8.651 +lemma (in partial_order) greatest_unique:
   8.652 +  "[| greatest L x A; greatest L y A |] ==> x = y"
   8.653 +  using weak_greatest_unique unfolding eq_is_equal .
   8.654 +
   8.655 +
   8.656 +subsection \<open>Bounded Orders\<close>
   8.657 +
   8.658 +definition
   8.659 +  top :: "_ => 'a" ("\<top>\<index>") where
   8.660 +  "\<top>\<^bsub>L\<^esub> = (SOME x. greatest L x (carrier L))"
   8.661 +
   8.662 +definition
   8.663 +  bottom :: "_ => 'a" ("\<bottom>\<index>") where
   8.664 +  "\<bottom>\<^bsub>L\<^esub> = (SOME x. least L x (carrier L))"
   8.665 +
   8.666 +locale weak_partial_order_bottom = weak_partial_order L for L (structure) +
   8.667 +  assumes bottom_exists: "\<exists> x. least L x (carrier L)"
   8.668 +begin
   8.669 +
   8.670 +lemma bottom_least: "least L \<bottom> (carrier L)"
   8.671 +proof -
   8.672 +  obtain x where "least L x (carrier L)"
   8.673 +    by (metis bottom_exists)
   8.674 +
   8.675 +  thus ?thesis
   8.676 +    by (auto intro:someI2 simp add: bottom_def)
   8.677 +qed
   8.678 +
   8.679 +lemma bottom_closed [simp, intro]:
   8.680 +  "\<bottom> \<in> carrier L"
   8.681 +  by (metis bottom_least least_mem)
   8.682 +
   8.683 +lemma bottom_lower [simp, intro]:
   8.684 +  "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqsubseteq> x"
   8.685 +  by (metis bottom_least least_le)
   8.686 +
   8.687 +end
   8.688 +
   8.689 +locale weak_partial_order_top = weak_partial_order L for L (structure) +
   8.690 +  assumes top_exists: "\<exists> x. greatest L x (carrier L)"
   8.691 +begin
   8.692 +
   8.693 +lemma top_greatest: "greatest L \<top> (carrier L)"
   8.694 +proof -
   8.695 +  obtain x where "greatest L x (carrier L)"
   8.696 +    by (metis top_exists)
   8.697 +
   8.698 +  thus ?thesis
   8.699 +    by (auto intro:someI2 simp add: top_def)
   8.700 +qed
   8.701 +
   8.702 +lemma top_closed [simp, intro]:
   8.703 +  "\<top> \<in> carrier L"
   8.704 +  by (metis greatest_mem top_greatest)
   8.705 +
   8.706 +lemma top_higher [simp, intro]:
   8.707 +  "x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> \<top>"
   8.708 +  by (metis greatest_le top_greatest)
   8.709 +
   8.710 +end
   8.711 +
   8.712 +
   8.713 +subsection \<open>Total Orders\<close>
   8.714 +
   8.715 +locale weak_total_order = weak_partial_order +
   8.716 +  assumes total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   8.717 +
   8.718 +text \<open>Introduction rule: the usual definition of total order\<close>
   8.719 +
   8.720 +lemma (in weak_partial_order) weak_total_orderI:
   8.721 +  assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   8.722 +  shows "weak_total_order L"
   8.723 +  by unfold_locales (rule total)
   8.724 +
   8.725 +
   8.726 +subsection \<open>Total orders where \<open>eq\<close> is the Equality\<close>
   8.727 +
   8.728 +locale total_order = partial_order +
   8.729 +  assumes total_order_total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   8.730 +
   8.731 +sublocale total_order < weak?: weak_total_order
   8.732 +  by unfold_locales (rule total_order_total)
   8.733 +
   8.734 +text \<open>Introduction rule: the usual definition of total order\<close>
   8.735 +
   8.736 +lemma (in partial_order) total_orderI:
   8.737 +  assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   8.738 +  shows "total_order L"
   8.739 +  by unfold_locales (rule total)
   8.740 +
   8.741 +end
     9.1 --- a/src/HOL/ROOT	Fri Mar 03 23:21:24 2017 +0100
     9.2 +++ b/src/HOL/ROOT	Thu Mar 02 21:16:02 2017 +0100
     9.3 @@ -297,7 +297,9 @@
     9.4      "~~/src/HOL/Number_Theory/Primes"
     9.5      "~~/src/HOL/Library/Permutation"
     9.6    theories
     9.7 -    (*** New development, based on explicit structures ***)
     9.8 +    (* Orders and Lattices *)
     9.9 +    Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
    9.10 +
    9.11      (* Groups *)
    9.12      FiniteProduct        (* Product operator for commutative groups *)
    9.13      Sylow                (* Sylow's theorem *)