colo12-c703.uibk.ac.at Git - Model of HOL/.git/blob - Model/syntax.ml

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