Isabelle/HOL translation: records and named patterns

[lukaszcz]

• Closes #2894
• Closes #2895
• The translation of pattern matching on records is a bit tricky because one cannot pattern match on records in Isabelle, except in top patterns of function clauses. We thus need to translate into nested pattern matching and record projections. Named patterns can be translated with a similar technique and are also handled in this PR.

Checklist

• [x] record creation
• [x] record projections
• [x] record update
• [x] top-level record patterns
• [x] nested record patterns
• [x] named patterns
• [x] remove redundant pattern matching clauses
• [x] remove redundant single-branch pattern matches