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