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



On 1/17/2013 11:35 PM, John Wickerson wrote:
The problem is here...
function sFOLf :: "sFOLdt =>  bool" where
...
"sFOLf (Forall u f) = (!u. f)"
[...]
That said, I haven't tested this in Isabelle, so I might be way off the mark.
John,

No, you're on the mark. Thanks for the tip. That gets rid of that particular error, but there are some major problems still. I'm not doing any real recursion. Like for this statement,

"sFOLf (And f1 f2)  = (f1 & f2)",

I would need to recurse on f1 and f2, but I'm not even close; that's all messed up. I get an error from trying

value "sFOLf (And True True)"

Alfio pointed out section 2.5.6 of the tutorial, page 19:

http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/tutorial.pdf

Thanks,
GB





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