如何使用 Isabelle 的 code_pred 和 values 命令？

Question

Tobias Nipkow 和 Gerwin Klein 在 "Concrete Semantics" 的第 7.2.2 节中有一个 code_pred 用法的示例。我基于示例实现了一种简单的语言，并尝试计算表达式的值：

theory BooLang
  imports Main
begin

type_synonym id = string
type_synonym 'a Env = "id ⇒ 'a"

datatype BooBoolExp =
  BooLiteralExp bool |
  BooLetExp id BooBoolExp BooBoolExp |
  BooVarExp id |
  BooAndExp BooBoolExp BooBoolExp

datatype BooVal = Bv bool

type_synonym BooEnv = "BooVal Env"

inductive tbooval :: "BooBoolExp × BooEnv ⇒ BooVal ⇒ bool" (infix "⇒" 55) where
  Literal: "(BooLiteralExp b, env) ⇒ Bv b" |
  And: "⟦(a, env) ⇒ Bv av; (b, env) ⇒ Bv bv⟧ ⟹ (BooAndExp a b, env) ⇒ Bv (av ∧ bv)" |
  Var: "(BooVarExp v, env) ⇒ env v" |
  Let: "⟦(val, env) ⇒ b; (body, env(v := b)) ⇒ x⟧ ⟹ (BooLetExp v val body, env) ⇒ x"

code_pred tbooval .

values "{t. True}"

values "{t. (BooLiteralExp true, λ_. Bv false) ⇒ t}"

end

但是对于第一个值的调用我得到了错误：

Evaluation with values is not possible because compilation with code_pred was not invoked.

对于第二个，我得到错误：

No mode possible for comprehension {t. (BooLiteralExp true, λ_. Bv false) ⇒ t}.

我的理论有什么问题？

Answer 1

第一个命令values {t. True}无法工作，因为此命令要求伊莎贝尔枚举t类型的所有值，该类型被推断为类型变量'a；这是做不到的。

对于第二个命令，您只是拼错了 True 和 False。照原样，true 和 false 被推断为布尔变量而不是布尔常量。与value不同，命令values在Isabelle2016-1中不支持符号执行。也就是说，归纳谓词的所有输入参数必须是没有变量的基础值。在您的示例中， code_pred 推断出两种执行模式：一种是将所有内容都作为输入，另一种是仅将第一个参数作为输入。您可以通过传递 [show_modes] 选项来查看推断模式，如

 code_pred [show_modes] tboolval .

您可以在 code generator tutorial.

中找到有关 code_pred 和 values 的更多文档

如何使用 Isabelle 的 code_pred 和 values 命令？

How to use Isabelle's code_pred and values commands?

isabelle