我花了一些时间使用 HOL 中的定理库构建“前向证明”。我现在希望转向应用策略来制作“向后证明”。
我想知道是否有一种方法可以在应用策略后查看该策略应用的定理列表，即详细重建前向证明。这主要是为了帮助我理解战术是如何运作的。
例如：
> g `x = 5 ==> 2*x = 10`;
val it = ...
> e (rw[]);
OK...
.
.
.
|- x = 5 ==> 2 * x = 10: proof
>
>
> list_steps(); (* or something similar? *)
REWRITE_RULE [...] t1
REWRITE_RULE [MULT] t2
REWRITE_RULE [MULT_ZERO] t3...
etc.
谢谢！