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
