Eisbach term parameters and subgoal_tac

Question

I'm currently trying to get into Eisbach.

How can I achieve that in the subgoal_tac (see below) the value of the parameter A is used, and that A is not interpreted as some variable name? Is there some general way to do this or would this need special tailoring of the subgoal_tac tactic?

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

Peter Zeller Peter Zeller · Accepted Answer · 2020-02-27T14:16:27

I don't know why it does not work with subgoal_tac. I think I read somewhere that all methods ending with _tac are kind of deprecated now.

As a workaround you could use a Lemma:

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
*)

Eisbach term parameters and subgoal_tac

1 Answers