# [isabelle] f(m+int(z+1)) = f(m+int(z)+1)

`I am trying to prove that f(m+int(z+1)) = f(m+int(z)+1). Here z must
``be of type nat, since it is an argument of the int function; m must
``be of type int, since it is added to int(z+1); and f must be of type
``int=>'a, since its arguments are of type int. When I enter:
`lemma "f(m+int(z+1)) = f(m+int(z)+1)" try0

`the output window says: No proof found. But there must be a simple
``proof of this somewhere, because, when I ask if the two arguments of
``f are equal, like this:
`lemma "(m+int(z+1)) = (m+int(z)+1)" try0

`then that is true by simp. Surely if e1=e2, then we must have
``f(e1)=f(e2); indeed, if I enter:
`lemma "[|(e1::int)=e2|] ==> f(e1)=f(e2)" try0

`then that is also true by simp. I have been able to prove other facts
``of the form (e1=e2 implies f(e1)=f(e2)) directly; for example, if I
``enter
`lemma "f(m+int(Suc z)) = f(m+int(z+1))" try0
then that is again true by simp.

`I have not used Find Theorems before, and perhaps I am misusing it.
``When I enter:
`"f(_) = f(_)"
into the Find window, it says: Found nothing. When I enter:
"_(_) = _(_)"
into the Find window, it says: Found 6934 theorem(s). When I enter:
"_(_+_) = _(_+_)"

`into the Find window, it says: Found 17 theorem(s); but I checked all
``17, and none of them seem to be relevant.
`Any help will be appreciated. Thanks! -WDMaurer
--
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*