*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problem with Int.int_ge_induct*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Tue, 14 Apr 2015 07:40:33 +0200*In-reply-to*: <a06200702d1523c435cee@[192.168.1.6]>*References*: <a06200702d1523c435cee@[192.168.1.6]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.6.0

On 14.04.2015 06:40, W. Douglas Maurer wrote: > 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). By default, Isabelle does not print the types (and in 2014, it also does not show them on hovering in the output, unfortunately), but your goal is indeed "(0 :: int) <= 0", so it can be discharged by simp. You get these goals, because of the way rule works, you still need to discharge the assumptions of 2, 3 after rule application. As you don't need the assumption in 2, just get rid of it. BTW, 3 is easily proved by simp. > 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 The standard way of applying this induction rule would be: lemma fixes x :: int assumes "0 â x" shows "x â x * x" using assms proof (induct x rule: Int.int_ge_induct) case base then show ?case by simp next case (step i) then show ?case by simp qed or -- if you prefer to spell out assumptions and conclusions (which I guess makes sense for teaching): lemma fixes x :: int assumes "0 â x" shows "x â x * x" using assms proof (induct x rule: Int.int_ge_induct) show "(0 :: int) â 0 * 0" by simp next fix i :: int assume "0 â i" "i â i * i" then show "i + 1 â (i + 1) * (i + 1)" by simp qed Even if you don't want your students to use the induct method, I would still suggest to use a structured proof: lemma fixes x :: int assumes "0 â x" shows "x â x * x" using assms proof (rule Int.int_ge_induct) show "(0 :: int) â 0 * 0" by simp next fix i :: int assume "0 â i" "i â i * i" then show "i + 1 â (i + 1) * (i + 1)" by simp qed Which looks almost the same here as the one using the induction method. But this will change once the goals get more complex. > 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 No :) -- Lars

**References**:**[isabelle] Problem with Int.int_ge_induct***From:*W. Douglas Maurer

- Previous by Date: [isabelle] Problem with Int.int_ge_induct
- Next by Date: Re: [isabelle] Isabelle2015-RC0 ML ATP_Util.unyxml
- Previous by Thread: [isabelle] Problem with Int.int_ge_induct
- Next by Thread: Re: [isabelle] Problem with Int.int_ge_induct
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list