author  wenzelm 
Thu, 15 Dec 2011 17:37:14 +0100  
changeset 45890  5f70aaecae26 
parent 44860  56101fa00193 
child 45891  d73605c829cc 
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 
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
43580
diff
changeset

8 
imports Complete_Lattices 
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") 
45890  17 
("Tools/Datatype/rep_datatype.ML") 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

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

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

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

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

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

26 

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

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

31 
definition 

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

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

35 

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

37 

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

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

40 

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

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

43 

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

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

46 

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

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

48 

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

51 

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

53 
by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) 

54 

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

56 
by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) 

57 

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

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

60 

61 

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

63 

64 
theorem lfp_induct: 

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

66 
shows "lfp f <= P" 

67 
proof  

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

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

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

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

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

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

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

75 
finally show ?thesis . 

76 
qed 

77 

78 
lemma lfp_induct_set: 

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

80 
and mono: "mono(f)" 

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

82 
shows "P(a)" 

83 
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

84 
(auto simp: intro: indhyp) 
24915  85 

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

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

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

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

89 
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

90 
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

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

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

93 
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

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

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

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

97 
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

98 
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

99 
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

100 
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

101 
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

102 
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

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

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

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

106 

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

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

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

111 
shows "P(lfp f)" 

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

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

114 

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

116 
to control unfolding*} 

117 

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

119 
by (auto intro!: lfp_unfold) 

120 

121 
lemma def_lfp_induct: 

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

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

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

125 
by (blast intro: lfp_induct) 

126 

127 
lemma def_lfp_induct_set: 

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

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

130 
] ==> P(a)" 

131 
by (blast intro: lfp_induct_set) 

132 

133 
(*Monotonicity of lfp!*) 

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

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

136 

137 

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

139 

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

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

142 

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

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

145 

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

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

148 

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

150 
by (iprover intro: gfp_least order_trans monoD gfp_upperbound) 

151 

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

153 
by (iprover intro: gfp_lemma2 monoD gfp_upperbound) 

154 

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

156 
by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) 

157 

158 

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

160 

161 
text{*weak version*} 

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

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

164 

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

166 
apply (erule gfp_upperbound [THEN subsetD]) 

167 
apply (erule imageI) 

168 
done 

169 

170 
lemma coinduct_lemma: 

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

172 
apply (frule gfp_lemma2) 

173 
apply (drule mono_sup) 

174 
apply (rule le_supI) 

175 
apply assumption 

176 
apply (rule order_trans) 

177 
apply (rule order_trans) 

178 
apply assumption 

179 
apply (rule sup_ge2) 

180 
apply assumption 

181 
done 

182 

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

184 
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

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

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

188 
apply (rule order_trans) 

189 
apply (rule sup_ge1) 

190 
apply (erule gfp_upperbound [OF coinduct_lemma]) 

191 
apply assumption 

192 
done 

193 

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

195 
by (blast dest: gfp_lemma2 mono_Un) 

196 

197 

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

199 

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

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

202 

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

204 
by (iprover intro: subset_refl monoI Un_mono monoD) 

205 

206 
lemma coinduct3_lemma: 

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

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

209 
apply (rule subset_trans) 

210 
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) 

211 
apply (rule Un_least [THEN Un_least]) 

212 
apply (rule subset_refl, assumption) 

213 
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

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

217 

218 
lemma coinduct3: 

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

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

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

24915  223 
done 
224 

225 

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

227 
to control unfolding*} 

228 

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

230 
by (auto intro!: gfp_unfold) 

231 

232 
lemma def_coinduct: 

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

234 
by (iprover intro!: coinduct) 

235 

236 
lemma def_coinduct_set: 

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

238 
by (auto intro!: coinduct_set) 

239 

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

241 
lemma def_Collect_coinduct: 

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

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

244 
a : A" 

245 
apply (erule def_coinduct_set, auto) 

246 
done 

247 

248 
lemma def_coinduct3: 

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

250 
by (auto intro!: coinduct3) 

251 

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

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

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

255 

256 

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

259 
text {* Package setup. *} 

10402  260 

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

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

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

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

267 

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

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

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

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

273 

11688  274 

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

11825  277 
text {* Package setup. *} 
278 

31775  279 
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

280 
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

281 
setup Datatype_Data.setup 
31604  282 

45890  283 
use "Tools/Datatype/rep_datatype.ML" 
284 

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

285 
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

286 
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

287 

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

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

289 

23526  290 
text{* Lambdaabstractions with pattern matching: *} 
291 

292 
syntax 

23529  293 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  294 
syntax (xsymbols) 
23529  295 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  296 

23529  297 
parse_translation (advanced) {* 
298 
let 

299 
fun fun_tr ctxt [cs] = 

300 
let 

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

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

302 
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

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

308 
end 