[isabelle] Problem with Int.int_ge_induct



From my previous posts you may be aware that I am still looking for the best possible way to do the kind of mathematical induction that is typically taught first in a course on discrete mathematics. After looking over the various replies I have gotten, I would like very much, for most of this, to use Int.int_ge_induct: "?k <= ?i ==> ?P ?k ==> (!!i. ?k <= i ==> ?P i ==> ?P (i + 1)) ==> ?P ?i". This assumes that the induction variable is an int, not a nat, so inductions starting at negative numbers can be covered, as well as numbers greater than zero. It can also be applied to course-of-values induction. Having made this decision, I now tried a very simple case, namely proving by induction that if x >= 0, then x <= x*x. Most of what Int.int_ge_induct is supposed to be doing seems to be working fine, but, at the end, I am getting the message: "Failed to finish proof: goal (1 subgoal): 1. 0 <= 0". Well, it's true that (0::int) <= 0 would be true by simp, but 0 <= 0 is not (and it makes sense to me that it is not, since 0 might be a label, for instance). But my question now is: Why am I getting 0 <= 0 in that form? Here is my proof, in which I have replaced every occurrence of 0 by (0::int), in order to try (unsuccessfully) to stop generating a subgoal involving 0 rather than 0::int:
theory IntInduct imports Main begin
lemma "[|x >= (0::int)|] ==> (x::int) <= x*x" proof-
assume "x >= (0::int)"
then have 1: "(0::int) <= x" by simp
have 2: "[|(0::int) <= (0::int)|] ==> (0::int) <= (0::int)*(0::int)" by simp
have 3: "!!i. (0::int) <= i ==> (i::int) <= i*i ==> (i::int)+1 <= (i+1)*(i+1)" sorry
from 1 and 2 and 3 show "(x::int) <= x*x" by (rule Int.int_ge_induct)
qed
end
I have also tried this starting with lemma fixes x::int assumes 4: "x >= (0::int)" shows "x <= x*x" proof- from 4 have 1: "(0::int) <= x" by simp
with the same result. -Douglas
P. S. Might there be a problem with Int.int_ge_induct having a variable called ?i and a (presumably different) bound variable called i? -WDM
--
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.