[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.