Isabelle/Simpl:使用hoarestate进行类型统一失败

Question

我开始使用Isabelle/Simpl，并根据用户指南编写了以下理论：

theory Scratch
  imports Simpl.Simpl
begin

hoarestate newvars =
  N :: nat

lemma (in newvars) "Γ ⊢ {} ´N :== ´N + 1 {}"
  sorry
end

但Isabelle抱怨类型统一失败：

Type unification failed

Type error in application: operator not of function type

Operator:  N_' :: 'a
Operand:   s :: ??'a

Simpl本身(包括它的用户指南)成功编译。我怎么才能让它通过呢？

Answer 1

正如Javier Díaz指出的那样，只导入Simpl.Vcg而不是Simpl.Simpl就可以了。

错误的原因似乎是与Simpl.SyntaxTest中定义的记录的名称冲突。它包含以下记录定义：

record 'g vars = "'g state" +
  A_' :: "nat list"
  AA_' :: "nat list list"
  I_' :: nat
  M_' :: nat
  N_' :: nat
  R_' :: int
  S_' :: int
  B_' :: bool
  Abr_':: string
  p_' :: ref
  q_' :: ref

Isabelle似乎更喜欢记录中的N_'而不是hoarestate中的N，尽管hoarestate是在稍后定义的。我不知道为什么会这样。