# [isabelle] case rule and OF

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