*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Reasoning with the option type*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 28 Apr 2015 12:48:48 -0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <553FA88C.9030809@in.tum.de>*References*: <CAAPnxw2YxsozyTqNnsmZghfdRa6_6f9mVTcPT7fqC7SCtp42qg@mail.gmail.com> <553F5055.2080009@cs.stonybrook.edu> <CAAPnxw0m+0cE8mTy0ABpFuBR45_iuF2-ipjkAXREaUTJb55=YA@mail.gmail.com> <553F594F.4000207@in.tum.de> <CAAPnxw2ASd+QUz3SNA2k_rCU4HtpOQsHPE6gfdHUS-7j3GtuXw@mail.gmail.com> <553FA88C.9030809@in.tum.de>*Sender*: alfio.martini at gmail.com

Great! I tried to use case, but it did not work, because I was not aware that I could declare the arbitrary fixed variables in that way (although it seems to be there in section 4.4.2 of the tutorial for the case of structural induction). Cheers! On Tue, Apr 28, 2015 at 12:34 PM, Manuel Eberl <eberlm at in.tum.de> wrote: > Since the induction hypothesis contains meta implication, there is no > other way to write it. You can, however, give names to your three different > cases so you don't have to fix/assume everything yourself: > > > theorem > assumes "l â u" > shows "sumO l u f = Some (âk=l..u. f k)" (is "?P l u f") > using assms > proof (induction l u f rule: sumO.induct[case_names 1 2 3]) > case (1 l f) > show ?case by simp > next > case (2 n m f) > thus ?case using setsum_last_int by simp > next > case (3 n m f) > hence False by simp > thus "?P n m f" by (rule FalseE) > qed > > > Cheers, > > Manuel > > > > On 28/04/15 17:11, Alfio Martini wrote: > >> Hi Manuel, >> >> Thank you for the explanations about this more general technique. I have >> seen now that it is >> explained in detail in the "Programming and Proving" tutorial under the >> name of "computation >> induction". I have tried to see the logical structure underlying your >> version of the proof using >> Isar. I came up with the following and I assume there is a more elegant >> way to write it. >> >> lemma setsum_last_int: >> "(n::int) < m â f m + setsum f {n..m - 1} = setsum f {n..m}" >> by (subst setsum.insert[symmetric]) >> (auto simp del: setsum.insert intro: setsum.cong) >> >> theorem >> assumes "l â u" >> shows "sumO l u f = Some (âk=l..u. f k)" (is "?P l u f") >> using assms >> proof (induction l u f rule: sumO.induct) >> fix l::int and f >> show "?P l l f" by simp >> next >> fix n::int and m and f >> assume "n<m" and "(n â m - 1 ==> ?P n (m - 1) f)" >> then show "?P n m f" using setsum_last_int by simp >> next >> fix n::int and m and f >> assume "m<n" and "nâm" >> then have False by simp >> then show "?P n m f" by (rule FalseE) >> qed >> >> It was very helpful, because I havenÂt seen before that the last goal >> follows by a simple contradiction. >> Yet, I am not comfortable with the way I wrote the induction hypothesis >> in the second goal. I had >> to use the metalogical symbol "==>". Assuming that I insist and writing >> all the details above, how could >> I avoid using "==>"? I have no clue. >> >> Best! >> >> On Tue, Apr 28, 2015 at 6:56 AM, Manuel Eberl <eberlm at in.tum.de <mailto: >> eberlm at in.tum.de>> wrote: >> >> It is, of course, not unreasonable to do things by hand like you >> did in order to get to know the system better. >> >> I would, however, like to show you how to shorten the proof a bit >> more. Isabelle's automation is very powerful, but you have to help >> it along a bit. As a rule, when you try to prove a fact about a >> recursively-defined function, it is advisable to use the induction >> rule for that function that the function package gives you. It >> makes things easier, both for you and for the automation. >> >> So let's apply it and see what we end up with: >> >> theorem >> "l â u â sumO l u f = Some (âk=l..u. f k)" >> apply (induction l u f rule: sumO.induct) >> apply simp_all >> >> The remaining goal is then something like >> ân m f. n < m â f m + setsum f {n..m - 1} = setsum f {n..m} >> >> This should be intuitively obvious, we're just splitting off the >> last term in the sum from n to m. We can show this as an auxiliary >> lemma, e.g. >> >> lemma setsum_last_int: >> "(n::int) < m â f m + setsum f {n..m - 1} = setsum f {n..m}" >> by (subst setsum.insert[symmetric]) (auto simp del: >> setsum.insert intro: setsum.cong) >> >> Now the proof is fully automatic: >> theorem >> "l â u â sumO l u f = Some (âk=l..u. f k)" >> by (induction l u f rule: sumO.induct) (simp_all add: >> setsum_last_int) >> >> >> Cheers, >> >> Manuel >> >> >> >> On 28/04/15 11:34, Alfio Martini wrote: >> >> Hi Eugene, >> >> Thank you for your feedback. Indeed it looks much shorter, >> since the >> simplifier takes care of the >> many intermediate steps I wrote it down. Anyway, at least for >> these >> exercises, I try to use Isabelle to check >> my handwritten proofs (or any handwritten proof that is made >> without >> assuming automated tools). >> That is why they look unnecessary long. But I will use some >> of your >> suggestions in order to improve its presentation. >> >> Best! >> >> On Tue, Apr 28, 2015 at 6:18 AM, Eugene W. Stark >> <stark at cs.stonybrook.edu <mailto:stark at cs.stonybrook.edu>> >> >> wrote: >> >> I am not very experienced, but I looked at your proof. >> It seems very long, and there are lots of apparently >> unnecessary >> assumptions that float in and out. I came up with the >> attached, >> which is rather shorter. I did not see how the use of the >> option type introduces any complication here. Hopefully I did >> not misunderstand something important. >> >> - Gene Stark >> >> >> On 04/27/2015 11:55 PM, Alfio Martini wrote: >> >> Dear Isabelle Users, >> >> In a previous thread (Isabelle: A logic of partial >> functions?) I asked >> some questions about the use of the constant >> "undefined" when >> dealing with partial functions, which have to be made >> total according >> to the foundations of Isabelle. >> >> The long thread about my difficulties with >> Sledgehammer made >> me realize that my definition was not general enough. >> And after >> looking into the very well written tutorial on Code >> Generation, I >> was convinced that I had to deal with the option type. >> >> I'm also very grateful to all that reply my original >> messages with >> many insightful and helpful observations. >> So, if some novice is interested I include here (my) >> proof of the >> total correctness of that sum algorithm. >> >> I only ask the evaluation of some more experienced >> user, if >> this is the correct way to reason with the option >> type. It looks >> a bit clumsy. >> >> The thy file is attached. Many thanks for any remarks! >> >> Best! >> >> >> >> >> >> >> >> >> -- >> Alfio Ricardo Martini >> PhD in Computer Science (TU Berlin) >> Associate Professor at Faculty of Informatics (PUCRS) >> www.inf.pucrs.br/alfio <http://www.inf.pucrs.br/alfio> >> Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica >> 90619-900 -Porto Alegre - RS - Brasil >> > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil

**References**:**[isabelle] Reasoning with the option type***From:*Alfio Martini

**Re: [isabelle] Reasoning with the option type***From:*Eugene W. Stark

**Re: [isabelle] Reasoning with the option type***From:*Alfio Martini

**Re: [isabelle] Reasoning with the option type***From:*Manuel Eberl

**Re: [isabelle] Reasoning with the option type***From:*Alfio Martini

**Re: [isabelle] Reasoning with the option type***From:*Manuel Eberl

- Previous by Date: [isabelle] Conditional simplification of constants
- Next by Date: Re: [isabelle] Conditional simplification of constants
- Previous by Thread: Re: [isabelle] Reasoning with the option type
- Next by Thread: Re: [isabelle] Reasoning with the option type
- Cl-isabelle-users April 2015 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