20 "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X"; |
20 "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X"; |
21 by (REPEAT (ares_tac ([Union_least]@prems) 1)); |
21 by (REPEAT (ares_tac ([Union_least]@prems) 1)); |
22 by (etac CollectD 1); |
22 by (etac CollectD 1); |
23 qed "gfp_least"; |
23 qed "gfp_least"; |
24 |
24 |
25 val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))"; |
25 Goal "mono(f) ==> gfp(f) <= f(gfp(f))"; |
26 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, |
26 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, |
27 rtac (mono RS monoD), rtac gfp_upperbound, atac]); |
27 etac monoD, rtac gfp_upperbound, atac]); |
28 qed "gfp_lemma2"; |
28 qed "gfp_lemma2"; |
29 |
29 |
30 val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)"; |
30 Goal "mono(f) ==> f(gfp(f)) <= gfp(f)"; |
31 by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), |
31 by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac, |
32 rtac gfp_lemma2, rtac mono]); |
32 etac gfp_lemma2]); |
33 qed "gfp_lemma3"; |
33 qed "gfp_lemma3"; |
34 |
34 |
35 val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))"; |
35 Goal "mono(f) ==> gfp(f) = f(gfp(f))"; |
36 by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1)); |
36 by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); |
37 qed "gfp_Tarski"; |
37 qed "gfp_Tarski"; |
38 |
38 |
39 (*** Coinduction rules for greatest fixed points ***) |
39 (*** Coinduction rules for greatest fixed points ***) |
40 |
40 |
41 (*weak version*) |
41 (*weak version*) |
68 |
68 |
69 (*** Even Stronger version of coinduct [by Martin Coen] |
69 (*** Even Stronger version of coinduct [by Martin Coen] |
70 - instead of the condition X <= f(X) |
70 - instead of the condition X <= f(X) |
71 consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***) |
71 consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***) |
72 |
72 |
73 val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X Un B)"; |
73 Goal "mono(f) ==> mono(%x. f(x) Un X Un B)"; |
74 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1)); |
74 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1)); |
75 qed "coinduct3_mono_lemma"; |
75 qed "coinduct3_mono_lemma"; |
76 |
76 |
77 val [prem,mono] = goal Gfp.thy |
77 val [prem,mono] = goal Gfp.thy |
78 "[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \ |
78 "[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \ |
79 \ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))"; |
79 \ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))"; |
86 by (rtac (mono RS monoD) 1); |
86 by (rtac (mono RS monoD) 1); |
87 by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); |
87 by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); |
88 by (rtac Un_upper2 1); |
88 by (rtac Un_upper2 1); |
89 qed "coinduct3_lemma"; |
89 qed "coinduct3_lemma"; |
90 |
90 |
91 val prems = goal Gfp.thy |
91 Goal |
92 "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
92 "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
93 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); |
93 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); |
94 by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1); |
94 by (resolve_tac [coinduct3_mono_lemma RS lfp_Tarski RS ssubst] 1); |
95 by (rtac (UnI2 RS UnI1) 1); |
95 by Auto_tac; |
96 by (REPEAT (resolve_tac prems 1)); |
|
97 qed "coinduct3"; |
96 qed "coinduct3"; |
98 |
97 |
99 |
98 |
100 (** Definition forms of gfp_Tarski and coinduct, to control unfolding **) |
99 (** Definition forms of gfp_Tarski and coinduct, to control unfolding **) |
101 |
100 |
109 by (rewtac rew); |
108 by (rewtac rew); |
110 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1)); |
109 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1)); |
111 qed "def_coinduct"; |
110 qed "def_coinduct"; |
112 |
111 |
113 (*The version used in the induction/coinduction package*) |
112 (*The version used in the induction/coinduction package*) |
114 val prems = goal Gfp.thy |
113 val prems = Goal |
115 "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \ |
114 "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \ |
116 \ a: X; !!z. z: X ==> P (X Un A) z |] ==> \ |
115 \ a: X; !!z. z: X ==> P (X Un A) z |] ==> \ |
117 \ a : A"; |
116 \ a : A"; |
118 by (rtac def_coinduct 1); |
117 by (rtac def_coinduct 1); |
119 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); |
118 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); |
124 by (rewtac rew); |
123 by (rewtac rew); |
125 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1)); |
124 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1)); |
126 qed "def_coinduct3"; |
125 qed "def_coinduct3"; |
127 |
126 |
128 (*Monotonicity of gfp!*) |
127 (*Monotonicity of gfp!*) |
129 val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; |
128 val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; |
130 by (rtac (gfp_upperbound RS gfp_least) 1); |
129 by (rtac (gfp_upperbound RS gfp_least) 1); |
131 by (etac (prem RSN (2,subset_trans)) 1); |
130 by (etac (prem RSN (2,subset_trans)) 1); |
132 qed "gfp_mono"; |
131 qed "gfp_mono"; |