Re: [isabelle] Can I assume an interpretation
interpretation is an operation on locales. Interpretations cannot be
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 not the case. In your theory, bop.refine_def is a
conditional equation, applicable in contexts where the locale bop is
present. In the lemma you don't have this information. The
assumption "a \<sqsubseteq> b" gives you the refine relation between
a and b, but you do not have "bop a b", and consequently neither
"ADType a" nor "ADType b".
This archive was generated by a fusion of
Pipermail (Mailman edition) and