tuned;
authorwenzelm
Mon Aug 02 17:58:46 1999 +0200 (1999-08-02)
changeset 7153820c8c8573d9
parent 7152 44d46a112127
child 7154 687657a3f7e6
tuned;
src/HOL/Isar_examples/KnasterTarski.thy
src/HOL/Isar_examples/Peirce.thy
src/HOL/cladata.ML
src/Provers/clasimp.ML
     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.4  
     1.5  theory KnasterTarski = Main:;
     1.6  
     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.26  
    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  *};
    1.39  
     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.10  
    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.11  
    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.4  
     4.5  (* methods *)
     4.6  
     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.10  
    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.14  
    4.15  val setup =
    4.16   [Method.add_methods
    4.17 -   [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp"),
    4.18 +   [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp (improper!)"),
    4.19      ("auto", clasimp_method auto_tac, "auto"),
    4.20      ("force", clasimp_method' force_tac, "force"),
    4.21      ("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]];