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