Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error



Hi Gottfried,

The problem is here...

> function sFOLf :: "sFOLdt => bool" where
> ...
> "sFOLf (Forall u f) = (!u. f)"

On the left you have free variables u and f, both of the same status. On the right, u is a binder, and any appearances of u inside f are bound to that binder.

I think things might be improved if you change your datatype from

> datatype sFOLdt =
> ...
> |Forall sT bool

to something like 

> datatype sFOLdt =
> ...
> |Forall "sT => bool"

Then you could write something like

> function sFOLf :: "sFOLdt => bool" where
> ...
> "sFOLf (Forall f) = (!u. f u)"

That said, I haven't tested this in Isabelle, so I might be way off the mark.

Best wishes,
john




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