Re: [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
> 



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.