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

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

Init :: "('g \<times> 'a)set"
Final :: "('a \<times> 'g)set"
Ops :: "('opn \<times> ('a \<times> 'a)set )set "

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" +
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.