17456

1 
(* Title: CCL/Gfp.thy

1474

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

3 
Copyright 1992 University of Cambridge


4 
*)


5 

60770

6 
section \<open>Greatest fixed points\<close>

17456

7 


8 
theory Gfp


9 
imports Lfp


10 
begin


11 

20140

12 
definition

62020

13 
gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> "greatest fixed point"

17456

14 
"gfp(f) == Union({u. u <= f(u)})"


15 

20140

16 
(* gfp(f) is the least upper bound of {u. u <= f(u)} *)


17 

58977

18 
lemma gfp_upperbound: "A <= f(A) \<Longrightarrow> A <= gfp(f)"

20140

19 
unfolding gfp_def by blast


20 

58977

21 
lemma gfp_least: "(\<And>u. u <= f(u) \<Longrightarrow> u <= A) \<Longrightarrow> gfp(f) <= A"

20140

22 
unfolding gfp_def by blast


23 

58977

24 
lemma gfp_lemma2: "mono(f) \<Longrightarrow> gfp(f) <= f(gfp(f))"

20140

25 
by (rule gfp_least, rule subset_trans, assumption, erule monoD,


26 
rule gfp_upperbound, assumption)


27 

58977

28 
lemma gfp_lemma3: "mono(f) \<Longrightarrow> f(gfp(f)) <= gfp(f)"

20140

29 
by (rule gfp_upperbound, frule monoD, rule gfp_lemma2, assumption+)


30 

58977

31 
lemma gfp_Tarski: "mono(f) \<Longrightarrow> gfp(f) = f(gfp(f))"

20140

32 
by (rule equalityI gfp_lemma2 gfp_lemma3  assumption)+


33 


34 


35 
(*** Coinduction rules for greatest fixed points ***)


36 


37 
(*weak version*)

58977

38 
lemma coinduct: "\<lbrakk>a: A; A <= f(A)\<rbrakk> \<Longrightarrow> a : gfp(f)"

20140

39 
by (blast dest: gfp_upperbound)


40 

58977

41 
lemma coinduct2_lemma: "\<lbrakk>A <= f(A) Un gfp(f); mono(f)\<rbrakk> \<Longrightarrow> A Un gfp(f) <= f(A Un gfp(f))"

20140

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*)

58977

51 
lemma coinduct2: "\<lbrakk>a: A; A <= f(A) Un gfp(f); mono(f)\<rbrakk> \<Longrightarrow> a : gfp(f)"

20140

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 

58977

62 
lemma coinduct3_mono_lemma: "mono(f) \<Longrightarrow> mono(\<lambda>x. f(x) Un A Un B)"

20140

63 
by (rule monoI) (blast dest: monoD)


64 


65 
lemma coinduct3_lemma:

58977

66 
assumes prem: "A <= f(lfp(\<lambda>x. f(x) Un A Un gfp(f)))"

20140

67 
and mono: "mono(f)"

58977

68 
shows "lfp(\<lambda>x. f(x) Un A Un gfp(f)) <= f(lfp(\<lambda>x. f(x) Un A Un gfp(f)))"

20140

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 


80 
lemma coinduct3:


81 
assumes 1: "a:A"

58977

82 
and 2: "A <= f(lfp(\<lambda>x. f(x) Un A Un gfp(f)))"

20140

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 

62020

93 
subsection \<open>Definition forms of \<open>gfp_Tarski\<close>, to control unfolding\<close>

20140

94 

58977

95 
lemma def_gfp_Tarski: "\<lbrakk>h == gfp(f); mono(f)\<rbrakk> \<Longrightarrow> h = f(h)"

20140

96 
apply unfold


97 
apply (erule gfp_Tarski)


98 
done


99 

58977

100 
lemma def_coinduct: "\<lbrakk>h == gfp(f); a:A; A <= f(A)\<rbrakk> \<Longrightarrow> a: h"

20140

101 
apply unfold


102 
apply (erule coinduct)


103 
apply assumption


104 
done


105 

58977

106 
lemma def_coinduct2: "\<lbrakk>h == gfp(f); a:A; A <= f(A) Un h; mono(f)\<rbrakk> \<Longrightarrow> a: h"

20140

107 
apply unfold


108 
apply (erule coinduct2)


109 
apply assumption


110 
apply assumption


111 
done


112 

58977

113 
lemma 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"

20140

114 
apply unfold


115 
apply (erule coinduct3)


116 
apply assumption


117 
apply assumption


118 
done


119 


120 
(*Monotonicity of gfp!*)

58977

121 
lemma gfp_mono: "\<lbrakk>mono(f); \<And>Z. f(Z) <= g(Z)\<rbrakk> \<Longrightarrow> gfp(f) <= gfp(g)"

20140

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

17456

128 

0

129 
end
