The entry point to the soundness theorem is RSP_soundness.thy. This file imports the other .thy files.