author | wenzelm |
Wed, 13 Jul 2005 16:07:35 +0200 | |
changeset 16813 | 67140ae50e77 |
parent 16417 | 9bc16273c2d4 |
child 18415 | eb68dc98bda2 |
permissions | -rw-r--r-- |
12201 | 1 |
(* Title: ZF/Induct/Tree_Forest.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
*) |
|
6 |
||
7 |
header {* Trees and forests, a mutually recursive type definition *} |
|
8 |
||
16417 | 9 |
theory Tree_Forest imports Main begin |
12201 | 10 |
|
11 |
subsection {* Datatype definition *} |
|
12 |
||
13 |
consts |
|
14 |
tree :: "i => i" |
|
15 |
forest :: "i => i" |
|
16 |
tree_forest :: "i => i" |
|
17 |
||
18 |
datatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)") |
|
19 |
and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)") |
|
20 |
||
21 |
declare tree_forest.intros [simp, TC] |
|
22 |
||
12216 | 23 |
lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)" |
12201 | 24 |
by (simp only: tree_forest.defs) |
25 |
||
12216 | 26 |
lemma forest_def: "forest(A) == Part(tree_forest(A), Inr)" |
12201 | 27 |
by (simp only: tree_forest.defs) |
28 |
||
29 |
||
30 |
text {* |
|
12205 | 31 |
\medskip @{term "tree_forest(A)"} as the union of @{term "tree(A)"} |
12201 | 32 |
and @{term "forest(A)"}. |
33 |
*} |
|
34 |
||
35 |
lemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)" |
|
36 |
apply (unfold tree_forest.defs) |
|
37 |
apply (rule Part_subset) |
|
38 |
done |
|
39 |
||
12243 | 40 |
lemma treeI [TC]: "x \<in> tree(A) ==> x \<in> tree_forest(A)" |
12201 | 41 |
by (rule tree_subset_TF [THEN subsetD]) |
42 |
||
43 |
lemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)" |
|
44 |
apply (unfold tree_forest.defs) |
|
45 |
apply (rule Part_subset) |
|
46 |
done |
|
47 |
||
13535 | 48 |
lemma treeI' [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)" |
12201 | 49 |
by (rule forest_subset_TF [THEN subsetD]) |
50 |
||
51 |
lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)" |
|
52 |
apply (insert tree_subset_TF forest_subset_TF) |
|
53 |
apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases) |
|
54 |
done |
|
55 |
||
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
56 |
lemma |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
57 |
notes rews = tree_forest.con_defs tree_def forest_def |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
58 |
shows |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
59 |
tree_forest_unfold: "tree_forest(A) = |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
60 |
(A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))" |
12201 | 61 |
-- {* NOT useful, but interesting \dots *} |
62 |
apply (unfold tree_def forest_def) |
|
63 |
apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1] |
|
64 |
elim: tree_forest.cases [unfolded rews]) |
|
65 |
done |
|
66 |
||
67 |
lemma tree_forest_unfold': |
|
68 |
"tree_forest(A) = |
|
69 |
A \<times> Part(tree_forest(A), \<lambda>w. Inr(w)) + |
|
70 |
{0} + Part(tree_forest(A), \<lambda>w. Inl(w)) * Part(tree_forest(A), \<lambda>w. Inr(w))" |
|
71 |
by (rule tree_forest_unfold [unfolded tree_def forest_def]) |
|
72 |
||
73 |
lemma tree_unfold: "tree(A) = {Inl(x). x \<in> A \<times> forest(A)}" |
|
74 |
apply (unfold tree_def forest_def) |
|
75 |
apply (rule Part_Inl [THEN subst]) |
|
76 |
apply (rule tree_forest_unfold' [THEN subst_context]) |
|
77 |
done |
|
78 |
||
79 |
lemma forest_unfold: "forest(A) = {Inr(x). x \<in> {0} + tree(A)*forest(A)}" |
|
80 |
apply (unfold tree_def forest_def) |
|
81 |
apply (rule Part_Inr [THEN subst]) |
|
82 |
apply (rule tree_forest_unfold' [THEN subst_context]) |
|
83 |
done |
|
84 |
||
85 |
text {* |
|
86 |
\medskip Type checking for recursor: Not needed; possibly interesting? |
|
87 |
*} |
|
88 |
||
89 |
lemma TF_rec_type: |
|
90 |
"[| z \<in> tree_forest(A); |
|
91 |
!!x f r. [| x \<in> A; f \<in> forest(A); r \<in> C(f) |
|
12243 | 92 |
|] ==> b(x,f,r) \<in> C(Tcons(x,f)); |
12201 | 93 |
c \<in> C(Fnil); |
12243 | 94 |
!!t f r1 r2. [| t \<in> tree(A); f \<in> forest(A); r1 \<in> C(t); r2 \<in> C(f) |
95 |
|] ==> d(t,f,r1,r2) \<in> C(Fcons(t,f)) |
|
12201 | 96 |
|] ==> tree_forest_rec(b,c,d,z) \<in> C(z)" |
97 |
by (induct_tac z) simp_all |
|
98 |
||
99 |
lemma tree_forest_rec_type: |
|
100 |
"[| !!x f r. [| x \<in> A; f \<in> forest(A); r \<in> D(f) |
|
12243 | 101 |
|] ==> b(x,f,r) \<in> C(Tcons(x,f)); |
12201 | 102 |
c \<in> D(Fnil); |
12243 | 103 |
!!t f r1 r2. [| t \<in> tree(A); f \<in> forest(A); r1 \<in> C(t); r2 \<in> D(f) |
104 |
|] ==> d(t,f,r1,r2) \<in> D(Fcons(t,f)) |
|
105 |
|] ==> (\<forall>t \<in> tree(A). tree_forest_rec(b,c,d,t) \<in> C(t)) \<and> |
|
12201 | 106 |
(\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))" |
107 |
-- {* Mutually recursive version. *} |
|
12243 | 108 |
apply (unfold Ball_def) |
12201 | 109 |
apply (rule tree_forest.mutual_induct) |
110 |
apply simp_all |
|
111 |
done |
|
112 |
||
113 |
||
114 |
subsection {* Operations *} |
|
115 |
||
116 |
consts |
|
117 |
map :: "[i => i, i] => i" |
|
118 |
size :: "i => i" |
|
119 |
preorder :: "i => i" |
|
120 |
list_of_TF :: "i => i" |
|
121 |
of_list :: "i => i" |
|
122 |
reflect :: "i => i" |
|
123 |
||
124 |
primrec |
|
125 |
"list_of_TF (Tcons(x,f)) = [Tcons(x,f)]" |
|
126 |
"list_of_TF (Fnil) = []" |
|
127 |
"list_of_TF (Fcons(t,tf)) = Cons (t, list_of_TF(tf))" |
|
128 |
||
129 |
primrec |
|
130 |
"of_list([]) = Fnil" |
|
131 |
"of_list(Cons(t,l)) = Fcons(t, of_list(l))" |
|
132 |
||
133 |
primrec |
|
134 |
"map (h, Tcons(x,f)) = Tcons(h(x), map(h,f))" |
|
135 |
"map (h, Fnil) = Fnil" |
|
136 |
"map (h, Fcons(t,tf)) = Fcons (map(h, t), map(h, tf))" |
|
137 |
||
138 |
primrec |
|
139 |
"size (Tcons(x,f)) = succ(size(f))" |
|
140 |
"size (Fnil) = 0" |
|
141 |
"size (Fcons(t,tf)) = size(t) #+ size(tf)" |
|
142 |
||
143 |
primrec |
|
144 |
"preorder (Tcons(x,f)) = Cons(x, preorder(f))" |
|
145 |
"preorder (Fnil) = Nil" |
|
146 |
"preorder (Fcons(t,tf)) = preorder(t) @ preorder(tf)" |
|
147 |
||
148 |
primrec |
|
149 |
"reflect (Tcons(x,f)) = Tcons(x, reflect(f))" |
|
150 |
"reflect (Fnil) = Fnil" |
|
151 |
"reflect (Fcons(t,tf)) = |
|
152 |
of_list (list_of_TF (reflect(tf)) @ Cons(reflect(t), Nil))" |
|
153 |
||
154 |
||
155 |
text {* |
|
156 |
\medskip @{text list_of_TF} and @{text of_list}. |
|
157 |
*} |
|
158 |
||
159 |
lemma list_of_TF_type [TC]: |
|
160 |
"z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))" |
|
161 |
apply (erule tree_forest.induct) |
|
162 |
apply simp_all |
|
163 |
done |
|
164 |
||
12243 | 165 |
lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)" |
12201 | 166 |
apply (erule list.induct) |
167 |
apply simp_all |
|
168 |
done |
|
169 |
||
170 |
text {* |
|
171 |
\medskip @{text map}. |
|
172 |
*} |
|
173 |
||
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
174 |
lemma |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
175 |
assumes h_type: "!!x. x \<in> A ==> h(x): B" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
176 |
shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12610
diff
changeset
|
177 |
and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)" |
12243 | 178 |
apply (induct rule: tree_forest.mutual_induct) |
179 |
apply (insert h_type) |
|
180 |
apply simp_all |
|
12201 | 181 |
done |
182 |
||
183 |
text {* |
|
184 |
\medskip @{text size}. |
|
185 |
*} |
|
186 |
||
187 |
lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat" |
|
188 |
apply (erule tree_forest.induct) |
|
189 |
apply simp_all |
|
190 |
done |
|
191 |
||
192 |
||
193 |
text {* |
|
194 |
\medskip @{text preorder}. |
|
195 |
*} |
|
196 |
||
197 |
lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)" |
|
198 |
apply (erule tree_forest.induct) |
|
199 |
apply simp_all |
|
200 |
done |
|
201 |
||
202 |
||
203 |
text {* |
|
204 |
\medskip Theorems about @{text list_of_TF} and @{text of_list}. |
|
205 |
*} |
|
206 |
||
207 |
lemma forest_induct: |
|
208 |
"[| f \<in> forest(A); |
|
209 |
R(Fnil); |
|
210 |
!!t f. [| t \<in> tree(A); f \<in> forest(A); R(f) |] ==> R(Fcons(t,f)) |
|
211 |
|] ==> R(f)" |
|
212 |
-- {* Essentially the same as list induction. *} |
|
12610 | 213 |
apply (erule tree_forest.mutual_induct |
214 |
[THEN conjunct2, THEN spec, THEN [2] rev_mp]) |
|
12201 | 215 |
apply (rule TrueI) |
216 |
apply simp |
|
217 |
apply simp |
|
218 |
done |
|
219 |
||
220 |
lemma forest_iso: "f \<in> forest(A) ==> of_list(list_of_TF(f)) = f" |
|
221 |
apply (erule forest_induct) |
|
222 |
apply simp_all |
|
223 |
done |
|
224 |
||
225 |
lemma tree_list_iso: "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts" |
|
226 |
apply (erule list.induct) |
|
227 |
apply simp_all |
|
228 |
done |
|
229 |
||
230 |
||
231 |
text {* |
|
232 |
\medskip Theorems about @{text map}. |
|
233 |
*} |
|
234 |
||
235 |
lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z" |
|
236 |
apply (erule tree_forest.induct) |
|
237 |
apply simp_all |
|
238 |
done |
|
239 |
||
12216 | 240 |
lemma map_compose: |
241 |
"z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)" |
|
12201 | 242 |
apply (erule tree_forest.induct) |
243 |
apply simp_all |
|
244 |
done |
|
245 |
||
246 |
||
247 |
text {* |
|
248 |
\medskip Theorems about @{text size}. |
|
249 |
*} |
|
250 |
||
251 |
lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)" |
|
252 |
apply (erule tree_forest.induct) |
|
253 |
apply simp_all |
|
254 |
done |
|
255 |
||
256 |
lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))" |
|
257 |
apply (erule tree_forest.induct) |
|
258 |
apply (simp_all add: length_app) |
|
259 |
done |
|
260 |
||
261 |
text {* |
|
262 |
\medskip Theorems about @{text preorder}. |
|
263 |
*} |
|
264 |
||
265 |
lemma preorder_map: |
|
266 |
"z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))" |
|
267 |
apply (erule tree_forest.induct) |
|
268 |
apply (simp_all add: map_app_distrib) |
|
269 |
done |
|
270 |
||
271 |
end |