Did you solve it by forwards or backwards reasoning?
On Thu, 2008-01-31 at 15:47 -0500, Lockwood Morris wrote:
> Yes, highly possible, as the following shows. (I apologize for having
> forgotten how to get HOL to show the assumptions as other than dots;
> that accounts for the DISCH_ALL's just so we can see where we are.
> The key move is t1: DISCH is willing to introduce a superfluous
> hypothesis.
>
> val t1 = DISCH (Term`A:bool`) (ASSUME (Term`B:bool`));
> (* [.] |- A ==> B *)
>
> DISCH(Term`B:bool`) t1;
> (* |- B ==> A ==> B *)
>
> val t2 = MP (ASSUME (Term`B ==> A`)) (ASSUME (Term`B:bool`));
> (* [..] |- A *)
>
> DISCH_ALL t2;
> (* |- (B ==> A) ==> B ==> A *)
>
> val t3 =
> MP (ASSUME (Term`(A ==> B) ==> A ==> C`)) (ASSUME (Term`A ==> B`));
> (* [..] |- A ==> C *)
>
> DISCH_ALL t3;
> (* t3' = |- ((A ==> B) ==> A ==> C) ==> (A ==> B) ==> A ==> C *)
>
> val t4 = MP t3 t2;
> (* [....] |- C *)
>
> DISCH_ALL t4;
> (* |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> (A ==> B) ==> B ==> C *)
>
> val t5 = DISCH (Term`A ==> B`) t4;
> (* [...] |- (A ==> B) ==> C *)
>
> DISCH_ALL t5;
> (* |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> B ==> (A ==> B) ==> C *)
>
> val t6 = MP t5 t1;
> (* [...] |- C *)
>
> val t7 = DISCH (Term`(A ==> B) ==> A ==> C`) (DISCH (Term`B ==> A`)
> (DISCH (Term`B:bool`) t6));
> (* t7 = |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> B ==> C *)
>
> Best wishes,
>
> Lockwood
>
> |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-
> Lockwood Morris [EMAIL PROTECTED] (315)443-3046 Rm. 4-125 CST
> Emeritus Professor Dept. of EECS Syracuse University Syracuse NY
>
> On Thu, 31 Jan 2008 [EMAIL PROTECTED] wrote:
>
> > Hi,
> >
> > Given,
> >
> > - val thm1 = DECIDE (--`((A ==> B) ==> (A ==> C)) ==> ((B ==> A) ==> (B ==>
> > C))`--);
> > > val thm1 = [] |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> B ==> C : thm
> >
> > is it possible to prove this theorem using only ASSUME, DISCH, and MP?
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
