Re: [isabelle] How to fix it?

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: ( )THE THEORY: ( )
Obtenha o novo Windows Live Messenger!

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