*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] How to fix it?*From*: Lucas Cavalcante <lu_cavalcante_ at hotmail.com>*Date*: Mon, 4 Jun 2007 00:19:17 +0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*Importance*: Normal

Dear Alex,> The theory you are pointing to builds on Pure, not HOL. In Pure,> application is written "f(x)", not "f x". That's why you get the parsing> errors. If you want curried application, you can use CPure.Ok, it seem's working, thanks very very much. I've added CPure and HOL at imports's field.consts neg_eq :: "sbf => sbf"primrec"neg_eq(P) = P""neg_eq((Neg(P))) = Neg(P)""neg_eq((Neg(Neg(P)))) = neg_eq(P)"but it steel remains not okay, it returns *** Uninitialized theory data "HOL/datatypes"*** At command "primrec".> I'm not sure what you are trying to do. If you want to implement your> own logic in Isabelle, then you are on the right track, but you can't> use any of the Isabelle/HOL facilities, and most of the Isabelle/HOL> documentation does not apply.I'm trying to prove that every possible proposicional formula can be wrriten usingone or any negations in front of. It's a very simple theorem. I'm just starting, but i did not found anything looking exactaly like this in'Isabelle Tutorial'.Something liketheorem ALL formula. "neg_eq(formula) = P | neg_eq(formula) = Neg( P )"But I think it is not possible, becouse he doesn't know who is "P" (:-\), it's why i've used"EX", but you're right, seems there's no definition of EX in my theory. And also i wouldapply induction over P, but it won't work, so i must apply over "formula", but it's quantified.> If you want to use Isabelle/HOL, you can also describe modal formulae as> a HOL datatype, and the define the semantics recursively. But this is> something else, since you are doing an embedding.Basicaly, it's what I'm trying to do, but I don't know how. I just want to learnhow to do in case of this very simple case at proposicional logic, mounting my own theory, then apply to modal logic, and then define it structuraly recusirve.Any hint? (:-P)Thank you,LucasTHIS MENSSAGE: ( http://paste.ubuntubrasil.org/4305 )THE THEORY: ( http://paste.ubuntubrasil.org/4304 ) _________________________________________________________________ Obtenha o novo Windows Live Messenger! http://get.live.com/messenger/overview

**Follow-Ups**:**Re: [isabelle] How to fix it?***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] How to fix it?
- Next by Date: Re: [isabelle] How to fix it?
- Previous by Thread: Re: [isabelle] How to fix it?
- Next by Thread: Re: [isabelle] How to fix it?
- Cl-isabelle-users June 2007 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