Re: [isabelle] Can I assume an interpretation

Hi David,

interpretation is an operation on locales. Interpretations cannot be assumed.

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 MHonArc.