Re: [isabelle] Specification depends on extra type variables

Hello Peter,

Thank you again for your answer. I have finally figured out how to interpret
the locale. What I needed was every easy:

locale HoareRule =
 fixes pair::"'a => 'b => ('c::well_founded_transitive)"

interpretation HoareRule "% (a::'a::well_founded_transitive) (b::('b::well_founded_transitive)) . (b, a)";

The tutorial on locales is a bit misleading. There an arbitrary order is interpreted as order on integers, and the name int is used for this interpretation. I thought of this name as being the instantiation of the locale for the int type, when actually this was just a name for the interpretation. The fact that the type name is used when interpreting a class has contributed to this confusion. Because of this misinterpretation I could not figure out how to give interpretation to something
which depends on more than one type.

There is still something which does not work as expected. The syntax defined in the locale cannot be used in the interpretation. Moreover, when I use facts from the locale in the interpretation they are parametrized by the instance for the function pair. On the other
hand when using classes things work more as I would expect them to work.

Best regards,


Peter Gammie wrote:

On 30/03/2010, at 1:55 AM, Viorel Preoteasa wrote:

locale HoareRule =
 fixes pair:: "'a => 'b => ('c::order)"

 "SUP_L_P X u i = SUPR {v . pair v i < u} (%v . X v i)";

 Hoare_dgr :: "('b => ('u::complete_lattice)) => ('b × 'b => 'u => 'u) => ('b => 'u) => bool"  ( "|- (_){| _ |}(_) "  [900,0,900] 900) where
 "|- P {| D |} Q = (? X . (! w i j .  X w i <= D(i, j) (SUP_L_P X (pair w i) j)) /\ P = SUP X /\ Q = (SUP X))"

I have succeeded to develop this general theory, but I have problem instantiating it
for concrete types. I need it instantiated for 'c = 'a * 'b where 'a and 'b are orders
and the order on 'c is the lexicographic order. (pair a b) = (b a). I have built the
lexicographic order on pairs, but I don't know how to instantiate this locale.
All examples I found with locales had only one type parameter.

I am bit confused by:

(pair a b) = (b a)

-- b does not have a function type.

If you want 'a and 'b to be fixed-but-arbitrary, define another locale, e.g.:

locale AB =
 fixes a :: "'a :: order"
 fixes b :: "'b :: order"

and use sublocale to interpret the locales containing the lemmas of interest. There was a recent thread with subject "Locale Import" initiated by Andreas Lochbihler that clearly presents the approach. Intuitively you need to define every context (set of assumptions) you want the lemmas to work in as a locale.

Note that you have to ensure that the order on 'a * 'b is the lexicographic one by examining the class instances -- you only get to define one instance per type.

Hope this helps.


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