Combine `Atomic e` and `StronglyAtomic e` into `Atomic s e` and introduce `HeadAtomic s e`.
I saw no need for `stuckness_flip`: strong atomicity always works, while weak atomicity works only for expressions that are not stuck. Since this seemed unclear, I split lemma `wp_atomic'` up into `wp_strong_atomic` (parametric in the WP's `s`) and `wp_weak_atomic` (not). The proof mode instance is stated in terms of the derived rule `wp_atomic` (parametric in `s`).
Showing
Please register or sign in to comment