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
package had
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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
