On 2015-05-22 04:16 AM, Robert White wrote: > I want to do it mainly because I want to prove things in the form of > ~~A, which means that I need to prove things like (A ==> F) ==> F. > There comes the problem you see.
In natural deduction forward order (HOL4 forward rules in parentheses): Prove ⊢A some way. Also introduce A==>F ⊢ A==>F (ASSUME). Then use ==>-elim (MP) to get A==>F ⊢ F Then ==>-intro (DISCH_ALL) to get ⊢ (A==>F)==>F. In HOL4 in tactical order: You have already used UNDISCH_TAC to get A==>F ?- F There are two methods. First method: MATCH_MP_TAC (ASSUME ``A==>F``) to get A==>F ?- A Now you just have to prove A. Second method: Obtain ⊢ A some way. Call it a_true. Then ASSUME_TAC a_true to get A==>F, A ?- F Then RES_TAC finishes it. ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
