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 :: ordや などを入力してみinstantiation graph_ext :: ordましたが、何もうまくいかないようです。何か案は？

4

1 に答える 1

2

レコードgraphが定義されると、舞台裏で新しいタイプ'a graph_extが実際に作成されます。このタイプはレコード タイプと同じですが、追加のデータを追加できるフィールド'aが追加されています (つまり、タイプを持つ新しいフィールドがレコード定義に追加され、後でレコードにデータを追加するために使用できます)。の上）。タイプgraphは単に の略ですunit graph_ext。

これは、grapha を型クラスにインスタンス化する場合、実際には基になる type をインスタンス化する必要があることを意味します'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_extclass にインスタンス化されると、最終補題の型チェックが行われます (ただし、実際に証明を実行するには、またはクラスにインスタンス化するordなど、もう少し作業が必要になる可能性があります)。'a graph_extpreorderorder

于 2013-08-01T00:16:38.193 に答える