*To*: Joachim Breitner <breitner at kit.edu>, Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Isar-Level cases command*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Tue, 25 Nov 2014 10:51:00 +0100*In-reply-to*: <1416906951.1435.7.camel@kit.edu>*References*: <1416906951.1435.7.camel@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

lemma "length (filter P xs) ≤ length xs" proof (induction xs) case (Cons x xs) { assume "P x"

also note Cons.IH also have "Suc (length xs) = length (x#xs)" by simp finally have ?case by simp } moreover { assume "¬ P x"

also note Cons.IH also have "length xs ≤ length (x#xs)" by simp finally have ?case . } ultimately show ?case by cases qed simp cheers chris On 11/25/2014 10:15 AM, Joachim Breitner wrote:

Dear Isabelle-users, we (rightfully) pride ourselves with how natural nicely written Isar proofs are. But things are (always) not perfect, and there is always room for careful improvements. Consider this rather idiomatic proof: lemma "length (filter P xs) ≤ length xs" proof(induction xs) case Nil thus ?case by simp next case (Cons x xs) show ?case proof(cases "P x") case True with Cons have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp also note Cons.IH also have "Suc (length xs) = length (x#xs)" by simp finally show ?thesis by this simp next case False with Cons have "length (filter P (x#xs)) = length (filter P xs)" by simp also note Cons.IH also have "length xs ≤ length (x#xs)" by simp finally show ?thesis . qed qed It is a nicely written structural proof and easy to follow. But there is a wart: The case distinction! * I have to write "show ?case" to initiate a case distinction. But this is not natural: At this point, the final result is not what is on my mind. And in a manually written proof, I would not re-state the current goal at this point. * If I had not used the "case" command I would actually have to copy’n’paste the current goal here; obviously not very nice. Especially if there are multiple case distinction, each requiring me to copy that. * The goal was conveniently named ?case, but suddenly I have to write ?thesis. I (believe I) understand the techical reasons, but again, this is a violation of the principle of least surprise. What I would like to be able to write is something like lemma "length (filter P xs) ≤ length xs" proof(induction xs) case Nil thus ?case by simp next case (Cons x xs) cases("P x") case True with Cons have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp also note Cons.IH also have "Suc (length xs) = length (x#xs)" by simp finally show ?case by this simp next case False with Cons have "length (filter P (x#xs)) = length (filter P xs)" by simp also note Cons.IH also have "length xs ≤ length (x#xs)" by simp finally show ?case . qed qed No seemingly redundant statement of the subgoals, the ability to simply use ?case and the conventional flow of thoughts and facts in such a proof. This would also open the way to conveniently discharge multiple subgoals in one case distinction: lemma "A" and "B" proof- have "C" sorry cases ("D") case True from `C` show A using True sorry thus B using True sorry next case False from `C` show B using False sorry thus A using False sorry qed qed (Note that in this case, no ?thesis is available, and show A and B proof (cases "D") does not do the right thing, as it apply the cases rule only to the first subgoal, so it becomes messy to do this proof right now.) This is the users mailing list, so I’ll refrain from making wild assumptions about if and how this could be implemented, and whether there is a similarity to the obtains command, but instead ask you for feedback on the user-facing design of this feature: Is it something you’d want as well? Is the syntax nice? What could be the closing keyword, if not qed? Greetings, Joachim

**Follow-Ups**:**Re: [isabelle] Isar-Level cases command***From:*Joachim Breitner

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

- Previous by Date: [isabelle] Isar-Level cases command
- Next by Date: Re: [isabelle] Isar-Level cases command
- Previous by Thread: [isabelle] Isar-Level cases command
- Next by Thread: Re: [isabelle] Isar-Level cases command
- 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