Email Gateway (Aug 19 2022 at 17:24): Email Gateway (Aug 19 2022 at 17:24):From: "W. Douglas Maurer" <maurer@gwu.edu>
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
Email Gateway (Aug 19 2022 at 17:24):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear W. Douglas Maurer,
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.
it suffices if you add associativity:
lemma "f(m+int(z+1)) = f(m+int(z)+1)" by (simp add: ac_simps)
Best,
René
Last updated: Apr 25 2024 at 16:19 UTC