# HG changeset patch
# User haftmann
# Date 1655885712 0
# Node ID 6de655ccac197b2466eca585003c91e20b66ab3c
# Parent  36965f6b3530756824c8a3f8e2d777ed7fe35407
Prefer existing horner sum combinator.

diff -r 36965f6b3530 -r 6de655ccac19 NEWS
--- a/NEWS	Wed Jun 22 08:15:10 2022 +0000
+++ b/NEWS	Wed Jun 22 08:15:12 2022 +0000
@@ -34,6 +34,9 @@
 
 *** HOL ***
 
+* Theory Char_ord: streamlined logical specifications.
+Minor INCOMPATIBILITY.
+
 * Rule split_of_bool_asm is not split any longer, analogously to
 split_if_asm.  INCOMPATIBILITY.
 
diff -r 36965f6b3530 -r 6de655ccac19 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Wed Jun 22 08:15:10 2022 +0000
+++ b/src/HOL/Library/Char_ord.thy	Wed Jun 22 08:15:12 2022 +0000
@@ -25,14 +25,14 @@
 
 lemma less_eq_char_simp [simp]:
   "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
-    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
-      \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
+    \<longleftrightarrow> horner_sum of_bool (2 :: nat) [b0, b1, b2, b3, b4, b5, b6, b7]
+      \<le> horner_sum of_bool (2 :: nat) [c0, c1, c2, c3, c4, c5, c6, c7]"
   by (simp add: less_eq_char_def)
 
 lemma less_char_simp [simp]:
   "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
-    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
-      < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
+    \<longleftrightarrow> horner_sum of_bool (2 :: nat) [b0, b1, b2, b3, b4, b5, b6, b7]
+      < horner_sum of_bool (2 :: nat) [c0, c1, c2, c3, c4, c5, c6, c7]"
   by (simp add: less_char_def)
 
 instantiation char :: distrib_lattice