[isabelle] interpretation and sublocale ignore order of parameters



Dear locale experts,

The commands for interpreting a locale (interpret/interpretation/sublocale) accept parameters declared with a for clause. The generated abbreviations for the constants defined in the locale then take the declared parameters as additional arguments. However, the order of these additional arguments is IMHO all but intutive and a night-mare for maintainability. The two examples below illustrate this.

1. Suppose we have a locale which fixes a parameter and defines a function f using the parameter x. For the interpretation, let's define an abbreviation foo with two arguments and interpret the locale for foo with both parameters declared in a for clause.

  locale l = fixes x :: int begin
  definition f where "f y = x + y"
  end

  abbreviation foo :: "nat â int â int" where "foo x y == y - 2 * int x"
  interpretation sl!: l "foo x y" for x :: nat and y :: int .
  term sl.f  (* Îy x. l.f (foo x y) *)

As can be seen by inspecting the generated abbreviation sl.f, the order of the parameters in the for clause (first x, then y) has been ignored, as sl.f takes first the y and then the x.

Now, if I later change foo from an abbreviation to a definition, the order of parameters changes. Now, sl'.f takes the x first and then the y.

  definition foo' :: "nat â int â int" where "foo' x y == y - 2 * int x"
  interpretation sl'!: l "foo' x y" for x :: nat and y :: int .
  term sl'.f  (* Îx y. l.f (foo' x y) *)

Apparently, not the order of the parameters in the for clause matters, but the order of the parameters as they occur in the term which is used to instantiate the parameter. So, when I going from an abbreviation to a definition, I have to reorder the first two parameters of all occurrences of sl.f in my theories.

2. If we have a locale with several parameters (say 2), things get even worse. The order of the parameter is not consistent over several constant declarations. In this example, there are two parameters and two definitions each of which depends on only one of the parameters.

  locale l2 = fixes x :: int and z :: int begin
  definition f where "f y = x + y"
  definition g where "g y = z + y"
  end

  interpretation sl2!: l2 "y - 2 * int x" "int x - 2 * y" for x :: nat and y :: int .
  term "sl2.f :: int â nat â int â int"
  term "sl2.g :: nat â int â int â int"

Now we see that sl2.f first takes the y and then the x, whereas sl2.g first takes the x and then the y.


I find this particularly annoying, because for every function defined in my locale I have to remember separately the order of the parameters. I'd prefer much more if interpretation and friends used the order of the parameters as given in the for clause consistently for all constants. Can this behaviour be somehow changed?

I tried to use unnamed context blocks to fix the order of parameters, but interpretations are gone at the end of the block and sublocale and permanent_interpretation do not work inside such blocks.

Andreas




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