# HG changeset patch
# User haftmann
# Date 1751395886 -7200
# Node ID c8d92d4ced73ea76b90b9fc18499d9f183c16b31
# Parent  476627cac12efa7f8e602fc0fc2293540828e95c
isabelle regenerate_cooper

diff -r 476627cac12e -r c8d92d4ced73 src/HOL/Tools/Qelim/cooper_procedure.ML
--- a/src/HOL/Tools/Qelim/cooper_procedure.ML	Mon Jun 30 20:44:40 2025 +0200
+++ b/src/HOL/Tools/Qelim/cooper_procedure.ML	Tue Jul 01 20:51:26 2025 +0200
@@ -478,6 +478,19 @@
     semiring_1_no_zero_divisors_semidom = semiring_1_no_zero_divisors_int}
   : inta semidom;
 
+type 'a divide_trivial =
+  {one_divide_trivial : 'a one, zero_divide_trivial : 'a zero,
+    divide_divide_trivial : 'a divide};
+val one_divide_trivial = #one_divide_trivial : 'a divide_trivial -> 'a one;
+val zero_divide_trivial = #zero_divide_trivial : 'a divide_trivial -> 'a zero;
+val divide_divide_trivial = #divide_divide_trivial :
+  'a divide_trivial -> 'a divide;
+
+val divide_trivial_int =
+  {one_divide_trivial = one_int, zero_divide_trivial = zero_int,
+    divide_divide_trivial = divide_int}
+  : inta divide_trivial;
+
 type 'a semiring_no_zero_divisors_cancel =
   {semiring_no_zero_divisors_semiring_no_zero_divisors_cancel :
      'a semiring_no_zero_divisors};
@@ -486,11 +499,12 @@
   'a semiring_no_zero_divisors_cancel -> 'a semiring_no_zero_divisors;
 
 type 'a semidom_divide =
-  {divide_semidom_divide : 'a divide, semidom_semidom_divide : 'a semidom,
+  {divide_trivial_semidom_divide : 'a divide_trivial,
+    semidom_semidom_divide : 'a semidom,
     semiring_no_zero_divisors_cancel_semidom_divide :
       'a semiring_no_zero_divisors_cancel};
-val divide_semidom_divide = #divide_semidom_divide :
-  'a semidom_divide -> 'a divide;
+val divide_trivial_semidom_divide = #divide_trivial_semidom_divide :
+  'a semidom_divide -> 'a divide_trivial;
 val semidom_semidom_divide = #semidom_semidom_divide :
   'a semidom_divide -> 'a semidom;
 val semiring_no_zero_divisors_cancel_semidom_divide =
@@ -503,16 +517,12 @@
   : inta semiring_no_zero_divisors_cancel;
 
 val semidom_divide_int =
-  {divide_semidom_divide = divide_int, semidom_semidom_divide = semidom_int,
+  {divide_trivial_semidom_divide = divide_trivial_int,
+    semidom_semidom_divide = semidom_int,
     semiring_no_zero_divisors_cancel_semidom_divide =
       semiring_no_zero_divisors_cancel_int}
   : inta semidom_divide;
 
-type 'a algebraic_semidom =
-  {semidom_divide_algebraic_semidom : 'a semidom_divide};
-val semidom_divide_algebraic_semidom = #semidom_divide_algebraic_semidom :
-  'a algebraic_semidom -> 'a semidom_divide;
-
 type 'a semiring_modulo =
   {comm_semiring_1_cancel_semiring_modulo : 'a comm_semiring_1_cancel,
     modulo_semiring_modulo : 'a modulo};
@@ -522,26 +532,47 @@
 val modulo_semiring_modulo = #modulo_semiring_modulo :
   'a semiring_modulo -> 'a modulo;
 
+type 'a semiring_modulo_trivial =
+  {divide_trivial_semiring_modulo_trivial : 'a divide_trivial,
+    semiring_modulo_semiring_modulo_trivial : 'a semiring_modulo};
+val divide_trivial_semiring_modulo_trivial =
+  #divide_trivial_semiring_modulo_trivial :
+  'a semiring_modulo_trivial -> 'a divide_trivial;
+val semiring_modulo_semiring_modulo_trivial =
+  #semiring_modulo_semiring_modulo_trivial :
+  'a semiring_modulo_trivial -> 'a semiring_modulo;
+
+type 'a algebraic_semidom =
+  {semidom_divide_algebraic_semidom : 'a semidom_divide};
+val semidom_divide_algebraic_semidom = #semidom_divide_algebraic_semidom :
+  'a algebraic_semidom -> 'a semidom_divide;
+
 type 'a semidom_modulo =
   {algebraic_semidom_semidom_modulo : 'a algebraic_semidom,
-    semiring_modulo_semidom_modulo : 'a semiring_modulo};
+    semiring_modulo_trivial_semidom_modulo : 'a semiring_modulo_trivial};
 val algebraic_semidom_semidom_modulo = #algebraic_semidom_semidom_modulo :
   'a semidom_modulo -> 'a algebraic_semidom;
-val semiring_modulo_semidom_modulo = #semiring_modulo_semidom_modulo :
-  'a semidom_modulo -> 'a semiring_modulo;
-
-val algebraic_semidom_int =
-  {semidom_divide_algebraic_semidom = semidom_divide_int} :
-  inta algebraic_semidom;
+val semiring_modulo_trivial_semidom_modulo =
+  #semiring_modulo_trivial_semidom_modulo :
+  'a semidom_modulo -> 'a semiring_modulo_trivial;
 
 val semiring_modulo_int =
   {comm_semiring_1_cancel_semiring_modulo = comm_semiring_1_cancel_int,
     modulo_semiring_modulo = modulo_int}
   : inta semiring_modulo;
 
+val semiring_modulo_trivial_int =
+  {divide_trivial_semiring_modulo_trivial = divide_trivial_int,
+    semiring_modulo_semiring_modulo_trivial = semiring_modulo_int}
+  : inta semiring_modulo_trivial;
+
+val algebraic_semidom_int =
+  {semidom_divide_algebraic_semidom = semidom_divide_int} :
+  inta algebraic_semidom;
+
 val semidom_modulo_int =
   {algebraic_semidom_semidom_modulo = algebraic_semidom_int,
-    semiring_modulo_semidom_modulo = semiring_modulo_int}
+    semiring_modulo_trivial_semidom_modulo = semiring_modulo_trivial_int}
   : inta semidom_modulo;
 
 datatype nat = Nat of int;
@@ -1160,7 +1191,11 @@
 
 fun dvd (A1_, A2_) a b =
   eq A1_
-    (modulo ((modulo_semiring_modulo o semiring_modulo_semidom_modulo) A2_) b a)
+    (modulo
+      ((modulo_semiring_modulo o semiring_modulo_semiring_modulo_trivial o
+         semiring_modulo_trivial_semidom_modulo)
+        A2_)
+      b a)
     (zero ((zero_mult_zero o mult_zero_semiring_0 o semiring_0_semiring_1 o
              semiring_1_comm_semiring_1 o
              comm_semiring_1_comm_semiring_1_cancel o
@@ -1389,10 +1424,10 @@
   | simpfm (Closed v) = Closed v
   | simpfm (NClosed v) = NClosed v;
 
-fun gen_length n (x :: xs) = gen_length (suc n) xs
-  | gen_length n [] = n;
+fun length_tailrec [] n = n
+  | length_tailrec (x :: xs) n = length_tailrec xs (suc n);
 
-fun size_list x = gen_length zero_nat x;
+fun size_list xs = length_tailrec xs zero_nat;
 
 fun a_beta (And (p, q)) k = And (a_beta p k, a_beta q k)
   | a_beta (Or (p, q)) k = Or (a_beta p k, a_beta q k)