Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
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"
"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,
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
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:
This archive was generated by a fusion of
Pipermail (Mailman edition) and