src/HOL/Isar_examples/KnasterTarski.thy

--- a/src/HOL/Isar_examples/KnasterTarski.thy	Sun Sep 17 22:15:08 2000 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sun Sep 17 22:19:02 2000 +0200
@@ -5,12 +5,12 @@
 Typical textbook proof example.
 *)
 
-header {* Textbook-style reasoning: the Knaster-Tarski Theorem *};
+header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
 
-theory KnasterTarski = Main:;
+theory KnasterTarski = Main:
 
 
-subsection {* Prose version *};
+subsection {* Prose version *}
 
 text {*
  According to the textbook \cite[pages 93--94]{davey-priestley}, the
@@ -28,10 +28,10 @@
  complete the proof that $a$ is a fixpoint.  Since $f$ is
  order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a
  \le f(a)$.
-*};
+*}
 
 
-subsection {* Formal versions *};
+subsection {* Formal versions *}
 
 text {*
  The Isar proof below closely follows the original presentation.
@@ -39,34 +39,34 @@
  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 KnasterTarski: "mono f ==> EX a::'a set. f a = a";
-proof;
-  let ?H = "{u. f u <= u}";
-  let ?a = "Inter ?H";
+theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"
+proof
+  let ?H = "{u. f u <= u}"
+  let ?a = "Inter ?H"
 
-  assume mono: "mono f";
-  show "f ?a = ?a";
-  proof -;
-    {;
-      fix x;
-      assume H: "x : ?H";
-      hence "?a <= x"; by (rule Inter_lower);
-      with mono; have "f ?a <= f x"; ..;
-      also; from H; have "... <= x"; ..;
-      finally; have "f ?a <= x"; .;
-    };
-    hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
-    {;
-      also; presume "... <= f ?a";
-      finally (order_antisym); show ?thesis; .;
-    };
-    from mono ge; have "f (f ?a) <= f ?a"; ..;
-    hence "f ?a : ?H"; ..;
-    thus "?a <= f ?a"; by (rule Inter_lower);
-  qed;
-qed;
+  assume mono: "mono f"
+  show "f ?a = ?a"
+  proof -
+    {
+      fix x
+      assume H: "x : ?H"
+      hence "?a <= x" by (rule Inter_lower)
+      with mono have "f ?a <= f x" ..
+      also from H have "... <= x" ..
+      finally have "f ?a <= x" .
+    }
+    hence ge: "f ?a <= ?a" by (rule Inter_greatest)
+    {
+      also presume "... <= f ?a"
+      finally (order_antisym) show ?thesis .
+    }
+    from mono ge have "f (f ?a) <= f ?a" ..
+    hence "f ?a : ?H" ..
+    thus "?a <= f ?a" by (rule Inter_lower)
+  qed
+qed
 
 text {*
  Above we have used several advanced Isar language elements, such as
@@ -78,31 +78,31 @@
  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 KnasterTarski': "mono f ==> EX a::'a set. f a = a";
-proof;
-  let ?H = "{u. f u <= u}";
-  let ?a = "Inter ?H";
+theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a"
+proof
+  let ?H = "{u. f u <= u}"
+  let ?a = "Inter ?H"
 
-  assume mono: "mono f";
-  show "f ?a = ?a";
-  proof (rule order_antisym);
-    show ge: "f ?a <= ?a";
-    proof (rule Inter_greatest);
-      fix x;
-      assume H: "x : ?H";
-      hence "?a <= x"; by (rule Inter_lower);
-      with mono; have "f ?a <= f x"; ..;
-      also; from H; have "... <= x"; ..;
-      finally; show "f ?a <= x"; .;
-    qed;
-    show "?a <= f ?a";
-    proof (rule Inter_lower);
-      from mono ge; have "f (f ?a) <= f ?a"; ..;
-      thus "f ?a : ?H"; ..;
-    qed;
-  qed;
-qed;
+  assume mono: "mono f"
+  show "f ?a = ?a"
+  proof (rule order_antisym)
+    show ge: "f ?a <= ?a"
+    proof (rule Inter_greatest)
+      fix x
+      assume H: "x : ?H"
+      hence "?a <= x" by (rule Inter_lower)
+      with mono have "f ?a <= f x" ..
+      also from H have "... <= x" ..
+      finally show "f ?a <= x" .
+    qed
+    show "?a <= f ?a"
+    proof (rule Inter_lower)
+      from mono ge have "f (f ?a) <= f ?a" ..
+      thus "f ?a : ?H" ..
+    qed
+  qed
+qed
 
-end;
+end