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
