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)
then supply this to simple_eq_match_conv you get
a conversion which will rewrite using the equation
and instantiate the assumption P(x,y) appropriately.
If you use that in a tactic the assumptions will get
subgoaled.
If you have a conversion which does that you can
apply it to get the relevant conditions (Ps), use that
to infer the corresponding equations (A=Bs) and add them
into the assumptions.
i.e. you get instances of:
P(x,y) |- A(x,y) = B(x,y)
which you asm_tac causing the equations to go into the
assumptions and the conditions to be subgoaled.
That's reasonably simple!
Probably not very intelligible, but I can fill out the details if necessary.
Roger
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
