1(* Title: CCL/Gfp.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4*) 5 6section \<open>Greatest fixed points\<close> 7 8theory Gfp 9imports Lfp 10begin 11 12definition 13 gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> \<open>greatest fixed point\<close> 14 "gfp(f) == Union({u. u <= f(u)})" 15 16(* gfp(f) is the least upper bound of {u. u <= f(u)} *) 17 18lemma gfp_upperbound: "A <= f(A) \<Longrightarrow> A <= gfp(f)" 19 unfolding gfp_def by blast 20 21lemma gfp_least: "(\<And>u. u <= f(u) \<Longrightarrow> u <= A) \<Longrightarrow> gfp(f) <= A" 22 unfolding gfp_def by blast 23 24lemma gfp_lemma2: "mono(f) \<Longrightarrow> gfp(f) <= f(gfp(f))" 25 by (rule gfp_least, rule subset_trans, assumption, erule monoD, 26 rule gfp_upperbound, assumption) 27 28lemma gfp_lemma3: "mono(f) \<Longrightarrow> f(gfp(f)) <= gfp(f)" 29 by (rule gfp_upperbound, frule monoD, rule gfp_lemma2, assumption+) 30 31lemma gfp_Tarski: "mono(f) \<Longrightarrow> gfp(f) = f(gfp(f))" 32 by (rule equalityI gfp_lemma2 gfp_lemma3 | assumption)+ 33 34 35(*** Coinduction rules for greatest fixed points ***) 36 37(*weak version*) 38lemma coinduct: "\<lbrakk>a: A; A <= f(A)\<rbrakk> \<Longrightarrow> a : gfp(f)" 39 by (blast dest: gfp_upperbound) 40 41lemma coinduct2_lemma: "\<lbrakk>A <= f(A) Un gfp(f); mono(f)\<rbrakk> \<Longrightarrow> A Un gfp(f) <= f(A Un gfp(f))" 42 apply (rule subset_trans) 43 prefer 2 44 apply (erule mono_Un) 45 apply (rule subst, erule gfp_Tarski) 46 apply (erule Un_least) 47 apply (rule Un_upper2) 48 done 49 50(*strong version, thanks to Martin Coen*) 51lemma coinduct2: "\<lbrakk>a: A; A <= f(A) Un gfp(f); mono(f)\<rbrakk> \<Longrightarrow> a : gfp(f)" 52 apply (rule coinduct) 53 prefer 2 54 apply (erule coinduct2_lemma, assumption) 55 apply blast 56 done 57 58(*** Even Stronger version of coinduct [by Martin Coen] 59 - instead of the condition A <= f(A) 60 consider A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***) 61 62lemma coinduct3_mono_lemma: "mono(f) \<Longrightarrow> mono(\<lambda>x. f(x) Un A Un B)" 63 by (rule monoI) (blast dest: monoD) 64 65lemma coinduct3_lemma: 66 assumes prem: "A <= f(lfp(\<lambda>x. f(x) Un A Un gfp(f)))" 67 and mono: "mono(f)" 68 shows "lfp(\<lambda>x. f(x) Un A Un gfp(f)) <= f(lfp(\<lambda>x. f(x) Un A Un gfp(f)))" 69 apply (rule subset_trans) 70 apply (rule mono [THEN coinduct3_mono_lemma, THEN lfp_lemma3]) 71 apply (rule Un_least [THEN Un_least]) 72 apply (rule subset_refl) 73 apply (rule prem) 74 apply (rule mono [THEN gfp_Tarski, THEN equalityD1, THEN subset_trans]) 75 apply (rule mono [THEN monoD]) 76 apply (subst mono [THEN coinduct3_mono_lemma, THEN lfp_Tarski]) 77 apply (rule Un_upper2) 78 done 79 80lemma coinduct3: 81 assumes 1: "a:A" 82 and 2: "A <= f(lfp(\<lambda>x. f(x) Un A Un gfp(f)))" 83 and 3: "mono(f)" 84 shows "a : gfp(f)" 85 apply (rule coinduct) 86 prefer 2 87 apply (rule coinduct3_lemma [OF 2 3]) 88 apply (subst lfp_Tarski [OF coinduct3_mono_lemma, OF 3]) 89 using 1 apply blast 90 done 91 92 93subsection \<open>Definition forms of \<open>gfp_Tarski\<close>, to control unfolding\<close> 94 95lemma def_gfp_Tarski: "\<lbrakk>h == gfp(f); mono(f)\<rbrakk> \<Longrightarrow> h = f(h)" 96 apply unfold 97 apply (erule gfp_Tarski) 98 done 99 100lemma def_coinduct: "\<lbrakk>h == gfp(f); a:A; A <= f(A)\<rbrakk> \<Longrightarrow> a: h" 101 apply unfold 102 apply (erule coinduct) 103 apply assumption 104 done 105 106lemma def_coinduct2: "\<lbrakk>h == gfp(f); a:A; A <= f(A) Un h; mono(f)\<rbrakk> \<Longrightarrow> a: h" 107 apply unfold 108 apply (erule coinduct2) 109 apply assumption 110 apply assumption 111 done 112 113lemma def_coinduct3: "\<lbrakk>h == gfp(f); a:A; A <= f(lfp(\<lambda>x. f(x) Un A Un h)); mono(f)\<rbrakk> \<Longrightarrow> a: h" 114 apply unfold 115 apply (erule coinduct3) 116 apply assumption 117 apply assumption 118 done 119 120(*Monotonicity of gfp!*) 121lemma gfp_mono: "\<lbrakk>mono(f); \<And>Z. f(Z) <= g(Z)\<rbrakk> \<Longrightarrow> gfp(f) <= gfp(g)" 122 apply (rule gfp_upperbound) 123 apply (rule subset_trans) 124 apply (rule gfp_lemma2) 125 apply assumption 126 apply (erule meta_spec) 127 done 128 129end 130