Как сгенерировать код для операции less_eq - PullRequest
Новая
       10

Как сгенерировать код для операции less_eq

0 голосов
/ 09 января 2019

Мне нужно сгенерировать код, вычисляющий все значения, которые больше или равны некоторому значению: 

datatype ty = A | B | C

instantiation ty :: order
begin

fun less_ty where
  "A < x = (x = C)"
| "B < x = (x = C)"
| "C < x = False"

definition "(x :: ty) ≤ y ≡ x = y ∨ x < y"

instance
  apply intro_classes
  apply (metis less_eq_ty_def less_ty.elims(2) ty.distinct(3) ty.distinct(5))
  apply (simp add: less_eq_ty_def)
  apply (metis less_eq_ty_def less_ty.elims(2))
  using less_eq_ty_def less_ty.elims(2) by fastforce

end

instantiation ty :: enum
begin

definition [simp]: "enum_ty ≡ [A, B, C]"
definition [simp]: "enum_all_ty P ≡ P A ∧ P B ∧ P C"
definition [simp]: "enum_ex_ty P ≡ P A ∨ P B ∨ P C" 

instance
  apply intro_classes
  apply auto
  by (case_tac x, auto)+

end

lemma less_eq_code_predI [code_pred_intro]:
  "Predicate_Compile.contains {z. x ≤ z} y ⟹ x ≤ y"
(*  "Predicate_Compile.contains {z. z ≤ y} x ⟹ x ≤ y"*)
  by (simp_all add: Predicate_Compile.contains_def)

code_pred [show_modes] less_eq
  by (simp add: Predicate_Compile.containsI)

values "{x. A ≤ x}"
(* values "{x. x ≤ C}" *)

Работает нормально. Но теория выглядит слишком сложной. Также я не могу вычислить значения, меньшие или равные некоторому значению. Если кто-то откомментирует 2-ю часть less_eq_code_predI леммы, то less_eq будет иметь только один режим i => i => boolpos.

Есть ли более простой и более общий подход?

Может ли less_eq поддерживать i => o => boolpos и o => i => boolpos одновременно?

Можно ли не объявлять ty как экземпляр класса enum? Я могу объявить функцию, возвращающую набор элементов, больший или равный некоторому элементу: 

fun ge_values where
  "ge_values A = {A, C}"
| "ge_values B = {B, C}"
| "ge_values C = {C}"

lemma ge_values_eq_less_eq_ty:
  "{y. x ≤ y} = ge_values x"
  by (cases x; auto simp add: dual_order.order_iff_strict)

Это позволило бы мне удалить вещи enum и code_pred. Но в этом случае я не смогу использовать эту функцию в определении других предикатов. Как заменить (≤) на ge_values в следующем определении? 

inductive pred1 where
  "x ≤ y ⟹ pred1 x y"

code_pred [show_modes] pred1 .

Мне нужно, чтобы pred1 имел как минимум режим i => o => boolpos.

1 Ответ

0 голосов
/ 10 января 2019

Компилятор предикатов имеет опцию inductify, которая пытается преобразовать функциональные определения в индуктивные. Это несколько экспериментально и не работает в каждом случае, поэтому используйте его с осторожностью. В приведенном выше примере классы типов усложняют ситуацию в целом. Вот что мне удалось получить: 

case_of_simps less_ty_alt: less_ty.simps

definition less_ty' :: "ty ⇒ ty ⇒ bool" where "less_ty' = (<)"

declare less_ty_alt [folded less_ty'_def, code_pred_def]

code_pred [inductify, show_modes] "less_ty'" .

values "{x. less_ty' A x}"
  1. Первая строка преобразует уравнения сопоставления с образцом в уравнение с регистром справа. Используется команда case_of_simps из HOL-Library.Simps_Case_Conv.
  2. К сожалению, предикатный компилятор, похоже, испытывает проблемы с компиляцией операций с классами типов. По крайней мере, я не мог заставить его работать. Итак, вторая строка вводит новую константу для (<) на ty.
  3. Атрибут code_pred_def указывает компилятору предиката использовать данную теорему (а именно less_ty_alt с less_ty' вместо (<)) в качестве «определяющего уравнения».
  4. code_pred с опцией inductify просматривает уравнение для less_ty', объявленное code_pred_def, и выводит из этого индуктивное определение. inductify обычно хорошо работает с выражениями, конструкторами и квантификаторами. Все, что за этим, вы на свой страх и риск.

Кроме того, вы также можете вручную реализовать перечисление, аналогичное ge_values, и зарегистрировать соединение между (<) и ge_values с помощью компилятора предикатов. См. Блок setup в конце теории Predicate_Compile в дистрибутиве для примера с Predicate.contains. Однако обратите внимание, что компилятор предикатов работает лучше всего с предикатами , а не с sets . Таким образом, вам нужно написать ge_values в предикатной монаде Predicate.pred.

...