### [ProofPower] apply conditional rewriting

```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]

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

Many thanks

best,
Yuhui

-
We invite research leaders and ambitious early career researchers to
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

```

### Re: [ProofPower] apply conditional rewriting

```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