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