*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 18 Jan 2013 08:28:45 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50F8E817.5080005@gmx.com>*References*: <50F85B11.4080205@gmx.com> <B5EE0B87-2B81-423A-B541-B206AF2AA37E@cam.ac.uk> <50F8E817.5080005@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Hi Gottfried,

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

type_synonym env = (sT => val) Then, your sFOLf function should look like this: fun sFOLf :: "env => sFOLdt => bool" where "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, Andreas 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 the mark.John, 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: http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/tutorial.pdf Thanks, GB

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

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

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