Make an obvious rewrite about function update automatic

HOL-Theorem-Prover · Oct 24, 2023 · 904e33c · 904e33c
1 parent 302279e
commit 904e33c
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/src/combin/combinScript.sml b/src/combin/combinScript.sml
@@ -189,6 +189,8 @@ val UPDATE_APPLY = Q.store_thm("UPDATE_APPLY",
    THEN REPEAT STRIP_TAC
    THEN ASM_REWRITE_TAC [])
 
+Theorem UPDATE_APPLY1 = cj 1 UPDATE_APPLY
+
 val APPLY_UPDATE_THM = Q.store_thm("APPLY_UPDATE_THM",
   `!f a b c. (a =+ b) f c = (if a = c then b else f c)`,
   PURE_REWRITE_TAC [UPDATE_def]

diff --git a/src/simp/src/combinSimps.sml b/src/simp/src/combinSimps.sml
@@ -7,7 +7,7 @@ val COMBIN_ss = SSFRAG {
       dprocs = [],
       rewrs = map (fn s => (SOME{Thy="combin",Name= s}, DB.fetch "combin" s)) [
         "I_THM","I_o_ID","K_THM","S_THM","o_ASSOC'","o_THM","W_THM","C_THM",
-        "K_o_THM", "UPDATE_EQ", "UPDATE_APPLY_ID_RWT"
+        "K_o_THM", "UPDATE_EQ", "UPDATE_APPLY_ID_RWT", "UPDATE_APPLY1"
       ]
     }