author wenzelm Mon, 02 Aug 1999 17:58:46 +0200 changeset 7153 820c8c8573d9 parent 7152 44d46a112127 child 7154 687657a3f7e6
tuned;
 src/HOL/Isar_examples/KnasterTarski.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Peirce.thy file | annotate | diff | comparison | revisions src/HOL/cladata.ML file | annotate | diff | comparison | revisions src/Provers/clasimp.ML file | annotate | diff | comparison | revisions
--- 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; ..;
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 =
("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]];