--- 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>
--- 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
--- 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)
--- 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