Email Gateway (Aug 18 2022 at 10:34): Email Gateway (Aug 18 2022 at 10:34):From: Lucas Cavalcante <lu_cavalcante_@hotmail.com>
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". 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"
Isar says "Inner lexical error at: = P".How to fix it?Regards,LucasPS.: THIS MENSAGE: (http://paste.ubuntubrasil.org/4300), THE THEORY: (http://paste.ubuntubrasil.org/4299).
Veja só alguns dos novos serviços online no Windows Live Ideas — são tão novos que ainda não foram disponibilizados oficialmente.
http://ideas.live.com
Email Gateway (Aug 18 2022 at 10:35):From: Alexander Krauss <krauss@in.tum.de>
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
Email Gateway (Aug 18 2022 at 10:36):From: Tobias Nipkow <nipkow@in.tum.de>
In your two examples you need to relace ~X by (~X).
Tobias
Lucas Cavalcante schrieb:
Email Gateway (Aug 18 2022 at 10:37):From: Lucas Cavalcante <lu_cavalcante_@hotmail.com>
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
Email Gateway (Aug 18 2022 at 10:37):From: Alexander Krauss <krauss@in.tum.de>
Lucas,
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).
Alex
Last updated: May 03 2024 at 12:27 UTC