# HG changeset patch
# User haftmann
# Date 1657353953 0
# Node ID ed15f2cd4f7d21dab89dcc57ca03b7b21670ffd2
# Parent  2d153e052aea1d9b70cecd47b1fd27bf246c9c30
refined code equations for characters

diff -r 2d153e052aea -r ed15f2cd4f7d src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Fri Jul 08 22:30:35 2022 +0200
+++ b/src/HOL/Groups_List.thy	Sat Jul 09 08:05:53 2022 +0000
@@ -403,6 +403,89 @@
 
 end
 
+context linordered_semidom
+begin
+
+lemma horner_sum_nonnegative:
+  \<open>0 \<le> horner_sum of_bool 2 bs\<close>
+  by (induction bs) simp_all
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_bound:
+  \<open>horner_sum of_bool 2 bs < 2 ^ length bs\<close>
+proof (induction bs)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  moreover define a where \<open>a = 2 ^ length bs - horner_sum of_bool 2 bs\<close>
+  ultimately have *: \<open>2 ^ length bs = horner_sum of_bool 2 bs + a\<close>
+    by simp
+  have \<open>1 < a * 2\<close> if \<open>0 < a\<close>
+    using that add_mono [of 1 a 1 a]
+    by (simp add: mult_2_right discrete)
+  with Cons show ?case
+    by (simp add: algebra_simps *)
+qed
+
+end
+
+lemma nat_horner_sum [simp]:
+  \<open>nat (horner_sum of_bool 2 bs) = horner_sum of_bool 2 bs\<close>
+  by (induction bs) (auto simp add: nat_add_distrib horner_sum_nonnegative)
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_less_eq_iff_lexordp_eq:
+  \<open>horner_sum of_bool 2 bs \<le> horner_sum of_bool 2 cs \<longleftrightarrow> lexordp_eq (rev bs) (rev cs)\<close>
+  if \<open>length bs = length cs\<close>
+proof -
+  have \<open>horner_sum of_bool 2 (rev bs) \<le> horner_sum of_bool 2 (rev cs) \<longleftrightarrow> lexordp_eq bs cs\<close>
+    if \<open>length bs = length cs\<close> for bs cs
+  using that proof (induction bs cs rule: list_induct2)
+    case Nil
+    then show ?case
+      by simp
+  next
+    case (Cons b bs c cs)
+    with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+      horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+    show ?case
+      by (auto simp add: horner_sum_append not_le Cons intro: add_strict_increasing2 add_increasing)
+  qed
+  from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+    by simp
+qed
+
+lemma horner_sum_less_iff_lexordp:
+  \<open>horner_sum of_bool 2 bs < horner_sum of_bool 2 cs \<longleftrightarrow> ord_class.lexordp (rev bs) (rev cs)\<close>
+  if \<open>length bs = length cs\<close>
+proof -
+  have \<open>horner_sum of_bool 2 (rev bs) < horner_sum of_bool 2 (rev cs) \<longleftrightarrow> ord_class.lexordp bs cs\<close>
+    if \<open>length bs = length cs\<close> for bs cs
+  using that proof (induction bs cs rule: list_induct2)
+    case Nil
+    then show ?case
+      by simp
+  next
+    case (Cons b bs c cs)
+    with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+      horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+    show ?case
+      by (auto simp add: horner_sum_append not_less Cons intro: add_strict_increasing2 add_increasing)
+  qed
+  from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+    by simp
+qed
+
+end
+
 
 subsection \<open>Further facts about \<^const>\<open>List.n_lists\<close>\<close>
 
diff -r 2d153e052aea -r ed15f2cd4f7d src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Fri Jul 08 22:30:35 2022 +0200
+++ b/src/HOL/Library/Char_ord.thy	Sat Jul 09 08:05:53 2022 +0000
@@ -8,85 +8,6 @@
   imports Main
 begin
 
-context linordered_semidom
-begin
-
-lemma horner_sum_nonnegative:
-  \<open>0 \<le> horner_sum of_bool 2 bs\<close>
-  by (induction bs) simp_all
-
-end
-
-context unique_euclidean_semiring_numeral
-begin
-
-lemma horner_sum_bound:
-  \<open>horner_sum of_bool 2 bs < 2 ^ length bs\<close>
-proof (induction bs)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  moreover define a where \<open>a = 2 ^ length bs - horner_sum of_bool 2 bs\<close>
-  ultimately have *: \<open>2 ^ length bs = horner_sum of_bool 2 bs + a\<close>
-    by simp
-  have \<open>1 < a * 2\<close> if \<open>0 < a\<close>
-    using that add_mono [of 1 a 1 a]
-    by (simp add: mult_2_right discrete)
-  with Cons show ?case
-    by (simp add: algebra_simps *)
-qed
-
-end
-
-context unique_euclidean_semiring_numeral
-begin
-
-lemma horner_sum_less_eq_iff_lexordp_eq:
-  \<open>horner_sum of_bool 2 bs \<le> horner_sum of_bool 2 cs \<longleftrightarrow> lexordp_eq (rev bs) (rev cs)\<close>
-  if \<open>length bs = length cs\<close>
-proof -
-  have \<open>horner_sum of_bool 2 (rev bs) \<le> horner_sum of_bool 2 (rev cs) \<longleftrightarrow> lexordp_eq bs cs\<close>
-    if \<open>length bs = length cs\<close> for bs cs
-  using that proof (induction bs cs rule: list_induct2)
-    case Nil
-    then show ?case
-      by simp
-  next
-    case (Cons b bs c cs)
-    with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
-      horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
-    show ?case
-      by (auto simp add: horner_sum_append not_le Cons intro: add_strict_increasing2 add_increasing)
-  qed
-  from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
-    by simp
-qed
-
-lemma horner_sum_less_iff_lexordp:
-  \<open>horner_sum of_bool 2 bs < horner_sum of_bool 2 cs \<longleftrightarrow> ord_class.lexordp (rev bs) (rev cs)\<close>
-  if \<open>length bs = length cs\<close>
-proof -
-  have \<open>horner_sum of_bool 2 (rev bs) < horner_sum of_bool 2 (rev cs) \<longleftrightarrow> ord_class.lexordp bs cs\<close>
-    if \<open>length bs = length cs\<close> for bs cs
-  using that proof (induction bs cs rule: list_induct2)
-    case Nil
-    then show ?case
-      by simp
-  next
-    case (Cons b bs c cs)
-    with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
-      horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
-    show ?case
-      by (auto simp add: horner_sum_append not_less Cons intro: add_strict_increasing2 add_increasing)
-  qed
-  from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
-    by simp
-qed
-
-end
-
 instantiation char :: linorder
 begin
 
diff -r 2d153e052aea -r ed15f2cd4f7d src/HOL/Library/Code_Abstract_Char.thy
--- a/src/HOL/Library/Code_Abstract_Char.thy	Fri Jul 08 22:30:35 2022 +0200
+++ b/src/HOL/Library/Code_Abstract_Char.thy	Sat Jul 09 08:05:53 2022 +0000
@@ -17,13 +17,19 @@
   by (simp add: integer_of_char_def)
 
 lemma char_of_integer_code [code]:
-  \<open>integer_of_char (char_of_integer k) = take_bit 8 k\<close>
-  by (simp add: integer_of_char_def char_of_integer_def take_bit_eq_mod)
+  \<open>integer_of_char (char_of_integer k) = (if 0 \<le> k \<and> k < 256 then k else take_bit 8 k)\<close>
+  by (simp add: integer_of_char_def char_of_integer_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
 
-context comm_semiring_1
-begin
+lemma of_char_code [code]:
+  \<open>of_char c = of_nat (nat_of_integer (integer_of_char c))\<close>
+proof -
+  have \<open>int_of_integer (of_char c) = of_char c\<close>
+    by (cases c) simp
+  then show ?thesis
+    by (simp add: integer_of_char_def nat_of_integer_def of_nat_of_char)
+qed
 
-definition byte :: \<open>bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> 'a\<close>
+definition byte :: \<open>bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> integer\<close>
   where [simp]: \<open>byte b0 b1 b2 b3 b4 b5 b6 b7 = horner_sum of_bool 2 [b0, b1, b2, b3, b4, b5, b6, b7]\<close>
 
 lemma byte_code [code]:
@@ -40,8 +46,6 @@
     in s7)\<close>
   by simp
 
-end
-
 lemma Char_code [code]:
   \<open>integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = byte b0 b1 b2 b3 b4 b5 b6 b7\<close>
   by (simp add: integer_of_char_def)
diff -r 2d153e052aea -r ed15f2cd4f7d src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Jul 08 22:30:35 2022 +0200
+++ b/src/HOL/String.thy	Sat Jul 09 08:05:53 2022 +0000
@@ -46,6 +46,10 @@
   \<open>of_int (of_char c) = of_char c\<close>
   by (cases c) simp
 
+lemma nat_of_char [simp]:
+  \<open>nat (of_char c) = of_char c\<close>
+  by (cases c) (simp only: of_char_Char nat_horner_sum)
+
 
 context unique_euclidean_semiring_with_bit_operations
 begin