[isabelle] abbreviations and locales



Hi
The following local is used to proov the soundness of bsimulation with respect to refinement. But the type of the local state 'lc needs to be 'la set to proove completeness.

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"


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 Init c) \<subseteq> Init a \<and> Final c \<subseteq> (Final a O (\<psi>^-1))"


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

Previously you have told me I need to add:

abbreviation pbsimulate where
 "pbsimulate == bop.bsimulate adtA adtC"


lemma  powerbsim: "pbsimulate a  (Pc a)"

The above abbreviation indeed lets the lemma be stated with out the appearance of the unwanted "adtA" and "adtC"
But the next step:

unfolding bsimulate_def poweradt_def

reintroduces "adtC"

I have made up numerous abbreviations that let the proof proceed but I have never been able to finish the proof.

My problem is that I have no idea what is going on!

From the definition of the local what tells me that I need an abbreviation and why "bop.bsimulate adtA adtC"?

Because abbreviations get "unfolded" (for want of a better word) automatically and then folded back up prior to any response being seen I can not tell what causes the unwanted "adtC" to appear. So is there any way to see what abbreviations are being applied and what the result is?

Any ideas what I could read to explain the relation between abbreviations and locales?

Thanks in advance
    david streader









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