author | huffman |
Fri, 13 Mar 2009 07:30:47 -0700 | |
changeset 30505 | 110e59507eec |
parent 26812 | c0fa62fa0e5b |
child 30816 | 4de62c902f9a |
permissions | -rw-r--r-- |
6882 | 1 |
(* Title: HOL/Isar_examples/KnasterTarski.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Typical textbook proof example. |
|
6 |
*) |
|
7 |
||
10007 | 8 |
header {* Textbook-style reasoning: the Knaster-Tarski Theorem *} |
6882 | 9 |
|
16417 | 10 |
theory KnasterTarski imports Main begin |
6882 | 11 |
|
7761 | 12 |
|
10007 | 13 |
subsection {* Prose version *} |
7761 | 14 |
|
7153 | 15 |
text {* |
7874 | 16 |
According to the textbook \cite[pages 93--94]{davey-priestley}, the |
17 |
Knaster-Tarski fixpoint theorem is as follows.\footnote{We have |
|
18 |
dualized the argument, and tuned the notation a little bit.} |
|
7153 | 19 |
|
7761 | 20 |
\medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a |
7153 | 21 |
complete lattice and $f \colon L \to L$ an order-preserving map. |
22 |
Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$. |
|
23 |
||
24 |
\textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a = |
|
25 |
\bigwedge H$. For all $x \in H$ we have $a \le x$, so $f(a) \le f(x) |
|
26 |
\le x$. Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$. |
|
27 |
We now use this inequality to prove the reverse one (!) and thereby |
|
28 |
complete the proof that $a$ is a fixpoint. Since $f$ is |
|
29 |
order-preserving, $f(f(a)) \le f(a)$. This says $f(a) \in H$, so $a |
|
30 |
\le f(a)$. |
|
10007 | 31 |
*} |
6883 | 32 |
|
7761 | 33 |
|
10007 | 34 |
subsection {* Formal versions *} |
7761 | 35 |
|
6893 | 36 |
text {* |
7818 | 37 |
The Isar proof below closely follows the original presentation. |
38 |
Virtually all of the prose narration has been rephrased in terms of |
|
39 |
formal Isar language elements. Just as many textbook-style proofs, |
|
7982 | 40 |
there is a strong bias towards forward proof, and several bends |
41 |
in the course of reasoning. |
|
10007 | 42 |
*} |
6882 | 43 |
|
10007 | 44 |
theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a" |
45 |
proof |
|
46 |
let ?H = "{u. f u <= u}" |
|
47 |
let ?a = "Inter ?H" |
|
6882 | 48 |
|
10007 | 49 |
assume mono: "mono f" |
50 |
show "f ?a = ?a" |
|
51 |
proof - |
|
52 |
{ |
|
53 |
fix x |
|
54 |
assume H: "x : ?H" |
|
55 |
hence "?a <= x" by (rule Inter_lower) |
|
56 |
with mono have "f ?a <= f x" .. |
|
57 |
also from H have "... <= x" .. |
|
58 |
finally have "f ?a <= x" . |
|
59 |
} |
|
60 |
hence ge: "f ?a <= ?a" by (rule Inter_greatest) |
|
61 |
{ |
|
62 |
also presume "... <= f ?a" |
|
63 |
finally (order_antisym) show ?thesis . |
|
64 |
} |
|
65 |
from mono ge have "f (f ?a) <= f ?a" .. |
|
26812
c0fa62fa0e5b
Rephrased forward proofs to avoid problems with HO unification
berghofe
parents:
16417
diff
changeset
|
66 |
hence "f ?a : ?H" by simp |
10007 | 67 |
thus "?a <= f ?a" by (rule Inter_lower) |
68 |
qed |
|
69 |
qed |
|
6898 | 70 |
|
7818 | 71 |
text {* |
72 |
Above we have used several advanced Isar language elements, such as |
|
73 |
explicit block structure and weak assumptions. Thus we have mimicked |
|
74 |
the particular way of reasoning of the original text. |
|
75 |
||
7982 | 76 |
In the subsequent version the order of reasoning is changed to |
77 |
achieve structured top-down decomposition of the problem at the outer |
|
78 |
level, while only the inner steps of reasoning are done in a forward |
|
79 |
manner. We are certainly more at ease here, requiring only the most |
|
80 |
basic features of the Isar language. |
|
10007 | 81 |
*} |
7818 | 82 |
|
10007 | 83 |
theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a" |
84 |
proof |
|
85 |
let ?H = "{u. f u <= u}" |
|
86 |
let ?a = "Inter ?H" |
|
7818 | 87 |
|
10007 | 88 |
assume mono: "mono f" |
89 |
show "f ?a = ?a" |
|
90 |
proof (rule order_antisym) |
|
91 |
show ge: "f ?a <= ?a" |
|
92 |
proof (rule Inter_greatest) |
|
93 |
fix x |
|
94 |
assume H: "x : ?H" |
|
95 |
hence "?a <= x" by (rule Inter_lower) |
|
96 |
with mono have "f ?a <= f x" .. |
|
97 |
also from H have "... <= x" .. |
|
98 |
finally show "f ?a <= x" . |
|
99 |
qed |
|
100 |
show "?a <= f ?a" |
|
101 |
proof (rule Inter_lower) |
|
102 |
from mono ge have "f (f ?a) <= f ?a" .. |
|
26812
c0fa62fa0e5b
Rephrased forward proofs to avoid problems with HO unification
berghofe
parents:
16417
diff
changeset
|
103 |
thus "f ?a : ?H" by simp |
10007 | 104 |
qed |
105 |
qed |
|
106 |
qed |
|
7818 | 107 |
|
10007 | 108 |
end |