Implementation of std::result functions

[jonasmittun]

Issue #17 :
Implementing std::result

Description of changes:
Restructured file with sections/subsections for ease of use with sidekick, every function has its own subsection.

Added preamble section intended for content reused across functions. Currently contains declare lift_pure_to_contract_def [crush_contracts] and ucincl_auto lift_pure_to_contract which are reused in all implementations taking a function as an argument.

Added 24 missing functions:
All the following functions are implemented to be as faithful as possible to the Rust docs and are complete with function, contract and proof.

• and
• and_then
• as_deref
• as_deref_mut
• as_ref
• cloned
• err
• expect_err
• flatten
• inspect
• inspect_err
• into_err
• into_ok
• is_err_and
• is_ok_and
• iter
• iter_mut
• map
• map_or
• map_or_else
• or_else
• transpose
• unwrap_err
• unwrap_or_else

Changed 9 existing functions:
General changes include: Renaming definitions to include a "result_" prefix to keep the namespace consistent and to avoid collisions. Refactoring variable names and HOL type names for consistency across functions. Proofs generally rewritten to use split: rather than split!:.

• map_err:
  Implemented contract and proof.
• unwrap_or:
  Function definition refactored. Implemented contract and proof.
• as_mut:
  Refactored contract and simplified proof, proof is now using by-form rather than apply style. Removed adhoc_overloading store_update_const ⇌ update_fun as it appeared to be unused, the store_update overloading isn't exercised here.
• ok:
  Proof rewritten to use by-form rather than apply style.
• expect
• unwrap
• is_err
• is_ok
• or

Added 5 unimplemented function subsections:
The following functions generally aren't functionally distinct in µRust and are therefore left unimplemented, please advise if this is the best approach, if an alias would be better or if you would prefer that these be handled in some other way.

• copied:
  Identical to cloned in µRust, no optimized execution available.
• map_or_default
• unwrap_or_default:
  Default values not implemented in µRust.
• unwrap_err_unchecked
• unwrap_unchecked:
  Unchecked (unsafe) execution not supported in µRust.

Items requiring extra review attention
Comparing unwrap and unwrap_err we find a difference in how the internal expect/expect_err function is called due to the latter not being implemented in the Core_Syntax.thy consts. I'm unsure what the intention is here for the future so I've left it as is, but perhaps this could be made into a new issue aiming to make StdLib functions callable in the way expect is?

micro_rust_notation and adhoc_overloading are used in a mixed fashion and depend on functions being added to other files. As these were recently changed and left mixed, I didn't want to make a call as to standardising the file to one or the other. I noticed that adhoc was left specifically in the places where the name is shared with one in Option, unsure if coincidence or not, but I want to point it out so you're aware. Furthermore, I felt it was easier for both me and the reviewer if my changes were isolated to just the one file. Perhaps this could be a new issue?

Regarding naming changes (appending result_ to definitions), I'm worried that this could break other proofs that depend on the existing implementations. Unsure how to handle this if that's the case, please advise.

I want to be transparent and admit that the as_deref, as_deref_mut, as_mut and as_ref functions were difficult to implement and I have some doubts if I've done this correctly. My biggest specific concern is regarding the optics/focus components used, e.g. ro_ref_from_ref, focus_focused, unsafe_ref_from_ro_ref. Please be careful to review these in case I have made some mistake.

AI Disclosure:
I've used Claude (Opus 4.8) to assist in both understanding the AutoCorrode codebase and writing certain contracts/proofs. I do my best not to use any AI input that I don't understand myself to a reasonable degree and strive to write most code/text by hand to force myself to check my output.

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