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