"CONJ_TAC" splits your goal into two subgoals and you need to specify
which lines of the subsequent code correspond to the first subgoal and
which ones are for verifying the second one.
This can be done in a number of ways. But, the most straight forward one
would be to use THENL as follows:
val thm3 = prove( (--`(B ==> (A ==> ( A /\ B )))`--),
DISCH_TAC THEN
DISCH_TAC THEN
CONJ_TAC THENL [
(UNDISCH_TAC (--`A:bool`--)) THEN
(ACCEPT_TAC ((DISCH_ALL (ASSUME (--`A:bool`--))))),
(UNDISCH_TAC (--`B:bool`--)) THEN
(ACCEPT_TAC (DISCH_ALL (ASSUME (--`B:bool`--))))]);
So after CONJ_TAC, we use a THENL and the start a square bracket. All the
lines until "," are for proving the first subgoal and the lines of code
after the "," until "]" are for the second subgoal. You can read more
about THENL from the manual. It would be good to read about THEN1 as well.
--Osman
On Sun, 19 Jul 2009, Tony Johnson wrote:
> Hi,
>
> In the proof I have here, I took each instruction, and applied it in
> sequence in the proof manager which worked. However the below doesn't
> work. Is there something to the THEN tactical that I'm not
> understanding?
>
> Thanks!
>
> (* prove |- (A ==> (B ==> ( A /\ B ))) in a backwards proof *)
> val thm3 = prove( (--`(B ==> (A ==> ( A /\ B )))`--),
> DISCH_TAC THEN
> DISCH_TAC THEN
> CONJ_TAC THEN
> (UNDISCH_TAC (--`A:bool`--)) THEN
> (ACCEPT_TAC ((DISCH_ALL (ASSUME (--`A:bool`--)))))THEN
> (UNDISCH_TAC (--`B:bool`--)) THEN
> (ACCEPT_TAC (DISCH_ALL (ASSUME (--`B:bool`--))))));
>
>
>
> ------------------------------------------------------------------------------
> Enter the BlackBerry Developer Challenge
> This is your chance to win up to $100,000 in prizes! For a limited time,
> vendors submitting new applications to BlackBerry App World(TM) will have
> the opportunity to enter the BlackBerry Developer Challenge. See full prize
> details at: http://p.sf.net/sfu/Challenge
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Enter the BlackBerry Developer Challenge
This is your chance to win up to $100,000 in prizes! For a limited time,
vendors submitting new applications to BlackBerry App World(TM) will have
the opportunity to enter the BlackBerry Developer Challenge. See full prize
details at: http://p.sf.net/sfu/Challenge
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
