Email Gateway (Aug 19 2022 at 08:23): Email Gateway (Aug 19 2022 at 08:23):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I'm trying to define the singleton "{x} == {x,x}", as shown on line 90
of the attached screenshot. I've tried lots of different things, but I
have the following four lines, :
consts upS :: "??e?t ? ??e?t ? ??e?t"
syntax "_upS" :: "args ? ??e?t" ("{_}??")
translations "{u,v}??" == "CONST upS u v"
translations "{u}??" == "{u,u}??"
On the fourth line above, I get this error:
Error in syntax translation rule: duplicate vars in lhs
("_upS" ("_args" u u)) -> ("_upS" u)
QUESTION: Can I somehow get "{x} == {x,x}" using only "syntax",
"translations", and the one function "upS"? I'm trying not to introduce
a second function.
EXAMPLES I'VE LOOKED AT
src/ZF/ZF.thy line 141:
translations
....
"<x, y, z>" == "<x, <y, z>>"
"<x, y>" == "CONST Pair(x, y)"
src/HOL/Set.thy line 140:
syntax
"_Finset" :: "args => 'a set" ("{(_)}")
translations
"{x, xs}" == "CONST insert x {xs}"
"{x}" == "CONST insert x {}"
src/HOL/ZF/HOLZF.thy:
definition Singleton:: "ZF \<Rightarrow> ZF" where
"Singleton x == Upair x x"
So this last example shows me a simple way to get what I'm trying to do,
but, at least at this point, I'd rather not introduce another function.
Thanks,
GB
singleton_def_error.png
Email Gateway (Aug 19 2022 at 08:23):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I'd still prefer to do as I say in my first email, but I go ahead and
introduce the second function for the singleton set, and so I end up
with something like this:
(Ct....Unordered pair: constant set to be axiomatized.)
consts upS :: "sT => sT => sT"
syntax "_upS" :: "args => sT" ("{_}")
translations "{u,v}" == "CONST upS u v"
(Df....Unordered pair: singleton set.)
definition upSs :: "sT => sT" where
"upSs u == upS u u"
translations "{u}" == "CONST upSs u"
Due to the last line of the code above, my next theorem gets this error:
Undeclared constant: "_args"
If I delete translations "{u}" == "CONST upSs u", the error goes away.
I can use two "syntax" commands for a "_upS" and "_upSs", and not use
"args", but I like the idea of using the "args" that I get from this
following code in Set.thy, line 140:
syntax
"_Finset" :: "args => 'a set" ("{(_)}")
translations
"{x, xs}" == "CONST insert x {xs}"
"{x}" == "CONST insert x {}"
I haven't tracked down what "args" does, but it would be nice to leave
that in, so in the future I can define finite sets similar to ZF.thy and
Set.thy.
Thanks,
GB
Email Gateway (Aug 19 2022 at 08:23):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I got something that works. If someone wants to tell me how to do it
with only the one function "consts upS", that would be okay.
I couldn't find where "args" is defined. It appears that it's defined
somewhere in Pure. I found "args" in the index of isar-ref.pdf (pg. 58),
but I couldn't tell if it was a reference to the "args" below.
This works:
consts upS :: "sT => sT => sT"
definition usS :: "sT => sT" where "usS u == upS u u"
syntax "_upS" :: "args => sT" ("\<lbrace>(_)\<rbrace>")
translations "\<lbrace>u,v\<rbrace>" == "CONST upS u v"
"\<lbrace>u\<rbrace>" == "CONST usS u"
This doesn't work:
consts upS :: "sT => sT => sT"
definition usS :: "sT => sT" where "usS u == upS u u"
syntax "_upS" :: "args => sT" ("\<lbrace>(_)\<rbrace>")
translations "\<lbrace>u,v\<rbrace>" == "CONST upS u v"
translations "\<lbrace>u\<rbrace>" == "CONST usS u"
Using the two "translations" causes this error on the next theorem:
Undeclared constant: "_args"
Regards,
GB
Last updated: Apr 26 2024 at 16:20 UTC