Add disjunctive/or-pattern support for Micro Rust

[DominicPM]

Implement Rust-style disjunctive patterns (p1 | p2) that work in all pattern contexts: match, match_switch, if let, let else, and for loops.

Changes:

• Micro_Rust_Syntax.thy: Add _urust_match_pattern_disjunction syntax with right-associative precedence [1000, 100] 100
• Core_Syntax.thy: Add shallow pattern syntax and expand disjunctions in parse_translation (expand_disjunction_pattern, expand_branch). Add switch branch translations for numeric disjunctive patterns.
• Micro_Rust_Shallow_Embedding.thy: Add translation rule and handle nested disjunctions in shallow_match_pattern_of
• Micro_Rust_Shallow_Embedding_Tests.thy: Add comprehensive tests including guards, nested patterns, and match_switch. Use three_case datatype for non-exhaustive if-let/let-else tests.

Examples now supported:

match x { Some(a) | None => ..., _ => ... }

match_switch n { 1 | 2 | 3 => ..., _ => ... }

if let CaseA(x) | CaseB(x) = val { ... }

let Ok(x) | Err(x) = result else { return; };

match nested { Some(Ok(x) | Err(x)) => x, _ => default }

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.