Re: [isabelle] Input/Output syntax for locale interpretation



You should be able to either introduce explicit abbreviations for your constants in the global theory, or, if suitable concepts are already available there, you might prefer to provide explicit mappings by adding "where" clauses to your interpretation.

Clemens


Quoting Peter Lammich <lammich at in.tum.de>:

Hi all,

I have some locale that fixes quite a few parameters, as for example:


locale foo =
  fixes a b c :: nat
begin
  definition "const1 == a<c"
  definition "const2 == a<c+b"
end


Now I want to interpret the locale, using some quite long
instantiations, eg:

interpretation prefix?: foo "(1+3)*7" "(1+9)*42" "91 - 11*2" .


All is nice up to here. However, when I start using the locale, e.g. in

lemma "const1 ==> const2"


then some horrible output occurs, that nobody want's to read any more:

foo.const1 ((1 + 3) * 7) (91 - 11 * 2) ==>
    foo.const2 ((1 + 3) * 7) ((1 + 9) * 42) (91 - 11 * 2)


How can I change this behaviour, such that I get the plain names in the
output (or, if I used prefix!, the prefixed names).
Note: The locale tutorial sais that the current behaviour is the
intended one, but does not mention how
to change it.

Regards,
  Peter








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