1 (* ========================================================================= *)
2 (* Syntactic definitions for "core HOL", including provability. *)
3 (* ========================================================================= *)
5 (* ------------------------------------------------------------------------- *)
6 (* HOL types. Just do the primitive ones for now. *)
7 (* ------------------------------------------------------------------------- *)
9 let type_INDUCT,type_RECURSION = define_type
15 let type_DISTINCT = distinctness "type";;
17 let type_INJ = injectivity "type";;
20 `domain (Fun s t) = s`;;
23 `codomain (Fun s t) = t`;;
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 (* ------------------------------------------------------------------------- *)
30 let term_INDUCT,term_RECURSION = define_type
31 "term = Var string type
32 | Equal type | Select type
34 | Abs string type term";;
36 let term_DISTINCT = distinctness "term";;
38 let term_INJ = injectivity "term";;
40 (* ------------------------------------------------------------------------- *)
41 (* Typing judgements. *)
42 (* ------------------------------------------------------------------------- *)
44 parse_as_infix("has_type",(12,"right"));;
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))`;;
54 let welltyped = new_definition
55 `welltyped tm <=> ?ty. tm has_type ty`;;
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))`;;
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]);;
70 (`!tm. welltyped tm <=> tm has_type (typeof tm)`,
71 REWRITE_TAC[welltyped] THEN MESON_TAC[WELLTYPED_LEMMA]);;
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]);;
87 (* ------------------------------------------------------------------------- *)
88 (* Since equations are important, a bit of derived syntax. *)
89 (* ------------------------------------------------------------------------- *)
91 parse_as_infix("===",(18,"right"));;
93 let equation = new_definition
94 `(s === t) = Comb (Comb (Equal(typeof s)) s) t`;;
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]);;
113 (* ------------------------------------------------------------------------- *)
114 (* Alpha-conversion. *)
115 (* ------------------------------------------------------------------------- *)
117 let ALPHAVARS = define
118 `(ALPHAVARS [] tmp <=> (FST tmp = SND tmp)) /\
119 (ALPHAVARS (CONS tp oenv) tmp <=>
121 ~(FST tp = FST tmp) /\ ~(SND tp = SND tmp) /\ ALPHAVARS oenv tmp)`;;
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)) /\
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))`;;
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))`,
166 GEN_REWRITE_TAC LAND_CONV [RACONV_CASES] THEN
167 REWRITE_TAC[term_INJ; term_DISTINCT; PAIR_EQ] THEN MESON_TAC[]);;
169 let ACONV = new_definition
170 `ACONV t1 t2 <=> RACONV [] (t1,t2)`;;
172 (* ------------------------------------------------------------------------- *)
174 (* ------------------------------------------------------------------------- *)
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]);;
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];
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[]]);;
192 let ACONV_REFL = prove
194 REWRITE_TAC[ACONV] THEN SIMP_TAC[RACONV_REFL; ALL]);;
196 (* ------------------------------------------------------------------------- *)
197 (* Alpha-convertible terms have the same type (if welltyped). *)
198 (* ------------------------------------------------------------------------- *)
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
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]]);;
228 let ACONV_TYPE = prove
229 (`!s t. ACONV s t ==> welltyped s /\ welltyped t ==> (typeof s = typeof t)`,
231 MP_TAC(SPECL [`[]:(term#term)list`; `(s:term,t:term)`] RACONV_TYPE) THEN
232 REWRITE_TAC[ACONV; ALL] THEN MESON_TAC[]);;
234 (* ------------------------------------------------------------------------- *)
235 (* HOL version of "term_union". *)
236 (* ------------------------------------------------------------------------- *)
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)`;;
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]);;
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]);;
258 (* ------------------------------------------------------------------------- *)
259 (* Handy lemma for using it in a sequent. *)
260 (* ------------------------------------------------------------------------- *)
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]);;
267 (* ------------------------------------------------------------------------- *)
268 (* Whether a variable/constant is free in a term. *)
269 (* ------------------------------------------------------------------------- *)
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)`;;
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
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]);;
299 (* ------------------------------------------------------------------------- *)
300 (* Auxiliary association list function. *)
301 (* ------------------------------------------------------------------------- *)
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)`;;
308 (* ------------------------------------------------------------------------- *)
309 (* Substition of types in types. *)
310 (* ------------------------------------------------------------------------- *)
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))`;;
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 (* ------------------------------------------------------------------------- *)
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]);;
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
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]);;
350 let VARIANT = new_specification ["VARIANT"]
351 (PURE_REWRITE_RULE[SKOLEM_THM] VARIANT_EXISTS);;
353 (* ------------------------------------------------------------------------- *)
354 (* Term substitution. *)
355 (* ------------------------------------------------------------------------- *)
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)
371 (* ------------------------------------------------------------------------- *)
372 (* Preservation of type. *)
373 (* ------------------------------------------------------------------------- *)
375 let VSUBST_HAS_TYPE = prove
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];
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
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]);;
425 let VSUBST_WELLTYPED = prove
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]);;
432 (* ------------------------------------------------------------------------- *)
433 (* Right set of free variables. *)
434 (* ------------------------------------------------------------------------- *)
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
448 let VFREE_IN_VSUBST = prove
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[];
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
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
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[]);;
488 (* ------------------------------------------------------------------------- *)
489 (* Sum type to model exception-raising. *)
490 (* ------------------------------------------------------------------------- *)
492 let result_INDUCT,result_RECURSION = define_type
493 "result = Clash term | Result term";;
495 let result_INJ = injectivity "result";;
497 let result_DISTINCT = distinctness "result";;
499 (* ------------------------------------------------------------------------- *)
500 (* Discriminators and extractors. (Nicer to pattern-match...) *)
501 (* ------------------------------------------------------------------------- *)
503 let IS_RESULT = define
504 `(IS_RESULT(Clash t) = F) /\
505 (IS_RESULT(Result t) = T)`;;
507 let IS_CLASH = define
508 `(IS_CLASH(Clash t) = T) /\
509 (IS_CLASH(Result t) = F)`;;
512 `RESULT(Result t) = t`;;
515 `CLASH(Clash t) = t`;;
517 (* ------------------------------------------------------------------------- *)
518 (* We want induction/recursion on term size next. *)
519 (* ------------------------------------------------------------------------- *)
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)`;;
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
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];
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]);;
550 (* ------------------------------------------------------------------------- *)
551 (* Prove existence of INST_CORE. *)
552 (* ------------------------------------------------------------------------- *)
554 let INST_CORE_EXISTS = prove
557 INST_CORE env tyin (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') /\
562 INST_CORE env tyin (Equal ty) = Result(Equal(TYPE_SUBST tyin ty))) /\
564 INST_CORE env tyin (Select ty) = Result(Select(TYPE_SUBST tyin ty))) /\
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')) /\
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).
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);;
593 (* ------------------------------------------------------------------------- *)
595 (* ------------------------------------------------------------------------- *)
597 let INST_CORE = new_specification ["INST_CORE"] INST_CORE_EXISTS;;
599 (* ------------------------------------------------------------------------- *)
600 (* And the overall function. *)
601 (* ------------------------------------------------------------------------- *)
603 let INST_DEF = new_definition
604 `INST tyin tm = RESULT(INST_CORE [] tyin tm)`;;
606 (* ------------------------------------------------------------------------- *)
607 (* Various misc lemmas. *)
608 (* ------------------------------------------------------------------------- *)
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]);;
615 (`(let x = t in P x) = P t`,
616 REWRITE_TAC[LET_DEF; LET_END_DEF]);;
618 (* ------------------------------------------------------------------------- *)
619 (* Put everything together into a deductive system. *)
620 (* ------------------------------------------------------------------------- *)
622 parse_as_infix("|-",(11,"right"));;
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) /\
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) /\
638 asl1 |- p === q /\ asl2 |- p' /\ ACONV p p'
639 ==> TERM_UNION asl1 asl2 |- q) /\
641 asl1 |- c1 /\ asl2 |- c2
642 ==> TERM_UNION (FILTER((~) o ACONV c2) asl1)
643 (FILTER((~) o ACONV c1) asl2)
645 (!tyin asl p. asl |- p ==> MAP (INST tyin) asl |- INST tyin 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)`;;