[ProofPower] tactic in backward reasoning for rewrite rules with conditions

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 ge

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

On 23/09/15 13:03, Lin, Yuhui wrote: > 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 >

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

Further to my last on this topic, I now see that simple_eq_match_conv already does what is needed for the solution of the first approximation to the requirement. If you take a theorem of the form: forall x, y. P(x,y) ==> A(x,y) = B(x,y) and infer: P(x,y) |- A(x,y) = B(x,y) the