0
|
1 |
(* Title: ZF/ex/tf.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1992 University of Cambridge
|
|
5 |
|
|
6 |
For tf.thy. Trees & forests, a mutually recursive type definition.
|
|
7 |
|
|
8 |
Still needs
|
|
9 |
|
|
10 |
"TF_reflect == (%z. TF_rec(z, %x ts r. Tcons(x,r), 0,
|
|
11 |
%t ts r1 r2. TF_of_list(list_of_TF(r2) @ <r1,0>)))"
|
|
12 |
*)
|
|
13 |
|
|
14 |
open TF_Fn;
|
|
15 |
|
|
16 |
|
|
17 |
(*** TF_rec -- by Vset recursion ***)
|
|
18 |
|
|
19 |
(*Used only to verify TF_rec*)
|
|
20 |
val TF_congs = mk_typed_congs TF.thy
|
|
21 |
[("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
|
|
22 |
|
|
23 |
(** conversion rules **)
|
|
24 |
|
|
25 |
goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
|
|
26 |
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
|
|
27 |
by (rewrite_goals_tac TF.con_defs);
|
|
28 |
by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
|
|
29 |
val TF_rec_Tcons = result();
|
|
30 |
|
|
31 |
goal TF_Fn.thy "TF_rec(Fnil, b, c, d) = c";
|
|
32 |
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
|
|
33 |
by (rewrite_goals_tac TF.con_defs);
|
|
34 |
by (SIMP_TAC rank_ss 1);
|
|
35 |
val TF_rec_Fnil = result();
|
|
36 |
|
|
37 |
goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
|
|
38 |
\ d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
|
|
39 |
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
|
|
40 |
by (rewrite_goals_tac TF.con_defs);
|
|
41 |
by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
|
|
42 |
val TF_rec_Fcons = result();
|
|
43 |
|
|
44 |
(*list_ss includes list operations as well as arith_ss*)
|
|
45 |
val TF_rec_ss = list_ss addrews
|
|
46 |
[TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
|
|
47 |
|
|
48 |
(** Type checking **)
|
|
49 |
|
|
50 |
val major::prems = goal TF_Fn.thy
|
|
51 |
"[| z: tree_forest(A); \
|
|
52 |
\ !!x tf r. [| x: A; tf: forest(A); r: C(tf) \
|
|
53 |
\ |] ==> b(x,tf,r): C(Tcons(x,tf)); \
|
|
54 |
\ c : C(Fnil); \
|
|
55 |
\ !!t tf r1 r2. [| t: tree(A); tf: forest(A); r1: C(t); r2: C(tf) \
|
|
56 |
\ |] ==> d(t,tf,r1,r2): C(Fcons(t,tf)) \
|
|
57 |
\ |] ==> TF_rec(z,b,c,d) : C(z)";
|
|
58 |
by (rtac (major RS TF.induct) 1);
|
|
59 |
by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
|
|
60 |
val TF_rec_type = result();
|
|
61 |
|
|
62 |
(*Mutually recursive version*)
|
|
63 |
val prems = goal TF_Fn.thy
|
|
64 |
"[| !!x tf r. [| x: A; tf: forest(A); r: D(tf) \
|
|
65 |
\ |] ==> b(x,tf,r): C(Tcons(x,tf)); \
|
|
66 |
\ c : D(Fnil); \
|
|
67 |
\ !!t tf r1 r2. [| t: tree(A); tf: forest(A); r1: C(t); r2: D(tf) \
|
|
68 |
\ |] ==> d(t,tf,r1,r2): D(Fcons(t,tf)) \
|
|
69 |
\ |] ==> (ALL t:tree(A). TF_rec(t,b,c,d) : C(t)) & \
|
|
70 |
\ (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
|
|
71 |
by (rewtac Ball_def);
|
|
72 |
by (rtac TF.mutual_induct 1);
|
|
73 |
by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
|
|
74 |
val tree_forest_rec_type = result();
|
|
75 |
|
|
76 |
|
|
77 |
(** Versions for use with definitions **)
|
|
78 |
|
|
79 |
val [rew] = goal TF_Fn.thy
|
|
80 |
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,tf)) = b(a,tf,j(tf))";
|
|
81 |
by (rewtac rew);
|
|
82 |
by (rtac TF_rec_Tcons 1);
|
|
83 |
val def_TF_rec_Tcons = result();
|
|
84 |
|
|
85 |
val [rew] = goal TF_Fn.thy
|
|
86 |
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
|
|
87 |
by (rewtac rew);
|
|
88 |
by (rtac TF_rec_Fnil 1);
|
|
89 |
val def_TF_rec_Fnil = result();
|
|
90 |
|
|
91 |
val [rew] = goal TF_Fn.thy
|
|
92 |
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,tf)) = d(t,tf,j(t),j(tf))";
|
|
93 |
by (rewtac rew);
|
|
94 |
by (rtac TF_rec_Fcons 1);
|
|
95 |
val def_TF_rec_Fcons = result();
|
|
96 |
|
|
97 |
fun TF_recs def = map standard
|
|
98 |
([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
|
|
99 |
|
|
100 |
|
|
101 |
(** list_of_TF and TF_of_list **)
|
|
102 |
|
|
103 |
val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] =
|
|
104 |
TF_recs list_of_TF_def;
|
|
105 |
|
|
106 |
goalw TF_Fn.thy [list_of_TF_def]
|
|
107 |
"!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
|
|
108 |
by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
|
|
109 |
val list_of_TF_type = result();
|
|
110 |
|
|
111 |
val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
|
|
112 |
|
|
113 |
goalw TF_Fn.thy [TF_of_list_def]
|
|
114 |
"!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
|
|
115 |
by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
|
|
116 |
val TF_of_list_type = result();
|
|
117 |
|
|
118 |
|
|
119 |
(** TF_map **)
|
|
120 |
|
|
121 |
val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def;
|
|
122 |
|
|
123 |
val prems = goalw TF_Fn.thy [TF_map_def]
|
|
124 |
"[| !!x. x: A ==> h(x): B |] ==> \
|
|
125 |
\ (ALL t:tree(A). TF_map(h,t) : tree(B)) & \
|
|
126 |
\ (ALL tf: forest(A). TF_map(h,tf) : forest(B))";
|
|
127 |
by (REPEAT
|
|
128 |
(ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
|
|
129 |
val TF_map_type = result();
|
|
130 |
|
|
131 |
|
|
132 |
(** TF_size **)
|
|
133 |
|
|
134 |
val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def;
|
|
135 |
|
|
136 |
goalw TF_Fn.thy [TF_size_def]
|
|
137 |
"!!z A. z: tree_forest(A) ==> TF_size(z) : nat";
|
|
138 |
by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
|
|
139 |
val TF_size_type = result();
|
|
140 |
|
|
141 |
|
|
142 |
(** TF_preorder **)
|
|
143 |
|
|
144 |
val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] =
|
|
145 |
TF_recs TF_preorder_def;
|
|
146 |
|
|
147 |
goalw TF_Fn.thy [TF_preorder_def]
|
|
148 |
"!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)";
|
|
149 |
by (REPEAT (ares_tac [TF_rec_type, app_type,NilI, ConsI] 1));
|
|
150 |
val TF_preorder_type = result();
|
|
151 |
|
|
152 |
|
|
153 |
(** Term simplification **)
|
|
154 |
|
|
155 |
val treeI = tree_subset_TF RS subsetD
|
|
156 |
and forestI = forest_subset_TF RS subsetD;
|
|
157 |
|
|
158 |
val TF_typechecks =
|
|
159 |
[TconsI, FnilI, FconsI, treeI, forestI,
|
|
160 |
list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
|
|
161 |
|
|
162 |
val TF_congs = TF.congs @
|
|
163 |
mk_congs TF_Fn.thy
|
|
164 |
["TF_rec", "list_of_TF", "TF_of_list", "TF_map", "TF_size", "TF_preorder"];
|
|
165 |
|
|
166 |
val TF_rewrites =
|
|
167 |
[TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
|
|
168 |
list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
|
|
169 |
TF_of_list_Nil,TF_of_list_Cons,
|
|
170 |
TF_map_Tcons, TF_map_Fnil, TF_map_Fcons,
|
|
171 |
TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
|
|
172 |
TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
|
|
173 |
|
|
174 |
val TF_ss = list_ss addcongs TF_congs
|
|
175 |
addrews (TF_rewrites@TF_typechecks);
|
|
176 |
|
|
177 |
(** theorems about list_of_TF and TF_of_list **)
|
|
178 |
|
|
179 |
(*essentially the same as list induction*)
|
|
180 |
val major::prems = goal TF_Fn.thy
|
|
181 |
"[| tf: forest(A); \
|
|
182 |
\ R(Fnil); \
|
|
183 |
\ !!t tf. [| t: tree(A); tf: forest(A); R(tf) |] ==> R(Fcons(t,tf)) \
|
|
184 |
\ |] ==> R(tf)";
|
|
185 |
by (rtac (major RS (TF.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
|
|
186 |
by (REPEAT (ares_tac (TrueI::prems) 1));
|
|
187 |
val forest_induct = result();
|
|
188 |
|
|
189 |
goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
|
|
190 |
by (etac forest_induct 1);
|
|
191 |
by (ALLGOALS (ASM_SIMP_TAC TF_ss));
|
|
192 |
val forest_iso = result();
|
|
193 |
|
|
194 |
goal TF_Fn.thy
|
|
195 |
"!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
|
|
196 |
by (etac List.induct 1);
|
|
197 |
by (ALLGOALS (ASM_SIMP_TAC TF_ss));
|
|
198 |
val tree_list_iso = result();
|
|
199 |
|
|
200 |
(** theorems about TF_map **)
|
|
201 |
|
|
202 |
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
|
|
203 |
by (etac TF.induct 1);
|
|
204 |
by (ALLGOALS (ASM_SIMP_TAC TF_ss));
|
|
205 |
val TF_map_ident = result();
|
|
206 |
|
|
207 |
goal TF_Fn.thy
|
|
208 |
"!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
|
|
209 |
by (etac TF.induct 1);
|
|
210 |
by (ALLGOALS (ASM_SIMP_TAC TF_ss));
|
|
211 |
val TF_map_compose = result();
|
|
212 |
|
|
213 |
(** theorems about TF_size **)
|
|
214 |
|
|
215 |
goal TF_Fn.thy
|
|
216 |
"!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
|
|
217 |
by (etac TF.induct 1);
|
|
218 |
by (ALLGOALS (ASM_SIMP_TAC TF_ss));
|
|
219 |
val TF_size_TF_map = result();
|
|
220 |
|
|
221 |
goal TF_Fn.thy
|
|
222 |
"!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
|
|
223 |
by (etac TF.induct 1);
|
|
224 |
by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [length_app])));
|
|
225 |
val TF_size_length = result();
|
|
226 |
|
|
227 |
(** theorems about TF_preorder **)
|
|
228 |
|
|
229 |
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> \
|
|
230 |
\ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
|
|
231 |
by (etac TF.induct 1);
|
|
232 |
by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [map_app_distrib])));
|
|
233 |
val TF_preorder_TF_map = result();
|