*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problem with Int.int_ge_induct*From*: "W. Douglas Maurer" <maurer at gwu.edu>*Date*: Wed, 15 Apr 2015 22:41:21 -0400*Cc*: maurer at gwu.edu*In-reply-to*: <mailman.33897.1429007609.13101.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.33897.1429007609.13101.cl-isabelle-users@lists.cam.ac.uk>

Message: 7 Date: Tue, 14 Apr 2015 07:40:33 +0200 From: Lars Noschinski <noschinl at in.tum.de> Subject: Re: [isabelle] Problem with Int.int_ge_induct To: cl-isabelle-users at lists.cam.ac.uk Message-ID: <552CA851.7000501 at in.tum.de> Content-Type: text/plain; charset=UTF-8 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.

I tried discharging this by writing: have 5: "(0 :: int) <= 0" by simp

Failed to finish proof: goal (1 subgoal): 1. 0 <= 0 Am I misunderstanding what "discharged" means?

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 endThe 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

(snip)

-- Lars

Thanks! -Douglas -- 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

**Follow-Ups**:**Re: [isabelle] Problem with Int.int_ge_induct***From:*Lars Noschinski

- Previous by Date: [isabelle] ASE 2015 - 30th IEEE/ACM International Conference on Automated Software Engineering
- Next by Date: Re: [isabelle] Isabelle2015-RC0 available for testing
- Previous by Thread: Re: [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