*To*: Andreas Lochbihler <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 13:12:39 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50FD6F9B.2040609@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> <50FD5430.5050702@gmx.com> <50FD56E3.20502@inf.ethz.ch> <50FD6A47.6060103@gmx.com> <50FD6F9B.2040609@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 10:40 AM, Andreas Lochbihler wrote:

If you want to prove that your notion of equality of sT is reallyreflexive, transitive and symmetric, then you might do the following:definition eq :: "sT => sT => bool" where "eq p q = (!x. inS x q <--> inS x p)" lemma "eq x x" <proof> lemma "eq x y = eq y x" <proof> lemma "eq x y ==> eq y z ==> eq x z" <proof>By using your own predicate eq instead of =, you avoid that theautomated proof methods use any of HOL's predefined properties.

Andreas,

consts eqS :: "sT = > sT => bool",

theorem "!x. !y. (eqS x y) <-> (x = y)",

typedecl i arities i :: "term"

typedecl sT arities sT :: equal arities sT :: enum

Thanks for the "eq" to help me try and isolate my equal from the HOL equal. Regards, GB theory sTs__sFOLdt_130121b imports Complex_Main begin typedecl sT arities sT :: equal arities sT :: enum 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" | "sFOLf E (Eq x y) = (E x = E y)" | "sFOLf E (Forall x f) = (!v. sFOLf (E(x := v)) f)" value "sFOLf sID (In x y)" value "sFOLf sID (Eq x y)" value "sFOLf sID (Forall x (Eq x x) )" 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

**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] *_sumC generated by function package
- Next by Date: Re: [isabelle] Isabelle2013-RC1 available for testing
- 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