[isabelle] interpretation of a locale in a locale



Hi I have read the isabelle/isar reference manual but thing are are still not clear. What does sentence: "Using defined parameters in {\it name} one may achieve an effect similar to instantiation, though"
, in second paragraph on interpretation, mean?

Is it possible, in the interpretation of D_po (below and attached) in my_po to instantiate the parameter D ?

many thanks
       david streader


theory po
imports  Main
begin

locale my_po =
  fixes le :: "'a => 'a  => bool"
  assumes refl [intro, simp]: "le x  x"
    and   anti_sym [intro]: "[|  le x  y ; le y  x |] ==> x = y"
    and trans [trans]: "[| le x  y ; le y  z |] ==> le x z"
begin
definition Dset:: "'a set" where "Dset = {x::'a. True}"
end

locale D_po =
  fixes D :: "'a set"
  fixes leD :: "'a => 'a => bool"
  assumes defined: "leD x  y ==> x : D ==> y: D"
    and   refl [intro, simp]: "leD x  x"
    and   anti_sym [intro]: "[| leD x  y ; leD y x |] ==> x = y"
    and trans [trans]: "[| leD x  y ; leD y  z |] ==> leD x z"

interpretation my_po <  D_po
  apply unfold_locales
theory po
imports  Main
begin

locale my_po =
   fixes le :: "'a => 'a  => bool" 
   assumes refl [intro, simp]: "le x  x"
     and   anti_sym [intro]: "[|  le x  y ; le y  x |] ==> x = y"
     and trans [trans]: "[| le x  y ; le y  z |] ==> le x z"
begin
definition Dset:: "'a set" where "Dset = {x::'a. True}"
end

locale D_po =
   fixes D :: "'a set"
   fixes leD :: "'a => 'a => bool" 
   assumes defined: "leD x  y ==> x : D ==> y: D"
     and   refl [intro, simp]: "leD x  x"
     and   anti_sym [intro]: "[| leD x  y ; leD y x |] ==> x = y"
     and trans [trans]: "[| leD x  y ; leD y  z |] ==> leD x z"

interpretation my_po <  D_po 
   apply unfold_locales 


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