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.
> 
> Lawrence Paulson has said : Itâs essential to understand that âproofâ by
> itself will attempt to use the default proof method. But this default
> proof method can lead to an unprovable goal.

The main Isar proof scheme is as follows:

  from facts1 have goal
    using facts2
  proof method1
    ...
  qed method2

The body "..." then consists recursively of sub-proofs, each with a
local context:

  fix parameters
  assume premises
  show conclusion
    <proof>

These usually address each sub-goal in turn, but the order is arbitrary.
The "next" command may be used to proceed with a fresh local context;
alternatively it is always possible to use { ... } to indicate context
block structure.

The initial refinement of "proof method1" uses facts = facts1 facts2
(appended in that order) and passes that to the proof method. It is
"standard" by default; "standard" is a bit more than just "rule", but
usually it is sufficient to think of "rule" as the standard step.

The terminal method2 has a chance to finish-off remaining sub-goals (it
may be omitted). Afterwards there is always an implicit stage to finish
everything implicitly by-assumption.

Some important abbreviations:

  proof method1 qed method2  == by method1 method2
  ..  == by standard
  .   == by this

Proof method "standard" applies a standard rule: the facts are put into
its premises (in that order), the remaining rule is applied to the goal.

Proof method "this" applies all "used" facts directly, without putting a
rule in between.


To apply these Isar principles in practice, I recommend to take all the
Natural Deduction rules for predicate logic as examples, and turn them
into canonical Isar proof outlines, e.g. like this for conjunction:

  have "A â B"
  proof
    show A sorry
    show B sorry
  qed

next

  assume *: "A â B"
  then have A ..
  from * have B ..

The double projection is a bit awkward. Better eliminate conjunction
simultaneously:

  assume "A â B"
  then obtain A B ..

Etc. ... Here is
http://teachinglogic.liglab.fr/DN/index.php?formula=p+%26+q+%3D%3E+q+%26+p&action=Prove+Formula
in Isar:

  have "A â B â B â A"
  proof
    assume "A â B"
    then obtain B A ..
    then show "B â A" ..
  qed


You can enclose the above snippets into "notepad begin ... end", to
avoid having toplevel theorem statements (which have separate syntax).

I also recommend to start Isar without ever writing Pure rule statements
in the text: these somehow belong to the "implementation" of logic and
are rarely needed in proof texts.


> I think the indication above on how to prove a thesis must be written in
> the tutorial prog-prove or an another short tutorial on
> the manner to write proofs in Isar.

After more than 30 years, the situation of Isabelle manuals is very
complex. Everything can be found somewhere, but it might take time to
find it. Moreover, some old materials needs to be ignored, especially
when getting started.


	Makarius





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