author | wenzelm |
Sun, 17 Dec 2023 21:12:18 +0100 | |
changeset 79270 | 90c5aadcc4b2 |
parent 76216 | 9fc34f76b4e8 |
permissions | -rw-r--r-- |
35762 | 1 |
(* Title: ZF/Fixedpt.thy |
1478 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1992 University of Cambridge |
4 |
*) |
|
5 |
||
60770 | 6 |
section\<open>Least and Greatest Fixed Points; the Knaster-Tarski Theorem\<close> |
13356 | 7 |
|
16417 | 8 |
theory Fixedpt imports equalities begin |
13218 | 9 |
|
24893 | 10 |
definition |
13218 | 11 |
(*monotone operator from Pow(D) to itself*) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
12 |
bnd_mono :: "[i,i\<Rightarrow>i]\<Rightarrow>o" where |
76214 | 13 |
"bnd_mono(D,h) \<equiv> h(D)<=D \<and> (\<forall>W X. W<=X \<longrightarrow> X<=D \<longrightarrow> h(W) \<subseteq> h(X))" |
13218 | 14 |
|
24893 | 15 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
16 |
lfp :: "[i,i\<Rightarrow>i]\<Rightarrow>i" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
17 |
"lfp(D,h) \<equiv> \<Inter>({X: Pow(D). h(X) \<subseteq> X})" |
13218 | 18 |
|
24893 | 19 |
definition |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
20 |
gfp :: "[i,i\<Rightarrow>i]\<Rightarrow>i" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
21 |
"gfp(D,h) \<equiv> \<Union>({X: Pow(D). X \<subseteq> h(X)})" |
13218 | 22 |
|
69593 | 23 |
text\<open>The theorem is proved in the lattice of subsets of \<^term>\<open>D\<close>, |
24 |
namely \<^term>\<open>Pow(D)\<close>, with Inter as the greatest lower bound.\<close> |
|
13218 | 25 |
|
60770 | 26 |
subsection\<open>Monotone Operators\<close> |
13218 | 27 |
|
28 |
lemma bnd_monoI: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
29 |
"\<lbrakk>h(D)<=D; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
30 |
\<And>W X. \<lbrakk>W<=D; X<=D; W<=X\<rbrakk> \<Longrightarrow> h(W) \<subseteq> h(X) |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
31 |
\<rbrakk> \<Longrightarrow> bnd_mono(D,h)" |
13218 | 32 |
by (unfold bnd_mono_def, clarify, blast) |
33 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
34 |
lemma bnd_monoD1: "bnd_mono(D,h) \<Longrightarrow> h(D) \<subseteq> D" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
35 |
unfolding bnd_mono_def |
13218 | 36 |
apply (erule conjunct1) |
37 |
done |
|
38 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
39 |
lemma bnd_monoD2: "\<lbrakk>bnd_mono(D,h); W<=X; X<=D\<rbrakk> \<Longrightarrow> h(W) \<subseteq> h(X)" |
13218 | 40 |
by (unfold bnd_mono_def, blast) |
41 |
||
42 |
lemma bnd_mono_subset: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
43 |
"\<lbrakk>bnd_mono(D,h); X<=D\<rbrakk> \<Longrightarrow> h(X) \<subseteq> D" |
13218 | 44 |
by (unfold bnd_mono_def, clarify, blast) |
45 |
||
46 |
lemma bnd_mono_Un: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
47 |
"\<lbrakk>bnd_mono(D,h); A \<subseteq> D; B \<subseteq> D\<rbrakk> \<Longrightarrow> h(A) \<union> h(B) \<subseteq> h(A \<union> B)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
48 |
unfolding bnd_mono_def |
13218 | 49 |
apply (rule Un_least, blast+) |
50 |
done |
|
51 |
||
13220 | 52 |
(*unused*) |
53 |
lemma bnd_mono_UN: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
54 |
"\<lbrakk>bnd_mono(D,h); \<forall>i\<in>I. A(i) \<subseteq> D\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
55 |
\<Longrightarrow> (\<Union>i\<in>I. h(A(i))) \<subseteq> h((\<Union>i\<in>I. A(i)))" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
56 |
unfolding bnd_mono_def |
13220 | 57 |
apply (rule UN_least) |
58 |
apply (elim conjE) |
|
59 |
apply (drule_tac x="A(i)" in spec) |
|
60 |
apply (drule_tac x="(\<Union>i\<in>I. A(i))" in spec) |
|
61 |
apply blast |
|
62 |
done |
|
63 |
||
13218 | 64 |
(*Useful??*) |
65 |
lemma bnd_mono_Int: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
66 |
"\<lbrakk>bnd_mono(D,h); A \<subseteq> D; B \<subseteq> D\<rbrakk> \<Longrightarrow> h(A \<inter> B) \<subseteq> h(A) \<inter> h(B)" |
13218 | 67 |
apply (rule Int_greatest) |
68 |
apply (erule bnd_monoD2, rule Int_lower1, assumption) |
|
69 |
apply (erule bnd_monoD2, rule Int_lower2, assumption) |
|
70 |
done |
|
71 |
||
69593 | 72 |
subsection\<open>Proof of Knaster-Tarski Theorem using \<^term>\<open>lfp\<close>\<close> |
13218 | 73 |
|
74 |
(*lfp is contained in each pre-fixedpoint*) |
|
75 |
lemma lfp_lowerbound: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
76 |
"\<lbrakk>h(A) \<subseteq> A; A<=D\<rbrakk> \<Longrightarrow> lfp(D,h) \<subseteq> A" |
13218 | 77 |
by (unfold lfp_def, blast) |
78 |
||
79 |
(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) |
|
46820 | 80 |
lemma lfp_subset: "lfp(D,h) \<subseteq> D" |
13218 | 81 |
by (unfold lfp_def Inter_def, blast) |
82 |
||
83 |
(*Used in datatype package*) |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
84 |
lemma def_lfp_subset: "A \<equiv> lfp(D,h) \<Longrightarrow> A \<subseteq> D" |
13218 | 85 |
apply simp |
86 |
apply (rule lfp_subset) |
|
87 |
done |
|
88 |
||
89 |
lemma lfp_greatest: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
90 |
"\<lbrakk>h(D) \<subseteq> D; \<And>X. \<lbrakk>h(X) \<subseteq> X; X<=D\<rbrakk> \<Longrightarrow> A<=X\<rbrakk> \<Longrightarrow> A \<subseteq> lfp(D,h)" |
13218 | 91 |
by (unfold lfp_def, blast) |
92 |
||
93 |
lemma lfp_lemma1: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
94 |
"\<lbrakk>bnd_mono(D,h); h(A)<=A; A<=D\<rbrakk> \<Longrightarrow> h(lfp(D,h)) \<subseteq> A" |
13218 | 95 |
apply (erule bnd_monoD2 [THEN subset_trans]) |
96 |
apply (rule lfp_lowerbound, assumption+) |
|
97 |
done |
|
3923 | 98 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
99 |
lemma lfp_lemma2: "bnd_mono(D,h) \<Longrightarrow> h(lfp(D,h)) \<subseteq> lfp(D,h)" |
13218 | 100 |
apply (rule bnd_monoD1 [THEN lfp_greatest]) |
101 |
apply (rule_tac [2] lfp_lemma1) |
|
102 |
apply (assumption+) |
|
103 |
done |
|
104 |
||
105 |
lemma lfp_lemma3: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
106 |
"bnd_mono(D,h) \<Longrightarrow> lfp(D,h) \<subseteq> h(lfp(D,h))" |
13218 | 107 |
apply (rule lfp_lowerbound) |
108 |
apply (rule bnd_monoD2, assumption) |
|
109 |
apply (rule lfp_lemma2, assumption) |
|
110 |
apply (erule_tac [2] bnd_mono_subset) |
|
111 |
apply (rule lfp_subset)+ |
|
112 |
done |
|
113 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
114 |
lemma lfp_unfold: "bnd_mono(D,h) \<Longrightarrow> lfp(D,h) = h(lfp(D,h))" |
13218 | 115 |
apply (rule equalityI) |
116 |
apply (erule lfp_lemma3) |
|
117 |
apply (erule lfp_lemma2) |
|
118 |
done |
|
119 |
||
120 |
(*Definition form, to control unfolding*) |
|
121 |
lemma def_lfp_unfold: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
122 |
"\<lbrakk>A\<equiv>lfp(D,h); bnd_mono(D,h)\<rbrakk> \<Longrightarrow> A = h(A)" |
13218 | 123 |
apply simp |
124 |
apply (erule lfp_unfold) |
|
125 |
done |
|
126 |
||
60770 | 127 |
subsection\<open>General Induction Rule for Least Fixedpoints\<close> |
13218 | 128 |
|
129 |
lemma Collect_is_pre_fixedpt: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
130 |
"\<lbrakk>bnd_mono(D,h); \<And>x. x \<in> h(Collect(lfp(D,h),P)) \<Longrightarrow> P(x)\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
131 |
\<Longrightarrow> h(Collect(lfp(D,h),P)) \<subseteq> Collect(lfp(D,h),P)" |
13218 | 132 |
by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD] |
133 |
lfp_subset [THEN subsetD]) |
|
134 |
||
135 |
(*This rule yields an induction hypothesis in which the components of a |
|
136 |
data structure may be assumed to be elements of lfp(D,h)*) |
|
137 |
lemma induct: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
138 |
"\<lbrakk>bnd_mono(D,h); a \<in> lfp(D,h); |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
139 |
\<And>x. x \<in> h(Collect(lfp(D,h),P)) \<Longrightarrow> P(x) |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
140 |
\<rbrakk> \<Longrightarrow> P(a)" |
13218 | 141 |
apply (rule Collect_is_pre_fixedpt |
142 |
[THEN lfp_lowerbound, THEN subsetD, THEN CollectD2]) |
|
143 |
apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]], |
|
144 |
blast+) |
|
145 |
done |
|
146 |
||
147 |
(*Definition form, to control unfolding*) |
|
148 |
lemma def_induct: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
149 |
"\<lbrakk>A \<equiv> lfp(D,h); bnd_mono(D,h); a:A; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
150 |
\<And>x. x \<in> h(Collect(A,P)) \<Longrightarrow> P(x) |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
151 |
\<rbrakk> \<Longrightarrow> P(a)" |
13218 | 152 |
by (rule induct, blast+) |
153 |
||
154 |
(*This version is useful when "A" is not a subset of D |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
155 |
second premise could simply be h(D \<inter> A) \<subseteq> D or \<And>X. X<=D \<Longrightarrow> h(X)<=D *) |
13218 | 156 |
lemma lfp_Int_lowerbound: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
157 |
"\<lbrakk>h(D \<inter> A) \<subseteq> A; bnd_mono(D,h)\<rbrakk> \<Longrightarrow> lfp(D,h) \<subseteq> A" |
13218 | 158 |
apply (rule lfp_lowerbound [THEN subset_trans]) |
159 |
apply (erule bnd_mono_subset [THEN Int_greatest], blast+) |
|
160 |
done |
|
161 |
||
162 |
(*Monotonicity of lfp, where h precedes i under a domain-like partial order |
|
163 |
monotonicity of h is not strictly necessary; h must be bounded by D*) |
|
164 |
lemma lfp_mono: |
|
165 |
assumes hmono: "bnd_mono(D,h)" |
|
166 |
and imono: "bnd_mono(E,i)" |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
167 |
and subhi: "\<And>X. X<=D \<Longrightarrow> h(X) \<subseteq> i(X)" |
46820 | 168 |
shows "lfp(D,h) \<subseteq> lfp(E,i)" |
13218 | 169 |
apply (rule bnd_monoD1 [THEN lfp_greatest]) |
170 |
apply (rule imono) |
|
171 |
apply (rule hmono [THEN [2] lfp_Int_lowerbound]) |
|
172 |
apply (rule Int_lower1 [THEN subhi, THEN subset_trans]) |
|
173 |
apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) |
|
174 |
done |
|
0 | 175 |
|
13218 | 176 |
(*This (unused) version illustrates that monotonicity is not really needed, |
177 |
but both lfp's must be over the SAME set D; Inter is anti-monotonic!*) |
|
178 |
lemma lfp_mono2: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
179 |
"\<lbrakk>i(D) \<subseteq> D; \<And>X. X<=D \<Longrightarrow> h(X) \<subseteq> i(X)\<rbrakk> \<Longrightarrow> lfp(D,h) \<subseteq> lfp(D,i)" |
13218 | 180 |
apply (rule lfp_greatest, assumption) |
181 |
apply (rule lfp_lowerbound, blast, assumption) |
|
182 |
done |
|
183 |
||
14046 | 184 |
lemma lfp_cong: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
185 |
"\<lbrakk>D=D'; \<And>X. X \<subseteq> D' \<Longrightarrow> h(X) = h'(X)\<rbrakk> \<Longrightarrow> lfp(D,h) = lfp(D',h')" |
14046 | 186 |
apply (simp add: lfp_def) |
187 |
apply (rule_tac t=Inter in subst_context) |
|
188 |
apply (rule Collect_cong, simp_all) |
|
189 |
done |
|
13218 | 190 |
|
14046 | 191 |
|
69593 | 192 |
subsection\<open>Proof of Knaster-Tarski Theorem using \<^term>\<open>gfp\<close>\<close> |
13218 | 193 |
|
194 |
(*gfp contains each post-fixedpoint that is contained in D*) |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
195 |
lemma gfp_upperbound: "\<lbrakk>A \<subseteq> h(A); A<=D\<rbrakk> \<Longrightarrow> A \<subseteq> gfp(D,h)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
196 |
unfolding gfp_def |
13218 | 197 |
apply (rule PowI [THEN CollectI, THEN Union_upper]) |
198 |
apply (assumption+) |
|
199 |
done |
|
200 |
||
46820 | 201 |
lemma gfp_subset: "gfp(D,h) \<subseteq> D" |
13218 | 202 |
by (unfold gfp_def, blast) |
203 |
||
204 |
(*Used in datatype package*) |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
205 |
lemma def_gfp_subset: "A\<equiv>gfp(D,h) \<Longrightarrow> A \<subseteq> D" |
13218 | 206 |
apply simp |
207 |
apply (rule gfp_subset) |
|
208 |
done |
|
209 |
||
210 |
lemma gfp_least: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
211 |
"\<lbrakk>bnd_mono(D,h); \<And>X. \<lbrakk>X \<subseteq> h(X); X<=D\<rbrakk> \<Longrightarrow> X<=A\<rbrakk> \<Longrightarrow> |
46820 | 212 |
gfp(D,h) \<subseteq> A" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
213 |
unfolding gfp_def |
13218 | 214 |
apply (blast dest: bnd_monoD1) |
215 |
done |
|
216 |
||
217 |
lemma gfp_lemma1: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
218 |
"\<lbrakk>bnd_mono(D,h); A<=h(A); A<=D\<rbrakk> \<Longrightarrow> A \<subseteq> h(gfp(D,h))" |
13218 | 219 |
apply (rule subset_trans, assumption) |
220 |
apply (erule bnd_monoD2) |
|
221 |
apply (rule_tac [2] gfp_subset) |
|
222 |
apply (simp add: gfp_upperbound) |
|
223 |
done |
|
224 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
225 |
lemma gfp_lemma2: "bnd_mono(D,h) \<Longrightarrow> gfp(D,h) \<subseteq> h(gfp(D,h))" |
13218 | 226 |
apply (rule gfp_least) |
227 |
apply (rule_tac [2] gfp_lemma1) |
|
228 |
apply (assumption+) |
|
229 |
done |
|
230 |
||
231 |
lemma gfp_lemma3: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
232 |
"bnd_mono(D,h) \<Longrightarrow> h(gfp(D,h)) \<subseteq> gfp(D,h)" |
13218 | 233 |
apply (rule gfp_upperbound) |
234 |
apply (rule bnd_monoD2, assumption) |
|
235 |
apply (rule gfp_lemma2, assumption) |
|
236 |
apply (erule bnd_mono_subset, rule gfp_subset)+ |
|
237 |
done |
|
238 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
239 |
lemma gfp_unfold: "bnd_mono(D,h) \<Longrightarrow> gfp(D,h) = h(gfp(D,h))" |
13218 | 240 |
apply (rule equalityI) |
241 |
apply (erule gfp_lemma2) |
|
242 |
apply (erule gfp_lemma3) |
|
243 |
done |
|
244 |
||
245 |
(*Definition form, to control unfolding*) |
|
246 |
lemma def_gfp_unfold: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
247 |
"\<lbrakk>A\<equiv>gfp(D,h); bnd_mono(D,h)\<rbrakk> \<Longrightarrow> A = h(A)" |
13218 | 248 |
apply simp |
249 |
apply (erule gfp_unfold) |
|
250 |
done |
|
251 |
||
252 |
||
60770 | 253 |
subsection\<open>Coinduction Rules for Greatest Fixed Points\<close> |
13218 | 254 |
|
255 |
(*weak version*) |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
256 |
lemma weak_coinduct: "\<lbrakk>a: X; X \<subseteq> h(X); X \<subseteq> D\<rbrakk> \<Longrightarrow> a \<in> gfp(D,h)" |
13218 | 257 |
by (blast intro: gfp_upperbound [THEN subsetD]) |
0 | 258 |
|
13218 | 259 |
lemma coinduct_lemma: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
260 |
"\<lbrakk>X \<subseteq> h(X \<union> gfp(D,h)); X \<subseteq> D; bnd_mono(D,h)\<rbrakk> \<Longrightarrow> |
46820 | 261 |
X \<union> gfp(D,h) \<subseteq> h(X \<union> gfp(D,h))" |
13218 | 262 |
apply (erule Un_least) |
263 |
apply (rule gfp_lemma2 [THEN subset_trans], assumption) |
|
264 |
apply (rule Un_upper2 [THEN subset_trans]) |
|
265 |
apply (rule bnd_mono_Un, assumption+) |
|
266 |
apply (rule gfp_subset) |
|
267 |
done |
|
268 |
||
269 |
(*strong version*) |
|
270 |
lemma coinduct: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
271 |
"\<lbrakk>bnd_mono(D,h); a: X; X \<subseteq> h(X \<union> gfp(D,h)); X \<subseteq> D\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
272 |
\<Longrightarrow> a \<in> gfp(D,h)" |
13218 | 273 |
apply (rule weak_coinduct) |
274 |
apply (erule_tac [2] coinduct_lemma) |
|
275 |
apply (simp_all add: gfp_subset Un_subset_iff) |
|
276 |
done |
|
277 |
||
278 |
(*Definition form, to control unfolding*) |
|
279 |
lemma def_coinduct: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
280 |
"\<lbrakk>A \<equiv> gfp(D,h); bnd_mono(D,h); a: X; X \<subseteq> h(X \<union> A); X \<subseteq> D\<rbrakk> \<Longrightarrow> |
46820 | 281 |
a \<in> A" |
13218 | 282 |
apply simp |
283 |
apply (rule coinduct, assumption+) |
|
284 |
done |
|
285 |
||
286 |
(*The version used in the induction/coinduction package*) |
|
287 |
lemma def_Collect_coinduct: |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
288 |
"\<lbrakk>A \<equiv> gfp(D, \<lambda>w. Collect(D,P(w))); bnd_mono(D, \<lambda>w. Collect(D,P(w))); |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
289 |
a: X; X \<subseteq> D; \<And>z. z: X \<Longrightarrow> P(X \<union> A, z)\<rbrakk> \<Longrightarrow> |
46820 | 290 |
a \<in> A" |
13218 | 291 |
apply (rule def_coinduct, assumption+, blast+) |
292 |
done |
|
0 | 293 |
|
13218 | 294 |
(*Monotonicity of gfp!*) |
295 |
lemma gfp_mono: |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
296 |
"\<lbrakk>bnd_mono(D,h); D \<subseteq> E; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
297 |
\<And>X. X<=D \<Longrightarrow> h(X) \<subseteq> i(X)\<rbrakk> \<Longrightarrow> gfp(D,h) \<subseteq> gfp(E,i)" |
13218 | 298 |
apply (rule gfp_upperbound) |
299 |
apply (rule gfp_lemma2 [THEN subset_trans], assumption) |
|
300 |
apply (blast del: subsetI intro: gfp_subset) |
|
301 |
apply (blast del: subsetI intro: subset_trans gfp_subset) |
|
302 |
done |
|
303 |
||
0 | 304 |
end |