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 |
|
|
9 |
theory Tree_Forest = Main:
|
|
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 |
|
|
40 |
lemma treeI [TC]: "x : tree(A) ==> x : tree_forest(A)"
|
|
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 |
|
|
48 |
lemma treeI [TC]: "x : forest(A) ==> x : tree_forest(A)"
|
|
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 |
|
|
56 |
lemma (notes rews = tree_forest.con_defs tree_def forest_def)
|
|
57 |
tree_forest_unfold: "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))"
|
|
58 |
-- {* NOT useful, but interesting \dots *}
|
|
59 |
apply (unfold tree_def forest_def)
|
|
60 |
apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
|
|
61 |
elim: tree_forest.cases [unfolded rews])
|
|
62 |
done
|
|
63 |
|
|
64 |
lemma tree_forest_unfold':
|
|
65 |
"tree_forest(A) =
|
|
66 |
A \<times> Part(tree_forest(A), \<lambda>w. Inr(w)) +
|
|
67 |
{0} + Part(tree_forest(A), \<lambda>w. Inl(w)) * Part(tree_forest(A), \<lambda>w. Inr(w))"
|
|
68 |
by (rule tree_forest_unfold [unfolded tree_def forest_def])
|
|
69 |
|
|
70 |
lemma tree_unfold: "tree(A) = {Inl(x). x \<in> A \<times> forest(A)}"
|
|
71 |
apply (unfold tree_def forest_def)
|
|
72 |
apply (rule Part_Inl [THEN subst])
|
|
73 |
apply (rule tree_forest_unfold' [THEN subst_context])
|
|
74 |
done
|
|
75 |
|
|
76 |
lemma forest_unfold: "forest(A) = {Inr(x). x \<in> {0} + tree(A)*forest(A)}"
|
|
77 |
apply (unfold tree_def forest_def)
|
|
78 |
apply (rule Part_Inr [THEN subst])
|
|
79 |
apply (rule tree_forest_unfold' [THEN subst_context])
|
|
80 |
done
|
|
81 |
|
|
82 |
text {*
|
|
83 |
\medskip Type checking for recursor: Not needed; possibly interesting?
|
|
84 |
*}
|
|
85 |
|
|
86 |
lemma TF_rec_type:
|
|
87 |
"[| z \<in> tree_forest(A);
|
|
88 |
!!x f r. [| x \<in> A; f \<in> forest(A); r \<in> C(f)
|
|
89 |
|] ==> b(x,f,r): C(Tcons(x,f));
|
|
90 |
c \<in> C(Fnil);
|
|
91 |
!!t f r1 r2. [| t \<in> tree(A); f \<in> forest(A); r1: C(t); r2: C(f)
|
|
92 |
|] ==> d(t,f,r1,r2): C(Fcons(t,f))
|
|
93 |
|] ==> tree_forest_rec(b,c,d,z) \<in> C(z)"
|
|
94 |
by (induct_tac z) simp_all
|
|
95 |
|
|
96 |
lemma tree_forest_rec_type:
|
|
97 |
"[| !!x f r. [| x \<in> A; f \<in> forest(A); r \<in> D(f)
|
|
98 |
|] ==> b(x,f,r): C(Tcons(x,f));
|
|
99 |
c \<in> D(Fnil);
|
|
100 |
!!t f r1 r2. [| t \<in> tree(A); f \<in> forest(A); r1: C(t); r2: D(f)
|
|
101 |
|] ==> d(t,f,r1,r2): D(Fcons(t,f))
|
|
102 |
|] ==> (\<forall>t \<in> tree(A). tree_forest_rec(b,c,d,t) \<in> C(t)) &
|
|
103 |
(\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
|
|
104 |
-- {* Mutually recursive version. *}
|
|
105 |
apply (unfold Ball_def) (* FIXME *)
|
|
106 |
apply (rule tree_forest.mutual_induct)
|
|
107 |
apply simp_all
|
|
108 |
done
|
|
109 |
|
|
110 |
|
|
111 |
subsection {* Operations *}
|
|
112 |
|
|
113 |
consts
|
|
114 |
map :: "[i => i, i] => i"
|
|
115 |
size :: "i => i"
|
|
116 |
preorder :: "i => i"
|
|
117 |
list_of_TF :: "i => i"
|
|
118 |
of_list :: "i => i"
|
|
119 |
reflect :: "i => i"
|
|
120 |
|
|
121 |
primrec
|
|
122 |
"list_of_TF (Tcons(x,f)) = [Tcons(x,f)]"
|
|
123 |
"list_of_TF (Fnil) = []"
|
|
124 |
"list_of_TF (Fcons(t,tf)) = Cons (t, list_of_TF(tf))"
|
|
125 |
|
|
126 |
primrec
|
|
127 |
"of_list([]) = Fnil"
|
|
128 |
"of_list(Cons(t,l)) = Fcons(t, of_list(l))"
|
|
129 |
|
|
130 |
primrec
|
|
131 |
"map (h, Tcons(x,f)) = Tcons(h(x), map(h,f))"
|
|
132 |
"map (h, Fnil) = Fnil"
|
|
133 |
"map (h, Fcons(t,tf)) = Fcons (map(h, t), map(h, tf))"
|
|
134 |
|
|
135 |
primrec
|
|
136 |
"size (Tcons(x,f)) = succ(size(f))"
|
|
137 |
"size (Fnil) = 0"
|
|
138 |
"size (Fcons(t,tf)) = size(t) #+ size(tf)"
|
|
139 |
|
|
140 |
primrec
|
|
141 |
"preorder (Tcons(x,f)) = Cons(x, preorder(f))"
|
|
142 |
"preorder (Fnil) = Nil"
|
|
143 |
"preorder (Fcons(t,tf)) = preorder(t) @ preorder(tf)"
|
|
144 |
|
|
145 |
primrec
|
|
146 |
"reflect (Tcons(x,f)) = Tcons(x, reflect(f))"
|
|
147 |
"reflect (Fnil) = Fnil"
|
|
148 |
"reflect (Fcons(t,tf)) =
|
|
149 |
of_list (list_of_TF (reflect(tf)) @ Cons(reflect(t), Nil))"
|
|
150 |
|
|
151 |
|
|
152 |
text {*
|
|
153 |
\medskip @{text list_of_TF} and @{text of_list}.
|
|
154 |
*}
|
|
155 |
|
|
156 |
lemma list_of_TF_type [TC]:
|
|
157 |
"z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))"
|
|
158 |
apply (erule tree_forest.induct)
|
|
159 |
apply simp_all
|
|
160 |
done
|
|
161 |
|
|
162 |
lemma map_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
|
|
163 |
apply (erule list.induct)
|
|
164 |
apply simp_all
|
|
165 |
done
|
|
166 |
|
|
167 |
text {*
|
|
168 |
\medskip @{text map}.
|
|
169 |
*}
|
|
170 |
|
|
171 |
lemma map_type:
|
|
172 |
"[| !!x. x \<in> A ==> h(x): B |] ==>
|
|
173 |
(\<forall>t \<in> tree(A). map(h,t) \<in> tree(B)) &
|
|
174 |
(\<forall>f \<in> forest(A). map(h,f) \<in> forest(B))"
|
|
175 |
apply (unfold Ball_def) (* FIXME *)
|
|
176 |
apply (rule tree_forest.mutual_induct)
|
|
177 |
apply simp_all
|
|
178 |
done
|
|
179 |
|
|
180 |
|
|
181 |
text {*
|
|
182 |
\medskip @{text size}.
|
|
183 |
*}
|
|
184 |
|
|
185 |
lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
|
|
186 |
apply (erule tree_forest.induct)
|
|
187 |
apply simp_all
|
|
188 |
done
|
|
189 |
|
|
190 |
|
|
191 |
text {*
|
|
192 |
\medskip @{text preorder}.
|
|
193 |
*}
|
|
194 |
|
|
195 |
lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
|
|
196 |
apply (erule tree_forest.induct)
|
|
197 |
apply simp_all
|
|
198 |
done
|
|
199 |
|
|
200 |
|
|
201 |
text {*
|
|
202 |
\medskip Theorems about @{text list_of_TF} and @{text of_list}.
|
|
203 |
*}
|
|
204 |
|
|
205 |
lemma forest_induct:
|
|
206 |
"[| f \<in> forest(A);
|
|
207 |
R(Fnil);
|
|
208 |
!!t f. [| t \<in> tree(A); f \<in> forest(A); R(f) |] ==> R(Fcons(t,f))
|
|
209 |
|] ==> R(f)"
|
|
210 |
-- {* Essentially the same as list induction. *}
|
|
211 |
apply (erule tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp])
|
|
212 |
apply (rule TrueI)
|
|
213 |
apply simp
|
|
214 |
apply simp
|
|
215 |
done
|
|
216 |
|
|
217 |
lemma forest_iso: "f \<in> forest(A) ==> of_list(list_of_TF(f)) = f"
|
|
218 |
apply (erule forest_induct)
|
|
219 |
apply simp_all
|
|
220 |
done
|
|
221 |
|
|
222 |
lemma tree_list_iso: "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts"
|
|
223 |
apply (erule list.induct)
|
|
224 |
apply simp_all
|
|
225 |
done
|
|
226 |
|
|
227 |
|
|
228 |
text {*
|
|
229 |
\medskip Theorems about @{text map}.
|
|
230 |
*}
|
|
231 |
|
|
232 |
lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
|
|
233 |
apply (erule tree_forest.induct)
|
|
234 |
apply simp_all
|
|
235 |
done
|
|
236 |
|
12216
|
237 |
lemma map_compose:
|
|
238 |
"z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
|
12201
|
239 |
apply (erule tree_forest.induct)
|
|
240 |
apply simp_all
|
|
241 |
done
|
|
242 |
|
|
243 |
|
|
244 |
text {*
|
|
245 |
\medskip Theorems about @{text size}.
|
|
246 |
*}
|
|
247 |
|
|
248 |
lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
|
|
249 |
apply (erule tree_forest.induct)
|
|
250 |
apply simp_all
|
|
251 |
done
|
|
252 |
|
|
253 |
lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))"
|
|
254 |
apply (erule tree_forest.induct)
|
|
255 |
apply (simp_all add: length_app)
|
|
256 |
done
|
|
257 |
|
|
258 |
text {*
|
|
259 |
\medskip Theorems about @{text preorder}.
|
|
260 |
*}
|
|
261 |
|
|
262 |
lemma preorder_map:
|
|
263 |
"z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))"
|
|
264 |
apply (erule tree_forest.induct)
|
|
265 |
apply (simp_all add: map_app_distrib)
|
|
266 |
done
|
|
267 |
|
|
268 |
end
|