*To*: Martin Desharnais <martin.desharnais at gmail.com>*Subject*: Re: [isabelle] Datatype definition in locale context*From*: "Traytel Dmitriy" <traytel at inf.ethz.ch>*Date*: Fri, 29 Mar 2019 11:04:40 +0000*Accept-language*: de-DE, de-CH, en-US*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1a857ed5-c547-4b6d-32a4-8b3605e0effa@gmail.com>*References*: <1b60c5d0-061f-5a6d-c365-fcd589a04342@gmail.com> <1a857ed5-c547-4b6d-32a4-8b3605e0effa@gmail.com>*Thread-index*: AQHU5hkEurNCBFGH+0a8cuqcO+DPkaYiYXMA*Thread-topic*: [isabelle] Datatype definition in locale context

Hi Martin, this is fundamental: typedefs in locales may not depend on locally fixed type parameters (or term parameters). See the error messages in the example below. Since datatypes ultimately reduce to typedefs, they inherit this limitation. The only workarounds I know is to either parametrize the datatype (outside of the locale) or to monomorphize the state. Cheers, Dmitriy locale A = fixes a :: 'a fixes A :: "nat set" begin typedef foo = "UNIV :: 'a set" typedef 'a foo = "UNIV :: 'a set" typedef foo = "A" end > On 28 Mar 2019, at 17:55, Martin Desharnais <martin.desharnais at gmail.com> wrote: > > Dear Isabelle users > > I am trying to get to get to know locales and get a strange error message when using the type abstracted over in a datatype definition. Consider the following example. > > locale semantics = > fixes > step :: "'state ⇒ 'state ⇒ bool" and > inital_state :: "'state ⇒ bool" and > final_state :: "'state ⇒ bool" > begin > > definition stuck :: "'state ⇒ bool" where > "stuck s1 ≡ (∄s2. step s1 s2)" > > inductive star :: "'state ⇒ 'state ⇒ bool" where > star_refl: "star s s" | > star_step: "step s1 s2 ⟹ star s2 s3 ⟹ star s1 s3" > > datatype behaviour = > Terminates 'state | Goes_wrong > > inductive has_behaviour :: "'state ⇒ behaviour ⇒ bool" where > state_terminates: > "star s1 s2 ⟹ final_state s2 ⟹ > has_behaviour s1 (Terminates s2)" | > state_goes_wrong: > "star s1 s2 ⟹ stuck s2 ⟹ ¬final_state s2 ⟹ > has_behaviour s1 Goes_wrong" > > end > > The constructor "Terminates" of the datatype "behaviour" is intended to contain a value of the state type abstracted over by the locale. The definition fails with the following error message. > >> Extra type variables on right-hand side: "'state" > > If I change the definition to add the type variable on the right-hand side, the definition still fails with the following error message. > >> Locally fixed type argument "'state" in datatype specification > > I can solve the problem by using a fresh type variable and instantiate the "behaviour" datatype with the "'state" type in every usage (e.g. in the inductive definition "has_behaviour"), but this is a unnecessary overhead that would not scale well when the number of abstracted types involved increases. > > Why is the definition using the abstracted type "'state" directly failing? > > Is there a workaround that does not involve type parametrization of the "behaviour" datatype? > > Regards, > Martin Desharnais >

**References**:**[isabelle] Datatype definition in locale context***From:*Martin Desharnais

- Previous by Date: [isabelle] Open Position: Lecturer in Cybersecurity - University of Exeter
- Next by Date: [isabelle] TAP 2019 CFP - Soft deadline for abstract
- Previous by Thread: [isabelle] Datatype definition in locale context
- Next by Thread: [isabelle] Open Position: Lecturer in Cybersecurity - University of Exeter
- Cl-isabelle-users March 2019 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