*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*: Wed, 23 Jan 2013 08:14:09 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50FE3D6F.6010204@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> <50FD9327.9070004@gmx.com> <50FE3D6F.6010204@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/22/2013 1:19 AM, Andreas Lochbihler wrote:

arities declares that a type belongs to the given type class, butleaves the parameters of the type class uninterpreted and theassumptions unproven. Thus, it is like axiomatisation: you can use itto introduce inconsistencies. Here's an example:

Andreas,

It looks like I have three options:

You say:

The second evaluation strategy (normalisation by evaluation) works.

Thanks for the "arities" example of inconsistency.

Regards, GB theory sTs__sF_130122_01 imports Complex_Main begin typedecl sT consts inS :: "sT => sT => bool" datatype sD = In sT sT | Eq sT sT | Not sD | And sD sD | Or sD sD | Imp sD sD | Iff sD sD | Forall sT sD | Exists sT sD type_synonym env = "(sT => sT)" definition sID :: "sT => sT" where "sID s = s" primrec sF :: "env => sD => bool" where "sF E (In x y) = inS x y" | "sF E (Eq x y) = (E x = E y)" | "sF E (Not f) = (¬(sF E f))" | "sF E (And f g) = (sF E f & sF E g)" | "sF E (Or f g) = (sF E f | sF E g)" | "sF E (Imp f g) = (sF E f --> sF E g)" | "sF E (Iff f g) = (sF E f <-> sF E g)" | "sF E (Forall x f) = (!v. sF (E(x := v)) f)" | "sF E (Exists x f) = (? v. sF (E(x := v)) f)" --"THE AXIOM OF EXTENSION: SET EQUALITY." axiomatization where Ax_x: "sF sID (Forall p (Forall q (Iff (Eq p q) (Forall x (Iff (In x p) (In x q)))) ) )" and Ax_x2: "sF sID (Iff (Eq p q) (Forall x (Iff (In x p) (In x q))))" theorem "(sF sID (In x y)) <-> (inS x y)" by(simp) theorem "(sF sID (Eq x y)) <-> (x = y)" by (metis sF.simps(2) sID_def) --"THE AXIOM OF EXISTENCE: THE EMPTY SET EXISTS." consts emS :: "sT" axiomatization where Ax_e: "sF sID (Forall x (Not (In x emS)))" and Ax_e2: "sF sID (Not (In x emS))" --"NO X EXISTS IN THE EMPTY SET." theorem "sF sID (Not (Exists x (In x emS)) )" by (metis Ax_e sF.simps(3) sF.simps(8) sF.simps(9)) --"THE EMPTY SET IS UNIQUE." theorem "sF sID (Forall q (Iff (Forall x (Not (In x q))) (Eq q emS) ) )" oops theorem "sF sID (Iff (Forall x (Not (In x q))) (Eq q emS) )" --"Sledgehammer found a proof, but it takes longer to execute than I'm willing to wait." --"by (metis Ax_e2 Ax_x2 sF.simps(1) sF.simps(3) sF.simps(7) sF.simps(8))" oops --"THE RECURSIVE SET TYPE: Everything is built from emS." --"The unordered pair set." consts upS :: "sT => sT => sT" --"The separation set, 'all x in q such that P x'." consts seS :: "sT => (sT => bool) => sT" datatype sTd = emSd | upSd sTd sTd | seSd sTd "sT => bool" fun sTf :: "sTd => sT" where "sTf emSd = emS" | "sTf (upSd p q) = upS (sTf p) (sTf q)" | "sTf (seSd q P) = seS (sTf q) P" value "sTf emSd" value "sTf ( upSd emSd emSd )" value "sTf ( seSd q (%x. inS x emS) )" value "sTf ( seSd emSd (%x. inS x emS) )" value "sTf ( seSd emSd (%x. P) )" end

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

**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] Isabelle2013-RC1 available for testing
- 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: [isabelle] Two questions of a beginner
- 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