[isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function



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







Attachment: singleton_def_error.png
Description: PNG image



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