Dear Robert,
i guess that you are working on hol-light theorem prover. To understand the
proof script, there is a very good tool for hol-light, which can help you
to flatten the packed-up form of Excludded_Middle proof. The link of the
tool is as below:
http://www.proof-technologies.com/tactician/
On Fri, May 15, 2015 at 9:58 PM, Robert White <[email protected]
> wrote:
>
> Dear Sir/Madam,
>
> I wonder if you could explain a bit of the last step of the proof of law
> of excluded middle (in the file class.ml). I am not sure how the
> rewriting magically converted
>
> 0 [`F <=> (@x. (x <=> F) \/ t)`]
> 1 [`T <=> (@x. (x <=> T) \/ t)`]
> 2 [`t`]
>
> `~((@x. (x <=> T) \/ t) <=> (@x. (x <=> F) \/ t)) ==> (@x. (x <=> F) \/ t)`
>
> to `t \/ ~t`
>
> The proof is as follows:
>
>
> let EXCLUDED_MIDDLE = prove
> (`!t. t \/ ~t`,
> GEN_TAC THEN SUBGOAL_THEN
> `(((@x. (x <=> F) \/ t) <=> F) \/ t) /\ (((@x. (x <=> T) \/ t) <=> T)
> \/ t)`
> MP_TAC THENL
> [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL
> [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN
> DISJ1_TAC THEN REFL_TAC;
> DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
> TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN
> DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN
> PURE_ONCE_ASM_REWRITE_TAC[] THEN
> * ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;*
>
> PS: Is there a way I can print out how it is done step by step form OCaml
> Toplevel?
>
> Thanks very much!
> --
>
> 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
>
>
--
Thanks and best regards,
Waqar Ahmed
Ph.D Candidate,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad,
Pakistan
------------------------------------------------------------------------------
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
