[isabelle] case rule and OF

[Esseger]

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

[Esseger]

Sorry, of course I meant:

proof (cases rule: my_case_rule[OF `p ≥ 1`])

My problem is that the cases names are not respected with this construction.

Post by Esseger
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.
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
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

[Andreas Lochbihler]

Dear Esseger,

When you instantiate some premises of a rule with OF, all the case name information gets
erased (because it is not trivial to determine how they would have to be shifted).
However, you normally do not instantiate premises manually in case distinctions, but
appropriately declare the first n premises to be unified with the facts chained in using
the "consumes n" attribute. "lemma assumes ... obtains ..." implicitly sets "consumes"
appropriately. Hence, you merely have to chain in the necessary assumptions, as I had
shown in my example.

Andreas

Thanks for your answer, and sorry for my typo: I indeed meant
proof (cases rule: my_case_rule[OF `p ≥ 1`])
With this construction, the case names are not honored (while the construction you advocate
using `p >= 1` proof (cases rule: my_case_rule)
works fine)
Best,
Esseger

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
lemma
assumes "p ≥ (1::ennreal)"
show foo
using `p >= 1`
proof (cases rule: my_case_rule)
Hope this helps,
Andreas

Post by Esseger
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.
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
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

[Esseger]

Post by Andreas Lochbihler
When you instantiate some premises of a rule with OF, all the case name
information gets erased (because it is not trivial to determine how they
would have to be shifted). However, you normally do not instantiate
premises manually in case distinctions, but appropriately declare the
first n premises to be unified with the facts chained in using the
"consumes n" attribute. "lemma assumes ... obtains ..." implicitly sets
"consumes" appropriately. Hence, you merely have to chain in the
necessary assumptions, as I had shown in my example.

This is perfectly clear, thanks a lot for the explanations.

[Andreas Lochbihler]

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

Post by Esseger
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.
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
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