1 (* ID: $Id$ |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1994 University of Cambridge |
|
4 |
|
5 *) |
|
6 |
|
7 header{*Greatest Fixed Points and the Knaster-Tarski Theorem*} |
|
8 |
|
9 theory Gfp |
|
10 imports Lfp |
|
11 begin |
|
12 |
|
13 constdefs |
|
14 gfp :: "['a set=>'a set] => 'a set" |
|
15 "gfp(f) == Union({u. u \<subseteq> f(u)})" |
|
16 |
|
17 |
|
18 |
|
19 subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*} |
|
20 |
|
21 |
|
22 text{*@{term "gfp f"} is the greatest lower bound of |
|
23 the set @{term "{u. u \<subseteq> f(u)}"} *} |
|
24 |
|
25 lemma gfp_upperbound: "[| X \<subseteq> f(X) |] ==> X \<subseteq> gfp(f)" |
|
26 by (auto simp add: gfp_def) |
|
27 |
|
28 lemma gfp_least: "[| !!u. u \<subseteq> f(u) ==> u\<subseteq>X |] ==> gfp(f) \<subseteq> X" |
|
29 by (auto simp add: gfp_def) |
|
30 |
|
31 lemma gfp_lemma2: "mono(f) ==> gfp(f) \<subseteq> f(gfp(f))" |
|
32 by (rules intro: gfp_least subset_trans monoD gfp_upperbound) |
|
33 |
|
34 lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) \<subseteq> gfp(f)" |
|
35 by (rules intro: gfp_lemma2 monoD gfp_upperbound) |
|
36 |
|
37 lemma gfp_unfold: "mono(f) ==> gfp(f) = f(gfp(f))" |
|
38 by (rules intro: equalityI gfp_lemma2 gfp_lemma3) |
|
39 |
|
40 subsection{*Coinduction rules for greatest fixed points*} |
|
41 |
|
42 text{*weak version*} |
|
43 lemma weak_coinduct: "[| a: X; X \<subseteq> f(X) |] ==> a : gfp(f)" |
|
44 by (rule gfp_upperbound [THEN subsetD], auto) |
|
45 |
|
46 lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f" |
|
47 apply (erule gfp_upperbound [THEN subsetD]) |
|
48 apply (erule imageI) |
|
49 done |
|
50 |
|
51 lemma coinduct_lemma: |
|
52 "[| X \<subseteq> f(X Un gfp(f)); mono(f) |] ==> X Un gfp(f) \<subseteq> f(X Un gfp(f))" |
|
53 by (blast dest: gfp_lemma2 mono_Un) |
|
54 |
|
55 text{*strong version, thanks to Coen and Frost*} |
|
56 lemma coinduct: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)" |
|
57 by (blast intro: weak_coinduct [OF _ coinduct_lemma]) |
|
58 |
|
59 lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))" |
|
60 by (blast dest: gfp_lemma2 mono_Un) |
|
61 |
|
62 subsection{*Even Stronger Coinduction Rule, by Martin Coen*} |
|
63 |
|
64 text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both |
|
65 @{term lfp} and @{term gfp}*} |
|
66 |
|
67 lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)" |
|
68 by (rules intro: subset_refl monoI Un_mono monoD) |
|
69 |
|
70 lemma coinduct3_lemma: |
|
71 "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] |
|
72 ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))" |
|
73 apply (rule subset_trans) |
|
74 apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) |
|
75 apply (rule Un_least [THEN Un_least]) |
|
76 apply (rule subset_refl, assumption) |
|
77 apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) |
|
78 apply (rule monoD, assumption) |
|
79 apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) |
|
80 done |
|
81 |
|
82 lemma coinduct3: |
|
83 "[| mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)" |
|
84 apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) |
|
85 apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto) |
|
86 done |
|
87 |
|
88 |
|
89 text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, |
|
90 to control unfolding*} |
|
91 |
|
92 lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)" |
|
93 by (auto intro!: gfp_unfold) |
|
94 |
|
95 lemma def_coinduct: |
|
96 "[| A==gfp(f); mono(f); a:X; X \<subseteq> f(X Un A) |] ==> a: A" |
|
97 by (auto intro!: coinduct) |
|
98 |
|
99 (*The version used in the induction/coinduction package*) |
|
100 lemma def_Collect_coinduct: |
|
101 "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); |
|
102 a: X; !!z. z: X ==> P (X Un A) z |] ==> |
|
103 a : A" |
|
104 apply (erule def_coinduct, auto) |
|
105 done |
|
106 |
|
107 lemma def_coinduct3: |
|
108 "[| A==gfp(f); mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A" |
|
109 by (auto intro!: coinduct3) |
|
110 |
|
111 text{*Monotonicity of @{term gfp}!*} |
|
112 lemma gfp_mono: "[| !!Z. f(Z)\<subseteq>g(Z) |] ==> gfp(f) \<subseteq> gfp(g)" |
|
113 by (rule gfp_upperbound [THEN gfp_least], blast) |
|
114 |
|
115 |
|
116 ML |
|
117 {* |
|
118 val gfp_def = thm "gfp_def"; |
|
119 val gfp_upperbound = thm "gfp_upperbound"; |
|
120 val gfp_least = thm "gfp_least"; |
|
121 val gfp_unfold = thm "gfp_unfold"; |
|
122 val weak_coinduct = thm "weak_coinduct"; |
|
123 val weak_coinduct_image = thm "weak_coinduct_image"; |
|
124 val coinduct = thm "coinduct"; |
|
125 val gfp_fun_UnI2 = thm "gfp_fun_UnI2"; |
|
126 val coinduct3 = thm "coinduct3"; |
|
127 val def_gfp_unfold = thm "def_gfp_unfold"; |
|
128 val def_coinduct = thm "def_coinduct"; |
|
129 val def_Collect_coinduct = thm "def_Collect_coinduct"; |
|
130 val def_coinduct3 = thm "def_coinduct3"; |
|
131 val gfp_mono = thm "gfp_mono"; |
|
132 *} |
|
133 |
|
134 |
|
135 end |
|