*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*: Fri, 18 Jan 2013 11:50:26 -0600*In-reply-to*: <50F8F9AD.1080108@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>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/18/2013 1:28 AM, Andreas Lochbihler wrote:

you need to embed your formulas deeply in HOL, i.e., you cannot usethe standard HOL connectives &, |, !, etc. for your syntax. So youmust use your formula datatype also for the subexpressions of yourconnectives: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 forvariable names or the type of values that variables can take. In theformer case: what is the type of values?

I have a function: consts seS :: "sT => (sT => bool) => sT"

The command value "sFOLf1 sID (In x y)" gives the error

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

**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

- Previous by Date: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- 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