Empty commit
[Model of HOL/.git] / Model / syntax.ml
1 (* ========================================================================= *)
2 (* Syntactic definitions for "core HOL", including provability.              *)
3 (* ========================================================================= *)
4
5 (* ------------------------------------------------------------------------- *)
6 (* HOL types. Just do the primitive ones for now.                            *)
7 (* ------------------------------------------------------------------------- *)
8
9 let type_INDUCT,type_RECURSION = define_type
10   "type = Tyvar string
11             | Bool
12             | Ind
13             | Fun type type";;
14
15 let type_DISTINCT = distinctness "type";;
16
17 let type_INJ = injectivity "type";;
18
19 let domain = define
20   `domain (Fun s t) = s`;;
21
22 let codomain = define
23   `codomain (Fun s t) = t`;;
24
25 (* ------------------------------------------------------------------------- *)
26 (* HOL terms. To avoid messing round with specification of the language,     *)
27 (* we just put "=" and "@" in as the only constants. For now...              *)
28 (* ------------------------------------------------------------------------- *)
29
30 let term_INDUCT,term_RECURSION = define_type
31  "term = Var string type
32        | Equal type | Select type
33        | Comb term term
34        | Abs string type term";;
35
36 let term_DISTINCT = distinctness "term";;
37
38 let term_INJ = injectivity "term";;
39
40 (* ------------------------------------------------------------------------- *)
41 (* Typing judgements.                                                        *)
42 (* ------------------------------------------------------------------------- *)
43
44 parse_as_infix("has_type",(12,"right"));;
45
46 let has_type_RULES,has_type_INDUCT,has_type_CASES = new_inductive_definition
47   `(!n ty. (Var n ty) has_type ty) /\
48    (!ty. (Equal ty) has_type (Fun ty (Fun ty Bool))) /\
49    (!ty. (Select ty) has_type (Fun (Fun ty Bool) ty)) /\
50    (!s t dty rty. s has_type (Fun dty rty) /\ t has_type dty
51                   ==> (Comb s t) has_type rty) /\
52    (!n dty t rty. t has_type rty ==> (Abs n dty t) has_type (Fun dty rty))`;;
53
54 let welltyped = new_definition
55   `welltyped tm <=> ?ty. tm has_type ty`;;
56
57 let typeof = define
58  `(typeof (Var n ty) = ty) /\
59   (typeof (Equal ty) = Fun ty (Fun ty Bool)) /\
60   (typeof (Select ty) = Fun (Fun ty Bool) ty) /\
61   (typeof (Comb s t) = codomain (typeof s)) /\
62   (typeof (Abs n ty t) = Fun ty (typeof t))`;;
63
64 let WELLTYPED_LEMMA = prove
65  (`!tm ty. tm has_type ty ==> (typeof tm = ty)`,
66   MATCH_MP_TAC has_type_INDUCT THEN
67   SIMP_TAC[typeof; has_type_RULES; codomain]);;
68
69 let WELLTYPED = prove
70  (`!tm. welltyped tm <=> tm has_type (typeof tm)`,
71   REWRITE_TAC[welltyped] THEN MESON_TAC[WELLTYPED_LEMMA]);;
72
73 let WELLTYPED_CLAUSES = prove
74  (`(!n ty. welltyped(Var n ty)) /\
75    (!ty. welltyped(Equal ty)) /\
76    (!ty. welltyped(Select ty)) /\
77    (!s t. welltyped (Comb s t) <=>
78             welltyped s /\ welltyped t /\
79             ?rty. typeof s = Fun (typeof t) rty) /\
80    (!n ty t. welltyped (Abs n ty t) = welltyped t)`,
81   REPEAT STRIP_TAC THEN REWRITE_TAC[welltyped] THEN
82   (GEN_REWRITE_TAC BINDER_CONV [has_type_CASES] ORELSE
83    GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [has_type_CASES]) THEN
84   REWRITE_TAC[term_INJ; term_DISTINCT] THEN
85   MESON_TAC[WELLTYPED; WELLTYPED_LEMMA]);;
86
87 (* ------------------------------------------------------------------------- *)
88 (* Since equations are important, a bit of derived syntax.                   *)
89 (* ------------------------------------------------------------------------- *)
90
91 parse_as_infix("===",(18,"right"));;
92
93 let equation = new_definition
94  `(s === t) = Comb (Comb (Equal(typeof s)) s) t`;;
95
96 let EQUATION_HAS_TYPE_BOOL = prove
97  (`!s t. (s === t) has_type Bool
98          <=> welltyped s /\ welltyped t /\ (typeof s = typeof t)`,
99   REWRITE_TAC[equation] THEN
100   ONCE_REWRITE_TAC[has_type_CASES] THEN
101   REWRITE_TAC[term_DISTINCT; term_INJ] THEN
102   REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
103   REWRITE_TAC[UNWIND_THM1] THEN REPEAT GEN_TAC THEN
104   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o LAND_CONV) [has_type_CASES] THEN
105   REWRITE_TAC[term_DISTINCT; term_INJ] THEN
106   REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
107   REWRITE_TAC[UNWIND_THM1] THEN
108   GEN_REWRITE_TAC (LAND_CONV o funpow 2(BINDER_CONV o LAND_CONV))
109     [has_type_CASES] THEN
110   REWRITE_TAC[term_DISTINCT; term_INJ; type_INJ] THEN
111   MESON_TAC[WELLTYPED; WELLTYPED_LEMMA]);;
112
113 (* ------------------------------------------------------------------------- *)
114 (* Alpha-conversion.                                                         *)
115 (* ------------------------------------------------------------------------- *)
116
117 let ALPHAVARS = define
118   `(ALPHAVARS [] tmp <=> (FST tmp = SND tmp)) /\
119    (ALPHAVARS (CONS tp oenv) tmp <=>
120         (tmp = tp) \/
121         ~(FST tp = FST tmp) /\ ~(SND tp = SND tmp) /\ ALPHAVARS oenv tmp)`;;
122
123 let RACONV_RULES,RACONV_INDUCT,RACONV_CASES = new_inductive_definition
124  `(!env x1 ty1 x2 ty2.
125        ALPHAVARS env (Var x1 ty1,Var x2 ty2)
126        ==> RACONV env (Var x1 ty1,Var x2 ty2)) /\
127   (!env ty. RACONV env (Equal ty,Equal ty)) /\
128   (!env ty. RACONV env (Select ty,Select ty)) /\
129   (!env s1 t1 s2 t2.
130        RACONV env (s1,s2) /\ RACONV env (t1,t2)
131        ==> RACONV env (Comb s1 t1,Comb s2 t2)) /\
132   (!env x1 ty1 t1 x2 ty2 t2.
133        (ty1 = ty2) /\ RACONV (CONS ((Var x1 ty1),(Var x2 ty2)) env) (t1,t2)
134        ==> RACONV env (Abs x1 ty1 t1,Abs x2 ty2 t2))`;;
135
136 let RACONV = prove
137  (`(RACONV env (Var x1 ty1,Var x2 ty2) <=>
138         ALPHAVARS env (Var x1 ty1,Var x2 ty2)) /\
139    (RACONV env (Var x1 ty1,Equal ty2) <=> F) /\
140    (RACONV env (Var x1 ty1,Select ty2) <=> F) /\
141    (RACONV env (Var x1 ty1,Comb l2 r2) <=> F) /\
142    (RACONV env (Var x1 ty1,Abs x2 ty2 t2) <=> F) /\
143    (RACONV env (Equal ty1,Var x2 ty2) <=> F) /\
144    (RACONV env (Equal ty1,Equal ty2) <=> (ty1 = ty2)) /\
145    (RACONV env (Equal ty1,Select ty2) <=> F) /\
146    (RACONV env (Equal ty1,Comb l2 r2) <=> F) /\
147    (RACONV env (Equal ty1,Abs x2 ty2 t2) <=> F) /\
148    (RACONV env (Select ty1,Var x2 ty2) <=> F) /\
149    (RACONV env (Select ty1,Equal ty2) <=> F) /\
150    (RACONV env (Select ty1,Select ty2) <=> (ty1 = ty2)) /\
151    (RACONV env (Select ty1,Comb l2 r2) <=> F) /\
152    (RACONV env (Select ty1,Abs x2 ty2 t2) <=> F) /\
153    (RACONV env (Comb l1 r1,Var x2 ty2) <=> F) /\
154    (RACONV env (Comb l1 r1,Equal ty2) <=> F) /\
155    (RACONV env (Comb l1 r1,Select ty2) <=> F) /\
156    (RACONV env (Comb l1 r1,Comb l2 r2) <=>
157         RACONV env (l1,l2) /\ RACONV env (r1,r2)) /\
158    (RACONV env (Comb l1 r1,Abs x2 ty2 t2) <=> F) /\
159    (RACONV env (Abs x1 ty1 t1,Var x2 ty2) <=> F) /\
160    (RACONV env (Abs x1 ty1 t1,Equal ty2) <=> F) /\
161    (RACONV env (Abs x1 ty1 t1,Select ty2) <=> F) /\
162    (RACONV env (Abs x1 ty1 t1,Comb l2 r2) <=> F) /\
163    (RACONV env (Abs x1 ty1 t1,Abs x2 ty2 t2) <=>
164         (ty1 = ty2) /\ RACONV (CONS (Var x1 ty1,Var x2 ty2) env) (t1,t2))`,
165   REPEAT CONJ_TAC THEN
166   GEN_REWRITE_TAC LAND_CONV [RACONV_CASES] THEN
167   REWRITE_TAC[term_INJ; term_DISTINCT; PAIR_EQ] THEN MESON_TAC[]);;
168
169 let ACONV = new_definition
170  `ACONV t1 t2 <=> RACONV [] (t1,t2)`;;
171
172 (* ------------------------------------------------------------------------- *)
173 (* Reflexivity.                                                              *)
174 (* ------------------------------------------------------------------------- *)
175
176 let ALPHAVARS_REFL = prove
177  (`!env t. ALL (\(s,t). s = t) env ==> ALPHAVARS env (t,t)`,
178   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[ALL; ALPHAVARS] THEN
179   REWRITE_TAC[FORALL_PAIR_THM] THEN
180   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN MESON_TAC[PAIR_EQ]);;
181
182 let RACONV_REFL = prove
183  (`!t env. ALL (\(s,t). s = t) env ==> RACONV env (t,t)`,
184   MATCH_MP_TAC term_INDUCT THEN
185   REWRITE_TAC[RACONV] THEN REPEAT STRIP_TAC THENL
186    [ASM_SIMP_TAC[ALPHAVARS_REFL];
187     ASM_MESON_TAC[];
188     ASM_MESON_TAC[];
189     FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[ALL] THEN
190     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN ASM_REWRITE_TAC[]]);;
191
192 let ACONV_REFL = prove
193  (`!t. ACONV t t`,
194   REWRITE_TAC[ACONV] THEN SIMP_TAC[RACONV_REFL; ALL]);;
195
196 (* ------------------------------------------------------------------------- *)
197 (* Alpha-convertible terms have the same type (if welltyped).                *)
198 (* ------------------------------------------------------------------------- *)
199
200 let ALPHAVARS_TYPE = prove
201  (`!env s t. ALPHAVARS env (s,t) /\
202              ALL (\(x,y). welltyped x /\ welltyped y /\
203                           (typeof x = typeof y)) env /\
204              welltyped s /\ welltyped t
205            ==> (typeof s = typeof t)`,
206   MATCH_MP_TAC list_INDUCT THEN
207   REWRITE_TAC[FORALL_PAIR_THM; ALPHAVARS; ALL; PAIR_EQ] THEN
208   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
209   CONJ_TAC THENL [SIMP_TAC[]; ALL_TAC] THEN REPEAT STRIP_TAC THEN
210   ASM_MESON_TAC[]);;
211
212 let RACONV_TYPE = prove
213  (`!env p. RACONV env p
214            ==> ALL (\(x,y). welltyped x /\ welltyped y /\
215                         (typeof x = typeof y)) env /\
216                welltyped (FST p) /\ welltyped (SND p)
217                ==> (typeof (FST p) = typeof (SND p))`,
218   MATCH_MP_TAC RACONV_INDUCT THEN
219   REWRITE_TAC[FORALL_PAIR_THM; typeof] THEN REPEAT STRIP_TAC THENL
220    [ASM_MESON_TAC[typeof; ALPHAVARS_TYPE];
221     AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
222     ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[WELLTYPED_CLAUSES];
223     ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
224     ASM_REWRITE_TAC[ALL] THEN
225     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
226     REWRITE_TAC[typeof] THEN ASM_MESON_TAC[WELLTYPED_CLAUSES]]);;
227
228 let ACONV_TYPE = prove
229  (`!s t. ACONV s t ==> welltyped s /\ welltyped t ==> (typeof s = typeof t)`,
230   REPEAT GEN_TAC THEN
231   MP_TAC(SPECL [`[]:(term#term)list`; `(s:term,t:term)`] RACONV_TYPE) THEN
232   REWRITE_TAC[ACONV; ALL] THEN MESON_TAC[]);;
233
234 (* ------------------------------------------------------------------------- *)
235 (* HOL version of "term_union".                                              *)
236 (* ------------------------------------------------------------------------- *)
237
238 let TERM_UNION = define
239  `(TERM_UNION [] l2 = l2) /\
240   (TERM_UNION (CONS h t) l2 =
241         let subun = TERM_UNION t l2 in
242         if EX (ACONV h) subun then subun else CONS h subun)`;;
243
244 let TERM_UNION_NONEW = prove
245  (`!l1 l2 x. MEM x (TERM_UNION l1 l2) ==> MEM x l1 \/ MEM x l2`,
246   LIST_INDUCT_TAC THEN REWRITE_TAC[TERM_UNION; MEM] THEN
247   LET_TAC THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
248   REWRITE_TAC[MEM] THEN ASM_MESON_TAC[ACONV_REFL]);;
249
250 let TERM_UNION_THM = prove
251  (`!l1 l2 x. MEM x l1 \/ MEM x l2
252              ==> ?y. MEM y (TERM_UNION l1 l2) /\ ACONV x y`,
253   LIST_INDUCT_TAC THEN REWRITE_TAC[TERM_UNION; MEM; GSYM EX_MEM] THENL
254    [MESON_TAC[ACONV_REFL]; ALL_TAC] THEN
255   REPEAT GEN_TAC THEN LET_TAC THEN COND_CASES_TAC THEN STRIP_TAC THEN
256   ASM_REWRITE_TAC[MEM] THEN  ASM_MESON_TAC[ACONV_REFL]);;
257
258 (* ------------------------------------------------------------------------- *)
259 (* Handy lemma for using it in a sequent.                                    *)
260 (* ------------------------------------------------------------------------- *)
261
262 let ALL_BOOL_TERM_UNION = prove
263  (`ALL (\a. a has_type Bool) l1 /\ ALL (\a. a has_type Bool) l2
264    ==> ALL (\a. a has_type Bool) (TERM_UNION l1 l2)`,
265   REWRITE_TAC[GSYM ALL_MEM] THEN MESON_TAC[TERM_UNION_NONEW]);;
266
267 (* ------------------------------------------------------------------------- *)
268 (* Whether a variable/constant is free in a term.                            *)
269 (* ------------------------------------------------------------------------- *)
270
271 let VFREE_IN = define
272   `(VFREE_IN v (Var x ty) <=> (Var x ty = v)) /\
273    (VFREE_IN v (Equal ty) <=> (Equal ty = v)) /\
274    (VFREE_IN v (Select ty) <=> (Select ty = v)) /\
275    (VFREE_IN v (Comb s t) <=> VFREE_IN v s \/ VFREE_IN v t) /\
276    (VFREE_IN v (Abs x ty t) <=> ~(Var x ty = v) /\ VFREE_IN v t)`;;
277
278 let VFREE_IN_RACONV = prove
279  (`!env p. RACONV env p
280            ==> !x ty. VFREE_IN (Var x ty) (FST p) /\
281                       ~(?y. MEM (Var x ty,y) env) <=>
282                       VFREE_IN (Var x ty) (SND p) /\
283                       ~(?y. MEM (y,Var x ty) env)`,
284   MATCH_MP_TAC RACONV_INDUCT THEN REWRITE_TAC[VFREE_IN; term_DISTINCT] THEN
285   REWRITE_TAC[PAIR_EQ; term_INJ; MEM] THEN CONJ_TAC THENL
286    [ALL_TAC; MESON_TAC[]] THEN
287   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[ALPHAVARS] THEN
288   REWRITE_TAC[MEM; FORALL_PAIR_THM; term_INJ; PAIR_EQ] THEN
289   CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
290   REPEAT GEN_TAC THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
291   MESON_TAC[]);;
292
293 let VFREE_IN_ACONV = prove
294  (`!s t x t. ACONV s t ==> (VFREE_IN (Var x ty) s <=> VFREE_IN (Var x ty) t)`,
295   REPEAT GEN_TAC THEN REWRITE_TAC[ACONV] THEN
296   DISCH_THEN(MP_TAC o MATCH_MP VFREE_IN_RACONV) THEN
297   SIMP_TAC[MEM; FST; SND]);;
298
299 (* ------------------------------------------------------------------------- *)
300 (* Auxiliary association list function.                                      *)
301 (* ------------------------------------------------------------------------- *)
302
303 let REV_ASSOCD = define
304   `(REV_ASSOCD a [] d = d) /\
305    (REV_ASSOCD a (CONS (x,y) t) d =
306         if y = a then x else REV_ASSOCD a t d)`;;
307
308 (* ------------------------------------------------------------------------- *)
309 (* Substition of types in types.                                             *)
310 (* ------------------------------------------------------------------------- *)
311
312 let TYPE_SUBST = define
313  `(TYPE_SUBST i (Tyvar v) = REV_ASSOCD (Tyvar v) i (Tyvar v)) /\
314   (TYPE_SUBST i Bool = Bool) /\
315   (TYPE_SUBST i Ind = Ind) /\
316   (TYPE_SUBST i (Fun ty1 ty2) = Fun (TYPE_SUBST i ty1) (TYPE_SUBST i ty2))`;;
317
318 (* ------------------------------------------------------------------------- *)
319 (* Variant function. Deliberately underspecified at the moment. In a bid to  *)
320 (* expunge use of sets, just pick it distinct from what's free in a term.    *)
321 (* ------------------------------------------------------------------------- *)
322
323 let VFREE_IN_FINITE = prove
324  (`!t. FINITE {x | VFREE_IN x t}`,
325   MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VFREE_IN] THEN
326   REWRITE_TAC[SET_RULE `{x | a = x} = {a}`;
327               SET_RULE `{x | P x \/ Q x} = {x | P x} UNION {x | Q x}`;
328               SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN
329   SIMP_TAC[FINITE_INSERT; FINITE_RULES; FINITE_UNION; FINITE_INTER]);;
330
331 let VFREE_IN_FINITE_ALT = prove
332  (`!t ty. FINITE {x | VFREE_IN (Var x ty) t}`,
333   REPEAT GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
334   EXISTS_TAC `IMAGE (\(Var x ty). x) {x | VFREE_IN x t}` THEN
335   SIMP_TAC[VFREE_IN_FINITE; FINITE_IMAGE] THEN
336   REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_THM] THEN
337   X_GEN_TAC `x:string` THEN DISCH_TAC THEN
338   EXISTS_TAC `Var x ty` THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
339   ASM_REWRITE_TAC[]);;
340
341 let VARIANT_EXISTS = prove
342  (`!t x:string ty. ?x'. ~(VFREE_IN (Var x' ty) t)`,
343   REPEAT STRIP_TAC THEN
344   MP_TAC(SPECL [`t:term`; `ty:type`] VFREE_IN_FINITE_ALT) THEN
345   DISCH_THEN(MP_TAC o CONJ string_INFINITE) THEN
346   DISCH_THEN(MP_TAC o MATCH_MP INFINITE_DIFF_FINITE) THEN
347   DISCH_THEN(MP_TAC o MATCH_MP INFINITE_NONEMPTY) THEN
348   REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_DIFF; IN_ELIM_THM; IN_UNIV]);;
349
350 let VARIANT = new_specification ["VARIANT"]
351  (PURE_REWRITE_RULE[SKOLEM_THM] VARIANT_EXISTS);;
352
353 (* ------------------------------------------------------------------------- *)
354 (* Term substitution.                                                        *)
355 (* ------------------------------------------------------------------------- *)
356
357 let VSUBST = define
358   `(VSUBST ilist (Var x ty) = REV_ASSOCD (Var x ty) ilist (Var x ty)) /\
359    (VSUBST ilist (Equal ty) = Equal ty) /\
360    (VSUBST ilist (Select ty) = Select ty) /\
361    (VSUBST ilist (Comb s t) = Comb (VSUBST ilist s) (VSUBST ilist t)) /\
362    (VSUBST ilist (Abs x ty t) =
363         let ilist' = FILTER (\(s',s). ~(s = Var x ty)) ilist in
364         let t' = VSUBST ilist' t in
365         if EX (\(s',s). VFREE_IN (Var x ty) s' /\ VFREE_IN s t) ilist'
366         then let z = VARIANT t' x ty in
367              let ilist'' = CONS (Var z ty,Var x ty) ilist' in
368              Abs z ty (VSUBST ilist'' t)
369         else Abs x ty t')`;;
370
371 (* ------------------------------------------------------------------------- *)
372 (* Preservation of type.                                                     *)
373 (* ------------------------------------------------------------------------- *)
374
375 let VSUBST_HAS_TYPE = prove
376  (`!tm ty ilist.
377         tm has_type ty /\
378         (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
379         ==> (VSUBST ilist tm) has_type ty`,
380   MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VSUBST] THEN
381   REPEAT CONJ_TAC THENL
382    [MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `tty:type`] THEN
383     MATCH_MP_TAC list_INDUCT THEN
384     SIMP_TAC[REV_ASSOCD; MEM; FORALL_PAIR_THM] THEN
385     REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
386     SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
387     REWRITE_TAC[ LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
388     ASM_CASES_TAC `(Var x ty) has_type tty` THEN ASM_REWRITE_TAC[] THEN
389     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_type_CASES]) THEN
390     REWRITE_TAC[term_DISTINCT; term_INJ; LEFT_EXISTS_AND_THM] THEN
391     REWRITE_TAC[GSYM EXISTS_REFL] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
392     MAP_EVERY X_GEN_TAC [`s:term`; `u:term`; `ilist:(term#term)list`] THEN
393     DISCH_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
394     FIRST_X_ASSUM(X_CHOOSE_THEN `y:string` MP_TAC) THEN
395     DISCH_THEN(X_CHOOSE_THEN `aty:type` MP_TAC) THEN
396     DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
397     ASM_MESON_TAC[term_INJ];
398     SIMP_TAC[];
399     SIMP_TAC[];
400     MAP_EVERY X_GEN_TAC [`s:term`; `t:term`] THEN REPEAT STRIP_TAC THEN
401     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_type_CASES]) THEN
402     REWRITE_TAC[term_DISTINCT; term_INJ; GSYM CONJ_ASSOC] THEN
403     REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
404     DISCH_THEN(X_CHOOSE_THEN `dty:type` STRIP_ASSUME_TAC) THEN
405     MATCH_MP_TAC(el 3 (CONJUNCTS has_type_RULES)) THEN
406     EXISTS_TAC `dty:type` THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
407     ASM_REWRITE_TAC[];
408     ALL_TAC] THEN
409   MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN DISCH_TAC THEN
410   MAP_EVERY X_GEN_TAC [`fty:type`; `ilist:(term#term)list`] THEN STRIP_TAC THEN
411   LET_TAC THEN LET_TAC THEN
412   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_type_CASES]) THEN
413   REWRITE_TAC[term_DISTINCT; term_INJ; GSYM CONJ_ASSOC] THEN
414   REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
415   DISCH_THEN(X_CHOOSE_THEN `rty:type` MP_TAC) THEN
416   DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC) THEN DISCH_TAC THEN
417   COND_CASES_TAC THEN REPEAT LET_TAC THEN
418   MATCH_MP_TAC(el 4 (CONJUNCTS has_type_RULES)) THEN
419   EXPAND_TAC "t'" THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THENL
420    [MAP_EVERY EXPAND_TAC ["ilist''"; "ilist'"]; EXPAND_TAC "ilist'"] THEN
421   REWRITE_TAC[MEM; MEM_FILTER] THEN
422   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
423   REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[has_type_RULES]);;
424
425 let VSUBST_WELLTYPED = prove
426  (`!tm ty ilist.
427         welltyped tm /\
428         (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
429         ==> welltyped (VSUBST ilist tm)`,
430   MESON_TAC[VSUBST_HAS_TYPE; welltyped]);;
431
432 (* ------------------------------------------------------------------------- *)
433 (* Right set of free variables.                                              *)
434 (* ------------------------------------------------------------------------- *)
435
436 let REV_ASSOCD_FILTER = prove
437  (`!l:(B#A)list a b d.
438         REV_ASSOCD a (FILTER (\(y,x). P x) l) b =
439             if P a then REV_ASSOCD a l b else b`,
440   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[REV_ASSOCD; FILTER; COND_ID] THEN
441   REWRITE_TAC[FORALL_PAIR_THM] THEN
442   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
443   MAP_EVERY X_GEN_TAC [`y:B`; `x:A`; `l:(B#A)list`] THEN
444   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REV_ASSOCD] THEN
445   ASM_CASES_TAC `(P:A->bool) x` THEN ASM_REWRITE_TAC[REV_ASSOCD] THEN
446   ASM_MESON_TAC[]);;
447
448 let VFREE_IN_VSUBST = prove
449  (`!tm u uty ilist.
450       VFREE_IN (Var u uty) (VSUBST ilist tm) <=>
451         ?y ty. VFREE_IN (Var y ty) tm /\
452                VFREE_IN (Var u uty) (REV_ASSOCD (Var y ty) ilist (Var y ty))`,
453   MATCH_MP_TAC term_INDUCT THEN
454   REWRITE_TAC[VFREE_IN; VSUBST; term_DISTINCT] THEN REPEAT CONJ_TAC THENL
455    [MESON_TAC[term_INJ];
456     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MESON_TAC[];
457     ALL_TAC] THEN
458   MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN DISCH_TAC THEN
459   REPEAT GEN_TAC THEN LET_TAC THEN LET_TAC THEN
460   COND_CASES_TAC THEN REPEAT LET_TAC THEN
461   ASM_REWRITE_TAC[VFREE_IN] THENL
462    [MAP_EVERY EXPAND_TAC ["ilist''"; "ilist'"];
463     EXPAND_TAC "t'" THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "ilist'"] THEN
464   SIMP_TAC[REV_ASSOCD; REV_ASSOCD_FILTER] THEN
465   ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN] THEN
466   REWRITE_TAC[TAUT `(if ~b then x:bool else y) <=> (if b then y else x)`] THEN
467   ONCE_REWRITE_TAC[TAUT `~a /\ b <=> ~(~a ==> ~b)`] THEN
468   SIMP_TAC[TAUT `(if b then F else c) <=> ~b /\ c`] THEN
469   MATCH_MP_TAC(TAUT
470    `(a ==> ~c) /\ (~a ==> (b <=> c)) ==> (~(~a ==> ~b) <=> c)`) THEN
471   (CONJ_TAC THENL [ALL_TAC; MESON_TAC[]]) THEN
472   GEN_REWRITE_TAC LAND_CONV [term_INJ] THEN
473   DISCH_THEN(CONJUNCTS_THEN(SUBST_ALL_TAC o SYM)) THEN
474   REWRITE_TAC[NOT_IMP] THENL
475    [MP_TAC(ISPECL [`VSUBST ilist' t`; `x:string`; `ty:type`] VARIANT) THEN
476     ASM_REWRITE_TAC[] THEN
477     EXPAND_TAC "ilist'" THEN ASM_REWRITE_TAC[REV_ASSOCD_FILTER] THEN
478     MESON_TAC[];
479     ALL_TAC] THEN
480   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EX]) THEN
481   EXPAND_TAC "ilist'" THEN
482   SPEC_TAC(`ilist:(term#term)list`,`l:(term#term)list`) THEN
483   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[ALL; REV_ASSOCD; VFREE_IN] THEN
484   REWRITE_TAC[REV_ASSOCD; FILTER; FORALL_PAIR_THM] THEN
485   ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[ALL] THEN
486   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN MESON_TAC[]);;
487
488 (* ------------------------------------------------------------------------- *)
489 (* Sum type to model exception-raising.                                      *)
490 (* ------------------------------------------------------------------------- *)
491
492 let result_INDUCT,result_RECURSION = define_type
493  "result = Clash term | Result term";;
494
495 let result_INJ = injectivity "result";;
496
497 let result_DISTINCT = distinctness "result";;
498
499 (* ------------------------------------------------------------------------- *)
500 (* Discriminators and extractors. (Nicer to pattern-match...)                *)
501 (* ------------------------------------------------------------------------- *)
502
503 let IS_RESULT = define
504  `(IS_RESULT(Clash t) = F) /\
505   (IS_RESULT(Result t) = T)`;;
506
507 let IS_CLASH = define
508  `(IS_CLASH(Clash t) = T) /\
509   (IS_CLASH(Result t) = F)`;;
510
511 let RESULT = define
512  `RESULT(Result t) = t`;;
513
514 let CLASH = define
515  `CLASH(Clash t) = t`;;
516
517 (* ------------------------------------------------------------------------- *)
518 (* We want induction/recursion on term size next.                            *)
519 (* ------------------------------------------------------------------------- *)
520
521 let rec sizeof = define
522  `(sizeof (Var x ty) = 1) /\
523   (sizeof (Equal ty) = 1) /\
524   (sizeof (Select ty) = 1) /\
525   (sizeof (Comb s t) = 1 + sizeof s + sizeof t) /\
526   (sizeof (Abs x ty t) = 2 + sizeof t)`;;
527
528 let SIZEOF_VSUBST = prove
529  (`!t ilist. (!s' s. MEM (s',s) ilist ==> ?x ty. s' = Var x ty)
530              ==> (sizeof (VSUBST ilist t) = sizeof t)`,
531   MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VSUBST; sizeof] THEN
532   CONJ_TAC THENL
533    [MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`] THEN
534     MATCH_MP_TAC list_INDUCT THEN
535     REWRITE_TAC[MEM; REV_ASSOCD; sizeof; FORALL_PAIR_THM] THEN
536     MAP_EVERY X_GEN_TAC [`s':term`; `s:term`; `l:(term#term)list`] THEN
537     REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC THEN
538     COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN ASM_MESON_TAC[sizeof];
539     ALL_TAC] THEN
540   CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
541   MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN
542   DISCH_TAC THEN X_GEN_TAC `ilist:(term#term)list` THEN DISCH_TAC THEN
543   LET_TAC THEN LET_TAC THEN COND_CASES_TAC THEN
544   REPEAT LET_TAC THEN REWRITE_TAC[sizeof; EQ_ADD_LCANCEL] THENL
545    [ALL_TAC; ASM_MESON_TAC[MEM_FILTER]] THEN
546   FIRST_X_ASSUM MATCH_MP_TAC THEN
547   EXPAND_TAC "ilist''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
548   ASM_MESON_TAC[MEM_FILTER]);;
549
550 (* ------------------------------------------------------------------------- *)
551 (* Prove existence of INST_CORE.                                             *)
552 (* ------------------------------------------------------------------------- *)
553
554 let INST_CORE_EXISTS = prove
555  (`?INST_CORE.
556   (!env tyin x ty.
557         INST_CORE env tyin (Var x ty) =
558           let tm = Var x ty
559           and tm' = Var x (TYPE_SUBST tyin ty) in
560          if REV_ASSOCD tm' env tm = tm then Result tm' else Clash tm') /\
561   (!env tyin ty.
562         INST_CORE env tyin (Equal ty) = Result(Equal(TYPE_SUBST tyin ty))) /\
563   (!env tyin ty.
564         INST_CORE env tyin (Select ty) = Result(Select(TYPE_SUBST tyin ty))) /\
565   (!env tyin s t.
566         INST_CORE env tyin (Comb s t) =
567             let sres = INST_CORE env tyin s in
568             if IS_CLASH sres then sres else
569             let tres = INST_CORE env tyin t in
570             if IS_CLASH tres then tres else
571             let s' = RESULT sres and t' = RESULT tres in
572             Result (Comb s' t')) /\
573   (!env tyin x ty t.
574         INST_CORE env tyin (Abs x ty t) =
575             let ty' = TYPE_SUBST tyin ty in
576             let env' = CONS (Var x ty,Var x ty') env in
577             let tres = INST_CORE env' tyin t in
578             if IS_RESULT tres then Result(Abs x ty' (RESULT tres)) else
579             let w = CLASH tres in
580             if ~(w = Var x ty') then tres else
581             let x' = VARIANT (RESULT(INST_CORE [] tyin t)) x ty' in
582             INST_CORE env tyin (Abs x' ty (VSUBST [Var x' ty,Var x ty] t)))`,
583   W(fun (asl,w) -> MATCH_MP_TAC(DISCH_ALL
584    (pure_prove_recursive_function_exists w))) THEN
585   EXISTS_TAC `MEASURE(\(env:(term#term)list,tyin:(type#type)list,t).
586                         sizeof t)` THEN
587   REWRITE_TAC[WF_MEASURE; MEASURE_LE; MEASURE] THEN
588   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
589   SIMP_TAC[MEM; PAIR_EQ; term_INJ; RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM;
590            GSYM EXISTS_REFL; SIZEOF_VSUBST; LE_REFL; sizeof] THEN
591   REPEAT STRIP_TAC THEN ARITH_TAC);;
592
593 (* ------------------------------------------------------------------------- *)
594 (* So define it.                                                             *)
595 (* ------------------------------------------------------------------------- *)
596
597 let INST_CORE = new_specification ["INST_CORE"] INST_CORE_EXISTS;;
598
599 (* ------------------------------------------------------------------------- *)
600 (* And the overall function.                                                 *)
601 (* ------------------------------------------------------------------------- *)
602
603 let INST_DEF = new_definition
604  `INST tyin tm = RESULT(INST_CORE [] tyin tm)`;;
605
606 (* ------------------------------------------------------------------------- *)
607 (* Various misc lemmas.                                                      *)
608 (* ------------------------------------------------------------------------- *)
609
610 let NOT_IS_RESULT = prove
611  (`!r. ~(IS_RESULT r) <=> IS_CLASH r`,
612   MATCH_MP_TAC result_INDUCT THEN REWRITE_TAC[IS_RESULT; IS_CLASH]);;
613
614 let letlemma = prove
615  (`(let x = t in P x) = P t`,
616   REWRITE_TAC[LET_DEF; LET_END_DEF]);;
617
618 (* ------------------------------------------------------------------------- *)
619 (* Put everything together into a deductive system.                          *)
620 (* ------------------------------------------------------------------------- *)
621
622 parse_as_infix("|-",(11,"right"));;
623
624 let prove_RULES,proves_INDUCT,proves_CASES = new_inductive_definition
625  `(!t. welltyped t ==> [] |- t === t) /\
626   (!asl1 asl2 l m1 m2 r.
627         asl1 |- l === m1 /\ asl2 |- m2 === r /\ ACONV m1 m2
628         ==> TERM_UNION asl1 asl2 |- l === r) /\
629   (!asl1 l1 r1 asl2 l2 r2.
630         asl1 |- l1 === r1 /\ asl2 |- l2 === r2 /\ welltyped(Comb l1 l2)
631         ==> TERM_UNION asl1 asl2 |- Comb l1 l2 === Comb r1 r2) /\
632   (!asl x ty l r.
633         ~(EX (VFREE_IN (Var x ty)) asl) /\ asl |- l === r
634         ==> asl |- (Abs x ty l) === (Abs x ty r)) /\
635   (!x ty t. welltyped t ==> [] |- Comb (Abs x ty t) (Var x ty) === t) /\
636   (!p. p has_type Bool ==> [p] |- p) /\
637   (!asl1 asl2 p q p'.
638         asl1 |- p === q /\ asl2 |- p' /\ ACONV p p'
639         ==> TERM_UNION asl1 asl2 |- q) /\
640   (!asl1 asl2 c1 c2.
641         asl1 |- c1 /\ asl2 |- c2
642         ==> TERM_UNION (FILTER((~) o ACONV c2) asl1)
643                        (FILTER((~) o ACONV c1) asl2)
644                |- c1 === c2) /\
645   (!tyin asl p. asl |- p ==> MAP (INST tyin) asl |- INST tyin p) /\
646   (!ilist asl p.
647       (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty) /\
648       asl |- p ==> MAP (VSUBST ilist) asl |- VSUBST ilist p)`;;