author  hoelzl 
Mon, 04 May 2015 18:49:51 +0200  
changeset 60174  70d8f7abde8f 
parent 60173  6a61bb577d5b 
child 60636  ee18efe9b246 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
10402  2 
Author: Markus Wenzel, TU Muenchen 
11688  3 
*) 
10727  4 

58889  5 
section {* KnasterTarski Fixpoint Theorem and inductive definitions *} 
1187  6 

54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52143
diff
changeset

7 
theory Inductive 
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52143
diff
changeset

8 
imports Complete_Lattices Ctr_Sugar 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

9 
keywords 
56146
8453d35e4684
discontinued somewhat pointless "thy_script" keyword kind;
wenzelm
parents:
55604
diff
changeset

10 
"inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and 
8453d35e4684
discontinued somewhat pointless "thy_script" keyword kind;
wenzelm
parents:
55604
diff
changeset

11 
"monos" and 
54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52143
diff
changeset

12 
"print_inductives" :: diag and 
58306
117ba6cbe414
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet
parents:
58187
diff
changeset

13 
"old_rep_datatype" :: thy_goal and 
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

14 
"primrec" :: thy_decl 
15131  15 
begin 
10727  16 

24915  17 
subsection {* Least and greatest fixed points *} 
18 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

19 
context complete_lattice 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

20 
begin 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

21 

24915  22 
definition 
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

23 
lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where 
24915  24 
"lfp f = Inf {u. f u \<le> u}" {*least fixed point*} 
25 

26 
definition 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

27 
gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where 
24915  28 
"gfp f = Sup {u. u \<le> f u}" {*greatest fixed point*} 
29 

30 

31 
subsection{* Proof of KnasterTarski Theorem using @{term lfp} *} 

32 

54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
52143
diff
changeset

33 
text{*@{term "lfp f"} is the least upper bound of 
24915  34 
the set @{term "{u. f(u) \<le> u}"} *} 
35 

36 
lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A" 

37 
by (auto simp add: lfp_def intro: Inf_lower) 

38 

39 
lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f" 

40 
by (auto simp add: lfp_def intro: Inf_greatest) 

41 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

42 
end 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

43 

24915  44 
lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f" 
45 
by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) 

46 

47 
lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)" 

48 
by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) 

49 

50 
lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)" 

51 
by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) 

52 

53 
lemma lfp_const: "lfp (\<lambda>x. t) = t" 

54 
by (rule lfp_unfold) (simp add:mono_def) 

55 

56 

57 
subsection {* General induction rules for least fixed points *} 

58 

60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

59 
lemma lfp_ordinal_induct[case_names mono step union]: 
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

60 
fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

61 
assumes mono: "mono f" 
60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

62 
and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)" 
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

63 
and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

64 
shows "P (lfp f)" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

65 
proof  
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

66 
let ?M = "{S. S \<le> lfp f \<and> P S}" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

67 
have "P (Sup ?M)" using P_Union by simp 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

68 
also have "Sup ?M = lfp f" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

69 
proof (rule antisym) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

70 
show "Sup ?M \<le> lfp f" by (blast intro: Sup_least) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

71 
hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD]) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

72 
hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp 
60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

73 
hence "f (Sup ?M) \<in> ?M" using P_Union by simp (intro P_f Sup_least, auto) 
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

74 
hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

75 
thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

76 
qed 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

77 
finally show ?thesis . 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

78 
qed 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

79 

60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

80 
theorem lfp_induct: 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

81 
assumes mono: "mono f" and ind: "f (inf (lfp f) P) \<le> P" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

82 
shows "lfp f \<le> P" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

83 
proof (induction rule: lfp_ordinal_induct) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

84 
case (step S) then show ?case 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

85 
by (intro order_trans[OF _ ind] monoD[OF mono]) auto 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

86 
qed (auto intro: mono Sup_least) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

87 

70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

88 
lemma lfp_induct_set: 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

89 
assumes lfp: "a: lfp(f)" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

90 
and mono: "mono(f)" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

91 
and indhyp: "!!x. [ x: f(lfp(f) Int {x. P(x)}) ] ==> P(x)" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

92 
shows "P(a)" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

93 
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

94 
(auto simp: intro: indhyp) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

95 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

96 
lemma lfp_ordinal_induct_set: 
24915  97 
assumes mono: "mono f" 
98 
and P_f: "!!S. P S ==> P(f S)" 

99 
and P_Union: "!!M. !S:M. P S ==> P(Union M)" 

100 
shows "P(lfp f)" 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
45907
diff
changeset

101 
using assms by (rule lfp_ordinal_induct) 
24915  102 

103 

104 
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 

105 
to control unfolding*} 

106 

107 
lemma def_lfp_unfold: "[ h==lfp(f); mono(f) ] ==> h = f(h)" 

45899  108 
by (auto intro!: lfp_unfold) 
24915  109 

110 
lemma def_lfp_induct: 

111 
"[ A == lfp(f); mono(f); 

112 
f (inf A P) \<le> P 

113 
] ==> A \<le> P" 

114 
by (blast intro: lfp_induct) 

115 

116 
lemma def_lfp_induct_set: 

117 
"[ A == lfp(f); mono(f); a:A; 

118 
!!x. [ x: f(A Int {x. P(x)}) ] ==> P(x) 

119 
] ==> P(a)" 

120 
by (blast intro: lfp_induct_set) 

121 

122 
(*Monotonicity of lfp!*) 

123 
lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g" 

124 
by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans) 

125 

126 

127 
subsection {* Proof of KnasterTarski Theorem using @{term gfp} *} 

128 

129 
text{*@{term "gfp f"} is the greatest lower bound of 

130 
the set @{term "{u. u \<le> f(u)}"} *} 

131 

132 
lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f" 

133 
by (auto simp add: gfp_def intro: Sup_upper) 

134 

135 
lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X" 

136 
by (auto simp add: gfp_def intro: Sup_least) 

137 

138 
lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)" 

139 
by (iprover intro: gfp_least order_trans monoD gfp_upperbound) 

140 

141 
lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f" 

142 
by (iprover intro: gfp_lemma2 monoD gfp_upperbound) 

143 

144 
lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)" 

145 
by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) 

146 

147 

148 
subsection {* Coinduction rules for greatest fixed points *} 

149 

150 
text{*weak version*} 

151 
lemma weak_coinduct: "[ a: X; X \<subseteq> f(X) ] ==> a : gfp(f)" 

45899  152 
by (rule gfp_upperbound [THEN subsetD]) auto 
24915  153 

154 
lemma weak_coinduct_image: "!!X. [ a : X; g`X \<subseteq> f (g`X) ] ==> g a : gfp f" 

45899  155 
apply (erule gfp_upperbound [THEN subsetD]) 
156 
apply (erule imageI) 

157 
done 

24915  158 

159 
lemma coinduct_lemma: 

160 
"[ X \<le> f (sup X (gfp f)); mono f ] ==> sup X (gfp f) \<le> f (sup X (gfp f))" 

161 
apply (frule gfp_lemma2) 

162 
apply (drule mono_sup) 

163 
apply (rule le_supI) 

164 
apply assumption 

165 
apply (rule order_trans) 

166 
apply (rule order_trans) 

167 
apply assumption 

168 
apply (rule sup_ge2) 

169 
apply assumption 

170 
done 

171 

172 
text{*strong version, thanks to Coen and Frost*} 

173 
lemma coinduct_set: "[ mono(f); a: X; X \<subseteq> f(X Un gfp(f)) ] ==> a : gfp(f)" 

55604  174 
by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+ 
24915  175 

176 
lemma gfp_fun_UnI2: "[ mono(f); a: gfp(f) ] ==> a: f(X Un gfp(f))" 

45899  177 
by (blast dest: gfp_lemma2 mono_Un) 
24915  178 

60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

179 
lemma gfp_ordinal_induct[case_names mono step union]: 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

180 
fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

181 
assumes mono: "mono f" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

182 
and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

183 
and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

184 
shows "P (gfp f)" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

185 
proof  
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

186 
let ?M = "{S. gfp f \<le> S \<and> P S}" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

187 
have "P (Inf ?M)" using P_Union by simp 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

188 
also have "Inf ?M = gfp f" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

189 
proof (rule antisym) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

190 
show "gfp f \<le> Inf ?M" by (blast intro: Inf_greatest) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

191 
hence "f (gfp f) \<le> f (Inf ?M)" by (rule mono [THEN monoD]) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

192 
hence "gfp f \<le> f (Inf ?M)" using mono [THEN gfp_unfold] by simp 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

193 
hence "f (Inf ?M) \<in> ?M" using P_Union by simp (intro P_f Inf_greatest, auto) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

194 
hence "Inf ?M \<le> f (Inf ?M)" by (rule Inf_lower) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

195 
thus "Inf ?M \<le> gfp f" by (rule gfp_upperbound) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

196 
qed 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

197 
finally show ?thesis . 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

198 
qed 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

199 

70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

200 
lemma coinduct: assumes mono: "mono f" and ind: "X \<le> f (sup X (gfp f))" shows "X \<le> gfp f" 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

201 
proof (induction rule: gfp_ordinal_induct) 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

202 
case (step S) then show ?case 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

203 
by (intro order_trans[OF ind _] monoD[OF mono]) auto 
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

204 
qed (auto intro: mono Inf_greatest) 
24915  205 

206 
subsection {* Even Stronger Coinduction Rule, by Martin Coen *} 

207 

208 
text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both 

209 
@{term lfp} and @{term gfp}*} 

210 

211 
lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)" 

212 
by (iprover intro: subset_refl monoI Un_mono monoD) 

213 

214 
lemma coinduct3_lemma: 

215 
"[ X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) ] 

216 
==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))" 

217 
apply (rule subset_trans) 

218 
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) 

219 
apply (rule Un_least [THEN Un_least]) 

220 
apply (rule subset_refl, assumption) 

221 
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
45907
diff
changeset

222 
apply (rule monoD, assumption) 
24915  223 
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) 
224 
done 

225 

226 
lemma coinduct3: 

227 
"[ mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) ] ==> a : gfp(f)" 

228 
apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) 

41081  229 
apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst]) 
230 
apply (simp_all) 

24915  231 
done 
232 

233 

234 
text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, 

235 
to control unfolding*} 

236 

237 
lemma def_gfp_unfold: "[ A==gfp(f); mono(f) ] ==> A = f(A)" 

45899  238 
by (auto intro!: gfp_unfold) 
24915  239 

240 
lemma def_coinduct: 

241 
"[ A==gfp(f); mono(f); X \<le> f(sup X A) ] ==> X \<le> A" 

45899  242 
by (iprover intro!: coinduct) 
24915  243 

244 
lemma def_coinduct_set: 

245 
"[ A==gfp(f); mono(f); a:X; X \<subseteq> f(X Un A) ] ==> a: A" 

45899  246 
by (auto intro!: coinduct_set) 
24915  247 

248 
(*The version used in the induction/coinduction package*) 

249 
lemma def_Collect_coinduct: 

250 
"[ A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); 

251 
a: X; !!z. z: X ==> P (X Un A) z ] ==> 

252 
a : A" 

45899  253 
by (erule def_coinduct_set) auto 
24915  254 

255 
lemma def_coinduct3: 

256 
"[ A==gfp(f); mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un A)) ] ==> a: A" 

45899  257 
by (auto intro!: coinduct3) 
24915  258 

259 
text{*Monotonicity of @{term gfp}!*} 

260 
lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g" 

261 
by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) 

262 

60173  263 
subsection {* Rules for fixed point calculus *} 
264 

265 

266 
lemma lfp_rolling: 

267 
assumes "mono g" "mono f" 

268 
shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))" 

269 
proof (rule antisym) 

270 
have *: "mono (\<lambda>x. f (g x))" 

271 
using assms by (auto simp: mono_def) 

272 

273 
show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))" 

274 
by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric]) 

275 

276 
show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))" 

277 
proof (rule lfp_greatest) 

278 
fix u assume "g (f u) \<le> u" 

279 
moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)" 

280 
by (intro assms[THEN monoD] lfp_lowerbound) 

281 
ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u" 

282 
by auto 

283 
qed 

284 
qed 

285 

286 
lemma lfp_square: 

287 
assumes "mono f" shows "lfp f = lfp (\<lambda>x. f (f x))" 

288 
proof (rule antisym) 

289 
show "lfp f \<le> lfp (\<lambda>x. f (f x))" 

290 
by (intro lfp_lowerbound) (simp add: assms lfp_rolling) 

291 
show "lfp (\<lambda>x. f (f x)) \<le> lfp f" 

292 
by (intro lfp_lowerbound) (simp add: lfp_unfold[OF assms, symmetric]) 

293 
qed 

294 

295 
lemma lfp_lfp: 

296 
assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z" 

297 
shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)" 

298 
proof (rule antisym) 

299 
have *: "mono (\<lambda>x. f x x)" 

300 
by (blast intro: monoI f) 

301 
show "lfp (\<lambda>x. lfp (f x)) \<le> lfp (\<lambda>x. f x x)" 

302 
by (intro lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric]) 

303 
show "lfp (\<lambda>x. lfp (f x)) \<ge> lfp (\<lambda>x. f x x)" (is "?F \<ge> _") 

304 
proof (intro lfp_lowerbound) 

305 
have *: "?F = lfp (f ?F)" 

306 
by (rule lfp_unfold) (blast intro: monoI lfp_mono f) 

307 
also have "\<dots> = f ?F (lfp (f ?F))" 

308 
by (rule lfp_unfold) (blast intro: monoI lfp_mono f) 

309 
finally show "f ?F ?F \<le> ?F" 

310 
by (simp add: *[symmetric]) 

311 
qed 

312 
qed 

313 

314 
lemma gfp_rolling: 

315 
assumes "mono g" "mono f" 

316 
shows "g (gfp (\<lambda>x. f (g x))) = gfp (\<lambda>x. g (f x))" 

317 
proof (rule antisym) 

318 
have *: "mono (\<lambda>x. f (g x))" 

319 
using assms by (auto simp: mono_def) 

320 
show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))" 

321 
by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric]) 

322 

323 
show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))" 

324 
proof (rule gfp_least) 

325 
fix u assume "u \<le> g (f u)" 

326 
moreover then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))" 

327 
by (intro assms[THEN monoD] gfp_upperbound) 

328 
ultimately show "u \<le> g (gfp (\<lambda>x. f (g x)))" 

329 
by auto 

330 
qed 

331 
qed 

332 

333 
lemma gfp_square: 

334 
assumes "mono f" shows "gfp f = gfp (\<lambda>x. f (f x))" 

335 
proof (rule antisym) 

336 
show "gfp (\<lambda>x. f (f x)) \<le> gfp f" 

337 
by (intro gfp_upperbound) (simp add: assms gfp_rolling) 

338 
show "gfp f \<le> gfp (\<lambda>x. f (f x))" 

339 
by (intro gfp_upperbound) (simp add: gfp_unfold[OF assms, symmetric]) 

340 
qed 

341 

342 
lemma gfp_gfp: 

343 
assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z" 

344 
shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)" 

345 
proof (rule antisym) 

346 
have *: "mono (\<lambda>x. f x x)" 

347 
by (blast intro: monoI f) 

348 
show "gfp (\<lambda>x. f x x) \<le> gfp (\<lambda>x. gfp (f x))" 

349 
by (intro gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric]) 

350 
show "gfp (\<lambda>x. gfp (f x)) \<le> gfp (\<lambda>x. f x x)" (is "?F \<le> _") 

351 
proof (intro gfp_upperbound) 

352 
have *: "?F = gfp (f ?F)" 

353 
by (rule gfp_unfold) (blast intro: monoI gfp_mono f) 

354 
also have "\<dots> = f ?F (gfp (f ?F))" 

355 
by (rule gfp_unfold) (blast intro: monoI gfp_mono f) 

356 
finally show "?F \<le> f ?F ?F" 

357 
by (simp add: *[symmetric]) 

358 
qed 

359 
qed 

24915  360 

23734  361 
subsection {* Inductive predicates and sets *} 
11688  362 

363 
text {* Package setup. *} 

10402  364 

23734  365 
theorems basic_monos = 
22218  366 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  367 
Collect_mono in_mono vimage_mono 
368 

48891  369 
ML_file "Tools/inductive.ML" 
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

370 

23734  371 
theorems [mono] = 
22218  372 
imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
33934
25d6a8982e37
Streamlined setup for monotonicity rules (no longer requires classical rules).
berghofe
parents:
32701
diff
changeset

373 
imp_mono not_mono 
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

374 
Ball_def Bex_def 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

375 
induct_rulify_fallback 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

376 

11688  377 

12023  378 
subsection {* Inductive datatypes and primitive recursion *} 
11688  379 

11825  380 
text {* Package setup. *} 
381 

58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
56146
diff
changeset

382 
ML_file "Tools/Old_Datatype/old_datatype_aux.ML" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
56146
diff
changeset

383 
ML_file "Tools/Old_Datatype/old_datatype_prop.ML" 
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset

384 
ML_file "Tools/Old_Datatype/old_datatype_data.ML" 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
56146
diff
changeset

385 
ML_file "Tools/Old_Datatype/old_rep_datatype.ML" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
56146
diff
changeset

386 
ML_file "Tools/Old_Datatype/old_datatype_codegen.ML" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
56146
diff
changeset

387 
ML_file "Tools/Old_Datatype/old_primrec.ML" 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

388 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

389 
ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML" 
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

390 
ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML" 
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

391 

23526  392 
text{* Lambdaabstractions with pattern matching: *} 
393 

394 
syntax 

23529  395 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  396 
syntax (xsymbols) 
23529  397 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  398 

52143  399 
parse_translation {* 
400 
let 

401 
fun fun_tr ctxt [cs] = 

402 
let 

403 
val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context))); 

404 
val ft = Case_Translation.case_tr true ctxt [x, cs]; 

405 
in lambda x ft end 

406 
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end 

23526  407 
*} 
408 

409 
end 