[isabelle] Can I assume an interpretation

I have defined a locale for (very abstract) ADTs and am proving soundness and completness of simulation w.r.t. refinement

Refinement is defined in a local bop built on two locals, one for each ADT

abbreviation myref (infix "\<sqsubseteq>" 70) where "a \<sqsubseteq> c \<equiv> bop.refine a c"

Transitivity becomes:

lemma transref: "a \<sqsubseteq> b \<longrightarrow> b \<sqsubseteq> c \<longrightarrow> a \<sqsubseteq> c"
See attached file for very short theory containing details.

But I am unable to proceed with this lemma. To the best of my understanding the assumption "a \<sqsubseteq> b " includes an assumption that "a c" are an interpretation of the local bop. (This is certainly what I want) But i am unable to unfold "a \<sqsubseteq> b ".
I think I need to use the assumed interpretation to do this.

As ever my basic lack of understanding is limiting me.

many thanks in advance

Isar is proofs have been very much more robust than any proofs I previously constructed in Isabelle.
header {*Abstract data types*}
theory ex
imports Main

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

locale ADType =
   fixes   adt :: "('g,  'a, 'opn, 'adtn) adtt"
    assumes ropsfun: "(a,relx)\<in> (Ops adt) \<and> (a,rely)\<in> (Ops adt) \<longrightarrow> relx = rely"
    assumes opsdef: "\<forall> x:: 'opn.  \<exists> r . (x,r)\<in> Ops adt"
definition OpsF :: "'opn \<Rightarrow> ('a \<times>'a)set" where
        "OpsF n \<equiv> THE  rel. (n,rel)\<in> (Ops adt)"
definition  pasem ::"('opn list)\<Rightarrow> ('a \<times>'a)set" where
     "pasem prog  \<equiv>   foldr (op O) (map OpsF prog) Id"


locale bop = ADType "a" + 
             ADType "c" +
constrains c::"('a, 'lc, 'c, 'd) adtt"
constrains a::"('a, 'la, 'c, 'd) adtt"
 abbreviation  ppasem ("_\<oslash>_" 190) where "ppasem \<equiv> ADType.pasem"

definition  refine:: "bool"  
     "refine \<equiv> \<forall> p. Final c O(c\<oslash> p )O Init c \<subseteq> Final a O((a\<oslash> p ))O Init a"

abbreviation  myref  (infix "\<sqsubseteq>" 70) where "a \<sqsubseteq> c \<equiv> bop.refine a c"

lemma transref: "a \<sqsubseteq> b \<longrightarrow> b \<sqsubseteq> c \<longrightarrow> a \<sqsubseteq> c"  
proof assume ab: "a \<sqsubseteq> b"  show "b \<sqsubseteq> c \<longrightarrow> a \<sqsubseteq> c"
    proof assume bc: "b \<sqsubseteq> c" show "a \<sqsubseteq> c"
      using ab bc 
      unfolding bop_def bop.refine_def
    sorry qed


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