isabelle - Eisbach 中具有自定义规则的案例

Question

我写了这条规则：

method rule_inversion uses P = 
  (cases rule: nt_network[OF P])

但伊莎贝尔告诉我

Rule has fewer premises than arguments given

确切的nt_network似乎并不重要，因为这以同样的方式失败：

method rule_inversion uses R P = 
  (cases rule: R[OF P])

当是策略的参数时，我如何应用OF P用于casesEisbach 内部的规则？P

标签： isabelle