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