时间戳

首页 > 解决方案 > Isabelle/Simpl：使用 hoarestate 类型统一失败

isabelle - Isabelle/Simpl：使用 hoarestate 类型统一失败

问题描述

我开始使用 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 本身（包括其用户指南）成功编译。我怎样才能让它通过？

标签： isabelle

解决方案

正如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_'在记录N中而不是在 hoarestate 中，尽管 hoarestate 是稍后定义的。我不知道为什么会这样。

推荐阅读