1 (* Title: HOL/Gfp.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 The Knaster-Tarski Theorem for greatest fixed points. |
|
7 *) |
|
8 |
|
9 (*** Proof of Knaster-Tarski Theorem using gfp ***) |
|
10 |
|
11 val gfp_def = thm "gfp_def"; |
|
12 |
|
13 (* gfp(f) is the least upper bound of {u. u <= f(u)} *) |
|
14 |
|
15 Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)"; |
|
16 by (etac (CollectI RS Union_upper) 1); |
|
17 qed "gfp_upperbound"; |
|
18 |
|
19 val prems = Goalw [gfp_def] |
|
20 "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X"; |
|
21 by (REPEAT (ares_tac ([Union_least]@prems) 1)); |
|
22 by (etac CollectD 1); |
|
23 qed "gfp_least"; |
|
24 |
|
25 Goal "mono(f) ==> gfp(f) <= f(gfp(f))"; |
|
26 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, |
|
27 etac monoD, rtac gfp_upperbound, atac]); |
|
28 qed "gfp_lemma2"; |
|
29 |
|
30 Goal "mono(f) ==> f(gfp(f)) <= gfp(f)"; |
|
31 by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac, |
|
32 etac gfp_lemma2]); |
|
33 qed "gfp_lemma3"; |
|
34 |
|
35 Goal "mono(f) ==> gfp(f) = f(gfp(f))"; |
|
36 by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); |
|
37 qed "gfp_unfold"; |
|
38 |
|
39 (*** Coinduction rules for greatest fixed points ***) |
|
40 |
|
41 (*weak version*) |
|
42 Goal "[| a: X; X <= f(X) |] ==> a : gfp(f)"; |
|
43 by (rtac (gfp_upperbound RS subsetD) 1); |
|
44 by Auto_tac; |
|
45 qed "weak_coinduct"; |
|
46 |
|
47 Goal "!!X. [| a : X; g`X <= f (g`X) |] ==> g a : gfp f"; |
|
48 by (etac (gfp_upperbound RS subsetD) 1); |
|
49 by (etac imageI 1); |
|
50 qed "weak_coinduct_image"; |
|
51 |
|
52 Goal "[| X <= f(X Un gfp(f)); mono(f) |] ==> \ |
|
53 \ X Un gfp(f) <= f(X Un gfp(f))"; |
|
54 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); |
|
55 qed "coinduct_lemma"; |
|
56 |
|
57 (*strong version, thanks to Coen & Frost*) |
|
58 Goal "[| mono(f); a: X; X <= f(X Un gfp(f)) |] ==> a : gfp(f)"; |
|
59 by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1); |
|
60 by (REPEAT (ares_tac [UnI1, Un_least] 1)); |
|
61 qed "coinduct"; |
|
62 |
|
63 Goal "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))"; |
|
64 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); |
|
65 qed "gfp_fun_UnI2"; |
|
66 |
|
67 (*** Even Stronger version of coinduct [by Martin Coen] |
|
68 - instead of the condition X <= f(X) |
|
69 consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***) |
|
70 |
|
71 Goal "mono(f) ==> mono(%x. f(x) Un X Un B)"; |
|
72 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1)); |
|
73 qed "coinduct3_mono_lemma"; |
|
74 |
|
75 Goal "[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \ |
|
76 \ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))"; |
|
77 by (rtac subset_trans 1); |
|
78 by (etac (coinduct3_mono_lemma RS lfp_lemma3) 1); |
|
79 by (rtac (Un_least RS Un_least) 1); |
|
80 by (rtac subset_refl 1); |
|
81 by (assume_tac 1); |
|
82 by (rtac (gfp_unfold RS equalityD1 RS subset_trans) 1); |
|
83 by (assume_tac 1); |
|
84 by (rtac monoD 1 THEN assume_tac 1); |
|
85 by (stac (coinduct3_mono_lemma RS lfp_unfold) 1); |
|
86 by Auto_tac; |
|
87 qed "coinduct3_lemma"; |
|
88 |
|
89 Goal |
|
90 "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
|
91 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); |
|
92 by (resolve_tac [coinduct3_mono_lemma RS lfp_unfold RS ssubst] 1); |
|
93 by Auto_tac; |
|
94 qed "coinduct3"; |
|
95 |
|
96 |
|
97 (** Definition forms of gfp_unfold and coinduct, to control unfolding **) |
|
98 |
|
99 Goal "[| A==gfp(f); mono(f) |] ==> A = f(A)"; |
|
100 by (auto_tac (claset() addSIs [gfp_unfold], simpset())); |
|
101 qed "def_gfp_unfold"; |
|
102 |
|
103 Goal "[| A==gfp(f); mono(f); a:X; X <= f(X Un A) |] ==> a: A"; |
|
104 by (auto_tac (claset() addSIs [coinduct], simpset())); |
|
105 qed "def_coinduct"; |
|
106 |
|
107 (*The version used in the induction/coinduction package*) |
|
108 val prems = Goal |
|
109 "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \ |
|
110 \ a: X; !!z. z: X ==> P (X Un A) z |] ==> \ |
|
111 \ a : A"; |
|
112 by (rtac def_coinduct 1); |
|
113 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); |
|
114 qed "def_Collect_coinduct"; |
|
115 |
|
116 Goal "[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) |] \ |
|
117 \ ==> a: A"; |
|
118 by (auto_tac (claset() addSIs [coinduct3], simpset())); |
|
119 qed "def_coinduct3"; |
|
120 |
|
121 (*Monotonicity of gfp!*) |
|
122 val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; |
|
123 by (rtac (gfp_upperbound RS gfp_least) 1); |
|
124 by (etac (prem RSN (2,subset_trans)) 1); |
|
125 qed "gfp_mono"; |
|