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  lockwood@ecs.syr.edu  (315)443-3046  Rm. 4-125 CST
Emeritus Professor  Dept. of EECS  Syracuse University  Syracuse NY

On Thu, 31 Jan 2008 tjohnson2059@comcast.net 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?