# 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.*