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

diff --git a/Arithmetic/derived.ml b/Arithmetic/derived.ml
new file mode 100644
index 0000000..8037251
--- /dev/null
+++ b/Arithmetic/derived.ml
@@ -0,0 +1,668 @@
+(* ========================================================================= *)
+(* Derived properties of provability.                                        *)
+(* ========================================================================= *)
+
+let negativef = new_definition
+  `negativef p = ?q. p = q --> False`;;
+
+let negatef = new_definition
+  `negatef p = if negativef p then @q. p = q --> False else p --> False`;;
+
+(* ------------------------------------------------------------------------- *)
+(* The primitive basis, separated into its named components.                 *)
+(* ------------------------------------------------------------------------- *)
+
+let axiom_addimp = prove
+ (`!A p q. A |-- p --> (q --> p)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_distribimp = prove
+ (`!A p q r. A |-- (p --> q --> r) --> (p --> q) --> (p --> r)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_doubleneg = prove
+ (`!A p. A |-- ((p --> False) --> False) --> p`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_allimp = prove
+ (`!A x p q. A |-- (!!x (p --> q)) --> (!!x p) --> (!!x q)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_impall = prove
+ (`!A x p. ~(x IN FV p) ==> A |-- p --> !!x p`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_existseq = prove
+ (`!A x t. ~(x IN FVT t) ==> A |-- ??x (V x === t)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_eqrefl = prove
+ (`!A t. A |-- t === t`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_funcong = prove
+ (`(!A s t. A |-- s === t --> Suc s === Suc t) /\
+   (!A s t u v. A |-- s === t --> u === v --> s ++ u === t ++ v) /\
+   (!A s t u v. A |-- s === t --> u === v --> s ** u === t ** v)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_predcong = prove
+ (`(!A s t u v. A |-- s === t --> u === v --> s === u --> t === v) /\
+   (!A s t u v. A |-- s === t --> u === v --> s << u --> t << v) /\
+   (!A s t u v. A |-- s === t --> u === v --> s <<= u --> t <<= v)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_iffimp1 = prove
+ (`!A p q. A |-- (p <-> q) --> p --> q`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_iffimp2 = prove
+ (`!A p q. A |-- (p <-> q) --> q --> p`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_impiff = prove
+ (`!A p q. A |-- (p --> q) --> (q --> p) --> (p <-> q)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_true = prove
+ (`A |-- True <-> (False --> False)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_not = prove
+ (`!A p. A |-- Not p <-> (p --> False)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_and = prove
+ (`!A p q. A |-- (p && q) <-> (p --> q --> False) --> False`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_or = prove
+ (`!A p q. A |-- (p || q) <-> Not(Not p && Not q)`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let axiom_exists = prove
+ (`!A x p. A |-- (??x p) <-> Not(!!x (Not p))`,
+  MESON_TAC[proves_RULES; axiom_RULES]);;
+
+let assume = prove
+ (`!A p. p IN A ==> A |-- p`,
+  MESON_TAC[proves_RULES]);;
+
+let modusponens = prove
+ (`!A p. A |-- (p --> q) /\ A |-- p ==> A |-- q`,
+  MESON_TAC[proves_RULES]);;
+
+let gen = prove
+ (`!A p x. A |-- p ==> A |-- !!x p`,
+  MESON_TAC[proves_RULES]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Now some theorems corresponding to derived rules.                         *)
+(* ------------------------------------------------------------------------- *)
+
+let iff_imp1 = prove
+ (`!A p q. A |-- p <-> q ==> A |-- p --> q`,
+  MESON_TAC[modusponens; axiom_iffimp1]);;
+
+let iff_imp2 = prove
+ (`!A p q. A |-- p <-> q ==> A |-- q --> p`,
+  MESON_TAC[modusponens; axiom_iffimp2]);;
+
+let imp_antisym = prove
+ (`!A p q. A |-- p --> q /\ A |-- q --> p ==> A |-- p <-> q`,
+  MESON_TAC[modusponens; axiom_impiff]);;
+
+let add_assum = prove
+ (`!A p q. A |-- q ==> A |-- p --> q`,
+  MESON_TAC[modusponens; axiom_addimp]);;
+
+let imp_refl = prove
+ (`!A p. A |-- p --> p`,
+  MESON_TAC[modusponens; axiom_distribimp; axiom_addimp]);;
+
+let imp_add_assum = prove
+ (`!A p q r. A |-- q --> r ==> A |-- (p --> q) --> (p --> r)`,
+  MESON_TAC[modusponens; axiom_distribimp; add_assum]);;
+
+let imp_unduplicate = prove
+ (`!A p q. A |-- p --> p --> q ==> A |-- p --> q`,
+  MESON_TAC[modusponens; axiom_distribimp; imp_refl]);;
+
+let imp_trans = prove
+ (`!A p q. A |-- p --> q /\ A |-- q --> r ==> A |-- p --> r`,
+  MESON_TAC[modusponens; imp_add_assum]);;
+
+let imp_swap = prove
+ (`!A p q r. A |-- p --> q --> r ==> A |-- q --> p --> r`,
+  MESON_TAC[imp_trans; axiom_addimp; modusponens; axiom_distribimp]);;
+
+let imp_trans_chain_2 = prove
+ (`!A p q1 q2 r. A |-- p --> q1 /\ A |-- p --> q2 /\ A |-- q1 --> q2 --> r
+                 ==> A |-- p --> r`,
+  ASM_MESON_TAC[imp_trans; imp_swap; imp_unduplicate]);;
+
+
+
+(*****
+
+let imp_trans_chain = prove
+ (`!A p qs r. ALL (\q. A |-- p --> q) qs /\
+              A |-- ITLIST (-->) qs r
+              ==> A |-- p --> r`,
+  GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
+  REWRITE_TAC[ALL; ITLIST] THENL
+   [ASM_MESON_TAC[add_assum]; ALL_TAC] THEN
+  REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC
+
+
+ASM_MESON_TAC[imp_trans; imp_swap; imp_unduplicate; axiom_distribimp;
+              modusponens; add_assum]
+
+add_assum] THEN
+  ... needs more thought. Maybe the REV
+
+ *****)
+
+
+let imp_trans_th = prove
+ (`!A p q r. A |-- (q --> r) --> (p --> q) --> (p --> r)`,
+  MESON_TAC[imp_trans; axiom_addimp; axiom_distribimp]);;
+
+let imp_add_concl = prove
+ (`!A p q r. A |-- p --> q ==> A |-- (q --> r) --> (p --> r)`,
+  MESON_TAC[modusponens; imp_swap; imp_trans_th]);;
+
+let imp_trans2 = prove
+ (`!A p q r s. A |-- p --> q --> r /\ A |-- r --> s ==> A |-- p --> q --> s`,
+  MESON_TAC[imp_add_assum; modusponens; imp_trans_th]);;
+
+let imp_swap_th = prove
+ (`!A p q r. A |-- (p --> q --> r) --> (q --> p --> r)`,
+  MESON_TAC[imp_trans; axiom_distribimp; imp_add_concl; axiom_addimp]);;
+
+let contrapos = prove
+ (`!A p q. A |-- p --> q ==> A |-- Not q --> Not p`,
+  MESON_TAC[imp_trans; iff_imp1; axiom_not; imp_add_concl; iff_imp2]);;
+
+let imp_truefalse = prove
+ (`!p q. A |-- (q --> False) --> p --> (p --> q) --> False`,
+  MESON_TAC[imp_trans; imp_trans_th; imp_swap_th]);;
+
+let imp_insert = prove
+ (`!A p q r. A |-- p --> r ==> A |-- p --> q --> r`,
+  MESON_TAC[imp_trans; axiom_addimp]);;
+
+let ex_falso = prove
+ (`!A p. A |-- False --> p`,
+  MESON_TAC[imp_trans; axiom_addimp; axiom_doubleneg]);;
+
+let imp_contr = prove
+ (`!A p q. A |-- (p --> False) --> (p --> r)`,
+  MESON_TAC[imp_add_assum; ex_falso]);;
+
+let imp_contrf = prove
+ (`!A p r. A |-- p --> negatef p --> r`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[negatef; negativef] THEN
+  COND_CASES_TAC THEN POP_ASSUM STRIP_ASSUME_TAC THEN
+  ASM_REWRITE_TAC[form_INJ] THEN
+  ASM_MESON_TAC[imp_contr; imp_swap]);;
+
+let contrad = prove
+ (`!A p. A |-- (p --> False) --> p ==> A |-- p`,
+  MESON_TAC[modusponens; axiom_distribimp; imp_refl; axiom_doubleneg]);;
+
+let bool_cases = prove
+ (`!p q. A |-- p --> q /\ A |-- (p --> False) --> q ==> A |-- q`,
+  MESON_TAC[contrad; imp_trans; imp_add_concl]);;
+
+(****
+
+let imp_front = prove
+ (`...` a bi more structure);;
+
+****)
+
+(*** This takes about a minute, but it does work ***)
+
+let imp_false_rule = prove
+ (`!p q r. A |-- (q --> False) --> p --> r
+           ==> A |-- ((p --> q) --> False) --> r`,
+  MESON_TAC[imp_add_concl; imp_add_assum; ex_falso; axiom_addimp; imp_swap;
+            imp_trans; axiom_doubleneg; imp_unduplicate]);;
+
+let imp_true_rule = prove
+ (`!A p q r. A |-- (p --> False) --> r /\ A |-- q --> r
+             ==> A |-- (p --> q) --> r`,
+  MESON_TAC[imp_insert; imp_swap; modusponens; imp_trans_th; bool_cases]);;
+
+let iff_def = prove
+ (`!A p q. A |-- (p <-> q) <-> (p --> q) && (q --> p)`,
+  REPEAT GEN_TAC THEN MATCH_MP_TAC imp_antisym THEN CONJ_TAC THENL
+   [SUBGOAL_THEN
+     `A |-- ((p --> q) --> (q --> p) --> False) --> (p <-> q) --> False`
+    ASSUME_TAC THENL
+     [ASM_MESON_TAC[imp_add_concl; imp_trans; axiom_distribimp; modusponens;
+                    imp_swap; axiom_iffimp1; axiom_iffimp2];
+      ALL_TAC] THEN
+    ASM_MESON_TAC[imp_add_concl; imp_trans; imp_swap; imp_refl;
+                   iff_imp2; axiom_and];
+    SUBGOAL_THEN
+     `A |-- (((p --> q) --> (q --> p) --> False) --> False)
+            --> ((p <-> q) --> False) --> False`
+    ASSUME_TAC THENL
+     [ASM_MESON_TAC[imp_swap; imp_trans_th; modusponens; imp_add_assum;
+                    axiom_impiff; imp_add_concl];
+      ALL_TAC] THEN
+    ASM_MESON_TAC[imp_trans; iff_imp1; axiom_and; axiom_doubleneg]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Equality rules.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+let eq_sym = prove
+ (`!A s t. A |-- s === t --> t === s`,
+  MESON_TAC[axiom_eqrefl; modusponens; imp_swap; axiom_predcong]);;
+
+let icongruence_general = prove
+ (`!A p x s t tm.
+     A |-- s === t -->
+           termsubst ((x |-> s) v) tm === termsubst ((x |-> t) v) tm`,
+  GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
+  MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[termsubst] THEN
+  REPEAT CONJ_TAC THENL
+   [MESON_TAC[axiom_eqrefl; add_assum];
+    GEN_TAC THEN REWRITE_TAC[valmod] THEN
+    COND_CASES_TAC THEN REWRITE_TAC[imp_refl] THEN
+    MESON_TAC[axiom_eqrefl; add_assum];
+    MESON_TAC[imp_trans; axiom_funcong];
+    MESON_TAC[imp_trans; axiom_funcong; imp_swap; imp_unduplicate];
+    MESON_TAC[imp_trans; axiom_funcong; imp_swap; imp_unduplicate]]);;
+
+let icongruence = prove
+ (`!A x s t tm.
+     A |-- s === t --> termsubst (x |=> s) tm === termsubst (x |=> t) tm`,
+  REWRITE_TAC[assign; icongruence_general]);;
+
+let icongruence_var = prove
+ (`!A x t tm.
+     A |-- V x === t --> tm === termsubst (x |=> t) tm`,
+  MESON_TAC[icongruence; TERMSUBST_TRIV; ASSIGN_TRIV]);;
+
+(* ------------------------------------------------------------------------- *)
+(* First-order rules.                                                        *)
+(* ------------------------------------------------------------------------- *)
+
+let gen_right = prove
+ (`!A x p q. ~(x IN FV(p)) /\ A |-- p --> q
+             ==> A |-- p --> !!x q`,
+  MESON_TAC[axiom_allimp; modusponens; gen; imp_trans; axiom_impall]);;
+
+let genimp = prove
+ (`!x p q. A |-- p --> q ==> A |-- (!!x p) --> (!!x q)`,
+  MESON_TAC[modusponens; axiom_allimp; gen]);;
+
+let eximp = prove
+ (`!x p q. A |-- p --> q ==> A |-- (??x p) --> (??x q)`,
+  MESON_TAC[contrapos; genimp; contrapos; imp_trans; iff_imp1; iff_imp2;
+            axiom_exists]);;
+
+let exists_imp = prove
+ (`!A x p q. A |-- ??x (p --> q) /\ ~(x IN FV(q)) ==> A |-- (!!x p) --> q`,
+  REPEAT STRIP_TAC THEN
+  SUBGOAL_THEN `A |-- (q --> False) --> !!x (p --> Not(p --> q))`
+  ASSUME_TAC THENL
+   [MATCH_MP_TAC gen_right THEN
+    ASM_REWRITE_TAC[FV; IN_UNION; NOT_IN_EMPTY] THEN
+    ASM_MESON_TAC[iff_imp2; axiom_not; imp_trans2; imp_truefalse];
+    ALL_TAC] THEN
+  SUBGOAL_THEN `A |-- (q --> False) --> !!x p --> !!x (Not(p --> q))`
+  ASSUME_TAC THENL
+   [ASM_MESON_TAC[imp_trans; axiom_allimp]; ALL_TAC] THEN
+  SUBGOAL_THEN `A |-- ((q --> False) --> !!x (Not(p --> q)))
+                      --> (q --> False) --> False`
+  ASSUME_TAC THENL
+   [ASM_MESON_TAC[modusponens; iff_imp1; axiom_exists; axiom_not; imp_trans_th];
+    ALL_TAC] THEN
+  ASM_MESON_TAC[imp_trans; imp_swap; axiom_doubleneg]);;
+
+let subspec = prove
+ (`!A x t p q. ~(x IN FVT(t)) /\ ~(x IN FV(q)) /\ A |-- V x === t --> p --> q
+               ==> A |-- (!!x p) --> q`,
+  MESON_TAC[exists_imp; modusponens; eximp; axiom_existseq]);;
+
+let subalpha = prove
+ (`!A x y p q. ((x = y) \/ ~(x IN FV(q)) /\ ~(y IN FV(p))) /\
+               A |-- V x === V y --> p --> q
+               ==> A |-- (!!x p) --> (!!y q)`,
+  REPEAT GEN_TAC THEN ASM_CASES_TAC `x = y:num` THEN ASM_REWRITE_TAC[] THEN
+  STRIP_TAC THENL
+   [FIRST_X_ASSUM SUBST_ALL_TAC THEN
+    ASM_MESON_TAC[genimp; modusponens; axiom_eqrefl];
+    ALL_TAC] THEN
+  MATCH_MP_TAC gen_right THEN ASM_REWRITE_TAC[FV; IN_DELETE] THEN
+  MATCH_MP_TAC subspec THEN EXISTS_TAC `V y` THEN
+  ASM_REWRITE_TAC[FVT; IN_SING]);;
+
+let imp_mono_th = prove
+ (`A |-- (p' --> p) --> (q --> q') --> (p --> q) --> (p' --> q')`,
+  MESON_TAC[imp_trans; imp_swap; imp_trans_th]);;
+
+(* ------------------------------------------------------------------------- *)
+(* We'll perform induction on this measure.                                  *)
+(* ------------------------------------------------------------------------- *)
+
+let complexity = new_recursive_definition form_RECURSION
+  `(complexity False = 1) /\
+   (complexity True = 1) /\
+   (!s t. complexity (s === t) = 1) /\
+   (!s t. complexity (s << t) = 1) /\
+   (!s t. complexity (s <<= t) = 1) /\
+   (!p. complexity (Not p) = complexity p + 3) /\
+   (!p q. complexity (p && q) = complexity p + complexity q + 6) /\
+   (!p q. complexity (p || q) = complexity p + complexity q + 16) /\
+   (!p q. complexity (p --> q) = complexity p + complexity q + 1) /\
+   (!p q. complexity (p <-> q) = 2 * (complexity p + complexity q) + 9) /\
+   (!x p. complexity (!!x p) = complexity p + 1) /\
+   (!x p. complexity (??x p) = complexity p + 8)`;;
+
+let COMPLEXITY_FORMSUBST = prove
+ (`!p i. complexity(formsubst i p) = complexity p`,
+  MATCH_MP_TAC form_INDUCT THEN
+  SIMP_TAC[formsubst; complexity; LET_DEF; LET_END_DEF]);;
+
+let isubst_general = prove
+ (`!A p x v s t. A |-- s === t
+                       --> formsubst ((x |-> s) v) p
+                           --> formsubst ((x |-> t) v) p`,
+  GEN_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `complexity p` THEN
+  POP_ASSUM MP_TAC THEN SPEC_TAC(`p:form`,`p:form`) THEN
+  MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[formsubst; complexity] THEN
+  REPEAT CONJ_TAC THENL
+   [MESON_TAC[imp_refl; add_assum];
+    MESON_TAC[imp_refl; add_assum];
+    MESON_TAC[imp_trans_chain_2; axiom_predcong; icongruence_general];
+    MESON_TAC[imp_trans_chain_2; axiom_predcong; icongruence_general];
+    MESON_TAC[imp_trans_chain_2; axiom_predcong; icongruence_general];
+    X_GEN_TAC `p:form` THEN DISCH_THEN(K ALL_TAC) THEN
+    DISCH_THEN(MP_TAC o SPEC `p --> False`) THEN
+    REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
+    REWRITE_TAC[formsubst] THEN
+    MESON_TAC[axiom_not; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
+    MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
+    DISCH_THEN(MP_TAC o SPEC `(p --> q --> False) --> False`) THEN
+    REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
+    REWRITE_TAC[formsubst] THEN
+    MESON_TAC[axiom_and; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
+    MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
+    DISCH_THEN(MP_TAC o SPEC `Not(Not p && Not q)`) THEN
+    REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
+    REWRITE_TAC[formsubst] THEN
+    MESON_TAC[axiom_or; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
+    MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
+    DISCH_THEN(fun th -> MP_TAC(SPEC `p:form` th) THEN
+                         MP_TAC(SPEC `q:form` th)) THEN
+    REWRITE_TAC[ARITH_RULE `p < p + q + 1 /\ q < p + q + 1`] THEN
+    MESON_TAC[imp_mono_th; eq_sym; imp_trans; imp_trans_chain_2];
+    MAP_EVERY X_GEN_TAC [`p:form`; `q:form`] THEN DISCH_THEN(K ALL_TAC) THEN
+    DISCH_THEN(MP_TAC o SPEC `(p --> q) && (q --> p)`) THEN
+    REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
+    REWRITE_TAC[formsubst] THEN
+    MESON_TAC[iff_def; iff_imp1; iff_imp2; imp_swap; imp_trans; imp_trans2];
+    ALL_TAC;
+    MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN DISCH_THEN(K ALL_TAC) THEN
+    DISCH_THEN(MP_TAC o SPEC `Not(!!x (Not p))`) THEN
+    REWRITE_TAC[complexity] THEN ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
+    REWRITE_TAC[formsubst] THEN
+    REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
+    REWRITE_TAC[FV] THEN REPEAT LET_TAC THEN
+    ASM_MESON_TAC[axiom_exists; iff_imp1; iff_imp2; imp_swap; imp_trans;
+                  imp_trans2]] THEN
+  MAP_EVERY X_GEN_TAC [`u:num`; `p:form`] THEN DISCH_THEN(K ALL_TAC) THEN
+  REWRITE_TAC[ARITH_RULE `a < b + 1 <=> a <= b`] THEN DISCH_TAC THEN
+  MAP_EVERY X_GEN_TAC [`v:num`; `i:num->term`; `s:term`; `t:term`] THEN
+  MAP_EVERY ABBREV_TAC
+   [`x = if ?y. y IN FV (!! u p) /\ u IN FVT ((v |-> s) i y)
+         then VARIANT (FV (formsubst ((u |-> V u) ((v |-> s) i)) p))
+         else u`;
+    `y = if ?y. y IN FV (!! u p) /\ u IN FVT ((v |-> t) i y)
+         then VARIANT (FV (formsubst ((u |-> V u) ((v |-> t) i)) p))
+         else u`] THEN
+  REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
+  SUBGOAL_THEN `~(x IN FV(formsubst ((v |-> s) i) (!!u p))) /\
+                ~(y IN FV(formsubst ((v |-> t) i) (!!u p)))`
+  STRIP_ASSUME_TAC THENL
+   [MAP_EVERY EXPAND_TAC ["x"; "y"] THEN CONJ_TAC THEN
+    (COND_CASES_TAC THENL
+       [ALL_TAC; ASM_REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM]] THEN
+      MATCH_MP_TAC NOT_IN_VARIANT THEN REWRITE_TAC[FV_FINITE] THEN
+      REWRITE_TAC[SUBSET; FORMSUBST_FV; IN_ELIM_THM; FV; IN_DELETE] THEN
+      REWRITE_TAC[valmod] THEN MESON_TAC[FVT; IN_SING]);
+    ALL_TAC] THEN
+  ASM_CASES_TAC `v:num = u` THENL
+   [ASM_REWRITE_TAC[VALMOD_VALMOD_BASIC] THEN
+    MATCH_MP_TAC add_assum THEN MATCH_MP_TAC subalpha THEN
+    ASM_SIMP_TAC[LE_REFL] THEN
+    ASM_CASES_TAC `y:num = x` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
+     [UNDISCH_TAC `~(x IN FV (formsubst ((v |-> s) i) (!! u p)))`;
+      UNDISCH_TAC `~(y IN FV (formsubst ((v |-> t) i) (!! u p)))`] THEN
+    ASM_REWRITE_TAC[FORMSUBST_FV; FV; IN_ELIM_THM; IN_DELETE] THEN
+    MATCH_MP_TAC MONO_NOT THEN MATCH_MP_TAC MONO_EXISTS THEN
+    X_GEN_TAC `w:num` THEN ASM_CASES_TAC `w:num = u` THEN
+    ASM_REWRITE_TAC[VALMOD_BASIC; FVT; IN_SING] THEN
+    ASM_REWRITE_TAC[valmod; FVT; IN_SING];
+    ALL_TAC] THEN
+  SUBGOAL_THEN
+   `?z. ~(z IN FVT s) /\ ~(z IN FVT t) /\
+        A |-- !!x (formsubst ((u |-> V x) ((v |-> s) i)) p)
+              --> !!z (formsubst ((u |-> V z) ((v |-> s) i)) p) /\
+        A |-- !!z (formsubst ((u |-> V z) ((v |-> t) i)) p)
+              --> !!y (formsubst ((u |-> V y) ((v |-> t) i)) p)`
+  MP_TAC THENL
+   [ALL_TAC;
+    DISCH_THEN(X_CHOOSE_THEN `z:num` STRIP_ASSUME_TAC) THEN
+    MATCH_MP_TAC imp_trans THEN
+    EXISTS_TAC `(!!z (formsubst ((v |-> s) ((u |-> V z) i)) p))
+                     --> (!!z (formsubst ((v |-> t) ((u |-> V z) i)) p))` THEN
+    CONJ_TAC THENL
+     [MATCH_MP_TAC imp_trans THEN
+      EXISTS_TAC `!!z (formsubst ((v |-> s) ((u |-> V z) i)) p
+                       --> formsubst ((v |-> t) ((u |-> V z) i)) p)` THEN
+      REWRITE_TAC[axiom_allimp] THEN
+      ASM_SIMP_TAC[complexity; LE_REFL; FV; IN_UNION; gen_right];
+      ALL_TAC] THEN
+    FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[MATCH_MP VALMOD_SWAP th]) THEN
+    ASM_MESON_TAC[imp_mono_th; modusponens]] THEN
+  MP_TAC(SPEC
+   `FVT(s) UNION FVT(t) UNION
+    FV(formsubst ((u |-> V x) ((v |-> s) i)) p) UNION
+    FV(formsubst ((u |-> V y) ((v |-> t) i)) p)` VARIANT_FINITE) THEN
+  REWRITE_TAC[FINITE_UNION; FV_FINITE; FVT_FINITE] THEN
+  W(fun (_,w) -> ABBREV_TAC(mk_comb(`(=) (z:num)`,lhand(rand(lhand w))))) THEN
+  REWRITE_TAC[IN_UNION; DE_MORGAN_THM] THEN STRIP_TAC THEN
+  EXISTS_TAC `z:num` THEN ASM_REWRITE_TAC[] THEN
+  CONJ_TAC THEN MATCH_MP_TAC subalpha THEN ASM_SIMP_TAC[LE_REFL] THENL
+   [ASM_CASES_TAC `z:num = x` THEN ASM_REWRITE_TAC[] THEN
+    UNDISCH_TAC `~(x IN FV (formsubst ((v |-> s) i) (!! u p)))`;
+    ASM_CASES_TAC `z:num = y` THEN ASM_REWRITE_TAC[] THEN
+    UNDISCH_TAC `~(y IN FV (formsubst ((v |-> t) i) (!! u p)))`] THEN
+  ASM_REWRITE_TAC[FORMSUBST_FV; FV; IN_ELIM_THM; IN_DELETE] THEN
+  MATCH_MP_TAC MONO_NOT THEN MATCH_MP_TAC MONO_EXISTS THEN
+  X_GEN_TAC `w:num` THEN ASM_CASES_TAC `w:num = u` THEN
+  ASM_REWRITE_TAC[VALMOD_BASIC; FVT; IN_SING] THEN
+  ASM_REWRITE_TAC[valmod; FVT; IN_SING]);;
+
+let isubst = prove
+ (`!A p x s t. A |-- s === t
+                     --> formsubst (x |=> s) p --> formsubst (x |=> t) p`,
+  REWRITE_TAC[assign; isubst_general]);;
+
+let isubst_var = prove
+ (`!A p x t. A |-- V x === t --> p --> formsubst (x |=> t) p`,
+  MESON_TAC[FORMSUBST_TRIV; ASSIGN_TRIV; isubst]);;
+
+let alpha = prove
+ (`!A x z p. ~(z IN FV p) ==> A |-- (!!x p) --> !!z (formsubst (x |=> V z) p)`,
+  REPEAT STRIP_TAC THEN MATCH_MP_TAC subalpha THEN CONJ_TAC THENL
+   [ALL_TAC; MESON_TAC[isubst_var]] THEN
+  REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; ASSIGN] THEN
+  ASM_MESON_TAC[IN_SING; FVT]);;
+
+(* ------------------------------------------------------------------------- *)
+(* To conclude cleanly, useful to have all variables.                        *)
+(* ------------------------------------------------------------------------- *)
+
+let VARS = new_recursive_definition form_RECURSION
+ `(VARS False = {}) /\
+  (VARS True = {}) /\
+  (VARS (s === t) = FVT s UNION FVT t) /\
+  (VARS (s << t) = FVT s UNION FVT t) /\
+  (VARS (s <<= t) = FVT s UNION FVT t) /\
+  (VARS (Not p) = VARS p) /\
+  (VARS (p && q) = VARS p UNION VARS q) /\
+  (VARS (p || q) = VARS p UNION VARS q) /\
+  (VARS (p --> q) = VARS p UNION VARS q) /\
+  (VARS (p <-> q) = VARS p UNION VARS q) /\
+  (VARS (!! x p) = x INSERT VARS p) /\
+  (VARS (?? x p) = x INSERT VARS p)`;;
+
+let VARS_FINITE = prove
+ (`!p. FINITE(VARS p)`,
+  MATCH_MP_TAC form_INDUCT THEN
+  ASM_SIMP_TAC[VARS; FINITE_RULES; FVT_FINITE; FINITE_UNION; FINITE_DELETE]);;
+
+let FV_SUBSET_VARS = prove
+ (`!p. FV(p) SUBSET VARS(p)`,
+  REWRITE_TAC[SUBSET] THEN
+  MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[FV; VARS] THEN
+  REWRITE_TAC[IN_INSERT; IN_UNION; IN_DELETE] THEN MESON_TAC[]);;
+
+let TERMSUBST_TWICE_GENERAL = prove
+ (`!x z t v s. ~(z IN FVT s)
+               ==> (termsubst ((x |-> t) v) s =
+                    termsubst ((z |-> t) v) (termsubst (x |=> V z) s))`,
+  GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
+  MATCH_MP_TAC term_INDUCT THEN
+  REWRITE_TAC[termsubst; ASSIGN; valmod; FVT; IN_SING; IN_UNION] THEN
+  MESON_TAC[termsubst; ASSIGN]);;
+
+let TERMSUBST_TWICE = prove
+ (`!x z t s. ~(z IN FVT s)
+             ==> (termsubst (x |=> t) s =
+                  termsubst (z |=> t) (termsubst (x |=> V z) s))`,
+  MESON_TAC[assign; TERMSUBST_TWICE_GENERAL]);;
+
+let FORMSUBST_TWICE_GENERAL = prove
+ (`!z p x t v. ~(z IN VARS p)
+               ==> (formsubst ((z |-> t) v) (formsubst (x |=> V z) p) =
+                    formsubst ((x |-> t) v) p)`,
+  GEN_TAC THEN MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[CONJ_ASSOC] THEN
+  GEN_REWRITE_TAC I [GSYM CONJ_ASSOC] THEN CONJ_TAC THENL
+   [REWRITE_TAC[formsubst; ASSIGN; VARS; IN_UNION; DE_MORGAN_THM] THEN
+    MESON_TAC[TERMSUBST_TWICE_GENERAL];
+    ALL_TAC] THEN
+  CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`y:num`; `p:form`] THEN
+  (REWRITE_TAC[VARS; IN_INSERT; DE_MORGAN_THM] THEN
+   DISCH_THEN(fun th -> REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC th) THEN
+   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
+   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [formsubst] THEN
+   COND_CASES_TAC THENL
+    [FIRST_X_ASSUM(CHOOSE_THEN MP_TAC) THEN
+     REWRITE_TAC[ASSIGN; FV; IN_DELETE] THEN
+     ASM_MESON_TAC[FVT; IN_SING];
+     ALL_TAC] THEN
+   REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
+   ASM_CASES_TAC `x:num = y` THENL
+    [ASM_REWRITE_TAC[assign; VALMOD_VALMOD_BASIC; VALMOD_REPEAT;
+                     FORMSUBST_TRIV] THEN
+     MATCH_MP_TAC FORMSUBST_EQ THEN
+     ASM_REWRITE_TAC[valmod; FV; IN_DELETE] THEN
+     ASM_MESON_TAC[FV_SUBSET_VARS; SUBSET];
+     ALL_TAC] THEN
+   SUBGOAL_THEN
+    `(!t. (y |-> V y) (x |=> t) = x |=> t) /\
+     (!t. (y |-> V y) (z |=> t) = z |=> t)`
+   STRIP_ASSUME_TAC THENL
+    [REWRITE_TAC[assign] THEN ASM_MESON_TAC[VALMOD_SWAP; VALMOD_REPEAT];
+     ALL_TAC] THEN
+   ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC BINOP_CONV [formsubst] THEN
+   ASM_REWRITE_TAC[FV] THEN
+   SUBGOAL_THEN
+    `(?u. u IN (FV(formsubst (x |=> V z) p) DELETE y) /\
+          y IN FVT ((z |-> t) v u)) =
+     (?u. u IN (FV p DELETE y) /\ y IN FVT ((x |-> t) v u))`
+   SUBST1_TAC THENL
+    [REWRITE_TAC[FV; FORMSUBST_FV; IN_ELIM_THM; IN_DELETE; valmod; ASSIGN] THEN
+     ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RAND] THEN
+     REWRITE_TAC[FVT; IN_SING] THEN
+     ASM_MESON_TAC[SUBSET; FV_SUBSET_VARS; FVT; IN_SING];
+     ALL_TAC] THEN
+   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
+    [ALL_TAC;
+     REWRITE_TAC[LET_DEF; LET_END_DEF; form_INJ] THEN
+     ASM_MESON_TAC[VALMOD_SWAP]] THEN
+   REWRITE_TAC[LET_DEF; LET_END_DEF; form_INJ] THEN
+   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
+    [ALL_TAC; DISCH_THEN SUBST1_TAC] THEN
+   REPEAT AP_TERM_TAC THEN ASM_MESON_TAC[VALMOD_SWAP]));;
+
+let FORMSUBST_TWICE = prove
+ (`!z p x t. ~(z IN VARS p)
+             ==> (formsubst (z |=> t) (formsubst (x |=> V z) p) =
+                  formsubst (x |=> t) p)`,
+  MESON_TAC[assign; FORMSUBST_TWICE_GENERAL]);;
+
+let ispec_lemma = prove
+ (`!A x p t. ~(x IN FVT(t)) ==> A |-- !!x p --> formsubst (x |=> t) p`,
+  REPEAT STRIP_TAC THEN MATCH_MP_TAC subspec THEN
+  EXISTS_TAC `t:term` THEN ASM_REWRITE_TAC[isubst_var] THEN
+  ASM_REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; ASSIGN] THEN
+  ASM_MESON_TAC[FVT; IN_SING]);;
+
+let ispec = prove
+ (`!A x p t. A |-- !!x p --> formsubst (x |=> t) p`,
+  REPEAT STRIP_TAC THEN ASM_CASES_TAC `x IN FVT(t)` THEN
+  ASM_SIMP_TAC[ispec_lemma] THEN
+  ABBREV_TAC `z = VARIANT (FVT t UNION VARS p)` THEN
+  MATCH_MP_TAC imp_trans THEN
+  EXISTS_TAC `!!z (formsubst (x |=> V z) p)` THEN CONJ_TAC THENL
+   [MATCH_MP_TAC alpha THEN EXPAND_TAC "z" THEN
+    MATCH_MP_TAC NOT_IN_VARIANT THEN
+    REWRITE_TAC[FINITE_UNION; SUBSET; IN_UNION] THEN
+    MESON_TAC[SUBSET; FVT_FINITE; VARS_FINITE; FV_SUBSET_VARS];
+    SUBGOAL_THEN
+     `formsubst (x |=> t) p =
+      formsubst (z |=> t) (formsubst (x |=> V z) p)`
+    SUBST1_TAC THENL
+     [MATCH_MP_TAC(GSYM FORMSUBST_TWICE); MATCH_MP_TAC ispec_lemma] THEN
+    EXPAND_TAC "z" THEN MATCH_MP_TAC NOT_IN_VARIANT THEN
+    REWRITE_TAC[VARS_FINITE; FVT_FINITE; FINITE_UNION] THEN
+    SIMP_TAC[SUBSET; IN_UNION]]);;
+
+let spec = prove
+ (`!A x p t. A |-- !!x p ==> A |-- formsubst (x |=> t) p`,
+  MESON_TAC[ispec; modusponens]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Monotonicity and the deduction theorem.                                   *)
+(* ------------------------------------------------------------------------- *)
+
+let PROVES_MONO = prove
+ (`!A B p. A SUBSET B /\ A |-- p ==> B |-- p`,
+  GEN_TAC THEN GEN_TAC THEN
+  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
+  MATCH_MP_TAC proves_INDUCT THEN  ASM_MESON_TAC[proves_RULES; SUBSET]);;
+
+let DEDUCTION_LEMMA = prove
+ (`!A p q. p INSERT A |-- q /\ closed p ==> A |-- p --> q`,
+  GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
+  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
+  GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC proves_INDUCT THEN
+  REPEAT CONJ_TAC THEN X_GEN_TAC `r:form` THENL
+   [REWRITE_TAC[IN_INSERT] THEN MESON_TAC[proves_RULES; add_assum; imp_refl];
+    MESON_TAC[modusponens; axiom_distribimp];
+    ASM_MESON_TAC[gen_right; closed; NOT_IN_EMPTY]]);;
+
+let DEDUCTION = prove
+ (`!A p q. closed p ==> (A |-- p --> q <=> p INSERT A |-- q)`,
+  MESON_TAC[DEDUCTION_LEMMA; modusponens; IN_INSERT; proves_RULES;
+            PROVES_MONO; SUBSET]);;