Hello Robert,
If you're interested in the proof itself, rather than how in how the HOL
Light one works, then there's also a proof in HOL Zero which could help.
This follows the same idea but is a "forwards proof" in terms of basic
inference rule steps rather than tactics, but might (or might not..) be more
understandable. Download the HOL Zero source distribution from:
http://www.proof-technologies.com/holzero/
Best,
Mark.
on 15/5/15 11:22 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
>
>
>
------------------------------------------------------------------------------
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
