On 04/06/15 10:30, YuHui Lin wrote:
> Hi,
>
> How can I apply a conditional rewrite rule in proof power. For example,
> applying the following thm:
>
> forall x,y, z | x > y dot x - y + z = x + z -y
>
> where x > y is the condition, to generate the following two subgoals:
> 1) x > y
> 2) goal [x - y + z / x + z -y]
There is no comprehensive support for conditional rewriting in ProofPower.
but the simpler cases can be accomplished by forward chaining on the
assumptions and rewriting with the result.
In this case you can use lemma_tac to get two goals then
forward chain using your conditional equation and rewrite
with the result, e.g. FC_T rewrite_tac [conditional_equation].
There is some help in describing the available rewriting
and forward chaining facilities in the HOL Tutorial chapter 7,
and all the facilities can be found in the reference manual
by looking for "fc" or "rewrite" in the KWIC index.
> Also, I wonder is there any interface of this mail list for searching, so
> that i can find possible solutions from previous questions of the mail list
> achieve ?x - y + z = x + z -y
>
Mailman doesn't provide for search.
You can search using google by including:
site:lemma-one.com
in your search expression.
Roger Jones
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
