|
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(); |