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