Fixed a soundness bug from the guard of alpha-char-p, and improved a few related rules.

Quoting :doc note-7-0:

  The guard for function [alpha-char-p] was strengthened to require
  that its argument is a standard character. The previous guard
  required only that the argument is a character, and was a soundness
  bug; for a proof of nil before this fix, see the comment about
  ``alpha-char-p'' in Community Books file system/doc/acl2-doc.lisp,
  form (defxdoc note-7-0 ...).

Here's the comment mentioned just above.

; Here is a proof of nil that exploits the weakeness of the previous guard for
; alpha-char-p.  This proof succeeds in every host Lisp for ACL2 except for GCL
; (and future versions of GCL might also evaluate (alpha-char-p (code-char
; 232)) to true).
;
;   (defthm false-prop
;     (not (alpha-char-p (code-char 232)))
;     :hints (("Goal" :in-theory (e/d (alpha-char-p) ((:e alpha-char-p)))))
;     :rule-classes nil)
;
;   (defthm true-prop
;     (alpha-char-p (code-char 232))
;     :rule-classes nil)
;
;   (defthm contradiction
;     nil
;     :hints (("Goal" :use (true-prop false-prop)))
;     :rule-classes nil)

I noticed that some rules could be improved.  Quoting :doc note-7-0:

  We improved a few built in rules: lower-case-p-char-downcase,
  upper-case-p-char-upcase, lower-case-p-forward-to-alpha-char-p, and
  upper-case-p-forward-to-alpha-char-p. We also improved the rule
  alpha-char-p-forward-to-characterp by replacing it with two rules,
  alpha-char-p-forward-to-standard-char-p and
  standard-char-p-forward-to-characterp. The new rules are, as
  before, in ACL2 source file axioms.lisp.

Note: Passed both "make proofs" and an "everything" ACL2(h)
regression.