*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Discharging one (trivial) case without nesting the proof*From*: Joachim Breitner <breitner at kit.edu>*Date*: Sun, 19 May 2013 12:02:03 +0200

Dear Isabelle users (and devs), Chrisoph’s question (http://stackoverflow.com/questions/16629417) proofs by cases reminded me of a feature wish that I wanted to talk about for a while. In pen-and-paper proofs, if there are corner cases for which the result is immediate, I just mention them at the beginning and continue with the interesting cases: Lemma: Every set that has property Q also has property P. Proof: Let S be a set with property Q. Clearly, empty sets have property P, so assume x ∈ S. [long proof] So S has property P. In Isar, I would have to write: lemma "Q S → P S" proof assume "Q S" show "P S" proof(cases "S = {}") assume True thus "P S" by simp next assume False then obtain "x ∈ S" by auto .. show "P S" qed qed What I don’t like about this is that the main proof (..) is indented deeper than it is in my mental model of the proof. Note that if I could conclude False from "S = {}" and my current facts, I could write the proof without additional indenting, e.g. using obtain. But showing False or showing that the result holds is not a huge difference in my understanding of a particular proof, so what I would like to see is, for example, lemma "Q S → P S" proof assume "Q S" trivially "S ~= {}" proof assume "~ ~ S = {}" show "P S" by simp qed then obtain "x ∈ S" by auto .. show "P S" qed where (attention, obviously inaccurate understanding of Isar’s workings under the hood following:) "trivially P" opens a proof goal "~P ==> ?P", and the user is expected to finish this proof with "show Q" where Q is the same result that he will show in the outer block. After the "trivially P" command, P is added to the facts and to this. Note the similarity with the obtain command, where I have to shown an abstract "that". I know that this is but a small reshuffling of the statements that I’d have to write with "show Q proof(cases P)...", but it does make a difference for the readability of the proof. Bonus points if somehow inside the proof block opened by tivially the statement to be shown is somehow inferred, so that I can just write lemma "Q S → P S" proof assume "Q S" trivially "S ~= {}" by simp then obtain "x ∈ S" by auto .. show "P S" qed Greetings and happy Whitsun, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Discharging one (trivial) case without nesting the proof***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Contributing some Q&A to StackOverflow; please help me to gain reputation
- Next by Date: Re: [isabelle] Contributing some Q&A to StackOverflow; please help me to gain reputation
- Previous by Thread: Re: [isabelle] Contributing some Q&A to StackOverflow; please help me to gain reputation
- Next by Thread: Re: [isabelle] Discharging one (trivial) case without nesting the proof
- Cl-isabelle-users May 2013 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