(*  Title:      HOL/Examples/Knaster_Tarski.thy
    Author:     Makarius

Typical textbook proof example.
*)

section ‹Textbook-style reasoning: the Knaster-Tarski Theorem›

theory Knaster_Tarski
  imports Main
begin

unbundle lattice_syntax


subsection ‹Prose version›

text ‹
 According to the textbook cite‹‹pages 93--94› in "davey-priestley"›, the
 Knaster-Tarski fixpoint theorem is as follows.🚫‹We have dualized the
 argument, and tuned the notation a little bit.›

 \‹The Knaster-Tarski Fixpoint Theorem.› Let ‹L› be a complete lattice and
 ‹f: L → L› an order-preserving map. Then ‹⊓{x ∈ L | f(x) ≤ x}› is a fixpoint
 of ‹f›.

 \‹Proof.› Let ‹H = {x ∈ L | f(x) ≤ x}› and ‹a = ⊓H›. For all ‹x ∈ H› we have
 ‹a ≤ x›, so ‹f(a) ≤ f(x) ≤ x›. Thus ‹f(a)› is a lower bound of ‹H›, whence
 ‹f(a) ≤ a›. We now use this inequality to prove the reverse one (!) and
 thereby complete the proof that ‹a› is a fixpoint. Since ‹f› is
 order-preserving, ‹f(f(a)) ≤ f(a)›. This says ‹f(a) ∈ H›, so ‹a ≤ f(a)›.›


subsection ‹Formal versions›

text ‹
 The Isar proof below closely follows the original presentation. Virtually
 all of the prose narration has been rephrased in terms of formal Isar
 language elements. Just as many textbook-style proofs, there is a strong
 bias towards forward proof, and several bends in the course of reasoning.
 ›

theorem Knaster_Tarski:
  fixes f :: "'a::complete_lattice → 'a"
  assumes "mono f"
  shows "∃a. f a = a"
proof
  let ?H = "{u. f u ≤ u}"
  let ?a = "⊓?H"
  show "f ?a = ?a"
  proof -
    {
      fix x
      assume "x ∈ ?H"
      then have "?a ≤ x" by (rule Inf_lower)
      with ‹mono f› have "f ?a ≤ f x" ..
      also from ‹x ∈ ?H› have "… ≤ x" ..
      finally have "f ?a ≤ x" .
    }
    then have "f ?a ≤ ?a" by (rule Inf_greatest)
    {
      also presume "… ≤ f ?a"
      finally (order_antisym) show ?thesis .
    }
    from ‹mono f› and ‹f ?a ≤ ?a› have "f (f ?a) ≤ f ?a" ..
    then have "f ?a ∈ ?H" ..
    then show "?a ≤ f ?a" by (rule Inf_lower)
  qed
qed

text ‹
 Above we have used several advanced Isar language elements, such as explicit
 block structure and weak assumptions. Thus we have mimicked the particular
 way of reasoning of the original text.

 In the subsequent version the order of reasoning is changed to achieve
 structured top-down decomposition of the problem at the outer level, while
 only the inner steps of reasoning are done in a forward manner. We are
 certainly more at ease here, requiring only the most basic features of the
 Isar language.
 ›

theorem Knaster_Tarski':
  fixes f :: "'a::complete_lattice → 'a"
  assumes "mono f"
  shows "∃a. f a = a"
proof
  let ?H = "{u. f u ≤ u}"
  let ?a = "⊓?H"
  show "f ?a = ?a"
  proof (rule order_antisym)
    show "f ?a ≤ ?a"
    proof (rule Inf_greatest)
      fix x
      assume "x ∈ ?H"
      then have "?a ≤ x" by (rule Inf_lower)
      with ‹mono f› have "f ?a ≤ f x" ..
      also from ‹x ∈ ?H› have "… ≤ x" ..
      finally show "f ?a ≤ x" .
    qed
    show "?a ≤ f ?a"
    proof (rule Inf_lower)
      from ‹mono f› and ‹f ?a ≤ ?a› have "f (f ?a) ≤ f ?a" ..
      then show "f ?a ∈ ?H" ..
    qed
  qed
qed

end