Hi,

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 
subterm.

Is there any existing function I can use? If not, how can I write such a tactic 
? Thanks in advance.

best,
Yuhui

----- 
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
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to