Re: [isabelle] elementary proofs



Hi,

It should be  in the reference manual and in the programming and proving
tutorial.

Best
Em 27/03/2016 07:06, "michel levy" <michel.levy at imag.fr> escreveu:

> On 27/03/2016 04:59, Alfio Martini wrote:
> Thank you really much for your help.
>
> Hi Michel,
>
> I think you have to use the hyphen method "-" as an argument for
> the command proof, because there is no introduction rule for proving
> an atomic statement like R. There are a lot of ways to prove this
> conjecture. One way possible (using more or less your style) goes
> as follows:
>
> Where do you find this information ? I don't find it in the tutorial,
> isar-ref and implementation.
>
>
> lemma facile2 : "(P â Q) â (Q â R) â (P â R)"
>   proof
>     assume 1: "(P âQ)â (Q â R)"
>     show "P â R"
>     proof (rule impI)
>       assume 2:"P"
>       show "R"
>       proof -
>         from 1 have "PâQ" by (rule conjE)
>         then have q: Q using 2 by (rule mp)
>         from 1 have "QâR" by  (rule conjE)
>         from this and q show ?thesis by (rule mp)
>       qed
>     qed
>   qed
>
> Best!
>
> I try these elementary proofs, because I have written an prover, which
> produces proofs in natural deduction for
> intuitionistic and classical propositional logic, with the following
> address <http://teachinglogic.liglab.fr/DN/>.
> And I plan to give an output which is the proof in isabelle, so I must
> understand how to do the translation.
> I am a retired   teacher (67 years old), so I am working slowly !
>
>
>     Sincerely yours
>
> --
> email : michel.levy at imag.frhttp://membres-liglab.imag.fr/michel.levy
>
>



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