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