如何为唯一性量词生成代码

Question

这是一个示例理论：

datatype ty = A | B | C

inductive test where
  "test A B"
| "test B B"
| "test B C"

inductive test2 where
  "The (λy. test x y) = y ⟹
   test2 x y"

code_pred [show_modes] test2 .

values "{x. test2 A x}"

生成的代码尝试枚举 ty 并失败（如）。我无法使数据类型成为 enum.

的实例

生成以下代码方程：

test2_i_o ?xa ≡
  Predicate.bind (Predicate.single ?xa)
    (λxa. Predicate.bind (eq_i_o (The (test xa))) Predicate.single

我想这个错误是因为方程包含 test 而不是 test_i_o.

你能建议如何定义这样的谓词吗？

Answer 1

我明白了。我不应该使用 The 运算符。谓词应定义如下。使用 inductify 指令可以很好地生成代码。在这种情况下会生成一个辅助谓词。

inductive test_uniq where
  "test x y ⟹
   (∀z. test x z ⟶ y = z) ⟹
   test_uniq x y"

code_pred [inductify, show_modes] test_uniq .

或者可以显式定义辅助谓词：

inductive test_not_uniq where
  "test x z ⟹
   y ≠ z ⟹
   test_not_uniq x y"

inductive test_uniq where
  "test x y ⟹
   ¬ test_not_uniq x y ⟹
   test_uniq x y"

code_pred [show_modes] test_uniq .

旧的错误答案

也许它可以帮助某人为 The 运算符生成代码：

inductive test_ex where
  "The (λy. test x y) = y ⟹
   test_ex x y"

code_pred [show_modes] test .

lemma test_ex_code [code_pred_intro]:
  "Predicate.the (test_i_o x) = y ⟹
   test_ex x y"
  by (rule test_ex.intros) (simp add: Predicate.the_def test_i_o_def)

code_pred [show_modes] test_ex
  by (metis test_ex.cases test_ex_code)

inductive test2 where
  "test_ex x y ⟹
   test2 x y"

code_pred [show_modes] test2 .

values "{x. test2 A x}"

代码方程现在包含 test_i_o 而不是 test:

test_ex_i_o ?xa =
  Predicate.bind (Predicate.single ?xa)
    (λxa. Predicate.bind (eq_i_o (Predicate.the (test_i_o xa))) Predicate.single)

如何为唯一性量词生成代码

How to generate code for the uniqueness quantifier

isabelle