Generalize match translation: recursive matcher for complex patterns

[DominicPM]

• Current match translation relies on Basic_Case_Expression which assumes constructor patterns with id/dummy args only.

  • As pattern features expand (nested, or, @, ref/mut, ranges, slices), we need a richer matcher.

  Request

  • Implement a recursive pattern elaboration step that:
    • Generates binder lists for nested patterns
    • Emits constructor tests / literal tests / range tests / guard checks
    • Handles or-patterns (short-circuiting) and @ bindings
    • Preserves Rust evaluation order (scrutinee evaluated once; pattern tests left-to-right)
  • Consider isolating this in a dedicated ML translation helper to keep syntax clean.

  Files likely involved

  • Shallow_Micro_Rust/Basic_Case_Expression.thy
  • Shallow_Micro_Rust/Core_Syntax.thy
  • Shallow_Micro_Rust/Micro_Rust_Shallow_Embedding.thy

  Acceptance criteria

  • Complex patterns elaborate without using ad-hoc restrictions.
  • Pattern semantics are documented (especially binding order and guard timing).
  • Existing match tests still pass.