(* * HOL Light proof that e is transcendental. * * This HOL Light proof and its relationship to the informal proof is * described in : * * "Formalizing a Proof that e is Transcendental", Journal of Formal * Reasoning, Vol 4, No 1. 2011. * * It follows the informal proof provided by the good folks at the * planetmath website: * * http://planetmath.org/encyclopedia/EIsTranscendental2.html * * Note: the original proof script linked to in the above paper * partitioned the proofs amongst several files, each encapsulated * in an Ocaml module. This file has simply concatenated those files * and hence the module structure persists. * * Jesse Bingham, Jan 2012 * jesse.d.bingham@intel.com * jesse.bingham@gmail.com *) (* this is needed since the sum from the HOL core (iter.ml, i think) * which is used below, gets overwritten when Library/analysis.ml is loaded. *) let OLD_SUM = sum;; (* required stuff from HOL Light library... *) needs "Library/binomial.ml";; needs "Library/analysis.ml";; needs "Library/transc.ml";; needs "Library/prime.ml";; needs "Library/iter.ml";; needs "Library/integer.ml";; needs "Library/floor.ml";; (* get def of transcendental from Harrison's Liouville proof *) needs "100/liouville.ml";; prioritize_real();; (* * A few misculaneous proof utility functions *) (* A listified version of ADD_ASSUM *) let ADD_ASSUMS lst thm = let f x y = ADD_ASSUM y x in List.fold_left f thm lst ;; (* A tactic that takes a goal with an assumption A /\ B and replaces * it with a goal with the two assumptions A and B *) let SPLIT_CONJOINED_ASSUMPT_TAC t = (UNDISCH_TAC t) THEN (ONCE_REWRITE_TAC [TAUT `(X /\ Y ==> Z) <=> (X ==> Y ==> Z)`]) THEN (DISCH_TAC THEN DISCH_TAC) ;; (* Adds an assumption and discharges it in one fell swoop *) let ADD_ASSUM_DISCH ass thm = DISCH ass (ADD_ASSUM ass thm);; (* BRW = Bolean ReWrite *) let BRW t f = ONCE_REWRITE_RULE [TAUT t] f;; (* Those two boolean rewrites come in handy *) let BRW0 f = BRW `(X ==> Y ==> Z) <=> (X /\ Y ==> Z)` f;; let BRW1 f = BRW `(X /\ Y ==> Z) <=> (X ==> Y ==> Z)` f;; (* a bunch of trivial real theorems that are useful for * rewriting/simplifying/mesoning *) let rewrites0 = map REAL_ARITH [`&0 + (y:real) = y`;`(x:real) * &0 = &0`;`(&1:real) + &0 = &1`;`(x:real) * &1 = x`];; module Pm_lemma1 = struct let PDI_DEF = new_recursive_definition num_RECURSION ` (poly_diff_iter p 0 = p) /\ (poly_diff_iter p (SUC n) = poly_diff (poly_diff_iter p n)) ` let PDI_POLY_DIFF_COMM = prove( `! p n.(poly_diff_iter (poly_diff p) n) = (poly_diff (poly_diff_iter p n))`, STRIP_TAC THEN INDUCT_TAC THEN (ASM_SIMP_TAC [PDI_DEF]) ) let SODN = new_definition `SODN p n = iterate poly_add (0..n) (\i.poly_diff_iter p i)` ;; let SOD = new_definition `!p. SOD p = SODN p (LENGTH p)`;; let PHI = new_definition `Phi f x = (exp (-- x)) * (poly (SOD f) x)` let PLANETMATH_EQN_1_1_1 = prove( `! x f.((Phi f) diffl ((exp (--x)) * ((poly (poly_diff (SOD f)) x) - (poly (SOD f) x))) )(x)`, let lem1 = SPECL [`\x.exp (--x)`; `\x.poly (SOD f) x`; `--(exp (--x))`; `poly (poly_diff (SOD f)) x`; `x:real`] DIFF_MUL in let EXP_NEG_X_DIFF = prove( `!x. ((\x.exp (--x)) diffl (-- (exp (--x))))(x)`, STRIP_TAC THEN DIFF_TAC THEN REAL_ARITH_TAC) in let lem2 = SPEC `x:real` EXP_NEG_X_DIFF in let lem3 = SPECL [`SOD f`;`x:real`] POLY_DIFF in let lem4 = CONJ lem2 lem3 in let lem5 = BETA_RULE (MP lem1 lem4) in let lem6 = REAL_ARITH `(a*(b - c)) = (-- a*c) + (b*a)` in let PHI_abs = prove( `Phi f = \x.((exp (-- x)) * (poly (SOD f) x))`, (PURE_REWRITE_TAC [SYM (ABS `x:real` (SPEC_ALL PHI))]) THEN (ACCEPT_TAC (SYM (ETA_CONV `\x.(Phi f x)`)))) in (REPEAT STRIP_TAC) THEN (REWRITE_TAC [PHI_abs]) THEN (REWRITE_TAC [lem6]) THEN (ACCEPT_TAC lem5) ) let POLY_SUB = prove( `!p1 p2 x. poly (p1 ++ (neg p2)) x = poly p1 x - poly p2 x`, (REWRITE_TAC [POLY_ADD;poly_neg;POLY_CMUL]) THEN REAL_ARITH_TAC ) let ZERO_INSERT_NUMSEG = prove( `!n. (0..n) = (0 INSERT (1..n))`, let lem01 = SIMP_RULE [ARITH_RULE `0 <= n`] (SPECL [`0`;`n:num`] NUMSEG_LREC) in let lem02 = SIMP_RULE [ARITH_RULE `0 + 1 = 1`] lem01 in (ACCEPT_TAC (GEN_ALL (GSYM lem02))) ) let PDI_POLYDIFF_SUC_LEMMA = prove( `!f n .(poly_diff_iter (poly_diff f) n) = poly_diff_iter f (SUC n)`, STRIP_TAC THEN INDUCT_TAC THENL [ (SIMP_TAC [PDI_DEF]); (ONCE_REWRITE_TAC [PDI_DEF]) THEN (ONCE_REWRITE_TAC [PDI_DEF]) THEN (SIMP_TAC [PDI_POLY_DIFF_COMM]) ] ) let SOD_POLY_DIFF_ITERATE = prove( `!f .(SOD (poly_diff f)) = iterate (++) (1..(LENGTH f)) (\i.poly_diff_iter f i)`, let lemA1 = SPECL [`1`;`0`] NUMSEG_EMPTY in let lemA2 = SIMP_RULE [ARITH_RULE `0 < 1`] lemA1 in let lem1 = MATCH_MP ITERATE_IMAGE_NONZERO MONOIDAL_POLY_ADD in let lem2 = ISPECL [`poly_diff_iter f`;`SUC`;`0..(LENGTH (poly_diff f))`] lem1 in let lem3 = SIMP_RULE [FINITE_NUMSEG] lem2 in let lem4 = ONCE_REWRITE_RULE [ARITH_RULE `~(~(x=y) /\ (SUC x) = (SUC y))`] lem3 in let lem5 = SIMP_RULE [] lem4 in let lem6 = ISPECL [`0`;`n:num`;`1`] NUMSEG_OFFSET_IMAGE in let lem7 = SIMP_RULE [ARITH_RULE `!m.m+1 = SUC m`] lem6 in let lem8 = SIMP_RULE [ARITH_RULE `SUC 0 = 1`] lem7 in let lem9 = ONCE_REWRITE_RULE [ETA_CONV `(\i. SUC i)`] lem8 in let lem10 = ONCE_REWRITE_RULE [GSYM lem9] lem5 in let lem11 = ONCE_REWRITE_RULE [GSYM (ETA_CONV `(\i. poly_diff_iter f i)`)] lem10 in let lem12 = SIMP_RULE [o_DEF] lem11 in let lemma0 = prove( `! h t.SUC (LENGTH (poly_diff (CONS h t))) = LENGTH (CONS h t)`, (SIMP_TAC [LENGTH_POLY_DIFF;LENGTH;PRE]) ) in (ONCE_REWRITE_TAC [SOD]) THEN (ONCE_REWRITE_TAC [SODN]) THEN (ONCE_REWRITE_TAC [PDI_POLYDIFF_SUC_LEMMA ]) THEN LIST_INDUCT_TAC THENL [ (SIMP_TAC [poly_diff;LENGTH]) THEN (SIMP_TAC [GSYM lemma0;lem12]) THEN (SIMP_TAC [NUMSEG_SING;MONOIDAL_POLY_ADD;ITERATE_SING]) THEN (SIMP_TAC [lemA2;MATCH_MP ITERATE_CLAUSES_GEN MONOIDAL_POLY_ADD]) THEN (ONCE_REWRITE_TAC [POLY_ADD_IDENT]) THEN (SIMP_TAC [PDI_DEF;POLY_DIFF_CLAUSES]); (SIMP_TAC [lem12;GSYM lemma0]) ] ) let ZERO_ITERATE_POLYADD_LEMMA = prove( `!n f .iterate (++) (0 INSERT (1..n)) f = (f 0) ++ iterate (++) (1..n) f`, let lem0 = prove(`!n. ~(0 IN (1..n))`, STRIP_TAC THEN (ONCE_REWRITE_TAC [IN_NUMSEG]) THEN ARITH_TAC) in let lem1 = ISPEC `poly_add` ITERATE_CLAUSES_GEN in let lem2 = SIMP_RULE [MONOIDAL_POLY_ADD] lem1 in let lem3 = CONJUNCT2 lem2 in let lem4 = ISPECL [`f:(num -> (real)list)`;`0`;`1..n`] lem3 in let lem5 = ISPECL [`poly_add`;`f:(num -> (real)list)`;`1..n` ] FINITE_SUPPORT in let lem6 = SIMP_RULE [FINITE_NUMSEG] lem5 in let lem7 = MP lem4 lem6 in let lem9 = SIMP_RULE [lem0] lem7 in (ACCEPT_TAC (GEN_ALL lem9)) ) let SOD_SOD_POLYDIFF = prove( `!f .(SOD f) = f ++ (SOD (poly_diff f))`, (ONCE_REWRITE_TAC [SOD_POLY_DIFF_ITERATE]) THEN (ONCE_REWRITE_TAC [SOD]) THEN (ONCE_REWRITE_TAC [SODN]) THEN (ONCE_REWRITE_TAC [ZERO_INSERT_NUMSEG]) THEN (ONCE_REWRITE_TAC [ZERO_ITERATE_POLYADD_LEMMA]) THEN (BETA_TAC) THEN (SIMP_TAC [PDI_DEF]) ) let SUC_INSERT_NUMSEG = prove( `!n. (0..(SUC n)) = (SUC n) INSERT (0..n)`, let lem01 = SIMP_RULE [ARITH_RULE `0 <= SUC n`] (SPECL [`0`;`n:num`] NUMSEG_REC) in ACCEPT_TAC (GEN_ALL lem01) ) let SUC_NOT_IN_NUMSEG = prove( `!m n. ~((SUC n) IN (m..n))`, STRIP_TAC THEN (ONCE_REWRITE_TAC [IN_NUMSEG]) THEN ARITH_TAC ) let SUC_ITERATE_PDI_POLYDIFF_LEMMA = prove( `iterate (++) ((SUC n) INSERT (0..n)) (\i.poly_diff_iter (poly_diff p) i) = (poly_diff_iter (poly_diff p) (SUC n)) ++ iterate (++) (0..n) (\i.poly_diff_iter (poly_diff p) i)`, let lem1 = ISPEC `poly_add` ITERATE_CLAUSES_GEN in let lem2 = SIMP_RULE [MONOIDAL_POLY_ADD] lem1 in let lem3 = CONJUNCT2 lem2 in let lem4 = ISPECL [`(\i.poly_diff_iter (poly_diff p) i)`;`SUC n`;`0..n`] lem3 in let lem5 = ISPECL [`poly_add`;`\i.poly_diff_iter (poly_diff p) i`;`0..n` ] FINITE_SUPPORT in let lem6 = SIMP_RULE [FINITE_NUMSEG] lem5 in let lem7 = MP lem4 lem6 in let lem9 = SIMP_RULE [SPEC `0` SUC_NOT_IN_NUMSEG] lem7 in ACCEPT_TAC lem9 ) let SODN_POLY_DIFF_COMM = prove( `!n p.(SODN (poly_diff p) n) = poly_diff (SODN p n)`, let lem = MP (ISPEC `poly_add` ITERATE_SING) MONOIDAL_POLY_ADD in let lem1 = ISPEC `poly_add` ITERATE_CLAUSES_GEN in let lem2 = SIMP_RULE [MONOIDAL_POLY_ADD] lem1 in let lem3 = CONJUNCT2 lem2 in let lem10 = SIMP_RULE [GSYM SUC_INSERT_NUMSEG] SUC_ITERATE_PDI_POLYDIFF_LEMMA in let lema00 = ISPECL [`(\i.poly_diff_iter (p) i)`;`SUC n`;`0..n`] lem3 in let lema0 = SIMP_RULE [GSYM SUC_INSERT_NUMSEG] lema00 in let lem15 = ISPECL [`poly_add`;`\i.poly_diff_iter (p) i`;`0..n` ] FINITE_SUPPORT in let lem16 = SIMP_RULE [FINITE_NUMSEG] lem15 in let lema1 = MP lema0 lem16 in let lema2 = SIMP_RULE [SPEC `0` SUC_NOT_IN_NUMSEG] lema1 in let lema3 = ONCE_REWRITE_RULE [GSYM SODN] lema2 in INDUCT_TAC THENL [ (ONCE_REWRITE_TAC [SODN]) THEN (SIMP_TAC [NUMSEG_SING;ITERATE_SING]) THEN (ONCE_REWRITE_TAC [lem]) THEN (BETA_TAC) THEN (SIMP_TAC [PDI_POLY_DIFF_COMM]) ; (ONCE_REWRITE_TAC [SODN]) THEN (ONCE_REWRITE_TAC [lem10]) THEN (ONCE_REWRITE_TAC [GSYM SODN]) THEN (ASM_SIMP_TAC []) THEN (ONCE_REWRITE_TAC [PDI_DEF ]) THEN (ONCE_REWRITE_TAC [PDI_POLY_DIFF_COMM]) THEN (ONCE_REWRITE_TAC [GSYM POLYDIFF_ADD]) THEN STRIP_TAC THEN AP_TERM_TAC THEN (ONCE_REWRITE_TAC [lema3]) THEN (SIMP_TAC [PDI_DEF]) ] ) let SUC_ITERATE_POLYADD_LEMMA = prove( `!n f .iterate (++) ((SUC n) INSERT (0..n)) f = (f (SUC n)) ++ iterate (++) (0..n) f`, let lem1 = ISPEC `poly_add` ITERATE_CLAUSES_GEN in let lem2 = SIMP_RULE [MONOIDAL_POLY_ADD] lem1 in let lem3 = CONJUNCT2 lem2 in let lem4 = ISPECL [`f:(num -> (real)list)`;`SUC n`;`0..n`] lem3 in let lem5 = ISPECL [`poly_add`;`f:(num -> (real)list)`;`0..n` ] FINITE_SUPPORT in let lem6 = SIMP_RULE [FINITE_NUMSEG] lem5 in let lem7 = MP lem4 lem6 in let lem9 = SIMP_RULE [SPEC `0` SUC_NOT_IN_NUMSEG] lem7 in ACCEPT_TAC (GEN_ALL lem9) ) let NUMSEG_LENGTH_POLYDIFF_LEMMA = prove( `!f. (0..(LENGTH f)) = ((LENGTH f) INSERT (0..(LENGTH (poly_diff f))))`, (SIMP_TAC [LENGTH_POLY_DIFF]) THEN (LIST_INDUCT_TAC) THENL [ (SIMP_TAC [LENGTH;PRE]) THEN (SIMP_TAC [NUMSEG_CLAUSES]) THEN (SIMP_TAC [INSERT_DEF;NOT_IN_EMPTY;IN]); (SIMP_TAC [LENGTH;PRE]) THEN (SIMP_TAC [ARITH_RULE `0 <= SUC n`;NUMSEG_REC]) ] ) let POLY_DIFF_LENGTH_LT = prove( `!p. (~(p=[])) ==> (LENGTH (poly_diff p)) < (LENGTH p)`, SIMP_TAC [LENGTH_POLY_DIFF;LENGTH_EQ_NIL; ARITH_RULE `!n.(~(n=0)) ==> (PRE n) < n`] );; let POLY_DIFF_LENGTH_LE_SUC = prove( `! p n . (LENGTH p <= SUC n) ==> (LENGTH (poly_diff p) <= n)`, (REPEAT STRIP_TAC) THEN (ASM_CASES_TAC `p:(real)list =[]`) THENL [ (ASM_SIMP_TAC [poly_diff;LENGTH]) THEN (ARITH_TAC); (ASM_MESON_TAC [POLY_DIFF_LENGTH_LT;LT_SUC_LE;LTE_TRANS]) ] ) let PDI_LENGTH_AUX = prove( `! n p. (LENGTH p <= n) ==> poly_diff_iter p n = []`, INDUCT_TAC THENL [ MESON_TAC [PDI_DEF;LENGTH_EQ_NIL;ARITH_RULE `n <= 0 <=> n = 0`]; ASM_MESON_TAC [PDI_DEF;PDI_POLY_DIFF_COMM;POLY_DIFF_LENGTH_LE_SUC] ] ) let PDI_LENGTH_NIL = prove( `! p . poly_diff_iter p (LENGTH p) = []`, SIMP_TAC [PDI_LENGTH_AUX;LE_REFL] ) let SOD_POLYDIFF_THEOREM = prove( `!f .(SOD (poly_diff f)) = (poly_diff (SOD f))`, let lemmmag = prove( `0 INSERT (0..0) = (0..0)`, (SIMP_TAC [NUMSEG_SING]) THEN (SIMP_TAC [INSERT_DEF;NOT_IN_EMPTY;IN])) in let SUC_LENGTH_CONS = prove( `SUC (LENGTH (t:(real)list)) = (LENGTH (CONS h t))`, (SIMP_TAC [LENGTH])) in (ONCE_REWRITE_TAC [SOD]) THEN (ONCE_REWRITE_TAC [SODN_POLY_DIFF_COMM]) THEN (ONCE_REWRITE_TAC [SODN]) THEN (STRIP_TAC) THEN (CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [NUMSEG_LENGTH_POLYDIFF_LEMMA]))) THEN (SPEC_TAC (`f:(real)list`,`f:(real)list`)) THEN (LIST_INDUCT_TAC) THENL [ (SIMP_TAC [poly_diff]) THEN (SIMP_TAC [LENGTH]) THEN (SIMP_TAC [SUM_SING_NUMSEG ]) THEN (SIMP_TAC [lemmmag]) ; (SIMP_TAC [LENGTH_POLY_DIFF]) THEN (SIMP_TAC [LENGTH;PRE]) THEN (CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [SUC_ITERATE_POLYADD_LEMMA]))) THEN (SIMP_TAC [LENGTH;PRE]) THEN (SIMP_TAC [GSYM SODN]) THEN (ONCE_REWRITE_TAC [GSYM SODN]) THEN (ONCE_REWRITE_TAC [SUC_LENGTH_CONS]) THEN (ONCE_REWRITE_TAC [PDI_LENGTH_NIL]) THEN (SIMP_TAC [POLY_ADD_CLAUSES ]); ] ) let SOD_SOD_DIFF_LEMMA = prove( `!f x.(poly (SOD f) x) - (poly (poly_diff (SOD f)) x) = poly f x`, MESON_TAC [SOD_SOD_POLYDIFF; POLY_ADD ; POLY_SUB;SOD_POLYDIFF_THEOREM; REAL_ARITH `((x:real) + y) -y = x`] ) let PLANETMATH_EQN_1_1_2 = prove( `!f x. ((exp (--x)) * ((poly (poly_diff (SOD f)) x) - (poly (SOD f) x))) = (-- (exp (--x))) * (poly f x)`, let lem17 = prove(`!x y.(x - y) = (-- (y - x))`,REAL_ARITH_TAC) in (REPEAT STRIP_TAC) THEN (ONCE_REWRITE_TAC [lem17]) THEN (ONCE_REWRITE_TAC [SOD_SOD_DIFF_LEMMA]) THEN REAL_ARITH_TAC ) let PLANETMATH_EQN_1_1_3 = prove( `! x f.((Phi f) diffl (-- (exp (--x)) * (poly f x)))(x)`, (ONCE_REWRITE_TAC [GSYM PLANETMATH_EQN_1_1_2]) THEN (ACCEPT_TAC PLANETMATH_EQN_1_1_1) ) let PHI_CONTL = let lem0 = SPECL [`Phi f`;`-- (exp (--x)) * (poly f x)`;`x:real`] DIFF_CONT in GEN_ALL (MP lem0 (SPEC_ALL PLANETMATH_EQN_1_1_3)) let PHI_DIFFERENTIABLE = prove( `!f x.(Phi f) differentiable x`, (SIMP_TAC [differentiable]) THEN (REPEAT STRIP_TAC) THEN (EXISTS_TAC `((exp (--x)) * ((poly (poly_diff (SOD f)) x) - (poly (SOD f) x)))`) THEN (SIMP_TAC [PLANETMATH_EQN_1_1_1]) ) let PLANETMATH_EQN_1_2 = (* this one's a bit nasty *) let FO_LEMMA2 = GEN_ALL (prove( `((! l z. (C (l:real) (z:real)) ==> l = (l' z))) ==> ((? (l:real) (z:real) .(A z) /\ (B z) /\ (C l z) /\ (D l) ) ==> (? (z:real).((A z) /\ (B z) /\ (D (l' z)))))`, let lem0 = prove(`(! (l:real) z.(C l (z:real)) ==> l = (l' z)) ==> ((C l z) = ((C l z) /\ l = (l' z)))`, MESON_TAC[]) in let lem1 = UNDISCH lem0 in (STRIP_TAC THEN (ONCE_REWRITE_TAC [lem1]) THEN (MESON_TAC[])) )) in let PROP_LEMMA = TAUT `! a b c d.((a /\ b /\ c) ==> d) = (b ==> c ==> a ==> d)` in let MVT_SPEC = SPECL [`Phi f`;`&0`;`x:real`] MVT in let MVT_SPEC2 = ONCE_REWRITE_RULE [PROP_LEMMA] MVT_SPEC in let MVT_SPEC3 = UNDISCH MVT_SPEC2 in let MVT_SPEC4 = UNDISCH MVT_SPEC3 in let MVT_SPEC5 = UNDISCH MVT_SPEC4 in let lem0 = prove(`! x. x - &0 = x`,REAL_ARITH_TAC) in let MVT_SPEC6 = ONCE_REWRITE_RULE [lem0] MVT_SPEC5 in let DIFF_UNIQ_SPEC1 = SPEC `Phi f` DIFF_UNIQ in let DIFF_UNIQ_SPEC2 = SPEC `l:real` DIFF_UNIQ_SPEC1 in let DIFF_UNIQ_SPEC3 = SPEC ` (-- (exp (--x)) * (poly f x)) ` DIFF_UNIQ_SPEC2 in let DIFF_UNIQ_SPEC4 = SPEC `x:real` DIFF_UNIQ_SPEC3 in let lem8 = SIMP_RULE [PLANETMATH_EQN_1_1_3] DIFF_UNIQ_SPEC4 in let lem9 = GENL [`l:real`;`x:real`] lem8 in let lem10 = SPECL [`\l x.((Phi f diffl l) x)`;`\z.(&0) ? z. (Q z x f)) = (! (x:real) (f:(real)list). ? (z:real). (P x) ==> (Q z x f))`, MESON_TAC []) in ((CONV_RULE SKOLEM_CONV) (ONCE_REWRITE_RULE [FO_LEM] (GEN_ALL (DISCH_ALL PLANETMATH_EQN_1_2))))) let PLANETMATH_LEMMA_1 = prove( `!x f. &0 < x ==> poly (SOD f) (&0) * exp x = poly (SOD f) x + x * exp (x - xi x f) * poly f (xi x f)`, let lemA = CONJUNCT2 (CONJUNCT2 (UNDISCH (SPEC_ALL xi_DEF))) in let lemB = ONCE_REWRITE_RULE [PHI] lemA in let lemC = ONCE_REWRITE_RULE [REAL_ARITH `((A:real) - B = C) = (B = A - C)`] lemB in let lemD = SIMP_RULE [REAL_NEG_0;REAL_EXP_0;REAL_MUL_LID] lemC in let lem01 = ASSUME `A = ((exp (-- x))*B - (C *( -- (exp (-- y))) * D))` in let lem02 = DISJ2 `exp x = &0` lem01 in let lem03 = REWRITE_RULE [GSYM (SPEC `exp x` REAL_EQ_MUL_LCANCEL)] lem02 in let lem04 = SIMP_RULE [REAL_EXP_NEG_MUL;REAL_EXP_ADD_MUL] lem03 in let lem05 = SIMP_RULE [REAL_SUB_LDISTRIB] lem04 in let lem07 = SIMP_RULE [REAL_MUL_ASSOC;REAL_EXP_NEG_MUL;REAL_MUL_LID] lem05 in let fact00 = REAL_ARITH `(B:real) - ((expx * C) * (--expy)) * D = B + C * (expx * expy) * D` in let lem08 = ONCE_REWRITE_RULE [fact00] lem07 in let lem09 = SIMP_RULE [GSYM REAL_EXP_ADD] lem08 in let lem10 = SIMP_RULE [prove(`(x:real) + -- y = x - y`, REAL_ARITH_TAC)] lem09 in let lem11 = GEN_ALL (DISCH_ALL lem10) in let lem12 = SPECL [`poly (SOD f) (&0)`; `poly (SOD f) x`; `x:real`; `x:real`; `xi x f`; `poly f (xi x f)`] lem11 in let lem13 = MP lem12 lemD in let lem14 = SPECL [`exp x`;`poly (SOD f) (&0)`] REAL_MUL_SYM in ACCEPT_TAC (GEN_ALL (DISCH_ALL (ONCE_REWRITE_RULE [lem14] lem13))) ) end;; module Pm_lemma2 = struct let POLY_MCLAURIN = prove( `! p x. poly p x = psum (0, LENGTH p) (\m.poly (poly_diff_iter p m) (&0) / &(FACT m) * x pow m)`, let lem002 = SPECL [`poly p`;`\n.poly (poly_diff_iter p n)`] MCLAURIN_ALL_LE in let lem003 = SIMP_RULE [Pm_lemma1.PDI_DEF;POLY_DIFF] lem002 in let lem004 = REWRITE_RULE [ETA_CONV `(\x.poly l x)`] POLY_DIFF in let lem005 = MATCH_MP lem003 (GEN `m:num` (SPECL [`poly_diff_iter p m`] lem004)) in let lem007 = SPECL [`x:real`;`LENGTH (p:(real)list)`] lem005 in let lem008 = ONCE_REWRITE_RULE [Pm_lemma1.PDI_LENGTH_NIL] lem007 in let lem009 = ONCE_REWRITE_RULE [poly] lem008 in let lem010 = SIMP_RULE [REAL_ARITH `!x. ((&0)/x) = &0`] lem009 in let lem011 = SIMP_RULE [REAL_MUL_LZERO;REAL_ADD_RID] lem010 in let lem012 = prove(`(? t . (A t) /\ B) ==> B`, MESON_TAC []) in ACCEPT_TAC (GEN_ALL (MATCH_MP lem012 lem011)) ) let DIFF_ADD_CONST_COMMUTE = prove( `!f a l x . (f diffl l) (x + a) ==> ((\x. f (x + a)) diffl l) x`, let lem01 = CONJ (SPEC_ALL DIFF_X) (SPECL [`a:real`;`x:real`] DIFF_CONST) in let lem02 = BETA_RULE (MATCH_MP DIFF_ADD lem01) in let lem03 = ONCE_REWRITE_RULE [REAL_ARITH `&1 + &0 = &1`] lem02 in let lem04 = SPECL [`f:real->real`;`\(x:real).((x + a)):real`;`l:real`;`&1`] DIFF_CHAIN in let MUL_ONE = REAL_ARITH `! x.(&1) * x = x /\ x * (&1) = x` in let lem05 = ONCE_REWRITE_RULE [MUL_ONE] (BETA_RULE lem04) in let lem06 = GEN_ALL (SIMP_RULE [lem03] lem05) in ACCEPT_TAC lem06 ) let POLY_DIFF_ADD_CONST_COMMUTE = prove( `! p1 p2 a.(!x.(poly p2 x) = (poly p1 (x-a))) ==> (!x . ((poly (poly_diff p2) x) = (poly (poly_diff p1) (x-a))))`, let lem01 = SPECL [`\x.poly p1 x`;`-- a:real`;`l:real`;`x:real`] DIFF_ADD_CONST_COMMUTE in let lem02 = ONCE_REWRITE_RULE [REAL_ARITH `w + --v = w - v`] (BETA_RULE lem01) in let lem03 = SPECL [`p1:(real)list`;`(x:real) -a`] POLY_DIFF in let lem04 = MATCH_MP lem02 lem03 in let lem05 = ASSUME `!x.poly p2 x = poly p1 (x - a)` in let lem06 = ONCE_REWRITE_RULE [GSYM lem05] lem04 in let lem07 = SPECL [`p2:(real)list`;`x:real`] POLY_DIFF in let lem08 = MATCH_MP DIFF_UNIQ (CONJ lem07 lem06) in (REPEAT STRIP_TAC) THEN (ACCEPT_TAC lem08) ) let HARD_WON = prove( `! p1 p2 a n.(!x.(poly p2 x) = (poly p1 (x-a))) ==> ((\x.poly (poly_diff_iter p2 n) x) = (\x.(poly (poly_diff_iter p1 n) (x - a)))) `, let lem = SPECL [`poly_diff_iter p1 n`;`poly_diff_iter p2 n`;`a:real`] POLY_DIFF_ADD_CONST_COMMUTE in let tm = `(!x . poly p2 x = poly p1 (x -a )) ==> (\x.poly (poly_diff_iter p2 n) x) = (\x. poly (poly_diff_iter p1 n) (x - a))` in (STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC ) THEN (INDUCT_TAC) THENL [ SIMP_TAC [Pm_lemma1.PDI_DEF] ; STRIP_TAC THEN (ONCE_REWRITE_TAC [Pm_lemma1.PDI_DEF]) THEN (UNDISCH_TAC tm) THEN (ASM_REWRITE_TAC[FUN_EQ_THM]) THEN (ACCEPT_TAC lem) ] ) (* if f:real->real is a function, let us call the function g x = f (x+a), * where a is a constant, a "shifting" of f by a. if f is defined by a poly, * i.e. a (real)list, then (poly_shift f a) is the (real)list defining * the shifting of f by a. *) let POLY_SHIFT_DEF = new_recursive_definition list_RECURSION ` (poly_shift [] a = []) /\ (poly_shift (CONS c t) a = (CONS c (poly_shift t a)) ++ (a ## (poly_shift t a)))` (* POLY_SHIFT simply says that poly_shift does what is supposed to do *) let POLY_SHIFT = prove( `! p a x .(poly p (x + a)) = (poly (poly_shift p a) x)`, let lem01 = ASSUME `! a x . poly t (x + a) = poly (poly_shift t a ) x` in LIST_INDUCT_TAC THENL [ (ONCE_REWRITE_TAC [POLY_SHIFT_DEF;poly]) THEN (SIMP_TAC [poly]); (REPEAT STRIP_TAC) THEN (ONCE_REWRITE_TAC [POLY_SHIFT_DEF]) THEN (ONCE_REWRITE_TAC [POLY_ADD]) THEN (ONCE_REWRITE_TAC [POLY_CMUL]) THEN (ONCE_REWRITE_TAC [poly;GSYM lem01]) THEN (ONCE_REWRITE_TAC [GSYM lem01]) THEN (REAL_ARITH_TAC) ] ) let POLY_SHIFT_LENGTH = prove( `! p a . (LENGTH (poly_shift p a)) = (LENGTH p)`, (LIST_INDUCT_TAC) THENL [ (SIMP_TAC [POLY_SHIFT_DEF]); (SIMP_TAC [POLY_SHIFT_DEF]) THEN (ASM_SIMP_TAC [LENGTH;POLY_CMUL_LENGTH;POLY_ADD_LENGTH; ARITH_RULE `MAX (x:num) y = if (x > y) then x else y`; ARITH_RULE `! n. SUC n >n`]) ] ) let POLY_TAYLOR = prove( `! p x a. poly p x = psum (0,LENGTH p) (\m.poly (poly_diff_iter p m) a/ &(FACT m) * (x - a) pow m)`, let lem01 = SPEC `poly_shift p a` POLY_MCLAURIN in let lem02 = SPECL [`p:(real)list`;`poly_shift p a`;`-- a:real`;`n:num`] HARD_WON in let lem03 = GSYM ( SPECL [`p:(real)list`;`a:real`] POLY_SHIFT) in let lem04 = SIMP_RULE [REAL_ARITH `a - --b = a + b`] lem02 in let lem05 = ONCE_REWRITE_RULE [ETA_AX] (MP lem04 lem03) in let lem06 = BETA_RULE (ONCE_REWRITE_RULE [lem05] lem01) in let lem07 = ONCE_REWRITE_RULE [REAL_ARITH `&0 + a = a`] lem06 in let lem08 = ONCE_REWRITE_RULE [GSYM POLY_SHIFT] lem07 in let lem09 = ONCE_REWRITE_RULE [POLY_SHIFT_LENGTH] lem08 in let lem10 = RATOR_CONV (ONCE_REWRITE_CONV [REAL_ARITH `(x:real) = (x + a) - a`]) `x pow m` in let lem11 = ONCE_REWRITE_RULE [lem10] lem09 in let lem12 = SPEC `(x - a):real` lem11 in let lem13 = ONCE_REWRITE_RULE [REAL_ARITH `(x:real) - a + a = x`] lem12 in ACCEPT_TAC (GEN_ALL lem13 ) ) let PLANETMATH_LEMMA_2_A = prove( `! p a x . poly p x = ((\s .psum (0,LENGTH p) ((\m.poly (poly_diff_iter p m) a/ &(FACT m) * (s m)))) (\m.(x - a) pow m))`, BETA_TAC THEN (MATCH_ACCEPT_TAC POLY_TAYLOR) ) let ITERATE_SUC_REC = prove( `!(op:D -> D -> D) m n (f:num -> D) . monoidal op ==> (m <= SUC n) ==> iterate op (m..(SUC n)) f = op (f (SUC n)) (iterate op (m..n) f)`, let lem0 = UNDISCH_ALL (SPEC_ALL (GSYM NUMSEG_REC)) in let lem1 = ISPEC `op:D -> D -> D` ITERATE_CLAUSES_GEN in let lem2 = CONJUNCT2 (UNDISCH lem1) in let lem3 = ISPECL [`f:(num -> D)`;`SUC n`;`m..n`] lem2 in let lem4 = SIMP_RULE [] (DISCH_ALL lem3) in let lem50 = prove( `!m n. ~((SUC n) IN (m..n))`, STRIP_TAC THEN (ONCE_REWRITE_TAC [IN_NUMSEG]) THEN ARITH_TAC) in let lem5 = SIMP_RULE [lem50;FINITE_SUPPORT;FINITE_NUMSEG] lem4 in let lem6 = ADD_ASSUM `m <= SUC n` lem5 in let lem7 = ONCE_REWRITE_RULE [lem0] lem6 in SIMP_TAC [lem7] );; let ITERATE_POLY_ADD_PRE_REC = prove( `!f n . n > 0 ==> iterate (++) (0..n) f = (f n) ++ (iterate (++) (0..n-1) f)`, MESON_TAC [ITERATE_CLAUSES_NUMSEG; MONOIDAL_POLY_ADD; POLY_ADD_SYM; ARITH_RULE `0 <= x`; ARITH_RULE `n > 0 ==> n = SUC (n - 1)`] );; let PSUM_ITERATE = prove( `! n m f. psum (m,n) f = if (n > 0) then (iterate (+) (m..((n+m)-1)) f) else &0`, let lem01 = ARITH_RULE `~(n+m=0) ==> (SUC n + m) -1 = SUC ((n + m) -1)` in let lem02 = MP (ISPEC `(+)` ITERATE_SING) MONOIDAL_REAL_ADD in let lem03 = prove( `iterate (+) (m..SUC ((n + m) - 1)) f = f (SUC ((n+m)-1)) + iterate (+) (m..(n+m)-1) f`, MESON_TAC [ARITH_RULE `m <= SUC ((n+m)-1)`;ITERATE_CLAUSES_NUMSEG; MONOIDAL_REAL_ADD;REAL_ADD_SYM]) in let lem04 = UNDISCH (UNDISCH (ARITH_RULE `~(n+m=0) ==> n=0 ==> m-1 < m`)) in let lem05 = SIMP_RULE [lem04] (SPECL [`m:num`;`m-1`] NUMSEG_EMPTY) in INDUCT_TAC THENL [ SIMP_TAC [ARITH_RULE `~(0 > 0)`;sum_DEF]; (SIMP_TAC [ARITH_RULE `(SUC n) > 0`]) THEN (REPEAT STRIP_TAC) THEN (ASM_CASES_TAC `n + m =0`) THENL [ (REWRITE_TAC [UNDISCH (ARITH_RULE `n + m = 0 ==> n = 0`)]) THEN (REWRITE_TAC [lem02;NUMSEG_SING;ARITH_RULE `(SUC 0 +m) -1 = m`]) THEN (MESON_TAC [sum_DEF; ADD_CLAUSES;REAL_ARITH `&0 + x = x`]) ; (ONCE_REWRITE_TAC [sum_DEF;UNDISCH lem01]) THEN (REWRITE_TAC [lem03]) THEN (ASM_CASES_TAC `n = 0`) THEN (ASM_SIMP_TAC [ARITH_RULE `~(0 > 0)`;ADD_CLAUSES;REAL_ADD_LID;REAL_ADD_RID; lem05;ITERATE_CLAUSES_GEN; MONOIDAL_REAL_ADD;NEUTRAL_REAL_ADD; REAL_ADD_SYM;ADD_SYM;ARITH_RULE `~(n=0) ==> n>0 /\ SUC (n-1) = n`]) ] ] );; let FACT_DIV_RCANCELS = prove( `!n x. x / &(FACT n) * &(FACT n) = x`, MESON_TAC [REAL_ARITH `!x. &0 < x ==> ~(x = &0)`; REAL_DIV_RMUL;FACT_LT;REAL_OF_NUM_LT] ) let PLANETMATH_LEMMA_2_B = prove( `! p (x:real) a . poly (SOD p) a = ((\s .psum (0,LENGTH p) ((\m.poly (poly_diff_iter p m) a/ &(FACT m) * (s m)))) (\m. &(FACT m)))`, let lem6 = ISPECL [`(\i.poly_diff_iter p i)`;`LENGTH (p:(real)list)`] ITERATE_POLY_ADD_PRE_REC in let lem7 = UNDISCH lem6 in let lem8 = UNDISCH (ARITH_RULE `~(LENGTH (p:(real)list) > 0) ==> (LENGTH p = 0)`) in let lem9 = ONCE_REWRITE_RULE [LENGTH_EQ_NIL] lem8 in BETA_TAC THEN (REPEAT STRIP_TAC) THEN (ONCE_REWRITE_TAC [FACT_DIV_RCANCELS]) THEN (ONCE_REWRITE_TAC [PSUM_ITERATE]) THEN (ASM_CASES_TAC `LENGTH (p:(real)list) > 0`) THENL [ (ASM_SIMP_TAC [Pm_lemma1.SOD;Pm_lemma1.SODN;ITERATE_RADD_POLYADD;ARITH_RULE `x + 0 = x`]) THEN (AP_THM_TAC) THEN (AP_TERM_TAC) THEN (SIMP_TAC [lem7;Pm_lemma1.PDI_LENGTH_NIL;POLY_ADD_CLAUSES]); (ASM_SIMP_TAC []) THEN (SIMP_TAC [lem9;poly;Pm_lemma1.SOD;Pm_lemma1.SODN;NUMSEG_SING;MONOIDAL_POLY_ADD;ITERATE_SING;LENGTH;Pm_lemma1.PDI_DEF]) ] ) end;; module Pm_eqn4 = struct let N_IS_INT = prove( `!n . integer (&n)`, MESON_TAC [is_int] ) let NEG_N_IS_INT = prove( `!n . integer (--(&n))`, MESON_TAC [is_int] );; let PLANETMATH_EQN_3 = prove( `!f. 0 < nu ==> poly (SOD f) (&0) * exp (&nu) = poly (SOD f) (&nu) + &nu * exp (&nu - xi (&nu) f) * poly f (xi (&nu) f)`, let RW = SPECL [`0`;`nu:num`] REAL_OF_NUM_LT in ACCEPT_TAC (ONCE_REWRITE_RULE [RW] (SPEC `(&nu):real` Pm_lemma1.PLANETMATH_LEMMA_1)) ) (* the RHS of PLANETMATH_EQN_4 * TBD: mentioned in paper *) let LHS = new_definition `LHS c f = sum (0..(PRE (LENGTH c))) (\i.(EL i c)*(poly (SOD f) (&i)))` (* the LHS of PLANETMATH_EQN_4 * TBD: mentioned in paper *) let RHS = new_definition `RHS c f = -- sum (1..(PRE (LENGTH c)) ) (\i. (&i) * (EL i c) * (exp ((&i) - (xi (&i) f))) * (poly f (xi (&i) f)) )` let E_POW_N = prove( `!n.(exp (real_of_num 1)) pow n = exp(&n)`, SIMP_TAC [GSYM REAL_EXP_N;REAL_MUL_RID]) (* The proof was originally done with a slightly different transcendental * predicate than found in Harrison's 100/liouville.ml it turns out the difference * is that &0 satisfies my transcendental! Thankfully, it is easy to show that * e != 0, and hence the two notions of transcendence are equivalent for e. * So that I could eliminate even brining my muddled definition of * transcendental into the proof, this file ultimately proves * E_TRANSCENDENTAL_EQUIV, which allows the main proof to only mention * Harrison's transcendental predicate. *) let NO_CONST_TERM_POLY_ROOT = prove( `!p . (~(x = &0) /\ ((HD p) = &0) /\ (poly p x = &0) /\ ~(p = [])) ==> ((poly (TL p) x) = &0)`, LIST_INDUCT_TAC THEN (ASM_SIMP_TAC [HD;TL;NOT_CONS_NIL;poly]) THEN (MESON_TAC [REAL_ARITH `((&0):real) + x = x`;REAL_ENTIRE]) ) let NEGATED_POLY_ROOT = prove( `!p . (poly p x = &0) ==> (poly ((-- &1) ## p) x = &0)`, MESON_TAC [POLY_CMUL;REAL_ARITH `(-- &1) * ((&0):real) = &0`] ) (* changes a polynomial p to p/x^k, where k is the lowest power * of x where p has a non-zero coefficient. This amounts to * just stripping off all leading zeros from the head of the list p. *) let POLY_NUKE = new_recursive_definition list_RECURSION ` (poly_nuk [] = []) /\ (poly_nuk (CONS (c:real) t) = (if (c = &0) then (poly_nuk t) else (CONS c t)))` let POLY_NUKE_ROOT = prove( `!p . ((~(x = &0)) /\ (poly p x = &0)) ==> (poly (poly_nuk p) x = &0)`, LIST_INDUCT_TAC THENL [ SIMP_TAC[POLY_NUKE]; (ASM_CASES_TAC `(h:real) = &0`) THEN (ASM_MESON_TAC [HD;TL;POLY_NUKE;NOT_CONS_NIL;NO_CONST_TERM_POLY_ROOT]) ] ) let POLY_NUKE_ZERO = prove( `!p . (poly p = poly []) <=> (poly (poly_nuk p) = poly [])`, LIST_INDUCT_TAC THEN (ASM_MESON_TAC [POLY_ZERO;ALL;POLY_NUKE]) ) let POLY_CONST_NO_ROOTS = prove( `! c. ~(poly [c] = poly []) ==> ~(poly [c] x = &0)`, (MESON_TAC [poly;REAL_ENTIRE;POLY_ZERO;ALL; REAL_ARITH `(x:real) + &0 = x`; REAL_ARITH `(x:real) * &0 = &0`]) ) let LENGTH_1 = prove( `! lst . (LENGTH lst = 1) <=> (? x. lst = [x])`, LIST_INDUCT_TAC THEN (MESON_TAC [LENGTH;ARITH_RULE `SUC x = 1 <=> x = 0`;NOT_CONS_NIL;LENGTH_EQ_NIL]) ) let SOUP_LEMMA = prove( `!p . ~(x = &0) /\ ~(poly p = poly []) /\ (poly p x = &0) ==> LENGTH (poly_nuk p) > 1`, let l0 = ARITH_RULE `(~(n = 0) /\ ~(n = 1)) <=> n > 1` in let l1 = UNDISCH (UNDISCH (BRW1 (SPEC_ALL POLY_NUKE_ROOT))) in (ONCE_REWRITE_TAC [GSYM l0]) THEN (REPEAT STRIP_TAC) THENL [ (ASM_MESON_TAC [LENGTH;LENGTH_EQ_NIL;POLY_NUKE_ZERO]); (ASM_MESON_TAC [l1;POLY_CONST_NO_ROOTS;LENGTH_1;LENGTH;POLY_NUKE_ZERO]) ] ) let POLY_NUKE_HD_NONZERO = prove( `!p . ~(poly p = poly []) ==> ~((HD (poly_nuk p)) = &0)`, LIST_INDUCT_TAC THEN (ASM_CASES_TAC `(h:real) = &0`) THEN (ASM_SIMP_TAC [HD;POLY_ZERO;ALL;POLY_NUKE]) ) let IS_INT_POLY_NUKE = prove( `!p . (ALL integer p) ==> (ALL integer (poly_nuk p))`, LIST_INDUCT_TAC THEN (ASM_MESON_TAC [ALL;POLY_NUKE;N_IS_INT]) ) let POLY_X_NOT_POLY_NIL = prove( `~(poly [&0;&1] = poly [])`, (SIMP_TAC [FUN_EQ_THM;POLY_X;poly;prove(`(~ ! x .P x) <=> (? x. ~ P x)`,MESON_TAC[])] ) THEN (EXISTS_TAC `real_of_num 1`) THEN (REAL_ARITH_TAC) ) let NOT_TRANSCENDENTAL_ZERO = prove( `~ (transcendental (&0))`, (REWRITE_TAC [transcendental;algebraic]) THEN (EXISTS_TAC `[&0 ; &1]:(real)list`) THEN (MESON_TAC [POLY_X;POLY_X_NOT_POLY_NIL;ALL;N_IS_INT]) ) let ALL_IS_INT_POLY_CMUL = prove( `! p c. (integer c) /\ (ALL integer p) ==> (ALL integer (c ## p))`, (LIST_INDUCT_TAC) THEN (ASM_SIMP_TAC [poly_cmul;ALL;INTEGER_MUL]) ) (* * Harrison's transcendental predicate from 100/liouville.ml is equivalent * to my predicate conjoined with x != 0. *) let TRANSCENDENTAL_MY_TRANSCENDENTAL = prove( `!x. transcendental x <=> (~(x = &0) /\ ~ ? c. (ALL integer c) /\ ((LENGTH c) > 1) /\ ((poly c x) = &0) /\ (HD c) > &0 )`, let contra_pos = TAUT `(~X ==> ~Y /\ ~Z) <=> ((Y \/ Z) ==> X)` in let contra_pos2 = TAUT `((~X /\ ~Y) ==> ~Z) <=> (Z ==> ~X ==> Y)` in let l0 = prove(`!c . LENGTH c > 1 ==> HD c > &0 ==> ~(poly c = poly [])`, LIST_INDUCT_TAC THEN (ASM_MESON_TAC [LENGTH_EQ_NIL;ARITH_RULE `n > 1 ==> ~(n = 0)`; REAL_ARITH `(x:real) > &0 ==> ~(x = &0)`; HD;ALL;POLY_ZERO])) in let witness = `if ((&0) <= (HD (poly_nuk p))) then (poly_nuk p) else ((-- &1) ## (poly_nuk p))` in let l2 = REAL_ARITH `!(x:real). (&0 <= x) /\ ~(x = &0) ==> x > &0` in let l3 = prove( `! c p. LENGTH (c ## p) = LENGTH p`, STRIP_TAC THEN LIST_INDUCT_TAC THEN (ASM_SIMP_TAC [poly_cmul;LENGTH])) in let POLY_CMUL_HD = prove( `! x p . (~(p = [])) ==> HD (x ## p) = x * (HD p)`, STRIP_TAC THEN LIST_INDUCT_TAC THEN (SIMP_TAC [NOT_CONS_NIL;poly_cmul;HD]) ) in (REWRITE_TAC [transcendental;algebraic]) THEN (STRIP_TAC THEN EQ_TAC) THENL [ (ONCE_REWRITE_TAC [contra_pos]) THEN STRIP_TAC THENL [ASM_MESON_TAC [transcendental;algebraic; NOT_TRANSCENDENTAL_ZERO]; (EXISTS_TAC `c:(real)list`) THEN (ASM_MESON_TAC [l0; NOT_TRANSCENDENTAL_ZERO ])]; (REWRITE_TAC [contra_pos2]) THEN (STRIP_TAC THEN STRIP_TAC) THEN (ASM_SIMP_TAC [IS_INT_POLY_NUKE]) THEN (EXISTS_TAC witness) THEN (ASM_CASES_TAC `((&0) <= (HD (poly_nuk p)))`) THEN (ASM_MESON_TAC [ IS_INT_POLY_NUKE;ALL_IS_INT_POLY_CMUL;NEG_N_IS_INT; l2;POLY_NUKE_HD_NONZERO;NEGATED_POLY_ROOT;SOUP_LEMMA; l3;POLY_NUKE_ROOT;POLY_NUKE_ZERO;POLY_CMUL_HD; REAL_ARITH `~(&0 <= (x:real)) <=> ((-- &1) * x) > &0`]) ] ) let E_TRANSCENDENTAL_EQUIV = prove( `(transcendental (exp (&1))) <=> (~ ? c. (ALL integer c) /\ ((LENGTH c) > 1) /\ ((poly c (exp (&1))) = &0) /\ (HD c) > &0 )`, MESON_TAC[TRANSCENDENTAL_MY_TRANSCENDENTAL; REAL_EXP_POS_LT; REAL_ARITH `&0 < (x:real) ==> ~(&0 = x)`] ) (* TBD mentionedin paper *) let PLANETMATH_EQN_4 = prove( `(~ (transcendental (exp (&1)))) ==> ? c . ((ALL integer c) /\ ((LENGTH c) > 1) /\ ((EL 0 c) > &0) /\ (! f .((LHS c f) = (RHS c f))))`, let foo2 = prove( `(HD c) > (real_of_num 0) ==> EL 0 c > &0`,SIMP_TAC [EL]) in let lem01 = SPECL [`f:num->real`;`0`;`0`;`PRE (LENGTH (c:(real)list))`] SUM_COMBINE_R in let lem02 = ARITH_RULE `(0 <= 0 + 1 /\ 0 <= (PRE (LENGTH (c:(real)list))))` in let lem03 = GSYM (MP lem01 (lem02) ) in let lem06 = ISPECL [`f1:num->real`; `f2:num->real`; `1`;`(PRE (LENGTH (c:(real)list)))`] SUM_ADD in let new0 = SPECL [`f:num->real`;`1`;`PRE (LENGTH (c:(real)list))`] PSUM_SUM_NUMSEG in let new1 = SIMP_RULE [ARITH_RULE `~(1 = 0)`;ARITH_RULE `(1 + x) -1 = x`] new0 in let new2 = ONCE_REWRITE_RULE [new1] lem06 in let lem001 = REAL_ARITH `((A:real) * B * C * D + B * E) = (B * (A * C * D + E))` in let lem0 = REAL_ARITH `(x:real) = x * (&1) - (&0) * y` in let lem1 = GEN_ALL (ONCE_REWRITE_RULE [GSYM REAL_EXP_0] lem0) in let lem2 = SPECL [`poly (SOD f) (&0)`; ` exp (&0 - xi (&0) f) * poly f (xi (&0) f)`] lem1 in let PLANETMATH_EQN_3_TWEAKED = REWRITE_RULE [REAL_ARITH `((A:real) = B+C) <=> (B = A -C)`] PLANETMATH_EQN_3 in let lem21 = GEN `nu:num` (SPEC_ALL PLANETMATH_EQN_3_TWEAKED) in let lem3 = CONJ lem21 lem2 in let NUM_CASES_LEMMA = prove( ` !P .((! n .(0 < n) ==> (P n)) /\ (P 0) ==> ! n . P n)`, (REPEAT STRIP_TAC) THEN (SPEC_TAC (`n:num`,`n:num`)) THEN INDUCT_TAC THEN (ASM_SIMP_TAC[]) THEN (ASM_SIMP_TAC [ARITH_RULE `0 < (SUC n)`])) in let lem4 = SPEC `(\nu.poly (SOD f) (&nu) = poly (SOD f) (&0) * exp (&nu) - &nu * (exp ((&nu) - xi (&nu) f)) * poly f (xi (&nu) f))` NUM_CASES_LEMMA in let lem5 = BETA_RULE lem4 in let lem6 = MP lem5 lem3 in let lem100 = SIMP_RULE [ARITH_RULE `!n.0 <= n`;ARITH_RULE `(0:num) + 1 = 1`] (ISPECL [`f:num->real`;`0`;`0`;`PRE (LENGTH (c:(real)list))`] SUM_COMBINE_R) in let lem0001 = ASSUME `LENGTH (c:(real)list) > 1` in let lem0002 = MATCH_MP (ARITH_RULE `(x:num) > 1 ==> ~(x=0)`) lem0001 in let lem0003 = REWRITE_RULE [LENGTH_EQ_NIL] lem0002 in let lem0004 = MATCH_MP POLY_SUM_EQUIV lem0003 in let SUM_LMUL_NUMSEG = GEN_ALL (ISPECL [`f:num->real`;`c:real`;`n..m`] SUM_LMUL) in (ONCE_REWRITE_TAC [E_TRANSCENDENTAL_EQUIV]) THEN (ONCE_REWRITE_TAC [LHS;RHS]) THEN (REPEAT STRIP_TAC) THEN (EXISTS_TAC `c:(real)list`) THEN (ONCE_REWRITE_TAC [GSYM REAL_RNEG_UNIQ]) THEN (ONCE_REWRITE_TAC [lem03]) THEN (ONCE_REWRITE_TAC [NUMSEG_CONV `0..0`]) THEN (ONCE_REWRITE_TAC [SUM_SING] ) THEN (ASM_SIMP_TAC[foo2]) THEN (BETA_TAC) THEN (ONCE_REWRITE_TAC [ARITH_RULE `0 + 1 = 1`] ) THEN (ONCE_REWRITE_TAC [REAL_ARITH `(A:real) + B + C = (A + C) + B`] ) THEN (ONCE_REWRITE_TAC [GSYM new2]) THEN (BETA_TAC) THEN (ONCE_REWRITE_TAC [lem001]) THEN (CONV_TAC ((RAND_CONV o ABS_CONV o RATOR_CONV o RAND_CONV o RATOR_CONV) (PURE_ONCE_REWRITE_CONV [lem6]))) THEN (ONCE_REWRITE_TAC [REAL_ARITH `(A:real) + B - A = B`]) THEN (ONCE_REWRITE_TAC [REAL_ARITH `(EL 0 c) * (poly (SOD f) (&0)) = (EL 0 c) * (poly (SOD f) (&0)) * (&1)`]) THEN (ONCE_REWRITE_TAC [GSYM REAL_EXP_0]) THEN (ONCE_REWRITE_TAC [GSYM (BETA_CONV `(\x.(EL x c) * (poly (SOD f) (&0)) * exp (&x)) (0)`)]) THEN (ONCE_REWRITE_TAC [GSYM (ISPEC `\x.(EL x c) * (poly (SOD f) (&0)) * exp (&x)` SUM_SING)]) THEN (ONCE_REWRITE_TAC [GSYM (NUMSEG_CONV `0..0`)]) THEN (ONCE_REWRITE_TAC [REAL_ADD_AC]) THEN (ONCE_REWRITE_TAC [lem100]) THEN (ONCE_REWRITE_TAC [REAL_ARITH `(A:real) * B * C = B * A * C`]) THEN (ONCE_REWRITE_TAC [ SUM_LMUL_NUMSEG ]) THEN (ONCE_REWRITE_TAC [GSYM E_POW_N]) THEN (ONCE_REWRITE_TAC [GSYM lem0004]) THEN (ASM_SIMP_TAC[]) THEN (REAL_ARITH_TAC) ) end;; module Pm_eqn5 = struct let POLY_MUL_ITER = new_recursive_definition num_RECURSION `(poly_mul_iter f 0 = [&1]) /\ (!n . poly_mul_iter f (SUC n) = (f (SUC n)) ** (poly_mul_iter f n))` let PLANETMATH_EQN_5 = new_definition `g n p = (&1/(&(FACT (p -1)))) ## ((poly_exp [&0;&1] (p-1)) ** (poly_exp (poly_mul_iter (\i.[-- &i; &1]) n) p))` end;; module Pm_eqn4_rhs = struct let ABS_LE_MUL2 = prove( `!(w:real) x y z. abs(w) <= y /\ abs(x) <= z ==> abs(w * x) <= (y * z)`, REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[ABS_POS]) let SEPTEMBER_2009_LEMMA = prove( `!x f n n'. (!i.(0 <= i /\ i <= n) ==> (abs (poly (f i) x)) <= &(n')) ==> (abs (poly (poly_mul_iter f n) x)) <= (&(n') pow n)`, let lem0 = ASSUME `!i. 0 <= i /\ i <= SUC n ==> abs (poly (f i) x) <= &n'` in let lem1 = SPEC `SUC n` lem0 in let lem2 = SIMP_RULE [ARITH_RULE `0 <= SUC n /\ SUC n <= SUC n`] lem1 in let lem3 = prove(`(!i:num.(P0 i) ==> (P1 i)) ==> (!i:num.((P1 i) ==> (Q i))) ==> (!i:num.((P0 i) ==> (Q i)))`, MESON_TAC[]) in let lem4 = ARITH_RULE `!i.(0 <= i /\ i <= n) ==> (0 <= i /\ i <= SUC n)` in let lem5 = GEN `Q:num->bool` (MATCH_MP lem3 lem4) in let lem6 = ASSUME `!n'. (!i. 0 <= i /\ i <= n ==> abs (poly (f i) x) <= &n') ==> abs (poly (poly_mul_iter f n) x) <= &n' pow n` in let lem7 = SPEC `n':num` lem6 in let lem9 = UNDISCH (BETA_RULE (SPEC `\i. abs (poly (f (i:num)) x) <= &n'` lem5)) in let lem11 = MP (lem7) (lem9) in STRIP_TAC THEN STRIP_TAC THEN INDUCT_TAC THENL [ (REWRITE_TAC ([Pm_eqn5.POLY_MUL_ITER;poly;real_pow]@rewrites0)) THEN (REAL_ARITH_TAC); (STRIP_TAC) THEN (STRIP_TAC) THEN (REWRITE_TAC [Pm_eqn5.POLY_MUL_ITER;POLY_MUL;real_pow]) THEN (MATCH_MP_TAC ABS_LE_MUL2) THEN (SIMP_TAC [lem2;lem11]) ] ) let SEPTEMBER_2009_LEMMA_2 = prove( `&0 < x /\ x < &n ==> (!i. 0 <= i /\ i <= n ==> abs(poly [-- &i; &1] x) <= &n)`, (REWRITE_TAC [GSYM REAL_LE]) THEN (REPEAT STRIP_TAC) THEN (REWRITE_TAC ([poly]@rewrites0)) THEN (REWRITE_TAC [REAL_ARITH `&0 <= -- &i + (x:real) <=> &i <= x`;real_abs]) THEN (ASM_CASES_TAC `&i <= (x:real)`) THENL [ (ASM_SIMP_TAC []) THEN (REWRITE_TAC [REAL_ARITH `-- &i + (x:real) = x - &i `]) THEN (ASM_REAL_ARITH_TAC); (ASM_SIMP_TAC []) THEN (REWRITE_TAC [REAL_ARITH `--(-- &i + (x:real)) = &i - x `]) THEN (ASM_REAL_ARITH_TAC) ] ) let FACT_DIV_LCANCELS = prove( `!n x. &(FACT n) * x / &(FACT n) = x`, let lem0 = SPECL [`0`;`FACT n`] REAL_OF_NUM_LT in let lem1 = ONCE_REWRITE_RULE [GSYM lem0] FACT_LT in let lem2 = SPECL [`x:real`;`(&(FACT n)):real`] REAL_DIV_LMUL in let lem3 = REAL_ARITH `!x:real. &0 < x ==> ~(x = &0)` in let lem4 = MATCH_MP lem3 (SPEC_ALL lem1) in ACCEPT_TAC (GEN_ALL (MP lem2 lem4)) ) let NOVEMBER_LEMMA_1 = prove( `p > 1 ==> &0 < x /\ x < &n ==> (abs(poly (g n p) x)) <= (&1/(&(FACT (p -1)))) * ((&n) pow (p - 1)) * ((&n pow n) pow p)`, let l0 = SPECL [`0`;`FACT (p-1)`] REAL_OF_NUM_LT in let l2 = snd (EQ_IMP_RULE l0) in let l3 = MP l2 (SPEC `(p:num) - 1` FACT_LT) in let l4 = SPEC `(&(FACT (p - 1))):real` REAL_LE_LCANCEL_IMP in let l5 = SIMP_RULE [l3] l4 in let ll0 = snd (EQ_IMP_RULE (SPEC_ALL REAL_ABS_REFL)) in let ll1 = IMP_TRANS (REAL_ARITH `(&0):real < x ==> &0 <= x`) ll0 in let ll2 = UNDISCH ll1 in let asses = [`(p:num) > 1`;`&0 < (x:real)`; `(x:real) < &n`] in let j0 = SPECL [`p - 1`;`x:real`;`(&n):real`] REAL_POW_LE2 in let j1 = REAL_ARITH `(&0) < (x:real) /\ x < (&n) ==> (&0 <=x /\ x <= (&n))` in let j2 = UNDISCH_ALL (BRW1 (IMP_TRANS j1 j0)) in let ll4 = SPECL [`(x:real) pow (p - 1)`;`((&n):real) pow (p - 1)`;`(abs (r:real)) pow p`] REAL_LE_MUL2 in let ll5 = (SPECL [`x:real`;`(p:num) - 1`] REAL_POW_LE) in let ll50 = UNDISCH (IMP_TRANS (REAL_ARITH `&0 < x ==> (&0) <= (x:real)`) ll5;) in let ll6 = ADD_ASSUMS asses ll4 in let ll7 = REAL_ARITH `(x:real) < y ==> x <= y` in let ll8 = SIMP_RULE [j2;ll50;ll7;REAL_POW_LE;REAL_ABS_POS] ll6 in let ll9 = ADD_ASSUM `p > 1` (SPEC `p:num` REAL_POW_LE2) in let ll10 = UNDISCH (ARITH_RULE `p > 1 ==> ~(p = 0)`) in let ll11 = SIMP_RULE [ll10] ll9 in let ll12 = SPEC `abs (r:real)` ll11 in let ll13 = SIMP_RULE [REAL_ABS_POS] ll12 in let lem0 = UNDISCH (UNDISCH (BRW1 SEPTEMBER_2009_LEMMA_2)) in let lem1 = MATCH_MP SEPTEMBER_2009_LEMMA lem0 in let lem2 = DISCH_ALL (DISCH `(&0) < (x:real)` lem1) in let lem3 = SPEC `SUC n` (GEN (`n:num`) lem2) in (STRIP_TAC) THEN (STRIP_TAC) THEN (ONCE_REWRITE_TAC [Pm_eqn5.PLANETMATH_EQN_5]) THEN (ONCE_REWRITE_TAC [POLY_CMUL]) THEN (ONCE_REWRITE_TAC [POLY_MUL]) THEN (ONCE_REWRITE_TAC [POLY_EXP]) THEN (ONCE_REWRITE_TAC [poly]) THEN (ONCE_REWRITE_TAC [poly]) THEN (ONCE_REWRITE_TAC [poly]) THEN (REWRITE_TAC rewrites0) THEN (ONCE_REWRITE_TAC [REAL_ABS_MUL]) THEN (ONCE_REWRITE_TAC [REAL_ABS_MUL]) THEN (ONCE_REWRITE_TAC [REAL_ABS_POW]) THEN (ONCE_REWRITE_TAC [REAL_ABS_DIV]) THEN (ONCE_REWRITE_TAC [ABS_N]) THEN (MATCH_MP_TAC l5) THEN (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]) THEN (SIMP_TAC [FACT_DIV_LCANCELS;REAL_ARITH `&1 * (x:real) = x`]) THEN (SIMP_TAC [ll2]) THEN (MATCH_MP_TAC ll8) THEN (MATCH_MP_TAC ll13) THEN (UNDISCH_TAC `&0 < (x:real)`) THEN (UNDISCH_TAC `(x:real) < &n`) THEN (SPEC_TAC (`n:num`,`n:num`)) THEN INDUCT_TAC THENL [(REAL_ARITH_TAC); (ACCEPT_TAC lem3)] ) let NOVEMBER_LEMMA_2 = prove( ` 1 <= v /\ v <= n ==> ((&0) < ( xi (&v) f) /\ (xi (&v) f) < (&n))`, let l0 = SPECL [`(&v):real`;`f:(real)list`] Pm_lemma1.xi_DEF in let l1 = UNDISCH (ONCE_REWRITE_RULE [REAL_OF_NUM_LT] l0) in let [l2;l3;_] = CONJUNCTS l1 in let l4 = GEN_ALL (REAL_ARITH `(&v) <= y ==> z < (&v) ==> (z:real) < y`) in let l6 = SPECL [`v:num`;`z:real`;`(&n):real`] l4 in let l7 = UNDISCH l6 in (ONCE_REWRITE_TAC [ TAUT `(X /\ Y ==> Z) <=> (X ==> Y ==> Z)`;ARITH_RULE `1 <= v <=> 0 < v` ]) THEN (ONCE_REWRITE_TAC [GSYM REAL_OF_NUM_LE;GSYM REAL_OF_NUM_LT]) THEN (STRIP_TAC) THEN (STRIP_TAC) THEN (SIMP_TAC [l2]) THEN (MATCH_MP_TAC l7) THEN (ACCEPT_TAC l3) ) let REAL_LE_MUL3 = prove( `! w0 x0 y0 w1 x1 (y1:real). (&0 <= w0) ==> (&0 <= x0) ==> (&0 <= y0) ==> (w0 <= w1) ==> (x0 <= x1) ==> (y0 <= y1) ==> (w0 * x0 * y0) <= (w1 * x1 * y1)`, let lst = [`w0:real`;`w1:real`;`(x0 * y0):real`;`(x1 * y1):real`] in let c0 = SPECL lst REAL_LE_MUL2 in MESON_TAC [c0;REAL_LE_MUL2;REAL_LE_MUL] ) let MAX_ABS_DEF = new_recursive_definition list_RECURSION ` (max_abs [] = &0) /\ (max_abs (CONS h t) = real_max (real_abs h) (max_abs t))` let MAX_ABS_LE = prove( `! cs i. (0 <= i /\ i < (LENGTH cs) ==> (real_abs (EL i cs)) <= (max_abs cs))`, let l0 = UNDISCH (REAL_ARITH `~((abs h) <= max_abs t) ==> x <= (max_abs t) ==> x <= (abs h)`) in LIST_INDUCT_TAC THENL [ (SIMP_TAC [LENGTH]) THEN ARITH_TAC; INDUCT_TAC THENL [ (SIMP_TAC [HD;EL;MAX_ABS_DEF;REAL_MAX_MAX]); (SIMP_TAC [TL;EL;MAX_ABS_DEF;REAL_MAX_MAX;LENGTH;LT_SUC]) THEN (ASM_CASES_TAC `(real_abs h) <= (max_abs t)`) THEN (ASM_SIMP_TAC [real_max;ARITH_RULE `0 <= y`;l0]) ] ] ) let KEATS_PART_1 = prove( `1 <= i /\ i <= PRE (LENGTH c) ==> ( &i * abs (EL i c) <= &i * max_abs c)`, let keats12 = ARITH_RULE `1 <= i /\ i <= (PRE (LENGTH (c:(real)list))) ==> (0 <= i /\ i < LENGTH c)` in let keats13 = IMP_TRANS keats12 (SPECL [`c:(real)list`;`i:num`] MAX_ABS_LE) in let keats14 = SPECL [`real_of_num i`] REAL_LE_LMUL in let keats15 = ARITH_RULE `(&0) <= (real_of_num i)` in let keats16 = SIMP_RULE [keats15] keats14 in let keats17 = UNDISCH keats13 in let keats18 = MATCH_MP keats16 keats17 in ACCEPT_TAC (DISCH_ALL keats18) ) let KEATS_PART_2 = prove( `(1 <= v /\ v <= PRE (LENGTH (c:(real)list))) ==> abs (exp ((&v) - xi (&v) (g (PRE (LENGTH c)) p))) <= abs (exp (&(PRE (LENGTH (c:(real)list)))))`, let j0 = ASSUME `1 <= v /\ (v:num) <= (PRE (LENGTH (c:(real)list)))` in let j00 = ONCE_REWRITE_RULE [GSYM REAL_OF_NUM_LE] (CONJUNCT2 j0) in let j1 = REAL_ARITH `!n .(real_of_num v <= &n) ==> (&0 > --xi (&v) (g n p)) ==> (&n) > (&v) - (xi (&v) (g n p))` in let j2 = MP (SPEC `PRE (LENGTH (c:(real)list))` j1) j00 in let g_term = `g (PRE (LENGTH (c:(real)list))) p` in let k33 = SPEC `PRE (LENGTH (c:(real)list))` (GEN `n:num` NOVEMBER_LEMMA_2) in let k34 = SPEC g_term (GEN `f:(real)list` k33) in let k35 = DISCH `1 <= v /\ v <= (PRE (LENGTH (c:(real)list)))` (CONJUNCT1 (UNDISCH k34)) in let k36 = UNDISCH (SPEC `PRE (LENGTH (c:(real)list))` (GEN `n:num` k35)) in let k37 = REAL_ARITH `!x. (real_of_num 0) < x ==> (real_of_num 0) > -- x` in let k38 = MATCH_MP k37 k36 in let k40 = MP j2 k38 in let k41 = REAL_ARITH `!x (y:real).x > y ==> y <= x` in let k42 = MATCH_MP k41 k40 in let k42 = ONCE_REWRITE_RULE [GSYM REAL_EXP_MONO_LE] k42 in let k43 = REAL_ARITH `!(x:real) . (&0) <= x ==> abs x = x` in let k44 = GEN `x:real` (MATCH_MP k43 (SPEC `x:real` REAL_EXP_POS_LE)) in let k45 = ONCE_REWRITE_RULE [GSYM k44] k42 in let k46 = DISCH_ALL k45 in let k47 = BRW0 (SIMP_RULE [ARITH_RULE `0 < v <=> 1 <= v`] k46) in ACCEPT_TAC k47 ) let KEATS_PART_3 = UNDISCH (prove( `p > 1 ==> (1 <= i /\ i <= PRE (LENGTH (c:(real)list))) ==> abs (poly (g (PRE (LENGTH c)) p) (xi (&i) (g (PRE (LENGTH c)) p))) <= &1 / &(FACT (p - 1)) * &(PRE (LENGTH c)) pow (p - 1) * &(PRE (LENGTH c)) pow PRE (LENGTH c) pow p`, let k0 = UNDISCH NOVEMBER_LEMMA_2 in let k1 = UNDISCH NOVEMBER_LEMMA_1 in let k2 = GEN `x:real` k1 in let k3 = SPEC `xi (real_of_num i) f` k2 in let k5 = MATCH_MP k3 k0 in let g_term = `g (PRE (LENGTH (c:(real)list))) p` in let k6 = SPEC g_term (GEN `f:(real)list` k5) in let k7 = SPEC `PRE (LENGTH (c:(real)list))` (GEN `n:num` (DISCH `1 <= v /\ v <= n` k6)) in let k8 = DISCH `0 < v` k7 in let k9 = BRW0 (SIMP_RULE [ARITH_RULE `0 < v <=> 1 <= v`] k8) in MATCH_ACCEPT_TAC (DISCH_ALL k9) )) let RHS_4_F5_LE_SUM = prove( `abs (RHS c (g (PRE (LENGTH c)) p)) <= sum (1..PRE (LENGTH c)) (\i. &i * abs (EL i c) * abs (exp (&i - xi (&i) (g (PRE (LENGTH c)) p))) * abs (poly (g (PRE (LENGTH c)) p) (xi (&i) (g (PRE (LENGTH c)) p))))`, let keats4 = REFL `abs (RHS c f)` in let keats5 = (CONV_RULE (RAND_CONV (REWRITE_CONV [Pm_eqn4.RHS]))) keats4 in let keats6 = REWRITE_RULE [REAL_ABS_NEG] keats5 in let keats7 = SPECL [`(\i.(&i) * (EL i c) * (exp (&i - (xi (&i) f))) * (poly f (xi (&i) f)))`;`1`;`PRE (LENGTH (c:(real)list))`] SUM_ABS_NUMSEG in let keats8 = ONCE_REWRITE_RULE [GSYM keats6] keats7 in let keats9 = REWRITE_RULE [REAL_ABS_NUM;REAL_ABS_MUL] keats8 in let g_term = `g (PRE (LENGTH (c:(real)list))) p` in let keats10 = SPEC g_term (GEN `f:(real)list` keats9) in ACCEPT_TAC keats10 ) let RHS_4_BOUND_PRE = prove( `abs (RHS c (g (PRE (LENGTH c)) p)) <= (sum (1..PRE (LENGTH c)) &) * (max_abs c * abs (exp (&(PRE (LENGTH c)))) * &1 / &(FACT (p - 1)) * &(PRE (LENGTH c)) pow (p - 1) * &(PRE (LENGTH c)) pow PRE (LENGTH c) pow p)`, let w0 = `(real_of_num i) * (real_abs (EL i c))` in let w1 = `(real_of_num i) * (max_abs c)` in let x0 = `abs (exp (&v - xi (&v) (g (PRE (LENGTH (c:(real)list))) p)))` in let x1 = `abs (exp (&(PRE (LENGTH (c:(real)list)))))` in let y0 = `abs (poly (g (PRE (LENGTH (c:(real)list))) p) (xi (&i) (g (PRE (LENGTH c)) p)))` in let y1 = ` &1 / &(FACT (p - 1)) * &(PRE (LENGTH (c:(real)list))) pow (p - 1) * &(PRE (LENGTH c)) pow PRE (LENGTH c) pow p` in let rename_free_var oo nn tt = SPEC nn (GEN oo tt) in let v2i tt = rename_free_var `v:num` `i:num` tt in let josh0 = SPECL [w0;x0;y0;w1;x1;y1] REAL_LE_MUL3 in let josh2 = SPECL [`real_of_num i`;`real_abs (EL i c)`] REAL_LE_MUL in let josh3 = SIMP_RULE [REAL_ABS_POS;REAL_ARITH `(real_of_num 0) <= &i`] josh2 in let josh4 = v2i (SIMP_RULE [josh3;REAL_ABS_POS] josh0) in let josh5 = SIMP_RULE [UNDISCH KEATS_PART_1] josh4 in let josh6 = SIMP_RULE [UNDISCH (v2i KEATS_PART_2)] josh5 in let josh7 = SIMP_RULE [UNDISCH KEATS_PART_3] josh6 in let josh8 = DISCH `1 <= i /\ i <= (PRE (LENGTH (c:(real)list)))` josh7 in let f0 = `(\i. &i * abs (EL i c) * abs (exp (&i - xi (&i) (g (PRE (LENGTH c)) p))) * abs (poly (g (PRE (LENGTH c)) p) (xi (&i) (g (PRE (LENGTH c)) p))))` in let f1 = `(\i. (&i * max_abs c) * abs (exp (&(PRE (LENGTH c)))) * &1 / &(FACT (p - 1)) * &(PRE (LENGTH c)) pow (p - 1) * &(PRE (LENGTH c)) pow PRE (LENGTH c) pow p)` in let josh9 = SPECL [f0;f1;`1`;`PRE (LENGTH (c:(real)list))`] SUM_LE_NUMSEG in let josh10 = REWRITE_RULE [GSYM REAL_MUL_ASSOC] (BETA_RULE josh9) in let josh11 = REWRITE_RULE [GSYM REAL_MUL_ASSOC] (GEN `i:num` josh8) in let josh12 = MP josh10 josh11 in let josh13 = CONJ RHS_4_F5_LE_SUM josh12 in let josh14 = MATCH_MP REAL_LE_TRANS josh13 in let josh15 = ONCE_REWRITE_RULE [SUM_RMUL] josh14 in ACCEPT_TAC josh15 ) (* A reviewer of the Journal of Formalized Reasoning paper for this proof * pointed out that the "abs" in "abs (exp (&(PRE (LENGTH c))))" of * RHS_4_BOUND_PRE is redundant. So here that theorem is rewritten to * remove that abs. *) let RHS_4_BOUND = let l1 = MATCH_MP (SPEC `&0:real` REAL_LT_IMP_LE) (SPEC `x:real` REAL_EXP_POS_LT) in let l2 = REWRITE_RULE [GSYM REAL_ABS_REFL] l1 in ONCE_REWRITE_RULE [l2] RHS_4_BOUND_PRE ;; let JESSE_POW_LEMMA = prove( `(p:num) > 1 ==> !x.real_pow x p = x * (real_pow x (p-1))`, let c0 = UNDISCH (ARITH_RULE `(p:num) > 1 ==> p = SUC (p - 1) `) in STRIP_TAC THEN STRIP_TAC THEN (CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [c0]))) THEN (SIMP_TAC [real_pow]) ) let JESSE_REAL_ABS_LE = prove( `!(x:real) y.(abs x) <= y ==> (abs x) <= (abs y)`, let int10 = UNDISCH (REAL_ARITH `(real_abs x) <= y ==> y = real_abs y`) in (REPEAT STRIP_TAC) THEN (ASM_SIMP_TAC [GSYM int10]) ) let OLDGERMAN_LEMMA = prove( ` !C2 C e. &0 < e ==> (?N . !n. n >= N ==> abs (C2 * inv (&(FACT n)) * C pow n - &0) < e)`, let w0 = MATCH_MP SUM_SUMMABLE (SPEC `C:real` REAL_EXP_CONVERGES) in let w1 = MATCH_MP SER_ZERO w0 in let w2 = BETA_RULE w1 in let w3 = SPEC `C2:real` SEQ_CONST in let w4 = CONJ w3 w2 in let w5 = BETA_RULE (MATCH_MP SEQ_MUL w4) in let w6 = ONCE_REWRITE_RULE [REAL_ARITH `(C2:real) * (&0) = &0`] w5 in let w7 = ONCE_REWRITE_RULE [SEQ] w6 in let w8 = GEN_ALL (BETA_RULE w7) in (REPEAT STRIP_TAC) THEN (CHOOSE_TAC (UNDISCH (SPEC_ALL w8))) THEN (EXISTS_TAC `SUC N`) THEN (ASM_SIMP_TAC [ARITH_RULE `n' >= SUC n ==> n' >= n`]) ) let RHS_4_LT_ONE_MESSY = prove( `?p0. !p. p > 1 ==> p> p0 ==> abs (RHS c (g (PRE (LENGTH c)) p)) < &1`, let c1 = ONCE_REWRITE_RULE [ UNDISCH JESSE_POW_LEMMA ] RHS_4_BOUND in let c2 = SPECL [`real_pow (&(PRE (LENGTH (c:(real)list)))) (p-1)`] REAL_MUL_SYM in let c3 = ONCE_REWRITE_RULE [ c2] c1 in let c4 = ONCE_REWRITE_RULE [ GSYM REAL_MUL_ASSOC ] c3 in let c5 = ONCE_REWRITE_RULE [ GSYM REAL_POW_MUL ] c4 in let c6 = ONCE_REWRITE_RULE [REAL_MUL_SYM] (CONJUNCT2 real_pow) in let c7 = ONCE_REWRITE_RULE [GSYM c6] c5 in let c8 = REAL_ARITH `!x. (real_of_num 1)/x = inv x` in let c9 = ONCE_REWRITE_RULE [c8] c7 in let c10 = REAL_ARITH `!x y z.(inv x) * y * z = y * inv x * z` in let c11 = ONCE_REWRITE_RULE [c10] c9 in let t0 = `sum (1..PRE (LENGTH c)) & * max_abs c * (exp (&(PRE (LENGTH c)))) * &(PRE (LENGTH c)) pow PRE (LENGTH c)` in let t1 = `real_of_num (PRE (LENGTH (c:(real)list))) pow SUC (PRE (LENGTH c))` in let int0 = SPECL [t0;t1;`real_of_num 1`] OLDGERMAN_LEMMA in let int1 = SIMP_RULE [REAL_ARITH `(real_of_num 0) < &1`] int0 in let int2 = SIMP_RULE [REAL_ARITH `x - (real_of_num 0) = x`] int1 in let t8 = `!n. n >= N ==> abs ((sum (1..PRE (LENGTH c)) & * max_abs c * (exp (&(PRE (LENGTH c)))) * &(PRE (LENGTH c)) pow PRE (LENGTH c)) * inv (&(FACT n)) * &(PRE (LENGTH c)) pow SUC (PRE (LENGTH c)) pow n) < &1` in let int5 = ASSUME t8 in let int50 = REAL_ARITH `((x:real) * y * z * w) * (a * b) = x * y * z * w * a * b` in let int51 = ONCE_REWRITE_RULE [int50] int5 in let int6 = SPEC `p - 1` int51 in let int7 = ARITH_RULE ` (p > N ==> p - 1 >= N)` in let int8 = UNDISCH (IMP_TRANS int7 int6) in let int9 = ARITH_RULE `(x:real) <= y ==> y < (real_of_num 1) ==> x < (&1)` in let int10 = MATCH_MP JESSE_REAL_ABS_LE c11 in let int11 = MATCH_MP int9 int10 in let int12 = MP int11 int8 in (CHOOSE_TAC int2) THEN (EXISTS_TAC `N:num`) THEN (STRIP_TAC) THEN (STRIP_TAC) THEN (ONCE_REWRITE_TAC [ARITH_RULE `p > 0 ==> ((p:num) > N <=> p - 1 >= N)`]) THEN (DISCH_TAC) THEN (MATCH_ACCEPT_TAC int12) ) let LT_ONE = prove( `!c. ?p0. !p. p> p0 ==> abs (RHS c (g (PRE (LENGTH c)) p)) < &1`, STRIP_TAC THEN (CHOOSE_TAC RHS_4_LT_ONE_MESSY) THEN (EXISTS_TAC `SUC p0`) THEN (ASM_MESON_TAC [ARITH_RULE `p > SUC p0 ==> (p > p0 /\ p > 1)`]) ) end;; module Pm_eqn4_lhs = struct let N_IS_INT = prove( `!n . integer (&n)`, MESON_TAC [is_int] ) let NEG_N_IS_INT = prove( `!n . integer (--(&n))`, MESON_TAC [is_int] ) let INT_OF_REAL_ADD = prove( `!x y.(integer x) /\ (integer y) ==> (int_of_real (x + y)) = (int_of_real x) + (int_of_real y)`, SIMP_TAC[integer;int_add;int_rep;N_IS_INT;NEG_N_IS_INT] ) let INT_OF_REAL_MUL = prove( `!x y.(integer x) /\ (integer y) ==> (int_of_real (x * y)) = (int_of_real x) * (int_of_real y)`, SIMP_TAC[is_int;int_mul;int_rep;N_IS_INT;NEG_N_IS_INT] ) let rec INT_OF_REAL_CONV_helper t = let real_op_2_int_op t = if (t = `real_add`) then `int_add` else if (t = `real_sub`) then `int_sub` else if (t = `real_mul`) then `int_mul` else if (t = `real_pow`) then `int_pow` else if (t = `real_neg`) then `int_neg` else t in if (is_var t) then (mk_comb (`int_of_real`,t),[],[t]) else if ((rator t) = `real_of_num`) then (mk_comb (`int_of_real`, t),[t],[]) else if ((rator t) = `real_neg`) then let rand1 = rand t in let (expr1,lst1,lst2) = INT_OF_REAL_CONV_helper rand1 in let lst = lst1 @ [t] in let expr = mk_comb (`int_neg`, expr1) in (expr,lst,lst2) else if ((rator (rator t)) = `real_pow`) then let rand1 = rand (rator t) in let exponent = rand t in let (expr1,lst1,lst2) = INT_OF_REAL_CONV_helper rand1 in let lst = lst1 @ [t] in let expr = mk_comb (mk_comb (`int_pow`,expr1),exponent) in (expr,lst,lst2) else if ( ((rator (rator t)) = `real_add`) or ((rator (rator t)) = `real_mul`) or ((rator (rator t)) = `real_sub`) ) then let int_op = real_op_2_int_op (rator (rator t)) in let rand1 = rand (rator t) in let rand2 = rand t in let (expr1,lst11,lst12) = INT_OF_REAL_CONV_helper rand1 in let (expr2,lst21,lst22) = INT_OF_REAL_CONV_helper rand2 in let lst1 = lst11 @ lst21 @ [t] in let lst2 = lst12 @ lst22 in let expr = mk_comb (mk_comb (int_op,expr1),expr2) in (expr,lst1,lst2) else (t,[],[t]) (* ------------------------------------------------------------------------- *) (* I wrote an initial version of this, but John Harrison proposed this *) (* version which is faster and also requires less theorems. *) (* ------------------------------------------------------------------------- *) let INT_OF_REAL_CONV = let final_tweak = MATCH_MP(MESON[int_tybij] `real_of_int x = y ==> int_of_real y = x`) in fun t -> let (exp,real_sub_terms,is_int_assumpts) = INT_OF_REAL_CONV_helper t in let is_int_assumpts = List.map (fun x -> mk_comb (`integer`,x)) is_int_assumpts in let fexp = rand(concl(PURE_REWRITE_CONV[GSYM int_of_num] exp)) in let rexp = mk_comb(`real_of_int`,fexp) and ths = map (GEN_REWRITE_RULE I [CONJUNCT2 int_tybij] o ASSUME) is_int_assumpts in let th3 = PURE_REWRITE_CONV(ths @ [int_pow_th; int_add_th; int_mul_th; int_sub_th; int_neg_th; int_of_num_th]) rexp in itlist DISCH is_int_assumpts (final_tweak th3) let ALL_IS_INT = prove( `! h t . (ALL integer (CONS h t)) ==> (integer h) /\ (ALL integer t)`, SIMP_TAC [ALL] ) let ALL_IS_INT_POLY_ADD = prove( `! p1 p2 . (ALL integer p1) /\ (ALL integer p2) ==> (ALL integer (p1 ++ p2))`, let lem01 = UNDISCH (SPECL [`h:real`;`t:(real)list`] ALL_IS_INT) in let [lem02;lem03] = CONJUNCTS lem01 in let lem04 = UNDISCH (SPECL [`h':real`;`t':(real)list`] ALL_IS_INT) in let [lem05;lem06] = CONJUNCTS lem04 in let lem07 = CONJ lem02 lem05 in let lem08 = MATCH_MP INTEGER_ADD lem07 in let lem09 = ASSUME `! p2. ALL integer t /\ ALL integer p2 ==> ALL integer (t ++ p2)` in let lem10 = SPEC `t':(real)list` lem09 in let lem11 = CONJ lem03 lem06 in let lem12 = MP lem10 lem11 in LIST_INDUCT_TAC THENL [ (SIMP_TAC [poly_add]); LIST_INDUCT_TAC THENL [ (SIMP_TAC [poly_add]); (SIMP_TAC [poly_add]) THEN (ONCE_REWRITE_TAC [NOT_CONS_NIL]) THEN (SIMP_TAC []) THEN (SIMP_TAC [HD;TL]) THEN (STRIP_TAC) THEN (SIMP_TAC [ALL]) THEN (CONJ_TAC) THENL [(ACCEPT_TAC lem08); (ACCEPT_TAC lem12)] ] ] ) let ALL_IS_INT_POLY_CMUL = prove( `! p c. (integer c) /\ (ALL integer p) ==> (ALL integer (c ## p))`, (LIST_INDUCT_TAC) THEN (ASM_SIMP_TAC [poly_cmul;ALL;INTEGER_MUL]) ) let ALL_IS_INT_POLY_MUL = prove( `! p1 p2 . (ALL integer p1) /\ (ALL integer p2) ==> (ALL integer (p1 ** p2))`, let lem01 = UNDISCH (SPECL [`h:real`;`t:(real)list`] ALL_IS_INT) in let lem02 = UNDISCH (SPECL [`h':real`;`t':(real)list`] ALL_IS_INT) in let [lem03;lem04] = CONJUNCTS lem01 in let [lem05;lem06] = CONJUNCTS lem02 in let lem07 = MATCH_MP INTEGER_MUL (CONJ lem03 lem05) in let lem08 = MATCH_MP ALL_IS_INT_POLY_CMUL (CONJ lem03 lem06) in let lem09 = ASSUME `! p2. ALL integer t /\ ALL integer p2 ==> ALL integer (t ** p2)` in let lem10 = SPEC `(CONS h' t'):(real)list` lem09 in LIST_INDUCT_TAC THENL [ (LIST_INDUCT_TAC THENL [(SIMP_TAC [ALL;poly_mul]);(SIMP_TAC [poly_mul])]); LIST_INDUCT_TAC THENL [ (SIMP_TAC [poly_mul]) THEN ((ASM_CASES_TAC `(t:(real)list) = []`) THENL [ (ASM_SIMP_TAC [ALL;poly_cmul]) THEN (SIMP_TAC [poly_cmul]); (ASM_SIMP_TAC [ALL;poly_cmul;poly_add]) THEN (SIMP_TAC [SPEC `0` N_IS_INT]) ]); (STRIP_TAC) THEN (ONCE_REWRITE_TAC [poly_mul] ) THEN (ASM_CASES_TAC `(t:(real)list) = []`) THENL [ (ASM_SIMP_TAC [ALL;poly_cmul]) THEN STRIP_TAC THENL [(ACCEPT_TAC lem07) ;(ACCEPT_TAC lem08)]; (ASM_SIMP_TAC []) THEN (MATCH_MP_TAC ALL_IS_INT_POLY_ADD) THEN (CONJ_TAC) THENL [ (MATCH_MP_TAC ALL_IS_INT_POLY_CMUL) THEN (CONJ_TAC) THENL [(ACCEPT_TAC lem03) ; (ASM_SIMP_TAC[])]; (SIMP_TAC [ALL]) THEN (CONJ_TAC) THENL [(ACCEPT_TAC (SPEC `0` N_IS_INT)); (ASM_SIMP_TAC [lem04;lem10])] ] ] ] ] ) let NOT_POLY_MUL_ITER_NIL = prove( `! n . ~((poly_mul_iter (\i.[ -- &i; &1]) n) = [])`, let lem02 = SIMP_RULE [NOT_CONS_NIL] (ISPEC `[ -- &(SUC n); &1]` NOT_POLY_MUL_NIL ) in let lem03 = ISPEC `(poly_mul_iter (\i.[ -- &i; &1]) n)` lem02 in let lem04 = UNDISCH lem03 in INDUCT_TAC THENL [ (SIMP_TAC [Pm_eqn5.POLY_MUL_ITER;NOT_CONS_NIL]); (SIMP_TAC [Pm_eqn5.POLY_MUL_ITER;lem04]) ] ) let ALL_IS_INT_POLY_MUL_ITER = prove( `! n. (ALL integer (poly_mul_iter (\i.[-- &i; &1]) n))`, let FOOBAR_LEMMA = prove( `ALL integer [-- &(SUC n); &1]`, (SIMP_TAC [ALL]) THEN (SIMP_TAC [N_IS_INT;NEG_N_IS_INT])) in INDUCT_TAC THENL [ (ONCE_REWRITE_TAC [Pm_eqn5.POLY_MUL_ITER]) THEN (ONCE_REWRITE_TAC [ALL]) THEN (SIMP_TAC [ALL;N_IS_INT]); (ONCE_REWRITE_TAC [Pm_eqn5.POLY_MUL_ITER]) THEN (BETA_TAC) THEN (MATCH_MP_TAC ALL_IS_INT_POLY_MUL) THEN (CONJ_TAC) THENL [(ACCEPT_TAC (FOOBAR_LEMMA)); (ASM_SIMP_TAC [])] ] ) let ALL_IS_INT_POLY_EXP = prove( `!n p. (ALL integer p) ==> (ALL integer (poly_exp p n))`, let lem01 = ASSUME `! p. ALL integer p ==> ALL integer (poly_exp p n)` in let lem02 = ASSUME ` ALL integer p` in let lem03 = MP (SPEC_ALL lem01) lem02 in let lem04 = CONJ lem02 lem03 in let lem05 = MATCH_MP ALL_IS_INT_POLY_MUL lem04 in INDUCT_TAC THENL [ (ONCE_REWRITE_TAC [poly_exp]) THEN (ONCE_REWRITE_TAC [ALL]) THEN (ONCE_REWRITE_TAC [ALL]) THEN (SIMP_TAC [SPEC `1` N_IS_INT]); (ONCE_REWRITE_TAC [poly_exp]) THEN (REPEAT STRIP_TAC) THEN (ACCEPT_TAC lem05) ] ) let BLAHBLAH = prove( `! p1 p2. (LENGTH p1 <= LENGTH p2) ==> (&0 ## p1 ++ p2) = p2`, LIST_INDUCT_TAC THENL [ (SIMP_TAC [LENGTH;poly_cmul;poly_add]); LIST_INDUCT_TAC THENL [ (SIMP_TAC [LENGTH]) THEN ARITH_TAC; (ASM_SIMP_TAC [poly_cmul;poly_add;NOT_CONS_NIL;HD;TL; REAL_ARITH `&0 * h + h' = h'`;LENGTH; ARITH_RULE `(SUC x) <= (SUC y) <=> x <= y`]) ] ] ) let BLAHBLAH3 = prove( `! n h t. (LENGTH t) <= LENGTH (poly_exp [&0;&1] n ** CONS h t)`, let lem04 = ASSUME `! h t . LENGTH t <= LENGTH (poly_exp [&0;&1] n ** CONS h t)` in let lem05 = SPECL [`h:real`;`t:(real)list`] lem04 in let lem06 = ARITH_RULE `!(x:num) y . x <= y ==> x <= SUC y` in let lem07 = MATCH_MP lem06 lem05 in let lem08 = GEN_ALL lem07 in INDUCT_TAC THENL [ (SIMP_TAC [poly_exp;poly_mul;poly_cmul;POLY_CMUL_LID;LENGTH]) THEN ARITH_TAC; (SIMP_TAC [POLY_EXP_X_REC;poly_mul;NOT_POLY_EXP_X_NIL;poly_cmul;poly_add;NOT_CONS_NIL;LENGTH;TL]) THEN (ASM_SIMP_TAC [BLAHBLAH]) THEN (ACCEPT_TAC lem08) ] ) let TELEVISION = prove ( `!n p.(~ (p = [])) ==> EL n (poly_exp [&0;&1] n ** p) = HD p`, let lem = MATCH_MP BLAHBLAH (SPEC_ALL BLAHBLAH3) in INDUCT_TAC THENL [ (SIMP_TAC [EL;poly_exp;POLY_MUL_CLAUSES]) THEN (LIST_INDUCT_TAC) THENL [ (SIMP_TAC[]); (SIMP_TAC [NOT_CONS_NIL;POLY_CMUL_LID])]; (SIMP_TAC [EL;POLY_EXP_X_REC;poly_mul;NOT_POLY_EXP_X_NIL]) THEN LIST_INDUCT_TAC THENL [ (SIMP_TAC []); (SIMP_TAC [poly_cmul;poly_add;NOT_CONS_NIL;TL;HD]) THEN (ASM_SIMP_TAC [lem;NOT_CONS_NIL;HD]) ] ] ) let JOSHUA = prove( `!i n p.(~ (p = [])) /\ (i < n) ==> EL i (poly_exp [&0;&1] n ** p) = &0`, let lem0000 = SPECL [`t:(real)list`;`poly_exp [&0;&1] n ** (CONS h t)`] BLAHBLAH in let lem0001 = MATCH_MP lem0000 (SPEC_ALL BLAHBLAH3) in let lem0002 = ASSUME `! n p . ~(p = []) /\ i < n ==> EL i (poly_exp [&0;&1] n ** p) = &0` in let lem0003 = SIMP_RULE [NOT_CONS_NIL] (SPECL [`n:num`;`(CONS (h:real) t)`] lem0002) in INDUCT_TAC THENL [ INDUCT_TAC THENL [ ARITH_TAC ; LIST_INDUCT_TAC THENL [ (SIMP_TAC[]); (SIMP_TAC [POLY_EXP_X_REC;EL;HD;poly_mul;NOT_POLY_EXP_NIL;NOT_CONS_NIL;HD_POLY_ADD;poly_cmul]) THEN REAL_ARITH_TAC ] ]; INDUCT_TAC THENL [ ARITH_TAC; (SIMP_TAC [EL;POLY_EXP_X_REC;poly_mul;NOT_POLY_EXP_NIL;NOT_CONS_NIL]) THEN LIST_INDUCT_TAC THENL [ (SIMP_TAC[]); (SIMP_TAC [poly_cmul;poly_add;NOT_CONS_NIL;TL;lem0001]) THEN (SIMP_TAC [ARITH_RULE `(SUC i) < (SUC n) <=> i < n`;lem0003]) ] ] ] ) let POLY_MUL_HD = prove( `! p1 p2. (~(p1 = []) /\ ~(p2 = [])) ==> (HD (p1 ** p2)) = (HD p1) * (HD p2)`, LIST_INDUCT_TAC THENL [ (SIMP_TAC[]); (LIST_INDUCT_TAC) THENL [ (SIMP_TAC[]); (SIMP_TAC [NOT_CONS_NIL]) THEN (ONCE_REWRITE_TAC [poly_mul]) THEN (ASM_CASES_TAC `(t:(real)list) = []`) THENL [ (ASM_SIMP_TAC [HD;poly_cmul]); (ASM_SIMP_TAC [HD;poly_cmul;poly_add]) THEN (SIMP_TAC [NOT_CONS_NIL;HD]) THEN (REAL_ARITH_TAC) ] ] ] ) let POLY_MUL_ITER_HD_FACTORIAL = prove( `! n. (HD (poly_mul_iter (\i.[-- &i; &1]) n)) = ((-- &1) pow n) * (&(FACT n))`, let lem01 = prove(`~([-- &(SUC n); &1] = [])`,SIMP_TAC [NOT_CONS_NIL]) in let lem02 = ISPECL [`[-- &(SUC n); &1]`;`poly_mul_iter (\i.[-- &i; &1]) n`] POLY_MUL_HD in let lem03 = CONJ lem01 (SPEC_ALL NOT_POLY_MUL_ITER_NIL) in let lem04 = MP lem02 lem03 in let lem05 = prove( `!n. ((-- &1) pow n) = -- ((-- &1) pow (SUC n))`, STRIP_TAC THEN (ONCE_REWRITE_TAC [pow]) THEN REAL_ARITH_TAC ) in INDUCT_TAC THENL [ (ONCE_REWRITE_TAC [Pm_eqn5.POLY_MUL_ITER]) THEN (SIMP_TAC [HD;FACT]) THEN REAL_ARITH_TAC; (ONCE_REWRITE_TAC [Pm_eqn5.POLY_MUL_ITER]) THEN BETA_TAC THEN (ONCE_REWRITE_TAC [lem04]) THEN (ONCE_REWRITE_TAC [HD]) THEN (ASM_SIMP_TAC []) THEN (ONCE_REWRITE_TAC [FACT]) THEN (ONCE_REWRITE_TAC [GSYM REAL_OF_NUM_MUL]) THEN (CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [lem05]))) THEN REAL_ARITH_TAC ] ) let PLANETMATH_THM_5_1 = prove( `! n p. p > 0 ==> n > 0 ==> ? As . ((g n p) = (&1/(&(FACT (p - 1)))) ## As) /\ (! i. i< (p-1) ==> (EL i As) = &0) /\ ((EL (p-1) As) = ((-- &1) pow (n * p)) * ((&(FACT n)) pow p)) /\ (ALL integer As)`, let lem01 = SPECL [`poly_exp [&0;&1] (p - 1)`;`poly_exp (poly_mul_iter (\i.[-- &i; &1]) n) p`] ALL_IS_INT_POLY_MUL in let lem02 = SPECL [`p-1`;`[&0;&1]`] ALL_IS_INT_POLY_EXP in let lem03 = prove(`ALL integer [&0;&1]`, (REWRITE_TAC [ALL]) THEN (SIMP_TAC [N_IS_INT])) in let lem04 = MP lem02 lem03 in let lem05 = SPECL [`p:num`;`poly_mul_iter (\i.[-- &i; &1]) n`] ALL_IS_INT_POLY_EXP in let lem06 = MP lem05 (SPEC_ALL ALL_IS_INT_POLY_MUL_ITER) in let lem07 = MP lem01 (CONJ lem04 lem06) in let lem08 = SPECL [`p-1`;`poly_exp (poly_mul_iter (\i.[-- &i; &1]) n) p`] TELEVISION in let lem09 = SIMP_RULE [ NOT_POLY_EXP_NIL;NOT_POLY_MUL_ITER_NIL] lem08 in let lem10 = SPECL [`i:num`;`p - 1`;`poly_exp (poly_mul_iter (\i. [ -- &i; &1]) n ) p`] JOSHUA in let lem11 = SIMP_RULE [NOT_POLY_MUL_ITER_NIL;NOT_POLY_EXP_NIL] lem10 in (REPEAT STRIP_TAC) THEN (EXISTS_TAC `((poly_exp [&0;&1] (p-1)) ** (poly_exp (poly_mul_iter (\i.[-- &i; &1]) n) p))`) THEN CONJ_TAC THENL [ (ONCE_REWRITE_TAC [Pm_eqn5.PLANETMATH_EQN_5]) THEN (SIMP_TAC[]); CONJ_TAC THENL [ (SIMP_TAC [lem11]); CONJ_TAC THENL [ (ONCE_REWRITE_TAC [lem09]) THEN (SPEC_TAC (`n:num`,`n:num`)) THEN (INDUCT_TAC) THENL [ (SIMP_TAC [NOT_CONS_NIL;HD_POLY_EXP;HD;Pm_eqn5.POLY_MUL_ITER;FACT;pow; REAL_POW_ONE;ARITH_RULE `0 * p = 0`;REAL_ARITH `&1 * &1 = &1`]); (SIMP_TAC [HD_POLY_EXP; NOT_POLY_MUL_ITER_NIL; POLY_MUL_ITER_HD_FACTORIAL]) THEN (SIMP_TAC [REAL_POW_MUL;REAL_POW_POW;BLAHBLAH3]) ]; ACCEPT_TAC lem07 ] ] ] ) let as_def = let ll01 = SPEC_ALL PLANETMATH_THM_5_1 in let FO_LEMMA1 = prove(`((p > 0) ==> (n > 0) ==> (? z. C p n z)) <=> (? z. (p > 0) ==> (n > 0) ==> C p n z)`,MESON_TAC[]) in let ll02 = GEN_ALL (SIMP_RULE [FO_LEMMA1] ll01) in let ll03 = ONCE_REWRITE_RULE [SKOLEM_CONV (concl ll02)] ll02 in new_specification ["As"] ll03 (* split up def of As into its four conjuncts *) let g_eq_As = (GEN_ALL o DISCH_ALL o CONJUNCT1 o UNDISCH o UNDISCH o SPEC_ALL) as_def let prefix_As_zero = (GEN_ALL o DISCH_ALL o CONJUNCT1 o CONJUNCT2 o UNDISCH o UNDISCH o SPEC_ALL) as_def let fact_As = (GEN_ALL o DISCH_ALL o CONJUNCT1 o CONJUNCT2 o CONJUNCT2 o UNDISCH o UNDISCH o SPEC_ALL) as_def let ALL_integer_As = (GEN_ALL o DISCH_ALL o CONJUNCT2 o CONJUNCT2 o CONJUNCT2 o UNDISCH o UNDISCH o SPEC_ALL) as_def let POLY_DIFF_AUX_LEM1 = prove( `! i p k. i < (LENGTH p) ==> EL i (poly_diff_aux k p) = (EL i p) * &(i + k)`, let lem0001 = ASSUME `! p k . i < LENGTH p ==> EL i (poly_diff_aux k p ) = EL i p * &(i + k)` in let lem0002 = SPECL [` t:(real)list`;`SUC k`] lem0001 in let lem0003 = prove(`SUC i < LENGTH (CONS (h:real) t) <=> i < LENGTH t`,(SIMP_TAC [LENGTH]) THEN ARITH_TAC) in INDUCT_TAC THENL [ LIST_INDUCT_TAC THENL [ (SIMP_TAC [poly_diff_aux;LENGTH]) THEN ARITH_TAC; (SIMP_TAC [poly_diff_aux;ARITH_RULE `0 + k = k`;poly_diff;LENGTH;EL;HD;TL]) THEN REAL_ARITH_TAC ]; LIST_INDUCT_TAC THENL [ (SIMP_TAC [LENGTH]) THEN ARITH_TAC; (SIMP_TAC [poly_diff_aux;EL;TL]) THEN STRIP_TAC THEN (SIMP_TAC [lem0003;lem0002;ARITH_RULE `i + SUC k = SUC i + k`]) ] ] ) let EL_POLY_DIFF = prove( `! i p. i < (LENGTH (poly_diff p)) ==> EL i (poly_diff p) = (EL (SUC i) p) * &(SUC i)`, let lem01 = SPECL [`SUC i`;`t:(real)list`;`1`] POLY_DIFF_AUX_LEM1 in INDUCT_TAC THENL [ LIST_INDUCT_TAC THENL [ ((SIMP_TAC [LENGTH;poly_diff]) THEN ARITH_TAC); (SIMP_TAC [LENGTH;PRE;EL;HD;TL;ARITH_RULE `SUC 0 = 1`;REAL_ARITH `x * &1 = x`;poly_diff;NOT_CONS_NIL]) THEN (SPEC_TAC (`t:(real)list`,`t:(real)list`)) THEN LIST_INDUCT_TAC THENL [(SIMP_TAC [LENGTH;poly_diff_aux]) THEN ARITH_TAC; (SIMP_TAC [HD;poly_diff_aux;REAL_ARITH `&1 * h = h`])] ]; LIST_INDUCT_TAC THENL [ ((SIMP_TAC [LENGTH;HD;poly_diff;REAL_ARITH `&1 * h = h`])) THEN ARITH_TAC; (SIMP_TAC [poly_diff;NOT_CONS_NIL;TL;LENGTH_POLY_DIFF_AUX ]) THEN (SIMP_TAC [lem01;EL;TL]) THEN ARITH_TAC ] ] ) let POLY_AT_ZERO = prove( `!p .(~(p = [])) ==> poly p (&0) = HD p`, LIST_INDUCT_TAC THENL [ SIMP_TAC []; (SIMP_TAC [poly;HD]) THEN REAL_ARITH_TAC ] ) let PDI_POLY_DIFF_COMM = prove( `! p n.(poly_diff_iter (poly_diff p) n) = (poly_diff (poly_diff_iter p n))`, STRIP_TAC THEN INDUCT_TAC THENL [(SIMP_TAC [Pm_lemma1.PDI_DEF]); (ONCE_REWRITE_TAC [Pm_lemma1.PDI_DEF]) THEN (ASM_SIMP_TAC [])] ) let EL_PDI_AT_ZERO = prove( `!i p. (i < (LENGTH p)) ==> ( poly (poly_diff_iter p i) (&0)) = ((EL i p) * (&(FACT i)))`, let lem03 = prove(`SUC i < LENGTH (CONS (h:real) t) <=> i < LENGTH t`,(SIMP_TAC [LENGTH]) THEN ARITH_TAC) in let lem04 = ASSUME `!p . i < LENGTH p ==> poly (poly_diff_iter p i) (&0) = EL i p * &(FACT i)` in let lem05 = SIMP_RULE [LENGTH_POLY_DIFF;LENGTH;PRE] (SPEC `poly_diff (CONS h t)` lem04) in let lem06 = prove(`i < LENGTH t ==> i < LENGTH (poly_diff (CONS h t))`,SIMP_TAC [LENGTH_POLY_DIFF;PRE;LENGTH]) in INDUCT_TAC THENL [ (LIST_INDUCT_TAC THENL [(SIMP_TAC [LENGTH]) THEN ARITH_TAC; (SIMP_TAC [Pm_lemma1.PDI_DEF;FACT;EL;NOT_CONS_NIL;POLY_AT_ZERO]) THEN REAL_ARITH_TAC]); LIST_INDUCT_TAC THENL [ (SIMP_TAC [LENGTH]) THEN ARITH_TAC; (SIMP_TAC [Pm_lemma1.PDI_DEF;GSYM PDI_POLY_DIFF_COMM;lem03;lem05]) THEN (SIMP_TAC [lem06;EL_POLY_DIFF;FACT;REAL_OF_NUM_MUL;GSYM REAL_MUL_ASSOC]) ] ] ) let EL_PDI_AT_ZERO2 = prove( `!i p. ((~ (p = [])) /\ (i <= (LENGTH p) - 1)) ==> ( poly (poly_diff_iter p i) (&0)) = ((EL i p) * (&(FACT i)))`, STRIP_TAC THEN LIST_INDUCT_TAC THEN (SIMP_TAC [NOT_CONS_NIL;LENGTH;ARITH_RULE `(i <= (SUC x) -1) <=> (i < (SUC x))`;EL_PDI_AT_ZERO]) ) let POLY_CMUL_PDI = prove( `!p c i. (poly_diff_iter (c ## p) i) = c ##(poly_diff_iter p i)`, STRIP_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN (ASM_SIMP_TAC [Pm_lemma1.PDI_DEF;POLY_CMUL_POLY_DIFF]) ) let LENGTH_g = prove( `! n p . (LENGTH (g n p)) >= p `, let lem00 = ARITH_RULE `SUC ((SUC p ) - 1) = SUC p` in let lem01 = prove(`! n p. ~((poly_exp (poly_mul_iter (\i.[-- &i; &1]) n ) (SUC p)) = [])`, SIMP_TAC [NOT_POLY_EXP_NIL; NOT_POLY_MUL_ITER_NIL]) in let lem02 = MATCH_MP POLY_MUL_LENGTH2 (SPEC_ALL lem01) in let lem03 = SPECL [`poly_exp [&0;&1] (SUC p - 1)`] lem02 in let lem04 = SIMP_RULE [POLY_EXP_X_LENGTH] lem03 in let lem05 = SIMP_RULE [lem00] lem04 in (SIMP_TAC [Pm_eqn5.PLANETMATH_EQN_5;POLY_CMUL_LENGTH]) THEN STRIP_TAC THEN INDUCT_TAC THENL [ ARITH_TAC; SIMP_TAC [lem05]] ) let LENGTH_As = prove( `! n p . p > 0 ==> n > 0 ==> LENGTH (As n p) >= p`, let lem50 = ADD_ASSUM `p > 0` (ADD_ASSUM `n > 0` (SPEC_ALL LENGTH_g)) in let lem51 = ONCE_REWRITE_RULE [UNDISCH_ALL (SPEC_ALL g_eq_As)] lem50 in let lem52 = ONCE_REWRITE_RULE [POLY_CMUL_LENGTH] lem51 in SIMP_TAC [lem52] ) let REAL_MUL_RDIV = prove( `!x y. ~(y = &0) ==> ((x * y) / y = x)`, SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_RID] ) let REAL_MUL_DIV_ASSOC = prove( `!x y z.((x * z) / y = x * (z / y))`, SIMP_TAC [real_div;GSYM REAL_MUL_ASSOC] ) let IS_INT_FACT_DIV = prove( `! n m. n >= m ==> integer ( (&(FACT n))/(&(FACT m)) )`, let lem0 = SPEC_ALL (ONCE_REWRITE_RULE [GSYM (SPECL [`FACT n`;`0`] REAL_OF_NUM_EQ)] FACT_NZ) in let lem1 = SPECL [`&(SUC n)`;`&(FACT n)`] REAL_MUL_RDIV in let lem2 = MP lem1 lem0 in let lem4 = ASSUME `! m. n >= m ==> integer (&(FACT n)/ &(FACT m))` in let lem5 = UNDISCH (SPEC_ALL lem4) in let lem6 = prove(`integer(&(SUC n))`,SIMP_TAC [N_IS_INT]) in let lem7 = CONJ lem6 lem5 in let lem8 = MATCH_MP INTEGER_MUL lem7 in let lem9 = UNDISCH_ALL (ARITH_RULE `(~(n >= m)) ==> (SUC n >= m) ==> m = SUC n`) in INDUCT_TAC THENL [ (SIMP_TAC [ARITH_RULE `0 >= m ==> m = 0`;FACT_NZ;REAL_OF_NUM_EQ;REAL_DIV_REFL;N_IS_INT]); (STRIP_TAC) THEN (ASM_CASES_TAC `(n:num) >= m`) THENL [ (ASM_SIMP_TAC [FACT;GSYM REAL_OF_NUM_MUL;lem2;N_IS_INT]) THEN (SIMP_TAC [FACT;GSYM REAL_OF_NUM_MUL;REAL_MUL_DIV_ASSOC;lem8]); (STRIP_TAC) THEN (SIMP_TAC [lem9;FACT_NZ;REAL_OF_NUM_EQ;REAL_DIV_REFL;N_IS_INT]) ] ] ) let SATURDAY_LEMMA = prove( `!x. p > 1 ==> m >= p ==> x * ((&(FACT m))/(&(FACT (p-1)))) = x * (&p) * ((&(FACT m))/(&(FACT p)))`, let lem01 = UNDISCH (ARITH_RULE `p > 1 ==> SUC (p -1) = p`) in let lem02 = ADD_ASSUM `p > 1` (SPEC `p - 1` (CONJUNCT2 FACT)) in let lem03 = GSYM (ONCE_REWRITE_RULE [lem01] lem02) in let lem04 = SPEC `&p` REAL_DIV_REFL in let lem05 = ADD_ASSUM `p > 1` (SPECL [`p:num`;`0`] REAL_OF_NUM_EQ) in let lem06 = SIMP_RULE [UNDISCH (ARITH_RULE `p > 1 ==> ~(p = 0)`)] lem05 in let lem07 = GSYM (MP lem04 lem06) in (REPEAT STRIP_TAC) THEN (CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [GSYM REAL_MUL_LID]))) THEN (ONCE_REWRITE_TAC [lem07]) THEN (ONCE_REWRITE_TAC [real_div]) THEN (ONCE_REWRITE_TAC [REAL_ARITH `((x1:real) * x2) * x * (x3 * x4) = x * x1 * (x3 * (x2 * x4))`]) THEN (ONCE_REWRITE_TAC [GSYM REAL_INV_MUL]) THEN (ONCE_REWRITE_TAC [REAL_OF_NUM_MUL]) THEN (SIMP_TAC [REAL_MUL_ASSOC;GSYM REAL_INV_MUL]) THEN (ONCE_REWRITE_TAC [lem03]) THEN (SIMP_TAC [REAL_MUL_ASSOC;GSYM REAL_OF_NUM_MUL]) ) let SHRIVER = prove( `!f0. (!i. m <= i /\ i <= SUC n ==> (f0 i)) ==> (!i. m <= i /\ i <= n ==> (f0 i)) `, let lem01 = UNDISCH_ALL (ARITH_RULE `i <= n ==> i <= SUC n`) in let lem02 = CONJ (ASSUME `(m:num) <= (i:num)`) lem01 in let lem03 = ASSUME `!i. m <= i /\ i <= SUC n ==> (f0 i)` in let lem04 = SPEC_ALL lem03 in let lem05 = MP lem04 lem02 in (REPEAT STRIP_TAC) THEN (ACCEPT_TAC lem05) ) let IS_INT_SUM = prove( `!f n m.(!i.m <= i /\ i <= n ==> integer (f i)) ==> integer (sum (m..n) f)`, let l0 = SPECL [`m:num`;`n:num`;`i:num`] IN_NUMSEG in let l1 = SPECL [`m:num`;`SUC n`] NUMSEG_EMPTY in let l2 = ADD_ASSUM `SUC n < m` l1 in let l3 = ASM_REWRITE_RULE [] l2 in let l4 = (UNDISCH o ARITH_RULE) `~(SUC n < m) ==> m <= SUC n` in let l5 = ONCE_REWRITE_RULE [GSYM IN_NUMSEG] SHRIVER in let l6 = SPEC `\(i:num).(integer (f i))` l5 in let l7 = BETA_RULE l6 in let l8 = ASSUME `! m. (!i. i IN m..n ==> integer (f i)) ==> integer (sum (m..n) f)` in let l9 = SPEC_ALL l8 in let l10 = UNDISCH (IMP_TRANS l7 l9) in let jj0 = ARITH_RULE `(~(SUC n < m)) ==> m <= SUC n /\ (SUC n) <= SUC n` in let jj1 = UNDISCH (ONCE_REWRITE_RULE [GSYM IN_NUMSEG] jj0) in let jj2 = SPEC `SUC n` (ASSUME `!i. i IN m.. SUC n ==> integer (f i)`) in let jj3 = (MP jj2 jj1) in let l18 = CONJ l10 jj3 in let l19 = MATCH_MP INTEGER_ADD l18 in let l20 = DISCH `!i. i IN m..SUC n ==> integer (f i)` l19 in let l21 = ASSUME `!i . i = 0 ==> integer (f 0)` in let l22 = SIMP_RULE [] (SPEC `0` l21) in (ONCE_REWRITE_TAC [GSYM l0]) THEN STRIP_TAC THEN INDUCT_TAC THENL [ STRIP_TAC THEN (ASM_CASES_TAC `m = 0`) THENL [ (ASM_SIMP_TAC []) THEN (ONCE_REWRITE_TAC [NUMSEG_CONV `0..0`]) THEN (ONCE_REWRITE_TAC [ SUM_SING]) THEN (SIMP_TAC [IN_SING]) THEN (DISCH_TAC) THEN (SIMP_TAC [l22]); (ASM_SIMP_TAC [NUMSEG_CLAUSES;SUM_CLAUSES;N_IS_INT]) ]; STRIP_TAC THEN (ASM_CASES_TAC `SUC n < m`) THENL [ (ASM_SIMP_TAC [l3;SUM_CLAUSES;N_IS_INT]); (ASM_SIMP_TAC [l4;SUM_CLAUSES_NUMSEG]) THEN (ACCEPT_TAC l20) ] ] ) let ALL_IMP_EL = prove( `! (l:(a)list) i P. (ALL P l) ==> (i < LENGTH l) ==> P (EL i l)`, SIMP_TAC[GSYM ALL_EL] ) let KEY_LEMMA = prove( `n > 0 ==> p > 0 ==> ! i . p <= i /\ i <= (LENGTH (As n p) - 1) ==> integer ((&(FACT i)/ &(FACT p)) * (EL i (As n p)))`, let jem0 = ISPECL [`(As n p)`;`i:num`;`integer`] ALL_IMP_EL in let jem1 = MP jem0 (UNDISCH (UNDISCH (SPEC_ALL ALL_integer_As))) in let jem3 = ARITH_RULE `LENGTH (As n p) > 0 ==> ((i < LENGTH (As n p)) <=> i <= LENGTH (As n p) - 1)` in let jem4 = UNDISCH_ALL ((SPEC_ALL LENGTH_As)) in let jem5 = UNDISCH (ARITH_RULE `p > 0 ==> (LENGTH (As n p) >= p) ==> (LENGTH (As n p) > 0)`) in let jem6 = MP jem5 jem4 in let jem7 = MP jem3 jem6 in let jem8 = ONCE_REWRITE_RULE [jem7] jem1 in let kem0 = SPECL [`i:num`;`p:num`] IS_INT_FACT_DIV in let kem1 = ADD_ASSUM `p <= (i:num)` (ADD_ASSUM `i <= (LENGTH (As n p) - 1)` kem0) in let kem2 = SIMP_RULE [UNDISCH_ALL (ARITH_RULE `p <= i ==> i <= LENGTH (As n p) -1 ==> i >= p`)] kem1 in (REPEAT STRIP_TAC) THEN (SIMP_TAC[UNDISCH jem8;kem2;INTEGER_MUL]) ) let KEY_LEMMA2 = prove( `p > 1 ==> n > 0 ==> ? K0 . integer K0 /\ (&1 / &(FACT ( p - 1))) * (sum (p.. LENGTH (As n p) -1) (\m. EL m (As n p) * &(FACT m))) = (&p) * K0`, let lem0000 = SPEC `EL m (As n p)` SATURDAY_LEMMA in let lem1000 = DISCH `m <= LENGTH (As n p) -1` (ADD_ASSUM `m <= LENGTH (As n p) -1` (UNDISCH_ALL lem0000)) in let lem2000 = DISCH `(m:num) >= p` lem1000 in let lem3000 = ONCE_REWRITE_RULE [ARITH_RULE `(m:num) >= p <=> p <= m`] lem2000 in let lem4000 = ONCE_REWRITE_RULE [TAUT `(a ==> b ==> c) <=> ((a /\ b) ==> c)`] (GEN `m:num` lem3000) in let lem5000 = MATCH_MP SUM_EQ_NUMSEG lem4000 in let nem2 = SPECL [`\x.(&(FACT x)/ &(FACT p)) * (EL x (As n p))`;`LENGTH (As n p) - 1`;`p:num`] IS_INT_SUM in let nem3 = BETA_RULE nem2 in let nem4 = SIMP_RULE [UNDISCH (UNDISCH KEY_LEMMA)] nem3 in let nem5 = ADD_ASSUM `p > 1` (DISCH `p > 0` nem4) in let nem6 = SIMP_RULE [(UNDISCH o ARITH_RULE) `(p:num) > 1 ==> p > 0`] nem5 in STRIP_TAC THEN STRIP_TAC THEN (ONCE_REWRITE_TAC [GSYM SUM_LMUL]) THEN (BETA_TAC) THEN (ONCE_REWRITE_TAC [real_div]) THEN (ONCE_REWRITE_TAC [REAL_MUL_LID]) THEN (ONCE_REWRITE_TAC [REAL_ARITH `(x1:real) * x2 * x3 = x2 * (x3 * x1)`]) THEN (ONCE_REWRITE_TAC [GSYM real_div]) THEN (ONCE_REWRITE_TAC [lem5000]) THEN (ONCE_REWRITE_TAC [REAL_ARITH `(x1:real) * x2 * x3 = x2 * (x3 * x1)`]) THEN (ONCE_REWRITE_TAC [SUM_LMUL]) THEN (EXISTS_TAC `sum (p .. LENGTH (As n p) -1) (\x. &(FACT x) / &(FACT p) * EL x (As n p))`) THEN (SIMP_TAC [nem6]) ) let NOT_g_NIL = prove( `!n p . ~ ((g n p ) = [])`, SIMP_TAC [Pm_eqn5.PLANETMATH_EQN_5; NOT_CONS_NIL; NOT_POLY_EXP_NIL; NOT_POLY_CMUL_NIL; NOT_POLY_MUL_NIL;NOT_POLY_MUL_ITER_NIL] ) let FACT_DIV_RCANCELS = prove( `!n x. x / &(FACT n) * &(FACT n) = x`, MESON_TAC [REAL_ARITH `!x. &0 < x ==> ~(x = &0)`; REAL_DIV_RMUL;FACT_LT;REAL_OF_NUM_LT] ) let PSUM_ITERATE = prove( `! n m f. psum (m,n) f = if (n > 0) then (iterate (+) (m..((n+m)-1)) f) else &0`, let lem01 = ARITH_RULE `~(n+m=0) ==> (SUC n + m) -1 = SUC ((n + m) -1)` in let lem02 = MP (ISPEC `(+)` ITERATE_SING) MONOIDAL_REAL_ADD in let lem03 = prove( `iterate (+) (m..SUC ((n + m) - 1)) f = f (SUC ((n+m)-1)) + iterate (+) (m..(n+m)-1) f`, MESON_TAC [ARITH_RULE `m <= SUC ((n+m)-1)`;ITERATE_CLAUSES_NUMSEG; MONOIDAL_REAL_ADD;REAL_ADD_SYM]) in let lem04 = UNDISCH (UNDISCH (ARITH_RULE `~(n+m=0) ==> n=0 ==> m-1 < m`)) in let lem05 = SIMP_RULE [lem04] (SPECL [`m:num`;`m-1`] NUMSEG_EMPTY) in INDUCT_TAC THENL [ SIMP_TAC [ARITH_RULE `~(0 > 0)`;sum_DEF]; (SIMP_TAC [ARITH_RULE `(SUC n) > 0`]) THEN (REPEAT STRIP_TAC) THEN (ASM_CASES_TAC `n + m =0`) THENL [ (REWRITE_TAC [UNDISCH (ARITH_RULE `n + m = 0 ==> n = 0`)]) THEN (REWRITE_TAC [lem02;NUMSEG_SING;ARITH_RULE `(SUC 0 +m) -1 = m`]) THEN (MESON_TAC [sum_DEF; ADD_CLAUSES;REAL_ARITH `&0 + x = x`]) ; (ONCE_REWRITE_TAC [sum_DEF;UNDISCH lem01]) THEN (REWRITE_TAC [lem03]) THEN (ASM_CASES_TAC `n = 0`) THEN (ASM_SIMP_TAC [ARITH_RULE `~(0 > 0)`;ADD_CLAUSES;REAL_ADD_LID;REAL_ADD_RID; lem05;ITERATE_CLAUSES_GEN; MONOIDAL_REAL_ADD;NEUTRAL_REAL_ADD; REAL_ADD_SYM;ADD_SYM;ARITH_RULE `~(n=0) ==> n>0 /\ SUC (n-1) = n`]) ] ] ) let PLANETMATH_EQN_5_2 = prove( `p > 1 ==> n > 0 ==> (? K0. integer K0 /\ poly (SOD (g n p)) (&0) = &(FACT n) pow p * -- &1 pow (n * p) + &p * K0)`, let lem01 = SPECL [`g n p`;`x:real`;`(&0):real`] Pm_lemma2.PLANETMATH_LEMMA_2_B in let lem02 = GEN_ALL lem01 in let lem03 = SPEC_ALL (BETA_RULE lem02) in let lem04 = SIMP_RULE [FACT_DIV_RCANCELS] lem03 in let lem05 = SIMP_RULE [PSUM_ITERATE] lem04 in let lem06 = SIMP_RULE [ARITH_RULE `(n:num) + 0 = n`] lem05 in let lem07 = ADD_ASSUM `n > 0` (ADD_ASSUM `p > 0` lem06) in let lem08 = REWRITE_RULE [GSYM LENGTH_EQ_NIL;ARITH_RULE `~(x = 0) <=> x > 0`] NOT_g_NIL in let lem09 = SIMP_RULE [lem08] lem07 in let lem10 = CONV_RULE (RAND_CONV (REWRITE_CONV [UNDISCH_ALL (SPEC_ALL g_eq_As)])) lem09 in let lem11 = SIMP_RULE [POLY_CMUL_LENGTH] lem10 in let lem12 = SPECL [`m:num`;`(As n p)`] EL_PDI_AT_ZERO in let lem13 = SIMP_RULE [POLY_CMUL_PDI;POLY_CMUL;lem12] lem11 in let lem14 = GSYM (BETA `(\m. poly (poly_diff_iter (As n p) m) (&0)) m`) in let lem15 = ISPECL [`(\m. poly (poly_diff_iter (As n p) m) (&0))`;`&1/ &(FACT (p - 1))`;`0..LENGTH (As n p) -1`] SUM_LMUL in let lem16 = ONCE_REWRITE_RULE [lem14] lem13 in let lem17 = ONCE_REWRITE_RULE [GSYM sum] lem16 in let lem18 = SIMP_RULE [GSYM lem17] lem15 in let lem20 = SPECL [`(\m. poly (poly_diff_iter (As n p) m) (&0))`;`(\m. EL m (As n p) * &(FACT m))`;`0`;`LENGTH (As n p) - 1`] SUM_EQ_NUMSEG in let lem21 = ONCE_REWRITE_RULE [ARITH_RULE `0 <= i`] (BETA_RULE lem20) in let lem22 = ADD_ASSUM `~(As n p = [])` (ONCE_REWRITE_RULE [EL_PDI_AT_ZERO2] lem21) in let lem30 = SPECL [`i:num`;`As n p`] EL_PDI_AT_ZERO2 in let lem31 = ASM_REWRITE_RULE [] (ADD_ASSUM `~(As n p = [])` lem30) in let lem23 = ONCE_REWRITE_RULE [lem31] lem22 in let lem24 = REWRITE_RULE [GSYM lem16] lem23 in let lem25 = ONCE_REWRITE_RULE [lem24] lem18 in let lem30 = ISPECL [`\m. EL m (As n p) * &(FACT m)`;`0`;`p-1`;`(LENGTH (As n p) - 1) - (p - 1)`] SUM_ADD_SPLIT in let lem31 = SIMP_RULE [ARITH_RULE `0 <= x`] lem30 in let lem32 = UNDISCH_ALL (ARITH_RULE `! x. x >= p ==> (p - 1) + (x - 1) - (p -1)= x - 1`) in let lem33 = UNDISCH_ALL (SPEC_ALL LENGTH_As) in let lem34 = SPEC `LENGTH (As n p)` lem32 in let lem35 = MP lem34 lem33 in let lem36 = ONCE_REWRITE_RULE [UNDISCH (ARITH_RULE `p > 1 ==> (p - 1) + 1 = p`);lem35] lem31 in let lem37 = ONCE_REWRITE_RULE [lem36] lem25 in let lem38 = SIMP_RULE [UNDISCH (ARITH_RULE `p > 1 ==> p > 0`)] (DISCH `p > 0` lem37) in let lem39 = ISPECL [`\m. EL m (As n p) * &(FACT m)`;`0`;`p-2`;`1`] SUM_ADD_SPLIT in let lem40 = ADD_ASSUM `n > 0` (ADD_ASSUM `p > 1` lem39) in let lem41 = SIMP_RULE (map (UNDISCH o ARITH_RULE) [`p > 1 ==> p - 2 + 1 = p-1`;`p > 1 ==> (p - 2) + 1 = p - 1`]) lem40 in let lem42 = SIMP_RULE [SUM_SING_NUMSEG;ARITH_RULE `0 <= x`] lem41 in let lem45 = ADD_ASSUM `p > 1` (SPEC_ALL prefix_As_zero) in let lem46 = SIMP_RULE [UNDISCH_ALL (ARITH_RULE `p > 1 ==> p > 0`)] lem45 in let lem47 = UNDISCH (ONCE_REWRITE_RULE [UNDISCH_ALL (ARITH_RULE `p > 1 ==> (i < p-1 <=> i <= p-2)`)] lem46) in let lem48 = SIMP_RULE [REAL_ARITH `((&0):real) + x = x`; SUM_EQ_0_NUMSEG;REAL_ARITH `((&0):real) * x = &0`;lem47] lem42 in let lem49 = SIMP_RULE [UNDISCH (ARITH_RULE `p > 1 ==> p > 0`)] (ADD_ASSUM `p > 1` (SPEC_ALL fact_As)) in let lem50 = SIMP_RULE [UNDISCH lem49] lem48 in let lem51 = ONCE_REWRITE_RULE [lem50] lem38 in let lem52 = SPECL [`p - 1`;`(&1):real`] FACT_DIV_RCANCELS in let lem53 = SIMP_RULE [REAL_ARITH `(x:real) * (y * z) = (x * z) * y`;lem52;REAL_ARITH `(x:real) * (y + z) = (x * y) + (x * z)`] lem51 in let lem54 = SIMP_RULE [REAL_ARITH `&1 * x = (x:real)`] lem53 in let josh0 = UNDISCH_ALL KEY_LEMMA2 in let josh1 = REAL_ARITH `!(y:real) x1 x2 . x1 = x2 <=> y + x1 = y + x2` in let josh2 = SPEC `(&(FACT n) pow p * -- &1 pow (n * p)):real` josh1 in let josh3 = ONCE_REWRITE_RULE [josh2] josh0 in let josh4 = ONCE_REWRITE_RULE [GSYM lem54] josh3 in let josh5 = DISCH `~ (As n p = [])` josh4 in let jem4 = ADD_ASSUM `p > 1` ((SPEC_ALL LENGTH_As)) in (* JOHN: the UNDISCH here is necessary... i don't think it should be *) let jem5 = UNDISCH (SIMP_RULE [UNDISCH (ARITH_RULE `(p:num) > 1 ==> p > 0`)] jem4) in let jem6 = UNDISCH (ARITH_RULE `p > 1 ==> (LENGTH (As n p) >= p) ==> ~((LENGTH (As n p) = 0))`) in let jem7 = MP jem6 jem5 in let jem8 = SIMP_RULE [LENGTH_EQ_NIL] jem7 in let josh6 = MP josh5 jem8 in let josh7 = DISCH_ALL josh6 in let josh11 = ONCE_REWRITE_RULE [GSYM OLD_SUM] lem17 in let josh12 = REWRITE_RULE [GSYM josh11] josh7 in let josh13 = SIMP_RULE [] (DISCH_ALL josh12) in let josh14 = BRW `(X ==> Y ==> Z ==> W) <=> ((X /\ Y /\ Z) ==> W)` josh13 in let josh15 = ONCE_REWRITE_RULE [ARITH_RULE `(p > 0 /\ n > 0 /\ p > 1) <=> (p > 1 /\ n > 0)`] (DISCH_ALL josh14) in let josh16 = BRW1 josh15 in let josh17 = SIMP_RULE [PSUM_ITERATE;ARITH_RULE `~(0 > 0)`] josh16 in ACCEPT_TAC josh17 ) let PLANETMATH_DIVIDES_FACT_PRIME_1 = prove ( `!p n. (prime p) /\ p > n ==> ~(num_divides p (FACT n))`, (SIMP_TAC [DIVIDES_FACT_PRIME]) THEN ARITH_TAC ) let INT_OF_REAL_NEG_NUM = prove( `!(n:num).int_of_real (-- (real_of_num n)) = -- (int_of_real (real_of_num n))`, SIMP_TAC [GSYM int_of_num;GSYM int_of_num_th;GSYM int_neg] ) let ABS_EQ_ONE = prove( `!(x:real) .((abs x) = &1) ==> ((x = &1) \/ (x = -- &1))`, ARITH_TAC ) let POW_NEG_1 = prove( `!(x:num). (((-- (&1 :real)) pow x) = -- &1) \/ (((-- (&1 : real)) pow x) = &1)`, let lem00 = ONCE_REWRITE_RULE [TAUT `x \/ y <=> y \/ x`] ABS_EQ_ONE in let lem01 = (SPEC `(-- (&1 :real)) pow x` lem00) in let lem02 = (SPEC `x:num` POW_M1) in let lem03 = MP lem01 lem02 in STRIP_TAC THEN (ACCEPT_TAC lem03) ) let NUM_DIVIDES_INT_DIVIDES = prove( `!(x:num) (y:num).(x divides y) <=> ((&x):int divides ((&y):int))`, (ONCE_REWRITE_TAC [num_divides]) THEN (SIMP_TAC []) ) let SON_OF_A_GUN = prove( `! (p:num) (n:num) . p > n ==> (prime p) ==> ~(int_divides (& p) (&(FACT n) pow p * -- &1 pow (n * p) ))`, let POW_INT_NEG_1 = INT_OF_REAL_THM POW_NEG_1 in let lem0000 = TAUT `(A /\ B ==> C) <=> (A ==> B ==> C)` in let lem0001 = ONCE_REWRITE_RULE [lem0000] PLANETMATH_DIVIDES_FACT_PRIME_1 in let lem0002 = UNDISCH_ALL (SPEC_ALL lem0001) in let lem0008 = ONCE_REWRITE_RULE [TAUT `(x /\ y ==> z) <=> (x ==> ~z ==> ~y)`] PRIME_DIVEXP in let lem0009 = SPECL [`p:num`;`p:num`;`FACT n`] lem0008 in let lem0010 = UNDISCH lem0009 in let lem0011 = MP lem0010 lem0002 in STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN (DISJ_CASES_TAC (SPEC `(n * p):num` POW_INT_NEG_1)) THENL [ (ASM_SIMP_TAC [INT_OF_NUM_POW; ARITH_RULE `x * (--(&1):int) = -- x`;ARITH_RULE `x * ((&1):int) = x`]) THEN (ONCE_REWRITE_TAC [GSYM INT_DIVIDES_RNEG]) THEN (ONCE_REWRITE_TAC [ARITH_RULE `-- -- (x:int) = x`]) THEN (ONCE_REWRITE_TAC [GSYM NUM_DIVIDES_INT_DIVIDES]) THEN (ACCEPT_TAC lem0011); (ASM_SIMP_TAC [INT_OF_NUM_POW; ARITH_RULE `x * (--(&1):int) = -- x`;ARITH_RULE `x * ((&1):int) = x`]) THEN (ONCE_REWRITE_TAC [GSYM NUM_DIVIDES_INT_DIVIDES]) THEN (ACCEPT_TAC lem0011) ] ) let MAY_LEMMA = prove( `(p:num) > (n:num) ==> (prime p) ==> ~(int_divides (& p) ((int_of_num (FACT n)) pow p * -- &1 pow (n * p) + &p * K0))`, let lem00 = BRW `(x /\ y ==> z) <=> (x ==> ~z ==> ~y)` INT_DIVIDES_ADD_REVR in let lem0 = prove(`int_divides ((&p):int) (&p * K0)`,INTEGER_TAC) in let lem1 = (UNDISCH_ALL o SPEC_ALL) SON_OF_A_GUN in let lem2 = SPECL [`(&p):int`;`((&p):int) * K0`; `(&(FACT n) pow p):int * -- &1 pow (n * p)` ] lem00 in let lem3 = MP (MP lem2 lem0) lem1 in let lem4 = (DISCH_ALL lem3) in let lem5 = ONCE_REWRITE_RULE [ARITH_RULE `(x:int) + y = y + x`] lem4 in (ACCEPT_TAC lem5) ) let PLANET_MATH_alpha_1 = prove( `n > 0 ==> p > n ==> prime p ==> (integer (poly (SOD (g n p )) (&0)))`, let a1 = UNDISCH (UNDISCH (ARITH_RULE `n > 0 ==> p > n ==> p > 1`)) in let a2 = UNDISCH (SIMP_RULE [] (DISCH `n > 0` (MP PLANETMATH_EQN_5_2 a1))) in let t1 = `integer K0 /\ poly (SOD (g n p)) (&0) = &(FACT n) pow p * -- &1 pow (n * p) + &p * K0` in (STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC) THEN (CHOOSE_TAC a2) THEN (SPLIT_CONJOINED_ASSUMPT_TAC t1) THEN (ASM_REWRITE_TAC[]) THEN (ASM_SIMP_TAC [N_IS_INT;INTEGER_ADD;NEG_N_IS_INT;INTEGER_POW;INTEGER_MUL]) ) let PLANET_MATH_alpha_2 = prove( `n > 0 ==> p > n ==> prime p ==> ( ~((&p) divides (int_of_real (poly (SOD (g n p )) (&0)))))`, let t1 = `integer K0 /\ poly (SOD (g n p)) (&0) = &(FACT n) pow p * -- &1 pow (n * p) + &p * K0` in let t = `((real_of_num (FACT n)) pow p) * (-- &1 pow (n * p)) + (&p * K0)` in let arch0 = INT_OF_REAL_CONV t in let a1 = UNDISCH (UNDISCH (ARITH_RULE `n > 0 ==> p > n ==> p > 1`)) in let a2 = UNDISCH (SIMP_RULE [] (DISCH `n > 0` (MP PLANETMATH_EQN_5_2 a1))) in let a3 = SPEC `int_of_real K0` (GEN `K0:int` MAY_LEMMA) in let a4 = GSYM (UNDISCH arch0) in let a5 = ONCE_REWRITE_RULE [a4] a3 in STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN (CHOOSE_TAC a2) THEN (SPLIT_CONJOINED_ASSUMPT_TAC t1) THEN (ASM_SIMP_TAC [a5]) ) let INT_OF_REAL_NEG_INT_OF_NUM = prove( `!n. int_of_real(-- (real_of_num n)) = -- int_of_num n`, SIMP_TAC [int_of_num;INT_OF_REAL_NEG_NUM] ) let PLANET_MATH_alpha_3 = prove( `n > 0 ==> p > n ==> prime p ==> (~((poly (SOD (g n p)) (&0)) = &0))`, let lem0 = prove( `!(x:num) (y:real). (x > 0) ==> (integer y) ==> (~(&x divides (int_of_real y))) ==> ~(y = &0)`, MESON_TAC [is_int;INT_OF_NUM_GT;INT_DIVIDES_RNEG;REAL_OF_NUM_EQ;int_of_num;INT_OF_REAL_NEG_INT_OF_NUM;INT_OF_NUM_EQ;INT_DIVIDES_0]) in let lem1 = ARITH_RULE `n > 0 ==> p > n ==> p > 0` in MESON_TAC [lem0;lem1; PLANET_MATH_alpha_1; PLANET_MATH_alpha_2] ) let PLANET_MATH_alpha = prove( `n > 0 ==> p > n ==> prime p ==> ( (integer (poly (SOD (g n p )) (&0))) /\ ~((&p) divides (int_of_real (poly (SOD (g n p )) (&0)))) /\ ~((poly (SOD (g n p)) (&0)) = &0))`, SIMP_TAC [PLANET_MATH_alpha_1; PLANET_MATH_alpha_2; PLANET_MATH_alpha_3] ) let REAL_FACT_NZ = prove( `~((&(FACT n)) = (real_of_num 0))`, let l0 = GSYM (SPECL [`FACT n`;`0`] REAL_OF_NUM_EQ) in ACCEPT_TAC (SPEC_ALL (ONCE_REWRITE_RULE [l0] FACT_NZ)) ) let IS_INT_FACT_DIV_FACT_DIV_FACT = prove( `! i k.integer ((&(FACT (i+k)))/(&(FACT i))/(&(FACT k)))`, let l0 = MATCH_MP (ARITH_RULE `(~(x=0)) ==> 0 < x`) (SPEC `k:num` FACT_NZ) in let l1 = ONCE_REWRITE_RULE [GSYM REAL_OF_NUM_LT] l0 in let l2 = MATCH_MP REAL_EQ_LDIV_EQ l1 in (REPEAT STRIP_TAC) THEN (REWRITE_TAC [is_int;l2]) THEN (EXISTS_TAC ` (binom(i+k,k))`) THEN DISJ1_TAC THEN (MESON_TAC [BINOM_FACT;MULT_SYM;MULT_ASSOC;REAL_OF_NUM_MUL;REAL_OF_NUM_EQ]) ) (* if you replace the second SIMP_TAC with MESON_TAC, it fails!! * (i alwasy thought MESON_TAC was strictly stronger than SIMP_TAC *) let POLY_CMUL_EL = prove( `!p c i.(i < (LENGTH p)) ==> (EL i (c ## p)) = c * (EL i p)`, let l0 = ARITH_RULE `(SUC i) < (SUC j) <=> i < j` in LIST_INDUCT_TAC THENL [ (SIMP_TAC [LENGTH;ARITH_RULE `~(n < (0:num))`]); STRIP_TAC THEN INDUCT_TAC THENL [ (SIMP_TAC [poly_cmul;HD;EL]); (ASM_SIMP_TAC [LENGTH;poly_cmul;TL;EL;l0]) ] ] ) let PDI_COEFF_FACT = prove( `! k q i.(i < LENGTH (poly_diff_iter q k)) ==> (EL i (poly_diff_iter q k)) = ((&(FACT (i+k)))/(&(FACT i))) * (EL (i+k) q)`, let t0 = `!q i. i < LENGTH (poly_diff_iter q k) ==> EL i (poly_diff_iter q k) = &(FACT (i + k)) / &(FACT i) * EL (i + k) q` in let l0 = SPECL [`q:(real)list`;`SUC i`] ( ASSUME t0) in let l1 = ONCE_REWRITE_RULE [ARITH_RULE `(SUC i) < x <=> i < (PRE x)`] l0 in let l2 = ONCE_REWRITE_RULE [GSYM LENGTH_POLY_DIFF] l1 in let l3 = ONCE_REWRITE_RULE [FACT;GSYM REAL_OF_NUM_MUL] l2 in let l4 = ONCE_REWRITE_RULE [GSYM REAL_OF_NUM_MUL] l3 in let l5 = REWRITE_RULE [real_div;REAL_INV_MUL] l4 in let l6 = REAL_ARITH `(w * (inv x) * y ) * z = (w * y * z) * (inv x)` in let l9 = ONCE_REWRITE_RULE [GSYM REAL_OF_NUM_LT] (ARITH_RULE `0 < SUC i`) in let l10 = MATCH_MP REAL_EQ_RDIV_EQ l9 in let l11 = ONCE_REWRITE_RULE [l6] l5 in let l12 = ONCE_REWRITE_RULE [real_div] l10 in let l13 = ONCE_REWRITE_RULE [l12] l11 in INDUCT_TAC THENL [ (REWRITE_TAC [Pm_lemma1.PDI_DEF;ARITH_RULE `i + 0 = i`]) THEN (MESON_TAC [REAL_DIV_REFL;FACT_NZ;REAL_OF_NUM_EQ;REAL_ARITH `(real_of_num 1) * x = x`]); (ONCE_REWRITE_TAC [Pm_lemma1.PDI_DEF]) THEN (SIMP_TAC [EL_POLY_DIFF]) THEN (ONCE_REWRITE_TAC [ARITH_RULE `i + (SUC k) = (SUC i) + k`]) THEN (ONCE_REWRITE_TAC [FACT]) THEN (ONCE_REWRITE_TAC [real_div]) THEN (SIMP_TAC [l13;real_div;REAL_MUL_ASSOC]) ] ) (* I think this should hold if we replace [--a;&1] with an arbitrary polynomial q, * however the existing ORDER* theorems would not be sufficient to prove it and * I don't feel like putting in the effort right now *) let POLY_DIVIDES_POLY_DIFF = prove( `!p n a. (poly_divides (poly_exp [--a;&1] (SUC n)) p) ==> (poly_divides (poly_exp [--a;&1] n) (poly_diff p))`, let l0 = ARITH_RULE `op = SUC odp ==> SUC n <= op ==> n <= odp` in let l1 = ARITH_RULE `(SUC n <= m ) ==> ~(m = 0)` in MESON_TAC [l0;l1;POLY_DIFF_ZERO;ORDER_DIVIDES;ORDER_DIFF] ) let POLY_DIVIDES_MUL = prove( `!p1 p2 p3.poly_divides p1 p2 ==> poly_divides p1 (p2 ** p3)`, (ONCE_REWRITE_TAC [divides]) THEN (REPEAT STRIP_TAC) THEN (EXISTS_TAC `q ** p3`) THEN (ASM_MESON_TAC [FUN_EQ_THM;POLY_MUL;POLY_MUL_ASSOC]) ) let POLY_DIVIDES_MUL3 = prove( `!p1 p2 p3.(poly_divides p1 p2) ==> (poly_divides p1 (p3 ** p2))`, (ONCE_REWRITE_TAC [divides]) THEN (REPEAT STRIP_TAC) THEN (EXISTS_TAC `p3 ** q`) THEN (UNDISCH_TAC `poly (p2) = poly (p1 ** q)`) THEN (ONCE_REWRITE_TAC [FUN_EQ_THM]) THEN (REWRITE_TAC [POLY_MUL]) THEN (MESON_TAC [REAL_MUL_ASSOC;REAL_MUL_SYM]) ) let POLY_DIVIDES_POLY_MUL_ITER = prove( `!f n v. 1 <= v ==> v <= n ==> poly_divides (f v) (poly_mul_iter f n)`, let l1 = ARITH_RULE `~(v <= n) ==> (v <= SUC n) ==> v = SUC n` in let l2 = UNDISCH (UNDISCH l1) in STRIP_TAC THEN INDUCT_TAC THENL [ ARITH_TAC; (ONCE_REWRITE_TAC [Pm_eqn5.POLY_MUL_ITER]) THEN STRIP_TAC THEN (ASM_CASES_TAC `v <= (n:num)`) THENL [ ASM_MESON_TAC [POLY_DIVIDES_MUL3]; STRIP_TAC THEN STRIP_TAC THEN (MESON_TAC [l2;POLY_DIVIDES_MUL;POLY_DIVIDES_REFL]) ] ] ) (* * This one was suprisingly tricky to prove... *) let POLY_DIVIDES_POLY_EXP2 = prove( `!n p1 p2.(poly_divides p1 p2) ==> poly_divides (poly_exp p1 n) (poly_exp p2 n)`, let t0 = `!p1 p2. (?q. poly p2 = poly (p1 ** q)) ==> (?q. poly (poly_exp p2 n) = poly (poly_exp p1 n ** q))` in let l0 = ASSUME t0 in let l1 = UNDISCH (REWRITE_RULE [divides] (SPEC_ALL l0)) in let l3 = prove( `(x2 = x5 * x6 /\ x1 = x4 * x7) ==> (x1:real) * x2 = (x4 * x5) * x6 * x7`, MESON_TAC [REAL_MUL_SYM;REAL_MUL_ASSOC]) in (ONCE_REWRITE_TAC [divides]) THEN INDUCT_TAC THENL [ (MESON_TAC [divides;poly_exp;POLY_DIVIDES_REFL]); (STRIP_TAC THEN STRIP_TAC THEN DISCH_TAC) THEN (CHOOSE_TAC l1) THEN (UNDISCH_TAC `?q. poly p2 = poly (p1 ** q)`) THEN STRIP_TAC THEN (ONCE_REWRITE_TAC [poly_exp]) THEN (EXISTS_TAC `q ** q'`) THEN (REWRITE_TAC [poly_exp;FUN_EQ_THM;POLY_MUL]) THEN (ASM_MESON_TAC [l3;FUN_EQ_THM;POLY_MUL]) ] ) let POLY_EXP_ONE = prove( `!p .p = poly_exp p 1`, MESON_TAC [poly_exp;ARITH_RULE `1 = SUC 0`;POLY_MUL_RID] ) let POLY_DIVIDES_ROOT = prove( `!p a.poly_divides [--a;&1] p ==> (poly p a) = &0`, MESON_TAC [ORDER_ROOT;ORDER_DIVIDES;POLY_EXP_ONE; ARITH_RULE `1 <= ord ==> ~(ord = 0)`] ) let POLY_DIVIDES_PDI = prove( `!n p a. (poly_divides (poly_exp [--a;&1] (SUC n)) p) ==> (poly_divides [--a;&1] (poly_diff_iter p n))`, let t0 = `!p a. poly_divides (poly_exp [--a; &1] (SUC n)) p ==> poly_divides [--a; &1] (poly_diff_iter p n)` in let l0 = ASSUME t0 in let l1 = SPEC `poly_diff p` l0 in let l2 = SPECL [`p:(real)list`;`SUC n`;`a:real`] POLY_DIVIDES_POLY_DIFF in let l3 = UNDISCH l2 in let l4 = MATCH_MP l1 l3 in INDUCT_TAC THENL [ (SIMP_TAC [poly_exp;POLY_MUL_RID;Pm_lemma1.PDI_DEF]); (REPEAT STRIP_TAC) THEN (ASM_MESON_TAC [l4;Pm_lemma1.PDI_DEF;PDI_POLY_DIFF_COMM]) ] ) let POLY_DIVIDES_PDI2 = prove( `!n m p a. m > n ==> (poly_divides (poly_exp [--a;&1] m) p) ==> (poly_divides [--a;&1] (poly_diff_iter p n))`, MESON_TAC [POLY_EXP_DIVIDES;POLY_DIVIDES_PDI; ARITH_RULE `m > n <=> (SUC n) <= m`] ) let TAIL_GUNNER = prove( ` x < p ==> 1 <= v ==> v <= n ==> poly (poly_diff_iter (poly_exp [&0; &1] (p - 1) ** poly_exp (poly_mul_iter (\i. [-- &i; &1]) n) p) x) (&v) = &0 `, MESON_TAC [POLY_DIVIDES_ROOT; ARITH_RULE `x < p <=> (p:num) > x`; POLY_DIVIDES_PDI2; POLY_DIVIDES_MUL3; POLY_DIVIDES_POLY_EXP2; POLY_DIVIDES_POLY_MUL_ITER] ) let IS_INT_POLY = prove( `!p x.(integer x) ==> (ALL integer p) ==> integer (poly p x)`, LIST_INDUCT_TAC THEN (ASM_MESON_TAC [N_IS_INT;ALL;poly;INTEGER_ADD;INTEGER_MUL]) ) (* surprising the MESON needs so much help with the rewrites here * (i.e. i though i could just hit it with ASM_MESON_TAC with all four thms *) let INV_POLY_CMUL = prove( `!y x . (~(x = &0)) ==> (x) ## (inv x) ## y = y`, LIST_INDUCT_TAC THENL [ ASM_MESON_TAC [poly_cmul]; (REPEAT STRIP_TAC) THEN (REWRITE_TAC [poly_cmul;REAL_MUL_ASSOC]) THEN (ASM_MESON_TAC [REAL_MUL_RINV;REAL_MUL_LID]) ] ) let INV_POLY_CMUL2 = prove( `!y x . (~(x = &0)) ==> (inv x) ## (x) ## y = y`, MESON_TAC [INV_POLY_CMUL;REAL_INV_INV;REAL_INV_EQ_0] ) (* the final ASM_MESON_TAC fails if poly_cmul is rolled into the thm list *) let POLY_CMUL_EQUALS = prove( `!z x y. (~(z = &0)) ==> ((x = y) <=> (z ## x = z ## y))`, (REPEAT STRIP_TAC) THEN EQ_TAC THENL [ (SIMP_TAC[]); (SPEC_TAC (`x:(real)list`,`x:(real)list`)) THEN (SPEC_TAC (`y:(real)list`,`y:(real)list`)) THEN (LIST_INDUCT_TAC) THENL [ LIST_INDUCT_TAC THENL [ (SIMP_TAC [POLY_CMUL_CLAUSES]); (ASM_MESON_TAC [POLY_CMUL_CLAUSES;NOT_CONS_NIL])]; LIST_INDUCT_TAC THENL [ (ASM_MESON_TAC [POLY_CMUL_CLAUSES;NOT_CONS_NIL]); (ONCE_REWRITE_TAC [poly_cmul]) THEN (ASM_MESON_TAC [REAL_EQ_LCANCEL_IMP;CONS_11])] ] ] ) let PDI_LENGTH_THM = prove( `!f n. LENGTH(poly_diff_iter f n) = (LENGTH f) - n`, STRIP_TAC THEN INDUCT_TAC THENL [ (SIMP_TAC [Pm_lemma1.PDI_DEF;ARITH_RULE `(x:num) - 0 = x`]); (ONCE_REWRITE_TAC [Pm_lemma1.PDI_DEF]) THEN (ONCE_REWRITE_TAC [LENGTH_POLY_DIFF]) THEN ASM_ARITH_TAC ] ) let CAPTAINS_CLOTHES = prove( `! k q. (ALL integer q) ==> ? r .(ALL integer r) /\ r = (inv (&(FACT k))) ## (poly_diff_iter q k)` , let e0 = `(inv (&(FACT k))) ## (poly_diff_iter q k)` in let l1 = ONCE_REWRITE_RULE [GSYM (SPEC `inv (&(FACT k))` POLY_CMUL_LENGTH)] PDI_COEFF_FACT in let l2 = UNDISCH (SPEC_ALL l1) in let l3 = prove(`i < LENGTH( inv (&(FACT k)) ## poly_diff_iter q k) ==> (i + k) < LENGTH q`, MESON_TAC [PDI_LENGTH_THM;POLY_CMUL_LENGTH; ARITH_RULE `(i:num) < f -k ==> (i+k) < f`]) in (REPEAT STRIP_TAC) THEN (EXISTS_TAC e0) THEN (SIMP_TAC []) THEN (ASM_SIMP_TAC [ONCE_REWRITE_RULE [GSYM POLY_CMUL_LENGTH] POLY_CMUL_EL]) THEN (ONCE_REWRITE_TAC [GSYM ALL_EL]) THEN (REPEAT STRIP_TAC) THEN (ASM_SIMP_TAC [ONCE_REWRITE_RULE [GSYM POLY_CMUL_LENGTH] POLY_CMUL_EL]) THEN (ONCE_REWRITE_TAC [l2]) THEN (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]) THEN (MATCH_MP_TAC INTEGER_MUL) THEN STRIP_TAC THENL [ (MESON_TAC [IS_INT_FACT_DIV_FACT_DIV_FACT;REAL_MUL_SYM;real_div;REAL_MUL_ASSOC]); (ASM_MESON_TAC [l3;ALL_IMP_EL]) ] ) let MESSY_JESSE2 = prove( `n > 0 ==> p > n ==> (? (Bs:num->num->real). ! v . (1 <= v) ==> (v <= n) ==> ( (! i . (integer (Bs v i))) /\ (poly (SOD (g n p)) (&v)) = ((real_of_num 1) / (&(FACT (p - 1)))) * (psum (0,LENGTH (g n p)) (\i. (&(FACT i)) * (Bs v i))) /\ (! i. (i < p) ==> (Bs v i) = &0) ))`, let root_canal = REAL_ARITH `(x:real) * (&0) = &0` in let bs = `\(v:num) . \(x:num). if (x <= (LENGTH (g n p)) ) then (poly ((inv (&(FACT x))) ## (poly_diff_iter (poly_exp [&0; &1] (p - 1) ** poly_exp (poly_mul_iter (\i. [-- &i; &1]) n) p) x)) (&v)) else (&0)` in let l0 = prove(`ALL integer [&0;&1]`,MESON_TAC [ALL;N_IS_INT]) in let t0 = `(poly_exp [&0; &1] (p - 1) ** poly_exp (poly_mul_iter (\i. [-- &i; &1]) n) p)` in let l2 = SPECL [`i:num`;t0] CAPTAINS_CLOTHES in let l3 = prove(`ALL integer (poly_exp [&0; &1] (p - 1) ** poly_exp (poly_mul_iter (\i. [-- &i; &1]) n) p)`,MESON_TAC[l0;ALL_IS_INT_POLY_MUL;ALL_IS_INT_POLY_EXP;ALL_IS_INT_POLY_MUL_ITER]) in let l4 = MP l2 l3 in let l7 = ONCE_REWRITE_RULE [GSYM REAL_OF_NUM_EQ] FACT_NZ in let l8 = (SIMP_RULE [l7]) (SPEC `(&(FACT i)):real` POLY_CMUL_EQUALS) in (* these are not true for x =0, however we only use it for x= &(FACT i) *) let l10_0 = SPECL [`y:(real)list`;`(real_of_num (FACT i))`] INV_POLY_CMUL in let l12_0 = SPECL [`y:(real)list`;`(real_of_num (FACT i))`] INV_POLY_CMUL2 in let l10 = SIMP_RULE [REAL_FACT_NZ] l10_0 in let l12 = SIMP_RULE [REAL_FACT_NZ] l12_0 in let l9 = ONCE_REWRITE_RULE [l8] l4 in let l11 = GSYM (ONCE_REWRITE_RULE [l10] l9) in let l133 = prove(` (psum (0,m) (\i.(x i) * (if i <= m then (y i) else c))) = (psum (0,m) (\i.(x i) * (y i)))`, MESON_TAC [SUM_EQ;ARITH_RULE `(0 <= i /\ i < (m:num) + 0) ==> i <= m`]) in let l18 = MATCH_MP REAL_MUL_RINV (SPEC `i:num` l7) in let lass2 = SPECL [`g n p`;`x:real`;`v:real`] Pm_lemma2.PLANETMATH_LEMMA_2_B in let lass3 = BETA_RULE lass2 in let lass4 = CONV_RULE (RAND_CONV (RAND_CONV (REWRITE_CONV [Pm_eqn5.PLANETMATH_EQN_5]))) lass3 in let lass5 = REWRITE_RULE [POLY_CMUL;POLY_CMUL_PDI] lass4 in let lass6 = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [GSYM (ISPEC `f:num->real` ETA_AX)])) (SPEC_ALL SUM_CMUL) in let lass7 = ONCE_REWRITE_RULE [GSYM REAL_MUL_ASSOC] lass5 in let lass8 = REWRITE_RULE [lass6] lass7 in let lass10 = ONCE_REWRITE_RULE [REAL_MUL_DIV_ASSOC] lass8 in let lass11 = ONCE_REWRITE_RULE [real_div] lass10 in let lass12 = REAL_ARITH `((w:real) * x * y) * z = w * x * y * z` in let lass13 = ONCE_REWRITE_RULE [lass12] lass11 in let lass14 = REWRITE_RULE [lass6] lass13 in let MUL_ONE = REAL_ARITH `! x.(&1) * x = x /\ x * (&1) = x` in let lass15 = SIMP_RULE [REAL_MUL_LINV;REAL_FACT_NZ;MUL_ONE] lass14 in STRIP_TAC THEN STRIP_TAC THEN (EXISTS_TAC bs) THEN (REPEAT STRIP_TAC) THENL [ (BETA_TAC THEN BETA_TAC) THEN (ASM_CASES_TAC `(i <= LENGTH (g n p))`) THENL [ (ASM_SIMP_TAC[]) THEN (ASM_CASES_TAC `((i:num) < p)`) THENL [ (ASM_MESON_TAC [POLY_CMUL;TAIL_GUNNER; N_IS_INT;REAL_ARITH `(x:real) * (&0) = &0`]); (ASSUME_TAC (UNDISCH (ARITH_RULE `~(i < (p:num)) ==> (p <= i)`))) THEN (CHOOSE_TAC l11) THEN (SPLIT_CONJOINED_ASSUMPT_TAC (snd (dest_exists (concl l11)))) THEN (ASM_REWRITE_TAC[l12]) THEN (ASM_MESON_TAC [N_IS_INT;IS_INT_POLY]) ]; (ASM_MESON_TAC [N_IS_INT]) ]; (BETA_TAC) THEN (SIMP_TAC [l133]) THEN (SIMP_TAC [POLY_CMUL;l18;REAL_MUL_ASSOC;REAL_MUL_LID]) THEN (SIMP_TAC [lass15;REAL_INV_1OVER]); BETA_TAC THEN (ASM_MESON_TAC [TAIL_GUNNER;POLY_CMUL;root_canal]) ] ) let INTEGER_PSUM = prove( `!f m.(! i . i < m ==> integer (f i)) ==> (integer (psum (0,m) f))`, let l0 = ASSUME `!i. i < SUC m ==> integer (f i)` in let l1 = SPEC `m:num` l0 in let l2 = SIMP_RULE [ARITH_RULE `m < SUC m`] l1 in STRIP_TAC THEN INDUCT_TAC THENL [ (MESON_TAC [sum;int_of_num;int_of_num_th;N_IS_INT]); (SIMP_TAC [sum;ARITH_RULE `0 + (x:num) = x`]) THEN (STRIP_TAC) THEN (MATCH_MP_TAC INTEGER_ADD) THEN (ASM_MESON_TAC[l2;ARITH_RULE `(i:num) < m ==> i < SUC m`]) ] ) let INT_DIVIDES_PSUM = prove( `!f m p.(! i . i < m ==> ((integer (f i)) /\ (int_divides p (int_of_real (f i))))) ==> (int_divides p (int_of_real (psum (0,m) f)))`, let l0 = ASSUME `!i. i < SUC m ==> integer (f i) /\ p divides int_of_real (f i)` in let l1 = SPEC `m:num` l0 in let l2 = SIMP_RULE [ARITH_RULE `m < SUC m`] l1 in let l3 = ASSUME `(!i. i < m ==> integer (f i)) ==> integer (psum (0,m) f)` in let l4 = SPEC `i:num` l0 in let l5 = DISCH `i < SUC m` ((CONJUNCT1 (UNDISCH l4))) in let l8 = prove(`(!i.i < SUC m ==> (integer (f i))) ==> (!i.i < m ==> (integer (f i)))`, MESON_TAC [ARITH_RULE `i < m ==> i < SUC m`]) in let ll1 = MP l8 (GEN_ALL l5) in let ll2 = MP l3 ll1 in let ll3 = MATCH_MP INT_OF_REAL_ADD (CONJ ll2 (CONJUNCT1 l2)) in STRIP_TAC THEN INDUCT_TAC THENL [ (MESON_TAC [sum;int_of_num;int_of_num_th;INT_DIVIDES_0]); (SIMP_TAC [sum;ARITH_RULE `0 + (x:num) = x`]) THEN (ASSUME_TAC (SPECL [`f:num->real`;`m:num`] INTEGER_PSUM)) THEN (STRIP_TAC) THEN (STRIP_TAC) THEN (ONCE_REWRITE_TAC [ll3]) THEN (MATCH_MP_TAC INT_DIVIDES_ADD) THEN (CONJ_TAC) THENL [ (ASM_MESON_TAC [ARITH_RULE `i < m ==> i < SUC m`]); (ASM_MESON_TAC [ARITH_RULE `m < SUC m`]) ] ] ) let PLANET_MATH_beta = prove( `p > n ==> n > 0 ==> (! v. (1 <= v /\ v <= n) ==> ( (integer (poly (SOD (g n p )) (&v))) /\ ((&p) divides (int_of_real (poly (SOD (g n p )) (&v)))) ) )`, let l2 = GSYM (ONCE_REWRITE_RULE [REAL_MUL_SYM] real_div) in let ll3 = ARITH_RULE `(int_of_num p) * &0 = &0` in let l7 = UNDISCH (SPECL [`i:num`;`p:num`] IS_INT_FACT_DIV) in let l11 = prove(`p > 0 ==> FACT p = p * (FACT (p-1))`, MESON_TAC [FACT; ARITH_RULE `p > 0 ==> SUC (p -1) = p `]) in let l12 = UNDISCH (UNDISCH (ARITH_RULE `(p:num) > n ==> n > 0 ==> p > 0`)) in let l13 = MP l11 l12 in let t9 = `1 <= (v:num) ==> v <= (n:num) ==> (!v. 1 <= v ==> v <= n ==> (!i. integer (Bs v i)) /\ poly (SOD (g n p)) (&v) = &1 / &(FACT (p - 1)) * psum (0,LENGTH (g n p)) (\i. &(FACT i) * Bs v i) /\ (!i. i < p ==> Bs v i = &0)) ==> (integer (Bs v i))` in let lll0 = UNDISCH (UNDISCH (UNDISCH (prove(t9,MESON_TAC[])))) in let l8 = REWRITE_RULE [l13;real_div;REAL_INV_MUL] l7 in let l9 = REWRITE_RULE [N_IS_INT;GSYM REAL_OF_NUM_MUL] l8 in let l10 = REWRITE_RULE [REAL_INV_MUL] l9 in let l11 = MATCH_MP (INTEGER_MUL) (CONJ l10 lll0) in let l12 = MATCH_MP INT_OF_REAL_MUL (CONJ (SPEC `p:num` N_IS_INT) l11) in let l15 = GSYM l12 in let lll8 = ARITH_RULE `p > n ==> n > 0 ==> ~(p = 0)` in let lll9 = ONCE_REWRITE_RULE [GSYM REAL_OF_NUM_EQ] lll8 in let lll10 = UNDISCH (UNDISCH lll9) in let sc1 = prove (`(~((x:real) = &0)) ==> (x * y * inv x) = y`, MESON_TAC [REAL_MUL_RID;REAL_MUL_ASSOC; REAL_MUL_SYM;REAL_MUL_LINV;REAL_MUL_LID]) in let sc2 = prove (`(~((x:real) = &0)) ==> (x * y * (inv x) * z) = y * z`, MESON_TAC [sc1;REAL_MUL_ASSOC]) in (REPEAT STRIP_TAC) THENL [ (CHOOSE_TAC (UNDISCH (UNDISCH MESSY_JESSE2))) THEN (ASM_SIMP_TAC []) THEN (ONCE_REWRITE_TAC [GSYM SUM_CMUL]) THEN (MATCH_MP_TAC INTEGER_PSUM) THEN (REPEAT STRIP_TAC) THEN BETA_TAC THEN (ASM_CASES_TAC `i < (p:num)`) THENL [ (ASM_SIMP_TAC [N_IS_INT;REAL_ARITH `(x:real) * (&0) = &0`]); (ASSUME_TAC (UNDISCH (ARITH_RULE `(~((i:num) < p)) ==> i >= p-1`))) THEN (ASM_MESON_TAC [REAL_INV_1OVER;REAL_MUL_ASSOC; IS_INT_FACT_DIV; l2;INTEGER_MUL]) ]; (CHOOSE_TAC (UNDISCH (UNDISCH MESSY_JESSE2))) THEN (ASM_SIMP_TAC []) THEN (ONCE_REWRITE_TAC [GSYM SUM_CMUL]) THEN (MATCH_MP_TAC INT_DIVIDES_PSUM) THEN (REPEAT STRIP_TAC) THENL [ BETA_TAC THEN (ASM_CASES_TAC `i < (p:num)`) THENL [ (ASM_SIMP_TAC [N_IS_INT;REAL_ARITH `(x:real) * (&0) = &0`]); (ASSUME_TAC (UNDISCH (ARITH_RULE `(~((i:num) < p)) ==> i >= p-1`))) THEN (ASM_MESON_TAC [REAL_INV_1OVER;REAL_MUL_ASSOC; IS_INT_FACT_DIV; l2;INTEGER_MUL]) ]; (ONCE_REWRITE_TAC [int_divides]) THEN BETA_TAC THEN (ASM_CASES_TAC `i < (p:num)`) THENL [ (ASM_SIMP_TAC [N_IS_INT;REAL_ARITH `(x:real) * (&0) = &0`]) THEN (EXISTS_TAC `int_of_num 0`) THEN (MESON_TAC [ll3;int_of_num_th;int_of_num]); (ASSUME_TAC (UNDISCH (ARITH_RULE `(~((i:num) < p)) ==> i >= p`))) THEN (EXISTS_TAC `int_of_real (((&(FACT i))/(&(FACT p))) * (Bs (v:num) i))`) THEN (ONCE_REWRITE_TAC [int_of_num]) THEN (ONCE_REWRITE_TAC [l13]) THEN (ONCE_REWRITE_TAC [N_IS_INT;GSYM REAL_OF_NUM_MUL]) THEN (SIMP_TAC [ real_div]) THEN (ONCE_REWRITE_TAC [ REAL_INV_MUL]) THEN (ONCE_REWRITE_TAC [ REAL_MUL_LID]) THEN (ONCE_REWRITE_TAC [l15]) THEN (ASSUME_TAC lll10) THEN (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]) THEN (ASM_MESON_TAC [sc2;REAL_MUL_SYM]) ] ] ] ) let JUNE_LEMMA = prove( `n > 0 ==> p > n ==> v <= n ==> integer (poly (SOD (g n p)) (&v))`, let lem0 = CONJUNCT1 (UNDISCH_ALL PLANET_MATH_alpha) in let lem1 = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL PLANET_MATH_beta)) in let lem2 = DISCH `1 <= v /\ v <= n` (CONJUNCT1 lem1) in let lem3 = SPEC `SUC v` (GEN `v:num` lem2) in let lem4 = SIMP_RULE [ARITH_RULE `1 <= SUC v`] lem3 in (STRIP_TAC THEN STRIP_TAC) THEN (SPEC_TAC (`v:num`,`v:num`)) THEN (INDUCT_TAC THENL [(SIMP_TAC [lem0]);(ACCEPT_TAC lem4)]) ) let DIVIDES_SUM_NOT_ZERO = prove( `!(x:int) (y:int) (z:int). (~(z divides x)) /\ (z divides y) ==> ~(x + y = &0)`, let l0 = ASSUME `(x:int) + y = &0` in let l1 = ONCE_REWRITE_RULE [ARITH_RULE `((x:int) + y = &0) <=> (x = --y)`] l0 in (REPEAT STRIP_TAC) THEN (UNDISCH_TAC `~((z:int) divides x)`) THEN (REWRITE_TAC [l1]) THEN (UNDISCH_TAC `((z:int) divides y)`) THEN (INTEGER_TAC) ) let NUM_OF_INT_ABS = prove( `!(x:num) (y:int).num_of_int (abs y) = x <=> abs y = &x`, (* stupid... *) let j0 = UNDISCH (prove(`(num_of_int (abs y) = x) ==> x = num_of_int (abs y)`,MESON_TAC [])) in let j1 = ARITH_RULE `&0 <= ((abs y):int)` in let j2 = MATCH_MP INT_OF_NUM_OF_INT j1 in (REPEAT STRIP_TAC) THEN EQ_TAC THENL [ (STRIP_TAC THEN SIMP_TAC [j0;j2]); (ASM_SIMP_TAC [NUM_OF_INT_OF_NUM])] ) let INT_DIVIDES_IMP_ABS_NUM_DIVIDES = prove( `! (x:int) (y:num). (x divides (&y)) ==> ((num_of_int (abs x)) divides y)`, let w0 = ARITH_RULE `((&0):int) <= abs x` in let w1 = fst (EQ_IMP_RULE (SPEC `abs (x:int)` NUM_OF_INT)) in let w2 = MP w1 w0 in let w3 = ARITH_RULE `((&0):int) <= x ==> abs x = x` in let w4 = ARITH_RULE `(~(((&0):int) <= x)) ==> abs x = -- x` in (REWRITE_TAC [int_divides;num_divides]) THEN (REPEAT STRIP_TAC) THEN (ASM_REWRITE_TAC [w2]) THEN (ASM_CASES_TAC `((&0):int) <= x`) THENL [ (ONCE_REWRITE_TAC [UNDISCH w3]) THEN (EXISTS_TAC `x':int`) THEN (REFL_TAC); (ONCE_REWRITE_TAC [UNDISCH w4]) THEN (EXISTS_TAC `--x':int`) THEN (ARITH_TAC) ] ) let INT_PRIME_NUM_PRIME = prove( `!p. int_prime (&p) <=> prime p`, (ONCE_REWRITE_TAC [int_prime;prime]) THEN (MESON_TAC [divides;num_divides; INT_ABS;INT_POS;INT_OF_NUM_EQ;INT_LT_IMP_NE;INT_GT; ARITH_RULE `2 <= p ==> abs((&p):int) > &1`; INT_DIVIDES_IMP_ABS_NUM_DIVIDES;NUM_OF_INT_ABS;PRIME_GE_2; prime;int_prime ]) ) let DIVIDES_INT_OF_REAL_ADD = prove( `!x y p.integer x /\ integer y /\ p divides (int_of_real x) /\ p divides (int_of_real y) ==> p divides (int_of_real (x + y))`, SIMP_TAC [INT_OF_REAL_ADD;INT_DIVIDES_ADD] ) let ITCHY_LEMMA = prove( `! f p n. (!v.1<= v /\ v <= n ==> integer (f v) /\ &p divides int_of_real (f v)) ==> (&p divides int_of_real (sum (1..n) f))`, let l0 = fst (EQ_IMP_RULE (SPECL [`1`;`0`] (GSYM NUMSEG_EMPTY))) in let l1 = INTEGER_RULE `&p divides ((&0))` in let l2 = SPEC `0` (GEN_ALL int_of_num) in let l3 = ONCE_REWRITE_RULE [l2] l1 in let l4 = SPECL [`f:num->real`;`n:num`;`1`] IS_INT_SUM in let l5 = prove(`(!v. 1 <= v /\ v <= SUC n ==> integer (f v)) ==> (!i. 1 <= i /\ i <= n ==> integer (f i))`,MESON_TAC [ARITH_RULE `v <= n ==> v <= SUC n`]) in let l6 = IMP_TRANS l5 l4 in let l7 = prove(`(!v. 1 <= v /\ v <= SUC n ==> (integer (f v)) /\ (&p) divides int_of_real (f v)) ==> (&p) divides int_of_real (f (SUC n))`,MESON_TAC [ARITH_RULE `1 <= (SUC n) /\ SUC n <= SUC n`]) in let l9 = prove(`(!v. 1 <= v /\ v <= SUC n ==> integer (f v)) ==> integer (f (SUC n))`,MESON_TAC [ARITH_RULE `1 <= SUC n /\ SUC n <= SUC n`]) in let tm = `\(v:num).integer (f v) /\ (&p) divides int_of_real (f v)` in let l10 = BETA_RULE (SPEC tm SHRIVER) in let l11 = UNDISCH (SPEC `1` (GEN `m:num` l10)) in STRIP_TAC THEN STRIP_TAC THEN INDUCT_TAC THENL [ SIMP_TAC [ARITH_RULE `0 < 1`;l0;SUM_CLAUSES;l3]; DISCH_TAC THEN (SIMP_TAC [SUM_CLAUSES_NUMSEG;ARITH_RULE `1 <= SUC n`]) THEN (MATCH_MP_TAC DIVIDES_INT_OF_REAL_ADD) THEN (CONJ_TAC) THENL [ ASM_SIMP_TAC [l6]; CONJ_TAC THENL [ ASM_SIMP_TAC [l9]; CONJ_TAC THENL [ ASM_SIMP_TAC [l11]; ASM_SIMP_TAC [l7] ]]]] ) let GOTTA_DO_DISHES_LEMMA = prove( `!(x:real) (y:real). (integer x) /\ (integer y) ==> (?(z:int).(~(z divides (int_of_real x))) /\ (z divides (int_of_real y))) ==> ~(x + y = &0)`, let mk_lemma x y = let lem0 = SPECL [x;y;`z:int`] DIVIDES_SUM_NOT_ZERO in let lem1 = TAUT `(X /\ Y ==> Z) <=> (X ==> Y ==> Z)` in UNDISCH (UNDISCH (ONCE_REWRITE_RULE [lem1] lem0)) in let mk_tac x y = (ASM_REWRITE_TAC [GSYM int_of_num;INT_OF_REAL_NEG_INT_OF_NUM]) THEN (STRIP_TAC) THEN (REWRITE_TAC [GSYM int_neg_th;GSYM int_eq; GSYM int_add_th;GSYM int_of_num_th]) THEN (ACCEPT_TAC (mk_lemma x y)) in (ONCE_REWRITE_TAC [is_int]) THEN (STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC ) THENL [ mk_tac `(&n):int` `(&n'):int` ; mk_tac `(&n):int` `--(&n'):int` ; mk_tac `--(&n):int` `(&n'):int` ; mk_tac `--(&n):int` `--(&n'):int` ] ) let RAINY_DAY = prove( `! p x y. prime p ==> (&p) > x ==> integer x ==> x > (&0) ==> integer y ==> (((&p) divides (int_of_real (x * y))) <=> ((&p) divides int_of_real y))`, let ss3 = SPECL [`int_of_num n`;`(&p):int`] INT_PRIME_COPRIME_LT in let ss4 = ONCE_REWRITE_RULE [ARITH_RULE `abs ((&x):int) = &x`] ss3 in let ss40 = prove(`!(x:num) (y:num). (int_of_num x) < (int_of_num y) <=> (real_of_num x) < (real_of_num y)`,SIMP_TAC [INT_OF_NUM_LT;REAL_OF_NUM_LT]) in let ss5 = ONCE_REWRITE_RULE [ss40;INT_COPRIME_SYM;INT_PRIME_NUM_PRIME] ss4 in let ss6 = SPECL [`(&p):int`;`(&n):int`;`int_of_real y`] INT_COPRIME_DIVPROD in let ss7 = ONCE_REWRITE_RULE [TAUT `(X /\ Y ==> Z) <=> (Y ==> X ==> Z)`] ss6 in let ss8 = IMP_TRANS ss5 ss7 in let ss9 = ONCE_REWRITE_RULE [TAUT `(A /\ B /\ C ==> D ==> E) <=> (A ==> B ==> C ==> D ==> E)`] ss8 in let ss10 = UNDISCH ss9 in (REPEAT STRIP_TAC) THEN (ASM_SIMP_TAC [INT_OF_REAL_MUL]) THEN (EQ_TAC) THENL [ (SIMP_TAC [INT_DIVIDES_LMUL]) THEN (UNDISCH_TAC `integer x`) THEN (ONCE_REWRITE_TAC [is_int]) THEN (STRIP_TAC) THENL [ (ASM_REWRITE_TAC[]) THEN (ONCE_REWRITE_TAC [GSYM int_of_num]) THEN (UNDISCH_TAC `(&(p:num)) > (x:real)`) THEN (UNDISCH_TAC `(x:real) > &0`) THEN (ASM_REWRITE_TAC []) THEN (ONCE_REWRITE_TAC [REAL_ARITH `(y:real) > z <=> z < y`]) THEN (ACCEPT_TAC ss10); (ASM_ARITH_TAC) ]; (SIMP_TAC [INT_DIVIDES_LMUL]) ] ) let PLANET_MATH_gamma = prove( `n > 0 ==> p > n ==> prime p ==> &p > (EL 0 c) ==> (EL 0 c) > (&0) ==> n = PRE (LENGTH (c)) ==> (ALL integer c) ==> ( (integer (LHS c (g n p))) /\ ~((LHS c (g n p)) = &0))`, let lemma01 = SPECL [`\i. EL i c * poly (SOD (g n p)) (&i)`;`n:num`;`k:num` ] IS_INT_SUM in let lemma02 = BETA_RULE lemma01 in let lemma021 = UNDISCH JUNE_LEMMA in let lemma022 = UNDISCH_ALL (ARITH_RULE `n > 0 ==> p > n ==> p > 1`) in let lemma023 = DISCH_ALL (SIMP_RULE [lemma022] lemma021) in let lemma04 = UNDISCH (UNDISCH lemma023) in let lemma08 = ISPECL [`c:(real)list`;`v:num`;`integer`] ALL_IMP_EL in let lemma09 = ADD_ASSUM `n > 0` (UNDISCH lemma08) in let lemma10 = ADD_ASSUM `n = PRE (LENGTH (c:(real)list))` lemma09 in let lemma11 = ARITH_RULE `n > 0 ==> (n = PRE (LENGTH (c:(real)list))) ==> ((v < LENGTH c) <=> (v <= n))` in let lemma12 = UNDISCH (UNDISCH lemma11) in let lemma13 = ONCE_REWRITE_RULE [lemma12] lemma10 in let lemma15 = CONJ (UNDISCH (UNDISCH lemma04)) (UNDISCH lemma13) in let lemma16 = MATCH_MP INTEGER_MUL (ONCE_REWRITE_RULE [CONJ_SYM] lemma15) in let lemma17 = DISCH `v <= (n:num)` lemma16 in let lemma18 = ADD_ASSUM_DISCH `k <= (v:num)` lemma17 in let lemma19 = ONCE_REWRITE_RULE [TAUT `(X ==> Y ==> Z) <=> ((X /\ Y) ==> Z)`] lemma18 in let lemma20 = GEN `v:num` lemma19 in let lemma21 = GEN `k:num` (MATCH_MP lemma02 lemma20) in let lemma29 = SPEC `0` lemma21 in let lemma30 = GSYM (ASSUME `n = PRE (LENGTH (c:(real)list))`) in let lemma300 = SPECL [`f:(num -> real)`;`0`;`PRE (LENGTH (c:(real)list))`] SUM_CLAUSES_LEFT in let lemma31 = ADD_ASSUM `n > 0` (ADD_ASSUM `n = PRE (LENGTH (c:(real)list))` lemma300) in let lemma32 = MP lemma31 (ARITH_RULE `0 <= PRE (LENGTH (c:(real)list))`) in let lemma0000 = BRW `(X ==> Y ==> Z) <=> ((X /\ Y) ==> Z)` GOTTA_DO_DISHES_LEMMA in let lemmaa00 = UNDISCH PLANET_MATH_alpha in let lemmaa03 = ARITH_RULE `n >0 ==> ((n = PRE (LENGTH (c:(real)list))) ==> 0 < (LENGTH c))` in let lemmaa04 = ISPECL [`c:(real)list`;`0`;`integer`] ALL_IMP_EL in let lemmaa05 = MP (UNDISCH lemmaa04) (UNDISCH (UNDISCH lemmaa03)) in let c1 = ARITH_RULE `n > 0 ==> n = PRE (LENGTH (c:(real)list)) ==> 0 < (LENGTH (c:(real)list))` in let c2 = UNDISCH (UNDISCH c1) in let c3 = MP (UNDISCH lemmaa04) c2 in let c4 = CONJUNCT1 (UNDISCH (UNDISCH (UNDISCH PLANET_MATH_alpha))) in let c40 = CONJUNCT2 (UNDISCH (UNDISCH (UNDISCH PLANET_MATH_alpha))) in let c5 = SPECL [`p:num`;`(EL 0 c):real`;`poly (SOD (g n p)) (&0)`] RAINY_DAY in let c7 = ((UNDISCH (UNDISCH c5))) in let c8 = SIMP_RULE [c3] c7 in let c9 = UNDISCH c8 in let c10 = SIMP_RULE [c4] c9 in let d0 = UNDISCH PLANET_MATH_beta in let d1 = BRW `(X ==> Y ==> Z) <=> (Y ==> X ==> Z)` d0 in let d2 = SIMP_RULE [UNDISCH (ARITH_RULE `p > (n:num) ==> n > 0 ==> p > 1`)] d1 in let d3 = UNDISCH d2 in let d8 = CONJUNCT2 (UNDISCH (SPEC_ALL d3)) in let d9 = SPECL [`(&p):int`;`int_of_real (EL v c)`;`int_of_real (poly (SOD (g n p)) (&v))`] INT_DIVIDES_LMUL in let d10 = ADD_ASSUM `ALL integer c` d9 in let d11 = ADD_ASSUM `n = PRE (LENGTH (c:(real)list))` d10 in let d12 = ADD_ASSUM `1 <= v /\ v <= n` d11 in let d13 = CONJUNCT1 (UNDISCH (SPEC_ALL d3)) in let d14 = DISCH `1 <= v` (ADD_ASSUM `1 <= v` lemma13) in let d15 = BRW `(X ==> Y ==> Z) <=> (X /\ Y ==> Z)` d14 in let d16 = UNDISCH d15 in let d17 = CONJ d16 d13 in let d18 = GSYM (MATCH_MP INT_OF_REAL_MUL d17) in let d19 = ONCE_REWRITE_RULE [d18] d12 in let d20 = MP d19 d8 in let d21 = UNDISCH (SPECL [`1`;`v:num`] (GEN `k:num` lemma20)) in let d22 = CONJ d21 d20 in let d23 = DISCH `1 <=v /\ v <= n` d22 in let d24 = GEN `v:num` d23 in let d25 = MATCH_MP ITCHY_LEMMA d24 in ((REPEAT STRIP_TAC) THENL [ (ONCE_REWRITE_TAC [Pm_eqn4.LHS]) THEN (SIMP_TAC [lemma30;lemma29]); (UNDISCH_TAC `LHS c (g n p) = &0`) THEN (REWRITE_TAC [Pm_eqn4.LHS]) THEN (SIMP_TAC [lemma32;ARITH_RULE `0 + 1 = 1`]) THEN (ONCE_REWRITE_TAC [lemma30]) THEN (MATCH_MP_TAC lemma0000) THEN (CONJ_TAC) THENL [ (CONJ_TAC) THENL [ (MATCH_MP_TAC INTEGER_MUL) THEN (ASM_SIMP_TAC [lemmaa00;lemmaa05]); (ACCEPT_TAC (SPEC `1` lemma21)) ]; (EXISTS_TAC `(&p):int`) THEN (CONJ_TAC) THENL [(ONCE_REWRITE_TAC [c10]) THEN (ASM_SIMP_TAC [c40]); (ACCEPT_TAC d25) ] ] ] ) ) end;; module Finale = struct let IS_INT_NZ_ABS_GE_1 = prove ( `!x. ((integer x) /\ ~(x = &0)) ==> ~(abs x < &1)`, let lemmy0 = REAL_ARITH `(x:real) < y <=> ~(y <= x)` in let lemmy1 = ONCE_REWRITE_RULE [lemmy0] REAL_NZ_IMP_LT in let lemmy2 = REAL_ARITH `(real_neg x) = &0 <=> x = &0` in let lemmy3 = REAL_ARITH `&0 <= (real_neg x) <=> x <= &0` in (ONCE_REWRITE_TAC [is_int]) THEN (ONCE_REWRITE_TAC [TAUT `(X /\ Y ==> Z) <=> (X ==> Y ==> Z)`]) THEN (STRIP_TAC) THEN (STRIP_TAC) THENL [ (ASM_REWRITE_TAC[]) THEN (SIMP_TAC [REAL_ABS_NUM] ) THEN (ONCE_REWRITE_TAC [REAL_OF_NUM_LT;REAL_OF_NUM_EQ]) THEN (ARITH_TAC); (ASM_REWRITE_TAC[]) THEN (ONCE_REWRITE_TAC [real_abs]) THEN (ONCE_REWRITE_TAC [lemmy2;lemmy3]) THEN (ONCE_REWRITE_TAC [REAL_OF_NUM_EQ]) THEN (SIMP_TAC [lemmy1;REAL_NEG_NEG]) THEN (ONCE_REWRITE_TAC [REAL_OF_NUM_LT]) THEN (ARITH_TAC) ] ) let PBR_LEMMA = prove( `!n1 n2 n3 p. p > MAX n1 (MAX n2 n3) ==> (p > n1 /\ p > n2 /\ p > n3)`, (REWRITE_TAC [MAX]) THEN ARITH_TAC ) let BIGGER_PRIME_EXISTS = prove( `!(n:num). ?p. prime p /\ p > n`, let lem0 = prove(`{x | prime x} = prime`,SET_TAC[]) in let lem1 = ARITH_RULE `p > n <=> ~(p <= (n:num))` in MESON_TAC [PRIMES_INFINITE;lem0;lem1;IN_ELIM_THM;num_FINITE;INFINITE] ) let BUD_LEMMA = prove( `!(f:num->bool) (n1:num) (n2:num).((?(N:num) . !(p:num).p > N ==> f p) ==> (? (p0:num).prime p0 /\ p0 > n1 /\ p0 > n2 /\ f p0))`, let amigo3 = SPECL [`N:num`;`n1:num`;`n2:num`;`p:num`] PBR_LEMMA in let amigo4 = UNDISCH amigo3 in (REPEAT STRIP_TAC) THEN (CHOOSE_TAC (SPEC `MAX N (MAX n1 n2)` BIGGER_PRIME_EXISTS )) THEN (EXISTS_TAC `p:num`) THEN (UNDISCH_TAC `prime p /\ p > MAX N (MAX n1 n2)`) THEN (ONCE_REWRITE_TAC [TAUT `(X /\ Y ==> Z) <=> (X ==> Y ==> Z)`]) THEN (DISCH_TAC THEN DISCH_TAC) THEN (ASM_SIMP_TAC [amigo4]) ) let ALL_IMP_EL = prove( `! (l:(a)list) i P. (ALL P l) ==> (i < LENGTH l) ==> P (EL i l)`, SIMP_TAC[GSYM ALL_EL] ) let HAMMS_LEMMA = prove( `~(?c. ALL integer c /\ LENGTH c > 1 /\ EL 0 c > &0 /\ (!f. LHS c f = RHS c f))`, let erica0 = UNDISCH_ALL Pm_eqn4_lhs.PLANET_MATH_gamma in let erica1 = MATCH_MP IS_INT_NZ_ABS_GE_1 erica0 in let erica2 = ASM_REWRITE_RULE [] erica1 in let erica3 = SPEC_ALL Pm_eqn4_rhs.LT_ONE in let erica4 = MATCH_MP BUD_LEMMA erica3 in let erica5 = ADD_ASSUM `ALL integer c` erica4 in let erica8 = ARITH_RULE `(n = PRE (LENGTH (c:(real)list))) ==> n > 0 ==> 0 < (LENGTH c) ` in let erica9 = UNDISCH (UNDISCH erica8) in let erica10 = UNDISCH (ISPECL [`c:(real)list`;`0`;`integer`] ALL_IMP_EL) in let erica11 = MP erica10 erica9 in let erica12 = ONCE_REWRITE_RULE [is_int] erica11 in let erica13 = ARITH_RULE `!n. ~(( -- (real_of_num n)) > &0)` in let erica14 = prove( `n = PRE (LENGTH c) ==> n > 0 ==> ALL integer c ==> (EL 0 c) > &0 ==> ?n. EL 0 c = &n`, MESON_TAC [DISCH_ALL erica12;erica13] ) in let erica15 = UNDISCH_ALL erica14 in let sim0 = SELECT_RULE (ASSUME (concl erica15)) in let sim1 = DISCH (concl erica15) sim0 in let sim2 = MP sim1 erica15 in let erica18 = SPECL [`n:num`;`@n. EL 0 c = (real_of_num n)`] erica5 in let erica19 = ONCE_REWRITE_RULE [GSYM REAL_OF_NUM_GT] erica18 in let erica20 = ONCE_REWRITE_RULE [GSYM sim2] erica19 in let erica21 = ONCE_REWRITE_RULE [REAL_OF_NUM_GT] erica20 in let erica22 = DISCH `(real_of_num p) > EL 0 c` erica2 in let erica23 = DISCH `(p:num) > n` erica22 in let erica24 = DISCH `prime (p:num)` erica23 in let erica25 = GEN `p:num` erica24 in let erica28 = UNDISCH (ARITH_RULE `n = PRE (LENGTH (c:(real)list)) ==> ((n > 0) <=> (LENGTH c) > 1)`) in let erica29 = UNDISCH (ONCE_REWRITE_RULE [erica28] (DISCH `n > 0` (erica25))) in let erica30 = UNDISCH (ONCE_REWRITE_RULE [erica28] (DISCH `n > 0` (erica21))) in (CONV_TAC NNF_CONV) THEN (REPEAT STRIP_TAC) THEN (ASM_MESON_TAC [DISCH_ALL erica29;DISCH_ALL erica30]) ) let TRANSCENDENTAL_E = prove( `transcendental (exp (&1))`, MESON_TAC [HAMMS_LEMMA;Pm_eqn4.PLANETMATH_EQN_4] ) end;; Finale.TRANSCENDENTAL_E;;