如何为 less_eq 操作生成代码

Question

我需要生成一个代码来计算所有大于或等于某个值的值：

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}" *)

它工作正常。但这个理论看起来过于复杂。我也无法计算小于或等于某个值的值。如果取消注释 less_eq_code_predI 引理的第二部分，那么 less_eq 将只有一种模式 i => i => boolpos.

是否有更简单、更通用的方法？

less_eq可以同时支持i => o => boolpos和o => i => boolpos吗？

是否可以不将 ty 声明为 enum class 的实例？我可以声明一个返回一组大于或等于某个元素的元素的函数：

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 模式。

Answer 1

谓词编译器有一个选项inductify，试图将函数定义转换为归纳定义。它有点实验性，并非在所有情况下都有效，因此请谨慎使用。在上面的例子中，类型 classes 使整个情况变得有点复杂。这是我设法开始工作的内容：

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}"

第一行将模式匹配方程转换为右侧带有 case 表达式的方程。它使用来自 HOL-Library.Simps_Case_Conv.

case_of_simps

不幸的是，谓词编译器似乎无法编译类型 class 操作。至少我无法让它工作。所以第二行在 ty.

(<)

属性 code_pred_def 告诉谓词编译器使用给定的定理（即 less_ty_alt 和 less_ty' 而不是 (<)）作为 "defining equation"。
code_pred 和 inductify 选项查看 code_pred_def 声明的 less_ty' 的等式，并从中推导出一个归纳定义。 inductify 通常适用于 case 表达式、构造函数和量词。超出此范围的一切风险由您自行承担。

或者，您也可以手动实现类似于ge_values 的枚举，并使用谓词编译器注册(<) 和ge_values 之间的连接。有关 Predicate.contains 的示例，请参阅分布中 Predicate_Compile 理论末尾的 setup 块。但是请注意，谓词编译器最适合 predicates 而不是 sets。所以你必须在谓词 monad Predicate.pred.

中写 ge_values

如何为 less_eq 操作生成代码

How to generate code for less_eq operation

isabelle