伊莎贝尔-挑剔-自动使用见证值

Question

我如何能够自动使用nitpick找到的值，而不是使用rule exI和手动输入见证值？

  theorem "EX a b. a + b = 5 & a - b = (1 :: int)"
    nitpick [falsify=false]

    (* Nitpicking formula... 
       Nitpick found a model:

       Skolem constants:
       a = 3
       b = 2
    *)

    apply (rule exI[where x="3"])
    apply (rule exI[where x="2"])
    apply (simp)
  done

Answer 1

我不认为功能存在，因为我会说这不是一个典型的用例。

您可能会在nitpick命令中添加这样的东西，只需相对较少的工作量，或者创建一个新的命令来完成它。