X-Git-Url: http://colo12-c703.uibk.ac.at/git/?p=G%C3%B6del%27s%20incompleteness%20theorem%2F.git;a=blobdiff_plain;f=Arithmetic%2Ffol.ml;fp=Arithmetic%2Ffol.ml;h=4465e87102b469f62a175cbd211679c036076935;hp=0000000000000000000000000000000000000000;hb=87defde679eb7f7eb6d8f7203472a6f6a8ab2966;hpb=67928fe38836205ca8d0705b3695186e998e3e29

diff --git a/Arithmetic/fol.ml b/Arithmetic/fol.ml
new file mode 100644
index 0000000..4465e87
--- /dev/null
+++ b/Arithmetic/fol.ml
@@ -0,0 +1,524 @@
+(* ========================================================================= *)
+(* First order logic based on the language of arithmetic.                    *)
+(* ========================================================================= *)
+
+prioritize_num();;
+
+(* ------------------------------------------------------------------------- *)
+(* Syntax of terms.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("++",(20,"right"));;
+parse_as_infix("**",(22,"right"));;
+
+let term_INDUCT,term_RECURSION = define_type
+  "term = Z
+        | V num
+        | Suc term
+        | ++ term term
+        | ** term term";;
+
+let term_CASES = prove_cases_thm term_INDUCT;;
+
+let term_DISTINCT = distinctness "term";;
+
+let term_INJ = injectivity "term";;
+
+(* ------------------------------------------------------------------------- *)
+(* Syntax of formulas.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("===",(18,"right"));;
+parse_as_infix("<<",(18,"right"));;
+parse_as_infix("<<=",(18,"right"));;
+
+parse_as_infix("&&",(16,"right"));;
+parse_as_infix("||",(15,"right"));;
+parse_as_infix("-->",(14,"right"));;
+parse_as_infix("<->",(13,"right"));;
+
+let form_INDUCT,form_RECURSION = define_type
+  "form = False
+        | True
+        | === term term
+        | << term term
+        | <<= term term
+        | Not form
+        | && form form
+        | || form form
+        | --> form form
+        | <-> form form
+        | !! num form
+        | ?? num form";;
+
+let form_CASES = prove_cases_thm form_INDUCT;;
+
+let form_DISTINCT = distinctness "form";;
+
+let form_INJ = injectivity "form";;
+
+(* ------------------------------------------------------------------------- *)
+(* Semantics of terms and formulas in the standard model.                    *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("|->",(22,"right"));;
+
+let valmod = new_definition
+  `(x |-> a) (v:A->B) = \y. if y = x then a else v(y)`;;
+
+let termval = new_recursive_definition term_RECURSION
+  `(termval v Z = 0) /\
+   (termval v (V n) = v(n)) /\
+   (termval v (Suc t) = SUC (termval v t)) /\
+   (termval v (s ++ t) = termval v s + termval v t) /\
+   (termval v (s ** t) = termval v s * termval v t)`;;
+
+let holds = new_recursive_definition form_RECURSION
+  `(holds v False <=> F) /\
+   (holds v True <=> T) /\
+   (holds v (s === t) <=> (termval v s = termval v t)) /\
+   (holds v (s << t) <=> (termval v s < termval v t)) /\
+   (holds v (s <<= t) <=> (termval v s <= termval v t)) /\
+   (holds v (Not p) <=> ~(holds v p)) /\
+   (holds v (p && q) <=> holds v p /\ holds v q) /\
+   (holds v (p || q) <=> holds v p \/ holds v q) /\
+   (holds v (p --> q) <=> holds v p ==> holds v q) /\
+   (holds v (p <-> q) <=> (holds v p <=> holds v q)) /\
+   (holds v (!! x p) <=> !a. holds ((x|->a) v) p) /\
+   (holds v (?? x p) <=> ?a. holds ((x|->a) v) p)`;;
+
+let true_def = new_definition
+  `true p <=> !v. holds v p`;;
+
+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[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Assignment.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("|=>",(22,"right"));;
+
+let assign = new_definition
+ `(x |=> a) = (x |-> a) V`;;
+
+let ASSIGN = prove
+ (`!x y a. (x |=> a) y = if y = x then a else V(y)`,
+  REWRITE_TAC[assign; valmod]);;
+
+let ASSIGN_TRIV = prove
+ (`!x. (x |=> V x) = V`,
+  REWRITE_TAC[VALMOD_REPEAT; assign]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Variables in a term and free variables in a formula.                      *)
+(* ------------------------------------------------------------------------- *)
+
+let FVT = new_recursive_definition term_RECURSION
+  `(FVT Z = {}) /\
+   (FVT (V n) = {n}) /\
+   (FVT (Suc t) = FVT t) /\
+   (FVT (s ++ t) = (FVT s) UNION (FVT t)) /\
+   (FVT (s ** t) = (FVT s) UNION (FVT t))`;;
+
+let FV = new_recursive_definition form_RECURSION
+  `(FV False = {}) /\
+   (FV True = {}) /\
+   (FV (s === t) = (FVT s) UNION (FVT t)) /\
+   (FV (s << t) = (FVT s) UNION (FVT t)) /\
+   (FV (s <<= t) = (FVT s) UNION (FVT t)) /\
+   (FV (Not p) = FV p) /\
+   (FV (p && q) = (FV p) UNION (FV q)) /\
+   (FV (p || q) = (FV p) UNION (FV q)) /\
+   (FV (p --> q) = (FV p) UNION (FV q)) /\
+   (FV (p <-> q) = (FV p) UNION (FV q)) /\
+   (FV (!!x p) = (FV p) DELETE x) /\
+   (FV (??x p) = (FV p) DELETE x)`;;
+
+let FVT_FINITE = prove
+ (`!t. FINITE(FVT t)`,
+  MATCH_MP_TAC term_INDUCT THEN
+  SIMP_TAC[FVT; FINITE_RULES; FINITE_INSERT; FINITE_UNION]);;
+
+let FV_FINITE = prove
+ (`!p. FINITE(FV p)`,
+  MATCH_MP_TAC form_INDUCT THEN
+  SIMP_TAC[FV; FVT_FINITE; FINITE_RULES; FINITE_DELETE; FINITE_UNION]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Logical axioms.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+let axiom_RULES,axiom_INDUCT,axiom_CASES = new_inductive_definition
+ `(!p q. axiom(p --> (q --> p))) /\
+  (!p q r. axiom((p --> q --> r) --> (p --> q) --> (p --> r))) /\
+  (!p. axiom(((p --> False) --> False) --> p)) /\
+  (!x p q. axiom((!!x (p --> q)) --> (!!x p) --> (!!x q))) /\
+  (!x p. ~(x IN FV p) ==> axiom(p --> !!x p)) /\
+  (!x t. ~(x IN FVT t) ==> axiom(??x (V x === t))) /\
+  (!t. axiom(t === t)) /\
+  (!s t. axiom((s === t) --> (Suc s === Suc t))) /\
+  (!s t u v. axiom(s === t --> u === v --> s ++ u === t ++ v)) /\
+  (!s t u v. axiom(s === t --> u === v --> s ** u === t ** v)) /\
+  (!s t u v. axiom(s === t --> u === v --> s === u --> t === v)) /\
+  (!s t u v. axiom(s === t --> u === v --> s << u --> t << v)) /\
+  (!s t u v. axiom(s === t --> u === v --> s <<= u --> t <<= v)) /\
+  (!p q. axiom((p <-> q) --> p --> q)) /\
+  (!p q. axiom((p <-> q) --> q --> p)) /\
+  (!p q. axiom((p --> q) --> (q --> p) --> (p <-> q))) /\
+  axiom(True <-> (False --> False)) /\
+  (!p. axiom(Not p <-> (p --> False))) /\
+  (!p q. axiom((p && q) <-> (p --> q --> False) --> False)) /\
+  (!p q. axiom((p || q) <-> Not(Not p && Not q))) /\
+  (!x p. axiom((??x p) <-> Not(!!x (Not p))))`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Deducibility from additional set of nonlogical axioms.                    *)
+(* ------------------------------------------------------------------------- *)
+
+parse_as_infix("|--",(11,"right"));;
+
+let proves_RULES,proves_INDUCT,proves_CASES = new_inductive_definition
+  `(!p. axiom p \/ p IN A ==> A |-- p) /\
+   (!p q. A |-- (p --> q) /\ A |-- p ==> A |-- q) /\
+   (!p x. A |-- p ==> A |-- (!!x p))`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Some lemmas.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+let TERMVAL_VALUATION = prove
+ (`!t v v'. (!x. x IN FVT(t) ==> (v'(x) = v(x)))
+            ==> (termval v' t = termval v t)`,
+  MATCH_MP_TAC term_INDUCT THEN
+  REWRITE_TAC[termval; FVT; IN_INSERT; IN_UNION; NOT_IN_EMPTY] THEN
+  REPEAT STRIP_TAC THEN ASM_MESON_TAC[]);;
+
+let HOLDS_VALUATION = prove
+ (`!p v v'.
+      (!x. x IN (FV p) ==> (v'(x) = v(x)))
+      ==> (holds v' p <=> holds v p)`,
+  MATCH_MP_TAC form_INDUCT THEN
+  REWRITE_TAC[FV; holds; IN_UNION; IN_DELETE] THEN
+  SIMP_TAC[TERMVAL_VALUATION] THEN
+  REWRITE_TAC[valmod] THEN REPEAT STRIP_TAC THEN
+  AP_TERM_TAC THEN ABS_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
+  ASM_SIMP_TAC[]);;
+
+let TERMVAL_VALMOD_OTHER = prove
+ (`!v x a t. ~(x IN FVT t) ==> (termval ((x |-> a) v) t = termval v t)`,
+  MESON_TAC[TERMVAL_VALUATION; VALMOD]);;
+
+let HOLDS_VALMOD_OTHER = prove
+ (`!v x a p. ~(x IN FV p) ==> (holds ((x |-> a) v) p <=> holds v p)`,
+  MESON_TAC[HOLDS_VALUATION; VALMOD]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Proof of soundness.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+let AXIOMS_TRUE = prove
+ (`!p. axiom p ==> true p`,
+  MATCH_MP_TAC axiom_INDUCT THEN
+  REWRITE_TAC[true_def] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[holds] THENL
+   [CONV_TAC TAUT;
+    CONV_TAC TAUT;
+    SIMP_TAC[];
+    REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN REPEAT GEN_TAC THEN
+    MATCH_MP_TAC EQ_IMP THEN
+    MATCH_MP_TAC HOLDS_VALUATION THEN
+    REWRITE_TAC[valmod] THEN GEN_TAC THEN COND_CASES_TAC THEN
+    ASM_MESON_TAC[];
+    EXISTS_TAC `termval v t` THEN
+    REWRITE_TAC[termval; valmod] THEN
+    MATCH_MP_TAC TERMVAL_VALUATION THEN
+    GEN_TAC THEN REWRITE_TAC[] THEN
+    COND_CASES_TAC THEN ASM_MESON_TAC[];
+    SIMP_TAC[termval];
+    SIMP_TAC[termval];
+    SIMP_TAC[termval];
+    SIMP_TAC[termval];
+    SIMP_TAC[termval];
+    SIMP_TAC[termval];
+    SIMP_TAC[termval];
+    SIMP_TAC[termval];
+    CONV_TAC TAUT;
+    CONV_TAC TAUT;
+    CONV_TAC TAUT;
+    MESON_TAC[]]);;
+
+let THEOREMS_TRUE = prove
+ (`!A p. (!q. q IN A ==> true q) /\ A |-- p ==> true p`,
+  GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
+  DISCH_TAC THEN MATCH_MP_TAC proves_INDUCT THEN
+  ASM_SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+  REWRITE_TAC[IN; AXIOMS_TRUE] THEN
+  SIMP_TAC[holds; true_def]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Variant variables for use in renaming substitution.                       *)
+(* ------------------------------------------------------------------------- *)
+
+let MAX_SYM = prove
+ (`!x y. MAX x y = MAX y x`,
+  ARITH_TAC);;
+
+let MAX_ASSOC = prove
+ (`!x y z. MAX x (MAX y z) = MAX (MAX x y) z`,
+  ARITH_TAC);;
+
+let SETMAX = new_definition
+  `SETMAX s = ITSET MAX s 0`;;
+
+let VARIANT = new_definition
+  `VARIANT s = SETMAX s + 1`;;
+
+let SETMAX_LEMMA = prove
+ (`(SETMAX {} = 0) /\
+   (!x s. FINITE s ==>
+           (SETMAX (x INSERT s) = if x IN s then SETMAX s
+                                  else MAX x (SETMAX s)))`,
+  REWRITE_TAC[SETMAX] THEN MATCH_MP_TAC FINITE_RECURSION THEN
+  REWRITE_TAC[MAX] THEN REPEAT GEN_TAC THEN
+  MAP_EVERY ASM_CASES_TAC
+   [`x:num <= s`; `y:num <= s`; `x:num <= y`; `y <= x`] THEN
+  ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LE_CASES; LE_TRANS; LE_ANTISYM]);;
+
+let SETMAX_MEMBER = prove
+ (`!s. FINITE s ==> !x. x IN s ==> x <= SETMAX s`,
+  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
+  REWRITE_TAC[NOT_IN_EMPTY; IN_INSERT] THEN
+  REPEAT GEN_TAC THEN STRIP_TAC THEN
+  ASM_SIMP_TAC [SETMAX_LEMMA] THEN
+  ASM_REWRITE_TAC[MAX] THEN
+  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
+  ASM_REWRITE_TAC[LE_REFL] THEN
+  ASM_MESON_TAC[LE_CASES; LE_TRANS]);;
+
+let SETMAX_THM = prove
+ (`(SETMAX {} = 0) /\
+   (!x s. FINITE s ==>
+           (SETMAX (x INSERT s) = MAX x (SETMAX s)))`,
+  REPEAT STRIP_TAC THEN ASM_SIMP_TAC [SETMAX_LEMMA] THEN
+  COND_CASES_TAC THEN REWRITE_TAC[MAX] THEN
+  COND_CASES_TAC THEN ASM_MESON_TAC[SETMAX_MEMBER]);;
+
+let SETMAX_UNION = prove
+ (`!s t. FINITE(s UNION t)
+         ==> (SETMAX(s UNION t) = MAX (SETMAX s) (SETMAX t))`,
+  let lemma = prove(`(x INSERT s) UNION t = x INSERT (s UNION t)`,SET_TAC[]) in
+  SUBGOAL_THEN `!t. FINITE(t) ==> !s. FINITE(s) ==>
+                        (SETMAX(s UNION t) = MAX (SETMAX s) (SETMAX t))`
+   (fun th -> MESON_TAC[th; FINITE_UNION]) THEN
+  GEN_TAC THEN DISCH_TAC THEN
+  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
+  REWRITE_TAC[UNION_EMPTY; SETMAX_THM] THEN CONJ_TAC THENL
+   [REWRITE_TAC[MAX; LE_0]; ALL_TAC] THEN
+  REPEAT STRIP_TAC THEN REWRITE_TAC[lemma] THEN
+  ASM_SIMP_TAC [SETMAX_THM; FINITE_UNION] THEN
+  REWRITE_TAC[MAX_ASSOC]);;
+
+let VARIANT_FINITE = prove
+ (`!s:num->bool. FINITE(s) ==> ~(VARIANT(s) IN s)`,
+  REWRITE_TAC[VARIANT] THEN
+  MESON_TAC[SETMAX_MEMBER; ARITH_RULE `~(x + 1 <= x)`]);;
+
+let VARIANT_THM = prove
+ (`!p. ~(VARIANT(FV p) IN FV(p))`,
+  GEN_TAC THEN MATCH_MP_TAC VARIANT_FINITE THEN REWRITE_TAC[FV_FINITE]);;
+
+let NOT_IN_VARIANT = prove
+ (`!s t. FINITE s /\ t SUBSET s ==> ~(VARIANT(s) IN t)`,
+  MESON_TAC[SUBSET; VARIANT_FINITE]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Substitution within terms.                                                *)
+(* ------------------------------------------------------------------------- *)
+
+let termsubst = new_recursive_definition term_RECURSION
+ `(termsubst v Z = Z) /\
+  (!x. termsubst v (V x) = v(x)) /\
+  (!t. termsubst v (Suc t) = Suc(termsubst v t)) /\
+  (!s t. termsubst v (s ++ t) = termsubst v s ++ termsubst v t) /\
+  (!s t. termsubst v (s ** t) = termsubst v s ** termsubst v t)`;;
+
+let TERMVAL_TERMSUBST = prove
+ (`!v i t. termval v (termsubst i t) = termval (termval v o i) t`,
+  GEN_TAC THEN GEN_TAC THEN
+  MATCH_MP_TAC term_INDUCT THEN SIMP_TAC[termval; termsubst; o_THM]);;
+
+let TERMSUBST_TERMSUBST = prove
+ (`!i j t. termsubst j (termsubst i t) = termsubst (termsubst j o i) t`,
+  GEN_TAC THEN GEN_TAC THEN
+  MATCH_MP_TAC term_INDUCT THEN SIMP_TAC[termval; termsubst; o_THM]);;
+
+let TERMSUBST_TRIV = prove
+ (`!t. termsubst V t = t`,
+  MATCH_MP_TAC term_INDUCT THEN SIMP_TAC[termsubst]);;
+
+let TERMSUBST_EQ = prove
+ (`!t v v'. (!x. x IN (FVT t) ==> (v'(x) = v(x)))
+            ==> (termsubst v' t = termsubst v t)`,
+  MATCH_MP_TAC term_INDUCT THEN
+  SIMP_TAC[termsubst; FVT; IN_SING; IN_UNION] THEN MESON_TAC[]);;
+
+let TERMSUBST_FVT = prove
+ (`!t i. FVT(termsubst i t) = {x | ?y. y IN FVT(t) /\ x IN FVT(i y)}`,
+  REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
+  MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[FVT; termsubst] THEN
+  REWRITE_TAC[IN_UNION; IN_SING; NOT_IN_EMPTY] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Formula substitution --- somewhat less trivial.                           *)
+(* ------------------------------------------------------------------------- *)
+
+let formsubst = new_recursive_definition form_RECURSION
+  `(formsubst v False = False) /\
+   (formsubst v True = True) /\
+   (formsubst v (s === t) = termsubst v s === termsubst v t) /\
+   (formsubst v (s << t) = termsubst v s << termsubst v t) /\
+   (formsubst v (s <<= t) = termsubst v s <<= termsubst v t) /\
+   (formsubst v (Not p) = Not(formsubst v p)) /\
+   (formsubst v (p && q) = formsubst v p && formsubst v q) /\
+   (formsubst v (p || q) = formsubst v p || formsubst v q) /\
+   (formsubst v (p --> q) = formsubst v p --> formsubst v q) /\
+   (formsubst v (p <-> q) = formsubst v p <-> formsubst v q) /\
+   (formsubst v (!!x q) =
+        let z = if ?y. y IN FV(!!x q) /\ x IN FVT(v(y))
+                then VARIANT(FV(formsubst ((x |-> V x) v) q)) else x in
+        !!z (formsubst ((x |-> V(z)) v) q)) /\
+   (formsubst v (??x q) =
+        let z = if ?y. y IN FV(??x q) /\ x IN FVT(v(y))
+                then VARIANT(FV(formsubst ((x |-> V x) v) q)) else x in
+        ??z (formsubst ((x |-> V(z)) v) q))`;;
+
+let FORMSUBST_PROPERTIES = prove
+ (`!p. (!i. FV(formsubst i p) = {x | ?y. y IN FV(p) /\ x IN FVT(i y)}) /\
+       (!i v. holds v (formsubst i p) = holds (termval v o i) p)`,
+  REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
+  MATCH_MP_TAC form_INDUCT THEN
+  REWRITE_TAC[FV; holds; formsubst; TERMSUBST_FVT; IN_ELIM_THM; NOT_IN_EMPTY;
+              IN_UNION; TERMVAL_TERMSUBST] THEN
+  REPEAT(CONJ_TAC THENL [MESON_TAC[];ALL_TAC]) THEN CONJ_TAC THEN
+  (MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN STRIP_TAC THEN
+   REWRITE_TAC[AND_FORALL_THM] THEN X_GEN_TAC `i:num->term` THEN
+   LET_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
+   SUBGOAL_THEN `~(?y. y IN (FV(p) DELETE x) /\ z IN FVT(i y))`
+   ASSUME_TAC THENL
+    [EXPAND_TAC "z" THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
+     MP_TAC(SPEC `formsubst ((x |-> V x) i) p` VARIANT_THM) THEN
+     ASM_REWRITE_TAC[valmod; IN_DELETE; CONTRAPOS_THM] THEN
+     MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[];
+     ALL_TAC] THEN
+   CONJ_TAC THEN GEN_TAC THEN ASM_REWRITE_TAC[FV; IN_DELETE; holds] THENL
+    [REWRITE_TAC[LEFT_AND_EXISTS_THM; valmod] THEN AP_TERM_TAC THEN
+     ABS_TAC THEN COND_CASES_TAC THEN ASM_MESON_TAC[FVT; IN_SING; IN_DELETE];
+     AP_TERM_TAC THEN ABS_TAC THEN MATCH_MP_TAC HOLDS_VALUATION THEN
+     GEN_TAC THEN REWRITE_TAC[valmod; o_DEF] THEN COND_CASES_TAC THEN
+     ASM_REWRITE_TAC[termval] THEN DISCH_TAC THEN
+     MATCH_MP_TAC TERMVAL_VALUATION THEN GEN_TAC THEN
+     REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_MESON_TAC[IN_DELETE]]));;
+
+let FORMSUBST_FV = prove
+ (`!p i. FV(formsubst i p) = {x | ?y. y IN FV(p) /\ x IN FVT(i y)}`,
+  REWRITE_TAC[FORMSUBST_PROPERTIES]);;
+
+let HOLDS_FORMSUBST = prove
+ (`!p i v. holds v (formsubst i p) <=> holds (termval v o i) p`,
+  REWRITE_TAC[FORMSUBST_PROPERTIES]);;
+
+let FORMSUBST_EQ = prove
+ (`!p i j. (!x. x IN FV(p) ==> (i(x) = j(x)))
+           ==> (formsubst i p = formsubst j p)`,
+  MATCH_MP_TAC form_INDUCT THEN
+  REWRITE_TAC[FV; formsubst; IN_UNION; IN_DELETE] THEN
+  SIMP_TAC[] THEN REWRITE_TAC[CONJ_ASSOC] THEN
+  GEN_REWRITE_TAC I [GSYM CONJ_ASSOC] THEN CONJ_TAC THENL
+   [MESON_TAC[TERMSUBST_EQ]; ALL_TAC] THEN
+  CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN
+  (DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`i:num->term`; `j:num->term`] THEN
+   DISCH_TAC THEN REWRITE_TAC[LET_DEF; LET_END_DEF; form_INJ] THEN
+   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN SIMP_TAC[] THEN
+   CONJ_TAC THENL
+    [ALL_TAC;
+     DISCH_THEN(K ALL_TAC) THEN FIRST_ASSUM MATCH_MP_TAC THEN
+     REWRITE_TAC[valmod] THEN ASM_SIMP_TAC[]] THEN
+   AP_THM_TAC THEN BINOP_TAC THENL
+    [ASM_MESON_TAC[];
+     AP_TERM_TAC THEN AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
+     REWRITE_TAC[valmod] THEN ASM_MESON_TAC[]]));;
+
+let FORMSUBST_TRIV = prove
+ (`!p. formsubst V p = p`,
+  MATCH_MP_TAC form_INDUCT THEN
+  SIMP_TAC[formsubst; TERMSUBST_TRIV] THEN
+  REWRITE_TAC[FVT; IN_SING; FV; IN_DELETE] THEN
+  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
+  ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; VALMOD_REPEAT] THEN
+  ASM_MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Quasi-substitution.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+let qsubst = new_definition
+ `qsubst (x,t) p = ??x (V x === t && p)`;;
+
+let FV_QSUBST = prove
+ (`!x n p. FV(qsubst (x,t) p) = (FV(p) UNION FVT(t)) DELETE x`,
+  REWRITE_TAC[qsubst; FV; FVT] THEN SET_TAC[]);;
+
+let HOLDS_QSUBST = prove
+ (`!v t p v. ~(x IN FVT(t))
+             ==> (holds v (qsubst (x,t) p) <=>
+                  holds ((x |-> termval v t) v) p)`,
+  REPEAT STRIP_TAC THEN
+  SUBGOAL_THEN `!v z. termval ((x |-> z) v) t = termval v t` ASSUME_TAC THENL
+   [REWRITE_TAC[valmod] THEN ASM_MESON_TAC[TERMVAL_VALUATION];
+    ASM_REWRITE_TAC[holds; qsubst; termval; VALMOD_BASIC; UNWIND_THM2]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* The numeral mapping.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+let numeral = new_recursive_definition num_RECURSION
+  `(numeral 0 = Z) /\
+   (!n. numeral (SUC n) = Suc(numeral n))`;;
+
+let TERMVAL_NUMERAL = prove
+ (`!v n. termval v (numeral n) = n`,
+  GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[termval;numeral]);;
+
+let FVT_NUMERAL = prove
+ (`!n. FVT(numeral n) = {}`,
+  INDUCT_TAC THEN ASM_REWRITE_TAC[FVT; numeral]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Closed-ness.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+let closed = new_definition
+  `closed p <=> (FV p = {})`;;