markerLib: make the theorem-list directive vocabulary a datatype

[lukaszcz]

Issue

Theorems passed in a tactic's or simpset's theorem list can be
directives rather than facts: AC, Cong, Excl, ExclSF, FRAG,
Req0, ReqD, Once/Ntimes, NoAsms, IgnAsm, Abbr and label
references. markerLib constructs most of them but offered no way to
enumerate or classify them. Each consumer restated the part of the
vocabulary it happened to know:

• simpLib.process_tags had its own is_AC/is_Cong head tests plus
  two hand-rolled extraction loops for Excl/ExclSF and FRAG.
• markerLib.dest_tacmarked knew only the tactic-level directives
  (NoAsms, IgnAsm, Abbr, labels).
• mk_require_tac knew only Req0/ReqD.

Nothing tied these together, and a directive that reached a consumer
which did not know it was not rejected: it fell through as an ordinary
rewrite. The failure is silent and directional. Concretely, on
develop:

SIMP_CONV bool_ss [Req0 (ASSUME “q”)] “q”;
(* [q, marker$Req0] |- q <=> T *)

The marker$Req0 hypothesis is carried into the result and nothing
ever discharges it. SIMP_RULE behaves the same way. NoAsms and
IgnAsm became vacuous rewrites (NoAsms <=> T). Every tactic entry
point strips these markers before the simpset layer, so the leak only
shows up at the conversion/rule level, but there it is undetectable
without inspecting hypotheses.

A second, independent instance surfaced while pinning the fix:
BoundedRewrites.DEST_BOUNDED searched the hypothesis set with
aconv bounded_tm o rator, which raises on any hypothesis that is not
an application. So for a theorem with a variable hypothesis,

Once (ASSUME “p:bool”)

was silently treated as unbounded by the rewriter and its BOUNDED
hypothesis leaked into every rewrite result.

Adding a directive obliged nobody to touch any list, so nothing
detected either omission at compile time. A downstream branch
(isabelle-tactics) already hit the classical-rule variant of this,
where an unrecognised directive is added to a claset as a logical rule.

Fix

markerLib now owns the vocabulary as a closed datatype:

datatype directive =
    DAC of thm * thm | DCong of thm
  | DExcl of string | DExclSF of string | DFRAG of string
  | DReq0 of thm | DReqD of thm | DBounded of thm * int
  | DNoAsms | DIgnAsm of string | DAbbr of string | DLabel of string
val dest_directive : thm -> directive option
val is_directive   : thm -> bool

Hypothesis-carried wrappers (Req0, ReqD, bounds) are reported before
the payload's own head, so consumers strip them first.
dest_tacmarked is now a projection of dest_directive, so there is a
single recogniser.

simpLib.process_tags becomes one fold over the datatype with an
explicit policy for every constructor:

• Cong/AC/Excl/ExclSF/FRAG: honoured as before.
• Req0/ReqD: refused with a process_tags error. Every tactic
  strips them via mk_require_tac before reaching here, so one that
  arrives can only corrupt the result.
• NoAsms/IgnAsm/Abbr/labels: dropped. These are the tactic
  layer's, but FULL_SIMP_TAC legitimately lets them reach SIMP_RULE
  for the assumptions, so they cannot be errors.
• Once/Ntimes: passed through; the rewriter honours them.

Because the type is closed, a consumer that dispatches with case
gets a non-exhaustive-match warning when a constructor is added, which
is the compile-time check that was missing. simpLib's private
is_AC, is_Cong, extract_excls and extract_frags are removed.

DEST_BOUNDED now tests is_comb before taking the rator.

Tests

• src/marker/selftest.sml: every constructor is recognised with the
  identity and payload its consumer needs; wrapper ordering
  (Req0 (Cong th)); five non-directives (including a plain reflexive
  equation and an equation over a marker$ constant) are rejected.
• src/simp/src/selftest.sml: SIMP_CONV refuses Req0/ReqD and
  leaves the term unchanged for NoAsms/IgnAsm.
• src/1/selftest.sml: DEST_BOUNDED finds the bound past a variable
  hypothesis (fails against the old code).

[mn200]

Very appealing; thanks! Please fix merge conflicts.