Как сгенерировать код для квантификатора уникальности - PullRequest
Новая
       4

Как сгенерировать код для квантификатора уникальности

1 голос
/ 05 марта 2019

Вот пример теории: 

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.

Не могли бы вы предложить, как определить такой предикат?

1 Ответ

0 голосов
/ 05 марта 2019

Я понял.Я не должен использовать оператор 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)
...