Generalize match translation: recursive matcher for complex patterns

- 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.

Start by reading Shallow_Micro_Rust/Basic_Case_Expression.thy, then trace the relevant syntax and translation definitions in Core_Syntax.thy and Micro_Rust_Shallow_Embedding.thy. Use the existing match tests as the baseline. Done means complex patterns elaborate without ad-hoc restrictions, pattern semantics document binding order and guard timing, and existing match tests still pass.

Written by the indexing model from the issue text.