*To*: Oleksandr Gavenko <gavenkoa at gmail.com>*Subject*: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 21 May 2012 11:08:25 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <87bolia9gu.fsf@desktop.home.int>*References*: <87havcyn5p.fsf@desktop.home.int> <CANofLe+qNjhzCpQP41OE+dLh8LLPAZpXRN8YezngkygnoOWL+Q@mail.gmail.com> <87bolia9gu.fsf@desktop.home.int>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

The comment that reasoning _within_ such deeply embedded systems is not vey convenient unless you put effort into building tools reflects the fact that instead of proving something, you are proving that it is provable. Fortunately the extra effort is just repetitive grunt work for which Isabelle's SML user interface is ideally suited. Unfortunately you will no doubt have been led to believe that the SML user interface is not the way to go in using Isabelle. Cheers, Jeremy Oleksandr Gavenko wrote:

On 2012-05-20, Randy Pollack wrote:You can do meta logic of "deeply embedded" formal systems. Define the syntax and derivations of your object system as datatypes and inductive relations in (for example) isabelle HOL. Then you have the power of induction over these representations.Firstly thanks to Larry Paulson and Randy Pollack for answer... I understand idea about "induction over these representations", and will try to learn more on Isabelle to realise this idea...However reasoning _within_ such deeply embedded systems is not vey convenient unless you put effort into building tools.I want to notice that proofs in 'Pure' also is not convenient. For example without deduction theorem I need make a lot of rut work... I as say that I am newbie for Isabelle and so I do not understand what you mean by saying "building tools"... Can you explain more? Is this mean to write some SML support code?Propositional logic should be simple. If your object system has binding, look into using nominal isabelle. There are many examples of reasoning about formalized object systems.By saying "nominal isabelle" do you mean: http://isabelle.in.tum.de/nominal/ ?? I would glad if someone point me for examples of "reasoning about formalized object systems" as I new to this field and don't know from what to start...

**Follow-Ups**:

**References**:**[isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Oleksandr Gavenko

**Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Randy Pollack

**Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Oleksandr Gavenko

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: [isabelle] $HOME, $USER_HOME, and how I call "bin/isabelle" commands with batch/bash files
- Previous by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Next by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Cl-isabelle-users May 2012 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