等差数列の和の公式の証明です． :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を満たす元があるならその一つ（何れかは不…

■ HOL Lightにおいては，集合は，述語と見做せるよう定義されています． let IN = new_definition `!P:A->bool. !x. x IN P P x`;; ■ 集合のconstantには (typ) (typは:num，:realなどのhol.type) EMPTY or {} UNIV があり，UNIVは # `x+ &1 IN UNIV`;; val …