Re: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function
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
 Previous by Date: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function
 Next by Date: Re: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function
 Previous by Thread: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function
 Next by Thread: Re: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function

Clisabelleusers August 2012 archives indexes sorted by: [ thread ]
[ subject ]
[ author ]
[ date ]

Clisabelleusers list archive Table of Contents

More information about the Clisabelleusers mailing list
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.