Wellfounded induction（２）

http://d.hatena.ne.jp/ehito/20111119/1321692292 のPVS版です．

lem00:lemma
  FORALL (p: pred [nat]):
    (FORALL (n: nat):
       (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n))
     IMPLIES (FORALL (n: nat): p(n))

%|- lem00 : PROOF
%|- (then (skeep*) (copy -1) (inst -2 "n")
%|-  (spread (split -2)
%|-   ((propax)
%|-    (then (generalize "n" "n" nat 1)
%|-     (spread (induct "n" 1)
%|-      ((ground)
%|-       (then (skeep*) (inst -3 "k")
%|-        (spread (case "k=j or k<j") ((grind) (grind))))))))))
%|- QED


lem00 :  

  |-------
{1}   FORALL (p: pred[nat]):
        (FORALL (n: nat):
           (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n))
         IMPLIES (FORALL (n: nat): p(n))

Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to: 
lem00 :  

{-1}  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
{1}   p(n)

Rerunning step: (copy -1)
Copying formula number: -1
this simplifies to: 
lem00 :  

{-1}  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
[-2]  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
[1]   p(n)

Rerunning step: (inst -2 "n")
Instantiating the top quantifier in -2 with the terms: 
 n,
this simplifies to: 
lem00 :  

[-1]  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
{-2}  (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
[1]   p(n)

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

{-1}  p(n)
[-2]  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
[1]   p(n)

which is trivially true.

This completes the proof of lem00.1.

lem00.2 :  

[-1]  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
{1}   FORALL (k: nat): k < n IMPLIES p(k)
[2]   p(n)

Rerunning step: (generalize "n" "n" nat 1)
Generalizing n by n,
this simplifies to: 
lem00.2 :  

[-1]  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
{1}   FORALL (n: nat), (k: nat): k < n IMPLIES p(k)
[2]   p(n)

Rerunning step: (induct "n" 1)
Inducting on n on formula 1,
this yields  2 subgoals: 
lem00.2.1 :  

[-1]  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
{1}   FORALL (k: nat): k < 0 IMPLIES p(k)
[2]   p(n)

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

This completes the proof of lem00.2.1.

lem00.2.2 :  

[-1]  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
{1}   FORALL j:
        (FORALL (k: nat): k < j IMPLIES p(k)) IMPLIES
         (FORALL (k: nat): k < j + 1 IMPLIES p(k))
[2]   p(n)

Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to: 
lem00.2.2 :  

{-1}  FORALL (k: nat): k < j IMPLIES p(k)
{-2}  k < j + 1
{-3}  FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)
  |-------
{1}   p(k)
{2}   p(n)

Rerunning step: (inst -3 "k")
Instantiating the top quantifier in -3 with the terms: 
 k,
this simplifies to: 
lem00.2.2 :  

[-1]  FORALL (k: nat): k < j IMPLIES p(k)
[-2]  k < j + 1
{-3}  (FORALL (k_1: nat): k_1 < k IMPLIES p(k_1)) IMPLIES p(k)
  |-------
[1]   p(k)
[2]   p(n)

Rerunning step: (case "k=j or k<j")
Case splitting on 
   k = j OR k < j, 
this yields  2 subgoals: 
lem00.2.2.1 :  

{-1}  k = j OR k < j
[-2]  FORALL (k: nat): k < j IMPLIES p(k)
[-3]  k < j + 1
[-4]  (FORALL (k_1: nat): k_1 < k IMPLIES p(k_1)) IMPLIES p(k)
  |-------
[1]   p(k)
[2]   p(n)

Rerunning step: (grind)
Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of lem00.2.2.1.

lem00.2.2.2 :  

[-1]  FORALL (k: nat): k < j IMPLIES p(k)
[-2]  k < j + 1
[-3]  (FORALL (k_1: nat): k_1 < k IMPLIES p(k_1)) IMPLIES p(k)
  |-------
{1}   k = j OR k < j
[2]   p(k)
[3]   p(n)

Rerunning step: (grind)
Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of lem00.2.2.2.


This completes the proof of lem00.2.2.


This completes the proof of lem00.2.

Q.E.D.