author | paulson |
Fri, 11 Sep 1998 18:09:54 +0200 (1998-09-11) | |
changeset 5484 | e9430ed7e8d6 |
parent 5147 | 825877190618 |
child 6046 | 2c8a8be36c94 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/tf.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Trees & forests, a mutually recursive type definition. |
|
515 | 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>)))" |
|
0 | 12 |
*) |
13 |
||
515 | 14 |
open TF; |
0 | 15 |
|
515 | 16 |
val [TconsI, FnilI, FconsI] = tree_forest.intrs; |
0 | 17 |
|
18 |
(** tree_forest(A) as the union of tree(A) and forest(A) **) |
|
19 |
||
739 | 20 |
val [_, tree_def, forest_def] = tree_forest.defs; |
21 |
||
5068 | 22 |
Goalw [tree_def] "tree(A) <= tree_forest(A)"; |
0 | 23 |
by (rtac Part_subset 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
24 |
qed "tree_subset_TF"; |
0 | 25 |
|
5068 | 26 |
Goalw [forest_def] "forest(A) <= tree_forest(A)"; |
0 | 27 |
by (rtac Part_subset 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
28 |
qed "forest_subset_TF"; |
0 | 29 |
|
5068 | 30 |
Goal "tree(A) Un forest(A) = tree_forest(A)"; |
739 | 31 |
by (safe_tac (subset_cs addSIs [equalityI, tree_subset_TF, forest_subset_TF])); |
4091 | 32 |
by (fast_tac (claset() addSIs tree_forest.intrs addEs [tree_forest.elim]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
33 |
qed "TF_equals_Un"; |
0 | 34 |
|
35 |
(** NOT useful, but interesting... **) |
|
36 |
||
5068 | 37 |
Goalw [tree_def, forest_def] |
434 | 38 |
"tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))"; |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
39 |
let open tree_forest; |
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
40 |
val rew = rewrite_rule (con_defs @ tl defs) in |
4091 | 41 |
by (fast_tac (claset() addSIs (map rew intrs RL [PartD1]) addEs [rew elim]) 1) |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
42 |
end; |
760 | 43 |
qed "tree_forest_unfold"; |
434 | 44 |
|
739 | 45 |
val tree_forest_unfold' = rewrite_rule [tree_def, forest_def] |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
46 |
tree_forest_unfold; |
434 | 47 |
|
5068 | 48 |
Goalw [tree_def, forest_def] |
515 | 49 |
"tree(A) = {Inl(x). x: A*forest(A)}"; |
438 | 50 |
by (rtac (Part_Inl RS subst) 1); |
51 |
by (rtac (tree_forest_unfold' RS subst_context) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
52 |
qed "tree_unfold"; |
0 | 53 |
|
5068 | 54 |
Goalw [tree_def, forest_def] |
515 | 55 |
"forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}"; |
438 | 56 |
by (rtac (Part_Inr RS subst) 1); |
57 |
by (rtac (tree_forest_unfold' RS subst_context) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
58 |
qed "forest_unfold"; |
0 | 59 |
|
434 | 60 |
|
515 | 61 |
(*** TF_rec -- by Vset recursion ***) |
434 | 62 |
|
515 | 63 |
(** conversion rules **) |
64 |
||
5068 | 65 |
Goal "TF_rec(Tcons(a,f), b, c, d) = b(a, f, TF_rec(f,b,c,d))"; |
515 | 66 |
by (rtac (TF_rec_def RS def_Vrec RS trans) 1); |
67 |
by (rewrite_goals_tac tree_forest.con_defs); |
|
68 |
by (simp_tac rank_ss 1); |
|
760 | 69 |
qed "TF_rec_Tcons"; |
515 | 70 |
|
5068 | 71 |
Goal "TF_rec(Fnil, b, c, d) = c"; |
515 | 72 |
by (rtac (TF_rec_def RS def_Vrec RS trans) 1); |
73 |
by (rewrite_goals_tac tree_forest.con_defs); |
|
2469 | 74 |
by (Simp_tac 1); |
760 | 75 |
qed "TF_rec_Fnil"; |
515 | 76 |
|
5068 | 77 |
Goal "TF_rec(Fcons(t,f), b, c, d) = \ |
515 | 78 |
\ d(t, f, TF_rec(t, b, c, d), TF_rec(f, b, c, d))"; |
79 |
by (rtac (TF_rec_def RS def_Vrec RS trans) 1); |
|
80 |
by (rewrite_goals_tac tree_forest.con_defs); |
|
81 |
by (simp_tac rank_ss 1); |
|
760 | 82 |
qed "TF_rec_Fcons"; |
515 | 83 |
|
2469 | 84 |
Addsimps [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI]; |
515 | 85 |
|
86 |
(** Type checking **) |
|
87 |
||
88 |
val major::prems = goal TF.thy |
|
89 |
"[| z: tree_forest(A); \ |
|
1461 | 90 |
\ !!x f r. [| x: A; f: forest(A); r: C(f) \ |
91 |
\ |] ==> b(x,f,r): C(Tcons(x,f)); \ |
|
92 |
\ c : C(Fnil); \ |
|
515 | 93 |
\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: C(f) \ |
1461 | 94 |
\ |] ==> d(t,f,r1,r2): C(Fcons(t,f)) \ |
515 | 95 |
\ |] ==> TF_rec(z,b,c,d) : C(z)"; |
96 |
by (rtac (major RS tree_forest.induct) 1); |
|
4091 | 97 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
760 | 98 |
qed "TF_rec_type"; |
515 | 99 |
|
100 |
(*Mutually recursive version*) |
|
101 |
val prems = goal TF.thy |
|
1461 | 102 |
"[| !!x f r. [| x: A; f: forest(A); r: D(f) \ |
103 |
\ |] ==> b(x,f,r): C(Tcons(x,f)); \ |
|
104 |
\ c : D(Fnil); \ |
|
515 | 105 |
\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: D(f) \ |
1461 | 106 |
\ |] ==> d(t,f,r1,r2): D(Fcons(t,f)) \ |
107 |
\ |] ==> (ALL t:tree(A). TF_rec(t,b,c,d) : C(t)) & \ |
|
515 | 108 |
\ (ALL f: forest(A). TF_rec(f,b,c,d) : D(f))"; |
109 |
by (rewtac Ball_def); |
|
110 |
by (rtac tree_forest.mutual_induct 1); |
|
4091 | 111 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
112 |
qed "tree_forest_rec_type"; |
515 | 113 |
|
114 |
||
115 |
(** Versions for use with definitions **) |
|
116 |
||
117 |
val [rew] = goal TF.thy |
|
118 |
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))"; |
|
119 |
by (rewtac rew); |
|
120 |
by (rtac TF_rec_Tcons 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
121 |
qed "def_TF_rec_Tcons"; |
515 | 122 |
|
123 |
val [rew] = goal TF.thy |
|
124 |
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c"; |
|
125 |
by (rewtac rew); |
|
126 |
by (rtac TF_rec_Fnil 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
127 |
qed "def_TF_rec_Fnil"; |
515 | 128 |
|
129 |
val [rew] = goal TF.thy |
|
130 |
"[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))"; |
|
131 |
by (rewtac rew); |
|
132 |
by (rtac TF_rec_Fcons 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
133 |
qed "def_TF_rec_Fcons"; |
515 | 134 |
|
135 |
fun TF_recs def = map standard |
|
1461 | 136 |
([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]); |
515 | 137 |
|
138 |
||
139 |
(** list_of_TF and TF_of_list **) |
|
140 |
||
141 |
val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] = |
|
1461 | 142 |
TF_recs list_of_TF_def; |
2469 | 143 |
Addsimps [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons]; |
515 | 144 |
|
5068 | 145 |
Goalw [list_of_TF_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
146 |
"z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))"; |
515 | 147 |
by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
148 |
qed "list_of_TF_type"; |
515 | 149 |
|
150 |
val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def; |
|
2469 | 151 |
Addsimps [TF_of_list_Nil,TF_of_list_Cons]; |
515 | 152 |
|
5068 | 153 |
Goalw [TF_of_list_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
154 |
"l: list(tree(A)) ==> TF_of_list(l) : forest(A)"; |
515 | 155 |
by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
156 |
qed "TF_of_list_type"; |
515 | 157 |
|
158 |
||
159 |
(** TF_map **) |
|
160 |
||
161 |
val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def; |
|
2469 | 162 |
Addsimps [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons]; |
515 | 163 |
|
164 |
val prems = goalw TF.thy [TF_map_def] |
|
165 |
"[| !!x. x: A ==> h(x): B |] ==> \ |
|
166 |
\ (ALL t:tree(A). TF_map(h,t) : tree(B)) & \ |
|
167 |
\ (ALL f: forest(A). TF_map(h,f) : forest(B))"; |
|
168 |
by (REPEAT |
|
169 |
(ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
170 |
qed "TF_map_type"; |
515 | 171 |
|
172 |
||
173 |
(** TF_size **) |
|
174 |
||
175 |
val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def; |
|
2469 | 176 |
Addsimps [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons]; |
515 | 177 |
|
5068 | 178 |
Goalw [TF_size_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
179 |
"z: tree_forest(A) ==> TF_size(z) : nat"; |
515 | 180 |
by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
181 |
qed "TF_size_type"; |
515 | 182 |
|
183 |
||
184 |
(** TF_preorder **) |
|
185 |
||
186 |
val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] = |
|
1461 | 187 |
TF_recs TF_preorder_def; |
2469 | 188 |
Addsimps [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons]; |
515 | 189 |
|
5068 | 190 |
Goalw [TF_preorder_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
191 |
"z: tree_forest(A) ==> TF_preorder(z) : list(A)"; |
515 | 192 |
by (REPEAT (ares_tac ([TF_rec_type, app_type] @ list.intrs) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
193 |
qed "TF_preorder_type"; |
515 | 194 |
|
195 |
||
196 |
(** Term simplification **) |
|
197 |
||
198 |
val treeI = tree_subset_TF RS subsetD |
|
199 |
and forestI = forest_subset_TF RS subsetD; |
|
200 |
||
201 |
val TF_typechecks = |
|
202 |
[TconsI, FnilI, FconsI, treeI, forestI, |
|
203 |
list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type]; |
|
204 |
||
4091 | 205 |
simpset_ref() := simpset() setSolver type_auto_tac (list_typechecks@TF_typechecks); |
515 | 206 |
|
207 |
(** theorems about list_of_TF and TF_of_list **) |
|
208 |
||
209 |
(*essentially the same as list induction*) |
|
210 |
val major::prems = goal TF.thy |
|
1461 | 211 |
"[| f: forest(A); \ |
515 | 212 |
\ R(Fnil); \ |
213 |
\ !!t f. [| t: tree(A); f: forest(A); R(f) |] ==> R(Fcons(t,f)) \ |
|
214 |
\ |] ==> R(f)"; |
|
215 |
by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1); |
|
216 |
by (REPEAT (ares_tac (TrueI::prems) 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
217 |
qed "forest_induct"; |
515 | 218 |
|
5137 | 219 |
Goal "f: forest(A) ==> TF_of_list(list_of_TF(f)) = f"; |
515 | 220 |
by (etac forest_induct 1); |
2469 | 221 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
222 |
qed "forest_iso"; |
515 | 223 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
224 |
Goal "ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts"; |
515 | 225 |
by (etac list.induct 1); |
2469 | 226 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
227 |
qed "tree_list_iso"; |
515 | 228 |
|
229 |
(** theorems about TF_map **) |
|
230 |
||
5137 | 231 |
Goal "z: tree_forest(A) ==> TF_map(%u. u, z) = z"; |
515 | 232 |
by (etac tree_forest.induct 1); |
2469 | 233 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
234 |
qed "TF_map_ident"; |
515 | 235 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
236 |
Goal "z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u. h(j(u)), z)"; |
515 | 237 |
by (etac tree_forest.induct 1); |
2469 | 238 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
239 |
qed "TF_map_compose"; |
515 | 240 |
|
241 |
(** theorems about TF_size **) |
|
242 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
243 |
Goal "z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)"; |
515 | 244 |
by (etac tree_forest.induct 1); |
2469 | 245 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
246 |
qed "TF_size_TF_map"; |
515 | 247 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
248 |
Goal "z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))"; |
515 | 249 |
by (etac tree_forest.induct 1); |
4091 | 250 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
251 |
qed "TF_size_length"; |
515 | 252 |
|
253 |
(** theorems about TF_preorder **) |
|
254 |
||
5137 | 255 |
Goal "z: tree_forest(A) ==> \ |
515 | 256 |
\ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))"; |
257 |
by (etac tree_forest.induct 1); |
|
4091 | 258 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
259 |
qed "TF_preorder_TF_map"; |