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

```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 connectives:
```Hope this helps,
```
```Andreas,

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 functions.
```
```
I could get more detailed, but I now get wellsortedness errors when trying to use the function sFOLf in a "value" statement.
```
The command

value "sFOLf1 sID (In x y)"

gives the error

```
"Wellsortedness error... Type sT not of sort equal. No type arity sT :: equal"
```
```
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 function.
```
The code is below, and I attached it as a THY.

Thanks for the help,
GB

theory sts__sFOLdt
imports Complex_Main
begin

typedecl sT

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)"

end

```
```theory sTs__sFOLdt
imports Complex_Main
begin

typedecl sT

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)"

end
```

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