author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 20140  98acc6d0fab6 
child 32153  a0e57fb1b930 
permissions  rwrr 
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 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20140
diff
changeset

14 
gfp :: "['a set=>'a set] => 'a set" where  "greatest fixed point" 
17456  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 