# HG changeset patch
# User desharna
# Date 1645602224 -3600
# Node ID 8adbfeaecbfecd0047bfdd1a680ace4afc2f70f0
# Parent  7add2d5322a7a198447b5524c076bd13bd9ffbc5
avoided recomputation in Cooper.djf and ran `isabelle regenerate_cooper`

diff -r 7add2d5322a7 -r 8adbfeaecbfe src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Mar 16 16:14:22 2022 +0000
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 23 08:43:44 2022 +0100
@@ -316,7 +316,7 @@
     else if q = F then f p
     else
       let fp = f p
-      in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q)"
+      in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or fp q)"
 
 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
   where "evaldjf f ps = foldr (djf f) ps F"
diff -r 7add2d5322a7 -r 8adbfeaecbfe src/HOL/Tools/Qelim/cooper_procedure.ML
--- a/src/HOL/Tools/Qelim/cooper_procedure.ML	Wed Mar 16 16:14:22 2022 +0000
+++ b/src/HOL/Tools/Qelim/cooper_procedure.ML	Wed Feb 23 08:43:44 2022 +0100
@@ -1026,15 +1026,19 @@
 fun djf f p q =
   (if equal_fm q T then T
     else (if equal_fm q F then f p
-           else (case f p of T => T | F => q | Lt _ => Or (f p, q)
-                  | Le _ => Or (f p, q) | Gt _ => Or (f p, q)
-                  | Ge _ => Or (f p, q) | Eq _ => Or (f p, q)
-                  | NEq _ => Or (f p, q) | Dvd (_, _) => Or (f p, q)
-                  | NDvd (_, _) => Or (f p, q) | Not _ => Or (f p, q)
-                  | And (_, _) => Or (f p, q) | Or (_, _) => Or (f p, q)
-                  | Imp (_, _) => Or (f p, q) | Iff (_, _) => Or (f p, q)
-                  | E _ => Or (f p, q) | A _ => Or (f p, q)
-                  | Closed _ => Or (f p, q) | NClosed _ => Or (f p, q))));
+           else let
+                  val fp = f p;
+                in
+                  (case fp of T => T | F => q | Lt _ => Or (fp, q)
+                    | Le _ => Or (fp, q) | Gt _ => Or (fp, q)
+                    | Ge _ => Or (fp, q) | Eq _ => Or (fp, q)
+                    | NEq _ => Or (fp, q) | Dvd (_, _) => Or (fp, q)
+                    | NDvd (_, _) => Or (fp, q) | Not _ => Or (fp, q)
+                    | And (_, _) => Or (fp, q) | Or (_, _) => Or (fp, q)
+                    | Imp (_, _) => Or (fp, q) | Iff (_, _) => Or (fp, q)
+                    | E _ => Or (fp, q) | A _ => Or (fp, q)
+                    | Closed _ => Or (fp, q) | NClosed _ => Or (fp, q))
+                end));
 
 fun evaldjf f ps = foldr (djf f) ps F;