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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to