explain how simp works

[fpvandoorn]

What question should the reference manual answer?

In what order are simp-lemmas applied? Similarly: Why is my high-priority simp-rule not always applied before a low-priority simp rule?
What is the difference between @[simp] and @[simp↓]
What are discrimination trees and how are they used (also useful to reference in the type class inference chapter)?
What is the role of the simp discharger and what is the default discharger?
EDIT: What are simpprocs? How do they work? How to write one?

Additional context
Add any other context about the question here that will help us ensure that the documentation meets your needs.