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



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













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