-1

我正在尝试将“s”应用于我的通用量词，以将假设列表操作为 P(s) ==> M(s), P(s) 的形式，然后证明 M(s)。

到目前为止，这是我所拥有的：

set_goal([``!(x:'a).(P(x) ==> M(x))``,``(P:'a->bool)(s:'a)``], ``(M:'a->bool)(s:'a)``);
e(PAT_ASSUM ``!x.'a`` (fn th => (ASSUME_TAC (SPEC ``s`` th))));

目标堆栈：

 Incomplete goalstack:
 Initial goal:

 (M :'a -> bool) (s :'a)
 ------------------------------------
   0.  (P :'a -> bool) (s :'a)
   1.  !(x :'a). (P :'a -> bool) x ==> (M :'a -> bool) x

扩展 PAT_ASSUM 时，我收到此错误提示 Alpha 'a.

> Exception-
   HOL_ERR
     {message =
      "on line 89, characters 17-18:\nLexical error - Term idents can't begin with prime characters",
      origin_function = "Absyn", origin_structure = "Parse"} raised

我知道要解决剩下的问题，另一个 PAT_ASSUM 将用于A ==> B该模式，我运行 IMP_ELIM，这部分是简单的部分。我只是在努力通过显示 s 是 'a.

4

0 回答 0