PVSのこと（６）

　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:lemma forall(a,b:int): b/=0 => exists(x:rat): x=a/b
numsys5:lemma forall(a,b:nat): exists(x:int): x=a-b
numsys6:lemma forall(a,b:int): b<=a => exists(x:nat): x=a-b
numsys7:lemma forall(a:nat): a - succ(a) = - 1

などがそのまま通ります．また，累乗の記号も定理を参照せず処理してくれますので，普通は帰納法で

ind1:lemma forall(n:nat):exists(x:nat): x * x <= n & n < succ(x) * succ(x)

%|- ind1 : PROOF
%|- (spread (induct "n")
%|-  ((then (inst?) (grind))
%|-   (then (skeep*)
%|-    (spread (case "j+1=succ(x) * succ(x)")
%|-     ((then (inst?) (grind)) (then (inst 2 "x") (grind)))))))
%|- QED

と済ませてしまうところを，それらしく

importing reals@sqrt
flr:lemma forall(n:int): 0 <= n => exists(x:int): x ^ 2 <= n & n < (x + 1) ^ 2

%|- flr : PROOF
%|- (then (skeep*)
%|-  (spread (inst 1 "floor(sqrt(n))")
%|-   ((spread (lemma "floor_def" ("x" "sqrt(n)"))
%|-     ((then (use "sq_sqrt")
%|-       (spread (use "sq_lt")
%|-        ((spread (use "sq_le") ((grind) (grind))) (grind))))
%|-      (grind)))
%|-    (grind))))
%|- QED

としても平易です．