Re: [isabelle] How to fix it?


> Ok, it seem's working, thanks very very much. I've added CPure and HOL
> at imports's field.

For normal applications, you should always import "Main" (which CPure
and HOL). Then the primrec command is available.

> consts neg_eq :: "sbf => sbf"
> primrec
> "neg_eq(P) = P"
> "neg_eq((Neg(P))) = Neg(P)"
> "neg_eq((Neg(Neg(P)))) = neg_eq(P)"

Primrec can only do primitive recursion over inductive datatypes (i.e.
you define them via the "datatype" command). So even if you import Main,
this will fail.

> I'm trying to prove that every possible proposicional formula can be
> wrriten using
> one or any negations in front of.

For that, you need to define your formulae as an inductive datatype,
just as a type of lists or trees (see Tutorial).


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