[ProofPower] apply conditional rewriting

2015-06-04 Thread YuHui Lin
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 
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


Re: [ProofPower] apply conditional rewriting

2015-06-04 Thread Roger Bishop Jones
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