--- a/src/HOL/Isar_examples/KnasterTarski.thy Mon Aug 02 17:58:23 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Mon Aug 02 17:58:46 1999 +0200
@@ -8,13 +8,31 @@
theory KnasterTarski = Main:;
+text {*
+
+ According to the book ``Introduction to Lattices and Order'' (by
+ B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
+ fixpoint theorem is as follows (pages 93--94). Note that we have
+ dualized their argument, and tuned the notation a little bit.
+
+ \paragraph{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a
+ complete lattice and $f \colon L \to L$ an order-preserving map.
+ Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
+
+ \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =
+ \bigwedge H$. For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)
+ \le x$. Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le 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)) \le f(a)$. This says $f(a) \in H$, so $a
+ \le f(a)$.
+*};
text {*
- The proof of Knaster-Tarski below closely follows the presentation in
- 'Introduction to Lattices' and Order by Davey/Priestley, pages
- 93--94. All of their narration has been rephrased in terms of formal
- Isar language elements. Just as many textbook-style proofs, there is
- a strong bias towards forward reasoning, and little hierarchical
+ Our proof below closely follows this 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 reasoning, and little hierarchical
structure.
*};
--- a/src/HOL/Isar_examples/Peirce.thy Mon Aug 02 17:58:23 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy Mon Aug 02 17:58:46 1999 +0200
@@ -17,7 +17,7 @@
have ab: "A --> B";
proof;
assume a: A;
- from not_a a; show B; ..;
+ show B; by contradiction;
qed;
from aba ab; show A; ..;
--- a/src/HOL/cladata.ML Mon Aug 02 17:58:23 1999 +0200
+++ b/src/HOL/cladata.ML Mon Aug 02 17:58:46 1999 +0200
@@ -76,7 +76,8 @@
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val claset = Classical.claset
val rep_cs = Classical.rep_cs
- val cla_method' = Classical.cla_method'
+ val cla_modifiers = Classical.cla_modifiers;
+ val cla_meth' = Classical.cla_meth'
end;
structure Blast = BlastFun(Blast_Data);
--- a/src/Provers/clasimp.ML Mon Aug 02 17:58:23 1999 +0200
+++ b/src/Provers/clasimp.ML Mon Aug 02 17:58:46 1999 +0200
@@ -149,7 +149,8 @@
(* methods *)
-fun get_local_clasimpset ctxt = (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
+fun get_local_clasimpset ctxt =
+ (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
@@ -166,7 +167,7 @@
val setup =
[Method.add_methods
- [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp"),
+ [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp (improper!)"),
("auto", clasimp_method auto_tac, "auto"),
("force", clasimp_method' force_tac, "force"),
("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]];