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