equal
deleted
inserted
replaced
1 (* Title: CCL/Gfp.thy |
1 (* Title: CCL/Gfp.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1992 University of Cambridge |
3 Copyright 1992 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* Greatest fixed points *} |
6 section \<open>Greatest fixed points\<close> |
7 |
7 |
8 theory Gfp |
8 theory Gfp |
9 imports Lfp |
9 imports Lfp |
10 begin |
10 begin |
11 |
11 |
88 apply (subst lfp_Tarski [OF coinduct3_mono_lemma, OF 3]) |
88 apply (subst lfp_Tarski [OF coinduct3_mono_lemma, OF 3]) |
89 using 1 apply blast |
89 using 1 apply blast |
90 done |
90 done |
91 |
91 |
92 |
92 |
93 subsection {* Definition forms of @{text "gfp_Tarski"}, to control unfolding *} |
93 subsection \<open>Definition forms of @{text "gfp_Tarski"}, to control unfolding\<close> |
94 |
94 |
95 lemma def_gfp_Tarski: "\<lbrakk>h == gfp(f); mono(f)\<rbrakk> \<Longrightarrow> h = f(h)" |
95 lemma def_gfp_Tarski: "\<lbrakk>h == gfp(f); mono(f)\<rbrakk> \<Longrightarrow> h = f(h)" |
96 apply unfold |
96 apply unfold |
97 apply (erule gfp_Tarski) |
97 apply (erule gfp_Tarski) |
98 done |
98 done |