# HG changeset patch
# User ballarin
# Date 1488485762 -3600
# Node ID 30d0b2f1df768f398c6a36da855205aa866a99a9
# Parent  b47ba1778e44f1a67fcdfec6f35cf3c1e3c090ba
Knaster-Tarski fixed point theorem and Galois Connections.

diff -r b47ba1778e44 -r 30d0b2f1df76 CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Mar 03 23:21:24 2017 +0100
+++ b/CONTRIBUTORS	Thu Mar 02 21:16:02 2017 +0100
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* March 2017: Alasdair Armstrong and Simon Foster, University of York
+  Fixed-point theory and Galois Connections in HOL-Algebra.
+
 * February 2017: Florian Haftmann, TUM
   Statically embedded computations implemented by generated code.
 
diff -r b47ba1778e44 -r 30d0b2f1df76 NEWS
--- a/NEWS	Fri Mar 03 23:21:24 2017 +0100
+++ b/NEWS	Thu Mar 02 21:16:02 2017 +0100
@@ -108,6 +108,9 @@
     with type class annotations. As a result, the tactic that derives
     it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
 
+* Session HOL-Algebra extended by additional lattice theory: the
+Knaster-Tarski fixed point theorem and Galois Connections.
+
 * Session HOL-Analysis: more material involving arcs, paths, covering
 spaces, innessential maps, retracts. Major results include the Jordan
 Curve Theorem and the Great Picard Theorem.
diff -r b47ba1778e44 -r 30d0b2f1df76 src/HOL/Algebra/Complete_Lattice.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Thu Mar 02 21:16:02 2017 +0100
@@ -0,0 +1,1191 @@
+(*  Title:      HOL/Algebra/Complete_Lattice.thy
+    Author:     Clemens Ballarin, started 7 November 2003
+    Copyright:  Clemens Ballarin
+
+Most congruence rules by Stephan Hohe.
+With additional contributions from Alasdair Armstrong and Simon Foster.
+*)
+
+theory Complete_Lattice
+imports Lattice
+begin
+
+section \<open>Complete Lattices\<close>
+
+locale weak_complete_lattice = weak_partial_order +
+  assumes sup_exists:
+    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
+    and inf_exists:
+    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
+
+sublocale weak_complete_lattice \<subseteq> weak_lattice
+proof
+  fix x y
+  assume a: "x \<in> carrier L" "y \<in> carrier L"
+  thus "\<exists>s. is_lub L s {x, y}"
+    by (rule_tac sup_exists[of "{x, y}"], auto)
+  from a show "\<exists>s. is_glb L s {x, y}"
+    by (rule_tac inf_exists[of "{x, y}"], auto)
+qed
+
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
+
+lemma (in weak_partial_order) weak_complete_latticeI:
+  assumes sup_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
+    and inf_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
+  shows "weak_complete_lattice L"
+  by standard (auto intro: sup_exists inf_exists)
+
+lemma (in weak_complete_lattice) dual_weak_complete_lattice:
+  "weak_complete_lattice (inv_gorder L)"
+proof -
+  interpret dual: weak_lattice "inv_gorder L"
+    by (metis dual_weak_lattice)
+
+  show ?thesis
+    apply (unfold_locales)
+    apply (simp_all add:inf_exists sup_exists)
+  done
+qed
+
+lemma (in weak_complete_lattice) supI:
+  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
+  ==> P (\<Squnion>A)"
+proof (unfold sup_def)
+  assume L: "A \<subseteq> carrier L"
+    and P: "!!l. least L l (Upper L A) ==> P l"
+  with sup_exists obtain s where "least L s (Upper L A)" by blast
+  with L show "P (SOME l. least L l (Upper L A))"
+  by (fast intro: someI2 weak_least_unique P)
+qed
+
+lemma (in weak_complete_lattice) sup_closed [simp]:
+  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
+  by (rule supI) simp_all
+
+lemma (in weak_complete_lattice) sup_cong:
+  assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"
+  shows "\<Squnion> A .= \<Squnion> B"
+proof -
+  have "\<And> x. is_lub L x A \<longleftrightarrow> is_lub L x B"
+    by (rule least_Upper_cong_r, simp_all add: assms)
+  moreover have "\<Squnion> B \<in> carrier L"
+    by (simp add: assms(2))
+  ultimately show ?thesis
+    by (simp add: sup_def)
+qed
+
+sublocale weak_complete_lattice \<subseteq> weak_bounded_lattice
+  apply (unfold_locales)
+  apply (metis Upper_empty empty_subsetI sup_exists)
+  apply (metis Lower_empty empty_subsetI inf_exists)
+done
+
+lemma (in weak_complete_lattice) infI:
+  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
+  ==> P (\<Sqinter>A)"
+proof (unfold inf_def)
+  assume L: "A \<subseteq> carrier L"
+    and P: "!!l. greatest L l (Lower L A) ==> P l"
+  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
+  with L show "P (SOME l. greatest L l (Lower L A))"
+  by (fast intro: someI2 weak_greatest_unique P)
+qed
+
+lemma (in weak_complete_lattice) inf_closed [simp]:
+  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
+  by (rule infI) simp_all
+
+lemma (in weak_complete_lattice) inf_cong:
+  assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"
+  shows "\<Sqinter> A .= \<Sqinter> B"
+proof -
+  have "\<And> x. is_glb L x A \<longleftrightarrow> is_glb L x B"
+    by (rule greatest_Lower_cong_r, simp_all add: assms)
+  moreover have "\<Sqinter> B \<in> carrier L"
+    by (simp add: assms(2))
+  ultimately show ?thesis
+    by (simp add: inf_def)
+qed
+
+theorem (in weak_partial_order) weak_complete_lattice_criterion1:
+  assumes top_exists: "EX g. greatest L g (carrier L)"
+    and inf_exists:
+      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
+  shows "weak_complete_lattice L"
+proof (rule weak_complete_latticeI)
+  from top_exists obtain top where top: "greatest L top (carrier L)" ..
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  let ?B = "Upper L A"
+  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
+  then have B_non_empty: "?B ~= {}" by fast
+  have B_L: "?B \<subseteq> carrier L" by simp
+  from inf_exists [OF B_L B_non_empty]
+  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
+  have "least L b (Upper L A)"
+apply (rule least_UpperI)
+   apply (rule greatest_le [where A = "Lower L ?B"])
+    apply (rule b_inf_B)
+   apply (rule Lower_memI)
+    apply (erule Upper_memD [THEN conjunct1])
+     apply assumption
+    apply (rule L)
+   apply (fast intro: L [THEN subsetD])
+  apply (erule greatest_Lower_below [OF b_inf_B])
+  apply simp
+ apply (rule L)
+apply (rule greatest_closed [OF b_inf_B])
+done
+  then show "EX s. least L s (Upper L A)" ..
+next
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  show "EX i. greatest L i (Lower L A)"
+  proof (cases "A = {}")
+    case True then show ?thesis
+      by (simp add: top_exists)
+  next
+    case False with L show ?thesis
+      by (rule inf_exists)
+  qed
+qed
+
+
+text \<open>Supremum\<close>
+
+declare (in partial_order) weak_sup_of_singleton [simp del]
+
+lemma (in partial_order) sup_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Squnion>{x} = x"
+  using weak_sup_of_singleton unfolding eq_is_equal .
+
+lemma (in upper_semilattice) join_assoc_lemma:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
+  using weak_join_assoc_lemma L unfolding eq_is_equal .
+
+lemma (in upper_semilattice) join_assoc:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+  using weak_join_assoc L unfolding eq_is_equal .
+
+
+text \<open>Infimum\<close>
+
+declare (in partial_order) weak_inf_of_singleton [simp del]
+
+lemma (in partial_order) inf_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Sqinter>{x} = x"
+  using weak_inf_of_singleton unfolding eq_is_equal .
+
+text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
+
+lemma (in lower_semilattice) meet_assoc_lemma:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
+  using weak_meet_assoc_lemma L unfolding eq_is_equal .
+
+lemma (in lower_semilattice) meet_assoc:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+  using weak_meet_assoc L unfolding eq_is_equal .
+
+
+subsection \<open>Infimum Laws\<close>
+
+context weak_complete_lattice
+begin
+
+lemma inf_glb: 
+  assumes "A \<subseteq> carrier L"
+  shows "greatest L (\<Sqinter>A) (Lower L A)"
+proof -
+  obtain i where "greatest L i (Lower L A)"
+    by (metis assms inf_exists)
+
+  thus ?thesis
+    apply (simp add: inf_def)
+    apply (rule someI2[of _ "i"])
+    apply (auto)
+  done
+qed
+
+lemma inf_lower:
+  assumes "A \<subseteq> carrier L" "x \<in> A"
+  shows "\<Sqinter>A \<sqsubseteq> x"
+  by (metis assms greatest_Lower_below inf_glb)
+
+lemma inf_greatest: 
+  assumes "A \<subseteq> carrier L" "z \<in> carrier L" 
+          "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x)"
+  shows "z \<sqsubseteq> \<Sqinter>A"
+  by (metis Lower_memI assms greatest_le inf_glb)
+
+lemma weak_inf_empty [simp]: "\<Sqinter>{} .= \<top>"
+  by (metis Lower_empty empty_subsetI inf_glb top_greatest weak_greatest_unique)
+
+lemma weak_inf_carrier [simp]: "\<Sqinter>carrier L .= \<bottom>"
+  by (metis bottom_weak_eq inf_closed inf_lower subset_refl)
+
+lemma weak_inf_insert [simp]: 
+  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
+  apply (rule weak_le_antisym)
+  apply (force intro: meet_le inf_greatest inf_lower inf_closed)
+  apply (rule inf_greatest)
+  apply (force)
+  apply (force intro: inf_closed)
+  apply (auto)
+  apply (metis inf_closed meet_left)
+  apply (force intro: le_trans inf_closed meet_right meet_left inf_lower)
+done
+
+
+subsection \<open>Supremum Laws\<close>
+
+lemma sup_lub: 
+  assumes "A \<subseteq> carrier L"
+  shows "least L (\<Squnion>A) (Upper L A)"
+    by (metis Upper_is_closed assms least_closed least_cong supI sup_closed sup_exists weak_least_unique)
+
+lemma sup_upper: 
+  assumes "A \<subseteq> carrier L" "x \<in> A"
+  shows "x \<sqsubseteq> \<Squnion>A"
+  by (metis assms least_Upper_above supI)
+
+lemma sup_least:
+  assumes "A \<subseteq> carrier L" "z \<in> carrier L" 
+          "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z)" 
+  shows "\<Squnion>A \<sqsubseteq> z"
+  by (metis Upper_memI assms least_le sup_lub)
+
+lemma weak_sup_empty [simp]: "\<Squnion>{} .= \<bottom>"
+  by (metis Upper_empty bottom_least empty_subsetI sup_lub weak_least_unique)
+
+lemma weak_sup_carrier [simp]: "\<Squnion>carrier L .= \<top>"
+  by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)
+
+lemma weak_sup_insert [simp]: 
+  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Squnion>insert a A .= a \<squnion> \<Squnion>A"
+  apply (rule weak_le_antisym)
+  apply (rule sup_least)
+  apply (auto)
+  apply (metis join_left sup_closed)
+  apply (rule le_trans) defer
+  apply (rule join_right)
+  apply (auto)
+  apply (rule join_le)
+  apply (auto intro: sup_upper sup_least sup_closed)
+done
+
+end
+
+
+subsection \<open>Fixed points of a lattice\<close>
+
+definition "fps L f = {x \<in> carrier L. f x .=\<^bsub>L\<^esub> x}"
+
+abbreviation "fpl L f \<equiv> L\<lparr>carrier := fps L f\<rparr>"
+
+lemma (in weak_partial_order) 
+  use_fps: "x \<in> fps L f \<Longrightarrow> f x .= x"
+  by (simp add: fps_def)
+
+lemma fps_carrier [simp]:
+  "fps L f \<subseteq> carrier L"
+  by (auto simp add: fps_def)
+
+lemma (in weak_complete_lattice) fps_sup_image: 
+  assumes "f \<in> carrier L \<rightarrow> carrier L" "A \<subseteq> fps L f" 
+  shows "\<Squnion> (f ` A) .= \<Squnion> A"
+proof -
+  from assms(2) have AL: "A \<subseteq> carrier L"
+    by (auto simp add: fps_def)
+  
+  show ?thesis
+  proof (rule sup_cong, simp_all add: AL)
+    from assms(1) AL show "f ` A \<subseteq> carrier L"
+      by (auto)
+    from assms(2) show "f ` A {.=} A"
+      apply (auto simp add: fps_def)
+      apply (rule set_eqI2)
+      apply blast
+      apply (rename_tac b)
+      apply (rule_tac x="f b" in bexI)
+      apply (metis (mono_tags, lifting) Ball_Collect assms(1) Pi_iff local.sym)
+      apply (auto)
+    done
+  qed
+qed
+
+lemma (in weak_complete_lattice) fps_idem:
+  "\<lbrakk> f \<in> carrier L \<rightarrow> carrier L; Idem f \<rbrakk> \<Longrightarrow> fps L f {.=} f ` carrier L"
+  apply (rule set_eqI2)
+  apply (auto simp add: idempotent_def fps_def)
+  apply (metis Pi_iff local.sym)
+  apply force
+done
+
+context weak_complete_lattice
+begin
+
+lemma weak_sup_pre_fixed_point: 
+  assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"
+  shows "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"
+proof (rule sup_least)
+  from assms(3) show AL: "A \<subseteq> carrier L"
+    by (auto simp add: fps_def)
+  thus fA: "f (\<Squnion>A) \<in> carrier L"
+    by (simp add: assms funcset_carrier[of f L L])
+  fix x
+  assume xA: "x \<in> A"
+  hence "x \<in> fps L f"
+    using assms subsetCE by blast
+  hence "f x .=\<^bsub>L\<^esub> x"
+    by (auto simp add: fps_def)
+  moreover have "f x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
+    by (meson AL assms(2) subsetCE sup_closed sup_upper use_iso1 xA)
+  ultimately show "x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
+    by (meson AL fA assms(1) funcset_carrier le_cong local.refl subsetCE xA)
+qed
+
+lemma weak_sup_post_fixed_point: 
+  assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"
+  shows "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"
+proof (rule inf_greatest)
+  from assms(3) show AL: "A \<subseteq> carrier L"
+    by (auto simp add: fps_def)
+  thus fA: "f (\<Sqinter>A) \<in> carrier L"
+    by (simp add: assms funcset_carrier[of f L L])
+  fix x
+  assume xA: "x \<in> A"
+  hence "x \<in> fps L f"
+    using assms subsetCE by blast
+  hence "f x .=\<^bsub>L\<^esub> x"
+    by (auto simp add: fps_def)
+  moreover have "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f x"
+    by (meson AL assms(2) inf_closed inf_lower subsetCE use_iso1 xA)   
+  ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> x"
+    by (meson AL assms(1) fA funcset_carrier le_cong_r subsetCE xA)
+qed
+
+
+subsubsection \<open>Least fixed points\<close>
+
+lemma LFP_closed [intro, simp]:
+  "\<mu> f \<in> carrier L"
+  by (metis (lifting) LFP_def inf_closed mem_Collect_eq subsetI)
+
+lemma LFP_lowerbound: 
+  assumes "x \<in> carrier L" "f x \<sqsubseteq> x" 
+  shows "\<mu> f \<sqsubseteq> x"
+  by (auto intro:inf_lower assms simp add:LFP_def)
+
+lemma LFP_greatest: 
+  assumes "x \<in> carrier L" 
+          "(\<And>u. \<lbrakk> u \<in> carrier L; f u \<sqsubseteq> u \<rbrakk> \<Longrightarrow> x \<sqsubseteq> u)"
+  shows "x \<sqsubseteq> \<mu> f"
+  by (auto simp add:LFP_def intro:inf_greatest assms)
+
+lemma LFP_lemma2: 
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "f (\<mu> f) \<sqsubseteq> \<mu> f"
+  using assms
+  apply (auto simp add:Pi_def)
+  apply (rule LFP_greatest)
+  apply (metis LFP_closed)
+  apply (metis LFP_closed LFP_lowerbound le_trans use_iso1)
+done
+
+lemma LFP_lemma3: 
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "\<mu> f \<sqsubseteq> f (\<mu> f)"
+  using assms
+  apply (auto simp add:Pi_def)
+  apply (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
+done
+
+lemma LFP_weak_unfold: 
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<mu> f .= f (\<mu> f)"
+  by (auto intro: LFP_lemma2 LFP_lemma3 funcset_mem)
+
+lemma LFP_fixed_point [intro]:
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "\<mu> f \<in> fps L f"
+proof -
+  have "f (\<mu> f) \<in> carrier L"
+    using assms(2) by blast
+  with assms show ?thesis
+    by (simp add: LFP_weak_unfold fps_def local.sym)
+qed
+
+lemma LFP_least_fixed_point:
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
+  shows "\<mu> f \<sqsubseteq> x"
+  using assms by (force intro: LFP_lowerbound simp add: fps_def)
+  
+lemma LFP_idem: 
+  assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
+  shows "\<mu> f .= (f \<bottom>)"
+proof (rule weak_le_antisym)
+  from assms(1) show fb: "f \<bottom> \<in> carrier L"
+    by (rule funcset_mem, simp)
+  from assms show mf: "\<mu> f \<in> carrier L"
+    by blast
+  show "\<mu> f \<sqsubseteq> f \<bottom>"
+  proof -
+    have "f (f \<bottom>) .= f \<bottom>"
+      by (auto simp add: fps_def fb assms(3) idempotent)
+    moreover have "f (f \<bottom>) \<in> carrier L"
+      by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
+    ultimately show ?thesis
+      by (auto intro: LFP_lowerbound simp add: fb)
+  qed
+  show "f \<bottom> \<sqsubseteq> \<mu> f"
+  proof -
+    have "f \<bottom> \<sqsubseteq> f (\<mu> f)"
+      by (auto intro: use_iso1[of _ f] simp add: assms)
+    moreover have "... .= \<mu> f"
+      using assms(1) assms(2) fps_def by force
+    moreover from assms(1) have "f (\<mu> f) \<in> carrier L"
+      by (auto)
+    ultimately show ?thesis
+      using fb by blast
+  qed
+qed
+
+
+subsubsection \<open>Greatest fixed points\<close>
+  
+lemma GFP_closed [intro, simp]:
+  "\<nu> f \<in> carrier L"
+  by (auto intro:sup_closed simp add:GFP_def)
+  
+lemma GFP_upperbound:
+  assumes "x \<in> carrier L" "x \<sqsubseteq> f x"
+  shows "x \<sqsubseteq> \<nu> f"
+  by (auto intro:sup_upper assms simp add:GFP_def)
+
+lemma GFP_least: 
+  assumes "x \<in> carrier L" 
+          "(\<And>u. \<lbrakk> u \<in> carrier L; u \<sqsubseteq> f u \<rbrakk> \<Longrightarrow> u \<sqsubseteq> x)"
+  shows "\<nu> f \<sqsubseteq> x"
+  by (auto simp add:GFP_def intro:sup_least assms)
+
+lemma GFP_lemma2:
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "\<nu> f \<sqsubseteq> f (\<nu> f)"
+  using assms
+  apply (auto simp add:Pi_def)
+  apply (rule GFP_least)
+  apply (metis GFP_closed)
+  apply (metis GFP_closed GFP_upperbound le_trans use_iso2)
+done
+
+lemma GFP_lemma3:
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "f (\<nu> f) \<sqsubseteq> \<nu> f"
+  by (metis GFP_closed GFP_lemma2 GFP_upperbound assms funcset_mem use_iso2)
+  
+lemma GFP_weak_unfold: 
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<nu> f .= f (\<nu> f)"
+  by (auto intro: GFP_lemma2 GFP_lemma3 funcset_mem)
+
+lemma (in weak_complete_lattice) GFP_fixed_point [intro]:
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "\<nu> f \<in> fps L f"
+  using assms
+proof -
+  have "f (\<nu> f) \<in> carrier L"
+    using assms(2) by blast
+  with assms show ?thesis
+    by (simp add: GFP_weak_unfold fps_def local.sym)
+qed
+
+lemma GFP_greatest_fixed_point:
+  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
+  shows "x \<sqsubseteq> \<nu> f"
+  using assms 
+  by (rule_tac GFP_upperbound, auto simp add: fps_def, meson PiE local.sym weak_refl)
+    
+lemma GFP_idem: 
+  assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
+  shows "\<nu> f .= (f \<top>)"
+proof (rule weak_le_antisym)
+  from assms(1) show fb: "f \<top> \<in> carrier L"
+    by (rule funcset_mem, simp)
+  from assms show mf: "\<nu> f \<in> carrier L"
+    by blast
+  show "f \<top> \<sqsubseteq> \<nu> f"
+  proof -
+    have "f (f \<top>) .= f \<top>"
+      by (auto simp add: fps_def fb assms(3) idempotent)
+    moreover have "f (f \<top>) \<in> carrier L"
+      by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
+    ultimately show ?thesis
+      by (rule_tac GFP_upperbound, simp_all add: fb local.sym)
+  qed
+  show "\<nu> f \<sqsubseteq> f \<top>"
+  proof -
+    have "\<nu> f \<sqsubseteq> f (\<nu> f)"
+      by (simp add: GFP_lemma2 assms(1) assms(2))
+    moreover have "... \<sqsubseteq> f \<top>"
+      by (auto intro: use_iso1[of _ f] simp add: assms)
+    moreover from assms(1) have "f (\<nu> f) \<in> carrier L"
+      by (auto)
+    ultimately show ?thesis
+      using fb local.le_trans by blast
+  qed
+qed
+
+end
+
+
+subsection \<open>Complete lattices where @{text eq} is the Equality\<close>
+
+locale complete_lattice = partial_order +
+  assumes sup_exists:
+    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
+    and inf_exists:
+    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
+
+sublocale complete_lattice \<subseteq> lattice
+proof
+  fix x y
+  assume a: "x \<in> carrier L" "y \<in> carrier L"
+  thus "\<exists>s. is_lub L s {x, y}"
+    by (rule_tac sup_exists[of "{x, y}"], auto)
+  from a show "\<exists>s. is_glb L s {x, y}"
+    by (rule_tac inf_exists[of "{x, y}"], auto)
+qed
+
+sublocale complete_lattice \<subseteq> weak?: weak_complete_lattice
+  by standard (auto intro: sup_exists inf_exists)
+
+lemma complete_lattice_lattice [simp]: 
+  assumes "complete_lattice X"
+  shows "lattice X"
+proof -
+  interpret c: complete_lattice X
+    by (simp add: assms)
+  show ?thesis
+    by (unfold_locales)
+qed
+
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
+
+lemma (in partial_order) complete_latticeI:
+  assumes sup_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
+    and inf_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
+  shows "complete_lattice L"
+  by standard (auto intro: sup_exists inf_exists)
+
+theorem (in partial_order) complete_lattice_criterion1:
+  assumes top_exists: "EX g. greatest L g (carrier L)"
+    and inf_exists:
+      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
+  shows "complete_lattice L"
+proof (rule complete_latticeI)
+  from top_exists obtain top where top: "greatest L top (carrier L)" ..
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  let ?B = "Upper L A"
+  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
+  then have B_non_empty: "?B ~= {}" by fast
+  have B_L: "?B \<subseteq> carrier L" by simp
+  from inf_exists [OF B_L B_non_empty]
+  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
+  have "least L b (Upper L A)"
+apply (rule least_UpperI)
+   apply (rule greatest_le [where A = "Lower L ?B"])
+    apply (rule b_inf_B)
+   apply (rule Lower_memI)
+    apply (erule Upper_memD [THEN conjunct1])
+     apply assumption
+    apply (rule L)
+   apply (fast intro: L [THEN subsetD])
+  apply (erule greatest_Lower_below [OF b_inf_B])
+  apply simp
+ apply (rule L)
+apply (rule greatest_closed [OF b_inf_B])
+done
+  then show "EX s. least L s (Upper L A)" ..
+next
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  show "EX i. greatest L i (Lower L A)"
+  proof (cases "A = {}")
+    case True then show ?thesis
+      by (simp add: top_exists)
+  next
+    case False with L show ?thesis
+      by (rule inf_exists)
+  qed
+qed
+
+(* TODO: prove dual version *)
+
+subsection \<open>Fixed points\<close>
+
+context complete_lattice
+begin
+
+lemma LFP_unfold: 
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<mu> f = f (\<mu> f)"
+  using eq_is_equal weak.LFP_weak_unfold by auto
+
+lemma LFP_const:
+  "t \<in> carrier L \<Longrightarrow> \<mu> (\<lambda> x. t) = t"
+  by (simp add: local.le_antisym weak.LFP_greatest weak.LFP_lowerbound)
+
+lemma LFP_id:
+  "\<mu> id = \<bottom>"
+  by (simp add: local.le_antisym weak.LFP_lowerbound)
+
+lemma GFP_unfold:
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<nu> f = f (\<nu> f)"
+  using eq_is_equal weak.GFP_weak_unfold by auto
+
+lemma GFP_const:
+  "t \<in> carrier L \<Longrightarrow> \<nu> (\<lambda> x. t) = t"
+  by (simp add: local.le_antisym weak.GFP_least weak.GFP_upperbound)
+
+lemma GFP_id:
+  "\<nu> id = \<top>"
+  using weak.GFP_upperbound by auto
+
+end
+
+
+subsection \<open>Interval complete lattices\<close>
+  
+context weak_complete_lattice
+begin
+
+  lemma at_least_at_most_Sup:
+    "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"
+    apply (rule weak_le_antisym)
+    apply (rule sup_least)
+    apply (auto simp add: at_least_at_most_closed)
+    apply (rule sup_upper)
+    apply (auto simp add: at_least_at_most_closed)
+  done
+
+  lemma at_least_at_most_Inf:
+    "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"
+    apply (rule weak_le_antisym)
+    apply (rule inf_lower)
+    apply (auto simp add: at_least_at_most_closed)
+    apply (rule inf_greatest)
+    apply (auto simp add: at_least_at_most_closed)
+  done
+
+end
+
+lemma weak_complete_lattice_interval:
+  assumes "weak_complete_lattice L" "a \<in> carrier L" "b \<in> carrier L" "a \<sqsubseteq>\<^bsub>L\<^esub> b"
+  shows "weak_complete_lattice (L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>)"
+proof -
+  interpret L: weak_complete_lattice L
+    by (simp add: assms)
+  interpret weak_partial_order "L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>"
+  proof -
+    have "\<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<subseteq> carrier L"
+      by (auto, simp add: at_least_at_most_def)
+    thus "weak_partial_order (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
+      by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
+  qed
+
+  show ?thesis
+  proof
+    fix A
+    assume a: "A \<subseteq> carrier (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
+    show "\<exists>s. is_lub (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
+    proof (cases "A = {}")
+      case True
+      thus ?thesis
+        by (rule_tac x="a" in exI, auto simp add: least_def assms)
+    next
+      case False
+      show ?thesis
+      proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)
+        show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
+          using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
+        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"
+          using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
+        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          by (auto)
+        from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          apply (rule_tac L.at_least_at_most_member)
+          apply (auto)
+          apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)
+          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)
+          apply (rule L.sup_least)
+          apply (auto simp add: assms)
+          using L.at_least_at_most_closed apply blast
+        done
+      qed
+    qed
+    show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
+    proof (cases "A = {}")
+      case True
+      thus ?thesis
+        by (rule_tac x="b" in exI, auto simp add: greatest_def assms)
+    next
+      case False
+      show ?thesis
+      proof (rule_tac x="\<Sqinter>\<^bsub>L\<^esub> A" in exI, rule greatest_LowerI, simp_all)
+        show b:"\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"
+          using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
+        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"
+           using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
+        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          by (auto)
+        from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          apply (rule_tac L.at_least_at_most_member)
+          apply (auto)
+          apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)
+          apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans)
+          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)            
+        done
+      qed
+    qed
+  qed
+qed
+
+
+subsection \<open>Knaster-Tarski theorem and variants\<close>
+  
+text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>
+
+theorem Knaster_Tarski:
+  assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"
+  shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
+proof -
+  interpret L: weak_complete_lattice L
+    by (simp add: assms)
+  interpret weak_partial_order ?L'
+  proof -
+    have "{x \<in> carrier L. f x .=\<^bsub>L\<^esub> x} \<subseteq> carrier L"
+      by (auto)
+    thus "weak_partial_order ?L'"
+      by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
+  qed
+  show ?thesis
+  proof (unfold_locales, simp_all)
+    fix A
+    assume A: "A \<subseteq> fps L f"
+    show "\<exists>s. is_lub (fpl L f) s A"
+    proof
+      from A have AL: "A \<subseteq> carrier L"
+        by (meson fps_carrier subset_eq)
+
+      let ?w = "\<Squnion>\<^bsub>L\<^esub> A"
+      have w: "f (\<Squnion>\<^bsub>L\<^esub>A) \<in> carrier L"
+        by (rule funcset_mem[of f "carrier L"], simp_all add: AL assms(2))
+
+      have pf_w: "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"
+        by (simp add: A L.weak_sup_pre_fixed_point assms(2) assms(3))
+
+      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>"
+      proof (auto simp add: at_least_at_most_def)
+        fix x
+        assume b: "x \<in> carrier L" "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"
+        from b show fx: "f x \<in> carrier L"
+          using assms(2) by blast
+        show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f x"
+        proof -
+          have "?w \<sqsubseteq>\<^bsub>L\<^esub> f ?w"
+          proof (rule_tac L.sup_least, simp_all add: AL w)
+            fix y
+            assume c: "y \<in> A" 
+            hence y: "y \<in> fps L f"
+              using A subsetCE by blast
+            with assms have "y .=\<^bsub>L\<^esub> f y"
+            proof -
+              from y have "y \<in> carrier L"
+                by (simp add: fps_def)
+              moreover hence "f y \<in> carrier L"
+                by (rule_tac funcset_mem[of f "carrier L"], simp_all add: assms)
+              ultimately show ?thesis using y
+                by (rule_tac L.sym, simp_all add: L.use_fps)
+            qed              
+            moreover have "y \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
+              by (simp add: AL L.sup_upper c(1))
+            ultimately show "y \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
+              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)
+          qed
+          thus ?thesis
+            by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) b(1) b(2) use_iso2)
+        qed
+   
+        show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>L\<^esub>"
+          by (simp add: fx)
+      qed
+  
+      let ?L' = "L\<lparr> carrier := \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rparr>"
+
+      interpret L': weak_complete_lattice ?L'
+        by (auto intro: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
+
+      let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
+
+      show "is_lub ?L'' (\<mu>\<^bsub>?L'\<^esub> f) A"
+      proof (rule least_UpperI, simp_all)
+        fix x
+        assume "x \<in> Upper ?L'' A"
+        hence "\<mu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
+          apply (rule_tac L'.LFP_lowerbound)
+          apply (auto simp add: Upper_def)
+          apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)          
+          apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)
+          apply (auto)
+          apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
+        done
+        thus " \<mu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
+          by (simp)
+      next
+        fix x
+        assume xA: "x \<in> A"
+        show "x \<sqsubseteq>\<^bsub>L\<^esub> \<mu>\<^bsub>?L'\<^esub> f"
+        proof -
+          have "\<mu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+            by blast
+          thus ?thesis
+            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)
+        qed
+      next
+        show "A \<subseteq> fps L f"
+          by (simp add: A)
+      next
+        show "\<mu>\<^bsub>?L'\<^esub> f \<in> fps L f"
+        proof (auto simp add: fps_def)
+          have "\<mu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+            by (rule L'.LFP_closed)
+          thus c:"\<mu>\<^bsub>?L'\<^esub> f \<in> carrier L"
+             by (auto simp add: at_least_at_most_def)
+          have "\<mu>\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (\<mu>\<^bsub>?L'\<^esub> f)"
+          proof (rule "L'.LFP_weak_unfold", simp_all)
+            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>"
+              apply (auto simp add: Pi_def at_least_at_most_def)
+              using assms(2) apply blast
+              apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
+              using assms(2) apply blast
+            done
+            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"
+              apply (auto simp add: isotone_def)
+              using L'.weak_partial_order_axioms apply blast
+              apply (meson L.at_least_at_most_closed subsetCE)
+            done
+          qed
+          thus "f (\<mu>\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> \<mu>\<^bsub>?L'\<^esub> f"
+            by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
+        qed
+      qed
+    qed
+    show "\<exists>i. is_glb (L\<lparr>carrier := fps L f\<rparr>) i A"
+    proof
+      from A have AL: "A \<subseteq> carrier L"
+        by (meson fps_carrier subset_eq)
+
+      let ?w = "\<Sqinter>\<^bsub>L\<^esub> A"
+      have w: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> carrier L"
+        by (simp add: AL funcset_carrier' assms(2))
+
+      have pf_w: "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"
+        by (simp add: A L.weak_sup_post_fixed_point assms(2) assms(3))
+
+      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>"
+      proof (auto simp add: at_least_at_most_def)
+        fix x
+        assume b: "x \<in> carrier L" "x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
+        from b show fx: "f x \<in> carrier L"
+          using assms(2) by blast
+        show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
+        proof -
+          have "f ?w \<sqsubseteq>\<^bsub>L\<^esub> ?w"
+          proof (rule_tac L.inf_greatest, simp_all add: AL w)
+            fix y
+            assume c: "y \<in> A" 
+            with assms have "y .=\<^bsub>L\<^esub> f y"
+              by (metis (no_types, lifting) A funcset_carrier'[OF assms(2)] L.sym fps_def mem_Collect_eq subset_eq)
+            moreover have "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
+              by (simp add: AL L.inf_lower c)
+            ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> y"
+              by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w)
+          qed
+          thus ?thesis
+            by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
+        qed
+   
+        show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"
+          by (simp add: fx)
+      qed
+  
+      let ?L' = "L\<lparr> carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rparr>"
+
+      interpret L': weak_complete_lattice ?L'
+        by (auto intro!: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
+
+      let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
+
+      show "is_glb ?L'' (\<nu>\<^bsub>?L'\<^esub> f) A"
+      proof (rule greatest_LowerI, simp_all)
+        fix x
+        assume "x \<in> Lower ?L'' A"
+        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
+          apply (rule_tac L'.GFP_upperbound)
+          apply (auto simp add: Lower_def)
+          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)
+          apply (simp add: funcset_carrier' L.sym assms(2) fps_def)          
+        done
+        thus "x \<sqsubseteq>\<^bsub>L\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
+          by (simp)
+      next
+        fix x
+        assume xA: "x \<in> A"
+        show "\<nu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
+        proof -
+          have "\<nu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+            by blast
+          thus ?thesis
+            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)     
+        qed
+      next
+        show "A \<subseteq> fps L f"
+          by (simp add: A)
+      next
+        show "\<nu>\<^bsub>?L'\<^esub> f \<in> fps L f"
+        proof (auto simp add: fps_def)
+          have "\<nu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+            by (rule L'.GFP_closed)
+          thus c:"\<nu>\<^bsub>?L'\<^esub> f \<in> carrier L"
+             by (auto simp add: at_least_at_most_def)
+          have "\<nu>\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (\<nu>\<^bsub>?L'\<^esub> f)"
+          proof (rule "L'.GFP_weak_unfold", simp_all)
+            show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
+              apply (auto simp add: Pi_def at_least_at_most_def)
+              using assms(2) apply blast
+              apply (simp add: funcset_carrier' assms(2))
+              apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
+            done
+            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
+              apply (auto simp add: isotone_def)
+              using L'.weak_partial_order_axioms apply blast
+              using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
+            done
+          qed
+          thus "f (\<nu>\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
+            by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
+        qed
+      qed
+    qed
+  qed
+qed
+
+theorem Knaster_Tarski_top:
+  assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> \<nu>\<^bsub>L\<^esub> f"
+proof -
+  interpret L: weak_complete_lattice L
+    by (simp add: assms)
+  interpret L': weak_complete_lattice "fpl L f"
+    by (rule Knaster_Tarski, simp_all add: assms)
+  show ?thesis
+  proof (rule L.weak_le_antisym, simp_all)
+    show "\<top>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> \<nu>\<^bsub>L\<^esub> f"
+      by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified])
+    show "\<nu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
+    proof -
+      have "\<nu>\<^bsub>L\<^esub> f \<in> fps L f"
+        by (rule L.GFP_fixed_point, simp_all add: assms)
+      hence "\<nu>\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
+        by simp
+      hence "\<nu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
+        by (rule L'.top_higher)
+      thus ?thesis
+        by simp
+    qed
+    show "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"
+    proof -
+      have "carrier (fpl L f) \<subseteq> carrier L"
+        by (auto simp add: fps_def)
+      with L'.top_closed show ?thesis
+        by blast
+    qed
+  qed
+qed
+
+theorem Knaster_Tarski_bottom:
+  assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
+  shows "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> \<mu>\<^bsub>L\<^esub> f"
+proof -
+  interpret L: weak_complete_lattice L
+    by (simp add: assms)
+  interpret L': weak_complete_lattice "fpl L f"
+    by (rule Knaster_Tarski, simp_all add: assms)
+  show ?thesis
+  proof (rule L.weak_le_antisym, simp_all)
+    show "\<mu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<bottom>\<^bsub>fpl L f\<^esub>"
+      by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified])
+    show "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> \<mu>\<^bsub>L\<^esub> f"
+    proof -
+      have "\<mu>\<^bsub>L\<^esub> f \<in> fps L f"
+        by (rule L.LFP_fixed_point, simp_all add: assms)
+      hence "\<mu>\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
+        by simp
+      hence "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<mu>\<^bsub>L\<^esub> f"
+        by (rule L'.bottom_lower)
+      thus ?thesis
+        by simp
+    qed
+    show "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"
+    proof -
+      have "carrier (fpl L f) \<subseteq> carrier L"
+        by (auto simp add: fps_def)
+      with L'.bottom_closed show ?thesis
+        by blast
+    qed
+  qed
+qed
+
+text \<open>If a function is both idempotent and isotone then the image of the function forms a complete lattice\<close>
+  
+theorem Knaster_Tarski_idem:
+  assumes "complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "idempotent L f"
+  shows "complete_lattice (L\<lparr>carrier := f ` carrier L\<rparr>)"
+proof -
+  interpret L: complete_lattice L
+    by (simp add: assms)
+  have "fps L f = f ` carrier L"
+    using L.weak.fps_idem[OF assms(2) assms(4)]
+    by (simp add: L.set_eq_is_eq)
+  then interpret L': weak_complete_lattice "(L\<lparr>carrier := f ` carrier L\<rparr>)"
+    by (metis Knaster_Tarski L.weak.weak_complete_lattice_axioms assms(2) assms(3))
+  show ?thesis
+    using L'.sup_exists L'.inf_exists
+    by (unfold_locales, auto simp add: L.eq_is_equal)
+qed
+
+theorem Knaster_Tarski_idem_extremes:
+  assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \<in> carrier L \<rightarrow> carrier L"
+  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>)"
+proof -
+  interpret L: weak_complete_lattice "L"
+    by (simp_all add: assms)
+  interpret L': weak_complete_lattice "fpl L f"
+    by (rule Knaster_Tarski, simp_all add: assms)
+  have FA: "fps L f \<subseteq> carrier L"
+    by (auto simp add: fps_def)
+  show "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<top>\<^bsub>L\<^esub>)"
+  proof -
+    from FA have "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"
+    proof -
+      have "\<top>\<^bsub>fpl L f\<^esub> \<in> fps L f"
+        using L'.top_closed by auto
+      thus ?thesis
+        using FA by blast
+    qed
+    moreover with assms have "f \<top>\<^bsub>L\<^esub> \<in> carrier L"
+      by (auto)
+
+    ultimately show ?thesis
+      using L.trans[OF Knaster_Tarski_top[of L f] L.GFP_idem[of f]]
+      by (simp_all add: assms)
+  qed
+  show "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<bottom>\<^bsub>L\<^esub>)"
+  proof -
+    from FA have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"
+    proof -
+      have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> fps L f"
+        using L'.bottom_closed by auto
+      thus ?thesis
+        using FA by blast
+    qed
+    moreover with assms have "f \<bottom>\<^bsub>L\<^esub> \<in> carrier L"
+      by (auto)
+
+    ultimately show ?thesis
+      using L.trans[OF Knaster_Tarski_bottom[of L f] L.LFP_idem[of f]]
+      by (simp_all add: assms)
+  qed
+qed
+
+
+subsection \<open>Examples\<close>
+
+subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
+
+theorem powerset_is_complete_lattice:
+  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
+  (is "complete_lattice ?L")
+proof (rule partial_order.complete_latticeI)
+  show "partial_order ?L"
+    by standard auto
+next
+  fix B
+  assume "B \<subseteq> carrier ?L"
+  then have "least ?L (\<Union> B) (Upper ?L B)"
+    by (fastforce intro!: least_UpperI simp: Upper_def)
+  then show "EX s. least ?L s (Upper ?L B)" ..
+next
+  fix B
+  assume "B \<subseteq> carrier ?L"
+  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
+    txt \<open>@{term "\<Inter> B"} is not the infimum of @{term B}:
+      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! \<close>
+    by (fastforce intro!: greatest_LowerI simp: Lower_def)
+  then show "EX i. greatest ?L i (Lower ?L B)" ..
+qed
+
+text \<open>Another example, that of the lattice of subgroups of a group,
+  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
+
+
+subsection \<open>Limit preserving functions\<close>
+
+definition weak_sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+"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)))"
+
+definition sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+"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)))"
+
+definition weak_inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+"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)))"
+
+definition inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+"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)))"
+
+lemma weak_sup_pres:
+  "sup_pres X Y f \<Longrightarrow> weak_sup_pres X Y f"
+  by (simp add: sup_pres_def weak_sup_pres_def)
+
+lemma weak_inf_pres:
+  "inf_pres X Y f \<Longrightarrow> weak_inf_pres X Y f"
+  by (simp add: inf_pres_def weak_inf_pres_def)
+
+lemma sup_pres_is_join_pres:
+  assumes "weak_sup_pres X Y f"
+  shows "join_pres X Y f"
+  using assms
+  apply (simp add: join_pres_def weak_sup_pres_def, safe)
+  apply (rename_tac x y)
+  apply (drule_tac x="{x, y}" in spec)
+  apply (auto simp add: join_def)
+done
+
+lemma inf_pres_is_meet_pres:
+  assumes "weak_inf_pres X Y f"
+  shows "meet_pres X Y f"
+  using assms
+  apply (simp add: meet_pres_def weak_inf_pres_def, safe)
+  apply (rename_tac x y)
+  apply (drule_tac x="{x, y}" in spec)
+  apply (auto simp add: meet_def)
+done
+
+end
diff -r b47ba1778e44 -r 30d0b2f1df76 src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Fri Mar 03 23:21:24 2017 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Thu Mar 02 21:16:02 2017 +0100
@@ -4,7 +4,9 @@
 *)
 
 theory Congruence
-imports Main
+imports 
+  Main
+  "~~/src/HOL/Library/FuncSet"
 begin
 
 section \<open>Objects\<close>
@@ -14,6 +16,14 @@
 record 'a partial_object =
   carrier :: "'a set"
 
+lemma funcset_carrier:
+  "\<lbrakk> f \<in> carrier X \<rightarrow> carrier Y; x \<in> carrier X \<rbrakk> \<Longrightarrow> f x \<in> carrier Y"
+  by (fact funcset_mem)
+
+lemma funcset_carrier':
+  "\<lbrakk> f \<in> carrier A \<rightarrow> carrier A; x \<in> carrier A \<rbrakk> \<Longrightarrow> f x \<in> carrier A"
+  by (fact funcset_mem)
+
 
 subsection \<open>Structure with Carrier and Equivalence Relation \<open>eq\<close>\<close>
 
@@ -413,4 +423,14 @@
 by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
 *)
 
+lemma equivalence_subset:
+  assumes "equivalence L" "A \<subseteq> carrier L"
+  shows "equivalence (L\<lparr> carrier := A \<rparr>)"
+proof -
+  interpret L: equivalence L
+    by (simp add: assms)
+  show ?thesis
+    by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD)
+qed
+  
 end
diff -r b47ba1778e44 -r 30d0b2f1df76 src/HOL/Algebra/Galois_Connection.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Galois_Connection.thy	Thu Mar 02 21:16:02 2017 +0100
@@ -0,0 +1,422 @@
+(*  Title:      HOL/Algebra/Galois_Connection.thy
+    Author:     Alasdair Armstrong and Simon Foster
+    Copyright:  Alasdair Armstrong and Simon Foster
+*)
+
+theory Galois_Connection
+  imports Complete_Lattice
+begin
+
+section \<open>Galois connections\<close>
+
+subsection \<open>Definition and basic properties\<close>
+
+record ('a, 'b, 'c, 'd) galcon =
+  orderA :: "('a, 'c) gorder_scheme" ("\<X>\<index>")
+  orderB :: "('b, 'd) gorder_scheme" ("\<Y>\<index>")
+  lower  :: "'a \<Rightarrow> 'b" ("\<pi>\<^sup>*\<index>")
+  upper  :: "'b \<Rightarrow> 'a" ("\<pi>\<^sub>*\<index>")
+
+type_synonym ('a, 'b) galois = "('a, 'b, unit, unit) galcon"
+
+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>"
+
+definition comp_galcon :: "('b, 'c) galois \<Rightarrow> ('a, 'b) galois \<Rightarrow> ('a, 'c) galois" (infixr "\<circ>\<^sub>g" 85)
+  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>"
+
+definition id_galcon :: "'a gorder \<Rightarrow> ('a, 'a) galois" ("I\<^sub>g") where
+"I\<^sub>g(A) = \<lparr> orderA = A, orderB = A, lower = id, upper = id \<rparr>"
+
+
+subsection \<open>Well-typed connections\<close>
+
+locale connection =
+  fixes G (structure)
+  assumes is_order_A: "partial_order \<X>"
+  and is_order_B: "partial_order \<Y>"
+  and lower_closure: "\<pi>\<^sup>* \<in> carrier \<X> \<rightarrow> carrier \<Y>"
+  and upper_closure: "\<pi>\<^sub>* \<in> carrier \<Y> \<rightarrow> carrier \<X>"
+begin
+
+  lemma lower_closed: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* x \<in> carrier \<Y>"
+    using lower_closure by auto
+
+  lemma upper_closed: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* y \<in> carrier \<X>"
+    using upper_closure by auto
+
+end
+
+
+subsection \<open>Galois connections\<close>
+  
+locale galois_connection = connection +
+  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"
+begin
+
+  lemma is_weak_order_A: "weak_partial_order \<X>"
+  proof -
+    interpret po: partial_order \<X>
+      by (metis is_order_A)
+    show ?thesis ..
+  qed
+
+  lemma is_weak_order_B: "weak_partial_order \<Y>"
+  proof -
+    interpret po: partial_order \<Y>
+      by (metis is_order_B)
+    show ?thesis ..
+  qed
+
+  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"
+    by (metis galois_property)
+
+  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"
+    by (metis galois_property)
+
+  lemma deflation: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
+    by (metis Pi_iff is_weak_order_A left upper_closure weak_partial_order.le_refl)
+
+  lemma inflation: "x \<in> carrier \<X> \<Longrightarrow> x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* x)"
+    by (metis (no_types, lifting) PiE galois_connection.right galois_connection_axioms is_weak_order_B lower_closure weak_partial_order.le_refl)
+
+  lemma lower_iso: "isotone \<X> \<Y> \<pi>\<^sup>*"
+  proof (auto simp add:isotone_def)
+    show "weak_partial_order \<X>"
+      by (metis is_weak_order_A)
+    show "weak_partial_order \<Y>"
+      by (metis is_weak_order_B)
+    fix x y
+    assume a: "x \<in> carrier \<X>" "y \<in> carrier \<X>" "x \<sqsubseteq>\<^bsub>\<X>\<^esub> y"
+    have b: "\<pi>\<^sup>* y \<in> carrier \<Y>"
+      using a(2) lower_closure by blast
+    then have "\<pi>\<^sub>* (\<pi>\<^sup>* y) \<in> carrier \<X>"
+      using upper_closure by blast
+    then have "x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* y)"
+      by (meson a inflation is_weak_order_A weak_partial_order.le_trans)
+    thus "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* y"
+      by (meson b a(1) Pi_iff galois_property lower_closure upper_closure)
+  qed
+
+  lemma upper_iso: "isotone \<Y> \<X> \<pi>\<^sub>*"
+    apply (auto simp add:isotone_def)
+    apply (metis is_weak_order_B)
+    apply (metis is_weak_order_A)
+    apply (metis (no_types, lifting) Pi_mem deflation is_weak_order_B lower_closure right upper_closure weak_partial_order.le_trans)
+  done
+
+  lemma lower_comp: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* (\<pi>\<^sup>* x)) = \<pi>\<^sup>* x"
+    by (meson deflation funcset_mem inflation is_order_B lower_closure lower_iso partial_order.le_antisym upper_closure use_iso2)
+
+  lemma lower_comp': "x \<in> carrier \<X> \<Longrightarrow> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>* \<circ> \<pi>\<^sup>*) x = \<pi>\<^sup>* x"
+    by (simp add: lower_comp)
+
+  lemma upper_comp: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) = \<pi>\<^sub>* y"
+  proof -
+    assume a1: "y \<in> carrier \<Y>"
+    hence f1: "\<pi>\<^sub>* y \<in> carrier \<X>" using upper_closure by blast 
+    have f2: "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y" using a1 deflation by blast
+    have f3: "\<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) \<in> carrier \<X>"
+      using f1 lower_closure upper_closure by auto 
+    have "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<in> carrier \<Y>" using f1 lower_closure by blast   
+    thus "\<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* y)) = \<pi>\<^sub>* y"
+      by (meson a1 f1 f2 f3 inflation is_order_A partial_order.le_antisym upper_iso use_iso2) 
+  qed
+
+  lemma upper_comp': "y \<in> carrier \<Y> \<Longrightarrow> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>* \<circ> \<pi>\<^sub>*) y = \<pi>\<^sub>* y"
+    by (simp add: upper_comp)
+
+  lemma adjoint_idem1: "idempotent \<Y> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>*)"
+    by (simp add: idempotent_def is_order_B partial_order.eq_is_equal upper_comp)
+
+  lemma adjoint_idem2: "idempotent \<X> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>*)"
+    by (simp add: idempotent_def is_order_A partial_order.eq_is_equal lower_comp)
+
+  lemma fg_iso: "isotone \<Y> \<Y> (\<pi>\<^sup>* \<circ> \<pi>\<^sub>*)"
+    by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)
+
+  lemma gf_iso: "isotone \<X> \<X> (\<pi>\<^sub>* \<circ> \<pi>\<^sup>*)"
+    by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)
+
+  lemma semi_inverse1: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sup>* x = \<pi>\<^sup>* (\<pi>\<^sub>* (\<pi>\<^sup>* x))"
+    by (metis lower_comp)
+
+  lemma semi_inverse2: "x \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sub>* x = \<pi>\<^sub>* (\<pi>\<^sup>* (\<pi>\<^sub>* x))"
+    by (metis upper_comp)
+
+  theorem lower_by_complete_lattice:
+    assumes "complete_lattice \<Y>" "x \<in> carrier \<X>"
+    shows "\<pi>\<^sup>*(x) = \<Sqinter>\<^bsub>\<Y>\<^esub> { y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>*(y) }"
+  proof -
+    interpret Y: complete_lattice \<Y>
+      by (simp add: assms)
+
+    show ?thesis
+    proof (rule Y.le_antisym)
+      show x: "\<pi>\<^sup>* x \<in> carrier \<Y>"
+        using assms(2) lower_closure by blast
+      show "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}"
+      proof (rule Y.weak.inf_greatest)
+        show "{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<subseteq> carrier \<Y>"
+          by auto
+        show "\<pi>\<^sup>* x \<in> carrier \<Y>" by (fact x)
+        fix z
+        assume "z \<in> {y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}" 
+        thus "\<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> z"
+          using assms(2) left by auto
+      qed
+      show "\<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* x"
+      proof (rule Y.weak.inf_lower)
+        show "{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<subseteq> carrier \<Y>"
+          by auto
+        show "\<pi>\<^sup>* x \<in> {y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y}"
+        proof (auto)
+          show "\<pi>\<^sup>* x \<in> carrier \<Y>" by (fact x)
+          show "x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* (\<pi>\<^sup>* x)"
+            using assms(2) inflation by blast
+        qed
+      qed
+      show "\<Sqinter>\<^bsub>\<Y>\<^esub>{y \<in> carrier \<Y>. x \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y} \<in> carrier \<Y>"
+       by (auto intro: Y.weak.inf_closed)
+    qed
+  qed
+
+  theorem upper_by_complete_lattice:
+    assumes "complete_lattice \<X>" "y \<in> carrier \<Y>"
+    shows "\<pi>\<^sub>*(y) = \<Squnion>\<^bsub>\<X>\<^esub> { x \<in> carrier \<X>. \<pi>\<^sup>*(x) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y }"
+  proof -
+    interpret X: complete_lattice \<X>
+      by (simp add: assms)
+    show ?thesis
+    proof (rule X.le_antisym)
+      show y: "\<pi>\<^sub>* y \<in> carrier \<X>"
+        using assms(2) upper_closure by blast
+      show "\<pi>\<^sub>* y \<sqsubseteq>\<^bsub>\<X>\<^esub> \<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}"
+      proof (rule X.weak.sup_upper)
+        show "{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<subseteq> carrier \<X>"
+          by auto
+        show "\<pi>\<^sub>* y \<in> {x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}"
+        proof (auto)
+          show "\<pi>\<^sub>* y \<in> carrier \<X>" by (fact y)
+          show "\<pi>\<^sup>* (\<pi>\<^sub>* y) \<sqsubseteq>\<^bsub>\<Y>\<^esub> y"
+            by (simp add: assms(2) deflation)
+        qed
+      qed
+      show "\<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
+      proof (rule X.weak.sup_least)
+        show "{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<subseteq> carrier \<X>"
+          by auto
+        show "\<pi>\<^sub>* y \<in> carrier \<X>" by (fact y)
+        fix z
+        assume "z \<in> {x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y}" 
+        thus "z \<sqsubseteq>\<^bsub>\<X>\<^esub> \<pi>\<^sub>* y"
+          by (simp add: assms(2) right)
+      qed
+      show "\<Squnion>\<^bsub>\<X>\<^esub>{x \<in> carrier \<X>. \<pi>\<^sup>* x \<sqsubseteq>\<^bsub>\<Y>\<^esub> y} \<in> carrier \<X>"
+       by (auto intro: X.weak.sup_closed)
+    qed
+  qed
+
+end
+
+lemma dual_galois [simp]: " galois_connection \<lparr> orderA = inv_gorder B, orderB = inv_gorder A, lower = f, upper = g \<rparr> 
+                          = galois_connection \<lparr> orderA = A, orderB = B, lower = g, upper = f \<rparr>"
+  by (auto simp add: galois_connection_def galois_connection_axioms_def connection_def dual_order_iff)
+
+definition lower_adjoint :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+  "lower_adjoint A B f \<equiv> \<exists>g. galois_connection \<lparr> orderA = A, orderB = B, lower = f, upper = g \<rparr>"
+
+definition upper_adjoint :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool" where
+  "upper_adjoint A B g \<equiv> \<exists>f. galois_connection \<lparr> orderA = A, orderB = B, lower = f, upper = g \<rparr>"
+
+lemma lower_adjoint_dual [simp]: "lower_adjoint (inv_gorder A) (inv_gorder B) f = upper_adjoint B A f"
+  by (simp add: lower_adjoint_def upper_adjoint_def)
+
+lemma upper_adjoint_dual [simp]: "upper_adjoint (inv_gorder A) (inv_gorder B) f = lower_adjoint B A f"
+  by (simp add: lower_adjoint_def upper_adjoint_def)
+
+lemma lower_type: "lower_adjoint A B f \<Longrightarrow> f \<in> carrier A \<rightarrow> carrier B"
+  by (auto simp add:lower_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)
+
+lemma upper_type: "upper_adjoint A B g \<Longrightarrow> g \<in> carrier B \<rightarrow> carrier A"
+  by (auto simp add:upper_adjoint_def galois_connection_def galois_connection_axioms_def connection_def)
+
+
+subsection \<open>Composition of Galois connections\<close>
+
+lemma id_galois: "partial_order A \<Longrightarrow> galois_connection (I\<^sub>g(A))"
+  by (simp add: id_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
+
+lemma comp_galcon_closed:
+  assumes "galois_connection G" "galois_connection F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
+  shows "galois_connection (G \<circ>\<^sub>g F)"
+proof -
+  interpret F: galois_connection F
+    by (simp add: assms)
+  interpret G: galois_connection G
+    by (simp add: assms)
+  
+  have "partial_order \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
+    by (simp add: F.is_order_A comp_galcon_def)
+  moreover have "partial_order \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
+    by (simp add: G.is_order_B comp_galcon_def)
+  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>"
+    using F.lower_closure G.lower_closure assms(3) by auto
+  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>"
+    using F.upper_closure G.upper_closure assms(3) by auto
+  moreover 
+  have "\<And> x y. \<lbrakk>x \<in> carrier \<X>\<^bsub>F\<^esub>; y \<in> carrier \<Y>\<^bsub>G\<^esub> \<rbrakk> \<Longrightarrow> 
+               (\<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))"
+    by (metis F.galois_property F.lower_closure G.galois_property G.upper_closure assms(3) Pi_iff)
+  ultimately show ?thesis
+    by (simp add: comp_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
+qed
+
+lemma comp_galcon_right_unit [simp]: "F \<circ>\<^sub>g I\<^sub>g(\<X>\<^bsub>F\<^esub>) = F"
+  by (simp add: comp_galcon_def id_galcon_def)
+
+lemma comp_galcon_left_unit [simp]: "I\<^sub>g(\<Y>\<^bsub>F\<^esub>) \<circ>\<^sub>g F = F"
+  by (simp add: comp_galcon_def id_galcon_def)
+
+lemma galois_connectionI:
+  assumes
+    "partial_order A" "partial_order B"
+    "L \<in> carrier A \<rightarrow> carrier B" "R \<in> carrier B \<rightarrow> carrier A"
+    "isotone A B L" "isotone B A R" 
+    "\<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"
+  shows "galois_connection \<lparr> orderA = A, orderB = B, lower = L, upper = R \<rparr>"
+  using assms by (simp add: galois_connection_def connection_def galois_connection_axioms_def)
+
+lemma galois_connectionI':
+  assumes
+    "partial_order A" "partial_order B"
+    "L \<in> carrier A \<rightarrow> carrier B" "R \<in> carrier B \<rightarrow> carrier A"
+    "isotone A B L" "isotone B A R" 
+    "\<And> X. X \<in> carrier(B) \<Longrightarrow> L(R(X)) \<sqsubseteq>\<^bsub>B\<^esub> X"
+    "\<And> X. X \<in> carrier(A) \<Longrightarrow> X \<sqsubseteq>\<^bsub>A\<^esub> R(L(X))"
+  shows "galois_connection \<lparr> orderA = A, orderB = B, lower = L, upper = R \<rparr>"
+  using assms
+  by (auto simp add: galois_connection_def connection_def galois_connection_axioms_def, (meson PiE isotone_def weak_partial_order.le_trans)+)
+
+
+subsection \<open>Retracts\<close>
+
+locale retract = galois_connection +
+  assumes retract_property: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) \<sqsubseteq>\<^bsub>\<X>\<^esub> x"
+begin
+  lemma retract_inverse: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) = x"
+    by (meson funcset_mem inflation is_order_A lower_closure partial_order.le_antisym retract_axioms retract_axioms_def retract_def upper_closure)
+
+  lemma retract_injective: "inj_on \<pi>\<^sup>* (carrier \<X>)"
+    by (metis inj_onI retract_inverse)
+end  
+
+theorem comp_retract_closed:
+  assumes "retract G" "retract F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
+  shows "retract (G \<circ>\<^sub>g F)"
+proof -
+  interpret f: retract F
+    by (simp add: assms)
+  interpret g: retract G
+    by (simp add: assms)
+  interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
+    by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed retract.axioms(1))
+  show ?thesis
+  proof
+    fix x
+    assume "x \<in> carrier \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
+    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"
+      using assms(3) f.inflation f.lower_closed f.retract_inverse g.retract_inverse by (auto simp add: comp_galcon_def)
+  qed
+qed
+
+
+subsection \<open>Coretracts\<close>
+  
+locale coretract = galois_connection +
+  assumes coretract_property: "y \<in> carrier \<Y> \<Longrightarrow> y \<sqsubseteq>\<^bsub>\<Y>\<^esub> \<pi>\<^sup>* (\<pi>\<^sub>* y)"
+begin
+  lemma coretract_inverse: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) = y"
+    by (meson coretract_axioms coretract_axioms_def coretract_def deflation funcset_mem is_order_B lower_closure partial_order.le_antisym upper_closure)
+ 
+  lemma retract_injective: "inj_on \<pi>\<^sub>* (carrier \<Y>)"
+    by (metis coretract_inverse inj_onI)
+end  
+
+theorem comp_coretract_closed:
+  assumes "coretract G" "coretract F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
+  shows "coretract (G \<circ>\<^sub>g F)"
+proof -
+  interpret f: coretract F
+    by (simp add: assms)
+  interpret g: coretract G
+    by (simp add: assms)
+  interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
+    by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed coretract.axioms(1))
+  show ?thesis
+  proof
+    fix y
+    assume "y \<in> carrier \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
+    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))"
+      by (simp add: comp_galcon_def assms(3) f.coretract_inverse g.coretract_property g.upper_closed)
+  qed
+qed
+
+
+subsection \<open>Galois Bijections\<close>
+  
+locale galois_bijection = connection +
+  assumes lower_iso: "isotone \<X> \<Y> \<pi>\<^sup>*" 
+  and upper_iso: "isotone \<Y> \<X> \<pi>\<^sub>*"
+  and lower_inv_eq: "x \<in> carrier \<X> \<Longrightarrow> \<pi>\<^sub>* (\<pi>\<^sup>* x) = x"
+  and upper_inv_eq: "y \<in> carrier \<Y> \<Longrightarrow> \<pi>\<^sup>* (\<pi>\<^sub>* y) = y"
+begin
+
+  lemma lower_bij: "bij_betw \<pi>\<^sup>* (carrier \<X>) (carrier \<Y>)"
+    by (rule bij_betwI[where g="\<pi>\<^sub>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)  
+
+  lemma upper_bij: "bij_betw \<pi>\<^sub>* (carrier \<Y>) (carrier \<X>)"
+    by (rule bij_betwI[where g="\<pi>\<^sup>*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)  
+
+sublocale gal_bij_conn: galois_connection
+  apply (unfold_locales, auto)
+  using lower_closed lower_inv_eq upper_iso use_iso2 apply fastforce
+  using lower_iso upper_closed upper_inv_eq use_iso2 apply fastforce
+done
+
+sublocale gal_bij_ret: retract
+  by (unfold_locales, simp add: gal_bij_conn.is_weak_order_A lower_inv_eq weak_partial_order.le_refl)
+
+sublocale gal_bij_coret: coretract
+  by (unfold_locales, simp add: gal_bij_conn.is_weak_order_B upper_inv_eq weak_partial_order.le_refl)
+
+end
+
+theorem comp_galois_bijection_closed:
+  assumes "galois_bijection G" "galois_bijection F" "\<Y>\<^bsub>F\<^esub> = \<X>\<^bsub>G\<^esub>"
+  shows "galois_bijection (G \<circ>\<^sub>g F)"
+proof -
+  interpret f: galois_bijection F
+    by (simp add: assms)
+  interpret g: galois_bijection G
+    by (simp add: assms)
+  interpret gf: galois_connection "(G \<circ>\<^sub>g F)"
+    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))
+  show ?thesis
+  proof
+    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>"
+      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)
+    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>"
+      by (simp add: gf.upper_iso)
+    fix x
+    assume "x \<in> carrier \<X>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
+    thus "\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> x) = x"
+      using assms(3) f.lower_closed f.lower_inv_eq g.lower_inv_eq by (auto simp add: comp_galcon_def)
+  next
+    fix y
+    assume "y \<in> carrier \<Y>\<^bsub>G \<circ>\<^sub>g F\<^esub>"
+    thus "\<pi>\<^sup>*\<^bsub>G \<circ>\<^sub>g F\<^esub> (\<pi>\<^sub>*\<^bsub>G \<circ>\<^sub>g F\<^esub> y) = y"
+      by (simp add: comp_galcon_def assms(3) f.upper_inv_eq g.upper_closed g.upper_inv_eq)
+  qed
+qed
+
+end
diff -r b47ba1778e44 -r 30d0b2f1df76 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Mar 03 23:21:24 2017 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Mar 02 21:16:02 2017 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory Group
-imports Lattice "~~/src/HOL/Library/FuncSet"
+imports Complete_Lattice "~~/src/HOL/Library/FuncSet"
 begin
 
 section \<open>Monoids and Groups\<close>
diff -r b47ba1778e44 -r 30d0b2f1df76 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Mar 03 23:21:24 2017 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Thu Mar 02 21:16:02 2017 +0100
@@ -3,406 +3,16 @@
     Copyright:  Clemens Ballarin
 
 Most congruence rules by Stephan Hohe.
+With additional contributions from Alasdair Armstrong and Simon Foster.
 *)
 
 theory Lattice
-imports Congruence
-begin
-
-section \<open>Orders and Lattices\<close>
-
-subsection \<open>Partial Orders\<close>
-
-record 'a gorder = "'a eq_object" +
-  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
-
-locale weak_partial_order = equivalence L for L (structure) +
-  assumes le_refl [intro, simp]:
-      "x \<in> carrier L ==> x \<sqsubseteq> x"
-    and weak_le_antisym [intro]:
-      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
-    and le_trans [trans]:
-      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
-    and le_cong:
-      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
-      x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
-
-definition
-  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
-  where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
-
-
-subsubsection \<open>The order relation\<close>
-
-context weak_partial_order
+imports Order
 begin
 
-lemma le_cong_l [intro, trans]:
-  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-  by (auto intro: le_cong [THEN iffD2])
-
-lemma le_cong_r [intro, trans]:
-  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-  by (auto intro: le_cong [THEN iffD1])
-
-lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
-  by (simp add: le_cong_l)
-
-end
-
-lemma weak_llessI:
-  fixes R (structure)
-  assumes "x \<sqsubseteq> y" and "~(x .= y)"
-  shows "x \<sqsubset> y"
-  using assms unfolding lless_def by simp
-
-lemma lless_imp_le:
-  fixes R (structure)
-  assumes "x \<sqsubset> y"
-  shows "x \<sqsubseteq> y"
-  using assms unfolding lless_def by simp
-
-lemma weak_lless_imp_not_eq:
-  fixes R (structure)
-  assumes "x \<sqsubset> y"
-  shows "\<not> (x .= y)"
-  using assms unfolding lless_def by simp
-
-lemma weak_llessE:
-  fixes R (structure)
-  assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
-  shows "P"
-  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
-
-lemma (in weak_partial_order) lless_cong_l [trans]:
-  assumes xx': "x .= x'"
-    and xy: "x' \<sqsubset> y"
-    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
-  shows "x \<sqsubset> y"
-  using assms unfolding lless_def by (auto intro: trans sym)
-
-lemma (in weak_partial_order) lless_cong_r [trans]:
-  assumes xy: "x \<sqsubset> y"
-    and  yy': "y .= y'"
-    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
-  shows "x \<sqsubset> y'"
-  using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
-
-
-lemma (in weak_partial_order) lless_antisym:
-  assumes "a \<in> carrier L" "b \<in> carrier L"
-    and "a \<sqsubset> b" "b \<sqsubset> a"
-  shows "P"
-  using assms
-  by (elim weak_llessE) auto
-
-lemma (in weak_partial_order) lless_trans [trans]:
-  assumes "a \<sqsubset> b" "b \<sqsubset> c"
-    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
-  shows "a \<sqsubset> c"
-  using assms unfolding lless_def by (blast dest: le_trans intro: sym)
-
-
-subsubsection \<open>Upper and lower bounds of a set\<close>
-
-definition
-  Upper :: "[_, 'a set] => 'a set"
-  where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
-
-definition
-  Lower :: "[_, 'a set] => 'a set"
-  where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
-
-lemma Upper_closed [intro!, simp]:
-  "Upper L A \<subseteq> carrier L"
-  by (unfold Upper_def) clarify
-
-lemma Upper_memD [dest]:
-  fixes L (structure)
-  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
-  by (unfold Upper_def) blast
-
-lemma (in weak_partial_order) Upper_elemD [dest]:
-  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
-  unfolding Upper_def elem_def
-  by (blast dest: sym)
-
-lemma Upper_memI:
-  fixes L (structure)
-  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
-  by (unfold Upper_def) blast
-
-lemma (in weak_partial_order) Upper_elemI:
-  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
-  unfolding Upper_def by blast
-
-lemma Upper_antimono:
-  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
-  by (unfold Upper_def) blast
-
-lemma (in weak_partial_order) Upper_is_closed [simp]:
-  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
-  by (rule is_closedI) (blast intro: Upper_memI)+
-
-lemma (in weak_partial_order) Upper_mem_cong:
-  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
-    and aa': "a .= a'"
-    and aelem: "a \<in> Upper L A"
-  shows "a' \<in> Upper L A"
-proof (rule Upper_memI[OF _ a'carr])
-  fix y
-  assume yA: "y \<in> A"
-  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
-  also note aa'
-  finally
-      show "y \<sqsubseteq> a'"
-      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
-qed
-
-lemma (in weak_partial_order) Upper_cong:
-  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
-    and AA': "A {.=} A'"
-  shows "Upper L A = Upper L A'"
-unfolding Upper_def
-apply rule
- apply (rule, clarsimp) defer 1
- apply (rule, clarsimp) defer 1
-proof -
-  fix x a'
-  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
-    and a'A': "a' \<in> A'"
-  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
-
-  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
-  from this obtain a
-      where aA: "a \<in> A"
-      and a'a: "a' .= a"
-      by auto
-  note [simp] = subsetD[OF Acarr aA] carr
-
-  note a'a
-  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
-  finally show "a' \<sqsubseteq> x" by simp
-next
-  fix x a
-  assume carr: "x \<in> carrier L" "a \<in> carrier L"
-    and aA: "a \<in> A"
-  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
-
-  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
-  from this obtain a'
-      where a'A': "a' \<in> A'"
-      and aa': "a .= a'"
-      by auto
-  note [simp] = subsetD[OF A'carr a'A'] carr
-
-  note aa'
-  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
-  finally show "a \<sqsubseteq> x" by simp
-qed
-
-lemma Lower_closed [intro!, simp]:
-  "Lower L A \<subseteq> carrier L"
-  by (unfold Lower_def) clarify
-
-lemma Lower_memD [dest]:
-  fixes L (structure)
-  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
-  by (unfold Lower_def) blast
-
-lemma Lower_memI:
-  fixes L (structure)
-  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
-  by (unfold Lower_def) blast
-
-lemma Lower_antimono:
-  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
-  by (unfold Lower_def) blast
-
-lemma (in weak_partial_order) Lower_is_closed [simp]:
-  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
-  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
-
-lemma (in weak_partial_order) Lower_mem_cong:
-  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
-    and aa': "a .= a'"
-    and aelem: "a \<in> Lower L A"
-  shows "a' \<in> Lower L A"
-using assms Lower_closed[of L A]
-by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
-
-lemma (in weak_partial_order) Lower_cong:
-  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
-    and AA': "A {.=} A'"
-  shows "Lower L A = Lower L A'"
-unfolding Lower_def
-apply rule
- apply clarsimp defer 1
- apply clarsimp defer 1
-proof -
-  fix x a'
-  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
-    and a'A': "a' \<in> A'"
-  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
-  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
-
-  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
-  from this obtain a
-      where aA: "a \<in> A"
-      and a'a: "a' .= a"
-      by auto
-
-  from aA and subsetD[OF Acarr aA]
-      have "x \<sqsubseteq> a" by (rule aLxCond)
-  also note a'a[symmetric]
-  finally
-      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
-next
-  fix x a
-  assume carr: "x \<in> carrier L" "a \<in> carrier L"
-    and aA: "a \<in> A"
-  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
-  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
-
-  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
-  from this obtain a'
-      where a'A': "a' \<in> A'"
-      and aa': "a .= a'"
-      by auto
-  from a'A' and subsetD[OF A'carr a'A']
-      have "x \<sqsubseteq> a'" by (rule a'LxCond)
-  also note aa'[symmetric]
-  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
-qed
-
-
-subsubsection \<open>Least and greatest, as predicate\<close>
-
-definition
-  least :: "[_, 'a, 'a set] => bool"
-  where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
-
-definition
-  greatest :: "[_, 'a, 'a set] => bool"
-  where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
-
-text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
-  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
-
-lemma least_closed [intro, simp]:
-  "least L l A ==> l \<in> carrier L"
-  by (unfold least_def) fast
-
-lemma least_mem:
-  "least L l A ==> l \<in> A"
-  by (unfold least_def) fast
-
-lemma (in weak_partial_order) weak_least_unique:
-  "[| least L x A; least L y A |] ==> x .= y"
-  by (unfold least_def) blast
-
-lemma least_le:
-  fixes L (structure)
-  shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
-  by (unfold least_def) fast
-
-lemma (in weak_partial_order) least_cong:
-  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
-  by (unfold least_def) (auto dest: sym)
-
-text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for 
-  @{term "A {.=} A'"}\<close>
-
-lemma (in weak_partial_order) least_Upper_cong_l:
-  assumes "x .= x'"
-    and "x \<in> carrier L" "x' \<in> carrier L"
-    and "A \<subseteq> carrier L"
-  shows "least L x (Upper L A) = least L x' (Upper L A)"
-  apply (rule least_cong) using assms by auto
-
-lemma (in weak_partial_order) least_Upper_cong_r:
-  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
-    and AA': "A {.=} A'"
-  shows "least L x (Upper L A) = least L x (Upper L A')"
-apply (subgoal_tac "Upper L A = Upper L A'", simp)
-by (rule Upper_cong) fact+
-
-lemma least_UpperI:
-  fixes L (structure)
-  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
-    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
-    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
-  shows "least L s (Upper L A)"
-proof -
-  have "Upper L A \<subseteq> carrier L" by simp
-  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
-  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
-  ultimately show ?thesis by (simp add: least_def)
-qed
-
-lemma least_Upper_above:
-  fixes L (structure)
-  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
-  by (unfold least_def) blast
-
-lemma greatest_closed [intro, simp]:
-  "greatest L l A ==> l \<in> carrier L"
-  by (unfold greatest_def) fast
-
-lemma greatest_mem:
-  "greatest L l A ==> l \<in> A"
-  by (unfold greatest_def) fast
-
-lemma (in weak_partial_order) weak_greatest_unique:
-  "[| greatest L x A; greatest L y A |] ==> x .= y"
-  by (unfold greatest_def) blast
-
-lemma greatest_le:
-  fixes L (structure)
-  shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
-  by (unfold greatest_def) fast
-
-lemma (in weak_partial_order) greatest_cong:
-  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
-  greatest L x A = greatest L x' A"
-  by (unfold greatest_def) (auto dest: sym)
-
-text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for 
-  @{term "A {.=} A'"}\<close>
-
-lemma (in weak_partial_order) greatest_Lower_cong_l:
-  assumes "x .= x'"
-    and "x \<in> carrier L" "x' \<in> carrier L"
-    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
-  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
-  apply (rule greatest_cong) using assms by auto
-
-lemma (in weak_partial_order) greatest_Lower_cong_r:
-  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
-    and AA': "A {.=} A'"
-  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
-apply (subgoal_tac "Lower L A = Lower L A'", simp)
-by (rule Lower_cong) fact+
-
-lemma greatest_LowerI:
-  fixes L (structure)
-  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
-    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
-    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
-  shows "greatest L i (Lower L A)"
-proof -
-  have "Lower L A \<subseteq> carrier L" by simp
-  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
-  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
-  ultimately show ?thesis by (simp add: greatest_def)
-qed
-
-lemma greatest_Lower_below:
-  fixes L (structure)
-  shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
-  by (unfold greatest_def) blast
-
-text \<open>Supremum and infimum\<close>
+section \<open>Lattices\<close>
+  
+subsection \<open>Supremum and infimum\<close>
 
 definition
   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
@@ -412,6 +22,26 @@
   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
 
+definition supr :: 
+  "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
+  where "supr L A f = \<Squnion>\<^bsub>L\<^esub>(f ` A)"
+
+definition infi :: 
+  "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
+  where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
+
+syntax
+  "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _./ _)" [0, 10] 10)
+  "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3IINF\<index> _:_./ _)" [0, 0, 10] 10)
+  "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
+  "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
+
+translations
+  "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
+  "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
+  "SSUP\<^bsub>L\<^esub> x. B"     == "CONST supr L CONST UNIV (%x. B)"
+  "SSUP\<^bsub>L\<^esub> x:A. B"   == "CONST supr L A (%x. B)"
+
 definition
   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
@@ -420,6 +50,49 @@
   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
 
+definition
+  LFP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<mu>\<index>") where
+  "LFP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
+
+definition
+  GFP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<nu>\<index>") where
+  "GFP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
+
+
+subsection \<open>Dual operators\<close>
+
+lemma sup_dual [simp]: 
+  "\<Squnion>\<^bsub>inv_gorder L\<^esub>A = \<Sqinter>\<^bsub>L\<^esub>A"
+  by (simp add: sup_def inf_def)
+
+lemma inf_dual [simp]: 
+  "\<Sqinter>\<^bsub>inv_gorder L\<^esub>A = \<Squnion>\<^bsub>L\<^esub>A"
+  by (simp add: sup_def inf_def)
+
+lemma join_dual [simp]:
+  "p \<squnion>\<^bsub>inv_gorder L\<^esub> q = p \<sqinter>\<^bsub>L\<^esub> q"
+  by (simp add:join_def meet_def)
+
+lemma meet_dual [simp]:
+  "p \<sqinter>\<^bsub>inv_gorder L\<^esub> q = p \<squnion>\<^bsub>L\<^esub> q"
+  by (simp add:join_def meet_def)
+
+lemma top_dual [simp]:
+  "\<top>\<^bsub>inv_gorder L\<^esub> = \<bottom>\<^bsub>L\<^esub>"
+  by (simp add: top_def bottom_def)
+
+lemma bottom_dual [simp]:
+  "\<bottom>\<^bsub>inv_gorder L\<^esub> = \<top>\<^bsub>L\<^esub>"
+  by (simp add: top_def bottom_def)
+
+lemma LFP_dual [simp]:
+  "LFP (inv_gorder L) f = GFP L f"
+  by (simp add:LFP_def GFP_def)
+
+lemma GFP_dual [simp]:
+  "GFP (inv_gorder L) f = LFP L f"
+  by (simp add:LFP_def GFP_def)
+
 
 subsection \<open>Lattices\<close>
 
@@ -433,6 +106,18 @@
 
 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
 
+lemma (in weak_lattice) dual_weak_lattice:
+  "weak_lattice (inv_gorder L)"
+proof -
+  interpret dual: weak_partial_order "inv_gorder L"
+    by (metis dual_weak_order)
+
+  show ?thesis
+    apply (unfold_locales)
+    apply (simp_all add: inf_of_two_exists sup_of_two_exists)
+  done
+qed
+
 
 subsubsection \<open>Supremum\<close>
 
@@ -589,7 +274,7 @@
 lemma (in weak_upper_semilattice) finite_sup_insertI:
   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Squnion>(insert x A))"
+  shows "P (\<Squnion> (insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
     by (simp add: finite_sup_least)
@@ -634,6 +319,11 @@
   with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
 qed
 
+lemma (in weak_lattice) weak_le_iff_meet:
+  assumes "x \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) .= y"
+  by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym)
+  
 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
@@ -828,7 +518,7 @@
 lemma (in weak_lower_semilattice) finite_inf_insertI:
   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Sqinter>(insert x A))"
+  shows "P (\<Sqinter> (insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
     by (simp add: finite_inf_greatest)
@@ -875,6 +565,11 @@
   with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
 qed
 
+lemma (in weak_lattice) weak_le_iff_join:
+  assumes "x \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubseteq> y \<longleftrightarrow> x .= (x \<sqinter> y)"
+  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)
+  
 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
@@ -904,28 +599,15 @@
 proof -
   (* FIXME: improved simp, see weak_join_assoc above *)
   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
-  also from L have "... .= \<Sqinter>{z, x, y}" by (simp add: weak_meet_assoc_lemma)
-  also from L have "... = \<Sqinter>{x, y, z}" by (simp add: insert_commute)
+  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
+  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
   finally show ?thesis by (simp add: L)
 qed
 
-
-subsection \<open>Total Orders\<close>
-
-locale weak_total_order = weak_partial_order +
-  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-
-text \<open>Introduction rule: the usual definition of total order\<close>
-
-lemma (in weak_partial_order) weak_total_orderI:
-  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-  shows "weak_total_order L"
-  by standard (rule total)
-
 text \<open>Total orders are lattices.\<close>
 
-sublocale weak_total_order < weak?: weak_lattice
+sublocale weak_total_order \<subseteq> weak?: weak_lattice
 proof
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
@@ -969,337 +651,136 @@
 qed
 
 
-subsection \<open>Complete Lattices\<close>
-
-locale weak_complete_lattice = weak_lattice +
-  assumes sup_exists:
-    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
-    and inf_exists:
-    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
-
-text \<open>Introduction rule: the usual definition of complete lattice\<close>
-
-lemma (in weak_partial_order) weak_complete_latticeI:
-  assumes sup_exists:
-    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
-    and inf_exists:
-    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
-  shows "weak_complete_lattice L"
-  by standard (auto intro: sup_exists inf_exists)
-
-definition
-  top :: "_ => 'a" ("\<top>\<index>")
-  where "\<top>\<^bsub>L\<^esub> = sup L (carrier L)"
-
-definition
-  bottom :: "_ => 'a" ("\<bottom>\<index>")
-  where "\<bottom>\<^bsub>L\<^esub> = inf L (carrier L)"
-
-
-lemma (in weak_complete_lattice) supI:
-  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
-  ==> P (\<Squnion>A)"
-proof (unfold sup_def)
-  assume L: "A \<subseteq> carrier L"
-    and P: "!!l. least L l (Upper L A) ==> P l"
-  with sup_exists obtain s where "least L s (Upper L A)" by blast
-  with L show "P (SOME l. least L l (Upper L A))"
-  by (fast intro: someI2 weak_least_unique P)
-qed
-
-lemma (in weak_complete_lattice) sup_closed [simp]:
-  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
-  by (rule supI) simp_all
-
-lemma (in weak_complete_lattice) top_closed [simp, intro]:
-  "\<top> \<in> carrier L"
-  by (unfold top_def) simp
-
-lemma (in weak_complete_lattice) infI:
-  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
-  ==> P (\<Sqinter>A)"
-proof (unfold inf_def)
-  assume L: "A \<subseteq> carrier L"
-    and P: "!!l. greatest L l (Lower L A) ==> P l"
-  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
-  with L show "P (SOME l. greatest L l (Lower L A))"
-  by (fast intro: someI2 weak_greatest_unique P)
-qed
-
-lemma (in weak_complete_lattice) inf_closed [simp]:
-  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
-  by (rule infI) simp_all
+subsection \<open>Weak Bounded Lattices\<close>
 
-lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
-  "\<bottom> \<in> carrier L"
-  by (unfold bottom_def) simp
-
-text \<open>Jacobson: Theorem 8.1\<close>
-
-lemma Lower_empty [simp]:
-  "Lower L {} = carrier L"
-  by (unfold Lower_def) simp
-
-lemma Upper_empty [simp]:
-  "Upper L {} = carrier L"
-  by (unfold Upper_def) simp
-
-theorem (in weak_partial_order) weak_complete_lattice_criterion1:
-  assumes top_exists: "EX g. greatest L g (carrier L)"
-    and inf_exists:
-      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
-  shows "weak_complete_lattice L"
-proof (rule weak_complete_latticeI)
-  from top_exists obtain top where top: "greatest L top (carrier L)" ..
-  fix A
-  assume L: "A \<subseteq> carrier L"
-  let ?B = "Upper L A"
-  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
-  then have B_non_empty: "?B ~= {}" by fast
-  have B_L: "?B \<subseteq> carrier L" by simp
-  from inf_exists [OF B_L B_non_empty]
-  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
-  have "least L b (Upper L A)"
-apply (rule least_UpperI)
-   apply (rule greatest_le [where A = "Lower L ?B"])
-    apply (rule b_inf_B)
-   apply (rule Lower_memI)
-    apply (erule Upper_memD [THEN conjunct1])
-     apply assumption
-    apply (rule L)
-   apply (fast intro: L [THEN subsetD])
-  apply (erule greatest_Lower_below [OF b_inf_B])
-  apply simp
- apply (rule L)
-apply (rule greatest_closed [OF b_inf_B])
-done
-  then show "EX s. least L s (Upper L A)" ..
-next
-  fix A
-  assume L: "A \<subseteq> carrier L"
-  show "EX i. greatest L i (Lower L A)"
-  proof (cases "A = {}")
-    case True then show ?thesis
-      by (simp add: top_exists)
-  next
-    case False with L show ?thesis
-      by (rule inf_exists)
-  qed
-qed
-
-(* TODO: prove dual version *)
-
-
-subsection \<open>Orders and Lattices where \<open>eq\<close> is the Equality\<close>
-
-locale partial_order = weak_partial_order +
-  assumes eq_is_equal: "op .= = op ="
+locale weak_bounded_lattice = 
+  weak_lattice + 
+  weak_partial_order_bottom + 
+  weak_partial_order_top
 begin
 
-declare weak_le_antisym [rule del]
+lemma bottom_meet: "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqinter> x .= \<bottom>"
+  by (metis bottom_least least_def meet_closed meet_left weak_le_antisym)
 
-lemma le_antisym [intro]:
-  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
-  using weak_le_antisym unfolding eq_is_equal .
+lemma bottom_join: "x \<in> carrier L \<Longrightarrow> \<bottom> \<squnion> x .= x"
+  by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym)
 
-lemma lless_eq:
-  "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
-  unfolding lless_def by (simp add: eq_is_equal)
+lemma bottom_weak_eq:
+  "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b .= \<bottom>"
+  by (metis bottom_closed bottom_lower weak_le_antisym)
 
-lemma lless_asym:
-  assumes "a \<in> carrier L" "b \<in> carrier L"
-    and "a \<sqsubset> b" "b \<sqsubset> a"
-  shows "P"
-  using assms unfolding lless_eq by auto
+lemma top_join: "x \<in> carrier L \<Longrightarrow> \<top> \<squnion> x .= \<top>"
+  by (metis join_closed join_left top_closed top_higher weak_le_antisym)
+
+lemma top_meet: "x \<in> carrier L \<Longrightarrow> \<top> \<sqinter> x .= x"
+  by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym)
+
+lemma top_weak_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t .= \<top>"
+  by (metis top_closed top_higher weak_le_antisym)
 
 end
 
-
-text \<open>Least and greatest, as predicate\<close>
-
-lemma (in partial_order) least_unique:
-  "[| least L x A; least L y A |] ==> x = y"
-  using weak_least_unique unfolding eq_is_equal .
-
-lemma (in partial_order) greatest_unique:
-  "[| greatest L x A; greatest L y A |] ==> x = y"
-  using weak_greatest_unique unfolding eq_is_equal .
+sublocale weak_bounded_lattice \<subseteq> weak_partial_order ..
 
 
-text \<open>Lattices\<close>
+subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close>
 
 locale upper_semilattice = partial_order +
   assumes sup_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
-sublocale upper_semilattice < weak?: weak_upper_semilattice
-  by standard (rule sup_of_two_exists)
+sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice
+  by unfold_locales (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
-sublocale lower_semilattice < weak?: weak_lower_semilattice
-  by standard (rule inf_of_two_exists)
+sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice
+  by unfold_locales (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
 
-
-text \<open>Supremum\<close>
-
-declare (in partial_order) weak_sup_of_singleton [simp del]
+sublocale lattice \<subseteq> weak_lattice ..
 
-lemma (in partial_order) sup_of_singleton [simp]:
-  "x \<in> carrier L ==> \<Squnion>{x} = x"
-  using weak_sup_of_singleton unfolding eq_is_equal .
-
-lemma (in upper_semilattice) join_assoc_lemma:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
-  using weak_join_assoc_lemma L unfolding eq_is_equal .
+lemma (in lattice) dual_lattice:
+  "lattice (inv_gorder L)"
+proof -
+  interpret dual: weak_lattice "inv_gorder L"
+    by (metis dual_weak_lattice)
 
-lemma (in upper_semilattice) join_assoc:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
-  using weak_join_assoc L unfolding eq_is_equal .
-
-
-text \<open>Infimum\<close>
+  show ?thesis
+    apply (unfold_locales)
+    apply (simp_all add: inf_of_two_exists sup_of_two_exists)
+    apply (simp add:eq_is_equal)
+  done
+qed
+  
+lemma (in lattice) le_iff_join:
+  assumes "x \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubseteq> y \<longleftrightarrow> x = (x \<sqinter> y)"
+  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join)
 
-declare (in partial_order) weak_inf_of_singleton [simp del]
+lemma (in lattice) le_iff_meet:
+  assumes "x \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) = y"
+  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet)
 
-lemma (in partial_order) inf_of_singleton [simp]:
-  "x \<in> carrier L ==> \<Sqinter>{x} = x"
-  using weak_inf_of_singleton unfolding eq_is_equal .
-
-text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
+text \<open> Total orders are lattices. \<close>
 
-lemma (in lower_semilattice) meet_assoc_lemma:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
-  using weak_meet_assoc_lemma L unfolding eq_is_equal .
+sublocale total_order \<subseteq> weak?: lattice
+  by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists)
+    
+text \<open>Functions that preserve joins and meets\<close>
+  
+definition join_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+"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)"
 
-lemma (in lower_semilattice) meet_assoc:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
-  using weak_meet_assoc L unfolding eq_is_equal .
-
-
-text \<open>Total Orders\<close>
+definition meet_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+"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)"
 
-locale total_order = partial_order +
-  assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-
-sublocale total_order < weak?: weak_total_order
-  by standard (rule total_order_total)
-
-text \<open>Introduction rule: the usual definition of total order\<close>
+lemma join_pres_isotone:
+  assumes "f \<in> carrier X \<rightarrow> carrier Y" "join_pres X Y f"
+  shows "isotone X Y f"
+  using assms
+  apply (rule_tac isotoneI)
+  apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier)
+  using lattice_def partial_order_def upper_semilattice_def apply blast
+  using lattice_def partial_order_def upper_semilattice_def apply blast
+  apply fastforce
+done
 
-lemma (in partial_order) total_orderI:
-  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-  shows "total_order L"
-  by standard (rule total)
-
-text \<open>Total orders are lattices.\<close>
-
-sublocale total_order < weak?: lattice
-  by standard (auto intro: sup_of_two_exists inf_of_two_exists)
+lemma meet_pres_isotone:
+  assumes "f \<in> carrier X \<rightarrow> carrier Y" "meet_pres X Y f"
+  shows "isotone X Y f"
+  using assms
+  apply (rule_tac isotoneI)
+  apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier)
+  using lattice_def partial_order_def upper_semilattice_def apply blast
+  using lattice_def partial_order_def upper_semilattice_def apply blast
+  apply fastforce
+done
 
 
-text \<open>Complete lattices\<close>
-
-locale complete_lattice = lattice +
-  assumes sup_exists:
-    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
-    and inf_exists:
-    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
+subsection \<open>Bounded Lattices\<close>
 
-sublocale complete_lattice < weak?: weak_complete_lattice
-  by standard (auto intro: sup_exists inf_exists)
-
-text \<open>Introduction rule: the usual definition of complete lattice\<close>
+locale bounded_lattice = 
+  lattice + 
+  weak_partial_order_bottom + 
+  weak_partial_order_top
 
-lemma (in partial_order) complete_latticeI:
-  assumes sup_exists:
-    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
-    and inf_exists:
-    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
-  shows "complete_lattice L"
-  by standard (auto intro: sup_exists inf_exists)
+sublocale bounded_lattice \<subseteq> weak_bounded_lattice ..
 
-theorem (in partial_order) complete_lattice_criterion1:
-  assumes top_exists: "EX g. greatest L g (carrier L)"
-    and inf_exists:
-      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
-  shows "complete_lattice L"
-proof (rule complete_latticeI)
-  from top_exists obtain top where top: "greatest L top (carrier L)" ..
-  fix A
-  assume L: "A \<subseteq> carrier L"
-  let ?B = "Upper L A"
-  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
-  then have B_non_empty: "?B ~= {}" by fast
-  have B_L: "?B \<subseteq> carrier L" by simp
-  from inf_exists [OF B_L B_non_empty]
-  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
-  have "least L b (Upper L A)"
-apply (rule least_UpperI)
-   apply (rule greatest_le [where A = "Lower L ?B"])
-    apply (rule b_inf_B)
-   apply (rule Lower_memI)
-    apply (erule Upper_memD [THEN conjunct1])
-     apply assumption
-    apply (rule L)
-   apply (fast intro: L [THEN subsetD])
-  apply (erule greatest_Lower_below [OF b_inf_B])
-  apply simp
- apply (rule L)
-apply (rule greatest_closed [OF b_inf_B])
-done
-  then show "EX s. least L s (Upper L A)" ..
-next
-  fix A
-  assume L: "A \<subseteq> carrier L"
-  show "EX i. greatest L i (Lower L A)"
-  proof (cases "A = {}")
-    case True then show ?thesis
-      by (simp add: top_exists)
-  next
-    case False with L show ?thesis
-      by (rule inf_exists)
-  qed
-qed
+context bounded_lattice
+begin
 
-(* TODO: prove dual version *)
-
-
-subsection \<open>Examples\<close>
-
-subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
+lemma bottom_eq:  
+  "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b = \<bottom>"
+  by (metis bottom_closed bottom_lower le_antisym)
 
-theorem powerset_is_complete_lattice:
-  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
-  (is "complete_lattice ?L")
-proof (rule partial_order.complete_latticeI)
-  show "partial_order ?L"
-    by standard auto
-next
-  fix B
-  assume "B \<subseteq> carrier ?L"
-  then have "least ?L (\<Union>B) (Upper ?L B)"
-    by (fastforce intro!: least_UpperI simp: Upper_def)
-  then show "EX s. least ?L s (Upper ?L B)" ..
-next
-  fix B
-  assume "B \<subseteq> carrier ?L"
-  then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
-    txt \<open>@{term "\<Inter>B"} is not the infimum of @{term B}:
-      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}!\<close>
-    by (fastforce intro!: greatest_LowerI simp: Lower_def)
-  then show "EX i. greatest ?L i (Lower ?L B)" ..
-qed
-
-text \<open>An other example, that of the lattice of subgroups of a group,
-  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
+lemma top_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>"
+  by (metis le_antisym top_closed top_higher)
 
 end
+
+end
diff -r b47ba1778e44 -r 30d0b2f1df76 src/HOL/Algebra/Order.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Order.thy	Thu Mar 02 21:16:02 2017 +0100
@@ -0,0 +1,738 @@
+(*  Title:      HOL/Algebra/Order.thy
+    Author:     Clemens Ballarin, started 7 November 2003
+    Copyright:  Clemens Ballarin
+
+Most congruence rules by Stephan Hohe.
+With additional contributions from Alasdair Armstrong and Simon Foster.
+*)
+
+theory Order
+imports 
+  "~~/src/HOL/Library/FuncSet"
+  Congruence
+begin
+
+section \<open>Orders\<close>
+
+subsection \<open>Partial Orders\<close>
+
+record 'a gorder = "'a eq_object" +
+  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
+
+abbreviation inv_gorder :: "_ \<Rightarrow> 'a gorder" where
+  "inv_gorder L \<equiv>
+   \<lparr> carrier = carrier L,
+     eq = op .=\<^bsub>L\<^esub>,
+     le = (\<lambda> x y. y \<sqsubseteq>\<^bsub>L \<^esub>x) \<rparr>"
+
+lemma inv_gorder_inv:
+  "inv_gorder (inv_gorder L) = L"
+  by simp
+
+locale weak_partial_order = equivalence L for L (structure) +
+  assumes le_refl [intro, simp]:
+      "x \<in> carrier L ==> x \<sqsubseteq> x"
+    and weak_le_antisym [intro]:
+      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
+    and le_trans [trans]:
+      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
+    and le_cong:
+      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
+      x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
+
+definition
+  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
+  where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
+
+
+subsubsection \<open>The order relation\<close>
+
+context weak_partial_order
+begin
+
+lemma le_cong_l [intro, trans]:
+  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+  by (auto intro: le_cong [THEN iffD2])
+
+lemma le_cong_r [intro, trans]:
+  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+  by (auto intro: le_cong [THEN iffD1])
+
+lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
+  by (simp add: le_cong_l)
+
+end
+
+lemma weak_llessI:
+  fixes R (structure)
+  assumes "x \<sqsubseteq> y" and "~(x .= y)"
+  shows "x \<sqsubset> y"
+  using assms unfolding lless_def by simp
+
+lemma lless_imp_le:
+  fixes R (structure)
+  assumes "x \<sqsubset> y"
+  shows "x \<sqsubseteq> y"
+  using assms unfolding lless_def by simp
+
+lemma weak_lless_imp_not_eq:
+  fixes R (structure)
+  assumes "x \<sqsubset> y"
+  shows "\<not> (x .= y)"
+  using assms unfolding lless_def by simp
+
+lemma weak_llessE:
+  fixes R (structure)
+  assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
+
+lemma (in weak_partial_order) lless_cong_l [trans]:
+  assumes xx': "x .= x'"
+    and xy: "x' \<sqsubset> y"
+    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubset> y"
+  using assms unfolding lless_def by (auto intro: trans sym)
+
+lemma (in weak_partial_order) lless_cong_r [trans]:
+  assumes xy: "x \<sqsubset> y"
+    and  yy': "y .= y'"
+    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+  shows "x \<sqsubset> y'"
+  using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
+
+
+lemma (in weak_partial_order) lless_antisym:
+  assumes "a \<in> carrier L" "b \<in> carrier L"
+    and "a \<sqsubset> b" "b \<sqsubset> a"
+  shows "P"
+  using assms
+  by (elim weak_llessE) auto
+
+lemma (in weak_partial_order) lless_trans [trans]:
+  assumes "a \<sqsubset> b" "b \<sqsubset> c"
+    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
+  shows "a \<sqsubset> c"
+  using assms unfolding lless_def by (blast dest: le_trans intro: sym)
+
+lemma weak_partial_order_subset:
+  assumes "weak_partial_order L" "A \<subseteq> carrier L"
+  shows "weak_partial_order (L\<lparr> carrier := A \<rparr>)"
+proof -
+  interpret L: weak_partial_order L
+    by (simp add: assms)
+  interpret equivalence "(L\<lparr> carrier := A \<rparr>)"
+    by (simp add: L.equivalence_axioms assms(2) equivalence_subset)
+  show ?thesis
+    apply (unfold_locales, simp_all)
+    using assms(2) apply auto[1]
+    using assms(2) apply auto[1]
+    apply (meson L.le_trans assms(2) contra_subsetD)
+    apply (meson L.le_cong assms(2) subsetCE)
+  done
+qed
+
+
+subsubsection \<open>Upper and lower bounds of a set\<close>
+
+definition
+  Upper :: "[_, 'a set] => 'a set"
+  where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
+
+definition
+  Lower :: "[_, 'a set] => 'a set"
+  where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
+
+lemma Upper_closed [intro!, simp]:
+  "Upper L A \<subseteq> carrier L"
+  by (unfold Upper_def) clarify
+
+lemma Upper_memD [dest]:
+  fixes L (structure)
+  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
+  by (unfold Upper_def) blast
+
+lemma (in weak_partial_order) Upper_elemD [dest]:
+  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
+  unfolding Upper_def elem_def
+  by (blast dest: sym)
+
+lemma Upper_memI:
+  fixes L (structure)
+  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
+  by (unfold Upper_def) blast
+
+lemma (in weak_partial_order) Upper_elemI:
+  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
+  unfolding Upper_def by blast
+
+lemma Upper_antimono:
+  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
+  by (unfold Upper_def) blast
+
+lemma (in weak_partial_order) Upper_is_closed [simp]:
+  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
+  by (rule is_closedI) (blast intro: Upper_memI)+
+
+lemma (in weak_partial_order) Upper_mem_cong:
+  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
+    and aa': "a .= a'"
+    and aelem: "a \<in> Upper L A"
+  shows "a' \<in> Upper L A"
+proof (rule Upper_memI[OF _ a'carr])
+  fix y
+  assume yA: "y \<in> A"
+  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
+  also note aa'
+  finally
+      show "y \<sqsubseteq> a'"
+      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
+qed
+
+lemma (in weak_partial_order) Upper_cong:
+  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "Upper L A = Upper L A'"
+unfolding Upper_def
+apply rule
+ apply (rule, clarsimp) defer 1
+ apply (rule, clarsimp) defer 1
+proof -
+  fix x a'
+  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
+    and a'A': "a' \<in> A'"
+  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
+
+  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
+  from this obtain a
+      where aA: "a \<in> A"
+      and a'a: "a' .= a"
+      by auto
+  note [simp] = subsetD[OF Acarr aA] carr
+
+  note a'a
+  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
+  finally show "a' \<sqsubseteq> x" by simp
+next
+  fix x a
+  assume carr: "x \<in> carrier L" "a \<in> carrier L"
+    and aA: "a \<in> A"
+  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
+
+  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
+  from this obtain a'
+      where a'A': "a' \<in> A'"
+      and aa': "a .= a'"
+      by auto
+  note [simp] = subsetD[OF A'carr a'A'] carr
+
+  note aa'
+  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
+  finally show "a \<sqsubseteq> x" by simp
+qed
+
+lemma Lower_closed [intro!, simp]:
+  "Lower L A \<subseteq> carrier L"
+  by (unfold Lower_def) clarify
+
+lemma Lower_memD [dest]:
+  fixes L (structure)
+  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
+  by (unfold Lower_def) blast
+
+lemma Lower_memI:
+  fixes L (structure)
+  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
+  by (unfold Lower_def) blast
+
+lemma Lower_antimono:
+  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
+  by (unfold Lower_def) blast
+
+lemma (in weak_partial_order) Lower_is_closed [simp]:
+  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
+  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
+
+lemma (in weak_partial_order) Lower_mem_cong:
+  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
+    and aa': "a .= a'"
+    and aelem: "a \<in> Lower L A"
+  shows "a' \<in> Lower L A"
+using assms Lower_closed[of L A]
+by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
+
+lemma (in weak_partial_order) Lower_cong:
+  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "Lower L A = Lower L A'"
+unfolding Lower_def
+apply rule
+ apply clarsimp defer 1
+ apply clarsimp defer 1
+proof -
+  fix x a'
+  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
+    and a'A': "a' \<in> A'"
+  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
+  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
+
+  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
+  from this obtain a
+      where aA: "a \<in> A"
+      and a'a: "a' .= a"
+      by auto
+
+  from aA and subsetD[OF Acarr aA]
+      have "x \<sqsubseteq> a" by (rule aLxCond)
+  also note a'a[symmetric]
+  finally
+      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
+next
+  fix x a
+  assume carr: "x \<in> carrier L" "a \<in> carrier L"
+    and aA: "a \<in> A"
+  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
+  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
+
+  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
+  from this obtain a'
+      where a'A': "a' \<in> A'"
+      and aa': "a .= a'"
+      by auto
+  from a'A' and subsetD[OF A'carr a'A']
+      have "x \<sqsubseteq> a'" by (rule a'LxCond)
+  also note aa'[symmetric]
+  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
+qed
+
+text \<open>Jacobson: Theorem 8.1\<close>
+
+lemma Lower_empty [simp]:
+  "Lower L {} = carrier L"
+  by (unfold Lower_def) simp
+
+lemma Upper_empty [simp]:
+  "Upper L {} = carrier L"
+  by (unfold Upper_def) simp
+
+
+subsubsection \<open>Least and greatest, as predicate\<close>
+
+definition
+  least :: "[_, 'a, 'a set] => bool"
+  where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
+
+definition
+  greatest :: "[_, 'a, 'a set] => bool"
+  where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
+
+text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
+  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
+
+lemma least_closed [intro, simp]:
+  "least L l A ==> l \<in> carrier L"
+  by (unfold least_def) fast
+
+lemma least_mem:
+  "least L l A ==> l \<in> A"
+  by (unfold least_def) fast
+
+lemma (in weak_partial_order) weak_least_unique:
+  "[| least L x A; least L y A |] ==> x .= y"
+  by (unfold least_def) blast
+
+lemma least_le:
+  fixes L (structure)
+  shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
+  by (unfold least_def) fast
+
+lemma (in weak_partial_order) least_cong:
+  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
+  by (unfold least_def) (auto dest: sym)
+
+abbreviation is_lub :: "[_, 'a, 'a set] => bool"
+where "is_lub L x A \<equiv> least L x (Upper L A)"
+
+text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for
+  @{term "A {.=} A'"}\<close>
+
+lemma (in weak_partial_order) least_Upper_cong_l:
+  assumes "x .= x'"
+    and "x \<in> carrier L" "x' \<in> carrier L"
+    and "A \<subseteq> carrier L"
+  shows "least L x (Upper L A) = least L x' (Upper L A)"
+  apply (rule least_cong) using assms by auto
+
+lemma (in weak_partial_order) least_Upper_cong_r:
+  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
+    and AA': "A {.=} A'"
+  shows "least L x (Upper L A) = least L x (Upper L A')"
+apply (subgoal_tac "Upper L A = Upper L A'", simp)
+by (rule Upper_cong) fact+
+
+lemma least_UpperI:
+  fixes L (structure)
+  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
+    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
+    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
+  shows "least L s (Upper L A)"
+proof -
+  have "Upper L A \<subseteq> carrier L" by simp
+  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
+  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
+  ultimately show ?thesis by (simp add: least_def)
+qed
+
+lemma least_Upper_above:
+  fixes L (structure)
+  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
+  by (unfold least_def) blast
+
+lemma greatest_closed [intro, simp]:
+  "greatest L l A ==> l \<in> carrier L"
+  by (unfold greatest_def) fast
+
+lemma greatest_mem:
+  "greatest L l A ==> l \<in> A"
+  by (unfold greatest_def) fast
+
+lemma (in weak_partial_order) weak_greatest_unique:
+  "[| greatest L x A; greatest L y A |] ==> x .= y"
+  by (unfold greatest_def) blast
+
+lemma greatest_le:
+  fixes L (structure)
+  shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
+  by (unfold greatest_def) fast
+
+lemma (in weak_partial_order) greatest_cong:
+  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
+  greatest L x A = greatest L x' A"
+  by (unfold greatest_def) (auto dest: sym)
+
+abbreviation is_glb :: "[_, 'a, 'a set] => bool"
+where "is_glb L x A \<equiv> greatest L x (Lower L A)"
+
+text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for
+  @{term "A {.=} A'"} \<close>
+
+lemma (in weak_partial_order) greatest_Lower_cong_l:
+  assumes "x .= x'"
+    and "x \<in> carrier L" "x' \<in> carrier L"
+    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
+  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
+  apply (rule greatest_cong) using assms by auto
+
+lemma (in weak_partial_order) greatest_Lower_cong_r:
+  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
+apply (subgoal_tac "Lower L A = Lower L A'", simp)
+by (rule Lower_cong) fact+
+
+lemma greatest_LowerI:
+  fixes L (structure)
+  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
+    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
+    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
+  shows "greatest L i (Lower L A)"
+proof -
+  have "Lower L A \<subseteq> carrier L" by simp
+  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
+  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
+  ultimately show ?thesis by (simp add: greatest_def)
+qed
+
+lemma greatest_Lower_below:
+  fixes L (structure)
+  shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
+  by (unfold greatest_def) blast
+
+lemma Lower_dual [simp]:
+  "Lower (inv_gorder L) A = Upper L A"
+  by (simp add:Upper_def Lower_def)
+
+lemma Upper_dual [simp]:
+  "Upper (inv_gorder L) A = Lower L A"
+  by (simp add:Upper_def Lower_def)
+
+lemma least_dual [simp]:
+  "least (inv_gorder L) x A = greatest L x A"
+  by (simp add:least_def greatest_def)
+
+lemma greatest_dual [simp]:
+  "greatest (inv_gorder L) x A = least L x A"
+  by (simp add:least_def greatest_def)
+
+lemma (in weak_partial_order) dual_weak_order:
+  "weak_partial_order (inv_gorder L)"
+  apply (unfold_locales)
+  apply (simp_all)
+  apply (metis sym)
+  apply (metis trans)
+  apply (metis weak_le_antisym)
+  apply (metis le_trans)
+  apply (metis le_cong_l le_cong_r sym)
+done
+
+lemma dual_weak_order_iff:
+  "weak_partial_order (inv_gorder A) \<longleftrightarrow> weak_partial_order A"
+proof
+  assume "weak_partial_order (inv_gorder A)"
+  then interpret dpo: weak_partial_order "inv_gorder A"
+  rewrites "carrier (inv_gorder A) = carrier A"
+  and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
+  and   "eq (inv_gorder A)      = eq A"
+    by (simp_all)
+  show "weak_partial_order A"
+    by (unfold_locales, auto intro: dpo.sym dpo.trans dpo.le_trans)
+next
+  assume "weak_partial_order A"
+  thus "weak_partial_order (inv_gorder A)"
+    by (metis weak_partial_order.dual_weak_order)
+qed
+
+
+subsubsection \<open>Intervals\<close>
+
+definition
+  at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set" ("(1\<lbrace>_.._\<rbrace>\<index>)")
+  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}"
+
+context weak_partial_order
+begin
+  
+  lemma at_least_at_most_upper [dest]:
+    "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> x \<sqsubseteq> b"
+    by (simp add: at_least_at_most_def)
+
+  lemma at_least_at_most_lower [dest]:
+    "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> a \<sqsubseteq> x"
+    by (simp add: at_least_at_most_def)
+
+  lemma at_least_at_most_closed: "\<lbrace>a..b\<rbrace> \<subseteq> carrier L"
+    by (auto simp add: at_least_at_most_def)
+
+  lemma at_least_at_most_member [intro]: 
+    "\<lbrakk> x \<in> carrier L; a \<sqsubseteq> x; x \<sqsubseteq> b \<rbrakk> \<Longrightarrow> x \<in> \<lbrace>a..b\<rbrace>"
+    by (simp add: at_least_at_most_def)
+
+end
+
+
+subsubsection \<open>Isotone functions\<close>
+
+definition isotone :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where
+  "isotone A B f \<equiv>
+   weak_partial_order A \<and> weak_partial_order B \<and>
+   (\<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)"
+
+lemma isotoneI [intro?]:
+  fixes f :: "'a \<Rightarrow> 'b"
+  assumes "weak_partial_order L1"
+          "weak_partial_order L2"
+          "(\<And>x y. \<lbrakk> x \<in> carrier L1; y \<in> carrier L1; x \<sqsubseteq>\<^bsub>L1\<^esub> y \<rbrakk> 
+                   \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L2\<^esub> f y)"
+  shows "isotone L1 L2 f"
+  using assms by (auto simp add:isotone_def)
+
+abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Mono\<index>")
+  where "Monotone L f \<equiv> isotone L L f"
+
+lemma use_iso1:
+  "\<lbrakk>isotone A A f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
+   f x \<sqsubseteq>\<^bsub>A\<^esub> f y"
+  by (simp add: isotone_def)
+
+lemma use_iso2:
+  "\<lbrakk>isotone A B f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
+   f x \<sqsubseteq>\<^bsub>B\<^esub> f y"
+  by (simp add: isotone_def)
+
+lemma iso_compose:
+  "\<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>
+   isotone A C (g \<circ> f)"
+  by (simp add: isotone_def, safe, metis Pi_iff)
+
+lemma (in weak_partial_order) inv_isotone [simp]: 
+  "isotone (inv_gorder A) (inv_gorder B) f = isotone A B f"
+  by (auto simp add:isotone_def dual_weak_order dual_weak_order_iff)
+
+
+subsubsection \<open>Idempotent functions\<close>
+
+definition idempotent :: 
+  "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Idem\<index>") where
+  "idempotent L f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
+
+lemma (in weak_partial_order) idempotent:
+  "\<lbrakk> Idem f; x \<in> carrier L \<rbrakk> \<Longrightarrow> f (f x) .= f x"
+  by (auto simp add: idempotent_def)
+
+
+subsubsection \<open>Order embeddings\<close>
+
+definition order_emb :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where
+  "order_emb A B f \<equiv> weak_partial_order A 
+                   \<and> weak_partial_order B 
+                   \<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 )"
+
+lemma order_emb_isotone: "order_emb A B f \<Longrightarrow> isotone A B f"
+  by (auto simp add: isotone_def order_emb_def)
+
+
+subsubsection \<open>Commuting functions\<close>
+    
+definition commuting :: "('a, 'c) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
+"commuting A f g = (\<forall>x\<in>carrier A. (f \<circ> g) x .=\<^bsub>A\<^esub> (g \<circ> f) x)"
+
+subsection \<open>Partial orders where \<open>eq\<close> is the Equality\<close>
+
+locale partial_order = weak_partial_order +
+  assumes eq_is_equal: "op .= = op ="
+begin
+
+declare weak_le_antisym [rule del]
+
+lemma le_antisym [intro]:
+  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
+  using weak_le_antisym unfolding eq_is_equal .
+
+lemma lless_eq:
+  "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
+  unfolding lless_def by (simp add: eq_is_equal)
+
+lemma set_eq_is_eq: "A {.=} B \<longleftrightarrow> A = B"
+  by (auto simp add: set_eq_def elem_def eq_is_equal)
+
+end
+
+lemma (in partial_order) dual_order:
+  "partial_order (inv_gorder L)"
+proof -
+  interpret dwo: weak_partial_order "inv_gorder L"
+    by (metis dual_weak_order)
+  show ?thesis
+    by (unfold_locales, simp add:eq_is_equal)
+qed
+
+lemma dual_order_iff:
+  "partial_order (inv_gorder A) \<longleftrightarrow> partial_order A"
+proof
+  assume assm:"partial_order (inv_gorder A)"
+  then interpret po: partial_order "inv_gorder A"
+  rewrites "carrier (inv_gorder A) = carrier A"
+  and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
+  and   "eq (inv_gorder A)      = eq A"
+    by (simp_all)
+  show "partial_order A"
+    apply (unfold_locales, simp_all)
+    apply (metis po.sym, metis po.trans)
+    apply (metis po.weak_le_antisym, metis po.le_trans)
+    apply (metis (full_types) po.eq_is_equal, metis po.eq_is_equal)
+  done
+next
+  assume "partial_order A"
+  thus "partial_order (inv_gorder A)"
+    by (metis partial_order.dual_order)
+qed
+
+text \<open>Least and greatest, as predicate\<close>
+
+lemma (in partial_order) least_unique:
+  "[| least L x A; least L y A |] ==> x = y"
+  using weak_least_unique unfolding eq_is_equal .
+
+lemma (in partial_order) greatest_unique:
+  "[| greatest L x A; greatest L y A |] ==> x = y"
+  using weak_greatest_unique unfolding eq_is_equal .
+
+
+subsection \<open>Bounded Orders\<close>
+
+definition
+  top :: "_ => 'a" ("\<top>\<index>") where
+  "\<top>\<^bsub>L\<^esub> = (SOME x. greatest L x (carrier L))"
+
+definition
+  bottom :: "_ => 'a" ("\<bottom>\<index>") where
+  "\<bottom>\<^bsub>L\<^esub> = (SOME x. least L x (carrier L))"
+
+locale weak_partial_order_bottom = weak_partial_order L for L (structure) +
+  assumes bottom_exists: "\<exists> x. least L x (carrier L)"
+begin
+
+lemma bottom_least: "least L \<bottom> (carrier L)"
+proof -
+  obtain x where "least L x (carrier L)"
+    by (metis bottom_exists)
+
+  thus ?thesis
+    by (auto intro:someI2 simp add: bottom_def)
+qed
+
+lemma bottom_closed [simp, intro]:
+  "\<bottom> \<in> carrier L"
+  by (metis bottom_least least_mem)
+
+lemma bottom_lower [simp, intro]:
+  "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqsubseteq> x"
+  by (metis bottom_least least_le)
+
+end
+
+locale weak_partial_order_top = weak_partial_order L for L (structure) +
+  assumes top_exists: "\<exists> x. greatest L x (carrier L)"
+begin
+
+lemma top_greatest: "greatest L \<top> (carrier L)"
+proof -
+  obtain x where "greatest L x (carrier L)"
+    by (metis top_exists)
+
+  thus ?thesis
+    by (auto intro:someI2 simp add: top_def)
+qed
+
+lemma top_closed [simp, intro]:
+  "\<top> \<in> carrier L"
+  by (metis greatest_mem top_greatest)
+
+lemma top_higher [simp, intro]:
+  "x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> \<top>"
+  by (metis greatest_le top_greatest)
+
+end
+
+
+subsection \<open>Total Orders\<close>
+
+locale weak_total_order = weak_partial_order +
+  assumes total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+
+text \<open>Introduction rule: the usual definition of total order\<close>
+
+lemma (in weak_partial_order) weak_total_orderI:
+  assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+  shows "weak_total_order L"
+  by unfold_locales (rule total)
+
+
+subsection \<open>Total orders where \<open>eq\<close> is the Equality\<close>
+
+locale total_order = partial_order +
+  assumes total_order_total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+
+sublocale total_order < weak?: weak_total_order
+  by unfold_locales (rule total_order_total)
+
+text \<open>Introduction rule: the usual definition of total order\<close>
+
+lemma (in partial_order) total_orderI:
+  assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+  shows "total_order L"
+  by unfold_locales (rule total)
+
+end
diff -r b47ba1778e44 -r 30d0b2f1df76 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Mar 03 23:21:24 2017 +0100
+++ b/src/HOL/ROOT	Thu Mar 02 21:16:02 2017 +0100
@@ -297,7 +297,9 @@
     "~~/src/HOL/Number_Theory/Primes"
     "~~/src/HOL/Library/Permutation"
   theories
-    (*** New development, based on explicit structures ***)
+    (* Orders and Lattices *)
+    Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
+
     (* Groups *)
     FiniteProduct        (* Product operator for commutative groups *)
     Sylow                (* Sylow's theorem *)