Re: [isabelle] Specification depends on extra type variables


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

> locale HoareRule =
>  fixes pair:: "'a => 'b => ('c::order)"
>  begin
> definition
>  "SUP_L_P X u i = SUPR {v . pair v i < u} (%v . X v i)";
> definition
>  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.