Re: [isabelle] A beginner's questionu



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





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