*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Isar-Level cases command*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 25 Nov 2014 10:15:51 +0100

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 -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Isar-Level cases command***From:*Christian Sternagel

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

- Previous by Date: Re: [isabelle] emergence of "TERM _" (using quickcheck and nitpick)
- Next by Date: Re: [isabelle] Isar-Level cases command
- Previous by Thread: [isabelle] Job offer on formalizing complexity and termination techniques
- 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