# [isabelle] Fwd: Re: case rule and OF

• To: isabelle-users <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] Fwd: Re: case rule and OF
• From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
• Date: Wed, 21 Sep 2016 09:11:09 +0200
• References: <f391a3bc-dcd2-6db6-f116-435a8068ceaf@inf.ethz.ch>
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

```Dear Esseger,

```
Case names as specified for rules are only honored by the proof methods "cases", "induct" and "coinduct" (and their derivatives "induction" and "coinduction"), but not plain "rule". Your rule "my_case_rule" should work if you use "cases" (which is the appropriate method here, because you are doing a case distinction). So, the following should do the job:
```
lemma
assumes "p â (1::ennreal)"
show foo
using `p >= 1`
proof (cases rule: my_case_rule)

Hope this helps,
Andreas

On 20/09/16 23:17, Esseger wrote:
```
```Dear all,

I am trying to set a convenient case rule, to distinguish if, given a parameter p â 1 in
ennreal, it is equal to 1, or between 1 and infinity, or infinite. When it is strictly
between 1 and infinity,
I would also like p to be written as p = ennreal p2, for some real number p2.

I would like to use it as:

lemma
assumes "p â (1::ennreal)"
show foo
proof (rule my_case_rule[OF `p â 1`])
case one
then show ?thesis sorry
next
case (gr p2)
then show ?thesis sorry
next
case PInf
then show ?thesis sorry
qed

I tried to define my rule as:

lemma my_case_rule:
assumes "p â (1::ennreal)"
obtains (gr) p2 where "p = ennreal p2" "p2 > 1"
| (one) "p = 1"
| (PInf) "p = â"
using assms by (metis (full_types) antisym_conv ennreal_cases ennreal_le_1
infinity_ennreal_def not_le)

It doesn't work, as the names of the cases are not respected, replacing them with the
names 1, 2, 3 (with which I can write the proofs, for sure, but this is much harder to read).

I tried several modifications of the rule to keep the names, with modifiers such as
case_names or consumes, to no avail. I could not locate in the reference manual any hint
on the canonical way to write this kind of thing. Any help on the best practice in this
situation?

Best,
Esseger

```
```

```

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