author  wenzelm 
Tue, 06 Oct 2015 15:14:28 +0200  
changeset 61337  4645502c3c64 
parent 61076  bdc1e2f0a86a 
child 61799  4cf66f21b764 
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 
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 

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 

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 
60758  24 
"lfp f = Inf {u. f u \<le> u}" \<open>least fixed point\<close> 
24915  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 
60758  28 
"gfp f = Sup {u. u \<le> f u}" \<open>greatest fixed point\<close> 
24915  29 

30 

60758  31 
subsection\<open>Proof of KnasterTarski Theorem using @{term lfp}\<close> 
24915  32 

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

24915  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 

60758  57 
subsection \<open>General induction rules for least fixed points\<close> 
24915  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]: 
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" 
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 

60758  104 
text\<open>Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
105 
to control unfolding\<close> 

24915  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 

60758  127 
subsection \<open>Proof of KnasterTarski Theorem using @{term gfp}\<close> 
24915  128 

60758  129 
text\<open>@{term "gfp f"} is the greatest lower bound of 
130 
the set @{term "{u. u \<le> f(u)}"}\<close> 

24915  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 

60758  148 
subsection \<open>Coinduction rules for greatest fixed points\<close> 
24915  149 

60758  150 
text\<open>weak version\<close> 
24915  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 

60758  172 
text\<open>strong version, thanks to Coen and Frost\<close> 
24915  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]: 
61076  180 
fixes f :: "'a::complete_lattice \<Rightarrow> 'a" 
60174
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 

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

60758  208 
text\<open>Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both 
209 
@{term lfp} and @{term gfp}\<close> 

24915  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 

60758  233 
text\<open>Definition forms of @{text gfp_unfold} and @{text coinduct}, 
234 
to control unfolding\<close> 

24915  235 

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

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

239 
lemma def_coinduct: 

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

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

243 
lemma def_coinduct_set: 

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

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

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

248 
lemma def_Collect_coinduct: 

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

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

251 
a : A" 

45899  252 
by (erule def_coinduct_set) auto 
24915  253 

254 
lemma def_coinduct3: 

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

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

60758  258 
text\<open>Monotonicity of @{term gfp}!\<close> 
24915  259 
lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g" 
260 
by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) 

261 

60758  262 
subsection \<open>Rules for fixed point calculus\<close> 
60173  263 

264 

265 
lemma lfp_rolling: 

266 
assumes "mono g" "mono f" 

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

268 
proof (rule antisym) 

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

270 
using assms by (auto simp: mono_def) 

271 

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

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

274 

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

276 
proof (rule lfp_greatest) 

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

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

279 
by (intro assms[THEN monoD] lfp_lowerbound) 

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

281 
by auto 

282 
qed 

283 
qed 

284 

285 
lemma lfp_lfp: 

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

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

288 
proof (rule antisym) 

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

290 
by (blast intro: monoI f) 

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

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

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

294 
proof (intro lfp_lowerbound) 

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

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

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

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

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

300 
by (simp add: *[symmetric]) 

301 
qed 

302 
qed 

303 

304 
lemma gfp_rolling: 

305 
assumes "mono g" "mono f" 

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

307 
proof (rule antisym) 

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

309 
using assms by (auto simp: mono_def) 

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

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

312 

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

314 
proof (rule gfp_least) 

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

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

317 
by (intro assms[THEN monoD] gfp_upperbound) 

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

319 
by auto 

320 
qed 

321 
qed 

322 

323 
lemma gfp_gfp: 

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

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

326 
proof (rule antisym) 

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

328 
by (blast intro: monoI f) 

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

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

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

332 
proof (intro gfp_upperbound) 

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

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

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

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

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

338 
by (simp add: *[symmetric]) 

339 
qed 

340 
qed 

24915  341 

60758  342 
subsection \<open>Inductive predicates and sets\<close> 
11688  343 

60758  344 
text \<open>Package setup.\<close> 
10402  345 

61337  346 
lemmas basic_monos = 
22218  347 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  348 
Collect_mono in_mono vimage_mono 
349 

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

351 

61337  352 
lemmas [mono] = 
22218  353 
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

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

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

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

357 

11688  358 

60758  359 
subsection \<open>Inductive datatypes and primitive recursion\<close> 
11688  360 

60758  361 
text \<open>Package setup.\<close> 
11825  362 

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

363 
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

364 
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

365 
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

366 
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

367 
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

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

369 

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

370 
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

371 
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

372 

60758  373 
text\<open>Lambdaabstractions with pattern matching:\<close> 
23526  374 

375 
syntax 

23529  376 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  377 
syntax (xsymbols) 
23529  378 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  379 

60758  380 
parse_translation \<open> 
52143  381 
let 
382 
fun fun_tr ctxt [cs] = 

383 
let 

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

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

386 
in lambda x ft end 

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

60758  388 
\<close> 
23526  389 

390 
end 