96 by (REPEAT (rtac lfp_subset 1)); |
96 by (REPEAT (rtac lfp_subset 1)); |
97 qed "lfp_lemma3"; |
97 qed "lfp_lemma3"; |
98 |
98 |
99 Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"; |
99 Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"; |
100 by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1)); |
100 by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1)); |
101 qed "lfp_Tarski"; |
101 qed "lfp_unfold"; |
102 |
102 |
103 (*Definition form, to control unfolding*) |
103 (*Definition form, to control unfolding*) |
104 val [rew,mono] = goal (the_context ()) |
104 val [rew,mono] = goal (the_context ()) |
105 "[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
105 "[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
106 by (rewtac rew); |
106 by (rewtac rew); |
107 by (rtac (mono RS lfp_Tarski) 1); |
107 by (rtac (mono RS lfp_unfold) 1); |
108 qed "def_lfp_Tarski"; |
108 qed "def_lfp_unfold"; |
109 |
109 |
110 (*** General induction rule for least fixedpoints ***) |
110 (*** General induction rule for least fixedpoints ***) |
111 |
111 |
112 val [hmono,indstep] = Goal |
112 val [hmono,indstep] = Goal |
113 "[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ |
113 "[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ |
220 by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1)); |
220 by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1)); |
221 qed "gfp_lemma3"; |
221 qed "gfp_lemma3"; |
222 |
222 |
223 Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"; |
223 Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"; |
224 by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); |
224 by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); |
225 qed "gfp_Tarski"; |
225 qed "gfp_unfold"; |
226 |
226 |
227 (*Definition form, to control unfolding*) |
227 (*Definition form, to control unfolding*) |
228 val [rew,mono] = goal (the_context ()) |
228 val [rew,mono] = goal (the_context ()) |
229 "[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
229 "[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
230 by (rewtac rew); |
230 by (rewtac rew); |
231 by (rtac (mono RS gfp_Tarski) 1); |
231 by (rtac (mono RS gfp_unfold) 1); |
232 qed "def_gfp_Tarski"; |
232 qed "def_gfp_unfold"; |
233 |
233 |
234 |
234 |
235 (*** Coinduction rules for greatest fixed points ***) |
235 (*** Coinduction rules for greatest fixed points ***) |
236 |
236 |
237 (*weak version*) |
237 (*weak version*) |