Some housekeeping changes to do with action graphs.

1. Actions can take lists of writes.  What they do with those writes
   is unspecified; some later apply_action function has the
   responsibility to apply the contents of the type to whatever is
   being updated.

2. The "iter" field is renamed to "ident" and the "expr" field is
   renamed to "data".

This is all looking forward to supporting graphs with nodes that are
themselves graphs.

Proofs have all been made to work again.
Clean up theories: delete cruft; move lemmas to appropriate theories.

Some lemmas may migrate to core HOL eventually.