(* ========================================================================= *)
(* 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]);;
(* ------------------------------------------------------------------------- *) (* Some purely propositional schemas and 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_th = 
prove (`!A p q r. A |-- (q --> r) --> (p --> q) --> (p --> r)`,
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)`,
let contrapos = 
prove (`!A p q. A |-- p --> q ==> A |-- Not q --> Not p`,
let imp_truefalse = 
prove (`!p q. A |-- (q --> False) --> p --> (p --> q) --> False`,
let imp_insert = 
prove (`!A p q r. A |-- p --> r ==> A |-- p --> q --> r`,
MESON_TAC[imp_trans; axiom_addimp]);;
let imp_mono_th = 
prove (`A |-- (p' --> p) --> (q --> q') --> (p --> q) --> (p' --> q')`,
let ex_falso = 
prove (`!A p. A |-- False --> p`,
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_false_rule = 
prove (`!p q r. A |-- (q --> False) --> p --> r ==> A |-- ((p --> q) --> False) --> r`,
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 truth = 
prove (`!A. A |-- True`,
MESON_TAC[modusponens; axiom_true; imp_refl; iff_imp2]);;
let and_left = 
prove (`!A p q. A |-- p && q --> p`,
let and_right = 
prove (`!A p q. A |-- p && q --> q`,
let and_pair = 
prove (`!A p q. A |-- p --> q --> p && q`,
let META_AND = 
prove (`!A p q. A |-- p && q <=> A |-- p /\ A |-- q`,
MESON_TAC[and_left; and_right; and_pair; modusponens]);;
let shunt = 
prove (`!A p q r. A |-- p && q --> r ==> A |-- p --> q --> r`,
MESON_TAC[modusponens; imp_add_assum; and_pair]);;
let ante_conj = 
prove (`!A p q r. A |-- p --> q --> r ==> A |-- p && q --> r`,
let not_not_false = 
prove (`!A p. A |-- (p --> False) --> False <-> p`,
let iff_sym = 
prove (`!A p q. A |-- p <-> q <=> A |-- q <-> p`,
MESON_TAC[iff_imp1; iff_imp2; imp_antisym]);;
let iff_trans = 
prove (`!A p q r. A |-- p <-> q /\ A |-- q <-> r ==> A |-- p <-> r`,
let not_not = 
prove (`!A p. A |-- Not(Not p) <-> p`,
let contrapos_eq = 
prove (`!A p q. A |-- Not p --> Not q <=> A |-- q --> p`,
MESON_TAC[contrapos; not_not; iff_imp1; iff_imp2; imp_trans]);;
let or_left = 
prove (`!A p q. A |-- q --> p || q`,
MESON_TAC[imp_trans; not_not; iff_imp2; and_right; contrapos; axiom_or]);;
let or_right = 
prove (`!A p q. A |-- p --> p || q`,
MESON_TAC[imp_trans; not_not; iff_imp2; and_left; contrapos; axiom_or]);;
let ante_disj = 
prove (`!A p q r. A |-- p --> r /\ A |-- q --> r ==> A |-- p || q --> r`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM contrapos_eq] THEN MESON_TAC[imp_trans; imp_trans_chain_2; and_pair; contrapos_eq; not_not; axiom_or; iff_imp1; iff_imp2; imp_trans]);;
let iff_def = 
prove (`!A p q. A |-- (p <-> q) <-> (p --> q) && (q --> p)`,
let iff_refl = 
prove (`!A p. A |-- p <-> p`,
MESON_TAC[imp_antisym; imp_refl]);;
(* ------------------------------------------------------------------------- *) (* 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]);;
(* ------------------------------------------------------------------------- *) (* 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 (`!p i j. (!x. x IN VARS p ==> safe_for x i) ==> formsubst j (formsubst i p) = formsubst (termsubst j o i) p`,
MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[VARS; FORALL_IN_INSERT; IN_UNION; NOT_IN_EMPTY; FORALL_AND_THM; TAUT `p \/ q ==> r <=> (p ==> r) /\ (q ==> r)`] THEN SIMP_TAC[FORMSUBST_SAFE_FOR] THEN REWRITE_TAC[formsubst; TERMSUBST_TERMSUBST] THEN SIMP_TAC[] THEN CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`i:num->term`; `j:num->term`] THEN STRIP_TAC THEN REWRITE_TAC[FV; FORMSUBST_FV; TERMSUBST_FVT; o_THM; IN_ELIM_THM; IN_DELETE] THEN (SUBGOAL_THEN `(?y. ((?y'. y' IN FV p /\ y IN FVT ((x |-> V x) i y')) /\ ~(y = x)) /\ x IN FVT (j y)) <=> (?y. (y IN FV p /\ ~(y = x)) /\ (?y'. y' IN FVT (i y) /\ x IN FVT (j y')))` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN X_GEN_TAC `y:num` THEN ASM_CASES_TAC `y IN FV p` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `y:num = x` THEN ASM_REWRITE_TAC[] THENL [ASM_REWRITE_TAC[VALMOD; FVT; IN_SING] THEN MESON_TAC[]; ALL_TAC] THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN X_GEN_TAC `z:num` THEN ASM_CASES_TAC `x IN FVT(j(z:num))` THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[VALMOD] THEN ASM_MESON_TAC[safe_for]; ALL_TAC] THEN CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL [SUBGOAL_THEN `{x' | ?y. (?y'. y' IN FV p /\ y IN FVT ((x |-> V x) i y')) /\ x' IN FVT ((x |-> V x) j y)} = {x' | ?y. y IN FV p /\ x' IN FVT ((x |-> V x) (termsubst j o i) y)}` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN X_GEN_TAC `z:num` THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN X_GEN_TAC `y:num` THEN ASM_CASES_TAC `y IN FV p` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `y:num = x` THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[VALMOD; FVT; IN_SING; UNWIND_THM2] THEN REWRITE_TAC[o_THM; TERMSUBST_FVT; IN_ELIM_THM] THEN ASM_MESON_TAC[safe_for]; ABBREV_TAC `z = VARIANT {x' | ?y. y IN FV p /\ x' IN FVT ((x |-> V x) (termsubst j o i) y)}`]; ALL_TAC]) THEN AP_TERM_TAC THEN FIRST_X_ASSUM(fun th -> W(MP_TAC o PART_MATCH (lhs o rand) th o lhs o snd)) THEN ASM_SIMP_TAC[SAFE_FOR_VALMOD; FVT; IN_SING] THEN DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC FORMSUBST_EQ THEN X_GEN_TAC `y:num` THEN DISCH_TAC THEN REWRITE_TAC[VALMOD; o_THM] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[termsubst; VALMOD] THEN MATCH_MP_TAC TERMSUBST_EQ THEN X_GEN_TAC `w:num` THEN REWRITE_TAC[VALMOD] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[safe_for]);;
let FORMSUBST_TWICE = 
prove (`!z p x t. ~(z IN VARS p) ==> (formsubst (z |=> t) (formsubst (x |=> V z) p) = formsubst (x |=> t) p)`,
REPEAT STRIP_TAC THEN W(MP_TAC o PART_MATCH (lhs o rand) FORMSUBST_TWICE_GENERAL o lhs o snd) THEN REWRITE_TAC[SAFE_FOR_ASSIGN; FVT; IN_SING] THEN ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST1_TAC] THEN MATCH_MP_TAC FORMSUBST_EQ THEN REPEAT STRIP_TAC THEN REWRITE_TAC[o_THM; VALMOD; ASSIGN] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[termsubst; ASSIGN] THEN ASM_MESON_TAC[FV_SUBSET_VARS; SUBSET]);;
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]);;
let spec_var = 
prove (`!A x p. A |-- !!x p ==> A |-- p`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o SPEC `V x` o MATCH_MP spec) THEN SIMP_TAC[ASSIGN_TRIV; FORMSUBST_TRIVIAL]);;
let instantiation = 
prove (`!A v p. A |-- p ==> A |-- formsubst v p`,
let lemma = prove
   (`!A p v. (!x y. x IN FV p /\ y IN FV p /\ x IN FVT(v y)
                    ==> x = y /\ v x = V x) /\
             A |-- p
             ==> A |-- formsubst v p`,
    REPEAT GEN_TAC THEN
    WF_INDUCT_TAC `CARD {x | x IN FV(p) /\ ~(v x = V x)}` THEN
    ASM_CASES_TAC `!x. x IN FV p ==> v x = V x` THEN
    ASM_SIMP_TAC[FORMSUBST_TRIVIAL] THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
    REWRITE_TAC[NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
    X_GEN_TAC `x:num` THEN REPEAT STRIP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPECL [`p:form`; `(x |-> V x) v`]) THEN
    ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
     [MATCH_MP_TAC CARD_PSUBSET THEN SIMP_TAC[FINITE_RESTRICT; FV_FINITE] THEN
      REWRITE_TAC[PSUBSET_ALT] THEN CONJ_TAC THENL
       [REWRITE_TAC[SUBSET; VALMOD; IN_ELIM_THM] THEN ASM_MESON_TAC[];
        EXISTS_TAC `x:num` THEN ASM_REWRITE_TAC[VALMOD; IN_ELIM_THM] THEN
        ASM_MESON_TAC[]];
      ALL_TAC] THEN
    ANTS_TAC THENL
     [REPEAT GEN_TAC THEN REWRITE_TAC[VALMOD] THEN
      COND_CASES_TAC THEN ASM_SIMP_TAC[FVT; IN_SING] THEN ASM_MESON_TAC[];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `formsubst v p = formsubst ((x |-> v x) v) p`
    SUBST1_TAC THENL [SIMP_TAC[VALMOD_TRIVIAL]; ALL_TAC] THEN
    DISCH_THEN(MP_TAC o SPEC `x:num` o MATCH_MP gen) THEN
    MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] modusponens) THEN
    MATCH_MP_TAC exists_imp THEN CONJ_TAC THENL
     [ALL_TAC;
      REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM; NOT_EXISTS_THM; VALMOD] THEN
      ASM SET_TAC[]] THEN
    MATCH_MP_TAC modusponens THEN EXISTS_TAC `??x (V x === v x)` THEN
    SIMP_TAC[eximp; isubst_general] THEN ASM_MESON_TAC[axiom_existseq]) in
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN
   `?n. !x. x IN VARS p \/ x IN FV(formsubst v p) ==> x < n`
  STRIP_ASSUME_TAC THENL
   [EXISTS_TAC `SUC(SETMAX(VARS p UNION FV(formsubst v p)))` THEN
    REWRITE_TAC[GSYM IN_UNION; LT_SUC_LE] THEN MATCH_MP_TAC SETMAX_MEMBER THEN
    REWRITE_TAC[FINITE_UNION; VARS_FINITE; FV_FINITE];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `formsubst v p =
    formsubst (\i. v(i - n)) (formsubst (\i. V(i + n)) p)`
  SUBST1_TAC THENL
   [W(MP_TAC o PART_MATCH (lhs o rand) FORMSUBST_TWICE_GENERAL o
      rand o snd) THEN
    REWRITE_TAC[safe_for; FVT; IN_SING] THEN ANTS_TAC THENL
     [ASM_MESON_TAC[ARITH_RULE `~(x + n:num < n)`];
      DISCH_THEN SUBST1_TAC THEN
      REWRITE_TAC[o_DEF; termsubst; ADD_SUB; ETA_AX]];
    MATCH_MP_TAC lemma THEN REWRITE_TAC[FVT] THEN CONJ_TAC THENL
     [REWRITE_TAC[FORMSUBST_FV; FVT; IN_SING] THEN
      REWRITE_TAC[SET_RULE `{x | ?y. y IN s /\ x = f y} = IMAGE f s`] THEN
      REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
      X_GEN_TAC `x:num` THEN DISCH_TAC THEN REWRITE_TAC[ADD_SUB; FVT] THEN
      X_GEN_TAC `y:num` THEN REPEAT DISCH_TAC THEN
      FIRST_X_ASSUM(MP_TAC o SPEC `x + n:num`) THEN
      MATCH_MP_TAC(TAUT `~p /\ q ==> (r \/ q ==> p) ==> s`) THEN
      CONJ_TAC THENL [ARITH_TAC; REWRITE_TAC[FORMSUBST_FV; IN_ELIM_THM]] THEN
      ASM_MESON_TAC[];
      MATCH_MP_TAC lemma THEN REWRITE_TAC[FVT; IN_SING] THEN
      ASM_MESON_TAC[ARITH_RULE `x < n /\ y < n ==> ~(x = y + n)`;
                    FV_SUBSET_VARS; SUBSET]]]);;
(* ------------------------------------------------------------------------- *) (* 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]);;
(* ------------------------------------------------------------------------- *) (* A few more derived rules. *) (* ------------------------------------------------------------------------- *)
let eq_trans = 
prove (`!A s t u. A |-- s === t --> t === u --> s === u`,
MESON_TAC[axiom_predcong; modusponens; imp_swap; axiom_eqrefl; imp_trans; eq_sym]);;
let spec_right = 
prove (`!A p q x. A |-- p --> !!x q ==> A |-- p --> formsubst (x |=> t) q`,
MESON_TAC[imp_trans; ispec]);;
let eq_trans_rule = 
prove (`!A s t u. A |-- s === t /\ A |-- t === u ==> A |-- s === u`,
MESON_TAC[modusponens; eq_trans]);;
let eq_sym_rule = 
prove (`!A s t. A |-- s === t <=> A |-- t === s`,
MESON_TAC[modusponens; eq_sym]);;
let allimp = 
prove (`!A x p q. A |-- p --> q ==> A |-- !!x p --> !!x q`,
MESON_TAC[axiom_allimp; modusponens; gen]);;
let alliff = 
prove (`!A x p q. A |-- p <-> q ==> A |-- !!x p <-> !!x q`,
MESON_TAC[allimp; iff_imp1; iff_imp2; imp_antisym]);;
let exiff = 
prove (`!A x p q. A |-- p <-> q ==> A |-- ??x p <-> ??x q`,
MESON_TAC[eximp; iff_imp1; iff_imp2; imp_antisym]);;
let cong_suc = 
prove (`!A s t. A |-- s === t ==> A |-- Suc s === Suc t`,
MESON_TAC[modusponens; axiom_funcong]);;
let cong_add = 
prove (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s ++ u === t ++ v`,
MESON_TAC[modusponens; axiom_funcong]);;
let cong_mul = 
prove (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s ** u === t ** v`,
MESON_TAC[modusponens; axiom_funcong]);;
let cong_eq = 
prove (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s === u <-> t === v`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC imp_antisym THEN ASM_MESON_TAC[modusponens; axiom_predcong; eq_sym]);;
let cong_le = 
prove (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s <<= u <-> t <<= v`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC imp_antisym THEN ASM_MESON_TAC[modusponens; axiom_predcong; eq_sym]);;
let cong_lt = 
prove (`!A s t u v. A |-- s === t /\ A |-- u === v ==> A |-- s << u <-> t << v`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC imp_antisym THEN ASM_MESON_TAC[modusponens; axiom_predcong; eq_sym]);;
let iexists = 
prove (`!A x t p. A |-- formsubst (x |=> t) p --> ??x p`,
REPEAT GEN_TAC THEN TRANS_TAC imp_trans `Not(!!x (Not p))` THEN CONJ_TAC THENL [ALL_TAC; MESON_TAC[axiom_exists; iff_imp2]] THEN TRANS_TAC imp_trans `Not(formsubst (x |=> t) (Not p))` THEN REWRITE_TAC[contrapos_eq; ispec] THEN REWRITE_TAC[formsubst] THEN MESON_TAC[not_not; iff_imp2]);;
let exists_intro = 
prove (`!A x t p. A |-- formsubst (x |=> t) p ==> A |-- ??x p`,
MESON_TAC[iexists; modusponens]);;
let impex = 
prove (`!A x p. ~(x IN FV p) ==> A |-- (??x p) --> p`,
REPEAT STRIP_TAC THEN TRANS_TAC imp_trans `Not(Not p)` THEN CONJ_TAC THENL [ALL_TAC; MESON_TAC[not_not; iff_imp1]] THEN TRANS_TAC imp_trans `Not(!!x (Not p))` THEN ASM_SIMP_TAC[contrapos_eq; axiom_impall; FV] THEN MESON_TAC[axiom_exists; iff_imp1]);;
let ichoose = 
prove (`!A x p q. A |-- !!x (p --> q) /\ ~(x IN FV q) ==> A |-- (??x p) --> q`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP spec_var) THEN DISCH_THEN(MP_TAC o SPEC `x:num` o MATCH_MP eximp) THEN MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] imp_trans) THEN ASM_SIMP_TAC[impex]);;
let eq_trans_imp = 
prove (`A |-- s === s' /\ A |-- t === t' ==> A |-- s === t --> s' === t'`,
MESON_TAC[axiom_predcong; modusponens]);;
(* ------------------------------------------------------------------------- *) (* Some conversions for performing explicit substitution operations in what *) (* we hope is the common case where no variable renaming occurs. *) (* ------------------------------------------------------------------------- *) let fv_theorems = ref [FV; FV_AXIOM; FV_DIAGONALIZE; FV_DIVIDES; FV_FINITE; FV_FIXPOINT; FV_FORM; FV_FORM1; FV_FREEFORM; FV_FREEFORM1; FV_FREETERM; FV_FREETERM1; FV_GNUMERAL; FV_GNUMERAL1; FV_GNUMERAL1'; FV_GSENTENCE; FV_HSENTENCE; FV_PRIME; FV_PRIMEPOW; FV_PRIMREC; FV_PRIMRECSTEP; FV_PROV; FV_PROV1; FV_QDIAG; FV_QSUBST; FV_RTC; FV_RTCP; FV_SUBSET_VARS; FV_TERM; FV_TERM1; FVT; FVT_NUMERAL];; let IN_FV_RULE ths tm = try EQT_ELIM ((GEN_REWRITE_CONV TOP_DEPTH_CONV ([IN_UNION; IN_DELETE; NOT_IN_EMPTY; IN_INSERT] @ ths @ !fv_theorems) THENC NUM_REDUCE_CONV) tm) with Failure _ -> ASSUME tm;; let rec SAFE_FOR_RULE tm = try PART_MATCH I SAFE_FOR_V tm with Failure _ -> try let th1 = PART_MATCH lhand SAFE_FOR_ASSIGN tm in let th2 = IN_FV_RULE [] (rand(concl th1)) in EQ_MP (SYM th1) th2 with Failure _ -> let th1 = PART_MATCH rand SAFE_FOR_VALMOD tm in let l,r = dest_conj(lhand(concl th1)) in let th2 = CONJ (SAFE_FOR_RULE l) (IN_FV_RULE [] r) in MP th1 th2;; let VALMOD_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV [ASSIGN; VALMOD] THENC NUM_REDUCE_CONV;;
let TERMSUBST_NUMERAL = 
prove (`!v n. termsubst v (numeral n) = numeral n`,
let rec TERMSUBST_CONV tm = (GEN_REWRITE_CONV I [CONJ TERMSUBST_NUMERAL (CONJUNCT1 termsubst)] ORELSEC (GEN_REWRITE_CONV I [el 1 (CONJUNCTS termsubst)] THENC VALMOD_CONV) ORELSEC (GEN_REWRITE_CONV I [el 2 (CONJUNCTS termsubst)] THENC RAND_CONV TERMSUBST_CONV) ORELSEC (GEN_REWRITE_CONV I [funpow 3 CONJUNCT2 termsubst] THENC BINOP_CONV TERMSUBST_CONV)) tm;; let rec FORMSUBST_CONV tm = (GEN_REWRITE_CONV I [el 0 (CONJUNCTS formsubst); el 1 (CONJUNCTS formsubst)] ORELSEC (GEN_REWRITE_CONV I [el 2 (CONJUNCTS formsubst); el 3 (CONJUNCTS formsubst); el 4 (CONJUNCTS formsubst)] THENC BINOP_CONV TERMSUBST_CONV) ORELSEC (GEN_REWRITE_CONV I [el 5 (CONJUNCTS formsubst)] THENC RAND_CONV FORMSUBST_CONV) ORELSEC (GEN_REWRITE_CONV I [el 6 (CONJUNCTS formsubst); el 7 (CONJUNCTS formsubst); el 8 (CONJUNCTS formsubst); el 9 (CONJUNCTS formsubst)] THENC BINOP_CONV FORMSUBST_CONV) ORELSEC ((fun tm -> let th = try PART_MATCH (lhand o rand) (CONJUNCT1 FORMSUBST_SAFE_FOR) tm with Failure _ -> PART_MATCH (lhand o rand) (CONJUNCT2 FORMSUBST_SAFE_FOR) tm in MP th (SAFE_FOR_RULE (lhand(concl th)))) THENC RAND_CONV FORMSUBST_CONV)) tm;; (* ------------------------------------------------------------------------- *) (* Hence a more convenient specialization rule. *) (* ------------------------------------------------------------------------- *) let spec_var_rule th = MATCH_MP spec_var th;; let spec_all_rule = repeat spec_var_rule;; let instantiate_rule ilist th = let v_tm = `(|->):num->term->(num->term)->(num->term)` in let v = itlist (fun (t,x) v -> mk_comb(mk_comb(mk_comb(v_tm,mk_small_numeral x),t),v)) ilist `V` in CONV_RULE (RAND_CONV FORMSUBST_CONV) (SPEC v (MATCH_MP instantiation th));; let specl_rule tms th = let avs = striplist (dest_binop `!!`) (rand(concl th)) in let vs = fst(chop_list(length tms) avs) in let ilist = map2 (fun t v -> (t,dest_small_numeral v)) tms vs in instantiate_rule ilist (funpow (length vs) spec_var_rule th);; let spec_rule t th = specl_rule [t] th;; let gen_rule t th = SPEC (mk_small_numeral t) (MATCH_MP gen th);; let gens_tac ns (asl,w) = let avs,bod = nsplit dest_forall ns w in let nvs = map (curry mk_comb `V` o mk_small_numeral) ns in let bod' = subst (zip nvs avs) bod in let th = GENL avs (instantiate_rule (zip avs ns) (ASSUME bod')) in MATCH_MP_TAC (DISCH_ALL th) (asl,w);; let gen_tac n = gens_tac [n];;