Make progress with evalpc symbolic evaluation.

Two problems dealt with:
* fastwave program was "wrong": a variable "d" was referred to that
  wasn't bound in the initial state (this state being specified in
  evalpc.ML).  Fixed by giving it initial value 0.
* some regressions in the evaluation technology caused by evolution of
  the PC language. Easy fixes.
Add an operational semantics rule to propagate Abort out of Seqs.

Fix correctness proof for semantics.

Also revise definition of graphOf in light of fix to HOL's handling of
pattern-variables in big (case-splitting) definitions.