From 8939159c25706f777718e32614e8c2b2a30989b6 Mon Sep 17 00:00:00 2001
From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Date: Wed, 26 Jun 2024 22:38:31 +1000
Subject: [PATCH] Add NOT_AND' (|- ~(~t /\ t)) to BOOL_ss (in addition to
 NOT_AND: |- ~(t /\ ~t))

---
 .../lambda/barendregt/standardisationScript.sml   |  4 ----
 src/pred_set/src/more_theories/iterateScript.sml  | 15 ++++++++++-----
 src/simp/src/boolSimps.sml                        |  2 +-
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml
index 2533f474fe..ae172e469d 100644
--- a/examples/lambda/barendregt/standardisationScript.sml
+++ b/examples/lambda/barendregt/standardisationScript.sml
@@ -416,17 +416,13 @@ val residuals_to_right_of_reduction = store_thm(
     PROVE_TAC [lrcc_new_labels'],
     PROVE_TAC [],
     PROVE_TAC [lrcc_new_labels'],
-    PROVE_TAC [],
     FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN SRW_TAC [][],
     PROVE_TAC [],
     FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN SRW_TAC [][],
-    FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN SRW_TAC [][],
-    PROVE_TAC [],
     PROVE_TAC [],
     PROVE_TAC []
   ]);
 
-
 val lemma11_4_3iii = store_thm(
   "lemma11_4_3iii",
   ``!M delta N.
diff --git a/src/pred_set/src/more_theories/iterateScript.sml b/src/pred_set/src/more_theories/iterateScript.sml
index 7c48bdd69e..a4afa080f7 100644
--- a/src/pred_set/src/more_theories/iterateScript.sml
+++ b/src/pred_set/src/more_theories/iterateScript.sml
@@ -1004,11 +1004,16 @@ val ITERATE_UNION_GEN = store_thm ("ITERATE_UNION_GEN",
 
 val lemma = prove (
  ``!t s. t SUBSET s ==> (s = (s DIFF t) UNION t) /\ DISJOINT (s DIFF t) t``,
-  REPEAT STRIP_TAC THENL [SIMP_TAC std_ss [UNION_DEF, DIFF_DEF, EXTENSION, GSPECIFICATION]
-  THEN GEN_TAC THEN EQ_TAC THENL [FULL_SIMP_TAC std_ss [], STRIP_TAC THEN
-  FULL_SIMP_TAC std_ss [SUBSET_DEF]], SIMP_TAC std_ss [DISJOINT_DEF, INTER_DEF, DIFF_DEF,
-  EXTENSION, GSPECIFICATION] THEN GEN_TAC THEN EQ_TAC THENL [STRIP_TAC,
-  FULL_SIMP_TAC std_ss [NOT_IN_EMPTY]]]);
+    rpt STRIP_TAC
+ >| [ (* goal 1 (of 2) *)
+      SIMP_TAC std_ss [UNION_DEF, DIFF_DEF, EXTENSION, GSPECIFICATION] \\
+      GEN_TAC \\
+      EQ_TAC >- FULL_SIMP_TAC std_ss [] \\
+      STRIP_TAC \\
+      FULL_SIMP_TAC std_ss [SUBSET_DEF],
+      (* goal 2 (of 2) *)
+      SIMP_TAC std_ss [DISJOINT_DEF, INTER_DEF, DIFF_DEF,
+                       EXTENSION, GSPECIFICATION, NOT_IN_EMPTY] ]);
 
 val ITERATE_DIFF = store_thm ("ITERATE_DIFF",
  ``!op. monoidal op
diff --git a/src/simp/src/boolSimps.sml b/src/simp/src/boolSimps.sml
index cbe40657af..64e4facd76 100644
--- a/src/simp/src/boolSimps.sml
+++ b/src/simp/src/boolSimps.sml
@@ -101,6 +101,7 @@ val BOOL_ss = SSFRAG
      ("EXISTS_REFL'", GSYM EXISTS_REFL),
      ("EXISTS_UNIQUE_REFL'", GSYM EXISTS_UNIQUE_REFL),
      ("EXCLUDED_MIDDLE'", ONCE_REWRITE_RULE [DISJ_COMM] EXCLUDED_MIDDLE),
+     ("NOT_AND'",         ONCE_REWRITE_RULE [CONJ_COMM] NOT_AND),
      ("literal_I_thm", literal_I_thm),
      ("COND_BOOL_CLAUSES", COND_BOOL_CLAUSES),
      ("lift_disj_eq", lift_disj_eq),
@@ -108,7 +109,6 @@ val BOOL_ss = SSFRAG
    ],
    congs = [literal_cong], filter = NONE, ac = [], dprocs = []};
 
-
 (*---------------------------------------------------------------------------
    Need to rewrite cong. rules to the iterated implication format assumed
    by the simplifier.