author  krauss 
Mon, 27 Jun 2011 17:04:04 +0200  
changeset 43580  023a1d1f97bd 
parent 43324  2b47822868e4 
child 44860  56101fa00193 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
10402  2 
Author: Markus Wenzel, TU Muenchen 
11688  3 
*) 
10727  4 

24915  5 
header {* KnasterTarski Fixpoint Theorem and inductive definitions *} 
1187  6 

15131  7 
theory Inductive 
33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
32701
diff
changeset

8 
imports Complete_Lattice 
16417  9 
uses 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

10 
("Tools/inductive.ML") 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
24349
diff
changeset

11 
"Tools/dseq.ML" 
33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
32701
diff
changeset

12 
"Tools/Datatype/datatype_aux.ML" 
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
32701
diff
changeset

13 
"Tools/Datatype/datatype_prop.ML" 
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
32701
diff
changeset

14 
"Tools/Datatype/datatype_case.ML" 
31775  15 
("Tools/Datatype/datatype_abs_proofs.ML") 
33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset

16 
("Tools/Datatype/datatype_data.ML") 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

17 
("Tools/primrec.ML") 
31775  18 
("Tools/Datatype/datatype_codegen.ML") 
15131  19 
begin 
10727  20 

24915  21 
subsection {* Least and greatest fixed points *} 
22 

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

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

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

25 

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

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

30 
definition 

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

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

34 

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

36 

37 
text{*@{term "lfp f"} is the least upper bound of 

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

39 

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

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

42 

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

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

45 

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

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

47 

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

50 

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

52 
by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) 

53 

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

55 
by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) 

56 

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

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

59 

60 

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

62 

63 
theorem lfp_induct: 

64 
assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P" 

65 
shows "lfp f <= P" 

66 
proof  

67 
have "inf (lfp f) P <= lfp f" by (rule inf_le1) 

68 
with mono have "f (inf (lfp f) P) <= f (lfp f)" .. 

69 
also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric]) 

70 
finally have "f (inf (lfp f) P) <= lfp f" . 

71 
from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI) 

72 
hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound) 

73 
also have "inf (lfp f) P <= P" by (rule inf_le2) 

74 
finally show ?thesis . 

75 
qed 

76 

77 
lemma lfp_induct_set: 

78 
assumes lfp: "a: lfp(f)" 

79 
and mono: "mono(f)" 

80 
and indhyp: "!!x. [ x: f(lfp(f) Int {x. P(x)}) ] ==> P(x)" 

81 
shows "P(a)" 

82 
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) 

32683
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32587
diff
changeset

83 
(auto simp: intro: indhyp) 
24915  84 

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

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

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

87 
assumes mono: "mono f" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

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

89 
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

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

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

92 
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

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

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

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

96 
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

97 
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

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

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

100 
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

101 
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

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

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

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

105 

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

106 
lemma lfp_ordinal_induct_set: 
24915  107 
assumes mono: "mono f" 
108 
and P_f: "!!S. P S ==> P(f S)" 

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

110 
shows "P(lfp f)" 

32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
31949
diff
changeset

111 
using assms by (rule lfp_ordinal_induct [where P=P]) 
24915  112 

113 

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

115 
to control unfolding*} 

116 

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

118 
by (auto intro!: lfp_unfold) 

119 

120 
lemma def_lfp_induct: 

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

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

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

124 
by (blast intro: lfp_induct) 

125 

126 
lemma def_lfp_induct_set: 

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

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

129 
] ==> P(a)" 

130 
by (blast intro: lfp_induct_set) 

131 

132 
(*Monotonicity of lfp!*) 

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

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

135 

136 

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

138 

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

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

141 

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

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

144 

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

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

147 

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

149 
by (iprover intro: gfp_least order_trans monoD gfp_upperbound) 

150 

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

152 
by (iprover intro: gfp_lemma2 monoD gfp_upperbound) 

153 

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

155 
by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) 

156 

157 

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

159 

160 
text{*weak version*} 

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

162 
by (rule gfp_upperbound [THEN subsetD], auto) 

163 

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

165 
apply (erule gfp_upperbound [THEN subsetD]) 

166 
apply (erule imageI) 

167 
done 

168 

169 
lemma coinduct_lemma: 

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

171 
apply (frule gfp_lemma2) 

172 
apply (drule mono_sup) 

173 
apply (rule le_supI) 

174 
apply assumption 

175 
apply (rule order_trans) 

176 
apply (rule order_trans) 

177 
apply assumption 

178 
apply (rule sup_ge2) 

179 
apply assumption 

180 
done 

181 

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

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

32683
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32587
diff
changeset

184 
by (blast intro: weak_coinduct [OF _ coinduct_lemma]) 
24915  185 

186 
lemma coinduct: "[ mono(f); X \<le> f (sup X (gfp f)) ] ==> X \<le> gfp(f)" 

187 
apply (rule order_trans) 

188 
apply (rule sup_ge1) 

189 
apply (erule gfp_upperbound [OF coinduct_lemma]) 

190 
apply assumption 

191 
done 

192 

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

194 
by (blast dest: gfp_lemma2 mono_Un) 

195 

196 

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

198 

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

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

201 

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

203 
by (iprover intro: subset_refl monoI Un_mono monoD) 

204 

205 
lemma coinduct3_lemma: 

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

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

208 
apply (rule subset_trans) 

209 
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) 

210 
apply (rule Un_least [THEN Un_least]) 

211 
apply (rule subset_refl, assumption) 

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

26793
e36a92ff543e
Instantiated some rules to avoid problems with HO unification.
berghofe
parents:
26013
diff
changeset

213 
apply (rule monoD [where f=f], assumption) 
24915  214 
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) 
215 
done 

216 

217 
lemma coinduct3: 

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

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

41081  220 
apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst]) 
221 
apply (simp_all) 

24915  222 
done 
223 

224 

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

226 
to control unfolding*} 

227 

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

229 
by (auto intro!: gfp_unfold) 

230 

231 
lemma def_coinduct: 

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

233 
by (iprover intro!: coinduct) 

234 

235 
lemma def_coinduct_set: 

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

237 
by (auto intro!: coinduct_set) 

238 

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

240 
lemma def_Collect_coinduct: 

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

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

243 
a : A" 

244 
apply (erule def_coinduct_set, auto) 

245 
done 

246 

247 
lemma def_coinduct3: 

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

249 
by (auto intro!: coinduct3) 

250 

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

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

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

254 

255 

23734  256 
subsection {* Inductive predicates and sets *} 
11688  257 

258 
text {* Package setup. *} 

10402  259 

23734  260 
theorems basic_monos = 
22218  261 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  262 
Collect_mono in_mono vimage_mono 
263 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

264 
use "Tools/inductive.ML" 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

265 
setup Inductive.setup 
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

266 

23734  267 
theorems [mono] = 
22218  268 
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

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

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

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

272 

11688  273 

12023  274 
subsection {* Inductive datatypes and primitive recursion *} 
11688  275 

11825  276 
text {* Package setup. *} 
277 

31775  278 
use "Tools/Datatype/datatype_abs_proofs.ML" 
33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset

279 
use "Tools/Datatype/datatype_data.ML" 
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset

280 
setup Datatype_Data.setup 
31604  281 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33966
diff
changeset

282 
use "Tools/Datatype/datatype_codegen.ML" 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33966
diff
changeset

283 
setup Datatype_Codegen.setup 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33966
diff
changeset

284 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

285 
use "Tools/primrec.ML" 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

286 

23526  287 
text{* Lambdaabstractions with pattern matching: *} 
288 

289 
syntax 

23529  290 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  291 
syntax (xsymbols) 
23529  292 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  293 

23529  294 
parse_translation (advanced) {* 
295 
let 

296 
fun fun_tr ctxt [cs] = 

297 
let 

43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
41081
diff
changeset

298 
(* FIXME proper name context!? *) 
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
41081
diff
changeset

299 
val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT); 
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors  side effect: function package correctly identifies 0::int as a nonconstructor;
krauss
parents:
43324
diff
changeset

300 
val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs]; 
23529  301 
in lambda x ft end 
35115  302 
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end 
23526  303 
*} 
304 

305 
end 