Update from HH
[hl193./.git] / Model / semantics.ml
1 (* ========================================================================= *)
2 (* Formal semantics of HOL inside itself.                                    *)
3 (* ========================================================================= *)
4
5 (* ------------------------------------------------------------------------- *)
6 (* Semantics of types.                                                       *)
7 (* ------------------------------------------------------------------------- *)
8
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))`;;
14
15 (* ------------------------------------------------------------------------- *)
16 (* Semantics of terms.                                                       *)
17 (* ------------------------------------------------------------------------- *)
18
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))`;;
35
36 (* ------------------------------------------------------------------------- *)
37 (* Valid type and term valuations.                                           *)
38 (* ------------------------------------------------------------------------- *)
39
40 let type_valuation = new_definition
41   `type_valuation tau <=> !x. (?y. y <: tau x)`;;
42
43 let term_valuation = new_definition
44   `term_valuation tau sigma <=> !n ty. sigma(n,ty) <: typeset tau ty`;;
45
46 let TERM_VALUATION_VALMOD = prove
47  (`!sigma taut n ty x.
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[]);;
51
52 (* ------------------------------------------------------------------------- *)
53 (* All the typesets are nonempty.                                            *)
54 (* ------------------------------------------------------------------------- *)
55
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
60   CONJ_TAC THENL
61    [ASM_MESON_TAC[type_valuation];
62     ASM_MESON_TAC[BOOLEAN_IN_BOOLSET; INDSET_INHABITED; FUNSPACE_INHABITED]]);;
63
64 (* ------------------------------------------------------------------------- *)
65 (* Semantics maps into the right place.                                      *)
66 (* ------------------------------------------------------------------------- *)
67
68 let SEMANTICS_TYPESET_INDUCT = prove
69  (`!tm ty. tm has_type ty
70            ==> 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]]);;
88
89 let SEMANTICS_TYPESET = prove
90  (`!sigma tau tm ty.
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]);;
94
95 (* ------------------------------------------------------------------------- *)
96 (* Semantics of equations.                                                   *)
97 (* ------------------------------------------------------------------------- *)
98
99 let SEMANTICS_EQUATION = prove
100  (`!sigma tau s t.
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]);;
108
109 let SEMANTICS_EQUATION_ALT = prove
110  (`!sigma tau s t.
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]);;
121
122 (* ------------------------------------------------------------------------- *)
123 (* Quick sanity check.                                                       *)
124 (* ------------------------------------------------------------------------- *)
125
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
134   W(fun (asl,w) ->
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
138   ANTS_TAC THENL
139    [CONJ_TAC THENL
140      [ASM_MESON_TAC[SEMANTICS_TYPESET; typeset];
141       REWRITE_TAC[SUCHTHAT] THEN
142       ASM_MESON_TAC[ch; SUCHTHAT; TYPESET_INHABITED]];
143     ALL_TAC] THEN
144   DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[]);;
145
146 (* ------------------------------------------------------------------------- *)
147 (* Semantics of a sequent.                                                   *)
148 (* ------------------------------------------------------------------------- *)
149
150 parse_as_infix("|=",(11,"right"));;
151
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)`;;
158
159 (* ------------------------------------------------------------------------- *)
160 (* Invariance of semantics under alpha-conversion.                           *)
161 (* ------------------------------------------------------------------------- *)
162
163 let SEMANTICS_RACONV = prove
164  (`!env tp.
165         RACONV env tp
166         ==> !sigma1 sigma2 tau.
167                 type_valuation tau /\
168                 term_valuation tau sigma1 /\ term_valuation tau sigma2 /\
169                 (!x1 ty1 x2 ty2.
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
178    [ASM_MESON_TAC[];
179     BINOP_TAC THEN ASM_MESON_TAC[];
180     ALL_TAC] THEN
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];
188     ALL_TAC] THEN
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
194   ASM_MESON_TAC[]);;
195
196 let SEMANTICS_ACONV = prove
197  (`!sigma tau s t.
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]);;
206
207 (* ------------------------------------------------------------------------- *)
208 (* General semantic lemma about binary inference rules.                      *)
209 (* ------------------------------------------------------------------------- *)
210
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`]
231     TERM_UNION_THM) THEN
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]);;
235
236 (* ------------------------------------------------------------------------- *)
237 (* Semantics only depends on valuations of free variables.                   *)
238 (* ------------------------------------------------------------------------- *)
239
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 /\
244         welltyped t /\
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
251    [ASM_MESON_TAC[];
252     BINOP_TAC THEN ASM_MESON_TAC[WELLTYPED_CLAUSES];
253     ALL_TAC] THEN
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;
257                   SEMANTICS_TYPESET];
258     ALL_TAC]) THEN
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[]);;
263
264 (* ------------------------------------------------------------------------- *)
265 (* Prove some inference rules correct.                                       *)
266 (* ------------------------------------------------------------------------- *)
267
268 let ASSUME_correct = prove
269  (`!p. p has_type Bool ==> [p] |= p`,
270   SIMP_TAC[sequent; ALL]);;
271
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]);;
276
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]]);;
288
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
300     MESON_TAC[codomain];
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]]);;
304
305 let EQ_MP_correct = prove
306  (`!asl1 asl2 p q p'.
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;
314                   ACONV_TYPE];
315     ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; IMP_CONJ; boolean] THEN
316     ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL; TRUE_NE_FALSE; SEMANTICS_ACONV;
317                   welltyped]]);;
318
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[];
325     ALL_TAC] THEN
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]);;
334
335 let ABS_correct = prove
336  (`!asl x ty l r.
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
341   CONJ_TAC THENL
342    [UNDISCH_TAC `(l === r) has_type Bool` THEN
343     SIMP_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_CLAUSES; typeof];
344     ALL_TAC] THEN
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];
354     ALL_TAC]) THEN
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[]);;
371
372 let DEDUCT_ANTISYM_RULE_correct = prove
373  (`!asl1 asl2 p q.
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`,
378   REPEAT GEN_TAC THEN
379   REWRITE_TAC[sequent; o_DEF; LET_DEF; LET_END_DEF; GSYM CONJ_ASSOC] THEN
380   MATCH_MP_TAC(TAUT `
381     (a1 /\ b1 ==> c1) /\ (a1 /\ b1 /\ c1 ==> a2 /\ b2 ==> c2)
382     ==> a1 /\ a2 /\ b1 /\ b2 ==> c1 /\ c2`) THEN
383   CONJ_TAC THENL
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];
387     ALL_TAC] THEN
388   REWRITE_TAC[ALL; AND_FORALL_THM] THEN REWRITE_TAC[GSYM ALL_MEM] THEN
389   STRIP_TAC 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
402   (SUBGOAL_THEN
403     `MEM a (FILTER (\x. ~ACONV c2 x) asl1) \/
404      MEM a (FILTER (\x. ~ACONV c1 x) asl2)`
405    MP_TAC THENL
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]));;
409
410 (* ------------------------------------------------------------------------- *)
411 (* Correct semantics for term substitution.                                  *)
412 (* ------------------------------------------------------------------------- *)
413
414 let DEST_VAR = new_recursive_definition term_RECURSION
415  `DEST_VAR (Var x ty) = (x,ty)`;;
416
417 let TERM_VALUATION_ITLIST = prove
418  (`!ilist sigma tau.
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]);;
431
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[]);;
460
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[]);;
468
469 let SEMANTICS_VSUBST = prove
470  (`!tm sigma tau ilist.
471        welltyped tm /\
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) =
475                             semantics
476                              (ITLIST
477                                 (\(t,x). DEST_VAR x |-> semantics sigma tau t)
478                                 ilist sigma)
479                              tau tm)`,
480   MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VSUBST; semantics] THEN
481   CONJ_TAC THENL
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
489     DISCH_THEN(fun th ->
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[];
497     ALL_TAC] THEN
498   CONJ_TAC THENL
499    [REWRITE_TAC[WELLTYPED_CLAUSES] THEN REPEAT STRIP_TAC THEN
500     BINOP_TAC THEN ASM_MESON_TAC[];
501     ALL_TAC] THEN
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
506   SUBGOAL_THEN
507    `!s s'. MEM (s',s) ilist' ==> (?x ty. (s = Var x ty) /\ s' has_type ty)`
508   ASSUME_TAC THENL
509    [EXPAND_TAC "ilist'" THEN ASM_SIMP_TAC[MEM_FILTER]; ALL_TAC] THEN
510   COND_CASES_TAC THENL
511    [REPEAT LET_TAC THEN
512     SUBGOAL_THEN
513      `!s s'. MEM (s',s) ilist'' ==> (?x ty. (s = Var x ty) /\ s' has_type ty)`
514     ASSUME_TAC THENL
515      [EXPAND_TAC "ilist''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
516       ASM_MESON_TAC[has_type_RULES];
517       ALL_TAC];
518     ALL_TAC] THEN
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
524   EXPAND_TAC "t'" 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];
533     ALL_TAC] THEN
534   EXPAND_TAC "ilist'" THEN ASM_SIMP_TAC[ITLIST_VALMOD_FILTER] THEN
535   REWRITE_TAC[VALMOD] THENL
536    [ALL_TAC;
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
569   SUBGOAL_THEN
570    `REV_ASSOCD (Var u uty) ilist' (Var u uty) =
571     REV_ASSOCD (Var u uty) ilist (Var u uty)`
572   SUBST1_TAC THENL
573    [EXPAND_TAC "ilist'" THEN REWRITE_TAC[REV_ASSOCD_FILTER] THEN
574     ASM_REWRITE_TAC[term_INJ];
575     ALL_TAC] THEN
576   UNDISCH_TAC
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
588   DISCH_THEN(fun th ->
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]);;
600
601 (* ------------------------------------------------------------------------- *)
602 (* Hence correctness of INST.                                                *)
603 (* ------------------------------------------------------------------------- *)
604
605 let INST_correct = prove
606  (`!ilist asl p.
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
612     CONJ_TAC THENL
613      [ALL_TAC;
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[];
617     ALL_TAC] THEN
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]);;
629
630 (* ------------------------------------------------------------------------- *)
631 (* Lemma about typesets to simplify some later goals.                        *)
632 (* ------------------------------------------------------------------------- *)
633
634 let TYPESET_LEMMA = prove
635  (`!ty tau tyin.
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]);;
639
640 (* ------------------------------------------------------------------------- *)
641 (* Semantics of type instantiation core.                                     *)
642 (* ------------------------------------------------------------------------- *)
643
644 let SEMANTICS_INST_CORE = prove
645  (`!n tm env tyin.
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)) /\
663                    !sigma tau.
664                        type_valuation tau /\ term_valuation tau sigma
665                        ==> (semantics sigma tau tm' =
666                             semantics
667                                (\(x,ty). sigma(x,TYPE_SUBST tyin ty))
668                                (\s. typeset tau (TYPE_SUBST tyin (Tyvar s)))
669                                tm))`,
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];
708       ALL_TAC] THEN
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];
716       ALL_TAC] THEN
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[];
726     ALL_TAC] THEN
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
737   ANTS_TAC THENL
738    [EXPAND_TAC "env'" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN ASM_MESON_TAC[];
739     ALL_TAC] THEN
740   DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
741    [ALL_TAC;
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[];
753       ALL_TAC] THEN
754     REWRITE_TAC[result_INJ; UNWIND_THM1; RESULT] THEN
755     MATCH_MP_TAC(TAUT `a /\ b /\ (b ==> c) ==> b /\ a /\ c`) THEN
756     CONJ_TAC THENL
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];
773       ALL_TAC] THEN
774     CONJ_TAC THENL
775      [REWRITE_TAC[typeof; TYPE_SUBST] THEN ASM_REWRITE_TAC[] THEN
776       ASM_MESON_TAC[has_type_RULES];
777       ALL_TAC] THEN
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];
787       ALL_TAC] THEN
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];
792       ALL_TAC] THEN
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];
799       ALL_TAC] THEN
800     CONJ_TAC THENL
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];
807       ALL_TAC] THEN
808     CONJ_TAC THENL
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];
816       ALL_TAC] THEN
817     UNDISCH_THEN
818      `!u uty.
819          VFREE_IN (Var u uty) t' <=>
820          (?oty. VFREE_IN (Var u oty) t /\ (uty = TYPE_SUBST tyin oty))`
821      (K ALL_TAC) THEN
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
838     DISCH_THEN(fun th ->
839       DISJ1_TAC THEN REWRITE_TAC[result_INJ] THEN
840       MAP_EVERY EXISTS_TAC [`z:string`; `zty:type`] THEN
841       MP_TAC th) THEN
842     ASM_REWRITE_TAC[VFREE_IN; term_INJ] THEN
843     EXPAND_TAC "env'" THEN ASM_REWRITE_TAC[REV_ASSOCD; term_INJ] THEN
844     ASM_MESON_TAC[];
845     ALL_TAC] 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
851   ABBREV_TAC
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
856   DISCH_THEN(fun th ->
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`]
860        th)) THEN
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
869   ANTS_TAC THENL
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];
873       ALL_TAC] THEN
874     CONJ_TAC THENL
875      [MATCH_MP_TAC SIZEOF_VSUBST THEN
876       ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN ASM_MESON_TAC[has_type_RULES];
877       ALL_TAC] THEN
878     EXPAND_TAC "env''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
879     ASM_MESON_TAC[];
880     ALL_TAC] 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
896       ASM_MESON_TAC[];
897       ALL_TAC] 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[];
909     ALL_TAC] THEN
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
915   CONJ_TAC THENL
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];
922     ALL_TAC] THEN
923   DISCH_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
924   CONJ_TAC THENL
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
929     SIMP_TAC[] 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
936     ASM_MESON_TAC[];
937     ALL_TAC] 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
949     SIMP_TAC[] 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[];
959     ALL_TAC] THEN
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];
968     ALL_TAC] THEN
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];
977     ALL_TAC] THEN
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
984   DISCH_THEN(fun th ->
985    W(fun (asl,w) -> MP_TAC(PART_MATCH (lhand o rand) th (lhand w)))) THEN
986   ANTS_TAC THENL
987    [ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN CONJ_TAC THENL
988      [MESON_TAC[has_type_RULES]; ALL_TAC] THEN
989     CONJ_TAC THENL
990      [REWRITE_TAC[type_valuation] THEN ASM_SIMP_TAC[TYPESET_INHABITED];
991       ALL_TAC] THEN
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];
999     ALL_TAC] THEN
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];
1004     ALL_TAC] THEN
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];
1016     ALL_TAC] THEN
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[]);;
1021
1022 (* ------------------------------------------------------------------------- *)
1023 (* So in particular, we get key properties of INST itself.                   *)
1024 (* ------------------------------------------------------------------------- *)
1025
1026 let SEMANTICS_INST = prove
1027  (`!tyin tm.
1028         welltyped tm
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)) /\
1033             !sigma tau.
1034                 type_valuation tau /\ term_valuation tau sigma
1035                 ==> (semantics sigma tau (INST tyin tm) =
1036                      semantics
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]);;
1043
1044 (* ------------------------------------------------------------------------- *)
1045 (* Hence soundness of the INST_TYPE rule.                                    *)
1046 (* ------------------------------------------------------------------------- *)
1047
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
1053     CONJ_TAC THENL
1054      [ALL_TAC;
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;
1058                     WELLTYPED_LEMMA];
1059     ALL_TAC] THEN
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];
1065     ALL_TAC] THEN
1066   CONJ_TAC THENL
1067    [REWRITE_TAC[term_valuation] THEN
1068     REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
1069     ASM_MESON_TAC[term_valuation];
1070     ALL_TAC] THEN
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]);;
1077
1078 (* ------------------------------------------------------------------------- *)
1079 (* Soundness.                                                                *)
1080 (* ------------------------------------------------------------------------- *)
1081
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]);;
1091
1092 (* ------------------------------------------------------------------------- *)
1093 (* Consistency.                                                              *)
1094 (* ------------------------------------------------------------------------- *)
1095
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]);;