author wenzelm Mon Aug 02 17:58:46 1999 +0200 (1999-08-02) changeset 7153 820c8c8573d9 parent 7152 44d46a112127 child 7154 687657a3f7e6
tuned;
 src/HOL/Isar_examples/KnasterTarski.thy file | annotate | diff | revisions src/HOL/Isar_examples/Peirce.thy file | annotate | diff | revisions src/HOL/cladata.ML file | annotate | diff | revisions src/Provers/clasimp.ML file | annotate | diff | revisions
1.1 --- a/src/HOL/Isar_examples/KnasterTarski.thy	Mon Aug 02 17:58:23 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/KnasterTarski.thy	Mon Aug 02 17:58:46 1999 +0200
1.3 @@ -8,13 +8,31 @@
1.5  theory KnasterTarski = Main:;
1.7 +text {*
1.8 +
1.9 + According to the book Introduction to Lattices and Order'' (by
1.10 + B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
1.11 + fixpoint theorem is as follows (pages 93--94).  Note that we have
1.12 + dualized their argument, and tuned the notation a little bit.
1.13 +
1.14 + \paragraph{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
1.15 + complete lattice and $f \colon L \to L$ an order-preserving map.
1.16 + Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
1.17 +
1.18 + \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a = 1.19 + \bigwedge H$.  For all $x \in H$ we have $a \le x$, so $f(a) \le f(x) 1.20 + \le x$.  Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.
1.21 + We now use this inequality to prove the reverse one (!) and thereby
1.22 + complete the proof that $a$ is a fixpoint.  Since $f$ is
1.23 + order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a 1.24 + \le f(a)$.
1.25 +*};
1.27  text {*
1.28 - The proof of Knaster-Tarski below closely follows the presentation in
1.29 - 'Introduction to Lattices' and Order by Davey/Priestley, pages
1.30 - 93--94.  All of their narration has been rephrased in terms of formal
1.31 - Isar language elements.  Just as many textbook-style proofs, there is
1.32 - a strong bias towards forward reasoning, and little hierarchical
1.33 + Our proof below closely follows this presentation.  Virtually all of
1.34 + the prose narration has been rephrased in terms of formal Isar
1.35 + language elements.  Just as many textbook-style proofs, there is a
1.36 + strong bias towards forward reasoning, and little hierarchical
1.37   structure.
1.38  *};
2.1 --- a/src/HOL/Isar_examples/Peirce.thy	Mon Aug 02 17:58:23 1999 +0200
2.2 +++ b/src/HOL/Isar_examples/Peirce.thy	Mon Aug 02 17:58:46 1999 +0200
2.3 @@ -17,7 +17,7 @@
2.4      have ab: "A --> B";
2.5      proof;
2.6        assume a: A;
2.7 -      from not_a a; show B; ..;
2.8 +      show B; by contradiction;
2.9      qed;
2.11      from aba ab; show A; ..;
3.1 --- a/src/HOL/cladata.ML	Mon Aug 02 17:58:23 1999 +0200
3.2 +++ b/src/HOL/cladata.ML	Mon Aug 02 17:58:46 1999 +0200
3.3 @@ -76,7 +76,8 @@
3.4    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
3.5    val claset	= Classical.claset
3.6    val rep_cs    = Classical.rep_cs
3.7 -  val cla_method' = Classical.cla_method'
3.8 +  val cla_modifiers = Classical.cla_modifiers;
3.9 +  val cla_meth' = Classical.cla_meth'
3.10    end;
3.12  structure Blast = BlastFun(Blast_Data);
4.1 --- a/src/Provers/clasimp.ML	Mon Aug 02 17:58:23 1999 +0200
4.2 +++ b/src/Provers/clasimp.ML	Mon Aug 02 17:58:46 1999 +0200
4.3 @@ -149,7 +149,8 @@
4.5  (* methods *)
4.7 -fun get_local_clasimpset ctxt = (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
4.8 +fun get_local_clasimpset ctxt =
4.9 +  (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
4.11  val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
4.12  val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
4.13 @@ -166,7 +167,7 @@
4.15  val setup =