*To*: cl-isabelle-users at lists.cam.ac.uk, andreas.lochbihler at inf.ethz.ch*Subject*: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 21 Jan 2013 08:44:00 -0600*In-reply-to*: <50FCEF87.10907@inf.ethz.ch>*References*: <50F85B11.4080205@gmx.com> <B5EE0B87-2B81-423A-B541-B206AF2AA37E@cam.ac.uk> <50F8E817.5080005@gmx.com> <50F8F9AD.1080108@inf.ethz.ch> <50F98B62.7040206@gmx.com> <50FCEF87.10907@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/21/2013 1:34 AM, Andreas Lochbihler wrote:

I still did not quite get the meaning of the sT type. If I understandyou correctly, you use the values over which a variable ranges (whatyou call "mapped to") also for the names of the variables.

Andreas,

--"The primitive type." typedecl sT --"The predicate 'is an element of'." consts inS :: "sT => sT => bool" --"HOL equal is defined." axiomatization where Ax_x: "!q.!p. ( !x. (inS x q) <-> (inS x p) ) <-> (p = q)" --"The empty set constant." consts emS :: "sT" --"The empty set constant axiomatized." axiomatization where Ax_e: "!x.~(inS x emS)"

Anyway, let's look at your issue with the value command. This commanduse various evaluation strategies with Isabelle's code generator beingthe default (and usually the fastest). Now, the definition of sFOLf1for Eq uses HOL equality on the right-hand side for the type sT:"sFOLf1 E (Eq x y) = (E x = E y)"However, you have not told Isabelle how to compute equality on typesT, which is done as an instance of the type class equal.

Regards, GB

The enum sort constraint comes from using the ! quantifier over sT in "sFOLf2 E (Forall x f) = (!v. sFOLf2 (E(x := v)) f)"By default, ! is implemented to enumerate all values for v and testfor each whether the predicate holds. Again, Isabelle does not knowhow to enumerate all values of type sT. You can do so by instantiatingthe type class enum.Best, Andreas On 01/18/2013 06:50 PM, Gottfried Barrow wrote: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

**Follow-Ups**:**Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error***From:*Andreas Lochbihler

**References**:**[isabelle] Trying to use "datatype" to restrict types of formulas used, getting error***From:*Gottfried Barrow

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

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

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

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

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

- Previous by Date: Re: [isabelle] Isabelle2013-RC1 available for testing
- Next by Date: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Previous by Thread: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Next by Thread: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list