I forgot to say that the theorem is 'excluded_middle_thm' and its proof is in file 'src/boolclass.ml'.
Mark. on 18/5/15 5:17 PM, Mark <[email protected]> wrote: > 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 > > > ------------------------------------------------------------------------------ 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
