[isabelle] interpretations and polymorphism



Hi
I am interested in using locales to instantiate type parameters and have been trying to do this when interpreting locales in locales! Not sure what is going wrong!

In the first example the interpretation worked but I subsequently could not see how to use definition bsimulate which now had additional parameters "adtA" "adtC". After some days still not sure what to do?

Example One:  (See ex.thy for details)
locale bop = RADType "adtA" +
               RADType "adtC" +
constrains adtC::"('a, 'la, 'c, 'd) rradt"
constrains adtA::"('a, 'lc, 'c, 'd) rradt"
begin
definition bsimulate :: "('a,'la,'c,'d) rradt \<Rightarrow> ('a,'lc,'c,'d) rradt \<Rightarrow> bool" (infixl "\<lesssim>\<^sup>B" 100) where ....
end

locale pbop = bop "adtA"  "adtC" +
constrains adtA::"('a, 'la, 'c, 'd) rradt"
constrains adtC::"('a, 'la set, 'c, 'd) rradt"
begin
end

interpretation pbop M bop
proof  unfold_locales qed

context pbop begin
lemma  shows "bsimulate (poweradt a) a"
unfolding bsimulate_def
proof -
end In order to understand this problem I tried to do a similar thing with partial orders but now I was unable to proov the interpretation. See ex2.thy for details.

Is there some restriction on interpretations in general?
or a restriction on locale to locale interpretations?
or have I just missed something?

kind regards  david streader

theory lift
imports  Main
begin

locale p_o =
   fixes le :: "'a\<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
   assumes refl [intro, simp]: "x \<sqsubseteq> x"
     and   anti_sym [intro]: "\<lbrakk> x \<sqsubseteq> y ; y \<sqsubseteq> x \<rbrakk> \<Longrightarrow> x = y"
     and trans [trans]: "\<lbrakk> x \<sqsubseteq> y ; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x\<sqsubseteq>z"
begin

  definition 
     less  ::"'a\<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
     where "(x \<sqsubset> y) = ( x \<sqsubseteq> y \<and> x \<noteq> y)"

  lemma less_le_trans [trans]:
    "\<lbrakk> x \<sqsubset> y ; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x\<sqsubset>z"
   
   unfolding less_def  by (blast intro: trans)

definition is_inf where "is_inf x y i = 
       (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall> z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))"
definition is_sup where "is_sup x y s = 
       (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall> z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))"

theorem is_inf_uniq: "\<lbrakk> is_inf x y i ; is_inf x y ii \<rbrakk> \<Longrightarrow> i = ii"
 unfolding is_inf_def by blast

theorem is_sup_uniq: "\<lbrakk> is_sup x y i ; is_sup x y ii \<rbrakk> \<Longrightarrow> i = ii"
 unfolding is_sup_def by blast

end

locale lattice = p_o +
      assumes ex_inf: "\<exists> inf. p_o.is_inf le x y inf"
         and  ex_sup: "\<exists> sup. p_o.is_sup le x y sup"
begin

definition mymeet (infixl "\<sqinter>" 70) where
     "x \<sqinter> y = (THE inf. is_inf x y inf)"
definition join (infixl "\<squnion>" 65) where
     "x \<squnion> y = (THE sup. is_sup x y sup)"

lemma "y\<sqsubseteq>x \<sqinter> y"
 unfolding mymeet_def proof - show "y \<sqsubseteq> The (is_inf x y)" 
sorry qed

end


locale p_op =
   fixes lep :: "'a set \<Rightarrow> 'a  set\<Rightarrow> bool" (infixl "\<sqsubseteq>\<^sub>p" 50)
   assumes reflp [intro, simp]: "x \<sqsubseteq>\<^sub>p x"
     and   anti_symp [intro]: "\<lbrakk> x \<sqsubseteq>\<^sub>p y ; y \<sqsubseteq>\<^sub>p x \<rbrakk> \<Longrightarrow> x = y"
     and transp [trans]: "\<lbrakk> x \<sqsubseteq>\<^sub>p y ; y \<sqsubseteq>\<^sub>p z \<rbrakk> \<Longrightarrow> x\<sqsubseteq>\<^sub>pz"
begin

end

interpretation p_op \<subseteq> p_o
proof unfold_locales 
fix x from reflp show "le x x" apply auto








 
end


 

header {* HHS result *}
theory ex
imports Main
begin
 

typedecl gstate
typedecl lstate
typedecl adtname
typedecl opname

consts adta :: adtname
       adtc :: adtname

consts opa :: opname
       opb :: opname
       opc :: opname

consts bull :: gstate ("\<bullet>")

record ('g,  'a, 'opn, 'adtn)  rradt = 
        AdtN :: "'adtn"
        Init :: "('g \<times> 'a)set"
        Final :: "('a \<times> 'g)set"
        Ops :: "('opn \<times> ('a \<times> 'a)set )set "


locale RADType =
   fixes   Radt :: "('g,  'a, 'opn, 'adtn) rradt"
    assumes ropsfun: "(a,rel1)\<in> (Ops Radt) \<and> (a,rel2)\<in> (Ops Radt) \<longrightarrow> rel1 = rel2"
begin
definition OpsF :: "'opn \<Rightarrow> ('a \<times>'a)set" where
        "OpsF n \<equiv> THE  rel. (n,rel)\<in> (Ops Radt)"
definition alph :: "'opn set" where "alph \<equiv> {n. \<exists> x. OpsF n = x }"
definition sem :: "'opn \<Rightarrow> ('opn \<Rightarrow> ('a \<times>'a)set ) \<Rightarrow> ('a \<times>'a)set " ("\<lbrakk>_ : _\<rbrakk>")
      where  " \<lbrakk>i:a\<rbrakk> \<equiv> (a i)"
definition  pasem ::"('opn list)\<Rightarrow> ('a \<times>'a)set" where
     "pasem prog  \<equiv>   foldr (op O) (map (\<lambda> x. sem x OpsF) prog) Id"
end   


locale bop = RADType "adtA" + 
                RADType "adtC" +
constrains adtC::"('a, 'lc, 'c, 'd) rradt"
constrains adtA::"('a, 'la, 'c, 'd) rradt"
begin
 abbreviation  OpsFc  where "OpsFc \<equiv> adtC.OpsF"
 abbreviation  OpsFa  where "OpsFa \<equiv> adtA.OpsF"
 abbreviation  pasemc ("_\<oslash>\<^sup>c" 190) where "pasemc \<equiv> adtC.pasem"
 abbreviation  pasema ("_\<oslash>\<^sup>a" 190) where "pasema \<equiv> adtA.pasem"
 abbreviation  sema ("\<lbrakk>_ : _\<rbrakk>\<^sup>a") where "sema \<equiv> adtA.sem"
abbreviation  semc ("\<lbrakk>_ : _\<rbrakk>\<^sup>c") where "semc \<equiv> adtC.sem"

abbreviation  finalc  where "finalc \<equiv> Final adtC"
abbreviation  finala  where "finala \<equiv> Final adtA"

abbreviation  initc  where "initc \<equiv> Init adtC"
abbreviation  inita  where "inita \<equiv> Init adtA"
definition  bsimulate :: "('a,'la,'c,'d) rradt  \<Rightarrow> ('a,'lc,'c,'d) rradt \<Rightarrow> bool"   (infixl "\<lesssim>\<^sup>B" 100) 
where
    "a \<lesssim>\<^sup>B c \<equiv> \<exists>\<psi>. (\<forall> nam.(\<psi>^-1  O \<lbrakk>nam : OpsFc\<rbrakk>\<^sup>c) \<subseteq> (\<lbrakk>nam : OpsFa\<rbrakk>\<^sup>aO \<psi>^-1))\<and> 
               (\<psi>^-1 O  initc) \<subseteq> inita  \<and> finalc \<subseteq> (finala O (\<psi>^-1))"
end


locale pbop = bop "adtA"  "adtC" +
constrains adtA::"('a, 'la, 'c, 'd) rradt"
constrains adtC::"('a, 'la set, 'c, 'd) rradt"
begin
end




interpretation pbop \<subseteq> bop
proof  unfold_locales qed


lemma  (in pbop) powerbsim: "bsimulate a (poweradt a)"
unfolding bsimulate_def 
proof  


 
end


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