今回は次を証明します． 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) ) …

今回は分数不等式についての証明です． 4変数の3次分数式は，CADによるQEでは難しいようです． Reduce[ForAll[ {a, b, c, d}, a >= 0 && b >= 0 && c >= 0 && d >= 0 && a + b + c + d == 4, a/(a^3 + 8) + b/(b^3 + 8) + c/(c^3 + 8) + d/(d^3 + 8) ... 一…

チェビシェフの多項式を書き下すことは難しくありません．まず，引数の処理に用いる，2以上の整数をn+2の形に書き換えるconvを作ります． let NUM_ADD2_CONV = let add_tm = `(+):num->num->num` and two_tm = `2` in fun tm -> let m = mk_numeral(dest_num…

先に定義したチェビシェフの多項式が定める関数による[-1,1]の像が[-1,1]に含まれることは，余弦の逆関数 # ACS;; val it : thm = |- !y. -- &1 ==> &0 acs y /\ acs y acs y) = y についての # ACS_COS;; val it : thm = |- !y. -- &1 cos (acs y) = y から…

では，証明です． # g `!n:num x:real. cheb n (cos(x)) = cos*1 /\ (!x. cheb 1 (cos x) = cos (&1 * x)) /\ (!n. (!x. cheb n (cos x) = cos (&n * x)) /\ (!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)) ==> (!x. cheb (n + 2) (cos x) = cos (&(n + 2…

次の２つのパッケージの使用例を示します．OCamlの#useの代わりに，HOL Lightのneedsを使うとファイルのリロードが防げます． needs "Library/analysis.ml";; needs "Library/transc.ml";; まずは，チェビシェフの多項式 # let cheb = define `(!x. cheb 0 x…

今回は，任意の集合Aについて，その冪集合2^AからAへの単射が存在しないこと(Cantor)の証明です． 先に示した単射による基数の大小関係の特徴付け # let INJECTIVE_IFF_LEFT_INVERSE = MESON[ MESON`(!a1:A a2:A. f(a1)=f(a2) ==> a1=a2) (!b:B. ?a1:A. !a2:…

等差数列の和の公式の証明です． :num 版 # g`(?a b. !n. x n = a * n + b)==>(!n m. 2 * nsum(m..m+n) x = (SUC n)*( x m + x (m+n) ) )`;; Warning: Free variables in goal: x val it : goalstack = 1 subgoal (1 total)`(?a b. !n. x n = a * n + b) ==>…

今回は，分数関数の和の例です．キーとなるthmは，:realの元の和sumについての # SUM_CLAUSES_NUMSEG;; val it : thm = |- (!m. sum (m..0) f = (if m = 0 then f 0 else &0)) /\ (!m n. sum (m..SUC n) f = (if m です． 先に述べたmからの帰納法，INDUCTm_…

前節の基数の大小関係の2通りの特徴付けのうち，単射Ｎ×Ｎ→Ｎの存在を示して，|Ｎ×Ｎ|≦|Ｎ|を確かめましょう．実際 # let cantor = new_definition `cantor(x,y) = ((x + y) EXP 2 + 3 * x + y) DIV 2`;; val cantor : thm = |- !x y. cantor (x,y) = ((x + …

20世紀の数学の中で最も劇的な進展は，無限集合の体系的利用でしょう．その基礎は，濃度（基数）と順序数の概念です．それらは有限集合の大きさの数え上げと比較のアイデアを無限集合に拡張したものです．■ まず，述語 FINITE で特徴付けられる，有限集合に…

これまで述べなかった述語あるいは集合に対する作用子の一つとして，選択関数@(:(A->bool)->bool)があります．それは，!や?と同じくbinder（従って，括弧付きで用いられるもの）であり，述語 P に対して (@)P は，Pを満たす元があるならその一つ（何れかは不…