PVSのこと（９）
以前 Isar で書いた自然数の分解 http://d.hatena.ne.jp/ehito/20130514/1368492752 の PVS 版です．
lem_odd_even:lemma forall(n:nat):(n=0 or exists(x:posint,y:nat):odd?(x) & n=x*2^y) %|- lem_odd_even : PROOF %|- (then (induct "n" 1 "NAT_induction") (skeep*) %|- (spread (case "odd?(j)") %|- ((spread (inst 2 "j" "0") ((grind) (grind))) %|- (then (rewrite "odd_iff_not_even") (expand "even?" -1) (skeep*) %|- (spread (inst -2 "j_1") %|- ((then (ground) (skeep*) (replace -2 * LR) (inst 2 "x" "1+y") %|- (grind)) %|- (grind))))))) %|- QED
lem_odd_even :
|-------
{1} FORALL (n: nat):
(n = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & n = x * 2 ^ y))
Rerunning step: (induct "n" 1 "NAT_induction")
Inducting on n on formula 1 using induction scheme NAT_induction,
this simplifies to:
lem_odd_even :
|-------
{1} FORALL j:
(FORALL k:
k < j IMPLIES
(k = 0 OR
(EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y)))
IMPLIES
(j = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y))
Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to:
lem_odd_even :
{-1} FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
{1} j = 0
{2} EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (case "odd?(j)")
Case splitting on
odd?(j),
this yields 2 subgoals:
lem_odd_even.1 :
{-1} odd?(j)
[-2] FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
[1] j = 0
[2] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (inst 2 "j" "0")
Instantiating the top quantifier in 2 with the terms:
j, 0,
this yields 2 subgoals:
lem_odd_even.1.1 :
[-1] odd?(j)
[-2] FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
[1] j = 0
{2} odd?(j) & j = j * 2 ^ 0
Rerunning step: (grind)
odd? rewrites odd?(j)
to EXISTS (j_1: int): j = 1 + 2 * j_1
expt rewrites expt(2, 0)
to 1
^ rewrites 2 ^ 0
to 1
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of lem_odd_even.1.1.
lem_odd_even.1.2 (TCC):
[-1] odd?(j)
[-2] FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
{1} j > 0
[2] j = 0
Rerunning step: (grind)
odd? rewrites odd?(j)
to FALSE
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of lem_odd_even.1.2.
This completes the proof of lem_odd_even.1.
lem_odd_even.2 :
[-1] FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
{1} odd?(j)
[2] j = 0
[3] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (rewrite "odd_iff_not_even")
Found matching substitution:
x: int gets j,
Rewriting using odd_iff_not_even, matching in *,
this simplifies to:
lem_odd_even.2 :
{-1} even?(j)
[-2] FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
[1] j = 0
[2] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (expand "even?" -1)
Expanding the definition of even?,
this simplifies to:
lem_odd_even.2 :
{-1} EXISTS (j_1: int): j = 2 * j_1
[-2] FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
[1] j = 0
[2] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (skeep -1)
Skolemizing and keeping names of the universal formula in -1,
this simplifies to:
lem_odd_even.2 :
{-1} j = 2 * j_1
[-2] FORALL k:
k < j IMPLIES
(k = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & k = x * 2 ^ y))
|-------
[1] j = 0
[2] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (inst -2 "j_1")
Instantiating the top quantifier in -2 with the terms:
j_1,
this yields 2 subgoals:
lem_odd_even.2.1 :
[-1] j = 2 * j_1
{-2} j_1 < j IMPLIES
(j_1 = 0 OR (EXISTS (x: posint, y: nat): odd?(x) & j_1 = x * 2 ^ y))
|-------
[1] j = 0
[2] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (ground)
Applying propositional simplification and decision procedures,
this simplifies to:
lem_odd_even.2.1 :
{-1} EXISTS (x: posint, y: nat): odd?(x) & j_1 = x * 2 ^ y
[-2] j = 2 * j_1
|-------
[1] j = 0
[2] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to:
lem_odd_even.2.1 :
{-1} odd?(x)
{-2} j_1 = x * 2 ^ y
{-3} j = 2 * j_1
|-------
{1} j = 0
{2} EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (replace -2 * LR)
Replacing using formula -2,
this simplifies to:
lem_odd_even.2.1 :
[-1] odd?(x)
[-2] j_1 = x * 2 ^ y
{-3} j = 2 * (x * 2 ^ y)
|-------
[1] j = 0
[2] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (inst 2 "x" "1+y")
Instantiating the top quantifier in 2 with the terms:
x, 1+y,
this simplifies to:
lem_odd_even.2.1 :
[-1] odd?(x)
[-2] j_1 = x * 2 ^ y
[-3] j = 2 * (x * 2 ^ y)
|-------
[1] j = 0
{2} odd?(x) & j = x * 2 ^ (1 + y)
Rerunning step: (grind)
odd? rewrites odd?(x)
to EXISTS j: x = 1 + 2 * j
^ rewrites 2 ^ y
to expt(2, y)
expt rewrites expt(2, 1 + y)
to 2 * expt(2, y)
^ rewrites 2 ^ (1 + y)
to 2 * expt(2, y)
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of lem_odd_even.2.1.
lem_odd_even.2.2 (TCC):
[-1] j = 2 * j_1
|-------
{1} j_1 >= 0
[2] j = 0
[3] EXISTS (x: posint, y: nat): odd?(x) & j = x * 2 ^ y
Rerunning step: (grind)
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of lem_odd_even.2.2.
This completes the proof of lem_odd_even.2.
Q.E.D.
Run time = 0.18 secs.
Real time = 0.49 secs.
