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
an equation with extra assumptions, then if you use it as a tactic those
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
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)


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))));
    (lhs, cnv)

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

val cond_rewrite_conv = prim_rewrite_conv
    (Value thm_eqn_cxt1)

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)

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

Proofpower mailing list

Reply via email to