艾斯巴赫项参数和 subgoal_tac

Question

我目前正在努力进入艾斯巴赫。

如何在 subgoal_tac（见下文）中实现该值使用了参数 A 的，并且 A 没有被解释为某个变量名？是否有一些通用的方法可以做到这一点，或者这是否需要对 subgoal_tac 策略进行特殊定制？

theory Scratch (* Isabelle2019 *)
imports
Main
"HOL-Eisbach.Eisbach"
begin

method test for A :: nat =
  subgoal_tac "A = 5"

lemma "True"
  apply (test 1)
(* 
proof (prove)
goal (2 subgoals):
 1. A = 5 ⟹ True
 2. A = 5
 *)
(* The A has a yellow background in the output pane*)
  oops

end

Answer 1

我不知道为什么它不适用于 subgoal_tac。我想我在某处读到过所有以 _tac 结尾的方法现在都已被弃用。

作为解决方法，您可以使用引理：

method test for A :: nat =
  (rule meta_mp[where P="A = 5"])

lemma "True"
  apply (test 1)
(*
goal (2 subgoals):
 1. 1 = 5 ⟹ True
 2. 1 = 5
*)

艾斯巴赫项参数和 subgoal_tac

Eisbach term parameters and subgoal_tac

isabelle