Re: [isabelle] case rule and OF



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.



Le 20/09/2016 Ã 23:17, Esseger a Ãcrit :
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










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