Make `if_1_0_0` lemmas consistent

[corlewis]

Currently, Lib.if_1_0_0, Polish.if_P_1_0_eq_0 and Word_Lemmas_Internal.if_then_1_else_0 are all duplicates of each other. if_P_1_0_eq_0 is declared as simp when it is proved in autocorres while the other two are never globally added to the simpset.

It would be nice if these were made consistent, preferably with only one lemma, which has the same status of being in the simpset or not everywhere that it is accessible.

[corlewis]

For completeness, these lemmas are

"(if P then 1 else 0) = (0 :: 'a :: zero_neq_one) ⟷ ¬P"

[lsf37]

The problem with making such lemmas globally [simp] is that P can be an equation (or negation of an equation). That means if we rewrite to P, then the simplifier will pick up that equation as a rewrite itself and may fail to terminate.

I encountered the same problem with the if_option and if_option_eq sets that ended up as not globally [simp].

Regardless of [simp] or not, we should have a complete general set of rules for the case where we do want to rewrite. It looks like all of the ones above are an instance of the same thing that if_option_eq is an instance of, which is really

x ~= y ==> (if P then x else y) = x ⟷ P
x ~= y ==> (if P then x else y) = y ⟷ ¬P

(plus the versions where the if is on the other side, i.e. x = (if ..) ....

It's not immediately clear to me if both the lemmas about 0 and 1 and the if_option_eq set could be derived nicely from the general set, since you can't say [simplified] without destroying the if.

Maybe we could make a locale that has x ~= y assumption and then interpret the locale to get instances.