Re: [isabelle] Specification depends on extra type variables

Hello Peter,

Thank you for our answer. I could get the definitions using locales. However my
case is more involved compared to the dummy example I presented in my
earlier message. The locale depends actually on three type parameters:

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.

Best regards,


On 3/27/2010 2:38 PM, Peter Gammie wrote:

On 26/03/2010, at 11:49 PM, Viorel Preoteasa wrote:

f :: "'a =>  ('b itself) =>  bool" where
"f a x = (?g . !u . g (u::'b) = a)";

However like this I have to use x as parameter for f everywhere.
Moreover, I am defining Hoare triples for some kind of programs,
and I want to use the syntax "|- _ {| _ |} _", but with this approach
I need a place for the extra dummy parameter also.

The fact is that the type 'b must be a type variable. I cannot instantiate it
at this point.
Can I suggest you look into locales?

locale L =
   fixes unused_x :: "'b"

   "f a = (?g. !u. g (u::'b) = a)"


(untested, but I can expand on this if you think it might be a profitable approach.)

You can later instantiate 'b with a sublocale or interpretation command.


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