The internal form of a goal-spec
To each goal-spec,
(parse-clause-id "[2]Subgoal *4.5.6/7.8.9'''")
returns
The function
As noted in the documentation for goal-spec, each clause printed in
the theorem prover's proof attempt is identified by a name. When these names
are represented as strings they are called ``goal specs.'' Such strings are
used to specify where in the proof attempt a given hint is to be applied. The
function
Examples of goal-specs and their corresponding clause identifiers are shown below.
parse-clause-id --> "Goal" ((0) NIL . 0) "Subgoal 3.2.1'" ((0) (3 2 1) . 1) "[2]Subgoal *4.5.6/7.8.9'''" ((2 4 5 6) (7 8 9) . 3) <-- string-for-tilde-@-clause-id-phrase
The caar of a clause id specifies the forcing round, the cdar specifies the goal being proved by induction, the cadr specifies the particular subgoal, and the cddr is the number of primes in that subgoal.
Internally, the system maintains clause ids, not goal-specs. The system prints clause ids in the form shown by goal-specs. When a goal-spec is used in a hint, it is parsed (before the proof attempt begins) into a clause id. During the proof attempt, the system watches for the clause id and uses the corresponding hint when the id arises. (Because of the expense of creating and garbage collecting a lot of strings, this design is more efficient than the alternative.)