0
|
1 |
(* Title: HOL/ex/simult.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
For simult.thy.
|
|
7 |
|
|
8 |
Primitives for simultaneous recursive type definitions
|
|
9 |
includes worked example of trees & forests
|
|
10 |
|
|
11 |
This is essentially the same data structure that on ex/term.ML, which is
|
|
12 |
simpler because it uses List as a new type former. The approach in this
|
|
13 |
file may be superior for other simultaneous recursions.
|
|
14 |
*)
|
|
15 |
|
|
16 |
open Simult;
|
|
17 |
|
|
18 |
(*** General rules for Part ***)
|
|
19 |
|
|
20 |
val prems = goalw Simult.thy [Part_def] "h(a) : A ==> h(a) : Part(A,h)";
|
|
21 |
by (cfast_tac prems 1);
|
|
22 |
val PartI = result();
|
|
23 |
|
|
24 |
val major::prems = goalw Simult.thy [Part_def]
|
|
25 |
"[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \
|
|
26 |
\ |] ==> P";
|
|
27 |
by (rtac (major RS CollectE) 1);
|
|
28 |
by (etac conjE 1);
|
|
29 |
by (etac exE 1);
|
|
30 |
by (REPEAT (ares_tac prems 1));
|
|
31 |
val PartE = result();
|
|
32 |
|
|
33 |
goal Simult.thy "!!A B. A<=B ==> Part(A,h) <= Part(B,h)";
|
|
34 |
by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
|
|
35 |
val Part_mono = result();
|
|
36 |
|
|
37 |
val [prem] = goal Simult.thy "A<=B ==> Part(A,h) <= B";
|
|
38 |
by (fast_tac (set_cs addSIs [PartI, prem RS subsetD] addSEs [PartE]) 1);
|
|
39 |
val Part_subset = result();
|
|
40 |
|
|
41 |
|
|
42 |
(*** Monotonicity and unfolding of the function ***)
|
|
43 |
|
|
44 |
goal Simult.thy "mono(%Z. A <*> Part(Z,In1) \
|
|
45 |
\ <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))";
|
|
46 |
by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
|
|
47 |
Part_mono] 1));
|
|
48 |
val TF_fun_mono = result();
|
|
49 |
|
|
50 |
val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
|
|
51 |
|
|
52 |
goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
|
|
53 |
by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
|
|
54 |
val TF_mono = result();
|
|
55 |
|
|
56 |
goalw Simult.thy [TF_def] "TF(Sexp) <= Sexp";
|
|
57 |
by (rtac lfp_lowerbound 1);
|
|
58 |
by (fast_tac (univ_cs addIs [Sexp_NumbI,Sexp_In0I,Sexp_In1I,Sexp_SconsI]
|
|
59 |
addSEs [PartE]) 1);
|
|
60 |
val TF_Sexp = result();
|
|
61 |
|
|
62 |
(* A <= Sexp ==> TF(A) <= Sexp *)
|
|
63 |
val TF_subset_Sexp = standard
|
|
64 |
(TF_mono RS (TF_Sexp RSN (2,subset_trans)));
|
|
65 |
|
|
66 |
|
|
67 |
(** Elimination -- structural induction on the set TF **)
|
|
68 |
|
|
69 |
val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def];
|
|
70 |
|
|
71 |
val major::prems = goalw Simult.thy TF_Rep_defs
|
|
72 |
"[| i: TF(A); \
|
|
73 |
\ !!M N. [| M: A; N: Part(TF(A),In1); R(N) |] ==> R(TCONS(M,N)); \
|
|
74 |
\ R(FNIL); \
|
|
75 |
\ !!M N. [| M: Part(TF(A),In0); N: Part(TF(A),In1); R(M); R(N) \
|
|
76 |
\ |] ==> R(FCONS(M,N)) \
|
|
77 |
\ |] ==> R(i)";
|
|
78 |
by (rtac (major RS (TF_def RS def_induct)) 1);
|
|
79 |
by (rtac TF_fun_mono 1);
|
|
80 |
by (fast_tac (set_cs addIs (prems@[PartI])
|
|
81 |
addEs [usumE, uprodE, PartE]) 1);
|
|
82 |
val TF_induct = result();
|
|
83 |
|
|
84 |
(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
|
|
85 |
val prems = goalw Simult.thy [Part_def]
|
|
86 |
"! M: TF(A). (M: Part(TF(A),In0) --> P(M)) & (M: Part(TF(A),In1) --> Q(M)) \
|
|
87 |
\ ==> (! M: Part(TF(A),In0). P(M)) & (! M: Part(TF(A),In1). Q(M))";
|
|
88 |
by (cfast_tac prems 1);
|
|
89 |
val TF_induct_lemma = result();
|
|
90 |
|
|
91 |
val uplus_cs = set_cs addSIs [PartI]
|
|
92 |
addSDs [In0_inject, In1_inject]
|
|
93 |
addSEs [In0_neq_In1, In1_neq_In0, PartE];
|
|
94 |
|
|
95 |
(*Could prove ~ TCONS(M,N) : Part(TF(A),In1) etc. *)
|
|
96 |
|
|
97 |
(*Induction on TF with separate predicates P, Q*)
|
|
98 |
val prems = goalw Simult.thy TF_Rep_defs
|
|
99 |
"[| !!M N. [| M: A; N: Part(TF(A),In1); Q(N) |] ==> P(TCONS(M,N)); \
|
|
100 |
\ Q(FNIL); \
|
|
101 |
\ !!M N. [| M: Part(TF(A),In0); N: Part(TF(A),In1); P(M); Q(N) \
|
|
102 |
\ |] ==> Q(FCONS(M,N)) \
|
|
103 |
\ |] ==> (! M: Part(TF(A),In0). P(M)) & (! N: Part(TF(A),In1). Q(N))";
|
|
104 |
by (rtac (ballI RS TF_induct_lemma) 1);
|
|
105 |
by (etac TF_induct 1);
|
|
106 |
by (rewrite_goals_tac TF_Rep_defs);
|
|
107 |
by (ALLGOALS (fast_tac (uplus_cs addIs prems)));
|
|
108 |
(*29 secs??*)
|
|
109 |
val Tree_Forest_induct = result();
|
|
110 |
|
|
111 |
(*Induction for the abstract types 'a tree, 'a forest*)
|
|
112 |
val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
|
|
113 |
"[| !!x ts. Q(ts) ==> P(Tcons(x,ts)); \
|
|
114 |
\ Q(Fnil); \
|
|
115 |
\ !!t ts. [| P(t); Q(ts) |] ==> Q(Fcons(t,ts)) \
|
|
116 |
\ |] ==> (! t. P(t)) & (! ts. Q(ts))";
|
|
117 |
by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
|
|
118 |
("Q1","%z.Q(Abs_Forest(z))")]
|
|
119 |
(Tree_Forest_induct RS conjE) 1);
|
|
120 |
(*Instantiates ?A1 to range(Leaf). *)
|
|
121 |
by (fast_tac (set_cs addSEs [Rep_Tree_inverse RS subst,
|
|
122 |
Rep_Forest_inverse RS subst]
|
|
123 |
addSIs [Rep_Tree,Rep_Forest]) 4);
|
|
124 |
(*Cannot use simplifier: the rewrites work in the wrong direction!*)
|
|
125 |
by (ALLGOALS (fast_tac (set_cs addSEs [Abs_Tree_inverse RS subst,
|
|
126 |
Abs_Forest_inverse RS subst]
|
|
127 |
addSIs prems)));
|
|
128 |
val tree_forest_induct = result();
|
|
129 |
|
|
130 |
|
|
131 |
|
|
132 |
(*** Isomorphisms ***)
|
|
133 |
|
|
134 |
goal Simult.thy "inj(Rep_Tree)";
|
|
135 |
by (rtac inj_inverseI 1);
|
|
136 |
by (rtac Rep_Tree_inverse 1);
|
|
137 |
val inj_Rep_Tree = result();
|
|
138 |
|
|
139 |
goal Simult.thy "inj_onto(Abs_Tree,Part(TF(range(Leaf)),In0))";
|
|
140 |
by (rtac inj_onto_inverseI 1);
|
|
141 |
by (etac Abs_Tree_inverse 1);
|
|
142 |
val inj_onto_Abs_Tree = result();
|
|
143 |
|
|
144 |
goal Simult.thy "inj(Rep_Forest)";
|
|
145 |
by (rtac inj_inverseI 1);
|
|
146 |
by (rtac Rep_Forest_inverse 1);
|
|
147 |
val inj_Rep_Forest = result();
|
|
148 |
|
|
149 |
goal Simult.thy "inj_onto(Abs_Forest,Part(TF(range(Leaf)),In1))";
|
|
150 |
by (rtac inj_onto_inverseI 1);
|
|
151 |
by (etac Abs_Forest_inverse 1);
|
|
152 |
val inj_onto_Abs_Forest = result();
|
|
153 |
|
|
154 |
(** Introduction rules for constructors **)
|
|
155 |
|
|
156 |
(* c : A <*> Part(TF(A),In1)
|
|
157 |
<+> {Numb(0)} <+> Part(TF(A),In0) <*> Part(TF(A),In1) ==> c : TF(A) *)
|
|
158 |
val TF_I = TF_unfold RS equalityD2 RS subsetD;
|
|
159 |
|
|
160 |
(*For reasoning about the representation*)
|
|
161 |
val TF_Rep_cs = uplus_cs addIs [TF_I, uprodI, usum_In0I, usum_In1I]
|
|
162 |
addSEs [Scons_inject];
|
|
163 |
|
|
164 |
val prems = goalw Simult.thy TF_Rep_defs
|
|
165 |
"[| a: A; M: Part(TF(A),In1) |] ==> TCONS(a,M) : Part(TF(A),In0)";
|
|
166 |
by (fast_tac (TF_Rep_cs addIs prems) 1);
|
|
167 |
val TCONS_I = result();
|
|
168 |
|
|
169 |
(* FNIL is a TF(A) -- this also justifies the type definition*)
|
|
170 |
goalw Simult.thy TF_Rep_defs "FNIL: Part(TF(A),In1)";
|
|
171 |
by (fast_tac TF_Rep_cs 1);
|
|
172 |
val FNIL_I = result();
|
|
173 |
|
|
174 |
val prems = goalw Simult.thy TF_Rep_defs
|
|
175 |
"[| M: Part(TF(A),In0); N: Part(TF(A),In1) |] ==> \
|
|
176 |
\ FCONS(M,N) : Part(TF(A),In1)";
|
|
177 |
by (fast_tac (TF_Rep_cs addIs prems) 1);
|
|
178 |
val FCONS_I = result();
|
|
179 |
|
|
180 |
(** Injectiveness of TCONS and FCONS **)
|
|
181 |
|
|
182 |
goalw Simult.thy TF_Rep_defs "(TCONS(K,M)=TCONS(L,N)) = (K=L & M=N)";
|
|
183 |
by (fast_tac TF_Rep_cs 1);
|
|
184 |
val TCONS_TCONS_eq = result();
|
|
185 |
val TCONS_inject = standard (TCONS_TCONS_eq RS iffD1 RS conjE);
|
|
186 |
|
|
187 |
goalw Simult.thy TF_Rep_defs "(FCONS(K,M)=FCONS(L,N)) = (K=L & M=N)";
|
|
188 |
by (fast_tac TF_Rep_cs 1);
|
|
189 |
val FCONS_FCONS_eq = result();
|
|
190 |
val FCONS_inject = standard (FCONS_FCONS_eq RS iffD1 RS conjE);
|
|
191 |
|
|
192 |
(** Distinctness of TCONS, FNIL and FCONS **)
|
|
193 |
|
6
|
194 |
goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FNIL";
|
0
|
195 |
by (fast_tac TF_Rep_cs 1);
|
|
196 |
val TCONS_not_FNIL = result();
|
|
197 |
val FNIL_not_TCONS = standard (TCONS_not_FNIL RS not_sym);
|
|
198 |
|
|
199 |
val TCONS_neq_FNIL = standard (TCONS_not_FNIL RS notE);
|
|
200 |
val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
|
|
201 |
|
6
|
202 |
goalw Simult.thy TF_Rep_defs "FCONS(M,N) ~= FNIL";
|
0
|
203 |
by (fast_tac TF_Rep_cs 1);
|
|
204 |
val FCONS_not_FNIL = result();
|
|
205 |
val FNIL_not_FCONS = standard (FCONS_not_FNIL RS not_sym);
|
|
206 |
|
|
207 |
val FCONS_neq_FNIL = standard (FCONS_not_FNIL RS notE);
|
|
208 |
val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
|
|
209 |
|
6
|
210 |
goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FCONS(K,L)";
|
0
|
211 |
by (fast_tac TF_Rep_cs 1);
|
|
212 |
val TCONS_not_FCONS = result();
|
|
213 |
val FCONS_not_TCONS = standard (TCONS_not_FCONS RS not_sym);
|
|
214 |
|
|
215 |
val TCONS_neq_FCONS = standard (TCONS_not_FCONS RS notE);
|
|
216 |
val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
|
|
217 |
|
|
218 |
(*???? Too many derived rules ????
|
|
219 |
Automatically generate symmetric forms? Always expand TF_Rep_defs? *)
|
|
220 |
|
|
221 |
(** Injectiveness of Tcons and Fcons **)
|
|
222 |
|
|
223 |
(*For reasoning about abstract constructors*)
|
|
224 |
val TF_cs = set_cs addSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I]
|
|
225 |
addSEs [TCONS_inject, FCONS_inject,
|
|
226 |
TCONS_neq_FNIL, FNIL_neq_TCONS,
|
|
227 |
FCONS_neq_FNIL, FNIL_neq_FCONS,
|
|
228 |
TCONS_neq_FCONS, FCONS_neq_TCONS]
|
|
229 |
addSDs [inj_onto_Abs_Tree RS inj_ontoD,
|
|
230 |
inj_onto_Abs_Forest RS inj_ontoD,
|
|
231 |
inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
|
|
232 |
Leaf_inject];
|
|
233 |
|
|
234 |
goalw Simult.thy [Tcons_def] "(Tcons(x,xs)=Tcons(y,ys)) = (x=y & xs=ys)";
|
|
235 |
by (fast_tac TF_cs 1);
|
|
236 |
val Tcons_Tcons_eq = result();
|
|
237 |
val Tcons_inject = standard (Tcons_Tcons_eq RS iffD1 RS conjE);
|
|
238 |
|
6
|
239 |
goalw Simult.thy [Fcons_def,Fnil_def] "Fcons(x,xs) ~= Fnil";
|
0
|
240 |
by (fast_tac TF_cs 1);
|
|
241 |
val Fcons_not_Fnil = result();
|
|
242 |
|
|
243 |
val Fcons_neq_Fnil = standard (Fcons_not_Fnil RS notE);;
|
|
244 |
val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
|
|
245 |
|
|
246 |
|
|
247 |
(** Injectiveness of Fcons **)
|
|
248 |
|
|
249 |
goalw Simult.thy [Fcons_def] "(Fcons(x,xs)=Fcons(y,ys)) = (x=y & xs=ys)";
|
|
250 |
by (fast_tac TF_cs 1);
|
|
251 |
val Fcons_Fcons_eq = result();
|
|
252 |
val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
|
|
253 |
|
|
254 |
|
|
255 |
(*** TF_rec -- by wf recursion on pred_Sexp ***)
|
|
256 |
|
|
257 |
val TF_rec_unfold =
|
|
258 |
wf_pred_Sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
|
|
259 |
|
|
260 |
(** conversion rules for TF_rec **)
|
|
261 |
|
|
262 |
val prems = goalw Simult.thy [TCONS_def]
|
|
263 |
"[| M: Sexp; N: Sexp |] ==> \
|
|
264 |
\ TF_rec(TCONS(M,N),b,c,d) = b(M, N, TF_rec(N,b,c,d))";
|
|
265 |
by (rtac (TF_rec_unfold RS trans) 1);
|
|
266 |
by (rtac (Case_In0 RS trans) 1);
|
|
267 |
by (rtac (Split RS trans) 1);
|
|
268 |
by (rewtac In0_def);
|
|
269 |
by (simp_tac (pred_Sexp_ss addsimps prems) 1);
|
|
270 |
val TF_rec_TCONS = result();
|
|
271 |
|
|
272 |
goalw Simult.thy [FNIL_def] "TF_rec(FNIL,b,c,d) = c";
|
|
273 |
by (rtac (TF_rec_unfold RS trans) 1);
|
|
274 |
by (rtac (Case_In1 RS trans) 1);
|
|
275 |
by (rtac List_case_NIL 1);
|
|
276 |
val TF_rec_FNIL = result();
|
|
277 |
|
|
278 |
val prems = goalw Simult.thy [FCONS_def]
|
|
279 |
"[| M: Sexp; N: Sexp |] ==> \
|
|
280 |
\ TF_rec(FCONS(M,N),b,c,d) = d(M, N, TF_rec(M,b,c,d), TF_rec(N,b,c,d))";
|
|
281 |
by (rtac (TF_rec_unfold RS trans) 1);
|
|
282 |
by (rtac (Case_In1 RS trans) 1);
|
|
283 |
by (rtac (List_case_CONS RS trans) 1);
|
|
284 |
by (rewrite_goals_tac [CONS_def,In1_def]);
|
|
285 |
by (simp_tac (pred_Sexp_ss addsimps prems) 1);
|
|
286 |
val TF_rec_FCONS = result();
|
|
287 |
|
|
288 |
|
|
289 |
(*** tree_rec, forest_rec -- by TF_rec ***)
|
|
290 |
|
|
291 |
val Rep_Tree_in_Sexp =
|
|
292 |
Rep_Tree RS (range_Leaf_subset_Sexp RS TF_subset_Sexp RS
|
|
293 |
Part_subset RS subsetD);
|
|
294 |
val Rep_Forest_in_Sexp =
|
|
295 |
Rep_Forest RS (range_Leaf_subset_Sexp RS TF_subset_Sexp RS
|
|
296 |
Part_subset RS subsetD);
|
|
297 |
|
|
298 |
val tf_rec_simps = [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
|
|
299 |
TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
|
|
300 |
Rep_Tree_inverse, Rep_Forest_inverse,
|
|
301 |
Abs_Tree_inverse, Abs_Forest_inverse,
|
|
302 |
inj_Leaf, Inv_f_f, Sexp_LeafI, range_eqI,
|
|
303 |
Rep_Tree_in_Sexp, Rep_Forest_in_Sexp];
|
|
304 |
val tf_rec_ss = HOL_ss addsimps tf_rec_simps;
|
|
305 |
|
|
306 |
goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
|
|
307 |
"tree_rec(Tcons(a,tf),b,c,d) = b(a,tf,forest_rec(tf,b,c,d))";
|
|
308 |
by (simp_tac tf_rec_ss 1);
|
|
309 |
val tree_rec_Tcons = result();
|
|
310 |
|
|
311 |
goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec(Fnil,b,c,d) = c";
|
|
312 |
by (simp_tac tf_rec_ss 1);
|
|
313 |
val forest_rec_Fnil = result();
|
|
314 |
|
|
315 |
goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
|
|
316 |
"forest_rec(Fcons(t,tf),b,c,d) = \
|
|
317 |
\ d(t,tf,tree_rec(t,b,c,d), forest_rec(tf,b,c,d))";
|
|
318 |
by (simp_tac tf_rec_ss 1);
|
|
319 |
val forest_rec_Cons = result();
|