diff --git a/src/HOL/Groups_List.thy b/src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy
+++ b/src/HOL/Groups_List.thy
@@ -1,509 +1,592 @@
 (* Author: Tobias Nipkow, TU Muenchen *)
 
 section \<open>Sum and product over lists\<close>
 
 theory Groups_List
 imports List
 begin
 
 locale monoid_list = monoid
 begin
 
 definition F :: "'a list \<Rightarrow> 'a"
 where
   eq_foldr [code]: "F xs = foldr f xs \<^bold>1"
 
 lemma Nil [simp]:
   "F [] = \<^bold>1"
   by (simp add: eq_foldr)
 
 lemma Cons [simp]:
   "F (x # xs) = x \<^bold>* F xs"
   by (simp add: eq_foldr)
 
 lemma append [simp]:
   "F (xs @ ys) = F xs \<^bold>* F ys"
   by (induct xs) (simp_all add: assoc)
 
 end
 
 locale comm_monoid_list = comm_monoid + monoid_list
 begin
 
 lemma rev [simp]:
   "F (rev xs) = F xs"
   by (simp add: eq_foldr foldr_fold  fold_rev fun_eq_iff assoc left_commute)
 
 end
 
 locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set
 begin
 
 lemma distinct_set_conv_list:
   "distinct xs \<Longrightarrow> set.F g (set xs) = list.F (map g xs)"
   by (induct xs) simp_all
 
 lemma set_conv_list [code]:
   "set.F g (set xs) = list.F (map g (remdups xs))"
   by (simp add: distinct_set_conv_list [symmetric])
 
 end
 
 
 subsection \<open>List summation\<close>
 
 context monoid_add
 begin
 
 sublocale sum_list: monoid_list plus 0
 defines
   sum_list = sum_list.F ..
 
 end
 
 context comm_monoid_add
 begin
 
 sublocale sum_list: comm_monoid_list plus 0
 rewrites
   "monoid_list.F plus 0 = sum_list"
 proof -
   show "comm_monoid_list plus 0" ..
   then interpret sum_list: comm_monoid_list plus 0 .
   from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
 qed
 
 sublocale sum: comm_monoid_list_set plus 0
 rewrites
   "monoid_list.F plus 0 = sum_list"
   and "comm_monoid_set.F plus 0 = sum"
 proof -
   show "comm_monoid_list_set plus 0" ..
   then interpret sum: comm_monoid_list_set plus 0 .
   from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
   from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym)
 qed
 
 end
 
 text \<open>Some syntactic sugar for summing a function over a list:\<close>
 syntax (ASCII)
   "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
 syntax
   "_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"
 
 context
   includes lifting_syntax
 begin
 
 lemma sum_list_transfer [transfer_rule]:
   "(list_all2 A ===> A) sum_list sum_list"
     if [transfer_rule]: "A 0 0" "(A ===> A ===> A) (+) (+)"
   unfolding sum_list.eq_foldr [abs_def]
   by transfer_prover
 
 end
 
 text \<open>TODO duplicates\<close>
 lemmas sum_list_simps = sum_list.Nil sum_list.Cons
 lemmas sum_list_append = sum_list.append
 lemmas sum_list_rev = sum_list.rev
 
 lemma (in monoid_add) fold_plus_sum_list_rev:
   "fold plus xs = plus (sum_list (rev xs))"
 proof
   fix x
   have "fold plus xs x = sum_list (rev xs @ [x])"
     by (simp add: foldr_conv_fold sum_list.eq_foldr)
   also have "\<dots> = sum_list (rev xs) + x"
     by simp
   finally show "fold plus xs x = sum_list (rev xs) + x"
     .
 qed
 
 lemma (in comm_monoid_add) sum_list_map_remove1:
   "x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
   by (induct xs) (auto simp add: ac_simps)
 
 lemma (in monoid_add) size_list_conv_sum_list:
   "size_list f xs = sum_list (map f xs) + size xs"
   by (induct xs) auto
 
 lemma (in monoid_add) length_concat:
   "length (concat xss) = sum_list (map length xss)"
   by (induct xss) simp_all
 
 lemma (in monoid_add) length_product_lists:
   "length (product_lists xss) = foldr (*) (map length xss) 1"
 proof (induct xss)
   case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
 qed simp
 
 lemma (in monoid_add) sum_list_map_filter:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
   shows "sum_list (map f (filter P xs)) = sum_list (map f xs)"
   using assms by (induct xs) auto
 
 lemma sum_list_filter_le_nat:
   fixes f :: "'a \<Rightarrow> nat"
   shows "sum_list (map f (filter P xs)) \<le> sum_list (map f xs)"
 by(induction xs; simp)
 
 lemma (in comm_monoid_add) distinct_sum_list_conv_Sum:
   "distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)"
   by (induct xs) simp_all
 
 lemma sum_list_upt[simp]:
   "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"
 by(simp add: distinct_sum_list_conv_Sum)
 
 context ordered_comm_monoid_add
 begin
 
 lemma sum_list_nonneg: "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> 0 \<le> sum_list xs"
 by (induction xs) auto
 
 lemma sum_list_nonpos: "(\<And>x. x \<in> set xs \<Longrightarrow> x \<le> 0) \<Longrightarrow> sum_list xs \<le> 0"
 by (induction xs) (auto simp: add_nonpos_nonpos)
 
 lemma sum_list_nonneg_eq_0_iff:
   "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> (\<forall>x\<in> set xs. x = 0)"
 by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg)
 
 end
 
 context canonically_ordered_monoid_add
 begin
 
 lemma sum_list_eq_0_iff [simp]:
   "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
 by (simp add: sum_list_nonneg_eq_0_iff)
 
 lemma member_le_sum_list:
   "x \<in> set xs \<Longrightarrow> x \<le> sum_list xs"
 by (induction xs) (auto simp: add_increasing add_increasing2)
 
 lemma elem_le_sum_list:
   "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns)"
 by (rule member_le_sum_list) simp
 
 end
 
 lemma (in ordered_cancel_comm_monoid_diff) sum_list_update:
   "k < size xs \<Longrightarrow> sum_list (xs[k := x]) = sum_list xs + x - xs ! k"
 apply(induction xs arbitrary:k)
  apply (auto simp: add_ac split: nat.split)
 apply(drule elem_le_sum_list)
 by (simp add: local.add_diff_assoc local.add_increasing)
 
 lemma (in monoid_add) sum_list_triv:
   "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   by (induct xs) (simp_all add: distrib_right)
 
 lemma (in monoid_add) sum_list_0 [simp]:
   "(\<Sum>x\<leftarrow>xs. 0) = 0"
   by (induct xs) (simp_all add: distrib_right)
 
 text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close>
 lemma (in ab_group_add) uminus_sum_list_map:
   "- sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)"
   by (induct xs) simp_all
 
 lemma (in comm_monoid_add) sum_list_addf:
   "(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)"
   by (induct xs) (simp_all add: algebra_simps)
 
 lemma (in ab_group_add) sum_list_subtractf:
   "(\<Sum>x\<leftarrow>xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)"
   by (induct xs) (simp_all add: algebra_simps)
 
 lemma (in semiring_0) sum_list_const_mult:
   "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
   by (induct xs) (simp_all add: algebra_simps)
 
 lemma (in semiring_0) sum_list_mult_const:
   "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
   by (induct xs) (simp_all add: algebra_simps)
 
 lemma (in ordered_ab_group_add_abs) sum_list_abs:
   "\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)"
   by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
 
 lemma sum_list_mono:
   fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
   shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
 by (induct xs) (simp, simp add: add_mono)
 
 lemma sum_list_strict_mono:
   fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, strict_ordered_ab_semigroup_add}"
   shows "\<lbrakk> xs \<noteq> [];  \<And>x. x \<in> set xs \<Longrightarrow> f x < g x \<rbrakk>
     \<Longrightarrow> sum_list (map f xs) < sum_list (map g xs)"
 proof (induction xs)
   case Nil thus ?case by simp
 next
   case C: (Cons _ xs)
   show ?case
   proof (cases xs)
     case Nil thus ?thesis using C.prems by simp
   next
     case Cons thus ?thesis using C by(simp add: add_strict_mono)
   qed
 qed
 
 lemma (in monoid_add) sum_list_distinct_conv_sum_set:
   "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)"
   by (induct xs) simp_all
 
 lemma (in monoid_add) interv_sum_list_conv_sum_set_nat:
   "sum_list (map f [m..<n]) = sum f (set [m..<n])"
   by (simp add: sum_list_distinct_conv_sum_set)
 
 lemma (in monoid_add) interv_sum_list_conv_sum_set_int:
   "sum_list (map f [k..l]) = sum f (set [k..l])"
   by (simp add: sum_list_distinct_conv_sum_set)
 
 text \<open>General equivalence between \<^const>\<open>sum_list\<close> and \<^const>\<open>sum\<close>\<close>
 lemma (in monoid_add) sum_list_sum_nth:
   "sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   using interv_sum_list_conv_sum_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth)
 
 lemma sum_list_map_eq_sum_count:
   "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) (set xs)"
 proof(induction xs)
   case (Cons x xs)
   show ?case (is "?l = ?r")
   proof cases
     assume "x \<in> set xs"
     have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH)
     also have "set xs = insert x (set xs - {x})" using \<open>x \<in> set xs\<close>by blast
     also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r"
       by (simp add: sum.insert_remove eq_commute)
     finally show ?thesis .
   next
     assume "x \<notin> set xs"
     hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast
     thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>)
   qed
 qed simp
 
 lemma sum_list_map_eq_sum_count2:
 assumes "set xs \<subseteq> X" "finite X"
 shows "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) X"
 proof-
   let ?F = "\<lambda>x. count_list xs x * f x"
   have "sum ?F X = sum ?F (set xs \<union> (X - set xs))"
     using Un_absorb1[OF assms(1)] by(simp)
   also have "\<dots> = sum ?F (set xs)"
     using assms(2)
     by(simp add: sum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel)
   finally show ?thesis by(simp add:sum_list_map_eq_sum_count)
 qed
 
 lemma sum_list_replicate: "sum_list (replicate n c) = of_nat n * c"
 by(induction n)(auto simp add: distrib_right)
 
 
 lemma sum_list_nonneg:
     "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
   by (induction xs) simp_all
 
 lemma sum_list_Suc:
   "sum_list (map (\<lambda>x. Suc(f x)) xs) = sum_list (map f xs) + length xs"
 by(induction xs; simp)
 
 lemma (in monoid_add) sum_list_map_filter':
   "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)"
   by (induction xs) simp_all
 
 text \<open>Summation of a strictly ascending sequence with length \<open>n\<close>
   can be upper-bounded by summation over \<open>{0..<n}\<close>.\<close>
 
 lemma sorted_wrt_less_sum_mono_lowerbound:
   fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)"
   assumes mono: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y"
   shows "sorted_wrt (<) ns \<Longrightarrow>
     (\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)"
 proof (induction ns rule: rev_induct)
   case Nil
   then show ?case by simp
 next
   case (snoc n ns)
   have "sum f {0..<length (ns @ [n])}
       = sum f {0..<length ns} + f (length ns)"
     by simp
   also have "sum f {0..<length ns} \<le> sum_list (map f ns)"
     using snoc by (auto simp: sorted_wrt_append)
   also have "length ns \<le> n"
     using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto
   finally have "sum f {0..<length (ns @ [n])} \<le> sum_list (map f ns) + f n"
     using mono add_mono by blast
   thus ?case by simp
 qed
 
 
 subsection \<open>Horner sums\<close>
 
 context comm_semiring_0
 begin
 
 definition horner_sum :: \<open>('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'a\<close>
   where horner_sum_foldr: \<open>horner_sum f a xs = foldr (\<lambda>x b. f x + a * b) xs 0\<close>
 
 lemma horner_sum_simps [simp]:
   \<open>horner_sum f a [] = 0\<close>
   \<open>horner_sum f a (x # xs) = f x + a * horner_sum f a xs\<close>
   by (simp_all add: horner_sum_foldr)
 
 lemma horner_sum_eq_sum_funpow:
   \<open>horner_sum f a xs = (\<Sum>n = 0..<length xs. ((*) a ^^ n) (f (xs ! n)))\<close>
 proof (induction xs)
   case Nil
   then show ?case
     by simp
 next
   case (Cons x xs)
   then show ?case
     by (simp add: sum.atLeast0_lessThan_Suc_shift sum_distrib_left del: sum.op_ivl_Suc)
 qed
 
 end
 
 context
   includes lifting_syntax
 begin
 
 lemma horner_sum_transfer [transfer_rule]:
   \<open>((B ===> A) ===> A ===> list_all2 B ===> A) horner_sum horner_sum\<close>
   if [transfer_rule]: \<open>A 0 0\<close>
     and [transfer_rule]: \<open>(A ===> A ===> A) (+) (+)\<close>
     and [transfer_rule]: \<open>(A ===> A ===> A) (*) (*)\<close>
   by (unfold horner_sum_foldr) transfer_prover
 
 end
 
 context comm_semiring_1
 begin
 
 lemma horner_sum_eq_sum:
   \<open>horner_sum f a xs = (\<Sum>n = 0..<length xs. f (xs ! n) * a ^ n)\<close>
 proof -
   have \<open>(*) a ^^ n = (*) (a ^ n)\<close> for n
     by (induction n) (simp_all add: ac_simps)
   then show ?thesis
     by (simp add: horner_sum_eq_sum_funpow ac_simps)
 qed
 
 lemma horner_sum_append:
   \<open>horner_sum f a (xs @ ys) = horner_sum f a xs + a ^ length xs * horner_sum f a ys\<close>
   using sum.atLeastLessThan_shift_bounds [of _ 0 \<open>length xs\<close> \<open>length ys\<close>]
     atLeastLessThan_add_Un [of 0 \<open>length xs\<close> \<open>length ys\<close>]
   by (simp add: horner_sum_eq_sum sum_distrib_left sum.union_disjoint ac_simps nth_append power_add)
 
 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>
 
 lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   by (induct n) (auto simp add: comp_def length_concat sum_list_triv)
 
 lemma distinct_n_lists:
   assumes "distinct xs"
   shows "distinct (List.n_lists n xs)"
 proof (rule card_distinct)
   from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
   proof (induct n)
     case 0 then show ?case by simp
   next
     case (Suc n)
     moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
       = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
       by (rule card_UN_disjoint) auto
     moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
       by (rule card_image) (simp add: inj_on_def)
     ultimately show ?case by auto
   qed
   also have "\<dots> = length xs ^ n" by (simp add: card_length)
   finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
     by (simp add: length_n_lists)
 qed
 
 
 subsection \<open>Tools setup\<close>
 
 lemmas sum_code = sum.set_conv_list
 
 lemma sum_set_upto_conv_sum_list_int [code_unfold]:
   "sum f (set [i..j::int]) = sum_list (map f [i..j])"
   by (simp add: interv_sum_list_conv_sum_set_int)
 
 lemma sum_set_upt_conv_sum_list_nat [code_unfold]:
   "sum f (set [m..<n]) = sum_list (map f [m..<n])"
   by (simp add: interv_sum_list_conv_sum_set_nat)
 
 
 subsection \<open>List product\<close>
 
 context monoid_mult
 begin
 
 sublocale prod_list: monoid_list times 1
 defines
   prod_list = prod_list.F ..
 
 end
 
 context comm_monoid_mult
 begin
 
 sublocale prod_list: comm_monoid_list times 1
 rewrites
   "monoid_list.F times 1 = prod_list"
 proof -
   show "comm_monoid_list times 1" ..
   then interpret prod_list: comm_monoid_list times 1 .
   from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
 qed
 
 sublocale prod: comm_monoid_list_set times 1
 rewrites
   "monoid_list.F times 1 = prod_list"
   and "comm_monoid_set.F times 1 = prod"
 proof -
   show "comm_monoid_list_set times 1" ..
   then interpret prod: comm_monoid_list_set times 1 .
   from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
   from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
 qed
 
 end
 
 text \<open>Some syntactic sugar:\<close>
 
 syntax (ASCII)
   "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
 syntax
   "_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"
 
 context
   includes lifting_syntax
 begin
 
 lemma prod_list_transfer [transfer_rule]:
   "(list_all2 A ===> A) prod_list prod_list"
     if [transfer_rule]: "A 1 1" "(A ===> A ===> A) (*) (*)"
   unfolding prod_list.eq_foldr [abs_def]
   by transfer_prover
 
 end
 
 lemma prod_list_zero_iff:
   "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
   by (induction xs) simp_all
 
 end
diff --git a/src/HOL/Library/Char_ord.thy b/src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy
+++ b/src/HOL/Library/Char_ord.thy
@@ -1,130 +1,51 @@
 (*  Title:      HOL/Library/Char_ord.thy
     Author:     Norbert Voelker, Florian Haftmann
 *)
 
 section \<open>Order on characters\<close>
 
 theory Char_ord
   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
 
 definition less_eq_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
   where \<open>c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)\<close>
 
 definition less_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
   where \<open>c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)\<close>
 
 
 instance
   by standard (auto simp add: less_eq_char_def less_char_def)
 
 end
 
 lemma less_eq_char_simp [simp, code]:
   \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
     \<longleftrightarrow> lexordp_eq [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
   by (simp only: less_eq_char_def of_char_def char.sel horner_sum_less_eq_iff_lexordp_eq list.size) simp
 
 lemma less_char_simp [simp, code]:
   \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
     \<longleftrightarrow> ord_class.lexordp [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
   by (simp only: less_char_def of_char_def char.sel horner_sum_less_iff_lexordp list.size) simp
 
 instantiation char :: distrib_lattice
 begin
 
 definition \<open>(inf :: char \<Rightarrow> _) = min\<close>
 definition \<open>(sup :: char \<Rightarrow> _) = max\<close>
 
 instance
   by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
 
 end
 
 code_identifier
   code_module Char_ord \<rightharpoonup>
     (SML) Str and (OCaml) Str and (Haskell) Str and (Scala) Str
 
 end
diff --git a/src/HOL/Library/Code_Abstract_Char.thy b/src/HOL/Library/Code_Abstract_Char.thy
--- a/src/HOL/Library/Code_Abstract_Char.thy
+++ b/src/HOL/Library/Code_Abstract_Char.thy
@@ -1,186 +1,190 @@
 (*  Title:      HOL/Library/Code_Abstract_Char.thy
     Author:     Florian Haftmann, TU Muenchen
     Author:     René Thiemann, UIBK
 *)
 
 theory Code_Abstract_Char
   imports 
     Main
     "HOL-Library.Char_ord" 
 begin
 
 definition Chr :: \<open>integer \<Rightarrow> char\<close>
   where [simp]: \<open>Chr = char_of\<close>
 
 lemma char_of_integer_of_char [code abstype]:
   \<open>Chr (integer_of_char c) = c\<close>
   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]:
   \<open>byte b0 b1 b2 b3 b4 b5 b6 b7 = (
     let
       s0 = if b0 then 1 else 0;
       s1 = if b1 then s0 + 2 else s0;
       s2 = if b2 then s1 + 4 else s1;
       s3 = if b3 then s2 + 8 else s2;
       s4 = if b4 then s3 + 16 else s3;
       s5 = if b5 then s4 + 32 else s4;
       s6 = if b6 then s5 + 64 else s5;
       s7 = if b7 then s6 + 128 else s6
     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)
                      
 lemma digit_0_code [code]:
   \<open>digit0 c \<longleftrightarrow> bit (integer_of_char c) 0\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma digit_1_code [code]:
   \<open>digit1 c \<longleftrightarrow> bit (integer_of_char c) 1\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma digit_2_code [code]:
   \<open>digit2 c \<longleftrightarrow> bit (integer_of_char c) 2\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma digit_3_code [code]:
   \<open>digit3 c \<longleftrightarrow> bit (integer_of_char c) 3\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma digit_4_code [code]:
   \<open>digit4 c \<longleftrightarrow> bit (integer_of_char c) 4\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma digit_5_code [code]:
   \<open>digit5 c \<longleftrightarrow> bit (integer_of_char c) 5\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma digit_6_code [code]:
   \<open>digit6 c \<longleftrightarrow> bit (integer_of_char c) 6\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma digit_7_code [code]:
   \<open>digit7 c \<longleftrightarrow> bit (integer_of_char c) 7\<close>
   by (cases c) (simp add: integer_of_char_def)
 
 lemma case_char_code [code]:
   \<open>case_char f c = f (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) (digit7 c)\<close>
   by (fact char.case_eq_if)
 
 lemma rec_char_code [code]:
   \<open>rec_char f c = f (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) (digit7 c)\<close>
   by (cases c) simp
 
 lemma char_of_code [code]:
   \<open>integer_of_char (char_of a) =
     byte (bit a 0) (bit a 1) (bit a 2) (bit a 3) (bit a 4) (bit a 5) (bit a 6) (bit a 7)\<close>
   by (simp add: char_of_def integer_of_char_def)
 
 lemma ascii_of_code [code]:
   \<open>integer_of_char (String.ascii_of c) = (let k = integer_of_char c in if k < 128 then k else k - 128)\<close>
 proof (cases \<open>of_char c < (128 :: integer)\<close>)
   case True
   moreover have \<open>(of_nat 0 :: integer) \<le> of_nat (of_char c)\<close>
     by simp
   then have \<open>(0 :: integer) \<le> of_char c\<close>
     by (simp only: of_nat_0 of_nat_of_char)
   ultimately show ?thesis
     by (simp add: Let_def integer_of_char_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
 next
   case False
   then have \<open>(128 :: integer) \<le> of_char c\<close>
     by simp
   moreover have \<open>of_nat (of_char c) < (of_nat 256 :: integer)\<close>
     by (simp only: of_nat_less_iff) simp
   then have \<open>of_char c < (256 :: integer)\<close>
     by (simp add: of_nat_of_char)
   moreover define k :: integer where \<open>k = of_char c - 128\<close>
   then have \<open>of_char c = k + 128\<close>
     by simp
   ultimately show ?thesis
     by (simp add: Let_def integer_of_char_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
 qed    
 
 lemma equal_char_code [code]:
   \<open>HOL.equal c d \<longleftrightarrow> integer_of_char c = integer_of_char d\<close>
   by (simp add: integer_of_char_def equal)
 
 lemma less_eq_char_code [code]:
   \<open>c \<le> d \<longleftrightarrow> integer_of_char c \<le> integer_of_char d\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
 proof -
   have \<open>?P \<longleftrightarrow> of_nat (of_char c) \<le> (of_nat (of_char d) :: integer)\<close>
     by (simp add: less_eq_char_def)
   also have \<open>\<dots> \<longleftrightarrow> ?Q\<close>
     by (simp add: of_nat_of_char integer_of_char_def)
   finally show ?thesis .
 qed
 
 lemma less_char_code [code]:
   \<open>c < d \<longleftrightarrow> integer_of_char c < integer_of_char d\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
 proof -
   have \<open>?P \<longleftrightarrow> of_nat (of_char c) < (of_nat (of_char d) :: integer)\<close>
     by (simp add: less_char_def)
   also have \<open>\<dots> \<longleftrightarrow> ?Q\<close>
     by (simp add: of_nat_of_char integer_of_char_def)
   finally show ?thesis .
 qed
 
 lemma absdef_simps:
   \<open>horner_sum of_bool 2 [] = (0 :: integer)\<close>
   \<open>horner_sum of_bool 2 (False # bs) = (0 :: integer) \<longleftrightarrow> horner_sum of_bool 2 bs = (0 :: integer)\<close>
   \<open>horner_sum of_bool 2 (True # bs) = (1 :: integer) \<longleftrightarrow> horner_sum of_bool 2 bs = (0 :: integer)\<close>
   \<open>horner_sum of_bool 2 (False # bs) = (numeral (Num.Bit0 n) :: integer) \<longleftrightarrow> horner_sum of_bool 2 bs = (numeral n :: integer)\<close>
   \<open>horner_sum of_bool 2 (True # bs) = (numeral (Num.Bit1 n) :: integer) \<longleftrightarrow> horner_sum of_bool 2 bs = (numeral n :: integer)\<close>
   by auto (auto simp only: numeral_Bit0 [of n] numeral_Bit1 [of n] mult_2 [symmetric] add.commute [of _ 1] add.left_cancel mult_cancel_left)
 
 local_setup \<open>
   let
     val simps = @{thms absdef_simps integer_of_char_def of_char_Char numeral_One}
     fun prove_eqn lthy n lhs def_eqn =
       let
         val eqn = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
           (\<^term>\<open>integer_of_char\<close> $ lhs, HOLogic.mk_number \<^typ>\<open>integer\<close> n)
       in
         Goal.prove_future lthy [] [] eqn (fn {context = ctxt, ...} =>
           unfold_tac ctxt (def_eqn :: simps))
       end
     fun define n =
       let
         val s = "Char_" ^ String_Syntax.hex n;
         val b = Binding.name s;
         val b_def = Thm.def_binding b;
         val b_code = Binding.name (s ^ "_code");
       in
         Local_Theory.define ((b, Mixfix.NoSyn),
           ((Binding.empty, []), HOLogic.mk_char n))
         #-> (fn (lhs, (_, raw_def_eqn)) =>
           Local_Theory.note ((b_def, @{attributes [code_abbrev]}), [HOLogic.mk_obj_eq raw_def_eqn])
           #-> (fn (_, [def_eqn]) => `(fn lthy => prove_eqn lthy n lhs def_eqn))
           #-> (fn raw_code_eqn => Local_Theory.note ((b_code, []), [raw_code_eqn]))
           #-> (fn (_, [code_eqn]) => Code.declare_abstract_eqn code_eqn))
       end
   in
     fold define (0 upto 255)
   end
 \<close>
 
 code_identifier
   code_module Code_Abstract_Char \<rightharpoonup>
     (SML) Str and (OCaml) Str and (Haskell) Str and (Scala) Str
 
 end
diff --git a/src/HOL/String.thy b/src/HOL/String.thy
--- a/src/HOL/String.thy
+++ b/src/HOL/String.thy
@@ -1,816 +1,820 @@
 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
 
 section \<open>Character and string types\<close>
 
 theory String
 imports Enum Bit_Operations Code_Numeral
 begin
 
 subsection \<open>Strings as list of bytes\<close>
 
 text \<open>
   When modelling strings, we follow the approach given
   in \<^url>\<open>https://utf8everywhere.org/\<close>:
 
   \<^item> Strings are a list of bytes (8 bit).
 
   \<^item> Byte values from 0 to 127 are US-ASCII.
 
   \<^item> Byte values from 128 to 255 are uninterpreted blobs.
 \<close>
 
 subsubsection \<open>Bytes as datatype\<close>
 
 datatype char =
   Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
        (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)
 
 context comm_semiring_1
 begin
 
 definition of_char :: \<open>char \<Rightarrow> 'a\<close>
   where \<open>of_char c = horner_sum of_bool 2 [digit0 c, digit1 c, digit2 c, digit3 c, digit4 c, digit5 c, digit6 c, digit7 c]\<close>
 
 lemma of_char_Char [simp]:
   \<open>of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
     horner_sum of_bool 2 [b0, b1, b2, b3, b4, b5, b6, b7]\<close>
   by (simp add: of_char_def)
 
 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
 
+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
 
 definition char_of :: \<open>'a \<Rightarrow> char\<close>
   where \<open>char_of n = Char (bit n 0) (bit n 1) (bit n 2) (bit n 3) (bit n 4) (bit n 5) (bit n 6) (bit n 7)\<close>
 
 lemma char_of_take_bit_eq:
   \<open>char_of (take_bit n m) = char_of m\<close> if \<open>n \<ge> 8\<close>
   using that by (simp add: char_of_def bit_take_bit_iff)
 
 lemma char_of_char [simp]:
   \<open>char_of (of_char c) = c\<close>
   by (simp only: of_char_def char_of_def bit_horner_sum_bit_iff) simp
 
 lemma char_of_comp_of_char [simp]:
   "char_of \<circ> of_char = id"
   by (simp add: fun_eq_iff)
 
 lemma inj_of_char:
   \<open>inj of_char\<close>
 proof (rule injI)
   fix c d
   assume "of_char c = of_char d"
   then have "char_of (of_char c) = char_of (of_char d)"
     by simp
   then show "c = d"
     by simp
 qed
 
 lemma of_char_eqI:
   \<open>c = d\<close> if \<open>of_char c = of_char d\<close>
   using that inj_of_char by (simp add: inj_eq)
 
 lemma of_char_eq_iff [simp]:
   \<open>of_char c = of_char d \<longleftrightarrow> c = d\<close>
   by (auto intro: of_char_eqI)
 
 lemma of_char_of [simp]:
   \<open>of_char (char_of a) = a mod 256\<close>
 proof -
   have \<open>[0..<8] = [0, Suc 0, 2, 3, 4, 5, 6, 7 :: nat]\<close>
     by (simp add: upt_eq_Cons_conv)
   then have \<open>[bit a 0, bit a 1, bit a 2, bit a 3, bit a 4, bit a 5, bit a 6, bit a 7] = map (bit a) [0..<8]\<close>
     by simp
   then have \<open>of_char (char_of a) = take_bit 8 a\<close>
     by (simp only: char_of_def of_char_def char.sel horner_sum_bit_eq_take_bit)
   then show ?thesis
     by (simp add: take_bit_eq_mod)
 qed
 
 lemma char_of_mod_256 [simp]:
   \<open>char_of (n mod 256) = char_of n\<close>
   by (rule of_char_eqI) simp
 
 lemma of_char_mod_256 [simp]:
   \<open>of_char c mod 256 = of_char c\<close>
 proof -
   have \<open>of_char (char_of (of_char c)) mod 256 = of_char (char_of (of_char c))\<close>
     by (simp only: of_char_of) simp
   then show ?thesis
     by simp
 qed
 
 lemma char_of_quasi_inj [simp]:
   \<open>char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
 proof
   assume ?Q
   then show ?P
     by (auto intro: of_char_eqI)
 next
   assume ?P
   then have \<open>of_char (char_of m) = of_char (char_of n)\<close>
     by simp
   then show ?Q
     by simp
 qed
 
 lemma char_of_eq_iff:
   \<open>char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c\<close>
   by (auto intro: of_char_eqI simp add: take_bit_eq_mod)
 
 lemma char_of_nat [simp]:
   \<open>char_of (of_nat n) = char_of n\<close>
   by (simp add: char_of_def String.char_of_def drop_bit_of_nat bit_simps possible_bit_def)
 
 end
 
 lemma inj_on_char_of_nat [simp]:
   "inj_on char_of {0::nat..<256}"
   by (rule inj_onI) simp
 
 lemma nat_of_char_less_256 [simp]:
   "of_char c < (256 :: nat)"
 proof -
   have "of_char c mod (256 :: nat) < 256"
     by arith
   then show ?thesis by simp
 qed
 
 lemma range_nat_of_char:
   "range of_char = {0::nat..<256}"
 proof (rule; rule)
   fix n :: nat
   assume "n \<in> range of_char"
   then show "n \<in> {0..<256}"
     by auto
 next
   fix n :: nat
   assume "n \<in> {0..<256}"
   then have "n = of_char (char_of n)"
     by simp
   then show "n \<in> range of_char"
     by (rule range_eqI)
 qed
 
 lemma UNIV_char_of_nat:
   "UNIV = char_of ` {0::nat..<256}"
 proof -
   have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}"
     by (auto simp add: range_nat_of_char intro!: image_eqI)
   with inj_of_char [where ?'a = nat] show ?thesis
     by (simp add: inj_image_eq_iff)
 qed
 
 lemma card_UNIV_char:
   "card (UNIV :: char set) = 256"
   by (auto simp add: UNIV_char_of_nat card_image)
 
 context
   includes lifting_syntax integer.lifting natural.lifting
 begin
 
 lemma [transfer_rule]:
   \<open>(pcr_integer ===> (=)) char_of char_of\<close>
   by (unfold char_of_def) transfer_prover
 
 lemma [transfer_rule]:
   \<open>((=) ===> pcr_integer) of_char of_char\<close>
   by (unfold of_char_def) transfer_prover
 
 lemma [transfer_rule]:
   \<open>(pcr_natural ===> (=)) char_of char_of\<close>
   by (unfold char_of_def) transfer_prover
 
 lemma [transfer_rule]:
   \<open>((=) ===> pcr_natural) of_char of_char\<close>
   by (unfold of_char_def) transfer_prover
 
 end
 
 lifting_update integer.lifting
 lifting_forget integer.lifting
 
 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 _")
 
 type_synonym string = "char list"
 
 syntax
   "_String" :: "str_position \<Rightarrow> string"    ("_")
 
 ML_file \<open>Tools/string_syntax.ML\<close>
 
 instantiation char :: enum
 begin
 
 definition
   "Enum.enum = [
     CHR 0x00, CHR 0x01, CHR 0x02, CHR 0x03,
     CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07,
     CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B,
     CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F,
     CHR 0x10, CHR 0x11, CHR 0x12, CHR 0x13,
     CHR 0x14, CHR 0x15, CHR 0x16, CHR 0x17,
     CHR 0x18, CHR 0x19, CHR 0x1A, CHR 0x1B,
     CHR 0x1C, CHR 0x1D, CHR 0x1E, CHR 0x1F,
     CHR '' '', CHR ''!'', CHR 0x22, CHR ''#'',
     CHR ''$'', CHR ''%'', CHR ''&'', CHR 0x27,
     CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
     CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
     CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
     CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
     CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
     CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
     CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
     CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
     CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
     CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
     CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
     CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
     CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
     CHR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
     CHR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
     CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
     CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
     CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
     CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
     CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
     CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
     CHR ''|'', CHR ''}'', CHR ''~'', CHR 0x7F,
     CHR 0x80, CHR 0x81, CHR 0x82, CHR 0x83,
     CHR 0x84, CHR 0x85, CHR 0x86, CHR 0x87,
     CHR 0x88, CHR 0x89, CHR 0x8A, CHR 0x8B,
     CHR 0x8C, CHR 0x8D, CHR 0x8E, CHR 0x8F,
     CHR 0x90, CHR 0x91, CHR 0x92, CHR 0x93,
     CHR 0x94, CHR 0x95, CHR 0x96, CHR 0x97,
     CHR 0x98, CHR 0x99, CHR 0x9A, CHR 0x9B,
     CHR 0x9C, CHR 0x9D, CHR 0x9E, CHR 0x9F,
     CHR 0xA0, CHR 0xA1, CHR 0xA2, CHR 0xA3,
     CHR 0xA4, CHR 0xA5, CHR 0xA6, CHR 0xA7,
     CHR 0xA8, CHR 0xA9, CHR 0xAA, CHR 0xAB,
     CHR 0xAC, CHR 0xAD, CHR 0xAE, CHR 0xAF,
     CHR 0xB0, CHR 0xB1, CHR 0xB2, CHR 0xB3,
     CHR 0xB4, CHR 0xB5, CHR 0xB6, CHR 0xB7,
     CHR 0xB8, CHR 0xB9, CHR 0xBA, CHR 0xBB,
     CHR 0xBC, CHR 0xBD, CHR 0xBE, CHR 0xBF,
     CHR 0xC0, CHR 0xC1, CHR 0xC2, CHR 0xC3,
     CHR 0xC4, CHR 0xC5, CHR 0xC6, CHR 0xC7,
     CHR 0xC8, CHR 0xC9, CHR 0xCA, CHR 0xCB,
     CHR 0xCC, CHR 0xCD, CHR 0xCE, CHR 0xCF,
     CHR 0xD0, CHR 0xD1, CHR 0xD2, CHR 0xD3,
     CHR 0xD4, CHR 0xD5, CHR 0xD6, CHR 0xD7,
     CHR 0xD8, CHR 0xD9, CHR 0xDA, CHR 0xDB,
     CHR 0xDC, CHR 0xDD, CHR 0xDE, CHR 0xDF,
     CHR 0xE0, CHR 0xE1, CHR 0xE2, CHR 0xE3,
     CHR 0xE4, CHR 0xE5, CHR 0xE6, CHR 0xE7,
     CHR 0xE8, CHR 0xE9, CHR 0xEA, CHR 0xEB,
     CHR 0xEC, CHR 0xED, CHR 0xEE, CHR 0xEF,
     CHR 0xF0, CHR 0xF1, CHR 0xF2, CHR 0xF3,
     CHR 0xF4, CHR 0xF5, CHR 0xF6, CHR 0xF7,
     CHR 0xF8, CHR 0xF9, CHR 0xFA, CHR 0xFB,
     CHR 0xFC, CHR 0xFD, CHR 0xFE, CHR 0xFF]"
 
 definition
   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
 
 definition
   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
 
 lemma enum_char_unfold:
   "Enum.enum = map char_of [0..<256]"
 proof -
   have "map (of_char :: char \<Rightarrow> nat) Enum.enum = [0..<256]"
     by (simp add: enum_char_def of_char_def upt_conv_Cons_Cons numeral_2_eq_2 [symmetric])
   then have "map char_of (map (of_char :: char \<Rightarrow> nat) Enum.enum) =
     map char_of [0..<256]"
     by simp
   then show ?thesis
     by simp
 qed
 
 instance proof
   show UNIV: "UNIV = set (Enum.enum :: char list)"
     by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
   show "distinct (Enum.enum :: char list)"
     by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
     by (simp add: UNIV enum_all_char_def list_all_iff)
   show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
     by (simp add: UNIV enum_ex_char_def list_ex_iff)
 qed
 
 end
 
 lemma linorder_char:
   "class.linorder (\<lambda>c d. of_char c \<le> (of_char d :: nat)) (\<lambda>c d. of_char c < (of_char d :: nat))"
   by standard auto
 
 text \<open>Optimized version for execution\<close>
 
 definition char_of_integer :: "integer \<Rightarrow> char"
   where [code_abbrev]: "char_of_integer = char_of"
 
 definition integer_of_char :: "char \<Rightarrow> integer"
   where [code_abbrev]: "integer_of_char = of_char"
 
 lemma char_of_integer_code [code]:
   "char_of_integer k = (let
      (q0, b0) = bit_cut_integer k;
      (q1, b1) = bit_cut_integer q0;
      (q2, b2) = bit_cut_integer q1;
      (q3, b3) = bit_cut_integer q2;
      (q4, b4) = bit_cut_integer q3;
      (q5, b5) = bit_cut_integer q4;
      (q6, b6) = bit_cut_integer q5;
      (_, b7) = bit_cut_integer q6
     in Char b0 b1 b2 b3 b4 b5 b6 b7)"
   by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq bit_iff_odd_drop_bit drop_bit_eq_div)
 
 lemma integer_of_char_code [code]:
   "integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
     ((((((of_bool b7 * 2 + of_bool b6) * 2 +
       of_bool b5) * 2 + of_bool b4) * 2 +
         of_bool b3) * 2 + of_bool b2) * 2 +
           of_bool b1) * 2 + of_bool b0"
   by (simp add: integer_of_char_def of_char_def)
 
 
 subsection \<open>Strings as dedicated type for target language code generation\<close>
 
 subsubsection \<open>Logical specification\<close>
 
 context
 begin
 
 qualified definition ascii_of :: "char \<Rightarrow> char"
   where "ascii_of c = Char (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) False"
 
 qualified lemma ascii_of_Char [simp]:
   "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)
 
 qualified lemma ascii_of_idem:
   "ascii_of c = c" if "\<not> digit7 c"
   using that by (cases c) simp
 
 qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
   morphisms explode Abs_literal
 proof
   show "[] \<in> {cs. \<forall>c\<in>set cs. \<not> digit7 c}"
     by simp
 qed
 
 qualified setup_lifting type_definition_literal
 
 qualified lift_definition implode :: "string \<Rightarrow> literal"
   is "map ascii_of"
   by auto
 
 qualified lemma implode_explode_eq [simp]:
   "String.implode (String.explode s) = s"
 proof transfer
   fix cs
   show "map ascii_of cs = cs" if "\<forall>c\<in>set cs. \<not> digit7 c"
     using that
       by (induction cs) (simp_all add: ascii_of_idem)
 qed
 
 qualified lemma explode_implode_eq [simp]:
   "String.explode (String.implode cs) = map ascii_of cs"
   by transfer rule
 
 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>
 
 text \<open>
   Logical ground representations for literals are:
 
   \<^enum> \<open>0\<close> for the empty literal;
 
   \<^enum> \<open>Literal b0 \<dots> b6 s\<close> for a literal starting with one
     character and continued by another literal.
 
   Syntactic representations for literals are:
 
   \<^enum> Printable text as string prefixed with \<open>STR\<close>;
 
   \<^enum> A single ascii value as numerical hexadecimal value prefixed with \<open>STR\<close>.
 \<close>
 
 instantiation String.literal :: zero
 begin
 
 context
 begin
 
 qualified lift_definition zero_literal :: String.literal
   is Nil
   by simp
 
 instance ..
 
 end
 
 end
 
 context
 begin
 
 qualified abbreviation (output) empty_literal :: String.literal
   where "empty_literal \<equiv> 0"
 
 qualified lift_definition Literal :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
   is "\<lambda>b0 b1 b2 b3 b4 b5 b6 cs. Char b0 b1 b2 b3 b4 b5 b6 False # cs"
   by auto
 
 qualified lemma Literal_eq_iff [simp]:
   "Literal b0 b1 b2 b3 b4 b5 b6 s = Literal c0 c1 c2 c3 c4 c5 c6 t
      \<longleftrightarrow> (b0 \<longleftrightarrow> c0) \<and> (b1 \<longleftrightarrow> c1) \<and> (b2 \<longleftrightarrow> c2) \<and> (b3 \<longleftrightarrow> c3)
          \<and> (b4 \<longleftrightarrow> c4) \<and> (b5 \<longleftrightarrow> c5) \<and> (b6 \<longleftrightarrow> c6) \<and> s = t"
   by transfer simp
 
 qualified lemma empty_neq_Literal [simp]:
   "empty_literal \<noteq> Literal b0 b1 b2 b3 b4 b5 b6 s"
   by transfer simp
 
 qualified lemma Literal_neq_empty [simp]:
   "Literal b0 b1 b2 b3 b4 b5 b6 s \<noteq> empty_literal"
   by transfer simp
 
 end
 
 code_datatype "0 :: String.literal" String.Literal
 
 syntax
   "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
   "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
 
 ML_file \<open>Tools/literal.ML\<close>
 
 
 subsubsection \<open>Operations\<close>
 
 instantiation String.literal :: plus
 begin
 
 context
 begin
 
 qualified lift_definition plus_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal"
   is "(@)"
   by auto
 
 instance ..
 
 end
 
 end
 
 instance String.literal :: monoid_add
   by (standard; transfer) simp_all
 
 instantiation String.literal :: size
 begin
 
 context
   includes literal.lifting
 begin
 
 lift_definition size_literal :: "String.literal \<Rightarrow> nat"
   is length .
 
 end
 
 instance ..
 
 end
 
 instantiation String.literal :: equal
 begin
 
 context
 begin
 
 qualified lift_definition equal_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
   is HOL.equal .
 
 instance
   by (standard; transfer) (simp add: equal)
 
 end
 
 end
 
 instantiation String.literal :: linorder
 begin
 
 context
 begin
 
 qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
   is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
   .
 
 qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
   is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
   .
 
 instance proof -
   from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
     "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
     by (rule linorder.lexordp_linorder)
   show "PROP ?thesis"
     by (standard; transfer) (simp_all add: less_le_not_le linear)
 qed
 
 end
 
 end
 
 lemma infinite_literal:
   "infinite (UNIV :: String.literal set)"
 proof -
   define S where "S = range (\<lambda>n. replicate n CHR ''A'')"
   have "inj_on String.implode S"
   proof (rule inj_onI)
     fix cs ds
     assume "String.implode cs = String.implode ds"
     then have "String.explode (String.implode cs) = String.explode (String.implode ds)"
       by simp
     moreover assume "cs \<in> S" and "ds \<in> S"
     ultimately show "cs = ds"
       by (auto simp add: S_def)
   qed
   moreover have "infinite S"
     by (auto simp add: S_def dest: finite_range_imageI [of _ length])
   ultimately have "infinite (String.implode ` S)"
     by (simp add: finite_image_iff)
   then show ?thesis
     by (auto intro: finite_subset)
 qed
 
 
 subsubsection \<open>Executable conversions\<close>
 
 context
 begin
 
 qualified lift_definition asciis_of_literal :: "String.literal \<Rightarrow> integer list"
   is "map of_char"
   .
 
 qualified lemma asciis_of_zero [simp, code]:
   "asciis_of_literal 0 = []"
   by transfer simp
 
 qualified lemma asciis_of_Literal [simp, code]:
   "asciis_of_literal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) =
     of_char (Char b0 b1 b2 b3 b4 b5 b6 False) # asciis_of_literal s "
   by transfer simp
 
 qualified lift_definition literal_of_asciis :: "integer list \<Rightarrow> String.literal"
   is "map (String.ascii_of \<circ> char_of)"
   by auto
 
 qualified lemma literal_of_asciis_Nil [simp, code]:
   "literal_of_asciis [] = 0"
   by transfer simp
 
 qualified lemma literal_of_asciis_Cons [simp, code]:
   "literal_of_asciis (k # ks) = (case char_of k
     of Char b0 b1 b2 b3 b4 b5 b6 b7 \<Rightarrow> String.Literal b0 b1 b2 b3 b4 b5 b6 (literal_of_asciis ks))"
   by (simp add: char_of_def) (transfer, simp add: char_of_def)
 
 qualified lemma literal_of_asciis_of_literal [simp]:
   "literal_of_asciis (asciis_of_literal s) = s"
 proof transfer
   fix cs
   assume "\<forall>c\<in>set cs. \<not> digit7 c"
   then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs"
     by (induction cs) (simp_all add: String.ascii_of_idem)
 qed
 
 qualified lemma explode_code [code]:
   "String.explode s = map char_of (asciis_of_literal s)"
   by transfer simp
 
 qualified lemma implode_code [code]:
   "String.implode cs = literal_of_asciis (map of_char cs)"
   by transfer simp
 
 qualified lemma equal_literal [code]:
   "HOL.equal (String.Literal b0 b1 b2 b3 b4 b5 b6 s)
     (String.Literal a0 a1 a2 a3 a4 a5 a6 r)
     \<longleftrightarrow> (b0 \<longleftrightarrow> a0) \<and> (b1 \<longleftrightarrow> a1) \<and> (b2 \<longleftrightarrow> a2) \<and> (b3 \<longleftrightarrow> a3)
       \<and> (b4 \<longleftrightarrow> a4) \<and> (b5 \<longleftrightarrow> a5) \<and> (b6 \<longleftrightarrow> a6) \<and> (s = r)"
   by (simp add: equal)
 
 end
 
 
 subsubsection \<open>Technical code generation setup\<close>
 
 text \<open>Alternative constructor for generated computations\<close>
 
 context
 begin
 
 qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
   where [simp]: "Literal' = String.Literal"
 
 lemma [code]:
   \<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
     [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s\<close>
 proof -
   have \<open>foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0 = of_char (Char b0 b1 b2 b3 b4 b5 b6 False)\<close>
     by simp
   moreover have \<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
     [of_char (Char b0 b1 b2 b3 b4 b5 b6 False)] + s\<close>
     by (unfold Literal'_def) (transfer, simp only: list.simps comp_apply char_of_char, simp)
   ultimately show ?thesis
     by simp
 qed
 
 lemma [code_computation_unfold]:
   "String.Literal = Literal'"
   by simp
 
 end
 
 code_reserved SML string String Char List
 code_reserved OCaml string String Char List
 code_reserved Haskell Prelude
 code_reserved Scala string
 
 code_identifier
   code_module String \<rightharpoonup>
     (SML) Str and (OCaml) Str and (Haskell) Str and (Scala) Str
 
 code_printing
   type_constructor String.literal \<rightharpoonup>
     (SML) "string"
     and (OCaml) "string"
     and (Haskell) "String"
     and (Scala) "String"
 | constant "STR ''''" \<rightharpoonup>
     (SML) "\"\""
     and (OCaml) "\"\""
     and (Haskell) "\"\""
     and (Scala) "\"\""
 
 setup \<open>
   fold Literal.add_code ["SML", "OCaml", "Haskell", "Scala"]
 \<close>
 
 code_printing
   constant "(+) :: String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal" \<rightharpoonup>
     (SML) infixl 18 "^"
     and (OCaml) infixr 6 "^"
     and (Haskell) infixr 5 "++"
     and (Scala) infixl 7 "+"
 | constant String.literal_of_asciis \<rightharpoonup>
     (SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
     and (OCaml) "!(let xs = _
       and chr k =
         let l = Z.to'_int k
           in if 0 <= l && l < 128
           then Char.chr l
           else failwith \"Non-ASCII character in literal\"
       in String.init (List.length xs) (List.nth (List.map chr xs)))"
     and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
     and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
 | constant String.asciis_of_literal \<rightharpoonup>
     (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end)/ o String.explode)"
     and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in
       if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
     and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
     and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
 | class_instance String.literal :: equal \<rightharpoonup>
     (Haskell) -
 | constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : string) = _)"
     and (OCaml) "!((_ : string) = _)"
     and (Haskell) infix 4 "=="
     and (Scala) infixl 5 "=="
 | constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : string) <= _)"
     and (OCaml) "!((_ : string) <= _)"
     and (Haskell) infix 4 "<="
     \<comment> \<open>Order operations for \<^typ>\<open>String.literal\<close> work in Haskell only
           if no type class instance needs to be generated, because String = [Char] in Haskell
           and \<^typ>\<open>char list\<close> need not have the same order as \<^typ>\<open>String.literal\<close>.\<close>
     and (Scala) infixl 4 "<="
     and (Eval) infixl 6 "<="
 | constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : string) < _)"
     and (OCaml) "!((_ : string) < _)"
     and (Haskell) infix 4 "<"
     and (Scala) infixl 4 "<"
     and (Eval) infixl 6 "<"
 
 
 subsubsection \<open>Code generation utility\<close>
 
 setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
 
 definition abort :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
   where [simp]: "abort _ f = f ()"
 
 declare [[code drop: Code.abort]]
 
 lemma abort_cong:
   "msg = msg' \<Longrightarrow> Code.abort msg f = Code.abort msg' f"
   by simp
 
 setup \<open>Sign.map_naming Name_Space.parent_path\<close>
 
 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
 
 code_printing
   constant Code.abort \<rightharpoonup>
     (SML) "!(raise/ Fail/ _)"
     and (OCaml) "failwith"
     and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
     and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }"
 
 
 subsubsection \<open>Finally\<close>
 
 lifting_update literal.lifting
 lifting_forget literal.lifting
 
 end