*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 10:18:15 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50FD56E3.20502@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>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/21/2013 8:55 AM, Andreas Lochbihler wrote:

The error remains because 1. you did not declare the axiom Ax_x as a code equation, and2. it is not executable as the !x-quantifier ranges over sT for whichyou have not provided an implementation.The code generator will not work unless you provide a concreterepresentation for the elements of sT.

Andreas,

Even after only having made the statement "typedecl sT", HOL will prove that "=" for type "sT" is reflexive, symmetric, and transitive.No, it is not HOL that proves these three properties, = on any type isby axiom in HOL.thy reflexive, transitive and symmetric. As you useaxiomatization, it is your job to make sure that your specification isconsistent with HOL's axioms.

I had looked previously at the axioms for "=" here in HOL.thy: axiomatization where refl: "t = (t::'a)" and subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"

rule, and similar to the ABS rule of HOL*} and the_eq_trivial: "(THE x. x = a) = (a::'a)"

lemma sym: "s = t ==> t = s" by (erule subst) (rule refl)

As you use axiomatization, it is your job to make sure that yourspecification is consistent with HOL's axioms.

Thanks, GB

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

- 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