I want to write a tactic to performance the following action,
assume that the goal is
h_1, … h_n |- g
and thm is
forall x, y. P(x,y) ==> A(x,y) = B(x,y)
where A(x,y) can be matched with a subterm of the current goal. After applying
the tactic, the following subgoals are generated:
1)h_1, … h_n, A(x’,y') = B(x’,y') |- g
2) h_1, … h_n |- P(x’,y’)
where x and y are instantiated as the related terms (x’ and y') in the matched
Is there any existing function I can use? If not, how can I write such a tactic
? Thanks in advance.
We invite research leaders and ambitious early career researchers to
join us in leading and driving research in key inter-disciplinary themes.
Please see www.hw.ac.uk/researchleaders for further information and how
Heriot-Watt University is a Scottish charity
registered under charity number SC000278.
Proofpower mailing list