Re: [isabelle] Declaring equal for a type; BNF not working on the left

On 11/6/2013 10:48 PM, Gottfried Barrow wrote:

As to BNF, again I have this datatype:

datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"

What I think I've found is that I can use it on the right side of recursive functions, but I can't use it on the left side.

I try using datatype_new_compat, and also primrec instead of fun. I tried to define a function to use "'a mS fset option", but it doesn't work, where a function like that for mT does work.

The BNF crew can officially consider that this error report has been resolved to my satisfaction, primarily because I should have been using primrec_new instead of primrec, though up to this point, I've stayed away from using primrec, because the magic of fun can kick in where the magic of primrec ends. Consequently, there being no fun_new caused me to forget about primrec_new, until things led me back to datatype.pdf

Here, Andrea's answer to my question about equality led me to a reference he gave me, which led me back to datatype.pdf.

I don't care that I can't make fun work with datatype_new, as long as primrec_new is working for me.

However, if one of the BNF crew cares, below is what I get, which could be due to me doing things wrong, or not knowing how to register something to make it work. I give an example of "value" returning an error, where I know that "value" and the code generator can be a whole different matter.


datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"

primrec_new mSSsome :: "'a mS => 'a mS fset option" where
"mSSsome (mSp x) = None"
|"mSSsome (mSS x) = Some x"

theorem "mSSsome (mSS{|mSp x|}) = Some {|mSp x|}"

theorem "mSSsome (mSp x) = None"

value "mSSsome (mSp x)"
"c.mS.mSp" is not a constructor, on left hand side of equation, in theorem:
mSSsome (mSp ?x) ≡ None*)

datatype_new_compat "mS"
Unsupported recursion via type constructor "FSet.fset" not associated with
new-style datatype (cf. "datatype_new")*)

fun mSSsome2 :: "'a mS => 'a mS fset option" where
"mSSsome2 (mSp x) = None"
|"mSSsome2 (mSS x) = Some x"
(*Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀x. mSSsome2 (mSp x) = None*)

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