1

我创建了一个名为 的记录类型graph，并定义了一个合适的“是”关系的子图。我想表明一组图与子图关系形成一个顺序，即是ord类的一个实例。但我无法让它工作。这是我的最小工作示例：

theory John imports
  Main
begin

typedecl node

record graph =
  nodes :: "node set"
  edges :: "(node × node) set"

definition subgraph :: "graph ⇒ graph ⇒ bool"
  (infix "⊑" 50)
where
  "G ⊑ H ≡ 
  nodes G ⊆ nodes H ∧ edges G ⊆ edges H"

lemma "(GREATEST H. H ⊑ G) = G"
oops

end

我得到错误：

Type unification failed: No type arity graph_ext :: ord"

我尝试输入诸如instantiation graph :: ordand之类的内容instantiation graph_ext :: ord，但似乎没有任何效果。有任何想法吗？

4

1 回答 1

2

定义记录后，实际上会在graph后台创建一个新类型。'a graph_ext此类型与您的记录类型相同，但有一个额外的字段，允许附加额外的数据（即，在'a您的记录定义中添加了一个具有类型的新字段，可用于稍后将其他数据添加到您的记录中上）。类型graph只是 的缩写unit graph_ext。

这意味着当您想将 a 实例graph化为类型类时，您实际上需要实例化底层类型'a graph_ext。这可以按如下方式完成：

instantiation graph_ext :: (type) ord
begin
  instance ..
end

尽管您可能还想为该ord类型提供一些定义，可能如下所示：

instantiation graph_ext :: (type) ord
begin
  definition "less_eq_graph_ext (G :: 'a graph_ext) (H :: 'a graph_ext) ≡
           nodes G ⊆ nodes H ∧ edges G ⊆ edges H"
  definition "less_graph_ext (G :: 'a graph_ext) (H :: 'a graph_ext)
         ≡ (nodes G ⊆ nodes H ∧ edges G ⊆ edges H) ∧
                 ¬ (nodes H ⊆ nodes G ∧ edges H ⊆ edges G)"
  instance ..
end

一旦'a graph_ext被实例化到类ord中，你的最终引理类型检查（虽然要实际执行证明，你可能需要做更多的工作，例如实例化'a graph_ext到preorderororder类。）

于 2013-08-01T00:16:38.193 回答