author  wenzelm 
Tue, 02 Aug 2016 21:05:34 +0200  
changeset 63588  d0e2bad67bd4 
parent 63561  fba08009ff3e 
child 63863  d14e580c3b8f 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
10402  2 
Author: Markus Wenzel, TU Muenchen 
11688  3 
*) 
10727  4 

60758  5 
section \<open>KnasterTarski Fixpoint Theorem and inductive definitions\<close> 
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 
63588  8 
imports Complete_Lattices Ctr_Sugar 
9 
keywords 

10 
"inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and 

11 
"monos" and 

12 
"print_inductives" :: diag and 

13 
"old_rep_datatype" :: thy_goal and 

14 
"primrec" :: thy_decl 

15131  15 
begin 
10727  16 

60758  17 
subsection \<open>Least and greatest fixed points\<close> 
24915  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 

63400  22 
definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>least fixed point\<close> 
23 
where "lfp f = Inf {u. f u \<le> u}" 

24915  24 

63400  25 
definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>greatest fixed point\<close> 
26 
where "gfp f = Sup {u. u \<le> f u}" 

24915  27 

28 

63400  29 
subsection \<open>Proof of KnasterTarski Theorem using @{term lfp}\<close> 
24915  30 

63400  31 
text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close> 
24915  32 

63400  33 
lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A" 
24915  34 
by (auto simp add: lfp_def intro: Inf_lower) 
35 

63400  36 
lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f" 
24915  37 
by (auto simp add: lfp_def intro: Inf_greatest) 
38 

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

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

40 

63400  41 
lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f" 
24915  42 
by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) 
43 

63400  44 
lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)" 
24915  45 
by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) 
46 

63400  47 
lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)" 
24915  48 
by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) 
49 

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

63400  51 
by (rule lfp_unfold) (simp add: mono_def) 
24915  52 

63588  53 
lemma lfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> x \<le> z) \<Longrightarrow> lfp F = x" 
54 
by (rule antisym) (simp_all add: lfp_lowerbound lfp_unfold[symmetric]) 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

55 

24915  56 

60758  57 
subsection \<open>General induction rules for least fixed points\<close> 
24915  58 

63400  59 
lemma lfp_ordinal_induct [case_names mono step union]: 
61076  60 
fixes f :: "'a::complete_lattice \<Rightarrow> 'a" 
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

61 
assumes mono: "mono f" 
63400  62 
and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)" 
63 
and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)" 

26013
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}" 
63588  67 
from P_Union have "P (Sup ?M)" by simp 
26013
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) 
63588  70 
show "Sup ?M \<le> lfp f" 
71 
by (blast intro: Sup_least) 

63400  72 
then have "f (Sup ?M) \<le> f (lfp f)" 
73 
by (rule mono [THEN monoD]) 

74 
then have "f (Sup ?M) \<le> lfp f" 

75 
using mono [THEN lfp_unfold] by simp 

76 
then have "f (Sup ?M) \<in> ?M" 

77 
using P_Union by simp (intro P_f Sup_least, auto) 

78 
then have "f (Sup ?M) \<le> Sup ?M" 

79 
by (rule Sup_upper) 

80 
then show "lfp f \<le> Sup ?M" 

81 
by (rule lfp_lowerbound) 

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

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

83 
finally show ?thesis . 
63400  84 
qed 
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

85 

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

86 
theorem lfp_induct: 
63400  87 
assumes mono: "mono f" 
88 
and ind: "f (inf (lfp f) P) \<le> P" 

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

89 
shows "lfp f \<le> P" 
63588  90 
proof (induct rule: lfp_ordinal_induct) 
91 
case mono 

92 
show ?case by fact 

93 
next 

63400  94 
case (step S) 
95 
then show ?case 

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

96 
by (intro order_trans[OF _ ind] monoD[OF mono]) auto 
63588  97 
next 
98 
case (union M) 

99 
then show ?case 

100 
by (auto intro: Sup_least) 

101 
qed 

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

102 

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

103 
lemma lfp_induct_set: 
63400  104 
assumes lfp: "a \<in> lfp f" 
105 
and mono: "mono f" 

106 
and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x" 

107 
shows "P a" 

108 
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp) 

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

109 

63400  110 
lemma lfp_ordinal_induct_set: 
24915  111 
assumes mono: "mono f" 
63400  112 
and P_f: "\<And>S. P S \<Longrightarrow> P (f S)" 
113 
and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)" 

114 
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

115 
using assms by (rule lfp_ordinal_induct) 
24915  116 

117 

63400  118 
text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close> 
24915  119 

63400  120 
lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h" 
45899  121 
by (auto intro!: lfp_unfold) 
24915  122 

63400  123 
lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P" 
24915  124 
by (blast intro: lfp_induct) 
125 

63400  126 
lemma def_lfp_induct_set: 
127 
"A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> f (A \<inter> {x. P x}) \<Longrightarrow> P x) \<Longrightarrow> P a" 

24915  128 
by (blast intro: lfp_induct_set) 
129 

63400  130 
text \<open>Monotonicity of \<open>lfp\<close>!\<close> 
131 
lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g" 

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

24915  133 

134 

63400  135 
subsection \<open>Proof of KnasterTarski Theorem using \<open>gfp\<close>\<close> 
24915  136 

63400  137 
text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close> 
24915  138 

63400  139 
lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f" 
24915  140 
by (auto simp add: gfp_def intro: Sup_upper) 
141 

63400  142 
lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X" 
24915  143 
by (auto simp add: gfp_def intro: Sup_least) 
144 

63400  145 
lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)" 
24915  146 
by (iprover intro: gfp_least order_trans monoD gfp_upperbound) 
147 

63400  148 
lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f" 
24915  149 
by (iprover intro: gfp_lemma2 monoD gfp_upperbound) 
150 

63400  151 
lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)" 
24915  152 
by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) 
153 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

154 
lemma gfp_const: "gfp (\<lambda>x. t) = t" 
63588  155 
by (rule gfp_unfold) (simp add: mono_def) 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

156 

63588  157 
lemma gfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> z \<le> x) \<Longrightarrow> gfp F = x" 
158 
by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric]) 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

159 

24915  160 

60758  161 
subsection \<open>Coinduction rules for greatest fixed points\<close> 
24915  162 

63400  163 
text \<open>Weak version.\<close> 
164 
lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f" 

45899  165 
by (rule gfp_upperbound [THEN subsetD]) auto 
24915  166 

63400  167 
lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f" 
45899  168 
apply (erule gfp_upperbound [THEN subsetD]) 
169 
apply (erule imageI) 

170 
done 

24915  171 

63400  172 
lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))" 
24915  173 
apply (frule gfp_lemma2) 
174 
apply (drule mono_sup) 

175 
apply (rule le_supI) 

63588  176 
apply assumption 
24915  177 
apply (rule order_trans) 
63588  178 
apply (rule order_trans) 
179 
apply assumption 

180 
apply (rule sup_ge2) 

24915  181 
apply assumption 
182 
done 

183 

63400  184 
text \<open>Strong version, thanks to Coen and Frost.\<close> 
185 
lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f" 

55604  186 
by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+ 
24915  187 

63400  188 
lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)" 
45899  189 
by (blast dest: gfp_lemma2 mono_Un) 
24915  190 

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

191 
lemma gfp_ordinal_induct[case_names mono step union]: 
61076  192 
fixes f :: "'a::complete_lattice \<Rightarrow> 'a" 
60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

193 
assumes mono: "mono f" 
63400  194 
and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)" 
195 
and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)" 

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

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

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

198 
let ?M = "{S. gfp f \<le> S \<and> P S}" 
63588  199 
from P_Union have "P (Inf ?M)" by simp 
60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

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

201 
proof (rule antisym) 
63400  202 
show "gfp f \<le> Inf ?M" 
203 
by (blast intro: Inf_greatest) 

204 
then have "f (gfp f) \<le> f (Inf ?M)" 

205 
by (rule mono [THEN monoD]) 

206 
then have "gfp f \<le> f (Inf ?M)" 

207 
using mono [THEN gfp_unfold] by simp 

208 
then have "f (Inf ?M) \<in> ?M" 

209 
using P_Union by simp (intro P_f Inf_greatest, auto) 

210 
then have "Inf ?M \<le> f (Inf ?M)" 

211 
by (rule Inf_lower) 

212 
then show "Inf ?M \<le> gfp f" 

213 
by (rule gfp_upperbound) 

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

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

215 
finally show ?thesis . 
63400  216 
qed 
60174
70d8f7abde8f
strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents:
60173
diff
changeset

217 

63400  218 
lemma coinduct: 
219 
assumes mono: "mono f" 

220 
and ind: "X \<le> f (sup X (gfp f))" 

221 
shows "X \<le> gfp f" 

63588  222 
proof (induct rule: gfp_ordinal_induct) 
223 
case mono 

224 
then show ?case by fact 

225 
next 

226 
case (step S) 

227 
then show ?case 

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

228 
by (intro order_trans[OF ind _] monoD[OF mono]) auto 
63588  229 
next 
230 
case (union M) 

231 
then show ?case 

232 
by (auto intro: mono Inf_greatest) 

233 
qed 

24915  234 

63400  235 

60758  236 
subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close> 
24915  237 

63400  238 
text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both 
60758  239 
@{term lfp} and @{term gfp}\<close> 
63400  240 
lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)" 
241 
by (iprover intro: subset_refl monoI Un_mono monoD) 

24915  242 

243 
lemma coinduct3_lemma: 

63400  244 
"X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow> 
245 
lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))" 

246 
apply (rule subset_trans) 

63588  247 
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) 
63400  248 
apply (rule Un_least [THEN Un_least]) 
63588  249 
apply (rule subset_refl, assumption) 
63400  250 
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) 
251 
apply (rule monoD, assumption) 

252 
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) 

253 
done 

24915  254 

63400  255 
lemma coinduct3: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> a \<in> gfp f" 
256 
apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) 

63588  257 
apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst]) 
258 
apply simp_all 

63400  259 
done 
24915  260 

63400  261 
text \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close> 
24915  262 

63400  263 
lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A" 
45899  264 
by (auto intro!: gfp_unfold) 
24915  265 

63400  266 
lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A" 
45899  267 
by (iprover intro!: coinduct) 
24915  268 

63400  269 
lemma def_coinduct_set: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> A) \<Longrightarrow> a \<in> A" 
45899  270 
by (auto intro!: coinduct_set) 
24915  271 

272 
lemma def_Collect_coinduct: 

63400  273 
"A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow> 
274 
(\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A" 

45899  275 
by (erule def_coinduct_set) auto 
24915  276 

63400  277 
lemma def_coinduct3: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> A)) \<Longrightarrow> a \<in> A" 
45899  278 
by (auto intro!: coinduct3) 
24915  279 

63400  280 
text \<open>Monotonicity of @{term gfp}!\<close> 
281 
lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g" 

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

283 

24915  284 

60758  285 
subsection \<open>Rules for fixed point calculus\<close> 
60173  286 

287 
lemma lfp_rolling: 

288 
assumes "mono g" "mono f" 

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

290 
proof (rule antisym) 

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

292 
using assms by (auto simp: mono_def) 

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

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

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

296 
proof (rule lfp_greatest) 

63400  297 
fix u 
63540  298 
assume u: "g (f u) \<le> u" 
299 
then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)" 

60173  300 
by (intro assms[THEN monoD] lfp_lowerbound) 
63540  301 
with u show "g (lfp (\<lambda>x. f (g x))) \<le> u" 
60173  302 
by auto 
303 
qed 

304 
qed 

305 

306 
lemma lfp_lfp: 

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

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

309 
proof (rule antisym) 

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

311 
by (blast intro: monoI f) 

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

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

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

315 
proof (intro lfp_lowerbound) 

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

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

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

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

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

321 
by (simp add: *[symmetric]) 

322 
qed 

323 
qed 

324 

325 
lemma gfp_rolling: 

326 
assumes "mono g" "mono f" 

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

328 
proof (rule antisym) 

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

330 
using assms by (auto simp: mono_def) 

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

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

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

334 
proof (rule gfp_least) 

63540  335 
fix u 
336 
assume u: "u \<le> g (f u)" 

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

60173  338 
by (intro assms[THEN monoD] gfp_upperbound) 
63540  339 
with u show "u \<le> g (gfp (\<lambda>x. f (g x)))" 
60173  340 
by auto 
341 
qed 

342 
qed 

343 

344 
lemma gfp_gfp: 

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

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

347 
proof (rule antisym) 

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

349 
by (blast intro: monoI f) 

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

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

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

353 
proof (intro gfp_upperbound) 

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

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

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

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

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

359 
by (simp add: *[symmetric]) 

360 
qed 

361 
qed 

24915  362 

63400  363 

60758  364 
subsection \<open>Inductive predicates and sets\<close> 
11688  365 

60758  366 
text \<open>Package setup.\<close> 
10402  367 

61337  368 
lemmas basic_monos = 
22218  369 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  370 
Collect_mono in_mono vimage_mono 
371 

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

373 

61337  374 
lemmas [mono] = 
22218  375 
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

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

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

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

379 

11688  380 

60758  381 
subsection \<open>Inductive datatypes and primitive recursion\<close> 
11688  382 

60758  383 
text \<open>Package setup.\<close> 
11825  384 

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_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

386 
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

387 
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

388 
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

389 
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

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

391 

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

392 
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

393 
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

394 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61952
diff
changeset

395 
text \<open>Lambdaabstractions with pattern matching:\<close> 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61952
diff
changeset

396 
syntax (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61952
diff
changeset

397 
"_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" ("(%_)" 10) 
23526  398 
syntax 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61952
diff
changeset

399 
"_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" ("(\<lambda>_)" 10) 
60758  400 
parse_translation \<open> 
52143  401 
let 
402 
fun fun_tr ctxt [cs] = 

403 
let 

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

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

406 
in lambda x ft end 

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

60758  408 
\<close> 
23526  409 

410 
end 