*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Thu, 17 Jan 2013 14:12:01 -0600*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Hi, I'm trying to set up this formula, !q. !P. ?u. (!x. x \<in> u <-> (x \<in> q & P x)),

Let x and y be variables, and let f and g be formulas, then x \<in> y is a formula, x = y is a formula, ~(f) is a formula, (f & g) is a formula, (f | g) is a formula, (f --> g) is a formula, (f <-> g) is formula, (!x. f) is a formula, (?x. f) is a formula, and nothing else is a formula.

------------------- typedecl sT consts inS :: "sT => sT => bool" (infixl "inS" 55) datatype sFOLdt = In sT sT |Eq sT sT |Not bool |And bool bool |Or bool bool |Imp bool bool |Iff bool bool |Forall sT bool function sFOLf :: "sFOLdt => bool" where "sFOLf (In u1 u2) = (u1 inS u2)" | "sFOLf (Eq u1 u2) = (u1 = u2)" | "sFOLf (Not f) = (~(f))" | "sFOLf (And f1 f2) = (f1 & f2)" | "sFOLf (Or f1 f2) = (f1 | f2)" | "sFOLf (Imp f1 f2) = (f1 --> f2)" | "sFOLf (Iff f1 f2) = (f1 <-> f2)" | "sFOLf (Forall u f) = (!u. f)" OUTPUT WINDOW ERROR: Additional type variable(s) in specification of "sFOLf_graph": 'a Specification depends on extra type variables: "'a" The error(s) above occurred in "sTs.sFOLf_sumC_def" The error(s) above occurred in definition "sFOLf_sumC_def":

-------------------

Thanks, GB

**Attachment:
function error.1.png**

**Follow-Ups**:**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:*John Wickerson

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