# [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

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.