*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isar-Level cases command*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 25 Nov 2014 12:39:42 +0100*In-reply-to*: <54745C6C.30602@inf.ethz.ch>*References*: <1416906951.1435.7.camel@kit.edu> <54745C6C.30602@inf.ethz.ch>

Hi, Am Dienstag, den 25.11.2014, 11:39 +0100 schrieb Andreas Lochbihler: > Personally, I do not mind having to state the "show ?case" part, because it makes clear > that you really need to do the case distinction to prove the whole case. In fact, I think > that your case distinction in the example is not as it should be, because you only need it > to for the unfolding of filter. True, in this sense the example is a bit lacking. And you are rightly pointing out that fact that for showing an intermediate statement using case distinction the current scheme is useful. So I would not go as far to expect that cases ("xs") case Nil have P next case (Cons x xs') have P qed to be equivalent to have P proof (cases "xs")) case Nil have P next case (Cons x xs') have P qed and hence (heh) suggest this feature only for the case (heh) where one or more actual subgoals are shown (heh) in each case (heh). (Although I would not dismiss the above if it turns out to be feasible). Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**References**:**[isabelle] Isar-Level cases command***From:*Joachim Breitner

**Re: [isabelle] Isar-Level cases command***From:*Andreas Lochbihler

- Previous by Date: [isabelle] 2-year postdoc position on security verification at TUM
- Next by Date: [isabelle] Define a fun
- Previous by Thread: Re: [isabelle] Isar-Level cases command
- Next by Thread: [isabelle] 2-year postdoc position on security verification at TUM
- Cl-isabelle-users November 2014 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