1 (* Title: CCL/lfp |
|
2 ID: $Id$ |
|
3 |
|
4 Modified version of |
|
5 Title: HOL/lfp.ML |
|
6 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
7 Copyright 1992 University of Cambridge |
|
8 |
|
9 For lfp.thy. The Knaster-Tarski Theorem |
|
10 *) |
|
11 |
|
12 open Lfp; |
|
13 |
|
14 (*** Proof of Knaster-Tarski Theorem ***) |
|
15 |
|
16 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) |
|
17 |
|
18 val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; |
|
19 by (rtac (CollectI RS Inter_lower) 1); |
|
20 by (resolve_tac prems 1); |
|
21 val lfp_lowerbound = result(); |
|
22 |
|
23 val prems = goalw Lfp.thy [lfp_def] |
|
24 "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)"; |
|
25 by (REPEAT (ares_tac ([Inter_greatest]@prems) 1)); |
|
26 by (etac CollectD 1); |
|
27 val lfp_greatest = result(); |
|
28 |
|
29 val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)"; |
|
30 by (EVERY1 [rtac lfp_greatest, rtac subset_trans, |
|
31 rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); |
|
32 val lfp_lemma2 = result(); |
|
33 |
|
34 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))"; |
|
35 by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), |
|
36 rtac lfp_lemma2, rtac mono]); |
|
37 val lfp_lemma3 = result(); |
|
38 |
|
39 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; |
|
40 by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); |
|
41 val lfp_Tarski = result(); |
|
42 |
|
43 |
|
44 (*** General induction rule for least fixed points ***) |
|
45 |
|
46 val [lfp,mono,indhyp] = goal Lfp.thy |
|
47 "[| a: lfp(f); mono(f); \ |
|
48 \ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \ |
|
49 \ |] ==> P(a)"; |
|
50 by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1); |
|
51 by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1); |
|
52 by (EVERY1 [rtac Int_greatest, rtac subset_trans, |
|
53 rtac (Int_lower1 RS (mono RS monoD)), |
|
54 rtac (mono RS lfp_lemma2), |
|
55 rtac (CollectI RS subsetI), rtac indhyp, atac]); |
|
56 val induct = result(); |
|
57 |
|
58 (** Definition forms of lfp_Tarski and induct, to control unfolding **) |
|
59 |
|
60 val [rew,mono] = goal Lfp.thy "[| h==lfp(f); mono(f) |] ==> h = f(h)"; |
|
61 by (rewtac rew); |
|
62 by (rtac (mono RS lfp_Tarski) 1); |
|
63 val def_lfp_Tarski = result(); |
|
64 |
|
65 val rew::prems = goal Lfp.thy |
|
66 "[| A == lfp(f); a:A; mono(f); \ |
|
67 \ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ |
|
68 \ |] ==> P(a)"; |
|
69 by (EVERY1 [rtac induct, (*backtracking to force correct induction*) |
|
70 REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); |
|
71 val def_induct = result(); |
|
72 |
|
73 (*Monotonicity of lfp!*) |
|
74 val prems = goal Lfp.thy |
|
75 "[| mono(g); !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; |
|
76 by (rtac lfp_lowerbound 1); |
|
77 by (rtac subset_trans 1); |
|
78 by (resolve_tac prems 1); |
|
79 by (rtac lfp_lemma2 1); |
|
80 by (resolve_tac prems 1); |
|
81 val lfp_mono = result(); |
|
82 |
|