diff -r aeb412065742 -r 53b61706749b src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Jun 25 16:51:24 2022 +0200
+++ b/src/HOL/String.thy	Sat Jun 25 09:50:37 2022 +0000
@@ -38,6 +38,15 @@
 
 end
 
+lemma (in comm_semiring_1) of_nat_of_char:
+  \<open>of_nat (of_char c) = of_char c\<close>
+  by (cases c) simp
+
+lemma (in comm_ring_1) of_int_of_char:
+  \<open>of_int (of_char c) = of_char c\<close>
+  by (cases c) simp
+
+
 context unique_euclidean_semiring_with_bit_operations
 begin
 
@@ -194,6 +203,14 @@
 lifting_update natural.lifting
 lifting_forget natural.lifting
 
+lemma size_char_eq_0 [simp, code]:
+  \<open>size c = 0\<close> for c :: char
+  by (cases c) simp
+
+lemma size'_char_eq_0 [simp, code]:
+  \<open>size_char c = 0\<close>
+  by (cases c) simp
+
 syntax
   "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
   "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
@@ -354,6 +371,34 @@
   "ascii_of (Char b0 b1 b2 b3 b4 b5 b6 b7) = Char b0 b1 b2 b3 b4 b5 b6 False"
   by (simp add: ascii_of_def)
 
+qualified lemma digit0_ascii_of_iff [simp]:
+  "digit0 (String.ascii_of c) \<longleftrightarrow> digit0 c"
+  by (simp add: String.ascii_of_def)
+
+qualified lemma digit1_ascii_of_iff [simp]:
+  "digit1 (String.ascii_of c) \<longleftrightarrow> digit1 c"
+  by (simp add: String.ascii_of_def)
+
+qualified lemma digit2_ascii_of_iff [simp]:
+  "digit2 (String.ascii_of c) \<longleftrightarrow> digit2 c"
+  by (simp add: String.ascii_of_def)
+
+qualified lemma digit3_ascii_of_iff [simp]:
+  "digit3 (String.ascii_of c) \<longleftrightarrow> digit3 c"
+  by (simp add: String.ascii_of_def)
+
+qualified lemma digit4_ascii_of_iff [simp]:
+  "digit4 (String.ascii_of c) \<longleftrightarrow> digit4 c"
+  by (simp add: String.ascii_of_def)
+
+qualified lemma digit5_ascii_of_iff [simp]:
+  "digit5 (String.ascii_of c) \<longleftrightarrow> digit5 c"
+  by (simp add: String.ascii_of_def)
+
+qualified lemma digit6_ascii_of_iff [simp]:
+  "digit6 (String.ascii_of c) \<longleftrightarrow> digit6 c"
+  by (simp add: String.ascii_of_def)
+
 qualified lemma not_digit7_ascii_of [simp]:
   "\<not> digit7 (ascii_of c)"
   by (simp add: ascii_of_def)
@@ -362,10 +407,6 @@
   "ascii_of c = c" if "\<not> digit7 c"
   using that by (cases c) simp
 
-qualified lemma char_of_ascii_of [simp]:
-  "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)"
-  by (cases c) (simp only: ascii_of_Char of_char_Char take_bit_horner_sum_bit_eq, simp)
-
 qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
   morphisms explode Abs_literal
 proof
@@ -394,6 +435,24 @@
 
 end
 
+context unique_euclidean_semiring_with_bit_operations
+begin
+
+context
+begin
+
+qualified lemma char_of_ascii_of [simp]:
+  \<open>of_char (String.ascii_of c) = take_bit 7 (of_char c)\<close>
+  by (cases c) (simp only: String.ascii_of_Char of_char_Char take_bit_horner_sum_bit_eq, simp)
+
+qualified lemma ascii_of_char_of:
+  \<open>String.ascii_of (char_of a) = char_of (take_bit 7 a)\<close>
+  by (simp add: char_of_def bit_simps)
+
+end
+
+end
+
 
 subsubsection \<open>Syntactic representation\<close>