Major Section: MISCELLANEOUS
To each goal-spec,
str, there corresponds a clause-identifier
(parse-clause-id str). For example,
(parse-clause-id "Subgoal *4.5.6/7.8.9'''")returns
((2 4 5 6) (7 8 9) . 3).
parse-clause-id in the sense that given a clause identifier it
returns the corresponding goal-spec.
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
parse-clause-id converts goal-specs into clause identifiers,
which are cons-trees containing natural numbers.
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) "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.)