Re: [isabelle] How to fix it?



Lucas Cavalcante wrote:
> I'd like to provetheorem negeq: "EX xs. ((neg_eq Formula) = ~xs
> (*here*) | (neq_eq Formula) = xs)" Applying induction over Formula,
> but Isar says "Inner lexical error at: = ~xs".

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.

Then, you are trying to use an existential quantifier, but your theory
does not define any quantifiers, just propositional and modal
connectives. So it won't be there. You just get what you define, plus
the meta logic ("!!" and "==>").

> Just as happen at neg_eq's recursive funcion definition:
> consts neg_eq :: "sbf => sbf"
> primrec 
> "neg_eq P = P" (*here*)
> "neg_eq ~P = ~P"
> "neg_eq ~~P = neg_eq P"

primrec definitions (and many other things described in the tutorial)
are only possible in HOL. If you use Pure, then you really only have the
bare logic.

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.

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.

Hope that helps a little...
Alex





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