2013-04-01から1ヶ月間の記事一覧
let lem1 = SIMP_RULE [REAL_POW2_ABS; REAL_INJ; REAL_MUL] (REAL_FIELD `~(&q = &0) ==> abs x = &p / &q ==> ~(&(gcd (p,q)) = &0) ==> &p = &a' * &(gcd (p,q)) ==> &q = &b' * &(gcd (p,q)) ==> &a' * &a' = abs x pow 2 * &b' * &b'`);; let RATIONAL_…
以下，表題の証明です． # g `!s. prime s ==> ~rational (sqrt (&s))` ;; val it : goalstack = 1 subgoal (1 total) `!s. prime s ==> ~rational (sqrt (&s))` まず，全称量化を外し，前件を仮定に廻して，結論を（その１）の定理でリライトします． # e( …
前回の性質を少し一般化したものの tactics による証明です．まず（その１）として，有理数が既約分数で表せることを定理にしておきます． # g `!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`;; val it : goalstack = 1 subgoa…
チュートリアルにもありますが，以下は既存の定理や補題を統合する，普通の数学と同じ流儀の証明です． let lem1 = PV9[SQRT_POS_LT; REAL_POS_NZ; ARITH; REAL_LT ]`~(sqrt (&2) = &0)`;; let lem2 = MESON[REAL_INV_0; REAL_FIELD`~(x / y = &0) ==> ~(x =…
次に全称量化をとるまえの状態に戻します． e( GEN_TAC );; すると val it : goalstack = 1 subgoal (1 total) `m = 0 \/ 3 EXP m MOD 3 = 0` のように !m. が付かないものが改めて目標（サブゴール）となります．さて，この式を証明するには，明らかにmが0…
では証明を書いていきましょう．簡単過ぎるのもおもしろくないので 任意の自然数 m に対して m=0 または 3^mを3で割った余りが0 の証明からはじめます．まずこれを論理式に直して，目標（ゴール）に設定します． g `!m. m = 0 \/ 3 EXP m MOD 3 = 0`;; g と…
先ほどの hol_light フォルダーにおいて， rlwrap -r ocaml と入力すると Objective Caml version 3.11.2 # のようにOCamelのインタープリタが起動するので，プロンプトに #use"hol.ml";; と（ # 記号も）入力，しばし待てば Camlp5 Parsing version 5.14 # …
新年度ということで，従来の内容に加え，これから HOL Light を始める方に向けた記事も書いていきます．プラットフォームは，Linux（MS-Windowsの方は http://d.hatena.ne.jp/ehito/20110203/1296713729 を参考にしてください）とします．まず，ターミナルを…
例えば # REAL_NEG_MINUS1;; val it : thm = |- !x. --x = -- &1 * x を `-- x` に適用しようと # REWRITE_CONV [REAL_NEG_MINUS1] `-- x`;; としても．．．帰ってきません．これは等式の右辺の -- &1 にも同じ書き換えが適用され，ループに陥っている為です…
前回の lem03 にあるように，REAL/COMPLEX_FIELD が知っているのは有理式までなので，それ以外のものを扱うには，必要な性質を前件として与えて証明させた後，SIMP,REWRITEなどにより前件を消去します． SIMP_RULE[COMPLEX_POW_II_2; GSYM CX_POW; SQRT_POW_…
幾何的に考えるまでもなく，等比数列と１の６乗根を用いればよいでしょう．数学としては位数６の巡回群の生成元を地道に求めさせる問題です．まずは帰納法で一般項を準備します． let lem01 = prove ( `z 0 = Cx(&1) /\ (!n. z (SUC n) = c * z n) ==> !n. c…
needs "Multivariate/transcendentals.ml";; needs "Examples/prover9_win.ml";; needs "Examples/sos_win.ml";; let lem01 = prove (`z 0 = Cx(&1) /\ (!n. z (SUC n) = c * z n) ==> (!n. z n = c pow n)`, STRIP_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[c…
