[isabelle] Datatype definition in locale context

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 =
    step :: "'state ⇒ 'state ⇒ bool" and
    inital_state :: "'state ⇒ bool" and
    final_state :: "'state ⇒ bool"

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
    "star s1 s2 ⟹ final_state s2 ⟹
    has_behaviour s1 (Terminates s2)" |
    "star s1 s2 ⟹ stuck s2 ⟹ ¬final_state s2 ⟹
    has_behaviour s1 Goes_wrong"


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?

Martin Desharnais

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