author | wenzelm |
Fri, 15 Dec 2000 17:59:30 +0100 | |
changeset 10680 | 26e4aecf3207 |
parent 10186 | 499637e8f2c6 |
child 11335 | c150861633da |
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 |
||
10067 | 17 |
val prems = Goalw [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)); |
|
10186 | 35 |
qed "gfp_unfold"; |
923 | 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 |
||
10067 | 45 |
Goal "[| X <= f(X Un gfp(f)); mono(f) |] ==> \ |
923 | 46 |
\ X Un gfp(f) <= f(X Un gfp(f))"; |
10067 | 47 |
by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); |
923 | 48 |
qed "coinduct_lemma"; |
49 |
||
50 |
(*strong version, thanks to Coen & Frost*) |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset
|
51 |
Goal "[| mono(f); a: X; X <= f(X Un gfp(f)) |] ==> a : gfp(f)"; |
923 | 52 |
by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1); |
53 |
by (REPEAT (ares_tac [UnI1, Un_least] 1)); |
|
54 |
qed "coinduct"; |
|
55 |
||
10067 | 56 |
Goal "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))"; |
57 |
by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); |
|
923 | 58 |
qed "gfp_fun_UnI2"; |
59 |
||
60 |
(*** Even Stronger version of coinduct [by Martin Coen] |
|
61 |
- instead of the condition X <= f(X) |
|
62 |
consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***) |
|
63 |
||
5316 | 64 |
Goal "mono(f) ==> mono(%x. f(x) Un X Un B)"; |
65 |
by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1)); |
|
923 | 66 |
qed "coinduct3_mono_lemma"; |
67 |
||
10067 | 68 |
Goal "[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \ |
3842 | 69 |
\ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))"; |
923 | 70 |
by (rtac subset_trans 1); |
10067 | 71 |
by (etac (coinduct3_mono_lemma RS lfp_lemma3) 1); |
923 | 72 |
by (rtac (Un_least RS Un_least) 1); |
73 |
by (rtac subset_refl 1); |
|
10067 | 74 |
by (assume_tac 1); |
10186 | 75 |
by (rtac (gfp_unfold RS equalityD1 RS subset_trans) 1); |
10067 | 76 |
by (assume_tac 1); |
77 |
by (rtac monoD 1 THEN assume_tac 1); |
|
10186 | 78 |
by (stac (coinduct3_mono_lemma RS lfp_unfold) 1); |
10067 | 79 |
by Auto_tac; |
923 | 80 |
qed "coinduct3_lemma"; |
81 |
||
5316 | 82 |
Goal |
83 |
"[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
|
923 | 84 |
by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); |
10186 | 85 |
by (resolve_tac [coinduct3_mono_lemma RS lfp_unfold RS ssubst] 1); |
5316 | 86 |
by Auto_tac; |
923 | 87 |
qed "coinduct3"; |
88 |
||
89 |
||
10186 | 90 |
(** Definition forms of gfp_unfold and coinduct, to control unfolding **) |
923 | 91 |
|
10067 | 92 |
Goal "[| A==gfp(f); mono(f) |] ==> A = f(A)"; |
10186 | 93 |
by (auto_tac (claset() addSIs [gfp_unfold], simpset())); |
94 |
qed "def_gfp_unfold"; |
|
923 | 95 |
|
10067 | 96 |
Goal "[| A==gfp(f); mono(f); a:X; X <= f(X Un A) |] ==> a: A"; |
97 |
by (auto_tac (claset() addSIs [coinduct], simpset())); |
|
923 | 98 |
qed "def_coinduct"; |
99 |
||
100 |
(*The version used in the induction/coinduction package*) |
|
5316 | 101 |
val prems = Goal |
923 | 102 |
"[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \ |
103 |
\ a: X; !!z. z: X ==> P (X Un A) z |] ==> \ |
|
104 |
\ a : A"; |
|
105 |
by (rtac def_coinduct 1); |
|
106 |
by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); |
|
107 |
qed "def_Collect_coinduct"; |
|
108 |
||
10067 | 109 |
Goal "[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) |] \ |
110 |
\ ==> a: A"; |
|
111 |
by (auto_tac (claset() addSIs [coinduct3], simpset())); |
|
923 | 112 |
qed "def_coinduct3"; |
113 |
||
114 |
(*Monotonicity of gfp!*) |
|
5316 | 115 |
val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; |
1465 | 116 |
by (rtac (gfp_upperbound RS gfp_least) 1); |
117 |
by (etac (prem RSN (2,subset_trans)) 1); |
|
923 | 118 |
qed "gfp_mono"; |