--- /dev/null
+(* ========================================================================= *)
+(* Set-theoretic hierarchy for modelling HOL inside itself. *)
+(* ========================================================================= *)
+
+let INJ_LEMMA = prove
+ (`(!x y. (f x = f y) ==> (x = y)) <=> (!x y. (f x = f y) <=> (x = y))`,
+ MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Useful to have a niceish "function update" notation. *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("|->",(12,"right"));;
+
+let valmod = new_definition
+ `(x |-> a) (v:A->B) = \y. if y = x then a else v(y)`;;
+
+let VALMOD = prove
+ (`!v x y a. ((x |-> y) v) a = if a = x then y else v(a)`,
+ REWRITE_TAC[valmod]);;
+
+let VALMOD_BASIC = prove
+ (`!v x y. (x |-> y) v x = y`,
+ REWRITE_TAC[valmod]);;
+
+let VALMOD_VALMOD_BASIC = prove
+ (`!v a b x. (x |-> a) ((x |-> b) v) = (x |-> a) v`,
+ REWRITE_TAC[valmod; FUN_EQ_THM] THEN
+ REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
+
+let VALMOD_REPEAT = prove
+ (`!v x. (x |-> v(x)) v = v`,
+ REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
+
+let FORALL_VALMOD = prove
+ (`!x. (!v a. P((x |-> a) v)) = (!v. P v)`,
+ MESON_TAC[VALMOD_REPEAT]);;
+
+let VALMOD_SWAP = prove
+ (`!v x y a b.
+ ~(x = y) ==> ((x |-> a) ((y |-> b) v) = (y |-> b) ((x |-> a) v))`,
+ REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* A dummy finite type inadequately modelling ":ind". *)
+(* ------------------------------------------------------------------------- *)
+
+let ind_model_tybij_th =
+ prove(`?x. x IN @s:num->bool. ~(s = {}) /\ FINITE s`,
+ MESON_TAC[MEMBER_NOT_EMPTY; IN_SING; FINITE_RULES]);;
+
+let ind_model_tybij =
+ new_type_definition "ind_model" ("mk_ind","dest_ind") ind_model_tybij_th;;
+
+(* ------------------------------------------------------------------------- *)
+(* Introduce a type whose universe is "inaccessible" starting from *)
+(* "ind_model". Since "ind_model" is finite, we can just use any *)
+(* infinite set. In order to make "ind_model" infinite, we would need *)
+(* a new axiom. In order to keep things generic we try to deduce *)
+(* everything from this one uniform "axiom". Note that even in the *)
+(* infinite case, this can still be a small set in ZF terms, not a real *)
+(* inaccessible cardinal. *)
+(* ------------------------------------------------------------------------- *)
+
+(****** Here's what we'd do in the infinite case
+
+ new_type("I",0);;
+
+ let I_AXIOM = new_axiom
+ `UNIV:ind_model->bool <_c UNIV:I->bool /\
+ (!s:A->bool. s <_c UNIV:I->bool ==> {t | t SUBSET s} <_c UNIV:I->bool)`;;
+
+ *******)
+
+let inacc_tybij_th = prove
+ (`?x:num. x IN UNIV`,REWRITE_TAC[IN_UNIV]);;
+
+let inacc_tybij =
+ new_type_definition "I" ("mk_I","dest_I") inacc_tybij_th;;
+
+let I_AXIOM = prove
+ (`UNIV:ind_model->bool <_c UNIV:I->bool /\
+ (!s:A->bool. s <_c UNIV:I->bool ==> {t | t SUBSET s} <_c UNIV:I->bool)`,
+ let lemma = prove
+ (`!s. s <_c UNIV:I->bool <=> FINITE s`,
+ GEN_TAC THEN REWRITE_TAC[FINITE_CARD_LT] THEN
+ MATCH_MP_TAC CARD_LT_CONG THEN REWRITE_TAC[CARD_EQ_REFL] THEN
+ REWRITE_TAC[GSYM CARD_LE_ANTISYM; le_c; IN_UNIV] THEN
+ MESON_TAC[inacc_tybij; IN_UNIV]) in
+ REWRITE_TAC[lemma; FINITE_POWERSET] THEN
+ SUBGOAL_THEN `UNIV = IMAGE mk_ind (@s. ~(s = {}) /\ FINITE s)`
+ SUBST1_TAC THENL
+ [MESON_TAC[EXTENSION; IN_IMAGE; IN_UNIV; ind_model_tybij];
+ MESON_TAC[FINITE_IMAGE; NOT_INSERT_EMPTY; FINITE_RULES]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* I is infinite and therefore admits an injective pairing. *)
+(* ------------------------------------------------------------------------- *)
+
+let I_INFINITE = prove
+ (`INFINITE(UNIV:I->bool)`,
+ REWRITE_TAC[INFINITE] THEN DISCH_TAC THEN
+ MP_TAC(ISPEC `{n | n < CARD(UNIV:I->bool) - 1}` (CONJUNCT2 I_AXIOM)) THEN
+ ASM_SIMP_TAC[CARD_LT_CARD; FINITE_NUMSEG_LT; FINITE_POWERSET] THEN
+ SIMP_TAC[CARD_NUMSEG_LT; CARD_POWERSET; FINITE_NUMSEG_LT] THEN
+ SUBGOAL_THEN `~(CARD(UNIV:I->bool) = 0)` MP_TAC THENL
+ [ASM_SIMP_TAC[CARD_EQ_0; GSYM MEMBER_NOT_EMPTY; IN_UNIV]; ALL_TAC] THEN
+ SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 1 < n`; NOT_LT] THEN
+ MATCH_MP_TAC(ARITH_RULE `a - 1 < b ==> ~(a = 0) ==> a <= b`) THEN
+ SPEC_TAC(`CARD(UNIV:I->bool) - 1`,`n:num`) THEN POP_ASSUM(K ALL_TAC) THEN
+ INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH] THEN POP_ASSUM MP_TAC THEN
+ ARITH_TAC);;
+
+let I_PAIR_EXISTS = prove
+ (`?f:I#I->I. !x y. (f x = f y) ==> (x = y)`,
+ SUBGOAL_THEN `UNIV:I#I->bool <=_c UNIV:I->bool` MP_TAC THENL
+ [ALL_TAC; REWRITE_TAC[le_c; IN_UNIV]] THEN
+ MATCH_MP_TAC CARD_EQ_IMP_LE THEN
+ MP_TAC(MATCH_MP CARD_SQUARE_INFINITE I_INFINITE) THEN
+ MATCH_MP_TAC(TAUT `(a = b) ==> a ==> b`) THEN
+ AP_THM_TAC THEN AP_TERM_TAC THEN
+ REWRITE_TAC[EXTENSION; mul_c; IN_ELIM_THM; IN_UNIV] THEN MESON_TAC[PAIR]);;
+
+let I_PAIR = REWRITE_RULE[INJ_LEMMA]
+ (new_specification ["I_PAIR"] I_PAIR_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* It also admits injections from "bool" and "ind_model". *)
+(* ------------------------------------------------------------------------- *)
+
+let CARD_BOOL_LT_I = prove
+ (`UNIV:bool->bool <_c UNIV:I->bool`,
+ REWRITE_TAC[GSYM CARD_NOT_LE] THEN
+ DISCH_TAC THEN MP_TAC I_INFINITE THEN REWRITE_TAC[INFINITE] THEN
+ SUBGOAL_THEN `FINITE(UNIV:bool->bool)`
+ (fun th -> ASM_MESON_TAC[th; CARD_LE_FINITE]) THEN
+ SUBGOAL_THEN `UNIV:bool->bool = {F,T}` SUBST1_TAC THENL
+ [REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT] THEN MESON_TAC[];
+ SIMP_TAC[FINITE_RULES]]);;
+
+let I_BOOL_EXISTS = prove
+ (`?f:bool->I. !x y. (f x = f y) ==> (x = y)`,
+ MP_TAC(MATCH_MP CARD_LT_IMP_LE CARD_BOOL_LT_I) THEN
+ SIMP_TAC[lt_c; le_c; IN_UNIV]);;
+
+let I_BOOL = REWRITE_RULE[INJ_LEMMA]
+ (new_specification ["I_BOOL"] I_BOOL_EXISTS);;
+
+let I_IND_EXISTS = prove
+ (`?f:ind_model->I. !x y. (f x = f y) ==> (x = y)`,
+ MP_TAC(CONJUNCT1 I_AXIOM) THEN SIMP_TAC[lt_c; le_c; IN_UNIV]);;
+
+let I_IND = REWRITE_RULE[INJ_LEMMA]
+ (new_specification ["I_IND"] I_IND_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* And the injection from powerset of any accessible set. *)
+(* ------------------------------------------------------------------------- *)
+
+let I_SET_EXISTS = prove
+ (`!s:I->bool.
+ s <_c UNIV:I->bool
+ ==> ?f:(I->bool)->I. !t u. t SUBSET s /\ u SUBSET s /\ (f t = f u)
+ ==> (t = u)`,
+ GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP(CONJUNCT2 I_AXIOM)) THEN
+ DISCH_THEN(MP_TAC o MATCH_MP CARD_LT_IMP_LE) THEN
+ REWRITE_TAC[le_c; IN_UNIV; IN_ELIM_THM]);;
+
+let I_SET = new_specification ["I_SET"]
+ (REWRITE_RULE[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] I_SET_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* Define a type for "levels" of our set theory. *)
+(* ------------------------------------------------------------------------- *)
+
+let setlevel_INDUCT,setlevel_RECURSION = define_type
+ "setlevel = Ur_bool
+ | Ur_ind
+ | Powerset setlevel
+ | Cartprod setlevel setlevel";;
+
+let setlevel_DISTINCT = distinctness "setlevel";;
+let setlevel_INJ = injectivity "setlevel";;
+
+(* ------------------------------------------------------------------------- *)
+(* Now define a subset of I corresponding to each. *)
+(* ------------------------------------------------------------------------- *)
+
+let setlevel = new_recursive_definition setlevel_RECURSION
+ `(setlevel Ur_bool = IMAGE I_BOOL UNIV) /\
+ (setlevel Ur_ind = IMAGE I_IND UNIV) /\
+ (setlevel (Cartprod l1 l2) =
+ IMAGE I_PAIR {x,y | x IN setlevel l1 /\ y IN setlevel l2}) /\
+ (setlevel (Powerset l) = IMAGE (I_SET (setlevel l))
+ {s | s SUBSET (setlevel l)})`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Show they all satisfy the cardinal limits. *)
+(* ------------------------------------------------------------------------- *)
+
+let SETLEVEL_CARD = prove
+ (`!l. setlevel l <_c UNIV:I->bool`,
+ MATCH_MP_TAC setlevel_INDUCT THEN REWRITE_TAC[setlevel] THEN
+ REPEAT CONJ_TAC THENL
+ [TRANS_TAC CARD_LET_TRANS `UNIV:bool->bool` THEN
+ REWRITE_TAC[CARD_LE_IMAGE; CARD_BOOL_LT_I];
+ TRANS_TAC CARD_LET_TRANS `UNIV:ind_model->bool` THEN
+ REWRITE_TAC[CARD_LE_IMAGE; I_AXIOM];
+ X_GEN_TAC `l:setlevel` THEN DISCH_TAC THEN
+ TRANS_TAC CARD_LET_TRANS `{s | s SUBSET (setlevel l)}` THEN
+ ASM_SIMP_TAC[I_AXIOM; CARD_LE_IMAGE];
+ ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`l1:setlevel`; `l2:setlevel`] THEN STRIP_TAC THEN
+ TRANS_TAC CARD_LET_TRANS `setlevel l1 *_c setlevel l2` THEN
+ ASM_SIMP_TAC[CARD_MUL_LT_INFINITE; I_INFINITE; GSYM mul_c; CARD_LE_IMAGE]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Hence the injectivity of the mapping from powerset. *)
+(* ------------------------------------------------------------------------- *)
+
+let I_SET_SETLEVEL = prove
+ (`!l s t. s SUBSET setlevel l /\ t SUBSET setlevel l /\
+ (I_SET (setlevel l) s = I_SET (setlevel l) t)
+ ==> (s = t)`,
+ MESON_TAC[SETLEVEL_CARD; I_SET]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Now our universe of sets and (ur)elements. *)
+(* ------------------------------------------------------------------------- *)
+
+let universe = new_definition
+ `universe = {(t,x) | x IN setlevel t}`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Define an actual type V. *)
+(* *)
+(* This satisfies a suitable number of the ZF axioms. It isn't extensional *)
+(* but we could then construct a quotient structure if desired. Anyway it's *)
+(* only empty sets that aren't. A more significant difference is that we *)
+(* have urelements and the hierarchy levels are all distinct rather than *)
+(* being cumulative. *)
+(* ------------------------------------------------------------------------- *)
+
+let v_tybij_th = prove
+ (`?a. a IN universe`,
+ EXISTS_TAC `Ur_bool,I_BOOL T` THEN
+ REWRITE_TAC[universe; IN_ELIM_THM; PAIR_EQ; CONJ_ASSOC;
+ ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1;
+ setlevel; IN_IMAGE; IN_UNIV] THEN
+ MESON_TAC[]);;
+
+let v_tybij =
+ new_type_definition "V" ("mk_V","dest_V") v_tybij_th;;
+
+let V_TYBIJ = prove
+ (`!l e. e IN setlevel l <=> (dest_V(mk_V(l,e)) = (l,e))`,
+ REWRITE_TAC[GSYM(CONJUNCT2 v_tybij)] THEN
+ REWRITE_TAC[IN_ELIM_THM; universe; FORALL_PAIR_THM; PAIR_EQ] THEN
+ MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Drop a level; test if something is a set. *)
+(* ------------------------------------------------------------------------- *)
+
+let droplevel = new_recursive_definition setlevel_RECURSION
+ `droplevel(Powerset l) = l`;;
+
+let isasetlevel = new_recursive_definition setlevel_RECURSION
+ `(isasetlevel Ur_bool = F) /\
+ (isasetlevel Ur_ind = F) /\
+ (isasetlevel (Cartprod l1 l2) = F) /\
+ (isasetlevel (Powerset l) = T)`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Define some useful inversions. *)
+(* ------------------------------------------------------------------------- *)
+
+let level = new_definition
+ `level x = FST(dest_V x)`;;
+
+let element = new_definition
+ `element x = SND(dest_V x)`;;
+
+let ELEMENT_IN_LEVEL = prove
+ (`!x. (element x) IN setlevel(level x)`,
+ REWRITE_TAC[V_TYBIJ; v_tybij; level; element; PAIR]);;
+
+let SET = prove
+ (`!x. mk_V(level x,element x) = x`,
+ REWRITE_TAC[level; element; PAIR; v_tybij]);;
+
+let set = new_definition
+ `set x = @s. s SUBSET (setlevel(droplevel(level x))) /\
+ (I_SET (setlevel(droplevel(level x))) s = element x)`;;
+
+let isaset = new_definition
+ `isaset x <=> ?l. level x = Powerset l`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Now all the critical relations. *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("<:",(11,"right"));;
+
+let inset = new_definition
+ `x <: s <=> (level s = Powerset(level x)) /\ (element x) IN (set s)`;;
+
+parse_as_infix("<=:",(12,"right"));;
+
+let subset_def = new_definition
+ `s <=: t <=> (level s = level t) /\ !x. x <: s ==> x <: t`;;
+
+(* ------------------------------------------------------------------------- *)
+(* If something has members, it's a set. *)
+(* ------------------------------------------------------------------------- *)
+
+let MEMBERS_ISASET = prove
+ (`!x s. x <: s ==> isaset s`,
+ REWRITE_TAC[inset; isaset] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Each level is nonempty. *)
+(* ------------------------------------------------------------------------- *)
+
+let LEVEL_NONEMPTY = prove
+ (`!l. ?x. x IN setlevel l`,
+ REWRITE_TAC[MEMBER_NOT_EMPTY] THEN
+ MATCH_MP_TAC setlevel_INDUCT THEN REWRITE_TAC[setlevel; IMAGE_EQ_EMPTY] THEN
+ REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_UNIV] THEN
+ REWRITE_TAC[EXISTS_PAIR_THM; IN_ELIM_THM] THEN
+ MESON_TAC[EMPTY_SUBSET]);;
+
+let LEVEL_SET_EXISTS = prove
+ (`!l. ?s. level s = l`,
+ MP_TAC LEVEL_NONEMPTY THEN MATCH_MP_TAC MONO_FORALL THEN
+ REWRITE_TAC[level] THEN MESON_TAC[FST; PAIR; V_TYBIJ]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Empty sets (or non-sets, of course) exist at all set levels. *)
+(* ------------------------------------------------------------------------- *)
+
+let MK_V_CLAUSES = prove
+ (`e IN setlevel l
+ ==> (level(mk_V(l,e)) = l) /\ (element(mk_V(l,e)) = e)`,
+ REWRITE_TAC[level; element; PAIR; GSYM PAIR_EQ; V_TYBIJ]);;
+
+let MK_V_SET = prove
+ (`s SUBSET setlevel l
+ ==> (set(mk_V(Powerset l,I_SET (setlevel l) s)) = s) /\
+ (level(mk_V(Powerset l,I_SET (setlevel l) s)) = Powerset l) /\
+ (element(mk_V(Powerset l,I_SET (setlevel l) s)) = I_SET (setlevel l) s)`,
+ REPEAT GEN_TAC THEN DISCH_TAC THEN
+ SUBGOAL_THEN `I_SET (setlevel l) s IN setlevel(Powerset l)` ASSUME_TAC THENL
+ [REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ ASM_SIMP_TAC[MK_V_CLAUSES; set] THEN
+ SUBGOAL_THEN `I_SET (setlevel l) s IN setlevel(Powerset l)` ASSUME_TAC THENL
+ [REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ ASM_SIMP_TAC[MK_V_CLAUSES; droplevel] THEN
+ MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[] THEN
+ ASM_MESON_TAC[I_SET_SETLEVEL]);;
+
+let EMPTY_EXISTS = prove
+ (`!l. ?s. (level s = l) /\ !x. ~(x <: s)`,
+ MATCH_MP_TAC setlevel_INDUCT THEN
+ REPEAT CONJ_TAC THENL
+ [ALL_TAC; ALL_TAC;
+ X_GEN_TAC `l:setlevel` THEN DISCH_THEN(K ALL_TAC) THEN
+ EXISTS_TAC `mk_V(Powerset l,I_SET (setlevel l) {})` THEN
+ SIMP_TAC[inset; MK_V_CLAUSES; MK_V_SET; EMPTY_SUBSET; NOT_IN_EMPTY];
+ ALL_TAC] THEN
+ MESON_TAC[LEVEL_SET_EXISTS; MEMBERS_ISASET; isaset;
+ setlevel_DISTINCT]);;
+
+let EMPTY_SET = new_specification ["emptyset"]
+ (REWRITE_RULE[SKOLEM_THM] EMPTY_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* Comprehension principle, with no change of levels. *)
+(* ------------------------------------------------------------------------- *)
+
+let COMPREHENSION_EXISTS = prove
+ (`!s p. ?t. (level t = level s) /\ !x. x <: t <=> x <: s /\ p x`,
+ REPEAT GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
+ [ALL_TAC; ASM_MESON_TAC[MEMBERS_ISASET]] THEN
+ POP_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
+ MP_TAC(SPEC `s:V` ELEMENT_IN_LEVEL) THEN
+ ASM_REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN
+ DISCH_THEN(X_CHOOSE_THEN `u:I->bool` STRIP_ASSUME_TAC) THEN
+ EXISTS_TAC `mk_V(Powerset l,
+ I_SET(setlevel l)
+ {i | i IN u /\ p(mk_V(l,i))})` THEN
+ SUBGOAL_THEN `{i | i IN u /\ p (mk_V (l,i))} SUBSET (setlevel l)`
+ ASSUME_TAC THENL
+ [REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[SUBSET];
+ ALL_TAC] THEN
+ ASM_SIMP_TAC[MK_V_SET; inset] THEN X_GEN_TAC `x:V` THEN
+ REWRITE_TAC[setlevel_INJ] THEN
+ REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[SET; MK_V_SET]);;
+
+parse_as_infix("suchthat",(21,"left"));;
+
+let SUCHTHAT = new_specification ["suchthat"]
+ (REWRITE_RULE[SKOLEM_THM] COMPREHENSION_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* Each setlevel exists as a set. *)
+(* ------------------------------------------------------------------------- *)
+
+let SETLEVEL_EXISTS = prove
+ (`!l. ?s. (level s = Powerset l) /\
+ !x. x <: s <=> (level x = l) /\ element(x) IN setlevel l`,
+ GEN_TAC THEN
+ EXISTS_TAC `mk_V(Powerset l,I_SET (setlevel l) (setlevel l))` THEN
+ SIMP_TAC[MK_V_SET; SUBSET_REFL; inset; setlevel_INJ] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Conversely, set(s) belongs in the appropriate level. *)
+(* ------------------------------------------------------------------------- *)
+
+let SET_DECOMP = prove
+ (`!s. isaset s
+ ==> (set s) SUBSET (setlevel(droplevel(level s))) /\
+ (I_SET (setlevel(droplevel(level s))) (set s) = element s)`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[isaset] THEN
+ DISCH_THEN(X_CHOOSE_TAC `l:setlevel`) THEN
+ REWRITE_TAC[set] THEN CONV_TAC SELECT_CONV THEN
+ ASM_REWRITE_TAC[setlevel; droplevel] THEN
+ MP_TAC(SPEC `s:V` ELEMENT_IN_LEVEL) THEN
+ ASM_REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN
+ MESON_TAC[]);;
+
+let SET_SUBSET_SETLEVEL = prove
+ (`!s. isaset s ==> set(s) SUBSET setlevel(droplevel(level s))`,
+ MESON_TAC[SET_DECOMP]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Power set exists. *)
+(* ------------------------------------------------------------------------- *)
+
+let POWERSET_EXISTS = prove
+ (`!s. ?t. (level t = Powerset(level s)) /\ !x. x <: t <=> x <=: s`,
+ GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
+ [FIRST_ASSUM(MP_TAC o GSYM o MATCH_MP SET_DECOMP) THEN
+ FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [isaset]) THEN
+ DISCH_THEN(X_CHOOSE_THEN `l:setlevel` STRIP_ASSUME_TAC) THEN
+ ASM_REWRITE_TAC[droplevel] THEN STRIP_TAC THEN
+ X_CHOOSE_THEN `t:V` STRIP_ASSUME_TAC
+ (SPEC `Powerset l` SETLEVEL_EXISTS) THEN
+ MP_TAC(SPECL [`t:V`; `\v. !x. x <: v ==> x <: s`]
+ COMPREHENSION_EXISTS) THEN
+ MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:V` THEN
+ STRIP_TAC THEN ASM_REWRITE_TAC[subset_def] THEN
+ ASM_MESON_TAC[ELEMENT_IN_LEVEL];
+ MP_TAC(SPEC `level s` SETLEVEL_EXISTS) THEN
+ MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:V` THEN
+ STRIP_TAC THEN ASM_REWRITE_TAC[subset_def] THEN
+ ASM_MESON_TAC[ELEMENT_IN_LEVEL; MEMBERS_ISASET; isaset]]);;
+
+let POWERSET = new_specification ["powerset"]
+ (REWRITE_RULE[SKOLEM_THM] POWERSET_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* Pairing operation. *)
+(* ------------------------------------------------------------------------- *)
+
+let pair = new_definition
+ `pair x y =
+ mk_V(Cartprod (level x) (level y),I_PAIR(element x,element y))`;;
+
+let PAIR_IN_LEVEL = prove
+ (`!x y l m. x IN setlevel l /\ y IN setlevel m
+ ==> I_PAIR(x,y) IN setlevel (Cartprod l m)`,
+ REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]);;
+
+let DEST_MK_PAIR = prove
+ (`dest_V(mk_V(Cartprod (level x) (level y),I_PAIR(element x,element y))) =
+ Cartprod (level x) (level y),I_PAIR(element x,element y)`,
+ REWRITE_TAC[GSYM V_TYBIJ] THEN SIMP_TAC[PAIR_IN_LEVEL; ELEMENT_IN_LEVEL]);;
+
+let PAIR_INJ = prove
+ (`!x1 y1 x2 y2. (pair x1 y1 = pair x2 y2) <=> (x1 = x2) /\ (y1 = y2)`,
+ REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
+ REWRITE_TAC[pair] THEN
+ DISCH_THEN(MP_TAC o AP_TERM `dest_V`) THEN REWRITE_TAC[DEST_MK_PAIR] THEN
+ REWRITE_TAC[setlevel_INJ; PAIR_EQ; I_PAIR] THEN
+ REWRITE_TAC[level; element] THEN MESON_TAC[PAIR; CONJUNCT1 v_tybij]);;
+
+let LEVEL_PAIR = prove
+ (`!x y. level(pair x y) = Cartprod (level x) (level y)`,
+ REWRITE_TAC[level;
+ REWRITE_RULE[DEST_MK_PAIR] (AP_TERM `dest_V` (SPEC_ALL pair))]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Decomposition functions. *)
+(* ------------------------------------------------------------------------- *)
+
+let fst_def = new_definition
+ `fst p = @x. ?y. p = pair x y`;;
+
+let snd_def = new_definition
+ `snd p = @y. ?x. p = pair x y`;;
+
+let PAIR_CLAUSES = prove
+ (`!x y. (fst(pair x y) = x) /\ (snd(pair x y) = y)`,
+ REWRITE_TAC[fst_def; snd_def] THEN MESON_TAC[PAIR_INJ]);;
+
+(* ------------------------------------------------------------------------- *)
+(* And the Cartesian product space. *)
+(* ------------------------------------------------------------------------- *)
+
+let CARTESIAN_EXISTS = prove
+ (`!s t. ?u. (level u =
+ Powerset(Cartprod (droplevel(level s))
+ (droplevel(level t)))) /\
+ !z. z <: u <=> ?x y. (z = pair x y) /\ x <: s /\ y <: t`,
+ REPEAT GEN_TAC THEN
+ ASM_CASES_TAC `isaset s` THENL
+ [ALL_TAC; ASM_MESON_TAC[EMPTY_EXISTS; MEMBERS_ISASET]] THEN
+ SUBGOAL_THEN `?l. (level s = Powerset l)` CHOOSE_TAC THENL
+ [ASM_MESON_TAC[isaset]; ALL_TAC] THEN
+ ASM_CASES_TAC `isaset t` THENL
+ [ALL_TAC; ASM_MESON_TAC[EMPTY_EXISTS; MEMBERS_ISASET]] THEN
+ SUBGOAL_THEN `?m. (level t = Powerset m)` CHOOSE_TAC THENL
+ [ASM_MESON_TAC[isaset]; ALL_TAC] THEN
+ MP_TAC(SPEC `Cartprod l m` SETLEVEL_EXISTS) THEN
+ ASM_REWRITE_TAC[droplevel] THEN
+ DISCH_THEN(X_CHOOSE_THEN `u:V` STRIP_ASSUME_TAC) THEN
+ MP_TAC(SPECL [`u:V`; `\z. ?x y. (z = pair x y) /\ x <: s /\ y <: t`]
+ COMPREHENSION_EXISTS) THEN
+ MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `w:V` THEN
+ STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
+ X_GEN_TAC `z:V` THEN
+ MATCH_MP_TAC(TAUT `(a ==> b) /\ (c ==> a) ==> ((a /\ b) /\ c <=> c)`) THEN
+ CONJ_TAC THENL [MESON_TAC[ELEMENT_IN_LEVEL]; ALL_TAC] THEN
+ STRIP_TAC THEN ASM_REWRITE_TAC[LEVEL_PAIR] THEN BINOP_TAC THEN
+ ASM_MESON_TAC[inset; setlevel_INJ]);;
+
+let PRODUCT = new_specification ["product"]
+ (REWRITE_RULE[SKOLEM_THM] CARTESIAN_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* Extensionality for sets at the same level. *)
+(* ------------------------------------------------------------------------- *)
+
+let IN_SET_ELEMENT = prove
+ (`!s. isaset s /\ e IN set(s)
+ ==> ?x. (e = element x) /\ (level s = Powerset(level x)) /\ x <: s`,
+ REPEAT STRIP_TAC THEN
+ FIRST_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
+ EXISTS_TAC `mk_V(l,e)` THEN REWRITE_TAC[inset] THEN
+ SUBGOAL_THEN `e IN setlevel l` (fun t -> ASM_SIMP_TAC[t; MK_V_CLAUSES]) THEN
+ ASM_MESON_TAC[SET_SUBSET_SETLEVEL; SUBSET; droplevel]);;
+
+let SUBSET_ALT = prove
+ (`isaset s /\ isaset t
+ ==> (s <=: t <=> (level s = level t) /\ set(s) SUBSET set(t))`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[subset_def; inset] THEN
+ ASM_CASES_TAC `level s = level t` THEN ASM_REWRITE_TAC[SUBSET] THEN
+ STRIP_TAC THEN EQ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
+ ASM_MESON_TAC[IN_SET_ELEMENT]);;
+
+let SUBSET_ANTISYM_LEVEL = prove
+ (`!s t. isaset s /\ isaset t /\ s <=: t /\ t <=: s ==> (s = t)`,
+ REPEAT GEN_TAC THEN
+ REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
+ ASM_SIMP_TAC[SUBSET_ALT] THEN
+ EVERY_ASSUM(MP_TAC o GSYM o MATCH_MP SET_DECOMP) THEN
+ REPEAT STRIP_TAC THEN
+ MP_TAC(SPEC `s:V` SET) THEN MP_TAC(SPEC `t:V` SET) THEN
+ REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN
+ AP_TERM_TAC THEN BINOP_TAC THEN ASM_MESON_TAC[SUBSET_ANTISYM]);;
+
+let EXTENSIONALITY_LEVEL = prove
+ (`!s t. isaset s /\ isaset t /\ (level s = level t) /\ (!x. x <: s <=> x <: t)
+ ==> (s = t)`,
+ MESON_TAC[SUBSET_ANTISYM_LEVEL; subset_def]);;
+
+(* ------------------------------------------------------------------------- *)
+(* And hence for any nonempty sets. *)
+(* ------------------------------------------------------------------------- *)
+
+let EXTENSIONALITY_NONEMPTY = prove
+ (`!s t. (?x. x <: s) /\ (?x. x <: t) /\ (!x. x <: s <=> x <: t)
+ ==> (s = t)`,
+ REPEAT STRIP_TAC THEN MATCH_MP_TAC EXTENSIONALITY_LEVEL THEN
+ ASM_MESON_TAC[MEMBERS_ISASET; inset]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Union set exists. I don't need this but if might be a sanity check. *)
+(* ------------------------------------------------------------------------- *)
+
+let UNION_EXISTS = prove
+ (`!s. ?t. (level t = droplevel(level s)) /\
+ !x. x <: t <=> ?u. x <: u /\ u <: s`,
+ GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
+ [ALL_TAC;
+ MP_TAC(SPEC `droplevel(level s)` EMPTY_EXISTS) THEN
+ MATCH_MP_TAC MONO_EXISTS THEN ASM_MESON_TAC[MEMBERS_ISASET]] THEN
+ FIRST_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
+ ASM_REWRITE_TAC[droplevel] THEN ASM_CASES_TAC `?m. l = Powerset m` THENL
+ [ALL_TAC;
+ MP_TAC(SPEC `l:setlevel` EMPTY_EXISTS) THEN MATCH_MP_TAC MONO_EXISTS THEN
+ REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[inset] THEN
+ ASM_MESON_TAC[setlevel_INJ]] THEN
+ FIRST_X_ASSUM(X_CHOOSE_THEN `m:setlevel` SUBST_ALL_TAC) THEN
+ MP_TAC(SPEC `m:setlevel` SETLEVEL_EXISTS) THEN
+ ASM_REWRITE_TAC[droplevel] THEN
+ DISCH_THEN(X_CHOOSE_THEN `t:V` STRIP_ASSUME_TAC) THEN
+ MP_TAC(SPECL [`t:V`; `\x. ?u. x <: u /\ u <: s`]
+ COMPREHENSION_EXISTS) THEN
+ MATCH_MP_TAC MONO_EXISTS THEN
+ GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
+ ASM_MESON_TAC[inset; ELEMENT_IN_LEVEL; setlevel_INJ]);;
+
+let SETUNION = new_specification ["setunion"]
+ (REWRITE_RULE[SKOLEM_THM] UNION_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* Boolean stuff. *)
+(* ------------------------------------------------------------------------- *)
+
+let true_def = new_definition
+ `true = mk_V(Ur_bool,I_BOOL T)`;;
+
+let false_def = new_definition
+ `false = mk_V(Ur_bool,I_BOOL F)`;;
+
+let boolset = new_definition
+ `boolset =
+ mk_V(Powerset Ur_bool,I_SET (setlevel Ur_bool) (setlevel Ur_bool))`;;
+
+let IN_BOOL = prove
+ (`!x. x <: boolset <=> (x = true) \/ (x = false)`,
+ REWRITE_TAC[inset; boolset; true_def; false_def] THEN
+ SIMP_TAC[MK_V_SET; SUBSET_REFL] THEN
+ REWRITE_TAC[setlevel_INJ; setlevel] THEN
+ SUBGOAL_THEN `IMAGE I_BOOL UNIV = {I_BOOL F,I_BOOL T}` SUBST1_TAC THENL
+ [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_UNIV; IN_INSERT; NOT_IN_EMPTY] THEN
+ MESON_TAC[I_BOOL];
+ ALL_TAC] THEN
+ GEN_TAC THEN
+ GEN_REWRITE_TAC (RAND_CONV o BINOP_CONV o LAND_CONV) [GSYM SET] THEN
+ REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
+ SUBGOAL_THEN `!b. (I_BOOL b) IN setlevel Ur_bool` ASSUME_TAC THENL
+ [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[];
+ ASM_MESON_TAC[V_TYBIJ; ELEMENT_IN_LEVEL; PAIR_EQ]]);;
+
+let TRUE_NE_FALSE = prove
+ (`~(true = false)`,
+ REWRITE_TAC[true_def; false_def] THEN
+ DISCH_THEN(MP_TAC o AP_TERM `dest_V`) THEN
+ SUBGOAL_THEN `!b. (I_BOOL b) IN setlevel Ur_bool` ASSUME_TAC THENL
+ [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[];
+ ASM_MESON_TAC[V_TYBIJ; I_BOOL; PAIR_EQ]]);;
+
+let BOOLEAN_EQ = prove
+ (`!x y. x <: boolset /\ y <: boolset /\
+ ((x = true) <=> (y = true))
+ ==> (x = y)`,
+ MESON_TAC[TRUE_NE_FALSE; IN_BOOL]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Ind stuff. *)
+(* ------------------------------------------------------------------------- *)
+
+let indset = new_definition
+ `indset = mk_V(Powerset Ur_ind,I_SET (setlevel Ur_ind) (setlevel Ur_ind))`;;
+
+let INDSET_IND_MODEL = prove
+ (`?f. (!i:ind_model. f(i) <: indset) /\ (!i j. (f i = f j) ==> (i = j))`,
+ EXISTS_TAC `\i. mk_V(Ur_ind,I_IND i)` THEN REWRITE_TAC[] THEN
+ SUBGOAL_THEN `!i. (I_IND i) IN setlevel Ur_ind` ASSUME_TAC THENL
+ [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[]; ALL_TAC] THEN
+ ASM_SIMP_TAC[MK_V_SET; SUBSET_REFL; inset; indset; MK_V_CLAUSES] THEN
+ ASM_MESON_TAC[V_TYBIJ; I_IND; ELEMENT_IN_LEVEL; PAIR_EQ]);;
+
+let INDSET_INHABITED = prove
+ (`?x. x <: indset`,
+ MESON_TAC[INDSET_IND_MODEL]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Axiom of choice (this is trivially so in HOL anyway, but...) *)
+(* ------------------------------------------------------------------------- *)
+
+let ch =
+ let th = prove
+ (`?ch. !s. (?x. x <: s) ==> ch(s) <: s`,
+ REWRITE_TAC[GSYM SKOLEM_THM] THEN MESON_TAC[]) in
+ new_specification ["ch"] th;;
+
+(* ------------------------------------------------------------------------- *)
+(* Sanity check lemmas. *)
+(* ------------------------------------------------------------------------- *)
+
+let IN_POWERSET = prove
+ (`!x s. x <: powerset s <=> x <=: s`,
+ MESON_TAC[POWERSET]);;
+
+let IN_PRODUCT = prove
+ (`!z s t. z <: product s t <=> ?x y. (z = pair x y) /\ x <: s /\ y <: t`,
+ MESON_TAC[PRODUCT]);;
+
+let IN_COMPREHENSION = prove
+ (`!p s x. x <: s suchthat p <=> x <: s /\ p x`,
+ MESON_TAC[SUCHTHAT]);;
+
+let PRODUCT_INHABITED = prove
+ (`(?x. x <: s) /\ (?y. y <: t) ==> ?z. z <: product s t`,
+ MESON_TAC[IN_PRODUCT]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Definition of function space. *)
+(* ------------------------------------------------------------------------- *)
+
+let funspace = new_definition
+ `funspace s t =
+ powerset(product s t) suchthat
+ (\u. !x. x <: s ==> ?!y. pair x y <: u)`;;
+
+let apply_def = new_definition
+ `apply f x = @y. pair x y <: f`;;
+
+let abstract = new_definition
+ `abstract s t f =
+ (product s t) suchthat (\z. !x y. (pair x y = z) ==> (y = f x))`;;
+
+let APPLY_ABSTRACT = prove
+ (`!x s t. x <: s /\ f(x) <: t ==> (apply(abstract s t f) x = f(x))`,
+ REPEAT STRIP_TAC THEN
+ REWRITE_TAC[apply_def; abstract; IN_PRODUCT; SUCHTHAT] THEN
+ MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[PAIR_INJ] THEN
+ ASM_MESON_TAC[]);;
+
+let APPLY_IN_RANSPACE = prove
+ (`!f x s t. x <: s /\ f <: funspace s t ==> apply f x <: t`,
+ REWRITE_TAC[funspace; SUCHTHAT; IN_POWERSET; IN_PRODUCT; subset_def] THEN
+ REWRITE_TAC[apply_def] THEN MESON_TAC[PAIR_INJ]);;
+
+let ABSTRACT_IN_FUNSPACE = prove
+ (`!f x s t. (!x. x <: s ==> f(x) <: t)
+ ==> abstract s t f <: funspace s t`,
+ REWRITE_TAC[funspace; abstract; SUCHTHAT; IN_POWERSET; IN_PRODUCT;
+ subset_def; PAIR_INJ] THEN
+ SIMP_TAC[LEFT_FORALL_IMP_THM; GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
+ REWRITE_TAC[UNWIND_THM1; EXISTS_REFL] THEN MESON_TAC[]);;
+
+let FUNSPACE_INHABITED = prove
+ (`!s t. ((?x. x <: s) ==> (?y. y <: t)) ==> ?f. f <: funspace s t`,
+ REPEAT STRIP_TAC THEN
+ EXISTS_TAC `abstract s t (\x. @y. y <: t)` THEN
+ MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN ASM_MESON_TAC[]);;
+
+let ABSTRACT_EQ = prove
+ (`!s t1 t2 f g.
+ (?x. x <: s) /\
+ (!x. x <: s ==> f(x) <: t1 /\ g(x) <: t2 /\ (f x = g x))
+ ==> (abstract s t1 f = abstract s t2 g)`,
+ REWRITE_TAC[abstract] THEN REPEAT STRIP_TAC THEN
+ MATCH_MP_TAC EXTENSIONALITY_NONEMPTY THEN
+ REWRITE_TAC[SUCHTHAT; IN_PRODUCT] THEN REPEAT CONJ_TAC THEN
+ REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
+ SIMP_TAC[TAUT `(a /\ b /\ c) /\ d <=> ~(a ==> b /\ c ==> ~d)`] THEN
+ REWRITE_TAC[PAIR_INJ] THEN SIMP_TAC[LEFT_FORALL_IMP_THM] THENL
+ [ASM_MESON_TAC[]; ASM_MESON_TAC[]; ALL_TAC] THEN
+ ASM_REWRITE_TAC[PAIR_INJ] THEN
+ REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_REFL] THEN
+ REWRITE_TAC[NOT_IMP] THEN GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
+ ASM_REWRITE_TAC[PAIR_INJ] THEN ASM_MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Special case of treating a Boolean function as a set. *)
+(* ------------------------------------------------------------------------- *)
+
+let boolean = new_definition
+ `boolean b = if b then true else false`;;
+
+let holds = new_definition
+ `holds s x <=> (apply s x = true)`;;
+
+let BOOLEAN_IN_BOOLSET = prove
+ (`!b. boolean b <: boolset`,
+ REWRITE_TAC[boolean] THEN MESON_TAC[IN_BOOL]);;
+
+let BOOLEAN_EQ_TRUE = prove
+ (`!b. (boolean b = true) <=> b`,
+ REWRITE_TAC[boolean] THEN MESON_TAC[TRUE_NE_FALSE]);;
--- /dev/null
+(* ========================================================================= *)
+(* Formal semantics of HOL inside itself. *)
+(* ========================================================================= *)
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics of types. *)
+(* ------------------------------------------------------------------------- *)
+
+let typeset = new_recursive_definition type_RECURSION
+ `(typeset tau (Tyvar s) = tau(s)) /\
+ (typeset tau Bool = boolset) /\
+ (typeset tau Ind = indset) /\
+ (typeset tau (Fun a b) = funspace (typeset tau a) (typeset tau b))`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics of terms. *)
+(* ------------------------------------------------------------------------- *)
+
+let semantics = new_recursive_definition term_RECURSION
+ `(semantics sigma tau (Var n ty) = sigma(n,ty)) /\
+ (semantics sigma tau (Equal ty) =
+ abstract (typeset tau ty) (typeset tau (Fun ty Bool))
+ (\x. abstract (typeset tau ty) (typeset tau Bool)
+ (\y. boolean(x = y)))) /\
+ (semantics sigma tau (Select ty) =
+ abstract (typeset tau (Fun ty Bool)) (typeset tau ty)
+ (\s. if ?x. x <: ((typeset tau ty) suchthat (holds s))
+ then ch ((typeset tau ty) suchthat (holds s))
+ else ch (typeset tau ty))) /\
+ (semantics sigma tau (Comb s t) =
+ apply (semantics sigma tau s) (semantics sigma tau t)) /\
+ (semantics sigma tau (Abs n ty t) =
+ abstract (typeset tau ty) (typeset tau (typeof t))
+ (\x. semantics (((n,ty) |-> x) sigma) tau t))`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Valid type and term valuations. *)
+(* ------------------------------------------------------------------------- *)
+
+let type_valuation = new_definition
+ `type_valuation tau <=> !x. (?y. y <: tau x)`;;
+
+let term_valuation = new_definition
+ `term_valuation tau sigma <=> !n ty. sigma(n,ty) <: typeset tau ty`;;
+
+let TERM_VALUATION_VALMOD = prove
+ (`!sigma taut n ty x.
+ term_valuation tau sigma /\ x <: typeset tau ty
+ ==> term_valuation tau (((n,ty) |-> x) sigma)`,
+ REWRITE_TAC[term_valuation; valmod; PAIR_EQ] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* All the typesets are nonempty. *)
+(* ------------------------------------------------------------------------- *)
+
+let TYPESET_INHABITED = prove
+ (`!tau ty. type_valuation tau ==> ?x. x <: typeset tau ty`,
+ REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
+ MATCH_MP_TAC type_INDUCT THEN REWRITE_TAC[typeset] THEN
+ CONJ_TAC THENL
+ [ASM_MESON_TAC[type_valuation];
+ ASM_MESON_TAC[BOOLEAN_IN_BOOLSET; INDSET_INHABITED; FUNSPACE_INHABITED]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics maps into the right place. *)
+(* ------------------------------------------------------------------------- *)
+
+let SEMANTICS_TYPESET_INDUCT = prove
+ (`!tm ty. tm has_type ty
+ ==> tm has_type ty /\
+ !sigma tau. type_valuation tau /\ term_valuation tau sigma
+ ==> (semantics sigma tau tm) <: (typeset tau ty)`,
+ MATCH_MP_TAC has_type_INDUCT THEN
+ ASM_SIMP_TAC[semantics; typeset; has_type_RULES] THEN
+ CONJ_TAC THENL [MESON_TAC[term_valuation]; ALL_TAC] THEN
+ REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
+ [MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN REWRITE_TAC[] THEN
+ REPEAT STRIP_TAC THEN MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN
+ REWRITE_TAC[BOOLEAN_IN_BOOLSET];
+ MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN
+ ASM_MESON_TAC[ch; SUCHTHAT; TYPESET_INHABITED];
+ ASM_MESON_TAC[has_type_RULES];
+ MATCH_MP_TAC APPLY_IN_RANSPACE THEN ASM_MESON_TAC[];
+ FIRST_ASSUM(SUBST1_TAC o MATCH_MP WELLTYPED_LEMMA) THEN
+ MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN
+ REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD]]);;
+
+let SEMANTICS_TYPESET = prove
+ (`!sigma tau tm ty.
+ type_valuation tau /\ term_valuation tau sigma /\ tm has_type ty
+ ==> (semantics sigma tau tm) <: (typeset tau ty)`,
+ MESON_TAC[SEMANTICS_TYPESET_INDUCT]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics of equations. *)
+(* ------------------------------------------------------------------------- *)
+
+let SEMANTICS_EQUATION = prove
+ (`!sigma tau s t.
+ s has_type (typeof s) /\ t has_type (typeof s) /\
+ type_valuation tau /\ term_valuation tau sigma
+ ==> (semantics sigma tau (s === t) =
+ boolean(semantics sigma tau s = semantics sigma tau t))`,
+ REPEAT STRIP_TAC THEN REWRITE_TAC[equation; semantics] THEN
+ ASM_SIMP_TAC[APPLY_ABSTRACT; typeset; SEMANTICS_TYPESET;
+ ABSTRACT_IN_FUNSPACE; BOOLEAN_IN_BOOLSET]);;
+
+let SEMANTICS_EQUATION_ALT = prove
+ (`!sigma tau s t.
+ (s === t) has_type Bool /\
+ type_valuation tau /\ term_valuation tau sigma
+ ==> (semantics sigma tau (s === t) =
+ boolean(semantics sigma tau s = semantics sigma tau t))`,
+ REPEAT STRIP_TAC THEN MATCH_MP_TAC SEMANTICS_EQUATION THEN
+ ASM_REWRITE_TAC[] THEN
+ SUBGOAL_THEN `welltyped(s === t)` MP_TAC THENL
+ [ASM_MESON_TAC[welltyped]; ALL_TAC] THEN
+ REWRITE_TAC[equation; WELLTYPED_CLAUSES; typeof; codomain] THEN
+ MESON_TAC[welltyped; type_INJ; WELLTYPED; WELLTYPED_CLAUSES]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Quick sanity check. *)
+(* ------------------------------------------------------------------------- *)
+
+let SEMANTICS_SELECT = prove
+ (`p has_type (Fun ty Bool) /\
+ type_valuation tau /\ term_valuation tau sigma
+ ==> (semantics sigma tau (Comb (Select ty) p) =
+ if ?x. x <: (typeset tau ty) suchthat (holds (semantics sigma tau p))
+ then ch((typeset tau ty) suchthat (holds (semantics sigma tau p)))
+ else ch(typeset tau ty))`,
+ REPEAT STRIP_TAC THEN REWRITE_TAC[semantics] THEN
+ W(fun (asl,w) ->
+ let t = find_term (fun t ->
+ can (PART_MATCH (lhs o rand) APPLY_ABSTRACT) t) w in
+ MP_TAC(PART_MATCH (lhs o rand) APPLY_ABSTRACT t)) THEN
+ ANTS_TAC THENL
+ [CONJ_TAC THENL
+ [ASM_MESON_TAC[SEMANTICS_TYPESET; typeset];
+ REWRITE_TAC[SUCHTHAT] THEN
+ ASM_MESON_TAC[ch; SUCHTHAT; TYPESET_INHABITED]];
+ ALL_TAC] THEN
+ DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics of a sequent. *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("|=",(11,"right"));;
+
+let sequent = new_definition
+ `asms |= p <=> ALL (\a. a has_type Bool) (CONS p asms) /\
+ !sigma tau. type_valuation tau /\
+ term_valuation tau sigma /\
+ ALL (\a. semantics sigma tau a = true) asms
+ ==> (semantics sigma tau p = true)`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Invariance of semantics under alpha-conversion. *)
+(* ------------------------------------------------------------------------- *)
+
+let SEMANTICS_RACONV = prove
+ (`!env tp.
+ RACONV env tp
+ ==> !sigma1 sigma2 tau.
+ type_valuation tau /\
+ term_valuation tau sigma1 /\ term_valuation tau sigma2 /\
+ (!x1 ty1 x2 ty2.
+ ALPHAVARS env (Var x1 ty1,Var x2 ty2)
+ ==> (semantics sigma1 tau (Var x1 ty1) =
+ semantics sigma2 tau (Var x2 ty2)))
+ ==> welltyped(FST tp) /\ welltyped(SND tp)
+ ==> (semantics sigma1 tau (FST tp) =
+ semantics sigma2 tau (SND tp))`,
+ MATCH_MP_TAC RACONV_INDUCT THEN REWRITE_TAC[FORALL_PAIR_THM] THEN
+ REWRITE_TAC[semantics; WELLTYPED_CLAUSES] THEN REPEAT STRIP_TAC THENL
+ [ASM_MESON_TAC[];
+ BINOP_TAC THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ FIRST_X_ASSUM SUBST_ALL_TAC THEN MATCH_MP_TAC ABSTRACT_EQ THEN
+ ASM_SIMP_TAC[TYPESET_INHABITED] THEN
+ X_GEN_TAC `x:V` THEN DISCH_TAC THEN REPEAT CONJ_TAC THENL
+ [MATCH_MP_TAC SEMANTICS_TYPESET THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD; GSYM WELLTYPED];
+ MATCH_MP_TAC SEMANTICS_TYPESET THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD; GSYM WELLTYPED];
+ ALL_TAC] THEN
+ RULE_ASSUM_TAC(REWRITE_RULE[IMP_IMP]) THEN
+ FIRST_X_ASSUM(fun th -> MATCH_MP_TAC th THEN CONJ_TAC) THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ REWRITE_TAC[ALPHAVARS; PAIR_EQ; term_INJ] THEN
+ REPEAT STRIP_TAC THEN ASM_SIMP_TAC[VALMOD; PAIR_EQ] THEN
+ ASM_MESON_TAC[]);;
+
+let SEMANTICS_ACONV = prove
+ (`!sigma tau s t.
+ type_valuation tau /\ term_valuation tau sigma /\
+ welltyped s /\ welltyped t /\ ACONV s t
+ ==> (semantics sigma tau s = semantics sigma tau t)`,
+ REWRITE_TAC[ACONV] THEN REPEAT STRIP_TAC THEN
+ MATCH_MP_TAC(REWRITE_RULE[IMP_IMP; RIGHT_IMP_FORALL_THM; FORALL_PAIR_THM]
+ SEMANTICS_RACONV) THEN
+ EXISTS_TAC `[]:(term#term)list` THEN
+ ASM_SIMP_TAC[ALPHAVARS; term_INJ; PAIR_EQ]);;
+
+(* ------------------------------------------------------------------------- *)
+(* General semantic lemma about binary inference rules. *)
+(* ------------------------------------------------------------------------- *)
+
+let BINARY_INFERENCE_RULE = prove
+ (`(p1 has_type Bool /\ p2 has_type Bool
+ ==> q has_type Bool /\
+ !sigma tau. type_valuation tau /\ term_valuation tau sigma /\
+ (semantics sigma tau p1 = true) /\
+ (semantics sigma tau p2 = true)
+ ==> (semantics sigma tau q = true))
+ ==> (asl1 |= p1 /\ asl2 |= p2 ==> TERM_UNION asl1 asl2 |= q)`,
+ REWRITE_TAC[sequent; ALL] THEN STRIP_TAC THEN STRIP_TAC THEN
+ ASM_SIMP_TAC[ALL_BOOL_TERM_UNION] THEN REPEAT STRIP_TAC THEN
+ FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN ASM_REWRITE_TAC[] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MATCH_MP_TAC) THEN
+ ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
+ ASM_REWRITE_TAC[] THEN UNDISCH_TAC
+ `ALL (\a. semantics sigma tau a = true) (TERM_UNION asl1 asl2)` THEN
+ REWRITE_TAC[GSYM ALL_MEM] THEN
+ REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM ALL_MEM])) THEN
+ REWRITE_TAC[] THEN STRIP_TAC THEN STRIP_TAC THEN
+ DISCH_THEN(fun th -> X_GEN_TAC `r:term` THEN DISCH_TAC THEN MP_TAC th) THEN
+ MP_TAC(SPECL [`asl1:term list`; `asl2:term list`; `r:term`]
+ TERM_UNION_THM) THEN
+ ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `s:term`) THEN
+ DISCH_THEN(MP_TAC o SPEC `s:term`) THEN ASM_REWRITE_TAC[] THEN
+ ASM_MESON_TAC[SEMANTICS_ACONV; welltyped; TERM_UNION_NONEW]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics only depends on valuations of free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+let TERM_VALUATION_VFREE_IN = prove
+ (`!tau sigma1 sigma2 t.
+ type_valuation tau /\
+ term_valuation tau sigma1 /\ term_valuation tau sigma2 /\
+ welltyped t /\
+ (!x ty. VFREE_IN (Var x ty) t ==> (sigma1(x,ty) = sigma2(x,ty)))
+ ==> (semantics sigma1 tau t = semantics sigma2 tau t)`,
+ GEN_TAC THEN GEN_REWRITE_TAC BINDER_CONV [SWAP_FORALL_THM] THEN
+ GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN MATCH_MP_TAC term_INDUCT THEN
+ REWRITE_TAC[semantics; VFREE_IN; term_DISTINCT; term_INJ] THEN
+ REPEAT STRIP_TAC THENL
+ [ASM_MESON_TAC[];
+ BINOP_TAC THEN ASM_MESON_TAC[WELLTYPED_CLAUSES];
+ ALL_TAC] THEN
+ MATCH_MP_TAC ABSTRACT_EQ THEN ASM_SIMP_TAC[TYPESET_INHABITED] THEN
+ X_GEN_TAC `x:V` THEN DISCH_TAC THEN REPEAT(CONJ_TAC THENL
+ [ASM_MESON_TAC[TERM_VALUATION_VALMOD; WELLTYPED; WELLTYPED_CLAUSES;
+ SEMANTICS_TYPESET];
+ ALL_TAC]) THEN
+ FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ CONJ_TAC THENL [ASM_MESON_TAC[WELLTYPED_CLAUSES]; ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`] THEN DISCH_TAC THEN
+ REWRITE_TAC[VALMOD; PAIR_EQ] THEN ASM_MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Prove some inference rules correct. *)
+(* ------------------------------------------------------------------------- *)
+
+let ASSUME_correct = prove
+ (`!p. p has_type Bool ==> [p] |= p`,
+ SIMP_TAC[sequent; ALL]);;
+
+let REFL_correct = prove
+ (`!t. welltyped t ==> [] |= t === t`,
+ SIMP_TAC[sequent; SEMANTICS_EQUATION; ALL; WELLTYPED] THEN
+ REWRITE_TAC[boolean; equation] THEN MESON_TAC[has_type_RULES]);;
+
+let TRANS_correct = prove
+ (`!asl1 asl2 l m1 m2 r.
+ asl1 |= l === m1 /\ asl2 |= m2 === r /\ ACONV m1 m2
+ ==> TERM_UNION asl1 asl2 |= l === r`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
+ MATCH_MP_TAC BINARY_INFERENCE_RULE THEN STRIP_TAC THEN
+ MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
+ [ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL; ACONV_TYPE];
+ ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; IMP_CONJ; boolean] THEN
+ ASM_MESON_TAC[SEMANTICS_ACONV; TRUE_NE_FALSE; EQUATION_HAS_TYPE_BOOL]]);;
+
+let MK_COMB_correct = prove
+ (`!asl1 l1 r1 asl2 l2 r2.
+ asl1 |= l1 === r1 /\ asl2 |= l2 === r2 /\
+ (?rty. typeof l1 = Fun (typeof l2) rty)
+ ==> TERM_UNION asl1 asl2 |= Comb l1 l2 === Comb r1 r2`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
+ MATCH_MP_TAC BINARY_INFERENCE_RULE THEN STRIP_TAC THEN
+ MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
+ [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
+ REWRITE_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_CLAUSES; typeof] THEN
+ MESON_TAC[codomain];
+ ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; IMP_CONJ; boolean] THEN
+ REWRITE_TAC[semantics] THEN
+ ASM_MESON_TAC[SEMANTICS_ACONV; TRUE_NE_FALSE; EQUATION_HAS_TYPE_BOOL]]);;
+
+let EQ_MP_correct = prove
+ (`!asl1 asl2 p q p'.
+ asl1 |= p === q /\ asl2 |= p' /\ ACONV p p'
+ ==> TERM_UNION asl1 asl2 |= q`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
+ MATCH_MP_TAC BINARY_INFERENCE_RULE THEN STRIP_TAC THEN
+ MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
+ [ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_LEMMA; WELLTYPED;
+ ACONV_TYPE];
+ ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; IMP_CONJ; boolean] THEN
+ ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL; TRUE_NE_FALSE; SEMANTICS_ACONV;
+ welltyped]]);;
+
+let BETA_correct = prove
+ (`!x ty t. welltyped t ==> [] |= Comb (Abs x ty t) (Var x ty) === t`,
+ REPEAT STRIP_TAC THEN REWRITE_TAC[sequent; ALL] THEN
+ MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
+ [REWRITE_TAC[EQUATION_HAS_TYPE_BOOL; typeof; WELLTYPED_CLAUSES] THEN
+ REWRITE_TAC[codomain; type_INJ] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ SIMP_TAC[SEMANTICS_EQUATION_ALT] THEN
+ DISCH_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
+ REWRITE_TAC[BOOLEAN_EQ_TRUE; semantics] THEN
+ MATCH_MP_TAC EQ_TRANS THEN
+ EXISTS_TAC `semantics (((x,ty) |-> sigma(x,ty)) sigma) tau t` THEN
+ CONJ_TAC THENL [MATCH_MP_TAC APPLY_ABSTRACT; ALL_TAC] THEN
+ REWRITE_TAC[VALMOD_REPEAT] THEN
+ ASM_MESON_TAC[term_valuation; SEMANTICS_TYPESET; WELLTYPED]);;
+
+let ABS_correct = prove
+ (`!asl x ty l r.
+ ~(EX (VFREE_IN (Var x ty)) asl) /\ asl |= l === r
+ ==> asl |= (Abs x ty l) === (Abs x ty r)`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[sequent; ALL] THEN STRIP_TAC THEN
+ ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
+ CONJ_TAC THENL
+ [UNDISCH_TAC `(l === r) has_type Bool` THEN
+ SIMP_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_CLAUSES; typeof];
+ ALL_TAC] THEN
+ DISCH_TAC THEN ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; BOOLEAN_EQ_TRUE] THEN
+ REPEAT STRIP_TAC THEN REWRITE_TAC[semantics] THEN
+ SUBGOAL_THEN `typeof r = typeof l` SUBST1_TAC THENL
+ [ASM_MESON_TAC[EQUATION_HAS_TYPE_BOOL]; ALL_TAC] THEN
+ MATCH_MP_TAC ABSTRACT_EQ THEN ASM_SIMP_TAC[TYPESET_INHABITED] THEN
+ X_GEN_TAC `x:V` THEN DISCH_TAC THEN
+ REPEAT(CONJ_TAC THENL
+ [ASM_MESON_TAC[SEMANTICS_TYPESET; TERM_VALUATION_VALMOD;
+ WELLTYPED; EQUATION_HAS_TYPE_BOOL];
+ ALL_TAC]) THEN
+ FIRST_X_ASSUM(MP_TAC o check (is_forall o concl)) THEN
+ ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; BOOLEAN_EQ_TRUE] THEN
+ DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ SUBGOAL_THEN `ALL (\a. a has_type Bool) asl /\
+ ALL (\a. ~(VFREE_IN (Var x ty) a)) asl /\
+ ALL (\a. semantics sigma tau a = true) asl`
+ MP_TAC THENL [ASM_REWRITE_TAC[GSYM NOT_EX; ETA_AX]; ALL_TAC] THEN
+ REWRITE_TAC[AND_ALL] THEN
+ MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
+ X_GEN_TAC `p:term` THEN DISCH_TAC THEN REWRITE_TAC[] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THEN
+ MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ CONJ_TAC THENL [ASM_MESON_TAC[welltyped]; ALL_TAC] THEN
+ REPEAT STRIP_TAC THEN REWRITE_TAC[VALMOD; PAIR_EQ] THEN ASM_MESON_TAC[]);;
+
+let DEDUCT_ANTISYM_RULE_correct = prove
+ (`!asl1 asl2 p q.
+ asl1 |= c1 /\ asl2 |= c2
+ ==> let asl1' = FILTER((~) o ACONV c2) asl1
+ and asl2' = FILTER((~) o ACONV c1) asl2 in
+ (TERM_UNION asl1' asl2') |= c1 === c2`,
+ REPEAT GEN_TAC THEN
+ REWRITE_TAC[sequent; o_DEF; LET_DEF; LET_END_DEF; GSYM CONJ_ASSOC] THEN
+ MATCH_MP_TAC(TAUT `
+ (a1 /\ b1 ==> c1) /\ (a1 /\ b1 /\ c1 ==> a2 /\ b2 ==> c2)
+ ==> a1 /\ a2 /\ b1 /\ b2 ==> c1 /\ c2`) THEN
+ CONJ_TAC THENL
+ [REWRITE_TAC[GSYM ALL_MEM; MEM] THEN REPEAT STRIP_TAC THEN
+ ASM_REWRITE_TAC[EQUATION_HAS_TYPE_BOOL] THEN
+ ASM_MESON_TAC[MEM_FILTER; TERM_UNION_NONEW; welltyped; WELLTYPED_LEMMA];
+ ALL_TAC] THEN
+ REWRITE_TAC[ALL; AND_FORALL_THM] THEN REWRITE_TAC[GSYM ALL_MEM] THEN
+ STRIP_TAC THEN
+ REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
+ DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
+ ASM_SIMP_TAC[SEMANTICS_EQUATION_ALT; BOOLEAN_EQ_TRUE] THEN
+ REPEAT STRIP_TAC THEN MATCH_MP_TAC BOOLEAN_EQ THEN
+ REPEAT(CONJ_TAC THENL
+ [ASM_MESON_TAC[typeset; SEMANTICS_TYPESET]; ALL_TAC]) THEN
+ EQ_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
+ X_GEN_TAC `a:term` THEN DISCH_TAC THENL
+ [ASM_CASES_TAC `ACONV c1 a` THENL
+ [ASM_MESON_TAC[SEMANTICS_ACONV; welltyped]; ALL_TAC];
+ ASM_CASES_TAC `ACONV c2 a` THENL
+ [ASM_MESON_TAC[SEMANTICS_ACONV; welltyped]; ALL_TAC]] THEN
+ (SUBGOAL_THEN
+ `MEM a (FILTER (\x. ~ACONV c2 x) asl1) \/
+ MEM a (FILTER (\x. ~ACONV c1 x) asl2)`
+ MP_TAC THENL
+ [REWRITE_TAC[MEM_FILTER] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
+ DISCH_THEN(MP_TAC o MATCH_MP TERM_UNION_THM) THEN
+ ASM_MESON_TAC[SEMANTICS_ACONV; welltyped]));;
+
+(* ------------------------------------------------------------------------- *)
+(* Correct semantics for term substitution. *)
+(* ------------------------------------------------------------------------- *)
+
+let DEST_VAR = new_recursive_definition term_RECURSION
+ `DEST_VAR (Var x ty) = (x,ty)`;;
+
+let TERM_VALUATION_ITLIST = prove
+ (`!ilist sigma tau.
+ type_valuation tau /\ term_valuation tau sigma /\
+ (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
+ ==> term_valuation tau
+ (ITLIST (\(t,x). DEST_VAR x |-> semantics sigma tau t) ilist sigma)`,
+ MATCH_MP_TAC list_INDUCT THEN SIMP_TAC[ITLIST] THEN
+ REWRITE_TAC[FORALL_PAIR_THM; MEM; PAIR_EQ] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+ SIMP_TAC[LEFT_FORALL_IMP_THM; FORALL_AND_THM] THEN
+ REWRITE_TAC[LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
+ REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[DEST_VAR] THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD; SEMANTICS_TYPESET]);;
+
+let ITLIST_VALMOD_FILTER = prove
+ (`!ilist sigma sem x ty y yty.
+ (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
+ ==> (ITLIST (\(t,x). DEST_VAR x |-> sem x t)
+ (FILTER (\(s',s). ~(s = Var x ty)) ilist) sigma (y,yty) =
+ if (y = x) /\ (yty = ty) then sigma(y,yty)
+ else ITLIST (\(t,x). DEST_VAR x |-> sem x t) ilist sigma (y,yty))`,
+ MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[FILTER; ITLIST; COND_ID] THEN
+ REWRITE_TAC[FORALL_PAIR_THM] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[MEM; TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+ SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
+ REWRITE_TAC[WELLTYPED_CLAUSES; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
+ MAP_EVERY X_GEN_TAC [`t:term`; `pp:term`; `ilist:(term#term)list`] THEN
+ DISCH_TAC THEN REPEAT GEN_TAC THEN
+ DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `s:string` MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `sty:type` MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
+ GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RAND] THEN
+ GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RATOR] THEN
+ ASM_REWRITE_TAC[ITLIST] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[DEST_VAR] THEN
+ GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [COND_RATOR] THEN
+ REWRITE_TAC[VALMOD] THEN REWRITE_TAC[term_INJ] THEN
+ ASM_CASES_TAC `(s:string = x) /\ (sty:type = ty)` THEN
+ ASM_SIMP_TAC[PAIR_EQ] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
+
+let ITLIST_VALMOD_EQ = prove
+ (`!l. (!t x. MEM (t,x) l /\ (f x = a) ==> (g x t = h x t)) /\ (i a = j a)
+ ==> (ITLIST (\(t,x). f(x) |-> g x t) l i a =
+ ITLIST (\(t,x). f(x) |-> h x t) l j a)`,
+ MATCH_MP_TAC list_INDUCT THEN SIMP_TAC[MEM; ITLIST; FORALL_PAIR_THM] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[PAIR_EQ; VALMOD] THEN MESON_TAC[]);;
+
+let SEMANTICS_VSUBST = prove
+ (`!tm sigma tau ilist.
+ welltyped tm /\
+ (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
+ ==> !sigma tau. type_valuation tau /\ term_valuation tau sigma
+ ==> (semantics sigma tau (VSUBST ilist tm) =
+ semantics
+ (ITLIST
+ (\(t,x). DEST_VAR x |-> semantics sigma tau t)
+ ilist sigma)
+ tau tm)`,
+ MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VSUBST; semantics] THEN
+ CONJ_TAC THENL
+ [MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`] THEN
+ MATCH_MP_TAC list_INDUCT THEN
+ REWRITE_TAC[MEM; REV_ASSOCD; ITLIST; semantics; FORALL_PAIR_THM] THEN
+ MAP_EVERY X_GEN_TAC [`t:term`; `s:term`; `ilist:(term#term)list`] THEN
+ REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+ SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
+ REWRITE_TAC[WELLTYPED_CLAUSES; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
+ DISCH_THEN(fun th ->
+ DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN MP_TAC th) THEN
+ ASM_REWRITE_TAC[] THEN
+ FIRST_X_ASSUM(X_CHOOSE_THEN `y:string` MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `tty:type` MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[DEST_VAR; VALMOD; term_INJ; PAIR_EQ] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ CONJ_TAC THENL
+ [REWRITE_TAC[WELLTYPED_CLAUSES] THEN REPEAT STRIP_TAC THEN
+ BINOP_TAC THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN
+ REWRITE_TAC[WELLTYPED_CLAUSES] THEN
+ ASM_CASES_TAC `welltyped t` THEN ASM_REWRITE_TAC[] THEN
+ REPEAT STRIP_TAC THEN LET_TAC THEN LET_TAC THEN
+ SUBGOAL_THEN
+ `!s s'. MEM (s',s) ilist' ==> (?x ty. (s = Var x ty) /\ s' has_type ty)`
+ ASSUME_TAC THENL
+ [EXPAND_TAC "ilist'" THEN ASM_SIMP_TAC[MEM_FILTER]; ALL_TAC] THEN
+ COND_CASES_TAC THENL
+ [REPEAT LET_TAC THEN
+ SUBGOAL_THEN
+ `!s s'. MEM (s',s) ilist'' ==> (?x ty. (s = Var x ty) /\ s' has_type ty)`
+ ASSUME_TAC THENL
+ [EXPAND_TAC "ilist''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
+ ASM_MESON_TAC[has_type_RULES];
+ ALL_TAC];
+ ALL_TAC] THEN
+ REWRITE_TAC[semantics] THEN
+ MATCH_MP_TAC ABSTRACT_EQ THEN ASM_SIMP_TAC[TYPESET_INHABITED] THEN
+ X_GEN_TAC `a:V` THEN DISCH_TAC THEN
+ REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC SEMANTICS_TYPESET) THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD; TERM_VALUATION_ITLIST] THEN
+ EXPAND_TAC "t'" THEN
+ ASM_SIMP_TAC[VSUBST_WELLTYPED; GSYM WELLTYPED; TERM_VALUATION_VALMOD] THEN
+ MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD; TERM_VALUATION_ITLIST] THEN
+ MAP_EVERY X_GEN_TAC [`u:string`; `uty:type`] THEN DISCH_TAC THENL
+ [EXPAND_TAC "ilist''" THEN REWRITE_TAC[ITLIST] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[DEST_VAR; VALMOD; PAIR_EQ] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[semantics; VALMOD];
+ ALL_TAC] THEN
+ EXPAND_TAC "ilist'" THEN ASM_SIMP_TAC[ITLIST_VALMOD_FILTER] THEN
+ REWRITE_TAC[VALMOD] THENL
+ [ALL_TAC;
+ REWRITE_TAC[PAIR_EQ] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
+ MATCH_MP_TAC ITLIST_VALMOD_EQ THEN ASM_REWRITE_TAC[VALMOD; PAIR_EQ] THEN
+ MAP_EVERY X_GEN_TAC [`s':term`; `s:term`] THEN STRIP_TAC THEN
+ FIRST_X_ASSUM(MP_TAC o C MATCH_MP
+ (ASSUME `MEM (s':term,s:term) ilist`)) THEN
+ DISCH_THEN(X_CHOOSE_THEN `w:string` MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `wty:type` MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
+ UNDISCH_TAC `DEST_VAR (Var w wty) = u,uty` THEN
+ REWRITE_TAC[DEST_VAR; PAIR_EQ] THEN
+ DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
+ MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ CONJ_TAC THENL [ASM_MESON_TAC[welltyped]; ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`v:string`; `vty:type`] THEN
+ DISCH_TAC THEN REWRITE_TAC[VALMOD; PAIR_EQ] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
+ FIRST_X_ASSUM(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
+ FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EX]) THEN
+ REWRITE_TAC[GSYM ALL_MEM] THEN
+ DISCH_THEN(MP_TAC o SPEC `(s':term,Var u uty)`) THEN
+ ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ ASM_REWRITE_TAC[] THEN EXPAND_TAC "ilist'" THEN
+ REWRITE_TAC[MEM_FILTER] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ ASM_REWRITE_TAC[term_INJ]] THEN
+ MP_TAC(ISPECL [`t':term`; `x:string`; `ty:type`] VARIANT) THEN
+ ASM_REWRITE_TAC[] THEN EXPAND_TAC "t'" THEN
+ REWRITE_TAC[VFREE_IN_VSUBST] THEN
+ REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b) = b ==> ~a`] THEN
+ DISCH_THEN(MP_TAC o SPECL [`u:string`; `uty:type`]) THEN
+ ASM_REWRITE_TAC[] THEN
+ SUBGOAL_THEN
+ `REV_ASSOCD (Var u uty) ilist' (Var u uty) =
+ REV_ASSOCD (Var u uty) ilist (Var u uty)`
+ SUBST1_TAC THENL
+ [EXPAND_TAC "ilist'" THEN REWRITE_TAC[REV_ASSOCD_FILTER] THEN
+ ASM_REWRITE_TAC[term_INJ];
+ ALL_TAC] THEN
+ UNDISCH_TAC
+ `!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty` THEN
+ SPEC_TAC(`ilist:(term#term)list`,`l:(term#term)list`) THEN
+ MATCH_MP_TAC list_INDUCT THEN
+ REWRITE_TAC[REV_ASSOCD; ITLIST; VFREE_IN; VALMOD; term_INJ] THEN
+ SIMP_TAC[PAIR_EQ] THEN REWRITE_TAC[FORALL_PAIR_THM] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[VALMOD; REV_ASSOCD; MEM] THEN
+ REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+ SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
+ REWRITE_TAC[WELLTYPED_CLAUSES; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
+ MAP_EVERY X_GEN_TAC [`t1:term`; `t2:term`; `i:(term#term)list`] THEN
+ DISCH_THEN(fun th ->
+ DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN MP_TAC th) THEN
+ FIRST_X_ASSUM(X_CHOOSE_THEN `v:string` MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `vty:type` MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
+ ASM_REWRITE_TAC[DEST_VAR; term_INJ; PAIR_EQ] THEN
+ SUBGOAL_THEN `(v:string = u) /\ (vty:type = uty) <=> (u = v) /\ (uty = vty)`
+ SUBST1_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
+ REPEAT STRIP_TAC THEN MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD; VALMOD] THEN
+ REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[welltyped; term_INJ]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Hence correctness of INST. *)
+(* ------------------------------------------------------------------------- *)
+
+let INST_correct = prove
+ (`!ilist asl p.
+ (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
+ ==> asl |= p ==> MAP (VSUBST ilist) asl |= VSUBST ilist p`,
+ REWRITE_TAC[sequent] THEN REPEAT STRIP_TAC THENL
+ [UNDISCH_TAC `ALL (\a. a has_type Bool) (CONS p asl)` THEN
+ REWRITE_TAC[ALL; ALL_MAP] THEN MATCH_MP_TAC MONO_AND THEN
+ CONJ_TAC THENL
+ [ALL_TAC;
+ MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
+ GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[o_THM]] THEN
+ DISCH_TAC THEN MATCH_MP_TAC VSUBST_HAS_TYPE THEN ASM_REWRITE_TAC[];
+ ALL_TAC] THEN
+ SUBGOAL_THEN `welltyped p` ASSUME_TAC THENL
+ [ASM_MESON_TAC[welltyped; ALL]; ALL_TAC] THEN
+ ASM_SIMP_TAC[SEMANTICS_VSUBST] THEN
+ FIRST_X_ASSUM MATCH_MP_TAC THEN
+ ASM_SIMP_TAC[TERM_VALUATION_ITLIST] THEN
+ FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ALL_MAP]) THEN
+ MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
+ X_GEN_TAC `a:term` THEN DISCH_TAC THEN
+ SUBGOAL_THEN `welltyped a` MP_TAC THENL
+ [ASM_MESON_TAC[ALL_MEM; MEM; welltyped]; ALL_TAC] THEN
+ ASM_SIMP_TAC[SEMANTICS_VSUBST; o_THM]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Lemma about typesets to simplify some later goals. *)
+(* ------------------------------------------------------------------------- *)
+
+let TYPESET_LEMMA = prove
+ (`!ty tau tyin.
+ typeset (\s. typeset tau (REV_ASSOCD (Tyvar s) tyin (Tyvar s))) ty =
+ typeset tau (TYPE_SUBST tyin ty)`,
+ MATCH_MP_TAC type_INDUCT THEN SIMP_TAC[typeset; TYPE_SUBST]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics of type instantiation core. *)
+(* ------------------------------------------------------------------------- *)
+
+let SEMANTICS_INST_CORE = prove
+ (`!n tm env tyin.
+ welltyped tm /\ (sizeof tm = n) /\
+ (!s s'. MEM (s,s') env
+ ==> ?x ty. (s = Var x ty) /\
+ (s' = Var x (TYPE_SUBST tyin ty)))
+ ==> (?x ty. (INST_CORE env tyin tm =
+ Clash(Var x (TYPE_SUBST tyin ty))) /\
+ VFREE_IN (Var x ty) tm /\
+ ~(REV_ASSOCD (Var x (TYPE_SUBST tyin ty))
+ env (Var x ty) = Var x ty)) \/
+ (!x ty. VFREE_IN (Var x ty) tm
+ ==> (REV_ASSOCD (Var x (TYPE_SUBST tyin ty))
+ env (Var x ty) = Var x ty)) /\
+ (?tm'. (INST_CORE env tyin tm = Result tm') /\
+ tm' has_type (TYPE_SUBST tyin (typeof tm)) /\
+ (!u uty. VFREE_IN (Var u uty) tm' <=>
+ ?oty. VFREE_IN (Var u oty) tm /\
+ (uty = TYPE_SUBST tyin oty)) /\
+ !sigma tau.
+ type_valuation tau /\ term_valuation tau sigma
+ ==> (semantics sigma tau tm' =
+ semantics
+ (\(x,ty). sigma(x,TYPE_SUBST tyin ty))
+ (\s. typeset tau (TYPE_SUBST tyin (Tyvar s)))
+ tm))`,
+ MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
+ MATCH_MP_TAC term_INDUCT THEN
+ ONCE_REWRITE_TAC[INST_CORE] THEN REWRITE_TAC[semantics] THEN
+ REPEAT CONJ_TAC THENL
+ [POP_ASSUM(K ALL_TAC) THEN
+ REWRITE_TAC[REV_ASSOCD; LET_DEF; LET_END_DEF] THEN
+ REPEAT GEN_TAC THEN COND_CASES_TAC THEN
+ ASM_REWRITE_TAC[result_DISTINCT; result_INJ; UNWIND_THM1] THEN
+ REWRITE_TAC[typeof; has_type_RULES] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[RESULT; semantics; VFREE_IN; term_INJ] THEN ASM_MESON_TAC[];
+ POP_ASSUM(K ALL_TAC) THEN
+ REWRITE_TAC[TYPE_SUBST; RESULT; VFREE_IN; term_DISTINCT] THEN
+ ASM_REWRITE_TAC[result_DISTINCT; result_INJ; UNWIND_THM1] THEN
+ REWRITE_TAC[typeof; has_type_RULES; TYPE_SUBST; VFREE_IN] THEN
+ REWRITE_TAC[semantics; typeset; TYPESET_LEMMA; TYPE_SUBST; term_DISTINCT];
+ POP_ASSUM(K ALL_TAC) THEN
+ REWRITE_TAC[TYPE_SUBST; RESULT; VFREE_IN; term_DISTINCT] THEN
+ ASM_REWRITE_TAC[result_DISTINCT; result_INJ; UNWIND_THM1] THEN
+ REWRITE_TAC[typeof; has_type_RULES; TYPE_SUBST; VFREE_IN] THEN
+ REWRITE_TAC[semantics; typeset; TYPESET_LEMMA; TYPE_SUBST; term_DISTINCT];
+ MAP_EVERY X_GEN_TAC [`s:term`; `t:term`] THEN DISCH_THEN(K ALL_TAC) THEN
+ POP_ASSUM MP_TAC THEN ASM_CASES_TAC `n = sizeof(Comb s t)` THEN
+ ASM_REWRITE_TAC[] THEN
+ DISCH_THEN(fun th -> MP_TAC(SPEC `sizeof t` th) THEN
+ MP_TAC(SPEC `sizeof s` th)) THEN
+ REWRITE_TAC[sizeof; ARITH_RULE `s < 1 + s + t /\ t < 1 + s + t`] THEN
+ DISCH_THEN(fun th -> DISCH_THEN(MP_TAC o SPEC `t:term`) THEN
+ MP_TAC(SPEC `s:term` th)) THEN
+ REWRITE_TAC[IMP_IMP; AND_FORALL_THM; WELLTYPED_CLAUSES] THEN
+ REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
+ DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN
+ GEN_REWRITE_TAC I [IMP_CONJ] THEN
+ DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
+ [DISCH_THEN(fun th -> DISCH_THEN(K ALL_TAC) THEN MP_TAC th) THEN
+ DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th) THEN
+ REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
+ STRIP_TAC THEN ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; IS_CLASH; VFREE_IN];
+ ALL_TAC] THEN
+ REWRITE_TAC[TYPE_SUBST] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `s':term` STRIP_ASSUME_TAC) THEN
+ DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
+ [DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th) THEN
+ REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
+ STRIP_TAC THEN ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; IS_CLASH; VFREE_IN];
+ ALL_TAC] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `t':term` STRIP_ASSUME_TAC) THEN
+ DISJ2_TAC THEN CONJ_TAC THENL
+ [REWRITE_TAC[VFREE_IN] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
+ EXISTS_TAC `Comb s' t'` THEN
+ ASM_SIMP_TAC[LET_DEF; LET_END_DEF; IS_CLASH; semantics; RESULT] THEN
+ ASM_REWRITE_TAC[VFREE_IN] THEN
+ ASM_REWRITE_TAC[typeof] THEN ONCE_REWRITE_TAC[has_type_CASES] THEN
+ REWRITE_TAC[term_DISTINCT; term_INJ; codomain] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN
+ DISCH_THEN(K ALL_TAC) THEN POP_ASSUM MP_TAC THEN
+ ASM_CASES_TAC `n = sizeof (Abs x ty t)` THEN ASM_REWRITE_TAC[] THEN
+ POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
+ REWRITE_TAC[WELLTYPED_CLAUSES] THEN STRIP_TAC THEN REPEAT LET_TAC THEN
+ FIRST_ASSUM(MP_TAC o SPEC `sizeof t`) THEN
+ REWRITE_TAC[sizeof; ARITH_RULE `t < 2 + t`] THEN
+ DISCH_THEN(MP_TAC o SPECL
+ [`t:term`; `env':(term#term)list`; `tyin:(type#type)list`]) THEN
+ ASM_REWRITE_TAC[] THEN
+ ANTS_TAC THENL
+ [EXPAND_TAC "env'" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
+ [ALL_TAC;
+ FIRST_X_ASSUM(K ALL_TAC o SPEC `0`) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `t':term` STRIP_ASSUME_TAC) THEN
+ DISJ2_TAC THEN ASM_REWRITE_TAC[IS_RESULT] THEN CONJ_TAC THENL
+ [FIRST_X_ASSUM(fun th ->
+ MP_TAC th THEN MATCH_MP_TAC MONO_FORALL THEN
+ GEN_TAC THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
+ DISCH_THEN(MP_TAC o check (is_imp o concl))) THEN
+ EXPAND_TAC "env'" THEN
+ REWRITE_TAC[VFREE_IN; REV_ASSOCD; term_INJ] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[term_INJ] THEN MESON_TAC[];
+ ALL_TAC] THEN
+ REWRITE_TAC[result_INJ; UNWIND_THM1; RESULT] THEN
+ MATCH_MP_TAC(TAUT `a /\ b /\ (b ==> c) ==> b /\ a /\ c`) THEN
+ CONJ_TAC THENL
+ [ASM_REWRITE_TAC[VFREE_IN; term_INJ] THEN
+ MAP_EVERY X_GEN_TAC [`u:string`; `uty:type`] THEN
+ ASM_CASES_TAC `u:string = x` THEN ASM_REWRITE_TAC[] THEN
+ UNDISCH_THEN `u:string = x` SUBST_ALL_TAC THEN
+ REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
+ AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
+ X_GEN_TAC `oty:type` THEN REWRITE_TAC[] THEN
+ ASM_CASES_TAC `uty = TYPE_SUBST tyin oty` THEN ASM_REWRITE_TAC[] THEN
+ ASM_CASES_TAC `VFREE_IN (Var x oty) t` THEN ASM_REWRITE_TAC[] THEN
+ EQ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
+ REWRITE_TAC[CONTRAPOS_THM] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
+ FIRST_X_ASSUM(fun th ->
+ MP_TAC(SPECL [`x:string`; `oty:type`] th) THEN
+ ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN NO_TAC; ALL_TAC]) THEN
+ EXPAND_TAC "env'" THEN REWRITE_TAC[REV_ASSOCD] THEN
+ ASM_MESON_TAC[term_INJ];
+ ALL_TAC] THEN
+ CONJ_TAC THENL
+ [REWRITE_TAC[typeof; TYPE_SUBST] THEN ASM_REWRITE_TAC[] THEN
+ ASM_MESON_TAC[has_type_RULES];
+ ALL_TAC] THEN
+ DISCH_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
+ REWRITE_TAC[semantics] THEN
+ ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
+ MATCH_MP_TAC ABSTRACT_EQ THEN
+ CONJ_TAC THENL [ASM_SIMP_TAC[TYPESET_INHABITED]; ALL_TAC] THEN
+ X_GEN_TAC `a:V` THEN REWRITE_TAC[] THEN DISCH_TAC THEN CONJ_TAC THENL
+ [MATCH_MP_TAC SEMANTICS_TYPESET THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ ASM_MESON_TAC[welltyped; WELLTYPED];
+ ALL_TAC] THEN
+ MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> a /\ b`) THEN CONJ_TAC THENL
+ [DISCH_THEN(SUBST1_TAC o SYM) THEN
+ MATCH_MP_TAC SEMANTICS_TYPESET THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD];
+ ALL_TAC] THEN
+ FIRST_X_ASSUM(MP_TAC o SPECL
+ [`(x,ty' |-> a) (sigma:(string#type)->V)`; `tau:string->V`]) THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN DISCH_TAC THEN
+ REWRITE_TAC[GSYM(CONJUNCT1 TYPE_SUBST)] THEN
+ MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN CONJ_TAC THENL
+ [REWRITE_TAC[type_valuation] THEN ASM_SIMP_TAC[TYPESET_INHABITED];
+ ALL_TAC] THEN
+ CONJ_TAC THENL
+ [REWRITE_TAC[term_valuation] THEN
+ MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[VALMOD; PAIR_EQ] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
+ ASM_MESON_TAC[term_valuation];
+ ALL_TAC] THEN
+ CONJ_TAC THENL
+ [REWRITE_TAC[term_valuation] THEN
+ MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
+ REWRITE_TAC[VALMOD] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[VALMOD; PAIR_EQ] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
+ ASM_MESON_TAC[term_valuation];
+ ALL_TAC] THEN
+ UNDISCH_THEN
+ `!u uty.
+ VFREE_IN (Var u uty) t' <=>
+ (?oty. VFREE_IN (Var u oty) t /\ (uty = TYPE_SUBST tyin oty))`
+ (K ALL_TAC) THEN
+ ASM_REWRITE_TAC[] THEN MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[VALMOD] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ ASM_CASES_TAC `y:string = x` THEN ASM_REWRITE_TAC[PAIR_EQ] THEN
+ ASM_CASES_TAC `yty:type = ty` THEN ASM_REWRITE_TAC[] THEN
+ UNDISCH_THEN `y:string = x` SUBST_ALL_TAC THEN COND_CASES_TAC THEN
+ ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
+ FIRST_X_ASSUM(MP_TAC o SPECL [`x:string`; `yty:type`]) THEN
+ ASM_REWRITE_TAC[] THEN EXPAND_TAC "env'" THEN
+ ASM_REWRITE_TAC[REV_ASSOCD; term_INJ]] THEN
+ DISCH_THEN(X_CHOOSE_THEN `z:string` (X_CHOOSE_THEN `zty:type`
+ (CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC))) THEN
+ EXPAND_TAC "w" THEN REWRITE_TAC[CLASH; IS_RESULT; term_INJ] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
+ [FIRST_X_ASSUM(K ALL_TAC o SPEC `0`) THEN
+ DISCH_THEN(fun th ->
+ DISJ1_TAC THEN REWRITE_TAC[result_INJ] THEN
+ MAP_EVERY EXISTS_TAC [`z:string`; `zty:type`] THEN
+ MP_TAC th) THEN
+ ASM_REWRITE_TAC[VFREE_IN; term_INJ] THEN
+ EXPAND_TAC "env'" THEN ASM_REWRITE_TAC[REV_ASSOCD; term_INJ] THEN
+ ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ FIRST_X_ASSUM(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN STRIP_TAC THEN
+ ONCE_REWRITE_TAC[INST_CORE] THEN ASM_REWRITE_TAC[] THEN
+ ONCE_REWRITE_TAC[letlemma] THEN
+ ABBREV_TAC `env'' = CONS (Var x' ty,Var x' ty') env` THEN
+ ONCE_REWRITE_TAC[letlemma] THEN
+ ABBREV_TAC
+ `ures = INST_CORE env'' tyin (VSUBST[Var x' ty,Var x ty] t)` THEN
+ ONCE_REWRITE_TAC[letlemma] THEN
+ FIRST_X_ASSUM(MP_TAC o SPEC `sizeof t`) THEN
+ REWRITE_TAC[sizeof; ARITH_RULE `t < 2 + t`] THEN
+ DISCH_THEN(fun th ->
+ MP_TAC(SPECL [`VSUBST [Var x' ty,Var x ty] t`;
+ `env'':(term#term)list`; `tyin:(type#type)list`] th) THEN
+ MP_TAC(SPECL [`t:term`; `[]:(term#term)list`; `tyin:(type#type)list`]
+ th)) THEN
+ REWRITE_TAC[MEM; REV_ASSOCD] THEN ASM_REWRITE_TAC[] THEN
+ DISCH_THEN(X_CHOOSE_THEN `t':term` MP_TAC) THEN STRIP_TAC THEN
+ UNDISCH_TAC `VARIANT (RESULT (INST_CORE [] tyin t)) x ty' = x'` THEN
+ ASM_REWRITE_TAC[RESULT] THEN DISCH_TAC THEN
+ MP_TAC(SPECL [`t':term`; `x:string`; `ty':type`] VARIANT) THEN
+ ASM_REWRITE_TAC[] THEN
+ GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
+ [NOT_EXISTS_THM; TAUT `~(a /\ b) <=> a ==> ~b`] THEN DISCH_TAC THEN
+ ANTS_TAC THENL
+ [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
+ [MATCH_MP_TAC VSUBST_WELLTYPED THEN ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN
+ ASM_MESON_TAC[has_type_RULES];
+ ALL_TAC] THEN
+ CONJ_TAC THENL
+ [MATCH_MP_TAC SIZEOF_VSUBST THEN
+ ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN ASM_MESON_TAC[has_type_RULES];
+ ALL_TAC] THEN
+ EXPAND_TAC "env''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
+ ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
+ [DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th) THEN
+ MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `v:string` THEN
+ MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `vty:type` THEN
+ ASM_REWRITE_TAC[] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC) THEN
+ ASM_REWRITE_TAC[IS_RESULT; CLASH] THEN
+ ONCE_REWRITE_TAC[letlemma] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
+ [REWRITE_TAC[VFREE_IN_VSUBST] THEN EXPAND_TAC "env''" THEN
+ REWRITE_TAC[REV_ASSOCD] THEN ASM_REWRITE_TAC[] THEN
+ DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
+ ASM_REWRITE_TAC[] THEN REWRITE_TAC[term_INJ] THEN
+ DISCH_THEN(REPEAT_TCL CHOOSE_THEN MP_TAC) THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[VFREE_IN; term_INJ] THEN
+ ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [term_INJ]) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
+ MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
+ EXPAND_TAC "env''" THEN REWRITE_TAC[REV_ASSOCD] THEN
+ ASM_CASES_TAC `vty:type = ty` THEN ASM_REWRITE_TAC[] THEN
+ DISCH_THEN(MP_TAC o CONJUNCT1) THEN
+ REWRITE_TAC[VFREE_IN_VSUBST; NOT_EXISTS_THM; REV_ASSOCD] THEN
+ ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN; term_INJ] THEN
+ MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
+ MP_TAC(SPECL [`t':term`; `x:string`; `ty':type`] VARIANT) THEN
+ ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `t'':term` STRIP_ASSUME_TAC) THEN
+ ASM_REWRITE_TAC[IS_RESULT; result_INJ; UNWIND_THM1; result_DISTINCT] THEN
+ REWRITE_TAC[RESULT] THEN
+ MATCH_MP_TAC(TAUT `b /\ (b ==> c /\ a /\ d) ==> a /\ b /\ c /\ d`) THEN
+ CONJ_TAC THENL
+ [ASM_REWRITE_TAC[typeof; TYPE_SUBST] THEN
+ MATCH_MP_TAC(last(CONJUNCTS has_type_RULES)) THEN
+ SUBGOAL_THEN `(VSUBST [Var x' ty,Var x ty] t) has_type (typeof t)`
+ (fun th -> ASM_MESON_TAC[th; WELLTYPED_LEMMA]) THEN
+ MATCH_MP_TAC VSUBST_HAS_TYPE THEN ASM_REWRITE_TAC[GSYM WELLTYPED] THEN
+ REWRITE_TAC[MEM; PAIR_EQ] THEN MESON_TAC[has_type_RULES];
+ ALL_TAC] THEN
+ DISCH_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
+ CONJ_TAC THENL
+ [ASM_REWRITE_TAC[VFREE_IN] THEN
+ MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
+ ASM_REWRITE_TAC[VFREE_IN_VSUBST; REV_ASSOCD] THEN
+ ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN; term_INJ] THEN
+ SIMP_TAC[] THEN
+ REWRITE_TAC[TAUT `x /\ (if p then a /\ b else c /\ b) <=>
+ b /\ x /\ (if p then a else c)`] THEN
+ REWRITE_TAC[UNWIND_THM2] THEN
+ REWRITE_TAC[TAUT `x /\ (if p /\ q then a else b) <=>
+ p /\ q /\ a /\ x \/ b /\ ~(p /\ q) /\ x`] THEN
+ REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM1; UNWIND_THM2] THEN
+ ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ DISCH_TAC THEN CONJ_TAC THENL
+ [MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
+ REWRITE_TAC[VFREE_IN] THEN STRIP_TAC THEN
+ UNDISCH_TAC `!x'' ty'.
+ VFREE_IN (Var x'' ty') (VSUBST [Var x' ty,Var x ty] t)
+ ==> (REV_ASSOCD (Var x'' (TYPE_SUBST tyin ty')) env''
+ (Var x'' ty') = Var x'' ty')` THEN
+ DISCH_THEN(MP_TAC o SPECL [`k:string`; `kty:type`]) THEN
+ REWRITE_TAC[VFREE_IN_VSUBST; REV_ASSOCD] THEN
+ ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN] THEN
+ REWRITE_TAC[VFREE_IN; term_INJ] THEN
+ SIMP_TAC[] THEN
+ REWRITE_TAC[TAUT `x /\ (if p then a /\ b else c /\ b) <=>
+ b /\ x /\ (if p then a else c)`] THEN
+ REWRITE_TAC[UNWIND_THM2] THEN
+ REWRITE_TAC[TAUT `x /\ (if p /\ q then a else b) <=>
+ p /\ q /\ a /\ x \/ b /\ ~(p /\ q) /\ x`] THEN
+ REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM1; UNWIND_THM2] THEN
+ UNDISCH_TAC `~(Var x ty = Var k kty)` THEN
+ REWRITE_TAC[term_INJ] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
+ EXPAND_TAC "env''" THEN REWRITE_TAC[REV_ASSOCD] THEN ASM_MESON_TAC[];
+ ALL_TAC] THEN
+ REPEAT STRIP_TAC THEN REWRITE_TAC[semantics] THEN
+ REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN ASM_REWRITE_TAC[] THEN
+ MATCH_MP_TAC ABSTRACT_EQ THEN
+ CONJ_TAC THENL [ASM_SIMP_TAC[TYPESET_INHABITED]; ALL_TAC] THEN
+ X_GEN_TAC `a:V` THEN REWRITE_TAC[] THEN DISCH_TAC THEN CONJ_TAC THENL
+ [MATCH_MP_TAC SEMANTICS_TYPESET THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ ASM_MESON_TAC[welltyped; WELLTYPED];
+ ALL_TAC] THEN
+ MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> a /\ b`) THEN CONJ_TAC THENL
+ [DISCH_THEN(SUBST1_TAC o SYM) THEN
+ MATCH_MP_TAC SEMANTICS_TYPESET THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN
+ SUBGOAL_THEN `(VSUBST [Var x' ty,Var x ty] t) has_type (typeof t)`
+ (fun th -> ASM_MESON_TAC[th; WELLTYPED_LEMMA]) THEN
+ MATCH_MP_TAC VSUBST_HAS_TYPE THEN ASM_REWRITE_TAC[GSYM WELLTYPED] THEN
+ REWRITE_TAC[MEM; PAIR_EQ] THEN MESON_TAC[has_type_RULES];
+ ALL_TAC] THEN
+ W(fun (asl,w) -> FIRST_X_ASSUM(fun th ->
+ MP_TAC(PART_MATCH (lhand o rand) th (lhand w)))) THEN
+ ASM_SIMP_TAC[TERM_VALUATION_VALMOD] THEN DISCH_TAC THEN
+ REWRITE_TAC[GSYM(CONJUNCT1 TYPE_SUBST)] THEN
+ MP_TAC SEMANTICS_VSUBST THEN
+ REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
+ DISCH_THEN(fun th ->
+ W(fun (asl,w) -> MP_TAC(PART_MATCH (lhand o rand) th (lhand w)))) THEN
+ ANTS_TAC THENL
+ [ASM_REWRITE_TAC[MEM; PAIR_EQ] THEN CONJ_TAC THENL
+ [MESON_TAC[has_type_RULES]; ALL_TAC] THEN
+ CONJ_TAC THENL
+ [REWRITE_TAC[type_valuation] THEN ASM_SIMP_TAC[TYPESET_INHABITED];
+ ALL_TAC] THEN
+ REWRITE_TAC[term_valuation] THEN
+ MAP_EVERY X_GEN_TAC [`y:string`; `yty:type`] THEN
+ REWRITE_TAC[VALMOD] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[VALMOD; PAIR_EQ] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
+ ASM_MESON_TAC[term_valuation];
+ ALL_TAC] THEN
+ DISCH_THEN SUBST1_TAC THEN
+ REWRITE_TAC[GSYM(CONJUNCT1 TYPE_SUBST)] THEN
+ MATCH_MP_TAC TERM_VALUATION_VFREE_IN THEN CONJ_TAC THENL
+ [REWRITE_TAC[type_valuation] THEN ASM_SIMP_TAC[TYPESET_INHABITED];
+ ALL_TAC] THEN
+ REWRITE_TAC[ITLIST] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[DEST_VAR] THEN REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
+ [ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
+ REWRITE_TAC[term_valuation; semantics] THEN
+ MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN
+ REWRITE_TAC[VALMOD] THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[TYPESET_LEMMA; TYPE_SUBST] THEN
+ SIMP_TAC[PAIR_EQ] THEN ASM_REWRITE_TAC[] THEN
+ COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
+ ASM_MESON_TAC[term_valuation];
+ ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`k:string`; `kty:type`] THEN DISCH_TAC THEN
+ REWRITE_TAC[VALMOD; semantics] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ SIMP_TAC[PAIR_EQ] THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* So in particular, we get key properties of INST itself. *)
+(* ------------------------------------------------------------------------- *)
+
+let SEMANTICS_INST = prove
+ (`!tyin tm.
+ welltyped tm
+ ==> (INST tyin tm) has_type (TYPE_SUBST tyin (typeof tm)) /\
+ (!u uty. VFREE_IN (Var u uty) (INST tyin tm) <=>
+ ?oty. VFREE_IN (Var u oty) tm /\
+ (uty = TYPE_SUBST tyin oty)) /\
+ !sigma tau.
+ type_valuation tau /\ term_valuation tau sigma
+ ==> (semantics sigma tau (INST tyin tm) =
+ semantics
+ (\(x,ty). sigma(x,TYPE_SUBST tyin ty))
+ (\s. typeset tau (TYPE_SUBST tyin (Tyvar s))) tm)`,
+ REPEAT GEN_TAC THEN STRIP_TAC THEN
+ MP_TAC(SPECL [`sizeof tm`; `tm:term`; `[]:(term#term)list`;
+ `tyin:(type#type)list`] SEMANTICS_INST_CORE) THEN
+ ASM_REWRITE_TAC[MEM; INST_DEF; REV_ASSOCD] THEN MESON_TAC[RESULT]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Hence soundness of the INST_TYPE rule. *)
+(* ------------------------------------------------------------------------- *)
+
+let INST_TYPE_correct = prove
+ (`!tyin asl p. asl |= p ==> MAP (INST tyin) asl |= INST tyin p`,
+ REWRITE_TAC[sequent] THEN REPEAT STRIP_TAC THENL
+ [UNDISCH_TAC `ALL (\a. a has_type Bool) (CONS p asl)` THEN
+ REWRITE_TAC[ALL; ALL_MAP] THEN MATCH_MP_TAC MONO_AND THEN
+ CONJ_TAC THENL
+ [ALL_TAC;
+ MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
+ GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[o_THM]] THEN
+ ASM_MESON_TAC[SEMANTICS_INST; TYPE_SUBST; welltyped; WELLTYPED;
+ WELLTYPED_LEMMA];
+ ALL_TAC] THEN
+ SUBGOAL_THEN `welltyped p` ASSUME_TAC THENL
+ [ASM_MESON_TAC[welltyped; ALL]; ALL_TAC] THEN
+ ASM_SIMP_TAC[SEMANTICS_INST] THEN
+ FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL
+ [REWRITE_TAC[type_valuation] THEN ASM_MESON_TAC[TYPESET_INHABITED];
+ ALL_TAC] THEN
+ CONJ_TAC THENL
+ [REWRITE_TAC[term_valuation] THEN
+ REWRITE_TAC[TYPE_SUBST; TYPESET_LEMMA] THEN
+ ASM_MESON_TAC[term_valuation];
+ ALL_TAC] THEN
+ FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ALL_MAP]) THEN
+ MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ALL_IMP) THEN
+ X_GEN_TAC `a:term` THEN DISCH_TAC THEN
+ SUBGOAL_THEN `welltyped a` MP_TAC THENL
+ [ASM_MESON_TAC[ALL_MEM; MEM; welltyped]; ALL_TAC] THEN
+ ASM_SIMP_TAC[SEMANTICS_INST; o_THM]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Soundness. *)
+(* ------------------------------------------------------------------------- *)
+
+let HOL_IS_SOUND = prove
+ (`!asl p. asl |- p ==> asl |= p`,
+ MATCH_MP_TAC proves_INDUCT THEN
+ REWRITE_TAC[REFL_correct; TRANS_correct; ABS_correct;
+ BETA_correct; ASSUME_correct; EQ_MP_correct; INST_TYPE_correct;
+ REWRITE_RULE[LET_DEF; LET_END_DEF] DEDUCT_ANTISYM_RULE_correct;
+ REWRITE_RULE[IMP_IMP] INST_correct] THEN
+ REPEAT STRIP_TAC THEN MATCH_MP_TAC MK_COMB_correct THEN
+ ASM_MESON_TAC[WELLTYPED_CLAUSES; MK_COMB_correct]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Consistency. *)
+(* ------------------------------------------------------------------------- *)
+
+let HOL_IS_CONSISTENT = prove
+ (`?p. p has_type Bool /\ ~([] |- p)`,
+ SUBGOAL_THEN `?p. p has_type Bool /\ ~([] |= p)`
+ (fun th -> MESON_TAC[th; HOL_IS_SOUND]) THEN
+ EXISTS_TAC `Var x Bool === Var (VARIANT (Var x Bool) x Bool) Bool` THEN
+ SIMP_TAC[EQUATION_HAS_TYPE_BOOL; WELLTYPED_CLAUSES; typeof;
+ sequent; ALL; SEMANTICS_EQUATION; has_type_RULES; semantics;
+ BOOLEAN_EQ_TRUE] THEN
+ MP_TAC(SPECL [`Var x Bool`; `x:string`; `Bool`] VARIANT) THEN
+ ABBREV_TAC `y = VARIANT (Var x Bool) x Bool` THEN
+ REWRITE_TAC[VFREE_IN; term_INJ; NOT_FORALL_THM] THEN DISCH_TAC THEN
+ EXISTS_TAC `((x:string,Bool) |-> false) (((y,Bool) |-> true)
+ (\(x,ty). @a. a <: typeset (\x. boolset) ty))` THEN
+ EXISTS_TAC `\x:string. boolset` THEN
+ ASM_REWRITE_TAC[type_valuation; VALMOD; PAIR_EQ; TRUE_NE_FALSE] THEN
+ CONJ_TAC THENL [MESON_TAC[IN_BOOL]; ALL_TAC] THEN
+ REWRITE_TAC[term_valuation] THEN REPEAT GEN_TAC THEN
+ REWRITE_TAC[VALMOD; PAIR_EQ] THEN
+ REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[typeset; IN_BOOL]) THEN
+ CONV_TAC SELECT_CONV THEN MATCH_MP_TAC TYPESET_INHABITED THEN
+ REWRITE_TAC[type_valuation] THEN MESON_TAC[IN_BOOL]);;
--- /dev/null
+(* ========================================================================= *)
+(* Syntactic definitions for "core HOL", including provability. *)
+(* ========================================================================= *)
+
+(* ------------------------------------------------------------------------- *)
+(* HOL types. Just do the primitive ones for now. *)
+(* ------------------------------------------------------------------------- *)
+
+let type_INDUCT,type_RECURSION = define_type
+ "type = Tyvar string
+ | Bool
+ | Ind
+ | Fun type type";;
+
+let type_DISTINCT = distinctness "type";;
+
+let type_INJ = injectivity "type";;
+
+let domain = define
+ `domain (Fun s t) = s`;;
+
+let codomain = define
+ `codomain (Fun s t) = t`;;
+
+(* ------------------------------------------------------------------------- *)
+(* HOL terms. To avoid messing round with specification of the language, *)
+(* we just put "=" and "@" in as the only constants. For now... *)
+(* ------------------------------------------------------------------------- *)
+
+let term_INDUCT,term_RECURSION = define_type
+ "term = Var string type
+ | Equal type | Select type
+ | Comb term term
+ | Abs string type term";;
+
+let term_DISTINCT = distinctness "term";;
+
+let term_INJ = injectivity "term";;
+
+(* ------------------------------------------------------------------------- *)
+(* Typing judgements. *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("has_type",(12,"right"));;
+
+let has_type_RULES,has_type_INDUCT,has_type_CASES = new_inductive_definition
+ `(!n ty. (Var n ty) has_type ty) /\
+ (!ty. (Equal ty) has_type (Fun ty (Fun ty Bool))) /\
+ (!ty. (Select ty) has_type (Fun (Fun ty Bool) ty)) /\
+ (!s t dty rty. s has_type (Fun dty rty) /\ t has_type dty
+ ==> (Comb s t) has_type rty) /\
+ (!n dty t rty. t has_type rty ==> (Abs n dty t) has_type (Fun dty rty))`;;
+
+let welltyped = new_definition
+ `welltyped tm <=> ?ty. tm has_type ty`;;
+
+let typeof = define
+ `(typeof (Var n ty) = ty) /\
+ (typeof (Equal ty) = Fun ty (Fun ty Bool)) /\
+ (typeof (Select ty) = Fun (Fun ty Bool) ty) /\
+ (typeof (Comb s t) = codomain (typeof s)) /\
+ (typeof (Abs n ty t) = Fun ty (typeof t))`;;
+
+let WELLTYPED_LEMMA = prove
+ (`!tm ty. tm has_type ty ==> (typeof tm = ty)`,
+ MATCH_MP_TAC has_type_INDUCT THEN
+ SIMP_TAC[typeof; has_type_RULES; codomain]);;
+
+let WELLTYPED = prove
+ (`!tm. welltyped tm <=> tm has_type (typeof tm)`,
+ REWRITE_TAC[welltyped] THEN MESON_TAC[WELLTYPED_LEMMA]);;
+
+let WELLTYPED_CLAUSES = prove
+ (`(!n ty. welltyped(Var n ty)) /\
+ (!ty. welltyped(Equal ty)) /\
+ (!ty. welltyped(Select ty)) /\
+ (!s t. welltyped (Comb s t) <=>
+ welltyped s /\ welltyped t /\
+ ?rty. typeof s = Fun (typeof t) rty) /\
+ (!n ty t. welltyped (Abs n ty t) = welltyped t)`,
+ REPEAT STRIP_TAC THEN REWRITE_TAC[welltyped] THEN
+ (GEN_REWRITE_TAC BINDER_CONV [has_type_CASES] ORELSE
+ GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [has_type_CASES]) THEN
+ REWRITE_TAC[term_INJ; term_DISTINCT] THEN
+ MESON_TAC[WELLTYPED; WELLTYPED_LEMMA]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Since equations are important, a bit of derived syntax. *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("===",(18,"right"));;
+
+let equation = new_definition
+ `(s === t) = Comb (Comb (Equal(typeof s)) s) t`;;
+
+let EQUATION_HAS_TYPE_BOOL = prove
+ (`!s t. (s === t) has_type Bool
+ <=> welltyped s /\ welltyped t /\ (typeof s = typeof t)`,
+ REWRITE_TAC[equation] THEN
+ ONCE_REWRITE_TAC[has_type_CASES] THEN
+ REWRITE_TAC[term_DISTINCT; term_INJ] THEN
+ REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
+ REWRITE_TAC[UNWIND_THM1] THEN REPEAT GEN_TAC THEN
+ GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o LAND_CONV) [has_type_CASES] THEN
+ REWRITE_TAC[term_DISTINCT; term_INJ] THEN
+ REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
+ REWRITE_TAC[UNWIND_THM1] THEN
+ GEN_REWRITE_TAC (LAND_CONV o funpow 2(BINDER_CONV o LAND_CONV))
+ [has_type_CASES] THEN
+ REWRITE_TAC[term_DISTINCT; term_INJ; type_INJ] THEN
+ MESON_TAC[WELLTYPED; WELLTYPED_LEMMA]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Alpha-conversion. *)
+(* ------------------------------------------------------------------------- *)
+
+let ALPHAVARS = define
+ `(ALPHAVARS [] tmp <=> (FST tmp = SND tmp)) /\
+ (ALPHAVARS (CONS tp oenv) tmp <=>
+ (tmp = tp) \/
+ ~(FST tp = FST tmp) /\ ~(SND tp = SND tmp) /\ ALPHAVARS oenv tmp)`;;
+
+let RACONV_RULES,RACONV_INDUCT,RACONV_CASES = new_inductive_definition
+ `(!env x1 ty1 x2 ty2.
+ ALPHAVARS env (Var x1 ty1,Var x2 ty2)
+ ==> RACONV env (Var x1 ty1,Var x2 ty2)) /\
+ (!env ty. RACONV env (Equal ty,Equal ty)) /\
+ (!env ty. RACONV env (Select ty,Select ty)) /\
+ (!env s1 t1 s2 t2.
+ RACONV env (s1,s2) /\ RACONV env (t1,t2)
+ ==> RACONV env (Comb s1 t1,Comb s2 t2)) /\
+ (!env x1 ty1 t1 x2 ty2 t2.
+ (ty1 = ty2) /\ RACONV (CONS ((Var x1 ty1),(Var x2 ty2)) env) (t1,t2)
+ ==> RACONV env (Abs x1 ty1 t1,Abs x2 ty2 t2))`;;
+
+let RACONV = prove
+ (`(RACONV env (Var x1 ty1,Var x2 ty2) <=>
+ ALPHAVARS env (Var x1 ty1,Var x2 ty2)) /\
+ (RACONV env (Var x1 ty1,Equal ty2) <=> F) /\
+ (RACONV env (Var x1 ty1,Select ty2) <=> F) /\
+ (RACONV env (Var x1 ty1,Comb l2 r2) <=> F) /\
+ (RACONV env (Var x1 ty1,Abs x2 ty2 t2) <=> F) /\
+ (RACONV env (Equal ty1,Var x2 ty2) <=> F) /\
+ (RACONV env (Equal ty1,Equal ty2) <=> (ty1 = ty2)) /\
+ (RACONV env (Equal ty1,Select ty2) <=> F) /\
+ (RACONV env (Equal ty1,Comb l2 r2) <=> F) /\
+ (RACONV env (Equal ty1,Abs x2 ty2 t2) <=> F) /\
+ (RACONV env (Select ty1,Var x2 ty2) <=> F) /\
+ (RACONV env (Select ty1,Equal ty2) <=> F) /\
+ (RACONV env (Select ty1,Select ty2) <=> (ty1 = ty2)) /\
+ (RACONV env (Select ty1,Comb l2 r2) <=> F) /\
+ (RACONV env (Select ty1,Abs x2 ty2 t2) <=> F) /\
+ (RACONV env (Comb l1 r1,Var x2 ty2) <=> F) /\
+ (RACONV env (Comb l1 r1,Equal ty2) <=> F) /\
+ (RACONV env (Comb l1 r1,Select ty2) <=> F) /\
+ (RACONV env (Comb l1 r1,Comb l2 r2) <=>
+ RACONV env (l1,l2) /\ RACONV env (r1,r2)) /\
+ (RACONV env (Comb l1 r1,Abs x2 ty2 t2) <=> F) /\
+ (RACONV env (Abs x1 ty1 t1,Var x2 ty2) <=> F) /\
+ (RACONV env (Abs x1 ty1 t1,Equal ty2) <=> F) /\
+ (RACONV env (Abs x1 ty1 t1,Select ty2) <=> F) /\
+ (RACONV env (Abs x1 ty1 t1,Comb l2 r2) <=> F) /\
+ (RACONV env (Abs x1 ty1 t1,Abs x2 ty2 t2) <=>
+ (ty1 = ty2) /\ RACONV (CONS (Var x1 ty1,Var x2 ty2) env) (t1,t2))`,
+ REPEAT CONJ_TAC THEN
+ GEN_REWRITE_TAC LAND_CONV [RACONV_CASES] THEN
+ REWRITE_TAC[term_INJ; term_DISTINCT; PAIR_EQ] THEN MESON_TAC[]);;
+
+let ACONV = new_definition
+ `ACONV t1 t2 <=> RACONV [] (t1,t2)`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Reflexivity. *)
+(* ------------------------------------------------------------------------- *)
+
+let ALPHAVARS_REFL = prove
+ (`!env t. ALL (\(s,t). s = t) env ==> ALPHAVARS env (t,t)`,
+ MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[ALL; ALPHAVARS] THEN
+ REWRITE_TAC[FORALL_PAIR_THM] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN MESON_TAC[PAIR_EQ]);;
+
+let RACONV_REFL = prove
+ (`!t env. ALL (\(s,t). s = t) env ==> RACONV env (t,t)`,
+ MATCH_MP_TAC term_INDUCT THEN
+ REWRITE_TAC[RACONV] THEN REPEAT STRIP_TAC THENL
+ [ASM_SIMP_TAC[ALPHAVARS_REFL];
+ ASM_MESON_TAC[];
+ ASM_MESON_TAC[];
+ FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[ALL] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN ASM_REWRITE_TAC[]]);;
+
+let ACONV_REFL = prove
+ (`!t. ACONV t t`,
+ REWRITE_TAC[ACONV] THEN SIMP_TAC[RACONV_REFL; ALL]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Alpha-convertible terms have the same type (if welltyped). *)
+(* ------------------------------------------------------------------------- *)
+
+let ALPHAVARS_TYPE = prove
+ (`!env s t. ALPHAVARS env (s,t) /\
+ ALL (\(x,y). welltyped x /\ welltyped y /\
+ (typeof x = typeof y)) env /\
+ welltyped s /\ welltyped t
+ ==> (typeof s = typeof t)`,
+ MATCH_MP_TAC list_INDUCT THEN
+ REWRITE_TAC[FORALL_PAIR_THM; ALPHAVARS; ALL; PAIR_EQ] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ CONJ_TAC THENL [SIMP_TAC[]; ALL_TAC] THEN REPEAT STRIP_TAC THEN
+ ASM_MESON_TAC[]);;
+
+let RACONV_TYPE = prove
+ (`!env p. RACONV env p
+ ==> ALL (\(x,y). welltyped x /\ welltyped y /\
+ (typeof x = typeof y)) env /\
+ welltyped (FST p) /\ welltyped (SND p)
+ ==> (typeof (FST p) = typeof (SND p))`,
+ MATCH_MP_TAC RACONV_INDUCT THEN
+ REWRITE_TAC[FORALL_PAIR_THM; typeof] THEN REPEAT STRIP_TAC THENL
+ [ASM_MESON_TAC[typeof; ALPHAVARS_TYPE];
+ AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
+ ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[WELLTYPED_CLAUSES];
+ ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
+ ASM_REWRITE_TAC[ALL] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[typeof] THEN ASM_MESON_TAC[WELLTYPED_CLAUSES]]);;
+
+let ACONV_TYPE = prove
+ (`!s t. ACONV s t ==> welltyped s /\ welltyped t ==> (typeof s = typeof t)`,
+ REPEAT GEN_TAC THEN
+ MP_TAC(SPECL [`[]:(term#term)list`; `(s:term,t:term)`] RACONV_TYPE) THEN
+ REWRITE_TAC[ACONV; ALL] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* HOL version of "term_union". *)
+(* ------------------------------------------------------------------------- *)
+
+let TERM_UNION = define
+ `(TERM_UNION [] l2 = l2) /\
+ (TERM_UNION (CONS h t) l2 =
+ let subun = TERM_UNION t l2 in
+ if EX (ACONV h) subun then subun else CONS h subun)`;;
+
+let TERM_UNION_NONEW = prove
+ (`!l1 l2 x. MEM x (TERM_UNION l1 l2) ==> MEM x l1 \/ MEM x l2`,
+ LIST_INDUCT_TAC THEN REWRITE_TAC[TERM_UNION; MEM] THEN
+ LET_TAC THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
+ REWRITE_TAC[MEM] THEN ASM_MESON_TAC[ACONV_REFL]);;
+
+let TERM_UNION_THM = prove
+ (`!l1 l2 x. MEM x l1 \/ MEM x l2
+ ==> ?y. MEM y (TERM_UNION l1 l2) /\ ACONV x y`,
+ LIST_INDUCT_TAC THEN REWRITE_TAC[TERM_UNION; MEM; GSYM EX_MEM] THENL
+ [MESON_TAC[ACONV_REFL]; ALL_TAC] THEN
+ REPEAT GEN_TAC THEN LET_TAC THEN COND_CASES_TAC THEN STRIP_TAC THEN
+ ASM_REWRITE_TAC[MEM] THEN ASM_MESON_TAC[ACONV_REFL]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Handy lemma for using it in a sequent. *)
+(* ------------------------------------------------------------------------- *)
+
+let ALL_BOOL_TERM_UNION = prove
+ (`ALL (\a. a has_type Bool) l1 /\ ALL (\a. a has_type Bool) l2
+ ==> ALL (\a. a has_type Bool) (TERM_UNION l1 l2)`,
+ REWRITE_TAC[GSYM ALL_MEM] THEN MESON_TAC[TERM_UNION_NONEW]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Whether a variable/constant is free in a term. *)
+(* ------------------------------------------------------------------------- *)
+
+let VFREE_IN = define
+ `(VFREE_IN v (Var x ty) <=> (Var x ty = v)) /\
+ (VFREE_IN v (Equal ty) <=> (Equal ty = v)) /\
+ (VFREE_IN v (Select ty) <=> (Select ty = v)) /\
+ (VFREE_IN v (Comb s t) <=> VFREE_IN v s \/ VFREE_IN v t) /\
+ (VFREE_IN v (Abs x ty t) <=> ~(Var x ty = v) /\ VFREE_IN v t)`;;
+
+let VFREE_IN_RACONV = prove
+ (`!env p. RACONV env p
+ ==> !x ty. VFREE_IN (Var x ty) (FST p) /\
+ ~(?y. MEM (Var x ty,y) env) <=>
+ VFREE_IN (Var x ty) (SND p) /\
+ ~(?y. MEM (y,Var x ty) env)`,
+ MATCH_MP_TAC RACONV_INDUCT THEN REWRITE_TAC[VFREE_IN; term_DISTINCT] THEN
+ REWRITE_TAC[PAIR_EQ; term_INJ; MEM] THEN CONJ_TAC THENL
+ [ALL_TAC; MESON_TAC[]] THEN
+ MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[ALPHAVARS] THEN
+ REWRITE_TAC[MEM; FORALL_PAIR_THM; term_INJ; PAIR_EQ] THEN
+ CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
+ REPEAT GEN_TAC THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
+ MESON_TAC[]);;
+
+let VFREE_IN_ACONV = prove
+ (`!s t x t. ACONV s t ==> (VFREE_IN (Var x ty) s <=> VFREE_IN (Var x ty) t)`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[ACONV] THEN
+ DISCH_THEN(MP_TAC o MATCH_MP VFREE_IN_RACONV) THEN
+ SIMP_TAC[MEM; FST; SND]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Auxiliary association list function. *)
+(* ------------------------------------------------------------------------- *)
+
+let REV_ASSOCD = define
+ `(REV_ASSOCD a [] d = d) /\
+ (REV_ASSOCD a (CONS (x,y) t) d =
+ if y = a then x else REV_ASSOCD a t d)`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Substition of types in types. *)
+(* ------------------------------------------------------------------------- *)
+
+let TYPE_SUBST = define
+ `(TYPE_SUBST i (Tyvar v) = REV_ASSOCD (Tyvar v) i (Tyvar v)) /\
+ (TYPE_SUBST i Bool = Bool) /\
+ (TYPE_SUBST i Ind = Ind) /\
+ (TYPE_SUBST i (Fun ty1 ty2) = Fun (TYPE_SUBST i ty1) (TYPE_SUBST i ty2))`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Variant function. Deliberately underspecified at the moment. In a bid to *)
+(* expunge use of sets, just pick it distinct from what's free in a term. *)
+(* ------------------------------------------------------------------------- *)
+
+let VFREE_IN_FINITE = prove
+ (`!t. FINITE {x | VFREE_IN x t}`,
+ MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VFREE_IN] THEN
+ REWRITE_TAC[SET_RULE `{x | a = x} = {a}`;
+ SET_RULE `{x | P x \/ Q x} = {x | P x} UNION {x | Q x}`;
+ SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN
+ SIMP_TAC[FINITE_INSERT; FINITE_RULES; FINITE_UNION; FINITE_INTER]);;
+
+let VFREE_IN_FINITE_ALT = prove
+ (`!t ty. FINITE {x | VFREE_IN (Var x ty) t}`,
+ REPEAT GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
+ EXISTS_TAC `IMAGE (\(Var x ty). x) {x | VFREE_IN x t}` THEN
+ SIMP_TAC[VFREE_IN_FINITE; FINITE_IMAGE] THEN
+ REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_THM] THEN
+ X_GEN_TAC `x:string` THEN DISCH_TAC THEN
+ EXISTS_TAC `Var x ty` THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ ASM_REWRITE_TAC[]);;
+
+let VARIANT_EXISTS = prove
+ (`!t x:string ty. ?x'. ~(VFREE_IN (Var x' ty) t)`,
+ REPEAT STRIP_TAC THEN
+ MP_TAC(SPECL [`t:term`; `ty:type`] VFREE_IN_FINITE_ALT) THEN
+ DISCH_THEN(MP_TAC o CONJ string_INFINITE) THEN
+ DISCH_THEN(MP_TAC o MATCH_MP INFINITE_DIFF_FINITE) THEN
+ DISCH_THEN(MP_TAC o MATCH_MP INFINITE_NONEMPTY) THEN
+ REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_DIFF; IN_ELIM_THM; IN_UNIV]);;
+
+let VARIANT = new_specification ["VARIANT"]
+ (PURE_REWRITE_RULE[SKOLEM_THM] VARIANT_EXISTS);;
+
+(* ------------------------------------------------------------------------- *)
+(* Term substitution. *)
+(* ------------------------------------------------------------------------- *)
+
+let VSUBST = define
+ `(VSUBST ilist (Var x ty) = REV_ASSOCD (Var x ty) ilist (Var x ty)) /\
+ (VSUBST ilist (Equal ty) = Equal ty) /\
+ (VSUBST ilist (Select ty) = Select ty) /\
+ (VSUBST ilist (Comb s t) = Comb (VSUBST ilist s) (VSUBST ilist t)) /\
+ (VSUBST ilist (Abs x ty t) =
+ let ilist' = FILTER (\(s',s). ~(s = Var x ty)) ilist in
+ let t' = VSUBST ilist' t in
+ if EX (\(s',s). VFREE_IN (Var x ty) s' /\ VFREE_IN s t) ilist'
+ then let z = VARIANT t' x ty in
+ let ilist'' = CONS (Var z ty,Var x ty) ilist' in
+ Abs z ty (VSUBST ilist'' t)
+ else Abs x ty t')`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Preservation of type. *)
+(* ------------------------------------------------------------------------- *)
+
+let VSUBST_HAS_TYPE = prove
+ (`!tm ty ilist.
+ tm has_type ty /\
+ (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
+ ==> (VSUBST ilist tm) has_type ty`,
+ MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VSUBST] THEN
+ REPEAT CONJ_TAC THENL
+ [MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `tty:type`] THEN
+ MATCH_MP_TAC list_INDUCT THEN
+ SIMP_TAC[REV_ASSOCD; MEM; FORALL_PAIR_THM] THEN
+ REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+ SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; PAIR_EQ] THEN
+ REWRITE_TAC[ LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
+ ASM_CASES_TAC `(Var x ty) has_type tty` THEN ASM_REWRITE_TAC[] THEN
+ FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_type_CASES]) THEN
+ REWRITE_TAC[term_DISTINCT; term_INJ; LEFT_EXISTS_AND_THM] THEN
+ REWRITE_TAC[GSYM EXISTS_REFL] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
+ MAP_EVERY X_GEN_TAC [`s:term`; `u:term`; `ilist:(term#term)list`] THEN
+ DISCH_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
+ FIRST_X_ASSUM(X_CHOOSE_THEN `y:string` MP_TAC) THEN
+ DISCH_THEN(X_CHOOSE_THEN `aty:type` MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
+ ASM_MESON_TAC[term_INJ];
+ SIMP_TAC[];
+ SIMP_TAC[];
+ MAP_EVERY X_GEN_TAC [`s:term`; `t:term`] THEN REPEAT STRIP_TAC THEN
+ FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_type_CASES]) THEN
+ REWRITE_TAC[term_DISTINCT; term_INJ; GSYM CONJ_ASSOC] THEN
+ REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
+ DISCH_THEN(X_CHOOSE_THEN `dty:type` STRIP_ASSUME_TAC) THEN
+ MATCH_MP_TAC(el 3 (CONJUNCTS has_type_RULES)) THEN
+ EXISTS_TAC `dty:type` THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
+ ASM_REWRITE_TAC[];
+ ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN DISCH_TAC THEN
+ MAP_EVERY X_GEN_TAC [`fty:type`; `ilist:(term#term)list`] THEN STRIP_TAC THEN
+ LET_TAC THEN LET_TAC THEN
+ FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_type_CASES]) THEN
+ REWRITE_TAC[term_DISTINCT; term_INJ; GSYM CONJ_ASSOC] THEN
+ REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
+ DISCH_THEN(X_CHOOSE_THEN `rty:type` MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC) THEN DISCH_TAC THEN
+ COND_CASES_TAC THEN REPEAT LET_TAC THEN
+ MATCH_MP_TAC(el 4 (CONJUNCTS has_type_RULES)) THEN
+ EXPAND_TAC "t'" THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THENL
+ [MAP_EVERY EXPAND_TAC ["ilist''"; "ilist'"]; EXPAND_TAC "ilist'"] THEN
+ REWRITE_TAC[MEM; MEM_FILTER] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ REWRITE_TAC[PAIR_EQ] THEN ASM_MESON_TAC[has_type_RULES]);;
+
+let VSUBST_WELLTYPED = prove
+ (`!tm ty ilist.
+ welltyped tm /\
+ (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty)
+ ==> welltyped (VSUBST ilist tm)`,
+ MESON_TAC[VSUBST_HAS_TYPE; welltyped]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Right set of free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+let REV_ASSOCD_FILTER = prove
+ (`!l:(B#A)list a b d.
+ REV_ASSOCD a (FILTER (\(y,x). P x) l) b =
+ if P a then REV_ASSOCD a l b else b`,
+ MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[REV_ASSOCD; FILTER; COND_ID] THEN
+ REWRITE_TAC[FORALL_PAIR_THM] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ MAP_EVERY X_GEN_TAC [`y:B`; `x:A`; `l:(B#A)list`] THEN
+ REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REV_ASSOCD] THEN
+ ASM_CASES_TAC `(P:A->bool) x` THEN ASM_REWRITE_TAC[REV_ASSOCD] THEN
+ ASM_MESON_TAC[]);;
+
+let VFREE_IN_VSUBST = prove
+ (`!tm u uty ilist.
+ VFREE_IN (Var u uty) (VSUBST ilist tm) <=>
+ ?y ty. VFREE_IN (Var y ty) tm /\
+ VFREE_IN (Var u uty) (REV_ASSOCD (Var y ty) ilist (Var y ty))`,
+ MATCH_MP_TAC term_INDUCT THEN
+ REWRITE_TAC[VFREE_IN; VSUBST; term_DISTINCT] THEN REPEAT CONJ_TAC THENL
+ [MESON_TAC[term_INJ];
+ REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MESON_TAC[];
+ ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN DISCH_TAC THEN
+ REPEAT GEN_TAC THEN LET_TAC THEN LET_TAC THEN
+ COND_CASES_TAC THEN REPEAT LET_TAC THEN
+ ASM_REWRITE_TAC[VFREE_IN] THENL
+ [MAP_EVERY EXPAND_TAC ["ilist''"; "ilist'"];
+ EXPAND_TAC "t'" THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "ilist'"] THEN
+ SIMP_TAC[REV_ASSOCD; REV_ASSOCD_FILTER] THEN
+ ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[VFREE_IN] THEN
+ REWRITE_TAC[TAUT `(if ~b then x:bool else y) <=> (if b then y else x)`] THEN
+ ONCE_REWRITE_TAC[TAUT `~a /\ b <=> ~(~a ==> ~b)`] THEN
+ SIMP_TAC[TAUT `(if b then F else c) <=> ~b /\ c`] THEN
+ MATCH_MP_TAC(TAUT
+ `(a ==> ~c) /\ (~a ==> (b <=> c)) ==> (~(~a ==> ~b) <=> c)`) THEN
+ (CONJ_TAC THENL [ALL_TAC; MESON_TAC[]]) THEN
+ GEN_REWRITE_TAC LAND_CONV [term_INJ] THEN
+ DISCH_THEN(CONJUNCTS_THEN(SUBST_ALL_TAC o SYM)) THEN
+ REWRITE_TAC[NOT_IMP] THENL
+ [MP_TAC(ISPECL [`VSUBST ilist' t`; `x:string`; `ty:type`] VARIANT) THEN
+ ASM_REWRITE_TAC[] THEN
+ EXPAND_TAC "ilist'" THEN ASM_REWRITE_TAC[REV_ASSOCD_FILTER] THEN
+ MESON_TAC[];
+ ALL_TAC] THEN
+ FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EX]) THEN
+ EXPAND_TAC "ilist'" THEN
+ SPEC_TAC(`ilist:(term#term)list`,`l:(term#term)list`) THEN
+ MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[ALL; REV_ASSOCD; VFREE_IN] THEN
+ REWRITE_TAC[REV_ASSOCD; FILTER; FORALL_PAIR_THM] THEN
+ ONCE_REWRITE_TAC[COND_RAND] THEN REWRITE_TAC[ALL] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Sum type to model exception-raising. *)
+(* ------------------------------------------------------------------------- *)
+
+let result_INDUCT,result_RECURSION = define_type
+ "result = Clash term | Result term";;
+
+let result_INJ = injectivity "result";;
+
+let result_DISTINCT = distinctness "result";;
+
+(* ------------------------------------------------------------------------- *)
+(* Discriminators and extractors. (Nicer to pattern-match...) *)
+(* ------------------------------------------------------------------------- *)
+
+let IS_RESULT = define
+ `(IS_RESULT(Clash t) = F) /\
+ (IS_RESULT(Result t) = T)`;;
+
+let IS_CLASH = define
+ `(IS_CLASH(Clash t) = T) /\
+ (IS_CLASH(Result t) = F)`;;
+
+let RESULT = define
+ `RESULT(Result t) = t`;;
+
+let CLASH = define
+ `CLASH(Clash t) = t`;;
+
+(* ------------------------------------------------------------------------- *)
+(* We want induction/recursion on term size next. *)
+(* ------------------------------------------------------------------------- *)
+
+let rec sizeof = define
+ `(sizeof (Var x ty) = 1) /\
+ (sizeof (Equal ty) = 1) /\
+ (sizeof (Select ty) = 1) /\
+ (sizeof (Comb s t) = 1 + sizeof s + sizeof t) /\
+ (sizeof (Abs x ty t) = 2 + sizeof t)`;;
+
+let SIZEOF_VSUBST = prove
+ (`!t ilist. (!s' s. MEM (s',s) ilist ==> ?x ty. s' = Var x ty)
+ ==> (sizeof (VSUBST ilist t) = sizeof t)`,
+ MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[VSUBST; sizeof] THEN
+ CONJ_TAC THENL
+ [MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`] THEN
+ MATCH_MP_TAC list_INDUCT THEN
+ REWRITE_TAC[MEM; REV_ASSOCD; sizeof; FORALL_PAIR_THM] THEN
+ MAP_EVERY X_GEN_TAC [`s':term`; `s:term`; `l:(term#term)list`] THEN
+ REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC THEN
+ COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN ASM_MESON_TAC[sizeof];
+ ALL_TAC] THEN
+ CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
+ MAP_EVERY X_GEN_TAC [`x:string`; `ty:type`; `t:term`] THEN
+ DISCH_TAC THEN X_GEN_TAC `ilist:(term#term)list` THEN DISCH_TAC THEN
+ LET_TAC THEN LET_TAC THEN COND_CASES_TAC THEN
+ REPEAT LET_TAC THEN REWRITE_TAC[sizeof; EQ_ADD_LCANCEL] THENL
+ [ALL_TAC; ASM_MESON_TAC[MEM_FILTER]] THEN
+ FIRST_X_ASSUM MATCH_MP_TAC THEN
+ EXPAND_TAC "ilist''" THEN REWRITE_TAC[MEM; PAIR_EQ] THEN
+ ASM_MESON_TAC[MEM_FILTER]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Prove existence of INST_CORE. *)
+(* ------------------------------------------------------------------------- *)
+
+let INST_CORE_EXISTS = prove
+ (`?INST_CORE.
+ (!env tyin x ty.
+ INST_CORE env tyin (Var x ty) =
+ let tm = Var x ty
+ and tm' = Var x (TYPE_SUBST tyin ty) in
+ if REV_ASSOCD tm' env tm = tm then Result tm' else Clash tm') /\
+ (!env tyin ty.
+ INST_CORE env tyin (Equal ty) = Result(Equal(TYPE_SUBST tyin ty))) /\
+ (!env tyin ty.
+ INST_CORE env tyin (Select ty) = Result(Select(TYPE_SUBST tyin ty))) /\
+ (!env tyin s t.
+ INST_CORE env tyin (Comb s t) =
+ let sres = INST_CORE env tyin s in
+ if IS_CLASH sres then sres else
+ let tres = INST_CORE env tyin t in
+ if IS_CLASH tres then tres else
+ let s' = RESULT sres and t' = RESULT tres in
+ Result (Comb s' t')) /\
+ (!env tyin x ty t.
+ INST_CORE env tyin (Abs x ty t) =
+ let ty' = TYPE_SUBST tyin ty in
+ let env' = CONS (Var x ty,Var x ty') env in
+ let tres = INST_CORE env' tyin t in
+ if IS_RESULT tres then Result(Abs x ty' (RESULT tres)) else
+ let w = CLASH tres in
+ if ~(w = Var x ty') then tres else
+ let x' = VARIANT (RESULT(INST_CORE [] tyin t)) x ty' in
+ INST_CORE env tyin (Abs x' ty (VSUBST [Var x' ty,Var x ty] t)))`,
+ W(fun (asl,w) -> MATCH_MP_TAC(DISCH_ALL
+ (pure_prove_recursive_function_exists w))) THEN
+ EXISTS_TAC `MEASURE(\(env:(term#term)list,tyin:(type#type)list,t).
+ sizeof t)` THEN
+ REWRITE_TAC[WF_MEASURE; MEASURE_LE; MEASURE] THEN
+ CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
+ SIMP_TAC[MEM; PAIR_EQ; term_INJ; RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM;
+ GSYM EXISTS_REFL; SIZEOF_VSUBST; LE_REFL; sizeof] THEN
+ REPEAT STRIP_TAC THEN ARITH_TAC);;
+
+(* ------------------------------------------------------------------------- *)
+(* So define it. *)
+(* ------------------------------------------------------------------------- *)
+
+let INST_CORE = new_specification ["INST_CORE"] INST_CORE_EXISTS;;
+
+(* ------------------------------------------------------------------------- *)
+(* And the overall function. *)
+(* ------------------------------------------------------------------------- *)
+
+let INST_DEF = new_definition
+ `INST tyin tm = RESULT(INST_CORE [] tyin tm)`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Various misc lemmas. *)
+(* ------------------------------------------------------------------------- *)
+
+let NOT_IS_RESULT = prove
+ (`!r. ~(IS_RESULT r) <=> IS_CLASH r`,
+ MATCH_MP_TAC result_INDUCT THEN REWRITE_TAC[IS_RESULT; IS_CLASH]);;
+
+let letlemma = prove
+ (`(let x = t in P x) = P t`,
+ REWRITE_TAC[LET_DEF; LET_END_DEF]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Put everything together into a deductive system. *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("|-",(11,"right"));;
+
+let prove_RULES,proves_INDUCT,proves_CASES = new_inductive_definition
+ `(!t. welltyped t ==> [] |- t === t) /\
+ (!asl1 asl2 l m1 m2 r.
+ asl1 |- l === m1 /\ asl2 |- m2 === r /\ ACONV m1 m2
+ ==> TERM_UNION asl1 asl2 |- l === r) /\
+ (!asl1 l1 r1 asl2 l2 r2.
+ asl1 |- l1 === r1 /\ asl2 |- l2 === r2 /\ welltyped(Comb l1 l2)
+ ==> TERM_UNION asl1 asl2 |- Comb l1 l2 === Comb r1 r2) /\
+ (!asl x ty l r.
+ ~(EX (VFREE_IN (Var x ty)) asl) /\ asl |- l === r
+ ==> asl |- (Abs x ty l) === (Abs x ty r)) /\
+ (!x ty t. welltyped t ==> [] |- Comb (Abs x ty t) (Var x ty) === t) /\
+ (!p. p has_type Bool ==> [p] |- p) /\
+ (!asl1 asl2 p q p'.
+ asl1 |- p === q /\ asl2 |- p' /\ ACONV p p'
+ ==> TERM_UNION asl1 asl2 |- q) /\
+ (!asl1 asl2 c1 c2.
+ asl1 |- c1 /\ asl2 |- c2
+ ==> TERM_UNION (FILTER((~) o ACONV c2) asl1)
+ (FILTER((~) o ACONV c1) asl2)
+ |- c1 === c2) /\
+ (!tyin asl p. asl |- p ==> MAP (INST tyin) asl |- INST tyin p) /\
+ (!ilist asl p.
+ (!s s'. MEM (s',s) ilist ==> ?x ty. (s = Var x ty) /\ s' has_type ty) /\
+ asl |- p ==> MAP (VSUBST ilist) asl |- VSUBST ilist p)`;;
--- /dev/null
+(* ========================================================================= *)
+(* Consistency proof of "pure HOL" (no axioms or definitions) in itself. *)
+(* ========================================================================= *)
+
+loadt "Library/card.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* Syntactic definitions (terms, types, theorems etc.) *)
+(* ------------------------------------------------------------------------- *)
+
+loadt "Model/syntax.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* Set-theoretic hierarchy to support semantics. *)
+(* ------------------------------------------------------------------------- *)
+
+loadt "Model/modelset.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics. *)
+(* ------------------------------------------------------------------------- *)
+
+loadt "Model/semantics.ml";;
git://colo12-c703.uibk.ac.at / Model of HOL/.git / commitdiff