author | nipkow |
Fri, 25 May 2007 18:08:34 +0200 | |
changeset 23100 | 1c84d7294d5b |
parent 22780 | 41162a270151 |
child 23755 | 1c4672d130b1 |
permissions | -rw-r--r-- |
18400 | 1 |
(* Title: HOL/Library/Coinductive_Lists.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson and Makarius |
|
4 |
*) |
|
5 |
||
6 |
header {* Potentially infinite lists as greatest fixed-point *} |
|
7 |
||
8 |
theory Coinductive_List |
|
9 |
imports Main |
|
10 |
begin |
|
11 |
||
12 |
subsection {* List constructors over the datatype universe *} |
|
13 |
||
19086 | 14 |
definition |
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
15 |
"NIL = Datatype.In0 (Datatype.Numb 0)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
16 |
definition |
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
17 |
"CONS M N = Datatype.In1 (Datatype.Scons M N)" |
18400 | 18 |
|
19 |
lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL" |
|
20 |
and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N" |
|
21 |
and CONS_inject [iff]: "(CONS K M) = (CONS L N) = (K = L \<and> M = N)" |
|
22 |
by (simp_all add: NIL_def CONS_def) |
|
23 |
||
24 |
lemma CONS_mono: "M \<subseteq> M' \<Longrightarrow> N \<subseteq> N' \<Longrightarrow> CONS M N \<subseteq> CONS M' N'" |
|
25 |
by (simp add: CONS_def In1_mono Scons_mono) |
|
26 |
||
27 |
lemma CONS_UN1: "CONS M (\<Union>x. f x) = (\<Union>x. CONS M (f x))" |
|
28 |
-- {* A continuity result? *} |
|
29 |
by (simp add: CONS_def In1_UN1 Scons_UN1_y) |
|
30 |
||
19086 | 31 |
definition |
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
32 |
"List_case c h = Datatype.Case (\<lambda>_. c) (Datatype.Split h)" |
18400 | 33 |
|
34 |
lemma List_case_NIL [simp]: "List_case c h NIL = c" |
|
35 |
and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N" |
|
36 |
by (simp_all add: List_case_def NIL_def CONS_def) |
|
37 |
||
38 |
||
39 |
subsection {* Corecursive lists *} |
|
40 |
||
41 |
consts |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
42 |
LList :: "'a Datatype.item set \<Rightarrow> 'a Datatype.item set" |
18400 | 43 |
|
44 |
coinductive "LList A" |
|
45 |
intros |
|
46 |
NIL [intro]: "NIL \<in> LList A" |
|
47 |
CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A" |
|
48 |
||
49 |
lemma LList_mono: "A \<subseteq> B \<Longrightarrow> LList A \<subseteq> LList B" |
|
50 |
-- {* This justifies using @{text LList} in other recursive type definitions. *} |
|
18730 | 51 |
unfolding LList.defs by (blast intro!: gfp_mono) |
18400 | 52 |
|
53 |
consts |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
54 |
LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow> |
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
55 |
'a \<Rightarrow> 'b Datatype.item" |
18400 | 56 |
primrec |
57 |
"LList_corec_aux 0 f x = {}" |
|
58 |
"LList_corec_aux (Suc k) f x = |
|
59 |
(case f x of |
|
60 |
None \<Rightarrow> NIL |
|
61 |
| Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))" |
|
62 |
||
19086 | 63 |
definition |
64 |
"LList_corec a f = (\<Union>k. LList_corec_aux k f a)" |
|
18400 | 65 |
|
66 |
text {* |
|
67 |
Note: the subsequent recursion equation for @{text LList_corec} may |
|
68 |
be used with the Simplifier, provided it operates in a non-strict |
|
69 |
fashion for case expressions (i.e.\ the usual @{text case} |
|
70 |
congruence rule needs to be present). |
|
71 |
*} |
|
72 |
||
73 |
lemma LList_corec: |
|
74 |
"LList_corec a f = |
|
75 |
(case f a of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (LList_corec w f))" |
|
76 |
(is "?lhs = ?rhs") |
|
77 |
proof |
|
78 |
show "?lhs \<subseteq> ?rhs" |
|
79 |
apply (unfold LList_corec_def) |
|
80 |
apply (rule UN_least) |
|
81 |
apply (case_tac k) |
|
82 |
apply (simp_all (no_asm_simp) split: option.splits) |
|
83 |
apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+ |
|
84 |
done |
|
85 |
show "?rhs \<subseteq> ?lhs" |
|
86 |
apply (simp add: LList_corec_def split: option.splits) |
|
87 |
apply (simp add: CONS_UN1) |
|
88 |
apply safe |
|
89 |
apply (rule_tac a = "Suc ?k" in UN_I, simp, simp)+ |
|
90 |
done |
|
91 |
qed |
|
92 |
||
93 |
lemma LList_corec_type: "LList_corec a f \<in> LList UNIV" |
|
94 |
proof - |
|
95 |
have "LList_corec a f \<in> {LList_corec a f | a. True}" by blast |
|
96 |
then show ?thesis |
|
97 |
proof coinduct |
|
98 |
case (LList L) |
|
99 |
then obtain x where L: "L = LList_corec x f" by blast |
|
100 |
show ?case |
|
101 |
proof (cases "f x") |
|
102 |
case None |
|
103 |
then have "LList_corec x f = NIL" |
|
104 |
by (simp add: LList_corec) |
|
105 |
with L have ?NIL by simp |
|
106 |
then show ?thesis .. |
|
107 |
next |
|
108 |
case (Some p) |
|
109 |
then have "LList_corec x f = CONS (fst p) (LList_corec (snd p) f)" |
|
22780
41162a270151
Adapted to new parse translation for case expressions.
berghofe
parents:
22367
diff
changeset
|
110 |
by (simp add: LList_corec split: prod.split) |
18400 | 111 |
with L have ?CONS by auto |
112 |
then show ?thesis .. |
|
113 |
qed |
|
114 |
qed |
|
115 |
qed |
|
116 |
||
117 |
||
118 |
subsection {* Abstract type definition *} |
|
119 |
||
120 |
typedef 'a llist = |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
121 |
"LList (range Datatype.Leaf) :: 'a Datatype.item set" |
18400 | 122 |
proof |
123 |
show "NIL \<in> ?llist" .. |
|
124 |
qed |
|
125 |
||
126 |
lemma NIL_type: "NIL \<in> llist" |
|
18730 | 127 |
unfolding llist_def by (rule LList.NIL) |
18400 | 128 |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
129 |
lemma CONS_type: "a \<in> range Datatype.Leaf \<Longrightarrow> |
18400 | 130 |
M \<in> llist \<Longrightarrow> CONS a M \<in> llist" |
18730 | 131 |
unfolding llist_def by (rule LList.CONS) |
18400 | 132 |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
133 |
lemma llistI: "x \<in> LList (range Datatype.Leaf) \<Longrightarrow> x \<in> llist" |
18400 | 134 |
by (simp add: llist_def) |
135 |
||
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
136 |
lemma llistD: "x \<in> llist \<Longrightarrow> x \<in> LList (range Datatype.Leaf)" |
18400 | 137 |
by (simp add: llist_def) |
138 |
||
139 |
lemma Rep_llist_UNIV: "Rep_llist x \<in> LList UNIV" |
|
140 |
proof - |
|
141 |
have "Rep_llist x \<in> llist" by (rule Rep_llist) |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
142 |
then have "Rep_llist x \<in> LList (range Datatype.Leaf)" |
18400 | 143 |
by (simp add: llist_def) |
144 |
also have "\<dots> \<subseteq> LList UNIV" by (rule LList_mono) simp |
|
145 |
finally show ?thesis . |
|
146 |
qed |
|
147 |
||
19086 | 148 |
definition |
149 |
"LNil = Abs_llist NIL" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
150 |
definition |
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
151 |
"LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))" |
18400 | 152 |
|
153 |
lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil" |
|
154 |
apply (simp add: LNil_def LCons_def) |
|
155 |
apply (subst Abs_llist_inject) |
|
156 |
apply (auto intro: NIL_type CONS_type Rep_llist) |
|
157 |
done |
|
158 |
||
159 |
lemma LNil_not_LCons [iff]: "LNil \<noteq> LCons x xs" |
|
160 |
by (rule LCons_not_LNil [symmetric]) |
|
161 |
||
162 |
lemma LCons_inject [iff]: "(LCons x xs = LCons y ys) = (x = y \<and> xs = ys)" |
|
163 |
apply (simp add: LCons_def) |
|
164 |
apply (subst Abs_llist_inject) |
|
165 |
apply (auto simp add: Rep_llist_inject intro: CONS_type Rep_llist) |
|
166 |
done |
|
167 |
||
168 |
lemma Rep_llist_LNil: "Rep_llist LNil = NIL" |
|
169 |
by (simp add: LNil_def add: Abs_llist_inverse NIL_type) |
|
170 |
||
171 |
lemma Rep_llist_LCons: "Rep_llist (LCons x l) = |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
172 |
CONS (Datatype.Leaf x) (Rep_llist l)" |
18400 | 173 |
by (simp add: LCons_def Abs_llist_inverse CONS_type Rep_llist) |
174 |
||
20802 | 175 |
lemma llist_cases [cases type: llist]: |
176 |
obtains |
|
177 |
(LNil) "l = LNil" |
|
178 |
| (LCons) x l' where "l = LCons x l'" |
|
18400 | 179 |
proof (cases l) |
180 |
case (Abs_llist L) |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
181 |
from `L \<in> llist` have "L \<in> LList (range Datatype.Leaf)" by (rule llistD) |
18400 | 182 |
then show ?thesis |
183 |
proof cases |
|
184 |
case NIL |
|
185 |
with Abs_llist have "l = LNil" by (simp add: LNil_def) |
|
186 |
with LNil show ?thesis . |
|
187 |
next |
|
188 |
case (CONS K a) |
|
189 |
then have "K \<in> llist" by (blast intro: llistI) |
|
190 |
then obtain l' where "K = Rep_llist l'" by cases |
|
191 |
with CONS and Abs_llist obtain x where "l = LCons x l'" |
|
192 |
by (auto simp add: LCons_def Abs_llist_inject) |
|
193 |
with LCons show ?thesis . |
|
194 |
qed |
|
195 |
qed |
|
196 |
||
197 |
||
19086 | 198 |
definition |
199 |
"llist_case c d l = |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
200 |
List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)" |
20770 | 201 |
|
202 |
syntax (* FIXME? *) |
|
203 |
LNil :: logic |
|
204 |
LCons :: logic |
|
18400 | 205 |
translations |
20770 | 206 |
"case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p" |
18400 | 207 |
|
208 |
lemma llist_case_LNil [simp]: "llist_case c d LNil = c" |
|
209 |
by (simp add: llist_case_def LNil_def |
|
210 |
NIL_type Abs_llist_inverse) |
|
211 |
||
212 |
lemma llist_case_LCons [simp]: "llist_case c d (LCons M N) = d M N" |
|
213 |
by (simp add: llist_case_def LCons_def |
|
214 |
CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf) |
|
215 |
||
216 |
||
19086 | 217 |
definition |
218 |
"llist_corec a f = |
|
18400 | 219 |
Abs_llist (LList_corec a |
220 |
(\<lambda>z. |
|
221 |
case f z of None \<Rightarrow> None |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
222 |
| Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)))" |
18400 | 223 |
|
224 |
lemma LList_corec_type2: |
|
225 |
"LList_corec a |
|
226 |
(\<lambda>z. case f z of None \<Rightarrow> None |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
227 |
| Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)) \<in> llist" |
18400 | 228 |
(is "?corec a \<in> _") |
229 |
proof (unfold llist_def) |
|
230 |
let "LList_corec a ?g" = "?corec a" |
|
231 |
have "?corec a \<in> {?corec x | x. True}" by blast |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
232 |
then show "?corec a \<in> LList (range Datatype.Leaf)" |
18400 | 233 |
proof coinduct |
234 |
case (LList L) |
|
235 |
then obtain x where L: "L = ?corec x" by blast |
|
236 |
show ?case |
|
237 |
proof (cases "f x") |
|
238 |
case None |
|
239 |
then have "?corec x = NIL" |
|
240 |
by (simp add: LList_corec) |
|
241 |
with L have ?NIL by simp |
|
242 |
then show ?thesis .. |
|
243 |
next |
|
244 |
case (Some p) |
|
245 |
then have "?corec x = |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
246 |
CONS (Datatype.Leaf (fst p)) (?corec (snd p))" |
22780
41162a270151
Adapted to new parse translation for case expressions.
berghofe
parents:
22367
diff
changeset
|
247 |
by (simp add: LList_corec split: prod.split) |
18400 | 248 |
with L have ?CONS by auto |
249 |
then show ?thesis .. |
|
250 |
qed |
|
251 |
qed |
|
252 |
qed |
|
253 |
||
254 |
lemma llist_corec: |
|
255 |
"llist_corec a f = |
|
256 |
(case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))" |
|
257 |
proof (cases "f a") |
|
258 |
case None |
|
259 |
then show ?thesis |
|
260 |
by (simp add: llist_corec_def LList_corec LNil_def) |
|
261 |
next |
|
262 |
case (Some p) |
|
263 |
||
264 |
let "?corec a" = "llist_corec a f" |
|
265 |
let "?rep_corec a" = |
|
266 |
"LList_corec a |
|
267 |
(\<lambda>z. case f z of None \<Rightarrow> None |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
268 |
| Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w))" |
18400 | 269 |
|
270 |
have "?corec a = Abs_llist (?rep_corec a)" |
|
271 |
by (simp only: llist_corec_def) |
|
272 |
also from Some have "?rep_corec a = |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
273 |
CONS (Datatype.Leaf (fst p)) (?rep_corec (snd p))" |
22780
41162a270151
Adapted to new parse translation for case expressions.
berghofe
parents:
22367
diff
changeset
|
274 |
by (simp add: LList_corec split: prod.split) |
18400 | 275 |
also have "?rep_corec (snd p) = Rep_llist (?corec (snd p))" |
276 |
by (simp only: llist_corec_def Abs_llist_inverse LList_corec_type2) |
|
277 |
finally have "?corec a = LCons (fst p) (?corec (snd p))" |
|
278 |
by (simp only: LCons_def) |
|
22780
41162a270151
Adapted to new parse translation for case expressions.
berghofe
parents:
22367
diff
changeset
|
279 |
with Some show ?thesis by (simp split: prod.split) |
18400 | 280 |
qed |
281 |
||
282 |
||
22367 | 283 |
subsection {* Equality as greatest fixed-point -- the bisimulation principle *} |
18400 | 284 |
|
285 |
consts |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
286 |
EqLList :: "('a Datatype.item \<times> 'a Datatype.item) set \<Rightarrow> |
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
287 |
('a Datatype.item \<times> 'a Datatype.item) set" |
18400 | 288 |
|
289 |
coinductive "EqLList r" |
|
290 |
intros |
|
291 |
EqNIL: "(NIL, NIL) \<in> EqLList r" |
|
292 |
EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow> |
|
293 |
(CONS a M, CONS b N) \<in> EqLList r" |
|
294 |
||
295 |
lemma EqLList_unfold: |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
296 |
"EqLList r = dsum (diag {Datatype.Numb 0}) (dprod r (EqLList r))" |
18400 | 297 |
by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def] |
298 |
elim: EqLList.cases [unfolded NIL_def CONS_def]) |
|
299 |
||
300 |
lemma EqLList_implies_ntrunc_equality: |
|
301 |
"(M, N) \<in> EqLList (diag A) \<Longrightarrow> ntrunc k M = ntrunc k N" |
|
20503 | 302 |
apply (induct k arbitrary: M N rule: nat_less_induct) |
18400 | 303 |
apply (erule EqLList.cases) |
304 |
apply (safe del: equalityI) |
|
305 |
apply (case_tac n) |
|
306 |
apply simp |
|
307 |
apply (rename_tac n') |
|
308 |
apply (case_tac n') |
|
309 |
apply (simp_all add: CONS_def less_Suc_eq) |
|
310 |
done |
|
311 |
||
312 |
lemma Domain_EqLList: "Domain (EqLList (diag A)) \<subseteq> LList A" |
|
313 |
apply (simp add: LList.defs NIL_def CONS_def) |
|
314 |
apply (rule gfp_upperbound) |
|
315 |
apply (subst EqLList_unfold) |
|
316 |
apply auto |
|
317 |
done |
|
318 |
||
319 |
lemma EqLList_diag: "EqLList (diag A) = diag (LList A)" |
|
320 |
(is "?lhs = ?rhs") |
|
321 |
proof |
|
322 |
show "?lhs \<subseteq> ?rhs" |
|
323 |
apply (rule subsetI) |
|
324 |
apply (rule_tac p = x in PairE) |
|
325 |
apply clarify |
|
326 |
apply (rule diag_eqI) |
|
327 |
apply (rule EqLList_implies_ntrunc_equality [THEN ntrunc_equality], |
|
328 |
assumption) |
|
329 |
apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]]) |
|
330 |
done |
|
331 |
show "?rhs \<subseteq> ?lhs" |
|
332 |
proof |
|
333 |
fix p assume "p \<in> diag (LList A)" |
|
334 |
then show "p \<in> EqLList (diag A)" |
|
335 |
proof coinduct |
|
336 |
case (EqLList q) |
|
337 |
then obtain L where L: "L \<in> LList A" and q: "q = (L, L)" .. |
|
338 |
from L show ?case |
|
339 |
proof cases |
|
340 |
case NIL with q have ?EqNIL by simp |
|
341 |
then show ?thesis .. |
|
342 |
next |
|
343 |
case CONS with q have ?EqCONS by (simp add: diagI) |
|
344 |
then show ?thesis .. |
|
345 |
qed |
|
346 |
qed |
|
347 |
qed |
|
348 |
qed |
|
349 |
||
350 |
lemma EqLList_diag_iff [iff]: "(p \<in> EqLList (diag A)) = (p \<in> diag (LList A))" |
|
351 |
by (simp only: EqLList_diag) |
|
352 |
||
353 |
||
354 |
text {* |
|
355 |
To show two LLists are equal, exhibit a bisimulation! (Also admits |
|
356 |
true equality.) |
|
357 |
*} |
|
358 |
||
359 |
lemma LList_equalityI |
|
360 |
[consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]: |
|
361 |
assumes r: "(M, N) \<in> r" |
|
362 |
and step: "\<And>p. p \<in> r \<Longrightarrow> |
|
363 |
p = (NIL, NIL) \<or> |
|
364 |
(\<exists>M N a b. |
|
365 |
p = (CONS a M, CONS b N) \<and> (a, b) \<in> diag A \<and> |
|
366 |
(M, N) \<in> r \<union> EqLList (diag A))" |
|
367 |
shows "M = N" |
|
368 |
proof - |
|
369 |
from r have "(M, N) \<in> EqLList (diag A)" |
|
370 |
proof coinduct |
|
371 |
case EqLList |
|
372 |
then show ?case by (rule step) |
|
373 |
qed |
|
374 |
then show ?thesis by auto |
|
375 |
qed |
|
376 |
||
377 |
lemma LList_fun_equalityI |
|
378 |
[consumes 1, case_names NIL_type NIL CONS, case_conclusion CONS EqNIL EqCONS]: |
|
379 |
assumes M: "M \<in> LList A" |
|
380 |
and fun_NIL: "g NIL \<in> LList A" "f NIL = g NIL" |
|
381 |
and fun_CONS: "\<And>x l. x \<in> A \<Longrightarrow> l \<in> LList A \<Longrightarrow> |
|
382 |
(f (CONS x l), g (CONS x l)) = (NIL, NIL) \<or> |
|
383 |
(\<exists>M N a b. |
|
384 |
(f (CONS x l), g (CONS x l)) = (CONS a M, CONS b N) \<and> |
|
385 |
(a, b) \<in> diag A \<and> |
|
386 |
(M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> diag (LList A))" |
|
387 |
(is "\<And>x l. _ \<Longrightarrow> _ \<Longrightarrow> ?fun_CONS x l") |
|
388 |
shows "f M = g M" |
|
389 |
proof - |
|
390 |
let ?bisim = "{(f L, g L) | L. L \<in> LList A}" |
|
391 |
have "(f M, g M) \<in> ?bisim" using M by blast |
|
392 |
then show ?thesis |
|
393 |
proof (coinduct taking: A rule: LList_equalityI) |
|
394 |
case (EqLList q) |
|
395 |
then obtain L where q: "q = (f L, g L)" and L: "L \<in> LList A" by blast |
|
396 |
from L show ?case |
|
397 |
proof (cases L) |
|
398 |
case NIL |
|
399 |
with fun_NIL and q have "q \<in> diag (LList A)" by auto |
|
400 |
then have "q \<in> EqLList (diag A)" .. |
|
401 |
then show ?thesis by cases simp_all |
|
402 |
next |
|
403 |
case (CONS K a) |
|
404 |
from fun_CONS and `a \<in> A` `K \<in> LList A` |
|
405 |
have "?fun_CONS a K" (is "?NIL \<or> ?CONS") . |
|
406 |
then show ?thesis |
|
407 |
proof |
|
408 |
assume ?NIL |
|
409 |
with q CONS have "q \<in> diag (LList A)" by auto |
|
410 |
then have "q \<in> EqLList (diag A)" .. |
|
411 |
then show ?thesis by cases simp_all |
|
412 |
next |
|
413 |
assume ?CONS |
|
414 |
with CONS obtain a b M N where |
|
415 |
fg: "(f L, g L) = (CONS a M, CONS b N)" |
|
416 |
and ab: "(a, b) \<in> diag A" |
|
417 |
and MN: "(M, N) \<in> ?bisim \<union> diag (LList A)" |
|
418 |
by blast |
|
419 |
from MN show ?thesis |
|
420 |
proof |
|
421 |
assume "(M, N) \<in> ?bisim" |
|
422 |
with q fg ab show ?thesis by simp |
|
423 |
next |
|
424 |
assume "(M, N) \<in> diag (LList A)" |
|
425 |
then have "(M, N) \<in> EqLList (diag A)" .. |
|
426 |
with q fg ab show ?thesis by simp |
|
427 |
qed |
|
428 |
qed |
|
429 |
qed |
|
430 |
qed |
|
431 |
qed |
|
432 |
||
433 |
text {* |
|
434 |
Finality of @{text "llist A"}: Uniqueness of functions defined by corecursion. |
|
435 |
*} |
|
436 |
||
437 |
lemma equals_LList_corec: |
|
438 |
assumes h: "\<And>x. h x = |
|
439 |
(case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h w))" |
|
440 |
shows "h x = (\<lambda>x. LList_corec x f) x" |
|
441 |
proof - |
|
442 |
def h' \<equiv> "\<lambda>x. LList_corec x f" |
|
443 |
then have h': "\<And>x. h' x = |
|
444 |
(case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))" |
|
18730 | 445 |
unfolding h'_def by (simp add: LList_corec) |
18400 | 446 |
have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast |
447 |
then show "h x = h' x" |
|
448 |
proof (coinduct rule: LList_equalityI [where A = UNIV]) |
|
449 |
case (EqLList q) |
|
450 |
then obtain x where q: "q = (h x, h' x)" by blast |
|
451 |
show ?case |
|
452 |
proof (cases "f x") |
|
453 |
case None |
|
454 |
with h h' q have ?EqNIL by simp |
|
455 |
then show ?thesis .. |
|
456 |
next |
|
457 |
case (Some p) |
|
458 |
with h h' q have "q = |
|
459 |
(CONS (fst p) (h (snd p)), CONS (fst p) (h' (snd p)))" |
|
22780
41162a270151
Adapted to new parse translation for case expressions.
berghofe
parents:
22367
diff
changeset
|
460 |
by (simp split: prod.split) |
18400 | 461 |
then have ?EqCONS by (auto iff: diag_iff) |
462 |
then show ?thesis .. |
|
463 |
qed |
|
464 |
qed |
|
465 |
qed |
|
466 |
||
467 |
||
468 |
lemma llist_equalityI |
|
469 |
[consumes 1, case_names Eqllist, case_conclusion Eqllist EqLNil EqLCons]: |
|
470 |
assumes r: "(l1, l2) \<in> r" |
|
471 |
and step: "\<And>q. q \<in> r \<Longrightarrow> |
|
472 |
q = (LNil, LNil) \<or> |
|
473 |
(\<exists>l1 l2 a b. |
|
474 |
q = (LCons a l1, LCons b l2) \<and> a = b \<and> |
|
475 |
((l1, l2) \<in> r \<or> l1 = l2))" |
|
476 |
(is "\<And>q. _ \<Longrightarrow> ?EqLNil q \<or> ?EqLCons q") |
|
477 |
shows "l1 = l2" |
|
478 |
proof - |
|
479 |
def M \<equiv> "Rep_llist l1" and N \<equiv> "Rep_llist l2" |
|
480 |
with r have "(M, N) \<in> {(Rep_llist l1, Rep_llist l2) | l1 l2. (l1, l2) \<in> r}" |
|
481 |
by blast |
|
482 |
then have "M = N" |
|
483 |
proof (coinduct rule: LList_equalityI [where A = UNIV]) |
|
484 |
case (EqLList q) |
|
485 |
then obtain l1 l2 where |
|
486 |
q: "q = (Rep_llist l1, Rep_llist l2)" and r: "(l1, l2) \<in> r" |
|
487 |
by auto |
|
488 |
from step [OF r] show ?case |
|
489 |
proof |
|
490 |
assume "?EqLNil (l1, l2)" |
|
491 |
with q have ?EqNIL by (simp add: Rep_llist_LNil) |
|
492 |
then show ?thesis .. |
|
493 |
next |
|
494 |
assume "?EqLCons (l1, l2)" |
|
495 |
with q have ?EqCONS |
|
496 |
by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV) |
|
497 |
then show ?thesis .. |
|
498 |
qed |
|
499 |
qed |
|
500 |
then show ?thesis by (simp add: M_def N_def Rep_llist_inject) |
|
501 |
qed |
|
502 |
||
503 |
lemma llist_fun_equalityI |
|
504 |
[case_names LNil LCons, case_conclusion LCons EqLNil EqLCons]: |
|
505 |
assumes fun_LNil: "f LNil = g LNil" |
|
506 |
and fun_LCons: "\<And>x l. |
|
507 |
(f (LCons x l), g (LCons x l)) = (LNil, LNil) \<or> |
|
508 |
(\<exists>l1 l2 a b. |
|
509 |
(f (LCons x l), g (LCons x l)) = (LCons a l1, LCons b l2) \<and> |
|
510 |
a = b \<and> ((l1, l2) \<in> {(f u, g u) | u. True} \<or> l1 = l2))" |
|
511 |
(is "\<And>x l. ?fun_LCons x l") |
|
512 |
shows "f l = g l" |
|
513 |
proof - |
|
514 |
have "(f l, g l) \<in> {(f l, g l) | l. True}" by blast |
|
515 |
then show ?thesis |
|
516 |
proof (coinduct rule: llist_equalityI) |
|
517 |
case (Eqllist q) |
|
518 |
then obtain l where q: "q = (f l, g l)" by blast |
|
519 |
show ?case |
|
520 |
proof (cases l) |
|
521 |
case LNil |
|
522 |
with fun_LNil and q have "q = (g LNil, g LNil)" by simp |
|
523 |
then show ?thesis by (cases "g LNil") simp_all |
|
524 |
next |
|
525 |
case (LCons x l') |
|
526 |
with `?fun_LCons x l'` q LCons show ?thesis by blast |
|
527 |
qed |
|
528 |
qed |
|
529 |
qed |
|
530 |
||
531 |
||
532 |
subsection {* Derived operations -- both on the set and abstract type *} |
|
533 |
||
534 |
subsubsection {* @{text Lconst} *} |
|
535 |
||
19086 | 536 |
definition |
18400 | 537 |
"Lconst M \<equiv> lfp (\<lambda>N. CONS M N)" |
538 |
||
539 |
lemma Lconst_fun_mono: "mono (CONS M)" |
|
540 |
by (simp add: monoI CONS_mono) |
|
541 |
||
542 |
lemma Lconst: "Lconst M = CONS M (Lconst M)" |
|
543 |
by (rule Lconst_def [THEN def_lfp_unfold]) (rule Lconst_fun_mono) |
|
544 |
||
545 |
lemma Lconst_type: |
|
546 |
assumes "M \<in> A" |
|
547 |
shows "Lconst M \<in> LList A" |
|
548 |
proof - |
|
549 |
have "Lconst M \<in> {Lconst M}" by simp |
|
550 |
then show ?thesis |
|
551 |
proof coinduct |
|
552 |
case (LList N) |
|
553 |
then have "N = Lconst M" by simp |
|
554 |
also have "\<dots> = CONS M (Lconst M)" by (rule Lconst) |
|
555 |
finally have ?CONS using `M \<in> A` by simp |
|
556 |
then show ?case .. |
|
557 |
qed |
|
558 |
qed |
|
559 |
||
560 |
lemma Lconst_eq_LList_corec: "Lconst M = LList_corec M (\<lambda>x. Some (x, x))" |
|
561 |
apply (rule equals_LList_corec) |
|
562 |
apply simp |
|
563 |
apply (rule Lconst) |
|
564 |
done |
|
565 |
||
566 |
lemma gfp_Lconst_eq_LList_corec: |
|
567 |
"gfp (\<lambda>N. CONS M N) = LList_corec M (\<lambda>x. Some(x, x))" |
|
568 |
apply (rule equals_LList_corec) |
|
569 |
apply simp |
|
570 |
apply (rule Lconst_fun_mono [THEN gfp_unfold]) |
|
571 |
done |
|
572 |
||
573 |
||
574 |
subsubsection {* @{text Lmap} and @{text lmap} *} |
|
575 |
||
19086 | 576 |
definition |
577 |
"Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
578 |
definition |
19086 | 579 |
"lmap f l = llist_corec l |
18400 | 580 |
(\<lambda>z. |
581 |
case z of LNil \<Rightarrow> None |
|
582 |
| LCons y z \<Rightarrow> Some (f y, z))" |
|
583 |
||
584 |
lemma Lmap_NIL [simp]: "Lmap f NIL = NIL" |
|
585 |
and Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)" |
|
586 |
by (simp_all add: Lmap_def LList_corec) |
|
587 |
||
588 |
lemma Lmap_type: |
|
589 |
assumes M: "M \<in> LList A" |
|
590 |
and f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B" |
|
591 |
shows "Lmap f M \<in> LList B" |
|
592 |
proof - |
|
593 |
from M have "Lmap f M \<in> {Lmap f N | N. N \<in> LList A}" by blast |
|
594 |
then show ?thesis |
|
595 |
proof coinduct |
|
596 |
case (LList L) |
|
597 |
then obtain N where L: "L = Lmap f N" and N: "N \<in> LList A" by blast |
|
598 |
from N show ?case |
|
599 |
proof cases |
|
600 |
case NIL |
|
601 |
with L have ?NIL by simp |
|
602 |
then show ?thesis .. |
|
603 |
next |
|
604 |
case (CONS K a) |
|
605 |
with f L have ?CONS by auto |
|
606 |
then show ?thesis .. |
|
607 |
qed |
|
608 |
qed |
|
609 |
qed |
|
610 |
||
611 |
lemma Lmap_compose: |
|
612 |
assumes M: "M \<in> LList A" |
|
613 |
shows "Lmap (f o g) M = Lmap f (Lmap g M)" (is "?lhs M = ?rhs M") |
|
614 |
proof - |
|
615 |
have "(?lhs M, ?rhs M) \<in> {(?lhs N, ?rhs N) | N. N \<in> LList A}" |
|
616 |
using M by blast |
|
617 |
then show ?thesis |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
618 |
proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)" |
18400 | 619 |
rule: LList_equalityI) |
620 |
case (EqLList q) |
|
621 |
then obtain N where q: "q = (?lhs N, ?rhs N)" and N: "N \<in> LList A" by blast |
|
622 |
from N show ?case |
|
623 |
proof cases |
|
624 |
case NIL |
|
625 |
with q have ?EqNIL by simp |
|
626 |
then show ?thesis .. |
|
627 |
next |
|
628 |
case CONS |
|
629 |
with q have ?EqCONS by auto |
|
630 |
then show ?thesis .. |
|
631 |
qed |
|
632 |
qed |
|
633 |
qed |
|
634 |
||
635 |
lemma Lmap_ident: |
|
636 |
assumes M: "M \<in> LList A" |
|
637 |
shows "Lmap (\<lambda>x. x) M = M" (is "?lmap M = _") |
|
638 |
proof - |
|
639 |
have "(?lmap M, M) \<in> {(?lmap N, N) | N. N \<in> LList A}" using M by blast |
|
640 |
then show ?thesis |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20802
diff
changeset
|
641 |
proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)" |
18400 | 642 |
rule: LList_equalityI) |
643 |
case (EqLList q) |
|
644 |
then obtain N where q: "q = (?lmap N, N)" and N: "N \<in> LList A" by blast |
|
645 |
from N show ?case |
|
646 |
proof cases |
|
647 |
case NIL |
|
648 |
with q have ?EqNIL by simp |
|
649 |
then show ?thesis .. |
|
650 |
next |
|
651 |
case CONS |
|
652 |
with q have ?EqCONS by auto |
|
653 |
then show ?thesis .. |
|
654 |
qed |
|
655 |
qed |
|
656 |
qed |
|
657 |
||
658 |
lemma lmap_LNil [simp]: "lmap f LNil = LNil" |
|
659 |
and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)" |
|
660 |
by (simp_all add: lmap_def llist_corec) |
|
661 |
||
662 |
lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)" |
|
663 |
by (coinduct _ _ l rule: llist_fun_equalityI) auto |
|
664 |
||
665 |
lemma lmap_ident [simp]: "lmap (\<lambda>x. x) l = l" |
|
666 |
by (coinduct _ _ l rule: llist_fun_equalityI) auto |
|
667 |
||
668 |
||
669 |
||
670 |
subsubsection {* @{text Lappend} *} |
|
671 |
||
19086 | 672 |
definition |
673 |
"Lappend M N = LList_corec (M, N) |
|
18400 | 674 |
(split (List_case |
675 |
(List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2)))) |
|
676 |
(\<lambda>M1 M2 N. Some (M1, (M2, N)))))" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
677 |
definition |
19086 | 678 |
"lappend l n = llist_corec (l, n) |
18400 | 679 |
(split (llist_case |
680 |
(llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2)))) |
|
681 |
(\<lambda>l1 l2 n. Some (l1, (l2, n)))))" |
|
682 |
||
683 |
lemma Lappend_NIL_NIL [simp]: |
|
684 |
"Lappend NIL NIL = NIL" |
|
685 |
and Lappend_NIL_CONS [simp]: |
|
686 |
"Lappend NIL (CONS N N') = CONS N (Lappend NIL N')" |
|
687 |
and Lappend_CONS [simp]: |
|
688 |
"Lappend (CONS M M') N = CONS M (Lappend M' N)" |
|
689 |
by (simp_all add: Lappend_def LList_corec) |
|
690 |
||
691 |
lemma Lappend_NIL [simp]: "M \<in> LList A \<Longrightarrow> Lappend NIL M = M" |
|
692 |
by (erule LList_fun_equalityI) auto |
|
693 |
||
694 |
lemma Lappend_NIL2: "M \<in> LList A \<Longrightarrow> Lappend M NIL = M" |
|
695 |
by (erule LList_fun_equalityI) auto |
|
696 |
||
697 |
lemma Lappend_type: |
|
698 |
assumes M: "M \<in> LList A" and N: "N \<in> LList A" |
|
699 |
shows "Lappend M N \<in> LList A" |
|
700 |
proof - |
|
701 |
have "Lappend M N \<in> {Lappend u v | u v. u \<in> LList A \<and> v \<in> LList A}" |
|
702 |
using M N by blast |
|
703 |
then show ?thesis |
|
704 |
proof coinduct |
|
705 |
case (LList L) |
|
706 |
then obtain M N where L: "L = Lappend M N" |
|
707 |
and M: "M \<in> LList A" and N: "N \<in> LList A" |
|
708 |
by blast |
|
709 |
from M show ?case |
|
710 |
proof cases |
|
711 |
case NIL |
|
712 |
from N show ?thesis |
|
713 |
proof cases |
|
714 |
case NIL |
|
715 |
with L and `M = NIL` have ?NIL by simp |
|
716 |
then show ?thesis .. |
|
717 |
next |
|
718 |
case CONS |
|
719 |
with L and `M = NIL` have ?CONS by simp |
|
720 |
then show ?thesis .. |
|
721 |
qed |
|
722 |
next |
|
723 |
case CONS |
|
724 |
with L N have ?CONS by auto |
|
725 |
then show ?thesis .. |
|
726 |
qed |
|
727 |
qed |
|
728 |
qed |
|
729 |
||
730 |
lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil" |
|
731 |
and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')" |
|
732 |
and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)" |
|
733 |
by (simp_all add: lappend_def llist_corec) |
|
734 |
||
735 |
lemma lappend_LNil1 [simp]: "lappend LNil l = l" |
|
736 |
by (coinduct _ _ l rule: llist_fun_equalityI) auto |
|
737 |
||
738 |
lemma lappend_LNil2 [simp]: "lappend l LNil = l" |
|
739 |
by (coinduct _ _ l rule: llist_fun_equalityI) auto |
|
740 |
||
741 |
lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)" |
|
742 |
by (coinduct _ _ l1 rule: llist_fun_equalityI) auto |
|
743 |
||
744 |
lemma lmap_lappend_distrib: "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)" |
|
745 |
by (coinduct _ _ l rule: llist_fun_equalityI) auto |
|
746 |
||
747 |
||
748 |
subsection{* iterates *} |
|
749 |
||
750 |
text {* @{text llist_fun_equalityI} cannot be used here! *} |
|
751 |
||
19086 | 752 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
753 |
iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where |
19086 | 754 |
"iterates f a = llist_corec a (\<lambda>x. Some (x, f x))" |
18400 | 755 |
|
756 |
lemma iterates: "iterates f x = LCons x (iterates f (f x))" |
|
757 |
apply (unfold iterates_def) |
|
758 |
apply (subst llist_corec) |
|
759 |
apply simp |
|
760 |
done |
|
761 |
||
762 |
lemma lmap_iterates: "lmap f (iterates f x) = iterates f (f x)" |
|
763 |
proof - |
|
764 |
have "(lmap f (iterates f x), iterates f (f x)) \<in> |
|
765 |
{(lmap f (iterates f u), iterates f (f u)) | u. True}" by blast |
|
766 |
then show ?thesis |
|
767 |
proof (coinduct rule: llist_equalityI) |
|
768 |
case (Eqllist q) |
|
769 |
then obtain x where q: "q = (lmap f (iterates f x), iterates f (f x))" |
|
770 |
by blast |
|
771 |
also have "iterates f (f x) = LCons (f x) (iterates f (f (f x)))" |
|
772 |
by (subst iterates) rule |
|
773 |
also have "iterates f x = LCons x (iterates f (f x))" |
|
774 |
by (subst iterates) rule |
|
775 |
finally have ?EqLCons by auto |
|
776 |
then show ?case .. |
|
777 |
qed |
|
778 |
qed |
|
779 |
||
780 |
lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))" |
|
781 |
by (subst lmap_iterates) (rule iterates) |
|
782 |
||
783 |
||
784 |
subsection{* A rather complex proof about iterates -- cf.\ Andy Pitts *} |
|
785 |
||
786 |
lemma funpow_lmap: |
|
787 |
fixes f :: "'a \<Rightarrow> 'a" |
|
788 |
shows "(lmap f ^ n) (LCons b l) = LCons ((f ^ n) b) ((lmap f ^ n) l)" |
|
789 |
by (induct n) simp_all |
|
790 |
||
791 |
||
792 |
lemma iterates_equality: |
|
793 |
assumes h: "\<And>x. h x = LCons x (lmap f (h x))" |
|
794 |
shows "h = iterates f" |
|
795 |
proof |
|
796 |
fix x |
|
797 |
have "(h x, iterates f x) \<in> |
|
798 |
{((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u)) | u n. True}" |
|
799 |
proof - |
|
800 |
have "(h x, iterates f x) = ((lmap f ^ 0) (h x), (lmap f ^ 0) (iterates f x))" |
|
801 |
by simp |
|
802 |
then show ?thesis by blast |
|
803 |
qed |
|
804 |
then show "h x = iterates f x" |
|
805 |
proof (coinduct rule: llist_equalityI) |
|
806 |
case (Eqllist q) |
|
807 |
then obtain u n where "q = ((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u))" |
|
808 |
(is "_ = (?q1, ?q2)") |
|
809 |
by auto |
|
810 |
also have "?q1 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (h u))" |
|
811 |
proof - |
|
812 |
have "?q1 = (lmap f ^ n) (LCons u (lmap f (h u)))" |
|
813 |
by (subst h) rule |
|
814 |
also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))" |
|
815 |
by (rule funpow_lmap) |
|
816 |
also have "(lmap f ^ n) (lmap f (h u)) = (lmap f ^ Suc n) (h u)" |
|
817 |
by (simp add: funpow_swap1) |
|
818 |
finally show ?thesis . |
|
819 |
qed |
|
820 |
also have "?q2 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (iterates f u))" |
|
821 |
proof - |
|
822 |
have "?q2 = (lmap f ^ n) (LCons u (iterates f (f u)))" |
|
823 |
by (subst iterates) rule |
|
824 |
also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))" |
|
825 |
by (rule funpow_lmap) |
|
826 |
also have "(lmap f ^ n) (iterates f (f u)) = (lmap f ^ Suc n) (iterates f u)" |
|
827 |
by (simp add: lmap_iterates funpow_swap1) |
|
828 |
finally show ?thesis . |
|
829 |
qed |
|
830 |
finally have ?EqLCons by (auto simp del: funpow.simps) |
|
831 |
then show ?case .. |
|
832 |
qed |
|
833 |
qed |
|
834 |
||
835 |
lemma lappend_iterates: "lappend (iterates f x) l = iterates f x" |
|
836 |
proof - |
|
837 |
have "(lappend (iterates f x) l, iterates f x) \<in> |
|
838 |
{(lappend (iterates f u) l, iterates f u) | u. True}" by blast |
|
839 |
then show ?thesis |
|
840 |
proof (coinduct rule: llist_equalityI) |
|
841 |
case (Eqllist q) |
|
842 |
then obtain x where "q = (lappend (iterates f x) l, iterates f x)" by blast |
|
843 |
also have "iterates f x = LCons x (iterates f (f x))" by (rule iterates) |
|
844 |
finally have ?EqLCons by auto |
|
845 |
then show ?case .. |
|
846 |
qed |
|
847 |
qed |
|
848 |
||
849 |
end |