Dear Robert,
I don't think that HOL Light has such a tactic, but it is not difficult to
implement it (see below).
For everyday work, you may want to delegate this kind of low-level logical
steps to a decision procedure like MESON.
For instance:
g `(a <=> b) /\ a ==> b`;;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `a:bool` (fun th -> ASM_MESON_TAC[th]));;
If you are lucky and the equality has the right orientation, (i.e. `b <=>
a` instead of `a <=> b`) you can simply use rewriting:
g `(b <=> a) /\ a ==> b`;;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
You can also define yourself a tactic that implements exactly the EQ_MP
rule:
let EQ_MP_TAC =
let pth = MESON [] `(a <=> b) ==> a ==> b` in
fun th -> MATCH_MP_TAC (MATCH_MP pth th);;
g `(a <=> b) /\ a ==> b`;;
e (REPEAT STRIP_TAC);;
e (FIRST_X_ASSUM EQ_MP_TAC);;
Personally I like very much the following tactic (not part of HOL Light)
for this kind of situations:
let CUT_TAC : term -> tactic =
let th = MESON [] `(p ==> q) /\ p ==> q`
and ptm = `p:bool` in
fun tm -> MATCH_MP_TAC (INST [tm,ptm] th) THEN CONJ_TAC;;
here is how I use it:
g `(b <=> a) /\ a ==> b`;;
e (REPEAT STRIP_TAC);;
e (CUT_TAC `a:bool`);;
e (ASM_REWRITE_TAC[]);;
Marco
2015-05-21 14:43 GMT+02:00 Petros Papapanagiotou <[email protected]>:
> Dear Robert,
>
> I am not sure what you are trying to accomplish. Do you have an example
> goal?
>
> Again, there may be better ways of doing this, but I keep this useful
> (though sometimes confusing) shortcut handy:
>
> let EQ_MP_THEN thmtc = fun x -> FIRST_ASSUM (fun y -> (thmtc (EQ_MP x
> y)));;
>
> Given a thm_tactic and a theorem thm of the form |- p <=> q it tries to
> use EQ_MP thm with the first matching assumption, then applies the
> thm_tactic to the result.
>
> Trivial example:
> g `p /\ q ==> q /\ p`;;
> e DISCH_TAC;;
> e (EQ_MP_THEN ACCEPT_TAC (SPECL [`p:bool`;`q:bool`] CONJ_SYM));;
>
> or if you want to use an assumed equivalence:
> g `p ==> (p <=> q) ==> q`;;
> e (REPEAT DISCH_TAC);;
> e (FIRST_ASSUM (EQ_MP_THEN ACCEPT_TAC));;
>
> Hope this helps.
>
> Regards,
> Petros
>
>
>
> On 21/05/2015 13:00, Robert White wrote:
> > Dear all,
> >
> >
> > I wonder if there is a way I can use TAC for EQ_MP.
> >
> > I'm sorry I'm not very familiar with bottom up proofs.
> >
> > A1 |- t1 <=> t2 A2 |- t1'
> > ----------------------------- EQ_MP
> > A1 u A2 |- t2
> >
> > Thanks!
> > --
> >
> > Regards,
> > Robert
> >
> >
> >
> ------------------------------------------------------------------------------
> > One dashboard for servers and applications across Physical-Virtual-Cloud
> > Widest out-of-the-box monitoring support with 50+ applications
> > Performance metrics, stats and reports that give you Actionable Insights
> > Deep dive visibility with transaction tracing using APM Insight.
> > http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
> >
> >
> >
> > _______________________________________________
> > hol-info mailing list
> > [email protected]
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
> --
> Petros Papapanagiotou, Ph.D.
> CISA, School of Informatics
> The University of Edinburgh
>
> Email: [email protected]
>
> ---
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
> ------------------------------------------------------------------------------
> One dashboard for servers and applications across Physical-Virtual-Cloud
> Widest out-of-the-box monitoring support with 50+ applications
> Performance metrics, stats and reports that give you Actionable Insights
> Deep dive visibility with transaction tracing using APM Insight.
> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
