author | wenzelm |
Mon, 18 Sep 2000 14:49:51 +0200 | |
changeset 10017 | e146bbfc38c1 |
parent 9422 | 4b6bc2b347e5 |
child 10067 | ab03cfd6be3a |
permissions | -rw-r--r-- |
9422 | 1 |
(* Title: HOL/Gfp.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset
|
6 |
The Knaster-Tarski Theorem for greatest fixed points. |
923 | 7 |
*) |
8 |
||
9 |
(*** Proof of Knaster-Tarski Theorem using gfp ***) |
|
10 |
||
11 |
(* gfp(f) is the least upper bound of {u. u <= f(u)} *) |
|
12 |
||
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset
|
13 |
Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)"; |
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset
|
14 |
by (etac (CollectI RS Union_upper) 1); |
923 | 15 |
qed "gfp_upperbound"; |
16 |
||
9422 | 17 |
val prems = goalw (the_context ()) [gfp_def] |
923 | 18 |
"[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X"; |
19 |
by (REPEAT (ares_tac ([Union_least]@prems) 1)); |
|
20 |
by (etac CollectD 1); |
|
21 |
qed "gfp_least"; |
|
22 |
||
5316 | 23 |
Goal "mono(f) ==> gfp(f) <= f(gfp(f))"; |
923 | 24 |
by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, |
5316 | 25 |
etac monoD, rtac gfp_upperbound, atac]); |
923 | 26 |
qed "gfp_lemma2"; |
27 |
||
5316 | 28 |
Goal "mono(f) ==> f(gfp(f)) <= gfp(f)"; |
29 |
by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac, |
|
30 |
etac gfp_lemma2]); |
|
923 | 31 |
qed "gfp_lemma3"; |
32 |
||
5316 | 33 |
Goal "mono(f) ==> gfp(f) = f(gfp(f))"; |
34 |
by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); |
|
923 | 35 |
qed "gfp_Tarski"; |
36 |
||
37 |
(*** Coinduction rules for greatest fixed points ***) |
|
38 |
||
39 |
(*weak version*) |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset
|
40 |
Goal "[| a: X; X <= f(X) |] ==> a : gfp(f)"; |
923 | 41 |
by (rtac (gfp_upperbound RS subsetD) 1); |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset
|
42 |
by Auto_tac; |
923 | 43 |
qed "weak_coinduct"; |
44 |
||
9422 | 45 |
val [prem,mono] = goal (the_context ()) |
923 | 46 |
"[| X <= f(X Un gfp(f)); mono(f) |] ==> \ |
47 |
\ X Un gfp(f) <= f(X Un gfp(f))"; |
|
48 |
by (rtac (prem RS Un_least) 1); |
|
49 |
by (rtac (mono RS gfp_lemma2 RS subset_trans) 1); |
|
50 |
by (rtac (Un_upper2 RS subset_trans) 1); |
|
51 |
by (rtac (mono RS mono_Un) 1); |
|
52 |
qed "coinduct_lemma"; |
|
53 |
||
54 |
(*strong version, thanks to Coen & Frost*) |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset
|
55 |
Goal "[| mono(f); a: X; X <= f(X Un gfp(f)) |] ==> a : gfp(f)"; |
923 | 56 |
by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1); |
57 |
by (REPEAT (ares_tac [UnI1, Un_least] 1)); |
|
58 |
qed "coinduct"; |
|
59 |
||
9422 | 60 |
val [mono,prem] = goal (the_context ()) |
923 | 61 |
"[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))"; |
1465 | 62 |
by (rtac (mono RS mono_Un RS subsetD) 1); |
63 |
by (rtac (mono RS gfp_lemma2 RS subsetD RS UnI2) 1); |
|
923 | 64 |
by (rtac prem 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 |
||
5316 | 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)); |
|
923 | 73 |
qed "coinduct3_mono_lemma"; |
74 |
||
9422 | 75 |
val [prem,mono] = goal (the_context ()) |
3842 | 76 |
"[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \ |
77 |
\ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))"; |
|
923 | 78 |
by (rtac subset_trans 1); |
79 |
by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1); |
|
80 |
by (rtac (Un_least RS Un_least) 1); |
|
81 |
by (rtac subset_refl 1); |
|
82 |
by (rtac prem 1); |
|
83 |
by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1); |
|
84 |
by (rtac (mono RS monoD) 1); |
|
2036 | 85 |
by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); |
923 | 86 |
by (rtac Un_upper2 1); |
87 |
qed "coinduct3_lemma"; |
|
88 |
||
5316 | 89 |
Goal |
90 |
"[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
|
923 | 91 |
by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); |
5316 | 92 |
by (resolve_tac [coinduct3_mono_lemma RS lfp_Tarski RS ssubst] 1); |
93 |
by Auto_tac; |
|
923 | 94 |
qed "coinduct3"; |
95 |
||
96 |
||
97 |
(** Definition forms of gfp_Tarski and coinduct, to control unfolding **) |
|
98 |
||
9422 | 99 |
val [rew,mono] = goal (the_context ()) "[| A==gfp(f); mono(f) |] ==> A = f(A)"; |
923 | 100 |
by (rewtac rew); |
101 |
by (rtac (mono RS gfp_Tarski) 1); |
|
102 |
qed "def_gfp_Tarski"; |
|
103 |
||
9422 | 104 |
val rew::prems = goal (the_context ()) |
923 | 105 |
"[| A==gfp(f); mono(f); a:X; X <= f(X Un A) |] ==> a: A"; |
106 |
by (rewtac rew); |
|
107 |
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1)); |
|
108 |
qed "def_coinduct"; |
|
109 |
||
110 |
(*The version used in the induction/coinduction package*) |
|
5316 | 111 |
val prems = Goal |
923 | 112 |
"[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \ |
113 |
\ a: X; !!z. z: X ==> P (X Un A) z |] ==> \ |
|
114 |
\ a : A"; |
|
115 |
by (rtac def_coinduct 1); |
|
116 |
by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); |
|
117 |
qed "def_Collect_coinduct"; |
|
118 |
||
9422 | 119 |
val rew::prems = goal (the_context ()) |
3842 | 120 |
"[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"; |
923 | 121 |
by (rewtac rew); |
122 |
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1)); |
|
123 |
qed "def_coinduct3"; |
|
124 |
||
125 |
(*Monotonicity of gfp!*) |
|
5316 | 126 |
val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; |
1465 | 127 |
by (rtac (gfp_upperbound RS gfp_least) 1); |
128 |
by (etac (prem RSN (2,subset_trans)) 1); |
|
923 | 129 |
qed "gfp_mono"; |