*To*: Vadim Zaliva <vzaliva at cmu.edu>*Subject*: Re: [isabelle] Isar syntax question*From*: Timothy Bourke <tim at tbrk.org>*Date*: Thu, 17 Jul 2014 00:12:38 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <2FBE95AA-17AD-4DA1-AB09-6766B79B4B37@cmu.edu>*Mail-followup-to*: Vadim Zaliva <vzaliva at cmu.edu>, USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*References*: <2FBE95AA-17AD-4DA1-AB09-6766B79B4B37@cmu.edu>*User-agent*: Mutt/1.5.21 (2010-09-15)

* Vadim Zaliva <vzaliva at cmu.edu> [2014-07-16 15:00 -0700]: > I am learning Isar and have another naive question on the syntax: > I am trying to do something like this in Isar: > > 1: lemma > 2: shows "not something" > 3: proof(rule ccontr) > 4: assume "something" > 5: thus False proof cases > 6: ... > 7: qed > 8: qed > > and get "*** Failed to refine any pending goal" error around line 5 > > Why this does not work? Something like this works instead: The consequent of ccontr does not match your stated goal. You want rather lemma "¬ something" proof (rule notI) assume "something" thus False sorry qed Typing "find_theorems intro" after line 2 gives a list of applicable rules. But, in fact, in this case Isar finds the right rule by itself: lemma "¬ something" proof assume "something" thus False sorry qed Tim.

**Attachment:
signature.asc**

**References**:**[isabelle] Isar syntax question***From:*Vadim Zaliva

- Previous by Date: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Next by Date: Re: [isabelle] Isar syntax question
- Previous by Thread: [isabelle] Isar syntax question
- Next by Thread: Re: [isabelle] Isar syntax question
- Cl-isabelle-users July 2014 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