これは、 Isabelle のコード生成: コンテナーの抽象化レンマ? のフォローアップです。:
the_question次の理論でコードを生成したい：
theory Scratch imports Main begin
typedef small = "{x::nat. x < 10}" morphisms to_nat small
by (rule exI[where x = 0], simp)
code_datatype small
lemma [code abstype]: "small (to_nat x) = x" by (rule to_nat_inverse)
definition a_pred :: "small ⇒ bool"
where "a_pred = undefined"
definition "smaller j = [small i . i <- [0 ..< to_nat j]]"
definition "the_question j = (∀i ∈ set (smaller j). a_pred j)"
問題は、 の式がsmaller抽象化関数に言及しているため、コード生成に適していないことsmallです。
私の最後の質問に対する Andreas の回答とデータの洗練に関する論文によると、次のステップは、小さな数のセットの型を導入しsmaller、その型の定義を作成することです。
typedef small_list = "{l. ∀x∈ set l. (x::nat) < 10}" by (rule exI[where x = "[]"], auto)
code_datatype Abs_small_list
lemma [code abstype]: "Abs_small_list (Rep_small_list x) = x" by (rule Rep_small_list_inverse)
definition "smaller' j = Abs_small_list [ i . i <- [0 ..< to_nat j]]"
lemma smaller'_code[code abstract]: "Rep_small_list (smaller' j) = [ i . i <- [0 ..< to_nat j]]"
unfolding smaller'_def
by (rule Abs_small_list_inverse, cases j, auto elim: less_trans simp add: small_inverse)
smaller'実行可能になりました。私が理解していることから、上の操作を次の操作として再定義する必要がありますsmall list。small_list
definition "small_list_all P l = list_all P (map small (Rep_small_list l))"
lemma[code]: "the_question j = small_list_all a_pred (smaller' j)"
unfolding small_list_all_def the_question_def smaller'_code smaller_def Ball_set by simp
の見栄えの良いコード式を定義できますthe_question。しかし、 の定義はsmall_list_all抽象化モーフィズムに言及しているため、コード生成には適していませんsmall。small_list_all実行可能にする方法を教えてください。
a_pred(問題は実際に再帰的な のコード方程式で実際に発生するため、のコード方程式を展開できないことに注意してくださいa_pred。また、実行時に不変条件を再チェックすることを含むハックを避けたいと思います。)