1 (* ========================================================================= *)
2 (* Formal semantics of HOL inside itself. *)
3 (* ========================================================================= *)
5 (* ------------------------------------------------------------------------- *)
6 (* Semantics of types. *)
7 (* ------------------------------------------------------------------------- *)
9 let typeset = new_recursive_definition type_RECURSION
10 `(typeset tau (Tyvar s) = tau(s)) /\
11 (typeset tau Bool = boolset) /\
12 (typeset tau Ind = indset) /\
13 (typeset tau (Fun a b) = funspace (typeset tau a) (typeset tau b))`;;
15 (* ------------------------------------------------------------------------- *)
16 (* Semantics of terms. *)
17 (* ------------------------------------------------------------------------- *)
19 let semantics = new_recursive_definition term_RECURSION
20 `(semantics sigma tau (Var n ty) = sigma(n,ty)) /\
21 (semantics sigma tau (Equal ty) =
22 abstract (typeset tau ty) (typeset tau (Fun ty Bool))
23 (\x. abstract (typeset tau ty) (typeset tau Bool)
24 (\y. boolean(x = y)))) /\
25 (semantics sigma tau (Select ty) =
26 abstract (typeset tau (Fun ty Bool)) (typeset tau ty)
27 (\s. if ?x. x <: ((typeset tau ty) suchthat (holds s))
28 then ch ((typeset tau ty) suchthat (holds s))
29 else ch (typeset tau ty))) /\
30 (semantics sigma tau (Comb s t) =
31 apply (semantics sigma tau s) (semantics sigma tau t)) /\
32 (semantics sigma tau (Abs n ty t) =
33 abstract (typeset tau ty) (typeset tau (typeof t))
34 (\x. semantics (((n,ty) |-> x) sigma) tau t))`;;
36 (* ------------------------------------------------------------------------- *)
37 (* Valid type and term valuations. *)
38 (* ------------------------------------------------------------------------- *)
40 let type_valuation = new_definition
41 `type_valuation tau <=> !x. (?y. y <: tau x)`;;
43 let term_valuation = new_definition
44 `term_valuation tau sigma <=> !n ty. sigma(n,ty) <: typeset tau ty`;;
46 let TERM_VALUATION_VALMOD = prove
48 term_valuation tau sigma /\ x <: typeset tau ty
49 ==> term_valuation tau (((n,ty) |-> x) sigma)`,
50 REWRITE_TAC[term_valuation; valmod; PAIR_EQ] THEN MESON_TAC[]);;
52 (* ------------------------------------------------------------------------- *)
53 (* All the typesets are nonempty. *)
54 (* ------------------------------------------------------------------------- *)
56 let TYPESET_INHABITED = prove
57 (`!tau ty. type_valuation tau ==> ?x. x <: typeset tau ty`,
58 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
59 MATCH_MP_TAC type_INDUCT THEN REWRITE_TAC[typeset] THEN
61 [ASM_MESON_TAC[type_valuation];
62 ASM_MESON_TAC[BOOLEAN_IN_BOOLSET; INDSET_INHABITED; FUNSPACE_INHABITED]]);;
64 (* ------------------------------------------------------------------------- *)
65 (* Semantics maps into the right place. *)
66 (* ------------------------------------------------------------------------- *)
68 let SEMANTICS_TYPESET_INDUCT = prove
69 (`!tm ty. tm has_type ty
71 !sigma tau. type_valuation tau /\ term_valuation tau sigma
72 ==> (semantics sigma tau tm) <: (typeset tau ty)`,
73 MATCH_MP_TAC has_type_INDUCT THEN
74 ASM_SIMP_TAC[semantics; typeset; has_type_RULES] THEN
75 CONJ_TAC THENL [MESON_TAC[term_valuation]; ALL_TAC] THEN
76 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
77 [MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN REWRITE_TAC[] THEN
78 REPEAT STRIP_TAC THEN MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN
79 REWRITE_TAC[BOOLEAN_IN_BOOLSET];
80 MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN
81 ASM_MESON_TAC[ch; SUCHTHAT; TYPESET_INHABITED];
82 ASM_MESON_TAC[has_type_RULES];
83 MATCH_MP_TAC APPLY_IN_RANSPACE THEN ASM_MESON_TAC[];
84 FIRST_ASSUM(SUBST1_TAC o MATCH_MP WELLTYPED_LEMMA) THEN
85 MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN
86 REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
87 ASM_SIMP_TAC[TERM_VALUATION_VALMOD]]);;
89 let SEMANTICS_TYPESET = prove
91 type_valuation tau /\ term_valuation tau sigma /\ tm has_type ty
92 ==> (semantics sigma tau tm) <: (typeset tau ty)`,
93 MESON_TAC[SEMANTICS_TYPESET_INDUCT]);;
95 (* ------------------------------------------------------------------------- *)
96 (* Semantics of equations. *)
97 (* ------------------------------------------------------------------------- *)
99 let SEMANTICS_EQUATION = prove
101 s has_type (typeof s) /\ t has_type (typeof s) /\
102 type_valuation tau /\ term_valuation tau sigma
103 ==> (semantics sigma tau (s === t) =
104 boolean(semantics sigma tau s = semantics sigma tau t))`,
105 REPEAT STRIP_TAC THEN REWRITE_TAC[equation; semantics] THEN
106 ASM_SIMP_TAC[APPLY_ABSTRACT; typeset; SEMANTICS_TYPESET;
107 ABSTRACT_IN_FUNSPACE; BOOLEAN_IN_BOOLSET]);;
109 let SEMANTICS_EQUATION_ALT = prove
111 (s === t) has_type Bool /\
112 type_valuation tau /\ term_valuation tau sigma
113 ==> (semantics sigma tau (s === t) =
114 boolean(semantics sigma tau s = semantics sigma tau t))`,
115 REPEAT STRIP_TAC THEN MATCH_MP_TAC SEMANTICS_EQUATION THEN
116 ASM_REWRITE_TAC[] THEN
117 SUBGOAL_THEN `welltyped(s === t)` MP_TAC THENL
118 [ASM_MESON_TAC[welltyped]; ALL_TAC] THEN
119 REWRITE_TAC[equation; WELLTYPED_CLAUSES; typeof; codomain] THEN
120 MESON_TAC[welltyped; type_INJ; WELLTYPED; WELLTYPED_CLAUSES]);;
122 (* ------------------------------------------------------------------------- *)
123 (* Quick sanity check. *)
124 (* ------------------------------------------------------------------------- *)
126 let SEMANTICS_SELECT = prove
127 (`p has_type (Fun ty Bool) /\
128 type_valuation tau /\ term_valuation tau sigma
129 ==> (semantics sigma tau (Comb (Select ty) p) =
130 if ?x. x <: (typeset tau ty) suchthat (holds (semantics sigma tau p))
131 then ch((typeset tau ty) suchthat (holds (semantics sigma tau p)))
132 else ch(typeset tau ty))`,
133 REPEAT STRIP_TAC THEN REWRITE_TAC[semantics] THEN
135 let t = find_term (fun t ->
136 can (PART_MATCH (lhs o rand) APPLY_ABSTRACT) t) w in
137 MP_TAC(PART_MATCH (lhs o rand) APPLY_ABSTRACT t)) THEN
140 [ASM_MESON_TAC[SEMANTICS_TYPESET; typeset];
141 REWRITE_TAC[SUCHTHAT] THEN
142 ASM_MESON_TAC[ch; SUCHTHAT; TYPESET_INHABITED]];
144 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[]);;
146 (* ------------------------------------------------------------------------- *)
147 (* Semantics of a sequent. *)
148 (* ------------------------------------------------------------------------- *)
150 parse_as_infix("|=",(11,"right"));;
152 let sequent = new_definition
153 `asms |= p <=> ALL (\a. a has_type Bool) (CONS p asms) /\
154 !sigma tau. type_valuation tau /\
155 term_valuation tau sigma /\
156 ALL (\a. semantics sigma tau a = true) asms
157 ==> (semantics sigma tau p = true)`;;
159 (* ------------------------------------------------------------------------- *)
160 (* Invariance of semantics under alpha-conversion. *)
161 (* ------------------------------------------------------------------------- *)
163 let SEMANTICS_RACONV = prove
166 ==> !sigma1 sigma2 tau.
167 type_valuation tau /\
168 term_valuation tau sigma1 /\ term_valuation tau sigma2 /\
170 ALPHAVARS env (Var x1 ty1,Var x2 ty2)
171 ==> (semantics sigma1 tau (Var x1 ty1) =
172 semantics sigma2 tau (Var x2 ty2)))
173 ==> welltyped(FST tp) /\ welltyped(SND tp)
174 ==> (semantics sigma1 tau (FST tp) =
175 semantics sigma2 tau (SND tp))`,
176 MATCH_MP_TAC RACONV_INDUCT THEN REWRITE_TAC[FORALL_PAIR_THM] THEN
177 REWRITE_TAC[semantics; WELLTYPED_CLAUSES] THEN REPEAT STRIP_TAC THENL
179 BINOP_TAC THEN ASM_MESON_TAC[];
181 FIRST_X_ASSUM SUBST_ALL_TAC THEN MATCH_MP_TAC ABSTRACT_EQ THEN
182 ASM_SIMP_TAC[TYPESET_INHABITED] THEN
183 X_GEN_TAC `x:V` THEN DISCH_TAC THEN REPEAT CONJ_TAC THENL
184 [MATCH_MP_TAC SEMANTICS_TYPESET THEN
185 ASM_SIMP_TAC[TERM_VALUATION_VALMOD; GSYM WELLTYPED];
186 MATCH_MP_TAC SEMANTICS_TYPESET THEN
187 ASM_SIMP_TAC[TERM_VALUATION_VALMOD; GSYM WELLTYPED];
189 RULE_ASSUM_TAC(REWRITE_RULE[IMP_IMP]) THEN
190 FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN CONJ_TAC) THEN
191 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
192 REWRITE_TAC[ALPHAVARS; PAIR_EQ; term_INJ] THEN
193 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[VALMOD; PAIR_EQ] THEN
196 let SEMANTICS_ACONV = prove
198 type_valuation tau /\ term_valuation tau sigma /\
199 welltyped s /\ welltyped t /\ ACONV s t
200 ==> (semantics sigma tau s = semantics sigma tau t)`,
201 REWRITE_TAC[ACONV] THEN REPEAT STRIP_TAC THEN
202 MATCH_MP_TAC(REWRITE_RULE[IMP_IMP; RIGHT_IMP_FORALL_THM; FORALL_PAIR_THM]
203 SEMANTICS_RACONV) THEN
204 EXISTS_TAC `[]:(term#term)list` THEN
205 ASM_SIMP_TAC[ALPHAVARS; term_INJ; PAIR_EQ]);;
207 (* ------------------------------------------------------------------------- *)
208 (* General semantic lemma about binary inference rules. *)
209 (* ------------------------------------------------------------------------- *)
211 let BINARY_INFERENCE_RULE = prove
212 (`(p1 has_type Bool /\ p2 has_type Bool
213 ==> q has_type Bool /\
214 !sigma tau. type_valuation tau /\ term_valuation tau sigma /\
215 (semantics sigma tau p1 = true) /\
216 (semantics sigma tau p2 = true)
217 ==> (semantics sigma tau q = true))
218 ==> (asl1 |= p1 /\ asl2 |= p2 ==> TERM_UNION asl1 asl2 |= q)`,
219 REWRITE_TAC[sequent; ALL] THEN STRIP_TAC THEN STRIP_TAC THEN
220 ASM_SIMP_TAC[ALL_BOOL_TERM_UNION] THEN REPEAT STRIP_TAC THEN
221 FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN ASM_REWRITE_TAC[] THEN
222 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MATCH_MP_TAC) THEN
223 ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
224 ASM_REWRITE_TAC[] THEN UNDISCH_TAC
225 `ALL (\a. semantics sigma tau a = true) (TERM_UNION asl1 asl2)` THEN
226 REWRITE_TAC[GSYM ALL_MEM] THEN
227 REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM ALL_MEM])) THEN
228 REWRITE_TAC[] THEN STRIP_TAC THEN STRIP_TAC THEN
229 DISCH_THEN(fun th -> X_GEN_TAC `r:term` THEN DISCH_TAC THEN MP_TAC th) THEN
230 MP_TAC(SPECL [`asl1:term list`; `asl2:term list`; `r:term`]
232 ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `s:term`) THEN
233 DISCH_THEN(MP_TAC o SPEC `s:term`) THEN ASM_REWRITE_TAC[] THEN
234 ASM_MESON_TAC[SEMANTICS_ACONV; welltyped; TERM_UNION_NONEW]);;
236 (* ------------------------------------------------------------------------- *)
237 (* Semantics only depends on valuations of free variables. *)
238 (* ------------------------------------------------------------------------- *)
240 let TERM_VALUATION_VFREE_IN = prove
241 (`!tau sigma1 sigma2 t.
242 type_valuation tau /\
243 term_valuation tau sigma1 /\ term_valuation tau sigma2 /\
245 (!x ty. VFREE_IN (Var x ty) t ==> (sigma1(x,ty) = sigma2(x,ty)))
246 ==> (semantics sigma1 tau t = semantics sigma2 tau t)`,
247 GEN_TAC THEN GEN_REWRITE_TAC BINDER_CONV [SWAP_FORALL_THM] THEN
248 GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN MATCH_MP_TAC term_INDUCT THEN
249 REWRITE_TAC[semantics; VFREE_IN; term_DISTINCT; term_INJ] THEN
250 REPEAT STRIP_TAC THENL
252 BINOP_TAC THEN ASM_MESON_TAC[WELLTYPED_CLAUSES];
254 MATCH_MP_TAC ABSTRACT_EQ THEN ASM_SIMP_TAC[TYPESET_INHABITED] THEN
255 X_GEN_TAC `x:V` THEN DISCH_TAC THEN REPEAT(CONJ_TAC THENL
256 [ASM_MESON_TAC[TERM_VALUATION_VALMOD; WELLTYPED; WELLTYPED_CLAUSES;
259 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
260 CONJ_TAC THENL [ASM_MESON_TAC[WELLTYPED_CLAUSES]; ALL_TAC] THEN
261 MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`] THEN DISCH_TAC THEN
262 REWRITE_TAC[VALMOD; PAIR_EQ] THEN ASM_MESON_TAC[]);;
264 (* ------------------------------------------------------------------------- *)
265 (* Prove some inference rules correct. *)
266 (* ------------------------------------------------------------------------- *)
268 let ASSUME_correct = prove
269 (`!p. p has_type Bool ==> [p] |= p`,
270 SIMP_TAC[sequent; ALL]);;
272 let REFL_correct = prove
273 (`!t. welltyped t ==> [] |= t === t`,
274 SIMP_TAC[sequent; SEMANTICS_EQUATION; ALL; WELLTYPED] THEN
275 REWRITE_TAC[boolean; equation] THEN MESON_TAC[has_type_RULES]);;
277 let TRANS_correct = prove
278 (`!asl1 asl2 l m1 m2 r.
279 asl1 |= l === m1 /\ asl2 |= m2 === r /\ ACONV m1 m2
280 ==> TERM_UNION asl1 asl2 |= l === r`,
281 REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
282 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
283 MATCH_MP_TAC BINARY_INFERENCE_RULE THEN STRIP_TAC THEN
284 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
285 [ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL; ACONV_TYPE];
286 ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; IMP_CONJ; boolean] THEN
287 ASM_MESON_TAC[SEMANTICS_ACONV; TRUE_NE_FALSE; EQUATION_HAS_TYPE_BOOL]]);;
289 let MK_COMB_correct = prove
290 (`!asl1 l1 r1 asl2 l2 r2.
291 asl1 |= l1 === r1 /\ asl2 |= l2 === r2 /\
292 (?rty. typeof l1 = Fun (typeof l2) rty)
293 ==> TERM_UNION asl1 asl2 |= Comb l1 l2 === Comb r1 r2`,
294 REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
295 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
296 MATCH_MP_TAC BINARY_INFERENCE_RULE THEN STRIP_TAC THEN
297 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
298 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
299 REWRITE_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_CLAUSES; typeof] THEN
301 ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; IMP_CONJ; boolean] THEN
302 REWRITE_TAC[semantics] THEN
303 ASM_MESON_TAC[SEMANTICS_ACONV; TRUE_NE_FALSE; EQUATION_HAS_TYPE_BOOL]]);;
305 let EQ_MP_correct = prove
307 asl1 |= p === q /\ asl2 |= p' /\ ACONV p p'
308 ==> TERM_UNION asl1 asl2 |= q`,
309 REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
310 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
311 MATCH_MP_TAC BINARY_INFERENCE_RULE THEN STRIP_TAC THEN
312 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
313 [ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_LEMMA; WELLTYPED;
315 ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; IMP_CONJ; boolean] THEN
316 ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL; TRUE_NE_FALSE; SEMANTICS_ACONV;
319 let BETA_correct = prove
320 (`!x ty t. welltyped t ==> [] |= Comb (Abs x ty t) (Var x ty) === t`,
321 REPEAT STRIP_TAC THEN REWRITE_TAC[sequent; ALL] THEN
322 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
323 [REWRITE_TAC[EQUATION_HAS_TYPE_BOOL; typeof; WELLTYPED_CLAUSES] THEN
324 REWRITE_TAC[codomain; type_INJ] THEN ASM_MESON_TAC[];
326 SIMP_TAC[SEMANTICS_EQUATION_ALT] THEN
327 DISCH_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
328 REWRITE_TAC[BOOLEAN_EQ_TRUE; semantics] THEN
329 MATCH_MP_TAC EQ_TRANS THEN
330 EXISTS_TAC `semantics (((x,ty) |-> sigma(x,ty)) sigma) tau t` THEN
331 CONJ_TAC THENL [MATCH_MP_TAC APPLY_ABSTRACT; ALL_TAC] THEN
332 REWRITE_TAC[VALMOD_REPEAT] THEN
333 ASM_MESON_TAC[term_valuation; SEMANTICS_TYPESET; WELLTYPED]);;
335 let ABS_correct = prove
337 ~(EX (VFREE_IN (Var x ty)) asl) /\ asl |= l === r
338 ==> asl |= (Abs x ty l) === (Abs x ty r)`,
339 REPEAT GEN_TAC THEN REWRITE_TAC[sequent; ALL] THEN STRIP_TAC THEN
340 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
342 [UNDISCH_TAC `(l === r) has_type Bool` THEN
343 SIMP_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_CLAUSES; typeof];
345 DISCH_TAC THEN ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; BOOLEAN_EQ_TRUE] THEN
346 REPEAT STRIP_TAC THEN REWRITE_TAC[semantics] THEN
347 SUBGOAL_THEN `typeof r = typeof l` SUBST1_TAC THENL
348 [ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL]; ALL_TAC] THEN
349 MATCH_MP_TAC ABSTRACT_EQ THEN ASM_SIMP_TAC[TYPESET_INHABITED] THEN
350 X_GEN_TAC `x:V` THEN DISCH_TAC THEN
351 REPEAT(CONJ_TAC THENL
352 [ASM_MESON_TAC[SEMANTICS_TYPESET; TERM_VALUATION_VALMOD;
353 WELLTYPED; EQUATION_HAS_TYPE_BOOL];
355 FIRST_X_ASSUM(MP_TAC o check (is_forall o concl)) THEN
356 ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; BOOLEAN_EQ_TRUE] THEN
357 DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
358 SUBGOAL_THEN `ALL (\a. a has_type Bool) asl /\
359 ALL (\a. ~(VFREE_IN (Var x ty) a)) asl /\
360 ALL (\a. semantics sigma tau a = true) asl`
361 MP_TAC THENL [ASM_REWRITE_TAC[GSYM NOT_EX; ETA_AX]; ALL_TAC] THEN
362 REWRITE_TAC[AND_ALL] THEN
363 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
364 X_GEN_TAC `p:term` THEN DISCH_TAC THEN REWRITE_TAC[] THEN
365 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
366 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THEN
367 MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
368 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
369 CONJ_TAC THENL [ASM_MESON_TAC[welltyped]; ALL_TAC] THEN
370 REPEAT STRIP_TAC THEN REWRITE_TAC[VALMOD; PAIR_EQ] THEN ASM_MESON_TAC[]);;
372 let DEDUCT_ANTISYM_RULE_correct = prove
374 asl1 |= c1 /\ asl2 |= c2
375 ==> let asl1' = FILTER((~) o ACONV c2) asl1
376 and asl2' = FILTER((~) o ACONV c1) asl2 in
377 (TERM_UNION asl1' asl2') |= c1 === c2`,
379 REWRITE_TAC[sequent; o_DEF; LET_DEF; LET_END_DEF; GSYM CONJ_ASSOC] THEN
381 (a1 /\ b1 ==> c1) /\ (a1 /\ b1 /\ c1 ==> a2 /\ b2 ==> c2)
382 ==> a1 /\ a2 /\ b1 /\ b2 ==> c1 /\ c2`) THEN
384 [REWRITE_TAC[GSYM ALL_MEM; MEM] THEN REPEAT STRIP_TAC THEN
385 ASM_REWRITE_TAC[EQUATION_HAS_TYPE_BOOL] THEN
386 ASM_MESON_TAC[MEM_FILTER; TERM_UNION_NONEW; welltyped; WELLTYPED_LEMMA];
388 REWRITE_TAC[ALL; AND_FORALL_THM] THEN REWRITE_TAC[GSYM ALL_MEM] THEN
390 REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
391 DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
392 ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; BOOLEAN_EQ_TRUE] THEN
393 REPEAT STRIP_TAC THEN MATCH_MP_TAC BOOLEAN_EQ THEN
394 REPEAT(CONJ_TAC THENL
395 [ASM_MESON_TAC[typeset; SEMANTICS_TYPESET]; ALL_TAC]) THEN
396 EQ_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
397 X_GEN_TAC `a:term` THEN DISCH_TAC THENL
398 [ASM_CASES_TAC `ACONV c1 a` THENL
399 [ASM_MESON_TAC[SEMANTICS_ACONV; welltyped]; ALL_TAC];
400 ASM_CASES_TAC `ACONV c2 a` THENL
401 [ASM_MESON_TAC[SEMANTICS_ACONV; welltyped]; ALL_TAC]] THEN
403 `MEM a (FILTER (\x. ~ACONV c2 x) asl1) \/
404 MEM a (FILTER (\x. ~ACONV c1 x) asl2)`
406 [REWRITE_TAC[MEM_FILTER] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
407 DISCH_THEN(MP_TAC o MATCH_MP TERM_UNION_THM) THEN
408 ASM_MESON_TAC[SEMANTICS_ACONV; welltyped]));;
410 (* ------------------------------------------------------------------------- *)
411 (* Correct semantics for term substitution. *)
412 (* ------------------------------------------------------------------------- *)
414 let DEST_VAR = new_recursive_definition term_RECURSION
415 `DEST_VAR (Var x ty) = (x,ty)`;;
417 let TERM_VALUATION_ITLIST = prove
419 type_valuation tau /\ term_valuation tau sigma /\
420 (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
421 ==> term_valuation tau
422 (ITLIST (\(t,x). DEST_VAR x |-> semantics sigma tau t) ilist sigma)`,
423 MATCH_MP_TAC list_INDUCT THEN SIMP_TAC[ITLIST] THEN
424 REWRITE_TAC[FORALL_PAIR_THM; MEM; PAIR_EQ] THEN
425 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
426 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
427 SIMP_TAC[LEFT_FORALL_IMP_THM; FORALL_AND_THM] THEN
428 REWRITE_TAC[LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
429 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[DEST_VAR] THEN
430 ASM_SIMP_TAC[TERM_VALUATION_VALMOD; SEMANTICS_TYPESET]);;
432 let ITLIST_VALMOD_FILTER = prove
433 (`!ilist sigma sem x ty y yty.
434 (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
435 ==> (ITLIST (\(t,x). DEST_VAR x |-> sem x t)
436 (FILTER (\(s',s). ~(s = Var x ty)) ilist) sigma (y,yty) =
437 if (y = x) /\ (yty = ty) then sigma(y,yty)
438 else ITLIST (\(t,x). DEST_VAR x |-> sem x t) ilist sigma (y,yty))`,
439 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[FILTER; ITLIST; COND_ID] THEN
440 REWRITE_TAC[FORALL_PAIR_THM] THEN
441 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
442 REWRITE_TAC[MEM; TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
443 SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
444 REWRITE_TAC[WELLTYPED_CLAUSES; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
445 MAP_EVERY X_GEN_TAC [`t:term`; `pp:term`; `ilist:(term#term)list`] THEN
446 DISCH_TAC THEN REPEAT GEN_TAC THEN
447 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
448 DISCH_THEN(X_CHOOSE_THEN `s:string` MP_TAC) THEN
449 DISCH_THEN(X_CHOOSE_THEN `sty:type` MP_TAC) THEN
450 DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
451 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RAND] THEN
452 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RATOR] THEN
453 ASM_REWRITE_TAC[ITLIST] THEN
454 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
455 REWRITE_TAC[DEST_VAR] THEN
456 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RATOR] THEN
457 REWRITE_TAC[VALMOD] THEN REWRITE_TAC[term_INJ] THEN
458 ASM_CASES_TAC `(s:string = x) /\ (sty:type = ty)` THEN
459 ASM_SIMP_TAC[PAIR_EQ] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
461 let ITLIST_VALMOD_EQ = prove
462 (`!l. (!t x. MEM (t,x) l /\ (f x = a) ==> (g x t = h x t)) /\ (i a = j a)
463 ==> (ITLIST (\(t,x). f(x) |-> g x t) l i a =
464 ITLIST (\(t,x). f(x) |-> h x t) l j a)`,
465 MATCH_MP_TAC list_INDUCT THEN SIMP_TAC[MEM; ITLIST; FORALL_PAIR_THM] THEN
466 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
467 REWRITE_TAC[PAIR_EQ; VALMOD] THEN MESON_TAC[]);;
469 let SEMANTICS_VSUBST = prove
470 (`!tm sigma tau ilist.
472 (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
473 ==> !sigma tau. type_valuation tau /\ term_valuation tau sigma
474 ==> (semantics sigma tau (VSUBST ilist tm) =
477 (\(t,x). DEST_VAR x |-> semantics sigma tau t)
480 MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VSUBST; semantics] THEN
482 [MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`] THEN
483 MATCH_MP_TAC list_INDUCT THEN
484 REWRITE_TAC[MEM; REV_ASSOCD; ITLIST; semantics; FORALL_PAIR_THM] THEN
485 MAP_EVERY X_GEN_TAC [`t:term`; `s:term`; `ilist:(term#term)list`] THEN
486 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
487 SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
488 REWRITE_TAC[WELLTYPED_CLAUSES; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
490 DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN MP_TAC th) THEN
491 ASM_REWRITE_TAC[] THEN
492 FIRST_X_ASSUM(X_CHOOSE_THEN `y:string` MP_TAC) THEN
493 DISCH_THEN(X_CHOOSE_THEN `tty:type` MP_TAC) THEN
494 DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
495 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
496 REWRITE_TAC[DEST_VAR; VALMOD; term_INJ; PAIR_EQ] THEN ASM_MESON_TAC[];
499 [REWRITE_TAC[WELLTYPED_CLAUSES] THEN REPEAT STRIP_TAC THEN
500 BINOP_TAC THEN ASM_MESON_TAC[];
502 MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN
503 REWRITE_TAC[WELLTYPED_CLAUSES] THEN
504 ASM_CASES_TAC `welltyped t` THEN ASM_REWRITE_TAC[] THEN
505 REPEAT STRIP_TAC THEN LET_TAC THEN LET_TAC THEN
507 `!s s'. MEM (s',s) ilist' ==> (?x ty. (s = Var x ty) /\ s' has_type ty)`
509 [EXPAND_TAC "ilist'" THEN ASM_SIMP_TAC[MEM_FILTER]; ALL_TAC] THEN
513 `!s s'. MEM (s',s) ilist'' ==> (?x ty. (s = Var x ty) /\ s' has_type ty)`
515 [EXPAND_TAC "ilist''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
516 ASM_MESON_TAC[has_type_RULES];
519 REWRITE_TAC[semantics] THEN
520 MATCH_MP_TAC ABSTRACT_EQ THEN ASM_SIMP_TAC[TYPESET_INHABITED] THEN
521 X_GEN_TAC `a:V` THEN DISCH_TAC THEN
522 REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC SEMANTICS_TYPESET) THEN
523 ASM_SIMP_TAC[TERM_VALUATION_VALMOD; TERM_VALUATION_ITLIST] THEN
525 ASM_SIMP_TAC[VSUBST_WELLTYPED; GSYM WELLTYPED; TERM_VALUATION_VALMOD] THEN
526 MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
527 ASM_SIMP_TAC[TERM_VALUATION_VALMOD; TERM_VALUATION_ITLIST] THEN
528 MAP_EVERY X_GEN_TAC [`u:string`; `uty:type`] THEN DISCH_TAC THENL
529 [EXPAND_TAC "ilist''" THEN REWRITE_TAC[ITLIST] THEN
530 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
531 REWRITE_TAC[DEST_VAR; VALMOD; PAIR_EQ] THEN
532 COND_CASES_TAC THEN ASM_REWRITE_TAC[semantics; VALMOD];
534 EXPAND_TAC "ilist'" THEN ASM_SIMP_TAC[ITLIST_VALMOD_FILTER] THEN
535 REWRITE_TAC[VALMOD] THENL
537 REWRITE_TAC[PAIR_EQ] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
538 MATCH_MP_TAC ITLIST_VALMOD_EQ THEN ASM_REWRITE_TAC[VALMOD; PAIR_EQ] THEN
539 MAP_EVERY X_GEN_TAC [`s':term`; `s:term`] THEN STRIP_TAC THEN
540 FIRST_X_ASSUM(MP_TAC o C MATCH_MP
541 (ASSUME `MEM (s':term,s:term) ilist`)) THEN
542 DISCH_THEN(X_CHOOSE_THEN `w:string` MP_TAC) THEN
543 DISCH_THEN(X_CHOOSE_THEN `wty:type` MP_TAC) THEN
544 DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
545 UNDISCH_TAC `DEST_VAR (Var w wty) = u,uty` THEN
546 REWRITE_TAC[DEST_VAR; PAIR_EQ] THEN
547 DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
548 MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
549 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
550 CONJ_TAC THENL [ASM_MESON_TAC[welltyped]; ALL_TAC] THEN
551 MAP_EVERY X_GEN_TAC [`v:string`; `vty:type`] THEN
552 DISCH_TAC THEN REWRITE_TAC[VALMOD; PAIR_EQ] THEN
553 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
554 FIRST_X_ASSUM(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
555 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EX]) THEN
556 REWRITE_TAC[GSYM ALL_MEM] THEN
557 DISCH_THEN(MP_TAC o SPEC `(s':term,Var u uty)`) THEN
558 ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
559 ASM_REWRITE_TAC[] THEN EXPAND_TAC "ilist'" THEN
560 REWRITE_TAC[MEM_FILTER] THEN
561 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
562 ASM_REWRITE_TAC[term_INJ]] THEN
563 MP_TAC(ISPECL [`t':term`; `x:string`; `ty:type`] VARIANT) THEN
564 ASM_REWRITE_TAC[] THEN EXPAND_TAC "t'" THEN
565 REWRITE_TAC[VFREE_IN_VSUBST] THEN
566 REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b) = b ==> ~a`] THEN
567 DISCH_THEN(MP_TAC o SPECL [`u:string`; `uty:type`]) THEN
568 ASM_REWRITE_TAC[] THEN
570 `REV_ASSOCD (Var u uty) ilist' (Var u uty) =
571 REV_ASSOCD (Var u uty) ilist (Var u uty)`
573 [EXPAND_TAC "ilist'" THEN REWRITE_TAC[REV_ASSOCD_FILTER] THEN
574 ASM_REWRITE_TAC[term_INJ];
577 `!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty` THEN
578 SPEC_TAC(`ilist:(term#term)list`,`l:(term#term)list`) THEN
579 MATCH_MP_TAC list_INDUCT THEN
580 REWRITE_TAC[REV_ASSOCD; ITLIST; VFREE_IN; VALMOD; term_INJ] THEN
581 SIMP_TAC[PAIR_EQ] THEN REWRITE_TAC[FORALL_PAIR_THM] THEN
582 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
583 REWRITE_TAC[VALMOD; REV_ASSOCD; MEM] THEN
584 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
585 SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
586 REWRITE_TAC[WELLTYPED_CLAUSES; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
587 MAP_EVERY X_GEN_TAC [`t1:term`; `t2:term`; `i:(term#term)list`] THEN
589 DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN MP_TAC th) THEN
590 FIRST_X_ASSUM(X_CHOOSE_THEN `v:string` MP_TAC) THEN
591 DISCH_THEN(X_CHOOSE_THEN `vty:type` MP_TAC) THEN
592 DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
593 ASM_REWRITE_TAC[DEST_VAR; term_INJ; PAIR_EQ] THEN
594 SUBGOAL_THEN `(v:string = u) /\ (vty:type = uty) <=> (u = v) /\ (uty = vty)`
595 SUBST1_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
596 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
597 REPEAT STRIP_TAC THEN MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
598 ASM_SIMP_TAC[TERM_VALUATION_VALMOD; VALMOD] THEN
599 REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[welltyped; term_INJ]);;
601 (* ------------------------------------------------------------------------- *)
602 (* Hence correctness of INST. *)
603 (* ------------------------------------------------------------------------- *)
605 let INST_correct = prove
607 (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
608 ==> asl |= p ==> MAP (VSUBST ilist) asl |= VSUBST ilist p`,
609 REWRITE_TAC[sequent] THEN REPEAT STRIP_TAC THENL
610 [UNDISCH_TAC `ALL (\a. a has_type Bool) (CONS p asl)` THEN
611 REWRITE_TAC[ALL; ALL_MAP] THEN MATCH_MP_TAC MONO_AND THEN
614 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
615 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[o_THM]] THEN
616 DISCH_TAC THEN MATCH_MP_TAC VSUBST_HAS_TYPE THEN ASM_REWRITE_TAC[];
618 SUBGOAL_THEN `welltyped p` ASSUME_TAC THENL
619 [ASM_MESON_TAC[welltyped; ALL]; ALL_TAC] THEN
620 ASM_SIMP_TAC[SEMANTICS_VSUBST] THEN
621 FIRST_X_ASSUM MATCH_MP_TAC THEN
622 ASM_SIMP_TAC[TERM_VALUATION_ITLIST] THEN
623 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ALL_MAP]) THEN
624 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
625 X_GEN_TAC `a:term` THEN DISCH_TAC THEN
626 SUBGOAL_THEN `welltyped a` MP_TAC THENL
627 [ASM_MESON_TAC[ALL_MEM; MEM; welltyped]; ALL_TAC] THEN
628 ASM_SIMP_TAC[SEMANTICS_VSUBST; o_THM]);;
630 (* ------------------------------------------------------------------------- *)
631 (* Lemma about typesets to simplify some later goals. *)
632 (* ------------------------------------------------------------------------- *)
634 let TYPESET_LEMMA = prove
636 typeset (\s. typeset tau (REV_ASSOCD (Tyvar s) tyin (Tyvar s))) ty =
637 typeset tau (TYPE_SUBST tyin ty)`,
638 MATCH_MP_TAC type_INDUCT THEN SIMP_TAC[typeset; TYPE_SUBST]);;
640 (* ------------------------------------------------------------------------- *)
641 (* Semantics of type instantiation core. *)
642 (* ------------------------------------------------------------------------- *)
644 let SEMANTICS_INST_CORE = prove
646 welltyped tm /\ (sizeof tm = n) /\
647 (!s s'. MEM (s,s') env
648 ==> ?x ty. (s = Var x ty) /\
649 (s' = Var x (TYPE_SUBST tyin ty)))
650 ==> (?x ty. (INST_CORE env tyin tm =
651 Clash(Var x (TYPE_SUBST tyin ty))) /\
652 VFREE_IN (Var x ty) tm /\
653 ~(REV_ASSOCD (Var x (TYPE_SUBST tyin ty))
654 env (Var x ty) = Var x ty)) \/
655 (!x ty. VFREE_IN (Var x ty) tm
656 ==> (REV_ASSOCD (Var x (TYPE_SUBST tyin ty))
657 env (Var x ty) = Var x ty)) /\
658 (?tm'. (INST_CORE env tyin tm = Result tm') /\
659 tm' has_type (TYPE_SUBST tyin (typeof tm)) /\
660 (!u uty. VFREE_IN (Var u uty) tm' <=>
661 ?oty. VFREE_IN (Var u oty) tm /\
662 (uty = TYPE_SUBST tyin oty)) /\
664 type_valuation tau /\ term_valuation tau sigma
665 ==> (semantics sigma tau tm' =
667 (\(x,ty). sigma(x,TYPE_SUBST tyin ty))
668 (\s. typeset tau (TYPE_SUBST tyin (Tyvar s)))
670 MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
671 MATCH_MP_TAC term_INDUCT THEN
672 ONCE_REWRITE_TAC[INST_CORE] THEN REWRITE_TAC[semantics] THEN
673 REPEAT CONJ_TAC THENL
674 [POP_ASSUM(K ALL_TAC) THEN
675 REWRITE_TAC[REV_ASSOCD; LET_DEF; LET_END_DEF] THEN
676 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
677 ASM_REWRITE_TAC[result_DISTINCT; result_INJ; UNWIND_THM1] THEN
678 REWRITE_TAC[typeof; has_type_RULES] THEN
679 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
680 REWRITE_TAC[RESULT; semantics; VFREE_IN; term_INJ] THEN ASM_MESON_TAC[];
681 POP_ASSUM(K ALL_TAC) THEN
682 REWRITE_TAC[TYPE_SUBST; RESULT; VFREE_IN; term_DISTINCT] THEN
683 ASM_REWRITE_TAC[result_DISTINCT; result_INJ; UNWIND_THM1] THEN
684 REWRITE_TAC[typeof; has_type_RULES; TYPE_SUBST; VFREE_IN] THEN
685 REWRITE_TAC[semantics; typeset; TYPESET_LEMMA; TYPE_SUBST; term_DISTINCT];
686 POP_ASSUM(K ALL_TAC) THEN
687 REWRITE_TAC[TYPE_SUBST; RESULT; VFREE_IN; term_DISTINCT] THEN
688 ASM_REWRITE_TAC[result_DISTINCT; result_INJ; UNWIND_THM1] THEN
689 REWRITE_TAC[typeof; has_type_RULES; TYPE_SUBST; VFREE_IN] THEN
690 REWRITE_TAC[semantics; typeset; TYPESET_LEMMA; TYPE_SUBST; term_DISTINCT];
691 MAP_EVERY X_GEN_TAC [`s:term`; `t:term`] THEN DISCH_THEN(K ALL_TAC) THEN
692 POP_ASSUM MP_TAC THEN ASM_CASES_TAC `n = sizeof(Comb s t)` THEN
693 ASM_REWRITE_TAC[] THEN
694 DISCH_THEN(fun th -> MP_TAC(SPEC `sizeof t` th) THEN
695 MP_TAC(SPEC `sizeof s` th)) THEN
696 REWRITE_TAC[sizeof; ARITH_RULE `s < 1 + s + t /\ t < 1 + s + t`] THEN
697 DISCH_THEN(fun th -> DISCH_THEN(MP_TAC o SPEC `t:term`) THEN
698 MP_TAC(SPEC `s:term` th)) THEN
699 REWRITE_TAC[IMP_IMP; AND_FORALL_THM; WELLTYPED_CLAUSES] THEN
700 REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
701 DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN
702 GEN_REWRITE_TAC I [IMP_CONJ] THEN
703 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
704 [DISCH_THEN(fun th -> DISCH_THEN(K ALL_TAC) THEN MP_TAC th) THEN
705 DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th) THEN
706 REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
707 STRIP_TAC THEN ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; IS_CLASH; VFREE_IN];
709 REWRITE_TAC[TYPE_SUBST] THEN
710 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
711 DISCH_THEN(X_CHOOSE_THEN `s':term` STRIP_ASSUME_TAC) THEN
712 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
713 [DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th) THEN
714 REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
715 STRIP_TAC THEN ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; IS_CLASH; VFREE_IN];
717 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
718 DISCH_THEN(X_CHOOSE_THEN `t':term` STRIP_ASSUME_TAC) THEN
719 DISJ2_TAC THEN CONJ_TAC THENL
720 [REWRITE_TAC[VFREE_IN] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
721 EXISTS_TAC `Comb s' t'` THEN
722 ASM_SIMP_TAC[LET_DEF; LET_END_DEF; IS_CLASH; semantics; RESULT] THEN
723 ASM_REWRITE_TAC[VFREE_IN] THEN
724 ASM_REWRITE_TAC[typeof] THEN ONCE_REWRITE_TAC[has_type_CASES] THEN
725 REWRITE_TAC[term_DISTINCT; term_INJ; codomain] THEN ASM_MESON_TAC[];
727 MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN
728 DISCH_THEN(K ALL_TAC) THEN POP_ASSUM MP_TAC THEN
729 ASM_CASES_TAC `n = sizeof (Abs x ty t)` THEN ASM_REWRITE_TAC[] THEN
730 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
731 REWRITE_TAC[WELLTYPED_CLAUSES] THEN STRIP_TAC THEN REPEAT LET_TAC THEN
732 FIRST_ASSUM(MP_TAC o SPEC `sizeof t`) THEN
733 REWRITE_TAC[sizeof; ARITH_RULE `t < 2 + t`] THEN
734 DISCH_THEN(MP_TAC o SPECL
735 [`t:term`; `env':(term#term)list`; `tyin:(type#type)list`]) THEN
736 ASM_REWRITE_TAC[] THEN
738 [EXPAND_TAC "env'" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN ASM_MESON_TAC[];
740 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
742 FIRST_X_ASSUM(K ALL_TAC o SPEC `0`) THEN
743 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
744 DISCH_THEN(X_CHOOSE_THEN `t':term` STRIP_ASSUME_TAC) THEN
745 DISJ2_TAC THEN ASM_REWRITE_TAC[IS_RESULT] THEN CONJ_TAC THENL
746 [FIRST_X_ASSUM(fun th ->
747 MP_TAC th THEN MATCH_MP_TAC MONO_FORALL THEN
748 GEN_TAC THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
749 DISCH_THEN(MP_TAC o check (is_imp o concl))) THEN
750 EXPAND_TAC "env'" THEN
751 REWRITE_TAC[VFREE_IN; REV_ASSOCD; term_INJ] THEN
752 COND_CASES_TAC THEN ASM_REWRITE_TAC[term_INJ] THEN MESON_TAC[];
754 REWRITE_TAC[result_INJ; UNWIND_THM1; RESULT] THEN
755 MATCH_MP_TAC(TAUT `a /\ b /\ (b ==> c) ==> b /\ a /\ c`) THEN
757 [ASM_REWRITE_TAC[VFREE_IN; term_INJ] THEN
758 MAP_EVERY X_GEN_TAC [`u:string`; `uty:type`] THEN
759 ASM_CASES_TAC `u:string = x` THEN ASM_REWRITE_TAC[] THEN
760 UNDISCH_THEN `u:string = x` SUBST_ALL_TAC THEN
761 REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
762 AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
763 X_GEN_TAC `oty:type` THEN REWRITE_TAC[] THEN
764 ASM_CASES_TAC `uty = TYPE_SUBST tyin oty` THEN ASM_REWRITE_TAC[] THEN
765 ASM_CASES_TAC `VFREE_IN (Var x oty) t` THEN ASM_REWRITE_TAC[] THEN
766 EQ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
767 REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
768 FIRST_X_ASSUM(fun th ->
769 MP_TAC(SPECL [`x:string`; `oty:type`] th) THEN
770 ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN NO_TAC; ALL_TAC]) THEN
771 EXPAND_TAC "env'" THEN REWRITE_TAC[REV_ASSOCD] THEN
772 ASM_MESON_TAC[term_INJ];
775 [REWRITE_TAC[typeof; TYPE_SUBST] THEN ASM_REWRITE_TAC[] THEN
776 ASM_MESON_TAC[has_type_RULES];
778 DISCH_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
779 REWRITE_TAC[semantics] THEN
780 ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
781 MATCH_MP_TAC ABSTRACT_EQ THEN
782 CONJ_TAC THENL [ASM_SIMP_TAC[TYPESET_INHABITED]; ALL_TAC] THEN
783 X_GEN_TAC `a:V` THEN REWRITE_TAC[] THEN DISCH_TAC THEN CONJ_TAC THENL
784 [MATCH_MP_TAC SEMANTICS_TYPESET THEN
785 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
786 ASM_MESON_TAC[welltyped; WELLTYPED];
788 MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> a /\ b`) THEN CONJ_TAC THENL
789 [DISCH_THEN(SUBST1_TAC o SYM) THEN
790 MATCH_MP_TAC SEMANTICS_TYPESET THEN
791 ASM_SIMP_TAC[TERM_VALUATION_VALMOD];
793 FIRST_X_ASSUM(MP_TAC o SPECL
794 [`(x,ty' |-> a) (sigma:(string#type)->V)`; `tau:string->V`]) THEN
795 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN DISCH_TAC THEN
796 REWRITE_TAC[GSYM(CONJUNCT1 TYPE_SUBST)] THEN
797 MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN CONJ_TAC THENL
798 [REWRITE_TAC[type_valuation] THEN ASM_SIMP_TAC[TYPESET_INHABITED];
801 [REWRITE_TAC[term_valuation] THEN
802 MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
803 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
804 REWRITE_TAC[VALMOD; PAIR_EQ] THEN
805 COND_CASES_TAC THEN ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
806 ASM_MESON_TAC[term_valuation];
809 [REWRITE_TAC[term_valuation] THEN
810 MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
811 REWRITE_TAC[VALMOD] THEN
812 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
813 REWRITE_TAC[VALMOD; PAIR_EQ] THEN
814 COND_CASES_TAC THEN ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
815 ASM_MESON_TAC[term_valuation];
819 VFREE_IN (Var u uty) t' <=>
820 (?oty. VFREE_IN (Var u oty) t /\ (uty = TYPE_SUBST tyin oty))`
822 ASM_REWRITE_TAC[] THEN MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
823 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
824 REWRITE_TAC[VALMOD] THEN
825 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
826 ASM_CASES_TAC `y:string = x` THEN ASM_REWRITE_TAC[PAIR_EQ] THEN
827 ASM_CASES_TAC `yty:type = ty` THEN ASM_REWRITE_TAC[] THEN
828 UNDISCH_THEN `y:string = x` SUBST_ALL_TAC THEN COND_CASES_TAC THEN
829 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
830 FIRST_X_ASSUM(MP_TAC o SPECL [`x:string`; `yty:type`]) THEN
831 ASM_REWRITE_TAC[] THEN EXPAND_TAC "env'" THEN
832 ASM_REWRITE_TAC[REV_ASSOCD; term_INJ]] THEN
833 DISCH_THEN(X_CHOOSE_THEN `z:string` (X_CHOOSE_THEN `zty:type`
834 (CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC))) THEN
835 EXPAND_TAC "w" THEN REWRITE_TAC[CLASH; IS_RESULT; term_INJ] THEN
836 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
837 [FIRST_X_ASSUM(K ALL_TAC o SPEC `0`) THEN
839 DISJ1_TAC THEN REWRITE_TAC[result_INJ] THEN
840 MAP_EVERY EXISTS_TAC [`z:string`; `zty:type`] THEN
842 ASM_REWRITE_TAC[VFREE_IN; term_INJ] THEN
843 EXPAND_TAC "env'" THEN ASM_REWRITE_TAC[REV_ASSOCD; term_INJ] THEN
846 FIRST_X_ASSUM(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN STRIP_TAC THEN
847 ONCE_REWRITE_TAC[INST_CORE] THEN ASM_REWRITE_TAC[] THEN
848 ONCE_REWRITE_TAC[letlemma] THEN
849 ABBREV_TAC `env'' = CONS (Var x' ty,Var x' ty') env` THEN
850 ONCE_REWRITE_TAC[letlemma] THEN
852 `ures = INST_CORE env'' tyin (VSUBST[Var x' ty,Var x ty] t)` THEN
853 ONCE_REWRITE_TAC[letlemma] THEN
854 FIRST_X_ASSUM(MP_TAC o SPEC `sizeof t`) THEN
855 REWRITE_TAC[sizeof; ARITH_RULE `t < 2 + t`] THEN
857 MP_TAC(SPECL [`VSUBST [Var x' ty,Var x ty] t`;
858 `env'':(term#term)list`; `tyin:(type#type)list`] th) THEN
859 MP_TAC(SPECL [`t:term`; `[]:(term#term)list`; `tyin:(type#type)list`]
861 REWRITE_TAC[MEM; REV_ASSOCD] THEN ASM_REWRITE_TAC[] THEN
862 DISCH_THEN(X_CHOOSE_THEN `t':term` MP_TAC) THEN STRIP_TAC THEN
863 UNDISCH_TAC `VARIANT (RESULT (INST_CORE [] tyin t)) x ty' = x'` THEN
864 ASM_REWRITE_TAC[RESULT] THEN DISCH_TAC THEN
865 MP_TAC(SPECL [`t':term`; `x:string`; `ty':type`] VARIANT) THEN
866 ASM_REWRITE_TAC[] THEN
867 GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
868 [NOT_EXISTS_THM; TAUT `~(a /\ b) <=> a ==> ~b`] THEN DISCH_TAC THEN
870 [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
871 [MATCH_MP_TAC VSUBST_WELLTYPED THEN ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN
872 ASM_MESON_TAC[has_type_RULES];
875 [MATCH_MP_TAC SIZEOF_VSUBST THEN
876 ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN ASM_MESON_TAC[has_type_RULES];
878 EXPAND_TAC "env''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
881 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
882 [DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th) THEN
883 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `v:string` THEN
884 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `vty:type` THEN
885 ASM_REWRITE_TAC[] THEN
886 DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC) THEN
887 ASM_REWRITE_TAC[IS_RESULT; CLASH] THEN
888 ONCE_REWRITE_TAC[letlemma] THEN
889 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
890 [REWRITE_TAC[VFREE_IN_VSUBST] THEN EXPAND_TAC "env''" THEN
891 REWRITE_TAC[REV_ASSOCD] THEN ASM_REWRITE_TAC[] THEN
892 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
893 ASM_REWRITE_TAC[] THEN REWRITE_TAC[term_INJ] THEN
894 DISCH_THEN(REPEAT_TCL CHOOSE_THEN MP_TAC) THEN
895 COND_CASES_TAC THEN ASM_REWRITE_TAC[VFREE_IN; term_INJ] THEN
898 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [term_INJ]) THEN
899 DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
900 MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
901 EXPAND_TAC "env''" THEN REWRITE_TAC[REV_ASSOCD] THEN
902 ASM_CASES_TAC `vty:type = ty` THEN ASM_REWRITE_TAC[] THEN
903 DISCH_THEN(MP_TAC o CONJUNCT1) THEN
904 REWRITE_TAC[VFREE_IN_VSUBST; NOT_EXISTS_THM; REV_ASSOCD] THEN
905 ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN; term_INJ] THEN
906 MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
907 MP_TAC(SPECL [`t':term`; `x:string`; `ty':type`] VARIANT) THEN
908 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
910 ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
911 DISCH_THEN(X_CHOOSE_THEN `t'':term` STRIP_ASSUME_TAC) THEN
912 ASM_REWRITE_TAC[IS_RESULT; result_INJ; UNWIND_THM1; result_DISTINCT] THEN
913 REWRITE_TAC[RESULT] THEN
914 MATCH_MP_TAC(TAUT `b /\ (b ==> c /\ a /\ d) ==> a /\ b /\ c /\ d`) THEN
916 [ASM_REWRITE_TAC[typeof; TYPE_SUBST] THEN
917 MATCH_MP_TAC(last(CONJUNCTS has_type_RULES)) THEN
918 SUBGOAL_THEN `(VSUBST [Var x' ty,Var x ty] t) has_type (typeof t)`
919 (fun th -> ASM_MESON_TAC[th; WELLTYPED_LEMMA]) THEN
920 MATCH_MP_TAC VSUBST_HAS_TYPE THEN ASM_REWRITE_TAC[GSYM WELLTYPED] THEN
921 REWRITE_TAC[MEM; PAIR_EQ] THEN MESON_TAC[has_type_RULES];
923 DISCH_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
925 [ASM_REWRITE_TAC[VFREE_IN] THEN
926 MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
927 ASM_REWRITE_TAC[VFREE_IN_VSUBST; REV_ASSOCD] THEN
928 ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN; term_INJ] THEN
930 REWRITE_TAC[TAUT `x /\ (if p then a /\ b else c /\ b) <=>
931 b /\ x /\ (if p then a else c)`] THEN
932 REWRITE_TAC[UNWIND_THM2] THEN
933 REWRITE_TAC[TAUT `x /\ (if p /\ q then a else b) <=>
934 p /\ q /\ a /\ x \/ b /\ ~(p /\ q) /\ x`] THEN
935 REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM1; UNWIND_THM2] THEN
938 DISCH_TAC THEN CONJ_TAC THENL
939 [MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
940 REWRITE_TAC[VFREE_IN] THEN STRIP_TAC THEN
941 UNDISCH_TAC `!x'' ty'.
942 VFREE_IN (Var x'' ty') (VSUBST [Var x' ty,Var x ty] t)
943 ==> (REV_ASSOCD (Var x'' (TYPE_SUBST tyin ty')) env''
944 (Var x'' ty') = Var x'' ty')` THEN
945 DISCH_THEN(MP_TAC o SPECL [`k:string`; `kty:type`]) THEN
946 REWRITE_TAC[VFREE_IN_VSUBST; REV_ASSOCD] THEN
947 ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN] THEN
948 REWRITE_TAC[VFREE_IN; term_INJ] THEN
950 REWRITE_TAC[TAUT `x /\ (if p then a /\ b else c /\ b) <=>
951 b /\ x /\ (if p then a else c)`] THEN
952 REWRITE_TAC[UNWIND_THM2] THEN
953 REWRITE_TAC[TAUT `x /\ (if p /\ q then a else b) <=>
954 p /\ q /\ a /\ x \/ b /\ ~(p /\ q) /\ x`] THEN
955 REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM1; UNWIND_THM2] THEN
956 UNDISCH_TAC `~(Var x ty = Var k kty)` THEN
957 REWRITE_TAC[term_INJ] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
958 EXPAND_TAC "env''" THEN REWRITE_TAC[REV_ASSOCD] THEN ASM_MESON_TAC[];
960 REPEAT STRIP_TAC THEN REWRITE_TAC[semantics] THEN
961 REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN ASM_REWRITE_TAC[] THEN
962 MATCH_MP_TAC ABSTRACT_EQ THEN
963 CONJ_TAC THENL [ASM_SIMP_TAC[TYPESET_INHABITED]; ALL_TAC] THEN
964 X_GEN_TAC `a:V` THEN REWRITE_TAC[] THEN DISCH_TAC THEN CONJ_TAC THENL
965 [MATCH_MP_TAC SEMANTICS_TYPESET THEN
966 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
967 ASM_MESON_TAC[welltyped; WELLTYPED];
969 MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> a /\ b`) THEN CONJ_TAC THENL
970 [DISCH_THEN(SUBST1_TAC o SYM) THEN
971 MATCH_MP_TAC SEMANTICS_TYPESET THEN
972 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
973 SUBGOAL_THEN `(VSUBST [Var x' ty,Var x ty] t) has_type (typeof t)`
974 (fun th -> ASM_MESON_TAC[th; WELLTYPED_LEMMA]) THEN
975 MATCH_MP_TAC VSUBST_HAS_TYPE THEN ASM_REWRITE_TAC[GSYM WELLTYPED] THEN
976 REWRITE_TAC[MEM; PAIR_EQ] THEN MESON_TAC[has_type_RULES];
978 W(fun (asl,w) -> FIRST_X_ASSUM(fun th ->
979 MP_TAC(PART_MATCH (lhand o rand) th (lhand w)))) THEN
980 ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN DISCH_TAC THEN
981 REWRITE_TAC[GSYM(CONJUNCT1 TYPE_SUBST)] THEN
982 MP_TAC SEMANTICS_VSUBST THEN
983 REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
985 W(fun (asl,w) -> MP_TAC(PART_MATCH (lhand o rand) th (lhand w)))) THEN
987 [ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN CONJ_TAC THENL
988 [MESON_TAC[has_type_RULES]; ALL_TAC] THEN
990 [REWRITE_TAC[type_valuation] THEN ASM_SIMP_TAC[TYPESET_INHABITED];
992 REWRITE_TAC[term_valuation] THEN
993 MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
994 REWRITE_TAC[VALMOD] THEN
995 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
996 REWRITE_TAC[VALMOD; PAIR_EQ] THEN
997 COND_CASES_TAC THEN ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
998 ASM_MESON_TAC[term_valuation];
1000 DISCH_THEN SUBST1_TAC THEN
1001 REWRITE_TAC[GSYM(CONJUNCT1 TYPE_SUBST)] THEN
1002 MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN CONJ_TAC THENL
1003 [REWRITE_TAC[type_valuation] THEN ASM_SIMP_TAC[TYPESET_INHABITED];
1005 REWRITE_TAC[ITLIST] THEN
1006 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
1007 REWRITE_TAC[DEST_VAR] THEN REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
1008 [ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
1009 REWRITE_TAC[term_valuation; semantics] THEN
1010 MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
1011 REWRITE_TAC[VALMOD] THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
1012 REWRITE_TAC[TYPESET_LEMMA; TYPE_SUBST] THEN
1013 SIMP_TAC[PAIR_EQ] THEN ASM_REWRITE_TAC[] THEN
1014 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
1015 ASM_MESON_TAC[term_valuation];
1017 MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN DISCH_TAC THEN
1018 REWRITE_TAC[VALMOD; semantics] THEN
1019 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
1020 SIMP_TAC[PAIR_EQ] THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
1022 (* ------------------------------------------------------------------------- *)
1023 (* So in particular, we get key properties of INST itself. *)
1024 (* ------------------------------------------------------------------------- *)
1026 let SEMANTICS_INST = prove
1029 ==> (INST tyin tm) has_type (TYPE_SUBST tyin (typeof tm)) /\
1030 (!u uty. VFREE_IN (Var u uty) (INST tyin tm) <=>
1031 ?oty. VFREE_IN (Var u oty) tm /\
1032 (uty = TYPE_SUBST tyin oty)) /\
1034 type_valuation tau /\ term_valuation tau sigma
1035 ==> (semantics sigma tau (INST tyin tm) =
1037 (\(x,ty). sigma(x,TYPE_SUBST tyin ty))
1038 (\s. typeset tau (TYPE_SUBST tyin (Tyvar s))) tm)`,
1039 REPEAT GEN_TAC THEN STRIP_TAC THEN
1040 MP_TAC(SPECL [`sizeof tm`; `tm:term`; `[]:(term#term)list`;
1041 `tyin:(type#type)list`] SEMANTICS_INST_CORE) THEN
1042 ASM_REWRITE_TAC[MEM; INST_DEF; REV_ASSOCD] THEN MESON_TAC[RESULT]);;
1044 (* ------------------------------------------------------------------------- *)
1045 (* Hence soundness of the INST_TYPE rule. *)
1046 (* ------------------------------------------------------------------------- *)
1048 let INST_TYPE_correct = prove
1049 (`!tyin asl p. asl |= p ==> MAP (INST tyin) asl |= INST tyin p`,
1050 REWRITE_TAC[sequent] THEN REPEAT STRIP_TAC THENL
1051 [UNDISCH_TAC `ALL (\a. a has_type Bool) (CONS p asl)` THEN
1052 REWRITE_TAC[ALL; ALL_MAP] THEN MATCH_MP_TAC MONO_AND THEN
1055 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
1056 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[o_THM]] THEN
1057 ASM_MESON_TAC[SEMANTICS_INST; TYPE_SUBST; welltyped; WELLTYPED;
1060 SUBGOAL_THEN `welltyped p` ASSUME_TAC THENL
1061 [ASM_MESON_TAC[welltyped; ALL]; ALL_TAC] THEN
1062 ASM_SIMP_TAC[SEMANTICS_INST] THEN
1063 FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL
1064 [REWRITE_TAC[type_valuation] THEN ASM_MESON_TAC[TYPESET_INHABITED];
1067 [REWRITE_TAC[term_valuation] THEN
1068 REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
1069 ASM_MESON_TAC[term_valuation];
1071 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ALL_MAP]) THEN
1072 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
1073 X_GEN_TAC `a:term` THEN DISCH_TAC THEN
1074 SUBGOAL_THEN `welltyped a` MP_TAC THENL
1075 [ASM_MESON_TAC[ALL_MEM; MEM; welltyped]; ALL_TAC] THEN
1076 ASM_SIMP_TAC[SEMANTICS_INST; o_THM]);;
1078 (* ------------------------------------------------------------------------- *)
1080 (* ------------------------------------------------------------------------- *)
1082 let HOL_IS_SOUND = prove
1083 (`!asl p. asl |- p ==> asl |= p`,
1084 MATCH_MP_TAC proves_INDUCT THEN
1085 REWRITE_TAC[REFL_correct; TRANS_correct; ABS_correct;
1086 BETA_correct; ASSUME_correct; EQ_MP_correct; INST_TYPE_correct;
1087 REWRITE_RULE[LET_DEF; LET_END_DEF] DEDUCT_ANTISYM_RULE_correct;
1088 REWRITE_RULE[IMP_IMP] INST_correct] THEN
1089 REPEAT STRIP_TAC THEN MATCH_MP_TAC MK_COMB_correct THEN
1090 ASM_MESON_TAC[WELLTYPED_CLAUSES; MK_COMB_correct]);;
1092 (* ------------------------------------------------------------------------- *)
1094 (* ------------------------------------------------------------------------- *)
1096 let HOL_IS_CONSISTENT = prove
1097 (`?p. p has_type Bool /\ ~([] |- p)`,
1098 SUBGOAL_THEN `?p. p has_type Bool /\ ~([] |= p)`
1099 (fun th -> MESON_TAC[th; HOL_IS_SOUND]) THEN
1100 EXISTS_TAC `Var x Bool === Var (VARIANT (Var x Bool) x Bool) Bool` THEN
1101 SIMP_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_CLAUSES; typeof;
1102 sequent; ALL; SEMANTICS_EQUATION; has_type_RULES; semantics;
1103 BOOLEAN_EQ_TRUE] THEN
1104 MP_TAC(SPECL [`Var x Bool`; `x:string`; `Bool`] VARIANT) THEN
1105 ABBREV_TAC `y = VARIANT (Var x Bool) x Bool` THEN
1106 REWRITE_TAC[VFREE_IN; term_INJ; NOT_FORALL_THM] THEN DISCH_TAC THEN
1107 EXISTS_TAC `((x:string,Bool) |-> false) (((y,Bool) |-> true)
1108 (\(x,ty). @a. a <: typeset (\x. boolset) ty))` THEN
1109 EXISTS_TAC `\x:string. boolset` THEN
1110 ASM_REWRITE_TAC[type_valuation; VALMOD; PAIR_EQ; TRUE_NE_FALSE] THEN
1111 CONJ_TAC THENL [MESON_TAC[IN_BOOL]; ALL_TAC] THEN
1112 REWRITE_TAC[term_valuation] THEN REPEAT GEN_TAC THEN
1113 REWRITE_TAC[VALMOD; PAIR_EQ] THEN
1114 REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[typeset; IN_BOOL]) THEN
1115 CONV_TAC SELECT_CONV THEN MATCH_MP_TAC TYPESET_INHABITED THEN
1116 REWRITE_TAC[type_valuation] THEN MESON_TAC[IN_BOOL]);;