# Re: [isabelle] Problem with Int.int_ge_induct

• 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
• 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",
```
```
```
How can I tell that the rule involves (0 :: int)? Is there some construction in Isar that I can use, to find this out?
```
```
```so it can be discharged by simp.
```
```
I tried discharging this by writing:
have 5: "(0 :: int) <= 0" by simp
```
I tried this just before, and also just after, the step starting with "from 1 and 2 and 3". In both cases I still get the same message on "by (rule Int.int_ge_induct)", namely
```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
end
```
```The standard way of applying this induction rule would be:

lemma
fixes x :: int
assumes "0 ? x"
shows "x ? x * x"
using assms
```
```
```
I've never needed "using assms" before, and its position in this proof confuses me. "Programming and Proving in Isabelle/HOL" (prog_prove) states (p. 43): "There are two further linguistic variations: (have|show) prop using facts = from facts (have|show) prop...The 'using' idiom de-emphasizes the used facts by moving them behind the proposition." This, however, is for "using" within a proof, not before the word "proof." Then (pp. 43-44), fixes-assumes-shows is introduced, with the meaning of assms; but there is no reference here to "using" immediately after fixes-assumes-shows and before "proof." No further occurrences of "using" in prog_prove involve "using" before the word "proof." Is there a better writeup which explains this?
```
```
```proof (induct x rule: Int.int_ge_induct)
case base then show ?case by simp
```
```
```
In this particular proof, the base case is the case "x=0". However, Int.int_ge_induct also works for proofs with other base cases. If I were to prove something with base case "x=1", would I still be able to write "case base then show" here? Or would I write something slightly different? Or would I have to spell out assumptions and conclusions, as you have done below?
```
```
```next
case (step i) then show ?case by simp
qed
```
```
```
You appear, here, to be making use of "base" and "step" as what I believe are called minor keywords within the case construction. Where are minor keywords (if that's what they're called) defined?
```
```
```
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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.