*To*: Esseger <esseger at free.fr>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] case rule and OF*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 21 Sep 2016 09:10:47 +0200*In-reply-to*: <32bcd7af-c774-d5b3-817f-de4473e28a45@free.fr>*References*: <nrs919$s9n$1@blaine.gmane.org> <f391a3bc-dcd2-6db6-f116-435a8068ceaf@inf.ethz.ch> <32bcd7af-c774-d5b3-817f-de4473e28a45@free.fr>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

Dear Esseger,

Andreas On 21/09/16 09:01, Esseger wrote:

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 Le 21/09/2016 Ã 08:23, Andreas Lochbihler a Ãcrit :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 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: 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

**Follow-Ups**:**Re: [isabelle] case rule and OF***From:*Esseger

**References**:**[isabelle] case rule and OF***From:*Esseger

- Previous by Date: Re: [isabelle] case rule and OF
- Next by Date: [isabelle] Fwd: Re: case rule and OF
- Previous by Thread: Re: [isabelle] case rule and OF
- Next by Thread: Re: [isabelle] case rule and OF
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list