Hi again :)
I meant to say , when we want to prove D |- A , we prove D |- A=B and D |-
B but not top down, instead, in a bottom-up fashion.
So yeah. Your reply has surely solved the problem.
Thanks for this fast reply :)
Regards,
Robert
On 21 May 2015 at 14:43, Petros Papapanagiotou <[email protected]> wrote:
> 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.
>
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
------------------------------------------------------------------------------
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
