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