sqrtp:theory begin importing ints@primes, ints@gcd, reals@sqrt lem1:lemma forall(p:int): prime?(p) => (exists(n:posint): p = n * n) => False %|- lem1 : PROOF %|- (then (skeep*) %|- (spread (case "divides (n,p)") %|- ((then (expand "prime?"…

HOL系と異なり，PVS の number system は数学と同じく，サブセットからなっていますので numsys1:lemma forall(a:nat): exists(x:real): x=a numsys2:lemma forall(a:nat): exists(x:rat): x=a numsys3:lemma forall(a:nat): exists(x:int): x=a numsys4:lem…

prob10:theory begin for_a:lemma forall(a:posreal,b:posreal,c:int,m:int,n:int):1 / a + 1 / b = 1 => c <= m * a & m * a < c + 1 => c <= n * b & n * b < c + 1 => c = m * a %|- for_a : PROOF %|- (then (skeep) %|- (spread (case "c < m * a") %|-…

theory prob10 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin lemma for_a: fixes a b :: real and c m n :: int assumes "0 < a" and "0 < b" and "1 / a + 1 / b = 1" assumes "c <= m * a" and "m * a < c + 1" assumes "c <= n * b" an…

定理自体はともかく，an_am_coprime の "0" の証明に even_zero_int 等を持ち出さないあたり，さすが metis といったところでしょう． theory prob01 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin fun a :: "nat => int" where "a 0 = 3" …

(grind) は中々です．pvsファイル nnseq:theory begin importing reals@sigma_nat a:[nat->nnreal] n:nat lem01:lemma sigma(0,n,a)>=0 lem02:lemma sigma(0,n,a)=0 => a(n)=0 %|- lem0* : PROOF %|- (grind) %|- QED end nnseq ＊PVS＊バッファ pvs(1160): …

PVS は LK を素直にインプリメントしており，否定は直ちにシーケントの対辺に移されます．これは数についての等式において移項により辺々を和の形に直すことに相当します．また，SUBGOALの導入・証明は，本来の case として (P ∨ ¬P),S ==> T が P,S ==> T …

一般項が分数である数列の和です．NASA製の (grind-reals) が要です．pvsファイル frseq:theory begin importing reals@sigma_posnat lem01:lemma FORALL (n: posnat): sigma(1, n, (LAMBDA (k: posnat): 1 / (k * (k + 1)))) = n / (n + 1) %|- lem01 : PRO…

数学的帰納法の例です． lem002 : |------- {1} FORALL (n: nat, x: real): x ^ n = 0 => x = 0 Rerunning step: (induct "n") Inducting on n on formula 1, this yields 2 subgoals: lem002.1 : |------- {1} FORALL (x: real): x ^ 0 = 0 => x = 0 Rerunn…

と言うわけで，暫くは PVS のことを書きます．PVS はSRI(スタンフォード)で90年代初めより開発が進められている対話的定理証明システムで，LK が素直にインプリメントされており論理記号の消去は極めて平易に行えるのですが，ground，grind，assertといった…

Paulson 教授の MetiTarski の組み込みは当然 Isabelle が最初になると思っていたのですが，13日に更新されたNASAのPVSライブラリーhttp://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/nasalib-6.0.5-full.tgzに先を越されてしまいました．出所はお弟子…

HOL Light の g コマンドによる証明と prove コマンドによる証明との変換ツール Tactician のご紹介です．http://www.proof-technologies.com/tactician/index.html 使い方は簡単で，HOL Light のディレクトリにhttp://www.proof-technologies.com/tactician…

ネットで参照できる Isabelle の解説は非常に充実していますが，日本語となると数える程しかありません．スライドでないものだと，ちょっと古いですが．．． http://www.ieice-hbkb.org/files/07/07gun_01hen_02.pdf http://www.score.is.tsukuba.ac.jp/~min…

これも HOL Light で書いた定理ですが，Isar では．．． theory convex imports Complex_Main begin theorem convex: fixes a b :: real and n :: nat assumes "0 <= a" and "0 <= b" shows "((a + b) / 2) ^ n <= (a ^ n + b ^ n) / 2" (is "?L n <= ?R n")…

いわゆる one line proof です． lemma "(f::nat⇒real) 0 < 0 ==> ∃n. 0 ≦ f n ==> ∃n. f n < 0 ∧ 0 ≦ f (Suc n)" by (metis nat_induct [of "%n. f n < 0"] not_le) 参照している定理は thm nat_induct [of "%n. f n f 0 (¬ ?x ≤ ?y) = (?y の２つですが，Z…

以前，HOL Light で書いた定理ですが，Isar では．．． lemma fixes f :: "nat ⇒ real" assumes "f 0 < 0" "∃n. 0 ≦ f n" shows "∃n. f n < 0 ∧ 0 ≦ f (Suc n)" proof (rule ccontr) assume 1: "¬ ?thesis" {fix n have "f n < 0" proof (induct n) show "f …