[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

lemma,inst? and replace



Hello

After defining a transitive relationship in succ_ax:

role : TYPE

succT : TYPE = PRED[[role,role]]

succ : succT

succ_ax : AXIOM 
  FORALL(x:role,y:role,z:role) :
   (succ(x,y) AND succ(y,z))  = succ(x,z)

I prove the first part of:

x1 : THEOREM
  reduce(succ(U,M) AND succ(M,N) AND succ(N,O), succ(U,O))

using 

(then (use "succ_ax")(replace -1 * lr)(delete -1))

which after several iterations of the above prover command looks like:


x1 :  

  |-------
[1]    reduce(succ(U, o), succ(U, o))

which I complete with another axiom.

I then repeat the theorem with a few terms in different order:

x2 : THEOREM
  reduce(succ(U,M) AND succ(N,O) AND succ(M,N), succ(U,O))

The (use "succ_ax")  [ as (lemma "succ_ax")(inst?)(inst?) ]
correctly identifies the assignment of variables in the axiom 
creating:

x2 :  

{-1}    (succ(U, M) AND succ(M, N)) = succ(U, N)
  |-------
[1]    reduce(succ(U, M) AND succ(N, o) AND succ(M, N), succ(U, o))

But in this case (replace -1 *  lr) fails.  I presume because (inst?)
looked into the structure of the formula where as (replace) does a
simple left to right scan.  But, intuition says that if (inst?) can do
the variable mapping correctly why can (replace) not take advantage of
it?

Does anyone have an ideas how to approach this simple sounding problem? 
It is not that this simple example cannot be restructured to match the
power of (replace) but the intended later use will be in a much more
complicated formula which would be very ackward to continually
rearrange.


thanks 

bill