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]);;