Continuing to answer my own questions ... I went back to Isabelle and found
that it has been evolving very nicely, and that very large scale proofs
about programs have been accomplished using it. One still has to know what
one is doing but it is no longer a matter of juggling chainsaws.
The Is
Apparently the answer to my last question is "yes". Since I originally
studied the Sage tutorials a couple of years ago "var" has been extended to
attache a domain to variables. Still reading up on it, it's connected to
the assumptions mechanism and simplify method. I used all of the above in
