*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*: Mon, 21 Jan 2013 15:55:31 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50FD5430.5050702@gmx.com>*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> <50FD5430.5050702@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Dear Gottfried,

--"HOL equal is defined." axiomatization where Ax_x: "!q.!p. ( !x. (inS x q) <-> (inS x p) ) <-> (p = q)"

>

Okay. I don't really compute equality, I define it as shown above by axiom Ax_x. I stuck that axiom into the experimental fFOLdt theory and it didn't get rid of the error.

The error remains because 1. you did not declare the axiom Ax_x as a code equation, and

Even after only having made the statement "typedecl sT", HOL will prove that "=" for type "sT" is reflexive, symmetric, and transitive.

Regards, Andreas

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

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

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