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