fix_IF_NONE_EQUALS_OPTION

This change removes IF_NONE_EQUALS_OPTION from the
srw_ss and adds 2 lemmas.
if_option_eq is the last two conjuncts + 2 more other useful case splits
if_option_neq is added for backward compatiblitity and it
preserves good behaviour of IF_NONE_EQUALS_OPTION.

Author: ordinarymath

src/coretypes/optionScript.sml

@@ -329,14 +329,29 @@ val IF_EQUALS_OPTION = store_thm(
   SRW_TAC [][]);
 val _ = export_rewrites ["IF_EQUALS_OPTION"]
 
+Theorem if_option_eq[simp]:
+    (((if P then X else SOME x) = NONE) <=> P /\ (X = NONE)) /\
+    (((if P then SOME x else X) = NONE) <=> ~P /\ (X = NONE)) /\
+    (((if P then X else NONE) = SOME x) <=> P /\ (X = SOME x)) /\
+    (((if P then NONE else X) = SOME x) <=> ~P /\ (X = SOME x))
+Proof
+  OPTION_CASES_TAC“X:'a option” THEN SRW_TAC [](option_rws)
+QED
+
+Theorem if_option_neq[simp]:
+    (((if P then X else NONE) ≠ NONE) <=> P /\ (X ≠ NONE)) /\
+    (((if P then NONE else X) ≠ NONE) <=> ~P /\ (X ≠ NONE))
+Proof
+  OPTION_CASES_TAC“X:'a option” THEN SRW_TAC [](option_rws)
+QED
+
 val IF_NONE_EQUALS_OPTION = store_thm(
   "IF_NONE_EQUALS_OPTION",
   ``(((if P then X else NONE) = NONE) <=> (P ==> IS_NONE X)) /\
     (((if P then NONE else X) = NONE) <=> (IS_SOME X ==> P)) /\
     (((if P then X else NONE) = SOME x) <=> P /\ (X = SOME x)) /\
     (((if P then NONE else X) = SOME x) <=> ~P /\ (X = SOME x))``,
   OPTION_CASES_TAC“X:'a option” THEN SRW_TAC [](option_rws));
-val _ = export_rewrites ["IF_NONE_EQUALS_OPTION"]
 
 (* ----------------------------------------------------------------------
     OPTION_MAP theorems