PVSのこと（８）

　PVS のプルーフマネージャは非常に上手く設計されており，ロジカルな展開で迷うことはまずありません．

lem0:lemma forall(a,b:real):(a/=0 or (a=0 & b=0)) <=> exists(x:real):a*x=b

%|- lem0 : PROOF
%|- (then (skeep)
%|-  (spread (split)
%|-   ((then (flatten)
%|-     (spread (split)
%|-      ((then (inst + "b/a") (ground)) (then (inst?) (ground)))))
%|-    (then (flatten) (ground)))))
%|- QED

lem0 :  

  |-------
{1}   FORALL (a, b: real):
        (a /= 0 OR (a = 0 & b = 0)) <=> (EXISTS (x: real): a * x = b)

Rerunning step: (skeep)
Skolemizing and keeping names of the universal formula in (+ -),
this simplifies to: 
lem0 :  

  |-------
{1}   (a /= 0 OR (a = 0 & b = 0)) <=> (EXISTS (x: real): a * x = b)

Rerunning step: (split)
Splitting conjunctions,
this yields  2 subgoals: 
lem0.1 :  

  |-------
{1}   (a /= 0 OR (a = 0 & b = 0)) IMPLIES (EXISTS (x: real): a * x = b)

Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
lem0.1 :  

{-1}  (a /= 0 OR (a = 0 & b = 0))
  |-------
{1}   EXISTS (x: real): a * x = b

Rerunning step: (split)
Splitting conjunctions,
this yields  2 subgoals: 
lem0.1.1 :  

{-1}  a /= 0
  |-------
[1]   EXISTS (x: real): a * x = b

Rerunning step: (inst + "b/a")
Instantiating the top quantifier in + with the terms: 
 b/a,
this simplifies to: 
lem0.1.1 :  

[-1]  a /= 0
  |-------
{1}   a * (b / a) = b

Rerunning step: (ground)
Applying propositional simplification and decision procedures,

This completes the proof of lem0.1.1.

lem0.1.2 :  

{-1}  (a = 0 & b = 0)
  |-------
[1]   EXISTS (x: real): a * x = b

Rerunning step: (inst?)
Found substitution:
x: real gets a,
Using template: x
Instantiating quantified variables,
this simplifies to: 
lem0.1.2 :  

[-1]  (a = 0 & b = 0)
  |-------
{1}   a * a = b

Rerunning step: (ground)
Applying propositional simplification and decision procedures,

This completes the proof of lem0.1.2.


This completes the proof of lem0.1.

lem0.2 :  

  |-------
{1}   (EXISTS (x: real): a * x = b) IMPLIES (a /= 0 OR (a = 0 & b = 0))

Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
lem0.2 :  

{-1}  EXISTS (x: real): a * x = b
{-2}  a = 0
  |-------
{1}   (a = 0 & b = 0)

Rerunning step: (ground)
Applying propositional simplification and decision procedures,

This completes the proof of lem0.2.

Q.E.D.




Run time  = 0.05 secs.
Real time = 0.19 secs.