已证明graph实例后，如何调用其locale内定义的path符号？

问题背景 #

已基于category3理论中的graph概念，证明了以下引理：

lemma i_have_a_graph: shows "graph Obj Arr Dom Cod"
  sorry

其中Obj、Arr、Dom和Cod已在文件中提前定义，当前可访问graph locale中的引理与定理，希望使用该locale内定义的path符号。

相关未解答问题（翻译后） #

如何从子locale访问定义？

方法1：通过interpretation绑定locale #

用interpretation命令将已证明的graph Obj Arr Dom Cod与graph locale关联，之后可直接通过别名引用path：

interpretation my_graph: graph Obj Arr Dom Cod by (rule i_have_a_graph)

后续使用示例：

lemma "my_graph.path x y"
  sorry

方法2：在locale上下文内编写代码 #

如果后续大量证明依赖该graph，可直接在graph locale的上下文内工作：

context graph begin
lemma "path x y"
  sorry
end

该方式需确保当前上下文满足graph的假设，或提前通过interpretation绑定具体参数。

方法3：直接使用限定语法引用 #

临时引用时，可通过locale限定形式结合已有引理约束上下文：

lemma assumes "graph Obj Arr Dom Cod"
  shows "graph.path Obj Arr Dom Cod x y"
  using assms sorry

内容的提问来源于stack exchange，提问作者Charles Staats