[isabelle] Fwd: Re: case rule and OF

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:

   assumes "p â (1::ennreal)"
   show foo
   using `p >= 1`
proof (cases rule: my_case_rule)

Hope this helps,

On 20/09/16 23:17, Esseger wrote:
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:

  assumes "p â (1::ennreal)"
  show foo
proof (rule my_case_rule[OF `p â 1`])
  case one
  then show ?thesis sorry
  case (gr p2)
  then show ?thesis sorry
  case PInf
  then show ?thesis sorry

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.