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:

     "_Finset" :: "args => 'a set"    ("{(_)}")
     "{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.


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