Esseger

2016-09-20 21:23:52 UTC

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

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