Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <19312.9304211001@frogland.inmos.co.uk>
Subject: Re: nested subgoals
To: coe@panther.cs.uidaho.edu (Mike Coe)
Date: Wed, 21 Apr 1993 11:01:31 +0100 (BST)
Cc: info-hol@ted.cs.uidaho.edu
In-Reply-To: <199304202028.AA20367@panther.cs.uidaho.edu> from "Mike Coe" at Apr 20, 93 01:28:56 pm
Content-Type: text
Content-Length: 1456

Mike Coe has said:
> I am currently doing a very large proof which breaks 
> down into several subgoals.  And each one of 
> those subgoals breaks down into several 
> subgoals and so on.
> 
> It has become so bad I can not keep track 
> of what conditions brought me to the 
> current subgoal.
> 
> Is there a way to make HOL tell me
> what conditions due to 
> BOOL_CASES, ASM_CASES_TAC, or 
> STRUCT_CASES_TAC brought me to 
> the current subgoal?

Have a look at the subgoal contrib package - this claims to do what you
want though I've never used it.

I always run HOL from inside emacs with an editing window and a HOL window
and build up the tactic as I go along. Now that I'm using hol90 I've
extended emacs' sml-mode with some extra support to automatically insert
templates for multi-subgoal splits -- e.g. if STRIP_TAC produced
3 subgoals then M-3 C-C T would add in

	THENL
	[

	  NO_TAC
	 ,

	  NO_TAC
	 ,

	  NO_TAC
	]

At the current point + all the auto-indentation stuff (should) keep the
tactic at the right indentations. I'd expect this would be even neater if
emacs supported folding!

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley