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 val [mono] = goal Lfp.thy "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 rtac (mono RS 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 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))"; |
32 by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), |
32 by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), |
33 rtac lfp_lemma2, rtac mono]); |
33 rtac lfp_lemma2, rtac mono]); |
34 qed "lfp_lemma3"; |
34 qed "lfp_lemma3"; |
35 |
35 |
36 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; |
36 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; |
37 by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); |
37 by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 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 Lfp.thy |
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); |
48 by (EVERY1 [rtac Int_greatest, rtac subset_trans, |
48 by (EVERY1 [rtac Int_greatest, rtac subset_trans, |
49 rtac (Int_lower1 RS (mono RS monoD)), |
49 rtac (Int_lower1 RS (mono RS monoD)), |
50 rtac (mono RS lfp_lemma2), |
50 rtac (mono RS lfp_lemma2), |
51 rtac (CollectI RS subsetI), rtac indhyp, atac]); |
51 rtac (CollectI RS subsetI), rtac indhyp, atac]); |
52 qed "induct"; |
52 qed "induct"; |
53 |
53 |
54 val major::prems = goal Lfp.thy |
54 val major::prems = goal Lfp.thy |
55 "[| (a,b) : lfp f; mono f; \ |
55 "[| (a,b) : lfp f; mono f; \ |
56 \ !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b"; |
56 \ !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b"; |
57 by(res_inst_tac [("c1","P")] (split RS subst) 1); |
57 by(res_inst_tac [("c1","P")] (split RS subst) 1); |
58 br (major RS induct) 1; |
58 by (rtac (major RS induct) 1); |
59 brs prems 1; |
59 by (resolve_tac prems 1); |
60 by(res_inst_tac[("p","x")]PairE 1); |
60 by(res_inst_tac[("p","x")]PairE 1); |
61 by(hyp_subst_tac 1); |
61 by(hyp_subst_tac 1); |
62 by(asm_simp_tac (!simpset addsimps prems) 1); |
62 by(asm_simp_tac (!simpset addsimps prems) 1); |
63 qed"induct2"; |
63 qed"induct2"; |
64 |
64 |
65 (*** Fixpoint induction a la David Park ***) |
65 (*** Fixpoint induction a la David Park ***) |
66 goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A"; |
66 goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A"; |
67 br subsetI 1; |
67 by (rtac subsetI 1); |
68 by(EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1, |
68 by(EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1, |
69 atac 2, fast_tac (set_cs addSEs [monoD]) 1]); |
69 atac 2, fast_tac (set_cs addSEs [monoD]) 1]); |
70 qed "Park_induct"; |
70 qed "Park_induct"; |
71 |
71 |
72 (** Definition forms of lfp_Tarski and induct, to control unfolding **) |
72 (** Definition forms of lfp_Tarski and induct, to control unfolding **) |
75 by (rewtac rew); |
75 by (rewtac rew); |
76 by (rtac (mono RS lfp_Tarski) 1); |
76 by (rtac (mono RS lfp_Tarski) 1); |
77 qed "def_lfp_Tarski"; |
77 qed "def_lfp_Tarski"; |
78 |
78 |
79 val rew::prems = goal Lfp.thy |
79 val rew::prems = goal Lfp.thy |
80 "[| A == lfp(f); mono(f); a:A; \ |
80 "[| A == lfp(f); mono(f); a:A; \ |
81 \ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ |
81 \ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ |
82 \ |] ==> P(a)"; |
82 \ |] ==> P(a)"; |
83 by (EVERY1 [rtac induct, (*backtracking to force correct induction*) |
83 by (EVERY1 [rtac induct, (*backtracking to force correct induction*) |
84 REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); |
84 REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); |
85 qed "def_induct"; |
85 qed "def_induct"; |
86 |
86 |
87 (*Monotonicity of lfp!*) |
87 (*Monotonicity of lfp!*) |
88 val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; |
88 val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; |
89 br (lfp_lowerbound RS lfp_greatest) 1; |
89 by (rtac (lfp_lowerbound RS lfp_greatest) 1); |
90 be (prem RS subset_trans) 1; |
90 by (etac (prem RS subset_trans) 1); |
91 qed "lfp_mono"; |
91 qed "lfp_mono"; |