author  wenzelm 
Thu, 23 Jul 2009 21:59:56 +0200  
changeset 32153  a0e57fb1b930 
parent 21404  eb85850d3eb7 
child 58889  5b7a9633cfa8 
permissions  rwrr 
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 

17456  6 
header {* Greatest fixed points *} 
7 

8 
theory Gfp 

9 
imports Lfp 

10 
begin 

11 

20140  12 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20140
diff
changeset

13 
gfp :: "['a set=>'a set] => 'a set" where  "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 

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

19 
unfolding gfp_def by blast 

20 

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

22 
unfolding gfp_def by blast 

23 

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

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

26 
rule gfp_upperbound, assumption) 

27 

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

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

30 

31 
lemma gfp_Tarski: "mono(f) ==> 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*) 

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

39 
by (blast dest: gfp_upperbound) 

40 

41 
lemma coinduct2_lemma: 

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

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

44 
apply (rule subset_trans) 

45 
prefer 2 

46 
apply (erule mono_Un) 

47 
apply (rule subst, erule gfp_Tarski) 

48 
apply (erule Un_least) 

49 
apply (rule Un_upper2) 

50 
done 

51 

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

53 
lemma coinduct2: 

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

55 
apply (rule coinduct) 

56 
prefer 2 

57 
apply (erule coinduct2_lemma, assumption) 

58 
apply blast 

59 
done 

60 

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

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

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

64 

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

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

67 

68 
lemma coinduct3_lemma: 

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

70 
and mono: "mono(f)" 

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

72 
apply (rule subset_trans) 

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

74 
apply (rule Un_least [THEN Un_least]) 

75 
apply (rule subset_refl) 

76 
apply (rule prem) 

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

78 
apply (rule mono [THEN monoD]) 

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

80 
apply (rule Un_upper2) 

81 
done 

82 

83 
lemma coinduct3: 

84 
assumes 1: "a:A" 

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

86 
and 3: "mono(f)" 

87 
shows "a : gfp(f)" 

88 
apply (rule coinduct) 

89 
prefer 2 

90 
apply (rule coinduct3_lemma [OF 2 3]) 

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

92 
using 1 apply blast 

93 
done 

94 

95 

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

97 

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

99 
apply unfold 

100 
apply (erule gfp_Tarski) 

101 
done 

102 

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

104 
apply unfold 

105 
apply (erule coinduct) 

106 
apply assumption 

107 
done 

108 

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

110 
apply unfold 

111 
apply (erule coinduct2) 

112 
apply assumption 

113 
apply assumption 

114 
done 

115 

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

117 
apply unfold 

118 
apply (erule coinduct3) 

119 
apply assumption 

120 
apply assumption 

121 
done 

122 

123 
(*Monotonicity of gfp!*) 

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

125 
apply (rule gfp_upperbound) 

126 
apply (rule subset_trans) 

127 
apply (rule gfp_lemma2) 

128 
apply assumption 

129 
apply (erule meta_spec) 

130 
done 

17456  131 

0  132 
end 