Re: [isabelle] A beginner's questionu



Thank you all for your comments, the documents are really useful.
I really liked the slides, it seems to be a great course, I would totally enrol in such a course.
The first part with the motivation and the objectives  presents the subject in an attractive, yet realistic way (with the "The Sad Facts of Life" slides). Additionally I liked the fact that the language that will be studied (IMP) is not a form lambda calculus, that is interesting
Isabelle is a powerful tool, no-one will deny it, but it is also very complex. To illustrate this, one of the demos(Isar_Demo.thy) uses the following tactic

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).

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.
Thanks,

Francisco


Attachment: Arith2.thy
Description: Binary data






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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.