Add NOT_AND' (|- ~(~t /\ t)) to BOOL_ss (in addition to NOT_AND: |- ~(t /\ ~t))

Author: binghe

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.

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

src/simp/src/boolSimps.sml

@@ -101,14 +101,14 @@ 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),
      ("lift_imp_disj", lift_imp_disj)
    ],
    congs = [literal_cong], filter = NONE, ac = [], dprocs = []};
 
-
 (*---------------------------------------------------------------------------
    Need to rewrite cong. rules to the iterated implication format assumed
    by the simplifier.