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



Hi Gottfried,

you need to embed your formulas deeply in HOL, i.e., you cannot use the standard HOL connectives &, |, !, etc. for your syntax. So you must use your formula datatype also for the subexpressions of your connectives:

datatype sFOLdt =
  In sT sT
| Eq sT sT
| Not sFOLdt
| And sFOLdt sFOLdt
| Or sFOLdt sFOLdt
| Imp sFOLdt sFOLdt
| Iff sFOLdt sFOLdt
| Forall sT sFOLdt

I am not sure what sT is supposed to stand for. Is it the type for variable names or the type of values that variables can take. In the former case: what is the type of values? In the latter case: this would be a very unusual setup, to mix values of variables (like in Eq and In) with name binding (like in Forall); in that case, replace sT with some type of variable names, e.g., string.

Your sFOLf function would then interpret such formulae in terms of HOL. However, you need to deal with variables (sT) that occur freely in your formula. They must be bound by some environment (I use val for the type of values that variables can take).

type_synonym env = (sT => val)

Then, your sFOLf function should look like this:

fun sFOLf :: "env => sFOLdt => bool"
where
  "sFOLf E (In x y) = inS x y"
| "sFOLf E (Eq x y) = (E x = E y)
| "sFOLf E (Not f) = \<not> (sFOLf E f)"
| "sFOLf E (And f g) = (sFOLf E f & sFOLf E g)"
| "sFOLf E (Forall x f) = (!v. sFOLf (E(x := v)) f)"
| ,.. (* remaining cases *)

Hope this helps,
Andreas

On 01/18/2013 07:13 AM, Gottfried Barrow wrote:
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.