[isabelle] Can I assume an interpretation



Hi
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
david

p.s.
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
begin

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"
begin
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"

end


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

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

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
qed

 end






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