--- /dev/null
+(* ========================================================================= *)
+(* 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 = {})`;;
git://colo12-c703.uibk.ac.at / Gödel's incompleteness theorem/.git / blobdiff