# Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

```On 28/09/15 11:05, Lin, Yuhui wrote:
> Thank you very much. Your solution works perfectly for me. Just be a little
> curious, what dose the following promoted message means when applying the
> tactic
>
>       'Tactics proof introduced the subgoal 2 but did not request it as a
> subgoal"
>
>
That's because the tactic doesn't really work properly, and the goal
to intervene to patch up the proof.
I mentioned in my description of a suggested method that if a conversion
produces
an equation with extra assumptions, then if you use it as a tactic those
assumptions
will get subgoaled.
This is true, and it works, but the tactic is not really doing what it
should and the
subgoal package is fixing the problem,```
```
I thought that was a bit off, and also I wasn't sure that the subgoal
created by
the goal package would always have the right assumptions so I did it
properly,
and include the result, for the record, below,

Its still very crude, some of the choices are arbitrary and not thought out
(like the parameters to prim_rewrite_conv, also the canon could do more)
But it does what was asked for.

(I did it in theory real because there was a nice conditional equation
available there for testing it, it doesn't really need to be there)

Roger

open_theory "%bbR%";

fun thm_eqn_cxt1 (thm : THM) : TERM * CONV = (
let    val cnv = simple_eq_match_conv thm
val lhs = fst(dest_eq(snd(strip_%forall% (concl thm))));
in
(lhs, cnv)
end);

fun cond_rewrite_canon thm = [strip_%implies%_rule (all_%forall%_elim thm)];

val cond_rewrite_conv = prim_rewrite_conv
empty_net
cond_rewrite_canon
(Value thm_eqn_cxt1)
MAP_C
[];

cond_rewrite_conv [%bbR%_over_times_over_thm] %<%2./3.*4./5.%>%;

fun cond_rewrite_tac thm (asml, conc) =
let val thm2 = cond_rewrite_conv [thm] conc
in  MAP_EVERY (fn p => (LEMMA_T p
(fn q => MAP_EVERY asm_tac (forward_chain_rule [thm] [q]))))
(asms thm2)
(asml, conc)
end;

set_goal ([%<%H1:BOOL%>%, %<%H2:BOOL%>%], %<%2./3.*4./5. = 0.%>%);
a(cond_rewrite_tac %bbR%_over_times_over_thm);

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
```