From 9374e6b0b720d605e785a376b0f1170e189eeab0 Mon Sep 17 00:00:00 2001
From: Irvin <ordinarymath@yahoo.com>
Date: Fri, 26 Sep 2025 16:23:49 +0800
Subject: [PATCH] Add UNCURRY_EQ to AllCaseEqs,

Also add a UNCURRY_PRED theorem and add it to AllCasePreds
---
 src/1/TypeBase.sig           | 2 ++
 src/1/TypeBase.sml           | 9 +++++++--
 src/coretypes/pairScript.sml | 7 +++++++
 src/coretypes/pairSimps.sml  | 3 ++-
 4 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/1/TypeBase.sig b/src/1/TypeBase.sig
index fd9fe81933..a255f139fb 100644
--- a/src/1/TypeBase.sig
+++ b/src/1/TypeBase.sig
@@ -64,6 +64,8 @@ sig
    val CaseEq             : string -> thm
    val CaseEqs            : string list -> thm
    val AllCaseEqs         : unit -> thm
+   val add_CaseEqs        : thm list -> unit
+   val add_CasePreds      : thm list -> unit
 
    val CasePred           : string -> thm
    val CasePreds          : string list -> thm
diff --git a/src/1/TypeBase.sml b/src/1/TypeBase.sml
index dc61552c9d..aee978f9e3 100644
--- a/src/1/TypeBase.sml
+++ b/src/1/TypeBase.sml
@@ -215,6 +215,8 @@ fun tyi_from_name s =
 
 val CaseEq = TypeBasePure.case_eq_of o tyi_from_name
 val CaseEqs = Drule.LIST_CONJ o map CaseEq
+val additional_CaseEqs = ref ([]:thm list)
+fun add_CaseEqs thms = ignore (additional_CaseEqs := thms @ (!additional_CaseEqs))
 fun AllCaseEqs() =
   let
     fun foldthis(ty, tyi, acc) =
@@ -223,7 +225,7 @@ fun AllCaseEqs() =
         | SOME th => if aconv (concl acc) boolSyntax.T then th
                      else CONJ th acc
   in
-    TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())
+    CONJ (TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())) (Drule.LIST_CONJ (!additional_CaseEqs))
   end
 
 fun type_info_of ty = {case_def = case_def_of ty, nchotomy = nchotomy_of ty}
@@ -248,6 +250,9 @@ fun CasePred' tyinfo =
 val CasePred = CasePred' o tyi_from_name
 
 val CasePreds = Drule.LIST_CONJ o map CasePred
+val additional_CasePreds = ref ([]:thm list)
+fun add_CasePreds thms = ignore (additional_CasePreds := thms @ (!additional_CasePreds))
+
 fun AllCasePreds() =
   let
     fun foldthis(ty, tyi, acc) =
@@ -256,7 +261,7 @@ fun AllCasePreds() =
         | SOME th => if aconv (concl acc) boolSyntax.T then th
                      else CONJ th acc
   in
-    TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())
+    CONJ (TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())) (Drule.LIST_CONJ (!additional_CasePreds))
   end
 
 (* ---------------------------------------------------------------------- *
diff --git a/src/coretypes/pairScript.sml b/src/coretypes/pairScript.sml
index a21e2d997d..3e346baf62 100644
--- a/src/coretypes/pairScript.sml
+++ b/src/coretypes/pairScript.sml
@@ -334,6 +334,13 @@ Proof
   ASM_SIMP_TAC bool_ss [UNCURRY_DEF, PAIR_EQ]
 QED
 
+Theorem UNCURRY_PRED:
+  UNCURRY f x <=> ?a b. x = (a,b) /\ f a b
+Proof
+  Q.SPEC_THEN ‘x’ STRIP_ASSUME_TAC pair_CASES >>
+  ASM_SIMP_TAC bool_ss [UNCURRY_DEF, PAIR_EQ]
+QED
+
 (* ------------------------------------------------------------------------- *)
 (* pair_Axiom = |- !f. ?fn. !x y. fn (x,y) = f x y                           *)
 (* ------------------------------------------------------------------------- *)
diff --git a/src/coretypes/pairSimps.sml b/src/coretypes/pairSimps.sml
index 64775773fe..50331180b1 100644
--- a/src/coretypes/pairSimps.sml
+++ b/src/coretypes/pairSimps.sml
@@ -5,7 +5,8 @@ open Lib Parse simpLib pairTheory PairedLambda;
 
 
 val PAIR_ss = BasicProvers.thy_ssfrag "pair"
-
+val _ = TypeBase.add_CaseEqs [UNCURRY_EQ]
+val _ = TypeBase.add_CasePreds [UNCURRY_PRED]
 val fvar = ``f:'a -> 'b -> bool``;
 val paired_forall_ss =
     conv_ss