*To*: Francisco Ferreira <ferrerif at iro.umontreal.ca>*Subject*: Re: [isabelle] A beginner's questionu*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 26 Nov 2010 08:07:44 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AC1CFE28-8308-4AD6-BDF0-3D008A349DE3@iro.umontreal.ca>*References*: <4CEAF770.1000304@iro.umontreal.ca> <20101123172838.10421xy6e31ub0za@mailbroy.informatik.tu-muenchen.de> <BF7B6099-B956-4041-A378-469EED0D8C86@iro.umontreal.ca> <4CECCF98.9020406@in.tum.de> <4CECC6AC.5050207@in.tum.de> <AC1CFE28-8308-4AD6-BDF0-3D008A349DE3@iro.umontreal.ca>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

> let ?ys = "take n xs" > have "xs = ?ys @ xs!n # rev ?ys" > by (metis Suc_le_lessD `length xs = Suc (n + n)` add_Suc_right add_Suc_shift append_take_drop_id assms diff_add_inverse le_add1 nth_drop' rev_take) > thus ?thesis by blast > qed > > That metis tactic is really scary (I hope that line is automatically generated by sledgehammer or something like that). Yes, it was found automatically by s/h. > That said, I am sure all the complexity problems won't be such in a live course with demos and office hours. As I said, I'd enjoy the course. I am highly interested in the subject, and Isabelle seems like a great tool. > > But, even with the documentation, and the fact that I am really trying to understand Isabelle, I just don't get it. > > I can't even prove that "step (Pred Z) m ==> m = Z", probably I am just saturated and tired of going in circles. This lemma is trivial, on one level: by(blast elim: step.cases) My slides have carefully avoided explaining this idiom in the beginning, because elimination rules (this is what "elim" stands for) and how to modify blast, are advanced concepts. You find some of this under "Rule inversion" in the IMP part of my slides. What I fail to explain there is "step.cases". The latter is a case distinction rule: how can "step x y" have been derived, i.e. like an induction but without the induction hypothesis. But my impression from your failed proof attempts is that you did not quite realize that a case distinction on which rules derived "step (Pred Z) m" is needed to perform the proof. Here is the structured proof that exposes the 2 case distinctions you need: lemma assumes "step (Pred Z) m" shows "m = Z" using assms proof cases case s_pred_zero thus "m=Z" by simp next case (s_pred m') from `step Z m'` have False by cases --"there is no rule with conclusion step Z m" thus "m=Z" by blast qed The "cases" proof method figures out which rules could have been used to derive the incoming "step x y". The assumes-shows-using contortion seems necessary, I could not get the proof to work with "step (Pred Z) m ==> m = Z", except by making it an induction instead of a case distinction, which would be misleading. As a preview of coming attractions: The lemma can now be proved automatically by s/h, but only with the latest link to smt solvers, thanks to Jasmin, Sascha, Lukas and Z3! by (smt arith.simps(5) arith.simps(2) arith.simps(4) arith.simps(8) step.simps) Yes, awesome! Tobias > Thanks, > > Francisco > > > > > ------------------------------------------------------------------------ > > > > > > > > On 2010-11-24, at 3:02 AM, Tobias Nipkow wrote: > >> For beginners I would recommend some material I have just put together >> for my Semantics course, where I use Isabelle: >> http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/ >> Under "Slides and files" you find a proof-pattern-oriented introduction >> to Isabelle proofs. Simply stop reading when the Isabelle intro stops >> and the Semantics material starts. >> >> This is work in progress and any feedback is warmly appreciated! >> >> Thanks >> Tobias >> >> Lars Noschinski schrieb: >>> On 24.11.2010 05:26, Francisco Ferreira wrote: >>>> Thank you! >>>> That was really helpful! But I am still having problems, I've checked >>>> the tutorial and the reference manual, but in the tutorial the Proof >>>> commands are not discussed, and I find the reference manual a bit too >>>> advanced, is there a tutorial on the proof command? >>> The "Tutorial on Isar"[1] covers the proof command. >>> >>> -- Lars >>> >>> [1] http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf >

**References**:**[isabelle] A beginner's questionu***From:*Francisco Ferreira

**Re: [isabelle] A beginner's questionu***From:*Christian Urban

**Re: [isabelle] A beginner's questionu***From:*Francisco Ferreira

**Re: [isabelle] A beginner's questionu***From:*Lars Noschinski

**Re: [isabelle] A beginner's questionu***From:*Tobias Nipkow

**Re: [isabelle] A beginner's questionu***From:*Francisco Ferreira

- Previous by Date: Re: [isabelle] A beginner's questionu
- Next by Date: [isabelle] Changing unification depth
- Previous by Thread: Re: [isabelle] A beginner's questionu
- Next by Thread: Re: [isabelle] A beginner's questionu
- Cl-isabelle-users November 2010 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