Re: [isabelle] isar in PIDE : strange behavior



On 03/03/17 15:26, Michel via Cl-isabelle-users wrote:
> Thank you really much for your examples.  I try to write basic proofs if
> it possible without automation and with your suggestion it was possible.
> I have written a software <http://teachinglogic.liglab.fr/DN/> (a long
> time ago) to produce proof in natural deduction.
> 
> This software was originally written in Prolog by Robert StÃrk, who was
> assistant at ETH ZÃrich. I try to see if the proofs given by this
> software can be translated in Isar. That is the origin of my questions
> on Isar.

Here is more exercise material based on the above website. It uses
Isabelle/Pure directly, without the huge Isabelle/HOL library.  Thus it
is really confined to single-step structure proofs in Isar. Moreover,
classical logic is not assumed globally, but confined to a separate
locale context (in contrast, most Isabelle/HOL tools use classical logic
implicitly).

As Peter has already pointed out before, these proofs are a bit atypical
for practical Isar: there is a fine art to write rule statements in open
form, without too many auxiliary logical connectives getting in between.
This is occasionally called "logic-free reasoning".


	Makarius


Attachment: Pure_Logic.thy
Description: application/extension-thy

Attachment: Ex.thy
Description: application/extension-thy



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