今回は次を証明します． fを整数係数の１変数多項式関数とするとき，任意の非負整数nに対してf(n)が素数ならば，fは定数関数である 方針は，素数f(0)の任意の正整数倍に対する関数値も素数，従ってf(0)となることより，任意の正整数を根とする多項式を見出す…

昨日のsimplifyです．a+bの符号は:int上の処理に含めました．(* *)内はMESON任せの方法で時間が掛かります． needs "Complex/make.ml";;let lemma04 = prove (`!a b:real. (?x. ~( x = Cx(&1) ) /\ x pow 3 = Cx(&1) /\ (Cx(a)*x+Cx(b))*(Cx(a)*x pow 2+Cx(b…

今回は，虚数と整数とが混在する証明です．変数はintとし，&，real_of_int，num_of_intを介して各ドメインの性質を適用します．なお，SOS系の利用はできるだけ控えました． needs "Complex/make.ml";;let lemma04 = prove (`!a b:real. (?x. ~( x = Cx(&1) )…

今回は Example(11)のmy_thm02の応用として を証明します．まずは g`!x a. (\n. x n - x (n-1) ) tends_num_real a ==> (\n. (x n - x 0) / &n ) tends_num_real a`;; e(REPEAT STRIP_TAC THEN SIMP_TAC[SEQ] THEN REPEAT STRIP_TAC);; let lemma02 = SPECL[…

今回は の証明です． let limits_num_pinfinity = define `!x:num->real. limits_num_pinfinity x = !K:real. &0 (?N:num. !n. n>=N ==> K g`!x. limits_num_pinfinity x==>limits_num_pinfinity (\n. (sum(1..n)x)/ &n)`;; e(REWRITE_TAC[limits_num_pinfin…

極限値が実数aの場合です． let my_thm02 = prove (`!x a. x tends_num_real a ==> (\n. sum(1..n)x / &n) tends_num_real a`, let lemma01,lemma02,lemma03 = CONV_RULE (REWRITE_CONV[SEQ; REAL_SUB_RZERO; SUM_SUB_NUMSEG; SUM_CONST_NUMSEG; ARITH_RULE`…

今回は # g`!x:num->real. x tends_num_real &0 ==> (\n. sum(1..n)x / &n) tends_num_real &0`;; val it : goalstack = 1 subgoal (1 total)`!x. x tends_num_real &0 ==> (\n. sum (1..n) x / &n) tends_num_real &0` です．数学的には分割して評価する標…

sos.mlには，次の定理が含まれています． # search[name"SOS"];; val it : (string * thm) list = [("INT_SOS_EQ_0", |- !x y. x pow 2 + y pow 2 = &0 x = &0 /\ y = &0); ("REAL_SOS_EQ_0", |- !x y. x pow 2 + y pow 2 = &0 x = &0 /\ y = &0)] 今回はこ…

SYM_CONV rewrites `a = b` to `b = a` # SYM_CONV `0=1`;; val it : thm = |- 0 = 1 1 = 0 # SYM (ARITH_RULE `0+1=1`);; val it : thm = |- 1 = 0 + 1 # SYM (ARITH_RULE `!m. m*0=0`);; Exception: Failure "dest_eq". CONV_RULE c th uses c to rewrite …

ONCE_DEPTH_CONV c applies c to only the first suitable subterm(s) found in a top-down search, i.e. the outermost subterm(s). # ONCE_DEPTH_CONV BETA_CONV `(\x. x+1) ((\y. y+2) 3)`;; val it : thm = |- (\x. x + 1) ((\y. y + 2) 3) = (\y. y + 2…

A conversion takes a term and returns an equality theorem with the term on the lhs (or it fails).NO_CONV is a conversion which always fails. # NO_CONV `0`;; Exception: Failure "NO_CONV". ALL_CONV is a conversion which always succeeds witho…

■ tacticをtheorem_tacticとして用いる方法 tactic tacの書式はtac goalstack， theorem_tactic ttacの書式はttac thm goalstackなので， ttac thmがcurryingによりtacticになっている訳です． 従って，(fun (t:thm)->tac)とすればtheorem_tacticが得られま…

BETA_CONV `(\x. A) y` gives `|- (\x. A) y = A[y/x]` # BETA_CONV `(\x. x+2) 1` ;; val it : thm = |- (\x. x + 2) 1 = 1 + 2 AP_TERM `f` `ASM1 |- a = b` gives `ASM1 |- (f a) = (f b)` # AP_TERM `(\x. x+2)` (ASSUME`a=b:num`) ;; val it : thm = a …

今回からは，QUICK_REFERENCE.txt，VERYQUICK_REFERENCE.txtに沿って進みたいと思います．■ thm: (HOL Light's 10 primitive inference rules) + αREFL `x` gives `|- x = x` # REFL `x:num` ;; val it : thm = |- x = x # REFL `x:bool` ;; val it : thm = …

■ 前件の導入 # g`a==>b`;; Warning: Free variables in goal: a, b val it : goalstack = 1 subgoal (1 total)`a ==> b`# e(DISCH_THEN(fun t->ALL_TAC));; val it : goalstack = 1 subgoal (1 total)`b` ■ 仮定の導入 # g`a==>b`;; Warning: Free variable…

■ 今更ですが，0 # LE_0;; val it : thm = |- !n. 0 で賄えることに気付きました． # g`!n. sum(0..n)(\k. &k)= &n*( &n+ &1)/ &2`;; val it : goalstack = 1 subgoal (1 total)`!n. sum (0..n) (\k. &k) = &n * (&n + &1) / &2`# e INDUCT_TAC;; val it : g…

IMAGEの用例です． # IMAGE;; val it : thm = |- !s f. IMAGE f s = {y | ?x. x IN s /\ y = f x} # g`y IN (IMAGE (\x. x+ &1) {x| &0 &1 &1 # e (REWRITE_TAC[IMAGE;IN_ELIM_THM]);; val it : goalstack = 1 subgoal (1 total)`(?x. &0 &1 # e EQ_TAC;; va…

今回は微分法です． # diffl;; val it : thm = |- !f x l. (f diffl l) x ((\h. (f (x + h) - f x) / h) tends_real_real l) (&0) イプシロンデルタでは # REWRITE_RULE[LIM; REAL_SUB_RZERO] diffl;; val it : thm = |- !f x l. (f diffl l) x (!e. &0 ==> …

今回は，連続関数の性質です．まず，f:real->realがx:realにおいて連続であることは，中置き演算子 cont(locally continuous) により，f contl xと表され，thmとしては # REWRITE_CONV[contl]`f contl x`;; val it : thm = |- f contl x ( (\h. f (x + h) ) …