17456

1 
(* Title: CCL/Gfp.thy

0

2 
ID: $Id$

1474

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1992 University of Cambridge


5 
*)


6 

17456

7 
header {* Greatest fixed points *}


8 


9 
theory Gfp


10 
imports Lfp


11 
begin


12 

20140

13 
definition

17456

14 
gfp :: "['a set=>'a set] => 'a set" (*greatest fixed point*)


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


16 

20140

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


18 


19 
lemma gfp_upperbound: "[ A <= f(A) ] ==> A <= gfp(f)"


20 
unfolding gfp_def by blast


21 


22 
lemma gfp_least: "[ !!u. u <= f(u) ==> u<=A ] ==> gfp(f) <= A"


23 
unfolding gfp_def by blast


24 


25 
lemma gfp_lemma2: "mono(f) ==> gfp(f) <= f(gfp(f))"


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


27 
rule gfp_upperbound, assumption)


28 


29 
lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) <= gfp(f)"


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


31 


32 
lemma gfp_Tarski: "mono(f) ==> gfp(f) = f(gfp(f))"


33 
by (rule equalityI gfp_lemma2 gfp_lemma3  assumption)+


34 


35 


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


37 


38 
(*weak version*)


39 
lemma coinduct: "[ a: A; A <= f(A) ] ==> a : gfp(f)"


40 
by (blast dest: gfp_upperbound)


41 


42 
lemma coinduct2_lemma:


43 
"[ A <= f(A) Un gfp(f); mono(f) ] ==>


44 
A Un gfp(f) <= f(A Un gfp(f))"


45 
apply (rule subset_trans)


46 
prefer 2


47 
apply (erule mono_Un)


48 
apply (rule subst, erule gfp_Tarski)


49 
apply (erule Un_least)


50 
apply (rule Un_upper2)


51 
done


52 


53 
(*strong version, thanks to Martin Coen*)


54 
lemma coinduct2:


55 
"[ a: A; A <= f(A) Un gfp(f); mono(f) ] ==> a : gfp(f)"


56 
apply (rule coinduct)


57 
prefer 2


58 
apply (erule coinduct2_lemma, assumption)


59 
apply blast


60 
done


61 


62 
(*** Even Stronger version of coinduct [by Martin Coen]


63 
 instead of the condition A <= f(A)


64 
consider A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***)


65 


66 
lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un A Un B)"


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


68 


69 
lemma coinduct3_lemma:


70 
assumes prem: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))"


71 
and mono: "mono(f)"


72 
shows "lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))"


73 
apply (rule subset_trans)


74 
apply (rule mono [THEN coinduct3_mono_lemma, THEN lfp_lemma3])


75 
apply (rule Un_least [THEN Un_least])


76 
apply (rule subset_refl)


77 
apply (rule prem)


78 
apply (rule mono [THEN gfp_Tarski, THEN equalityD1, THEN subset_trans])


79 
apply (rule mono [THEN monoD])


80 
apply (subst mono [THEN coinduct3_mono_lemma, THEN lfp_Tarski])


81 
apply (rule Un_upper2)


82 
done


83 


84 
lemma coinduct3:


85 
assumes 1: "a:A"


86 
and 2: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))"


87 
and 3: "mono(f)"


88 
shows "a : gfp(f)"


89 
apply (rule coinduct)


90 
prefer 2


91 
apply (rule coinduct3_lemma [OF 2 3])


92 
apply (subst lfp_Tarski [OF coinduct3_mono_lemma, OF 3])


93 
using 1 apply blast


94 
done


95 


96 


97 
subsection {* Definition forms of @{text "gfp_Tarski"}, to control unfolding *}


98 


99 
lemma def_gfp_Tarski: "[ h==gfp(f); mono(f) ] ==> h = f(h)"


100 
apply unfold


101 
apply (erule gfp_Tarski)


102 
done


103 


104 
lemma def_coinduct: "[ h==gfp(f); a:A; A <= f(A) ] ==> a: h"


105 
apply unfold


106 
apply (erule coinduct)


107 
apply assumption


108 
done


109 


110 
lemma def_coinduct2: "[ h==gfp(f); a:A; A <= f(A) Un h; mono(f) ] ==> a: h"


111 
apply unfold


112 
apply (erule coinduct2)


113 
apply assumption


114 
apply assumption


115 
done


116 


117 
lemma def_coinduct3: "[ h==gfp(f); a:A; A <= f(lfp(%x. f(x) Un A Un h)); mono(f) ] ==> a: h"


118 
apply unfold


119 
apply (erule coinduct3)


120 
apply assumption


121 
apply assumption


122 
done


123 


124 
(*Monotonicity of gfp!*)


125 
lemma gfp_mono: "[ mono(f); !!Z. f(Z)<=g(Z) ] ==> gfp(f) <= gfp(g)"


126 
apply (rule gfp_upperbound)


127 
apply (rule subset_trans)


128 
apply (rule gfp_lemma2)


129 
apply assumption


130 
apply (erule meta_spec)


131 
done

17456

132 

0

133 
end
