On 1/18/2013 1:28 AM, Andreas Lochbihler wrote:
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
Hope this helps,
It helped a lot. I wouldn't have gotten to this next step without a fix.
I'll answer a few questions and then show you the failure I'm at now.
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?
Type "sT" is a primitive type that represents a set. By "can take", I
guess you mean "mapped to" as shown by your "env" below.
Semantically, I don't think a variable of type sT is mapped to another
value in the sense of a function.
I have a function:
consts seS :: "sT => (sT => bool) => sT"
I then use a function of that type, (seS q P), in an axiom describing a
property for every (q::sT) and (P::(sT => bool)), where P is a property
that holds for q. (Actually the (sT => bool) type function is what I'm
trying to tighten up with this sFOLf function.)
Variables of type sT are only used with the predicate \<in>, such as
(x::sT \<in> y::sT), or as a binder variable in \<exists> or \<forall>,
such as (!x. phi) or (? x. phi), where phi is a FOL formula built up
starting with the atomic formulas (x \<in> y) and (x = y).
Variables of type sT are used in HOL functions, but that's only because
that's how Isabelle makes me do it. The constant functions I define
represent sets, and axioms are used to state what is true about those
I could get more detailed, but I now get wellsortedness errors when
trying to use the function sFOLf in a "value" statement.
value "sFOLf1 sID (In x y)"
gives the error
"Wellsortedness error... Type sT not of sort equal. No type arity sT ::
A similar error with "enum" in place of "equal" is after the third
"value" command. The "Eq" and the "Forall" mess things up.
I'm trying to keep this short, but I'm not all that clear on the
"environment" requirement. However, like I said, variables of type sT
aren't really mapped anywhere.
To use the "value" command, I just made my "env" function the identity
The code is below, and I attached it as a THY.
Thanks for the help,
consts inS :: "sT => sT => bool"
datatype sFOLdt =
In sT sT
| Eq sT sT
| Forall sT sFOLdt
type_synonym env = "(sT => sT)"
definition sID :: "sT => sT" where
"sID s = s"
fun sFOLf :: "env => sFOLdt => bool" where
"sFOLf E (In x y) = inS x y"
value "sFOLf sID (In x y)"
fun sFOLf1 :: "env => sFOLdt => bool" where
"sFOLf1 E (In x y) = inS x y"
| "sFOLf1 E (Eq x y) = (E x = E y)"
value "sFOLf1 sID (In x y)"
fun sFOLf2 :: "env => sFOLdt => bool" where
"sFOLf2 E (In x y) = inS x y"
| "sFOLf2 E (Forall x f) = (!v. sFOLf2 (E(x := v)) f)"
value "sFOLf2 sID (In x y)"