1

コードジェネレーターを試しています。私の理論には、不変式をエンコードするデータ型が含まれています。

typedef small = "{x::nat. x < 10}" morphisms to_nat small
  by (rule exI[where x = 0], simp)

definition "is_one x ⟷ x = small 1"

のコードをエクスポートしたいと思いますis_one。まず、コード ジェネレーターのデータ型を次のように設定する必要があるようです。

code_datatype small

instantiation small :: equal
begin
  definition "HOL.equal a b ⟷ to_nat a = to_nat b" 
  instance
  apply default
  unfolding equal_small_def
  apply (rule to_nat_inject)
  done
end

lemma [code abstype]: "small (to_nat x) = x" by (rule to_nat_inverse)

そして今is_one、抽象化に違反しないためのコード方程式を定義することができます:

definition [code del]:"small_one = small 1"
declare is_one_def[code del]
lemma [code]: "is_one x ⟷ x = small_one" unfolding is_one_def small_one_def..
lemma [code abstract]: "to_nat small_one = 1"
  unfolding small_one_def by (rule small_inverse, simp)

export_code is_one in Haskell file -

質問 1:の定義をsmall_oneから引き出さないようにすることはできますis_oneか?

これで、小さなアイテムの複合値が得られました。

definition foo :: "small set list" where "foo = [ {small (10-i), small i} . i <- [2,3,4] ]"

その形式では、それを使用してコードをエクスポートできません (「コード式 foo の抽象化違反...」)。

質問 2:[code abstract]そのような値のレンマを定義するにはどうすればよいですか? コード ジェネレーターは、形式の補題を受け入れないようmap to_nat foo = ...です。

4

2 に答える 2

3

code_abstractなどによって宣言された不変条件を持つ型smallの場合、コード式に抽象化関数を含めることはできませんsmall。したがって、 の等値テストis_oneを type で表現したい場合は、まずsmallの定数を定義しsmall 1、対応するコード方程式を証明する必要がありますto_nat。これはあなたがしたことです。ただし、表現型で同等性を使用する方が簡単です。natつまり、実装をインライン化しますequal_class.equal。equalその場合、どちらもインスタンス化する必要はありませんsmall。

lemma is_one_code [code]: "is_one x ⟷ to_nat x = 1"
by(cases x)(simp add: is_one_def small_inject small_inverse)

パッケージは、このliftingほとんどを自動的に行います。

setup_lifting type_definition_small
lift_definition is_one :: "small => bool" is "%x. x = 1" ..
export_code is_one in SML file -

残念ながら、コード ジェネレーターは、 のような抽象型を含む複合戻り型をサポートしていませんsmall set list。Isabelle/HOL の Data Refinement で説明されているように、セクション。3.2では、型を独自のsmall set list型コンストラクターとしてラップし、 typeで定義する必要があります。次に、型はinvariant のように表されます。small_set_listfoosmall_set_listsmall_set_listnat set listlist_all (%A. ALL x:A. x < 10)

于 2013-04-16T15:46:53.647 に答える
0

Andreas の説明と包括的な解決策に加えて、新しい型の導入を回避する回避策を見つけました。Assumfooは多くの場所では使用されていません。

definition "in_foo x = (∀s ∈ set foo. x ∈ s)"

のコードをエクスポートしようとするとin_foo、「抽象化違反」エラーが発生します。しかし、プログラムを改良することで、問題のあるコードを回避できます。

code_thmsがどのように使われているかを調べるために使用しfoo、それが として使用されていることを発見しましたlist_all (op ∈ ?x) foo。fooここで、言及せずにのこの特定の使用法を書き直しますsmall。

lemma [code_unfold]:
  "list_all (op ∈ x) foo ⟷
    list_all (op ∈ (to_nat x))  [ {(10-i), i} . i <- [2, 3, 4] ]"
  unfolding foo_def by (auto simp add: small_inverse small_inject)

foo(を使用して定義しlift_definitionた場合、後の証明apply transferはさらに簡単になります。)

fooのすべてのメンバーがの不変式を満たすことを基本的に捉えるこの変換の後small、コード エクスポートは意図したとおりに機能します。

export_code in_foo in Haskell file -
于 2013-04-16T19:49:45.820 に答える