diff --git a/thys/Show/Number_Parser.thy b/thys/Show/Number_Parser.thy
new file mode 100644
--- /dev/null
+++ b/thys/Show/Number_Parser.thy
@@ -0,0 +1,167 @@
+(*
+Author:  Christian Sternagel <c.sternagel@gmail.com>
+Author:  René Thiemann <rene.thiemann@uibk.ac.at>
+*)
+
+text \<open>We provide two parsers for natural numbers and integers, which are
+  verified in the sense that they are the inverse of the show-function for
+  these types. We therefore also prove that the show-functions are injective.\<close>
+theory Number_Parser
+  imports 
+    Show_Instances
+begin
+
+text \<open>We define here the bind-operations for option and sum-type. We do not 
+  import these operations from Certification_Monads.Strict-Sum and Parser-Monad,
+  since these imports would yield a cyclic dependency of 
+  the two AFP entries Show and Certification-Monads.\<close>
+
+definition obind where "obind opt f = (case opt of None \<Rightarrow> None | Some x \<Rightarrow> f x)" 
+definition sbind where "sbind su  f = (case su of Inl e \<Rightarrow> Inl e | Inr r \<Rightarrow> f r)" 
+
+context begin
+
+text \<open>A natural number parser which is proven correct:\<close>
+
+definition nat_of_digit :: "char \<Rightarrow> nat option" where
+  "nat_of_digit x \<equiv>
+    if x = CHR ''0'' then Some 0
+    else if x = CHR ''1'' then Some 1
+    else if x = CHR ''2'' then Some 2
+    else if x = CHR ''3'' then Some 3
+    else if x = CHR ''4'' then Some 4
+    else if x = CHR ''5'' then Some 5
+    else if x = CHR ''6'' then Some 6
+    else if x = CHR ''7'' then Some 7
+    else if x = CHR ''8'' then Some 8
+    else if x = CHR ''9'' then Some 9
+    else None" 
+
+private fun nat_of_string_aux :: "nat \<Rightarrow> string \<Rightarrow> nat option"
+  where
+    "nat_of_string_aux n [] = Some n" |
+    "nat_of_string_aux n (d # s) = (obind (nat_of_digit d) (\<lambda>m. nat_of_string_aux (10 * n + m) s))"
+
+definition "nat_of_string s \<equiv>
+  case if s = [] then None else nat_of_string_aux 0 s of
+    None \<Rightarrow> Inl (STR ''cannot convert \"'' + String.implode s + STR ''\" to a number'')
+  | Some n \<Rightarrow> Inr n"
+
+private lemma nat_of_string_aux_snoc:
+  "nat_of_string_aux n (s @ [c]) =
+     obind (nat_of_string_aux n s) (\<lambda> l. obind (nat_of_digit c) (\<lambda> m. Some (10 * l + m)))"
+  by (induct s arbitrary:n, auto simp: obind_def split: option.splits)
+
+private lemma nat_of_string_aux_digit:
+  assumes m10: "m < 10"
+  shows "nat_of_string_aux n (s @ string_of_digit m) =
+    obind (nat_of_string_aux n s) (\<lambda> l. Some (10 * l + m))"
+proof -
+  from m10 have "m = 0 \<or> m = 1 \<or> m = 2 \<or> m = 3 \<or> m = 4 \<or> m = 5 \<or> m = 6 \<or> m = 7 \<or> m = 8 \<or> m = 9" 
+    by presburger
+  thus ?thesis by (auto simp add: nat_of_digit_def nat_of_string_aux_snoc string_of_digit_def
+        obind_def split: option.splits)
+qed
+
+
+private lemmas shows_move = showsp_nat_append[of 0 _ "[]",simplified, folded shows_prec_nat_def]
+
+private lemma nat_of_string_aux_show: "nat_of_string_aux 0 (show m) = Some m"
+proof (induct m rule:less_induct)
+  case IH: (less m)
+  show ?case proof (cases "m < 10")
+    case m10: True
+    show ?thesis
+      apply (unfold shows_prec_nat_def)
+      apply (subst showsp_nat.simps)
+      using m10 nat_of_string_aux_digit[OF m10, of 0 "[]"]
+      by (auto simp add:shows_string_def nat_of_string_def string_of_digit_def obind_def)
+  next
+    case m: False
+    then have "m div 10 < m" by auto
+    note IH = IH[OF this]
+    show ?thesis apply (unfold shows_prec_nat_def, subst showsp_nat.simps)
+      using m apply (simp add: shows_prec_nat_def[symmetric] shows_string_def)
+      apply (subst shows_move)
+      using nat_of_string_aux_digit m IH 
+      by (auto simp: nat_of_string_def obind_def)
+  qed
+qed
+
+lemma fixes m :: nat shows show_nonemp: "show m \<noteq> []"
+  apply (unfold shows_prec_nat_def)
+  apply (subst showsp_nat.simps)
+  apply (fold shows_prec_nat_def)
+  apply (unfold o_def)
+  apply (subst shows_move)
+  apply (auto simp: shows_string_def string_of_digit_def)
+  done
+
+text \<open>The parser \<open>nat_of_string\<close> is the inverse of \<open>show\<close>.\<close>
+lemma nat_of_string_show[simp]: "nat_of_string (show m) = Inr m"
+  using nat_of_string_aux_show by (auto simp: nat_of_string_def show_nonemp)
+
+end
+
+
+text \<open>We also provide a verified parser for integers.\<close>
+
+fun safe_head where "safe_head [] = None" | "safe_head (x#xs) = Some x"
+
+definition int_of_string :: "string \<Rightarrow> String.literal + int"
+  where "int_of_string s \<equiv>
+    if safe_head s = Some (CHR ''-'') then sbind (nat_of_string (tl s)) (\<lambda> n. Inr (- int n))
+    else sbind (nat_of_string s) (\<lambda> n. Inr (int n))"
+
+definition digit_chars where "digit_chars = 
+  {CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'',
+   CHR ''7'', CHR ''8'', CHR ''9'', CHR ''0''}" 
+
+lemma range_string_of_digit: "set (string_of_digit x) \<subseteq> digit_chars" 
+  unfolding digit_chars_def string_of_digit_def by auto
+
+lemma range_showsp_nat: "set (showsp_nat p n s) \<subseteq> digit_chars \<union> set s" 
+proof (induct p n arbitrary: s rule: showsp_nat.induct)
+  case (1 p n s)
+  then show ?case using range_string_of_digit[of n] range_string_of_digit[of "n mod 10"]
+    by (auto simp: showsp_nat.simps[of p n] shows_string_def) fastforce
+qed
+
+lemma range_show_nat: "set (show (n :: nat)) \<subseteq> digit_chars" 
+  using range_showsp_nat[of 0 n Nil] unfolding shows_prec_nat_def by auto
+
+lemma int_of_string_show[simp]: "int_of_string (show x) = Inr x" 
+proof -
+  have "show x = showsp_int 0 x []" 
+    by (simp add: shows_prec_int_def)
+  also have "\<dots> = (if x < 0 then ''-'' @ show (nat (-x)) else show (nat x))" 
+    unfolding showsp_int_def if_distrib shows_prec_nat_def
+    by (simp add: shows_string_def)
+  also have "int_of_string \<dots> = Inr x" 
+  proof (cases "x < 0")
+    case True
+    thus ?thesis unfolding int_of_string_def sbind_def by simp
+  next
+    case False
+    from range_show_nat have "set (show (nat x)) \<subseteq> digit_chars" .
+    hence "CHR ''-'' \<notin> set (show (nat x))" unfolding digit_chars_def by auto
+    hence "safe_head (show (nat x)) \<noteq> Some CHR ''-''" 
+      by (cases "show (nat x)", auto) 
+    thus ?thesis using False
+      by (simp add: int_of_string_def sbind_def)
+  qed
+  finally show ?thesis .
+qed
+
+hide_const (open) obind sbind
+
+text \<open>Eventually, we derive injectivity of the show-functions for nat and int.\<close>
+
+lemma inj_show_nat: "inj (show :: nat \<Rightarrow> string)" 
+  by (rule inj_on_inverseI[of _ "\<lambda> s. case nat_of_string s of Inr x \<Rightarrow> x"], auto)
+
+lemma inj_show_int: "inj (show :: int \<Rightarrow> string)" 
+  by (rule inj_on_inverseI[of _ "\<lambda> s. case int_of_string s of Inr x \<Rightarrow> x"], auto)
+
+
+end
\ No newline at end of file
diff --git a/thys/Show/ROOT b/thys/Show/ROOT
--- a/thys/Show/ROOT
+++ b/thys/Show/ROOT
@@ -1,21 +1,22 @@
 chapter AFP
 
 session Show = Deriving +
   options [timeout = 600]
   sessions
     "HOL-Computational_Algebra"
   theories
     Show_Instances
     Show_Poly
     Show_Complex
     Show_Real_Impl
     Shows_Literal
+    Number_Parser
   document_files
     "root.bib"
     "root.tex"
 
 session Old_Datatype_Show in "Old_Datatype" = Datatype_Order_Generator +
   options [timeout = 600]
   theories
     Old_Show_Instances
     Old_Show_Examples
diff --git a/thys/Show/Show_Instances.thy b/thys/Show/Show_Instances.thy
--- a/thys/Show/Show_Instances.thy
+++ b/thys/Show/Show_Instances.thy
@@ -1,335 +1,163 @@
 (*  Title:       Show
     Author:      Christian Sternagel <c.sternagel@gmail.com>
     Author:      René Thiemann <rene.thiemann@uibk.ac.at>
     Maintainer:  Christian Sternagel <c.sternagel@gmail.com>
     Maintainer:  René Thiemann <rene.thiemann@uibk.ac.at>
 *)
 
 section \<open>Instances of the Show Class for Standard Types\<close>
 
 theory Show_Instances
   imports
     Show
     HOL.Rat
 begin
 
 definition showsp_unit :: "unit showsp"
   where
     "showsp_unit p x = shows_string ''()''"
 
 lemma show_law_unit [show_law_intros]:
   "show_law showsp_unit x"
   by (rule show_lawI) (simp add: showsp_unit_def show_law_simps)
 
 abbreviation showsp_char :: "char showsp"
   where
     "showsp_char \<equiv> shows_prec"
 
 lemma show_law_char [show_law_intros]:
   "show_law showsp_char x"
   by (rule show_lawI) (simp add: show_law_simps)
 
 primrec showsp_bool :: "bool showsp"
   where
     "showsp_bool p True = shows_string ''True''" |
     "showsp_bool p False = shows_string ''False''"
 
 lemma show_law_bool [show_law_intros]:
   "show_law showsp_bool x"
   by (rule show_lawI, cases x) (simp_all add: show_law_simps)
 
 primrec pshowsp_prod :: "(shows \<times> shows) showsp"
   where
     "pshowsp_prod p (x, y) = shows_string ''('' o x o shows_string '', '' o y o shows_string '')''"
 
 (*NOTE: in order to be compatible with automatically generated show funtions,
 show-arguments of "map"-functions need to get precedence 1 (which may lead to
 redundant parentheses in the output, but seems unavoidable in the current setup,
 i.e., pshowsp via primrec followed by defining showsp via pshowsp composed with map).*)
 definition showsp_prod :: "'a showsp \<Rightarrow> 'b showsp \<Rightarrow> ('a \<times> 'b) showsp"
   where
     [code del]: "showsp_prod s1 s2 p = pshowsp_prod p o map_prod (s1 1) (s2 1)"
 
 lemma showsp_prod_simps [simp, code]:
   "showsp_prod s1 s2 p (x, y) =
     shows_string ''('' o s1 1 x o shows_string '', '' o s2 1 y o shows_string '')''"
   by (simp add: showsp_prod_def)
 
 lemma show_law_prod [show_law_intros]:
   "(\<And>x. x \<in> Basic_BNFs.fsts y \<Longrightarrow> show_law s1 x) \<Longrightarrow>
    (\<And>x. x \<in> Basic_BNFs.snds y \<Longrightarrow> show_law s2 x) \<Longrightarrow>
     show_law (showsp_prod s1 s2) y"
 proof (induct y)
   case (Pair x y)
   note * = Pair [unfolded prod_set_simps]
   show ?case
     by (rule show_lawI)
       (auto simp del: o_apply intro!: o_append intro: show_lawD * simp: show_law_simps)
 qed
 
-fun string_of_digit :: "nat \<Rightarrow> string"
+definition string_of_digit :: "nat \<Rightarrow> string"
   where
     "string_of_digit n =
     (if n = 0 then ''0''
     else if n = 1 then ''1''
     else if n = 2 then ''2''
     else if n = 3 then ''3''
     else if n = 4 then ''4''
     else if n = 5 then ''5''
     else if n = 6 then ''6''
     else if n = 7 then ''7''
     else if n = 8 then ''8''
     else ''9'')"
 
 fun showsp_nat :: "nat showsp"
   where
     "showsp_nat p n =
     (if n < 10 then shows_string (string_of_digit n)
     else showsp_nat p (n div 10) o shows_string (string_of_digit (n mod 10)))"
 declare showsp_nat.simps [simp del]
 
 lemma show_law_nat [show_law_intros]:
   "show_law showsp_nat n"
   by (rule show_lawI, induct n rule: nat_less_induct) (simp add: show_law_simps showsp_nat.simps)
 
 lemma showsp_nat_append [show_law_simps]:
   "showsp_nat p n (x @ y) = showsp_nat p n x @ y"
   by (intro show_lawD show_law_intros)
 
 definition showsp_int :: "int showsp"
   where
     "showsp_int p i =
     (if i < 0 then shows_string ''-'' o showsp_nat p (nat (- i)) else showsp_nat p (nat i))"
 
 lemma show_law_int [show_law_intros]:
   "show_law showsp_int i"
   by (rule show_lawI, cases "i < 0") (simp_all add: showsp_int_def show_law_simps)
 
 lemma showsp_int_append [show_law_simps]:
   "showsp_int p i (x @ y) = showsp_int p i x @ y"
   by (intro show_lawD show_law_intros)
 
 definition showsp_rat :: "rat showsp"
   where
     "showsp_rat p x =
     (case quotient_of x of (d, n) \<Rightarrow>
       if n = 1 then showsp_int p d else showsp_int p d o shows_string ''/'' o showsp_int p n)"
 
 lemma show_law_rat [show_law_intros]:
   "show_law showsp_rat r"
   by (rule show_lawI, cases "quotient_of r") (simp add: showsp_rat_def show_law_simps)
 
 lemma showsp_rat_append [show_law_simps]:
   "showsp_rat p r (x @ y) = showsp_rat p r x @ y"
   by (intro show_lawD show_law_intros)
 
 text \<open>
   Automatic show functions are not used for @{type unit}, @{type prod}, and numbers:
   for @{type unit} and @{type prod}, we do not want to display @{term "''Unity''"} and
   @{term "''Pair''"}; for @{type nat}, we do not want to display
   @{term "''Suc (Suc (... (Suc 0) ...))''"}; and neither @{type int}
   nor @{type rat} are datatypes.
 \<close>
 
 local_setup \<open>
   Show_Generator.register_foreign_partial_and_full_showsp @{type_name prod} 0
        @{term "pshowsp_prod"}
        @{term "showsp_prod"} (SOME @{thm showsp_prod_def})
        @{term "map_prod"} (SOME @{thm prod.map_comp}) [true, true]
        @{thm show_law_prod}
   #> Show_Generator.register_foreign_showsp @{typ unit} @{term "showsp_unit"} @{thm show_law_unit}
   #> Show_Generator.register_foreign_showsp @{typ bool} @{term "showsp_bool"} @{thm show_law_bool}
   #> Show_Generator.register_foreign_showsp @{typ char} @{term "showsp_char"} @{thm show_law_char}
   #> Show_Generator.register_foreign_showsp @{typ nat} @{term "showsp_nat"} @{thm show_law_nat}
   #> Show_Generator.register_foreign_showsp @{typ int} @{term "showsp_int"} @{thm show_law_int}
   #> Show_Generator.register_foreign_showsp @{typ rat} @{term "showsp_rat"} @{thm show_law_rat}
 \<close>
 
 derive "show" option sum prod unit bool nat int rat
 
 export_code
   "shows_prec :: 'a::show option showsp"
   "shows_prec :: ('a::show, 'b::show) sum showsp"
   "shows_prec :: ('a::show \<times> 'b::show) showsp"
   "shows_prec :: unit showsp"
   "shows_prec :: char showsp"
   "shows_prec :: bool showsp"
   "shows_prec :: nat showsp"
   "shows_prec :: int showsp"
   "shows_prec :: rat showsp"
   checking
 
-text \<open>In the sequel we prove injectivity of @{term "show :: nat \<Rightarrow> string"}.\<close>
-
-lemma string_of_digit_inj:
-  assumes "x < y \<and> y < 10"
-  shows "string_of_digit x \<noteq> string_of_digit y"
-  using assms
-  apply (cases "y=1", simp)
-  apply (cases "y=2", simp)
-  apply (cases "y=3", simp)
-  apply (cases "y=4", simp)
-  apply (cases "y=5", simp)
-  apply (cases "y=6", simp)
-  apply (cases "y=7", simp)
-  apply (cases "y=8", simp)
-  apply (cases "y=9", simp)
-  by arith
-
-
-lemma string_of_digit_inj_2:
-  assumes "x < 10"
-  shows "length (string_of_digit x) = 1"
-  using assms
-  apply (cases "x=0", simp)
-  apply (cases "x=1", simp)
-  apply (cases "x=2", simp)
-  apply (cases "x=3", simp)
-  apply (cases "x=4", simp)
-  apply (cases "x=5", simp)
-  apply (cases "x=6", simp)
-  apply (cases "x=7", simp)
-  apply (cases "x=8", simp)
-  apply (cases "x=9", simp)
-  by arith
-
-declare string_of_digit.simps[simp del]
-
-lemma string_of_digit_inj_1:
-  assumes "x < 10" and "y < 10" and "x \<noteq> y"
-  shows "string_of_digit x \<noteq> string_of_digit y"
-proof
-  assume ass: "string_of_digit x = string_of_digit y"
-  with assms have  "\<exists> xx yy :: nat. xx < 10 \<and> yy < 10 \<and> xx < yy \<and> string_of_digit xx = string_of_digit yy" 
-  proof (cases "x < y", blast)
-    case False
-    with \<open>x \<noteq> y\<close> have "y < x" by arith
-    with assms ass have "y < 10 \<and> x < 10 \<and> y < x \<and> string_of_digit y = string_of_digit x" by auto
-    then show ?thesis by blast
-  qed
-  from this obtain xx yy :: nat where cond: "xx < 10 \<and> yy < 10 \<and> xx < yy \<and> string_of_digit xx = string_of_digit yy" by blast
-  then show False using string_of_digit_inj by auto
-qed
-
-lemma shows_prec_nat_simp1:
-  fixes n::nat assumes "\<not> n < 10" shows "shows_prec d n xs = ((shows_prec d (n div 10) \<circ> shows_string (string_of_digit (n mod 10)))) xs"
-  using showsp_nat.simps[of d n]
-  unfolding if_not_P[OF assms] shows_string_def o_def
-  unfolding shows_prec_nat_def by simp
-
-lemma show_nat_simp1: "\<not> (n::nat) < 10 \<Longrightarrow> show n = show (n div 10) @ string_of_digit (n mod 10)"
-  using shows_prec_nat_simp1[of n "0::nat" "[]"] unfolding shows_string_def o_def
-  unfolding shows_prec_append[symmetric] by simp
-
-lemma show_nat_len_1: fixes x :: nat 
-  shows "length (show x) > 0"
-proof (cases "x < 10")
-  assume ass: "\<not> x < 10"
-  then have "show x = show (x div 10) @ string_of_digit (x mod 10)" by (rule show_nat_simp1)
-  then have "length (show x) = length (show (x div 10)) + length (string_of_digit (x mod 10))"
-    unfolding length_append[symmetric] by simp
-  with ass show ?thesis by (simp add: string_of_digit_inj_2)
-next
-  assume "x < 10" then show ?thesis
-    unfolding shows_prec_nat_def
-    unfolding showsp_nat.simps[of 0 x]
-    unfolding shows_string_def by (simp add: string_of_digit_inj_2)
-qed
-
-lemma shows_prec_nat_simp2:
-  fixes n::nat assumes "n < 10" shows "shows_prec d n xs = string_of_digit n @ xs"
-  using showsp_nat.simps[of d n]
-  unfolding shows_prec_nat_def if_P[OF assms] shows_string_def by simp
-
-lemma show_nat_simp2:
-  fixes n::nat assumes "n < 10" shows "show n = string_of_digit n"
-  using shows_prec_nat_simp2[OF assms, of "0::nat" "[]"] by simp
-
-lemma show_nat_len_2:
-  fixes x :: nat 
-  assumes one: "length (show x) = 1" 
-  shows "x < 10"
-proof (rule ccontr)
-  assume ass: "\<not> x < 10"
-  then have "show x = show (x div 10) @ string_of_digit (x mod 10)" by (rule show_nat_simp1)
-  then have "length (show x) = length (show (x div 10)) + length (string_of_digit (x mod 10))"
-    unfolding length_append[symmetric] by simp
-  with one have "length (show (x div 10)) = 0" by (simp add: string_of_digit_inj_2)
-  with show_nat_len_1 show False by best
-qed
-
-lemma show_nat_len_3:
-  fixes x :: nat 
-  assumes one: "length (show x) > 1"
-  shows "\<not> x < 10"
-proof 
-  assume ass: "x < 10"
-  then have "show x = string_of_digit x" by (rule show_nat_simp2)
-  with string_of_digit_inj_2 ass have "length (show x) = 1" by simp
-  with one show False by arith
-qed
-
-lemma inj_show_nat: "inj (show::nat \<Rightarrow> string)"
-  unfolding inj_on_def
-proof (clarify)
-  fix x y :: nat assume "show x = show y"
-  then obtain n where "length (show x) = n \<and> show x = show y" by blast
-  then show "x = y" 
-  proof (induct n arbitrary: x y)
-    case 0
-    fix x y :: nat
-    assume ass: "length (show x) = 0 \<and> show x = show y"
-    then show ?case using show_nat_len_1 by best
-  next
-    case (Suc n)
-    then have eq: "show x = show y" by blast
-    from Suc have len: "length (show x) = Suc n" by blast
-    show ?case
-    proof (cases n)
-      case 0
-      with Suc have one: "length(show x) = 1 \<and> length (show y) = 1" by (auto)
-      with show_nat_len_2 have ten: "x < 10 \<and> y < 10" by simp
-      show ?thesis 
-      proof (cases "x = y", simp)
-        case False
-        with ten string_of_digit_inj_1 have "string_of_digit x \<noteq> string_of_digit y" by auto
-        with ten eq show ?thesis using show_nat_simp2[of x] show_nat_simp2[of y] by simp
-      qed
-    next
-      case (Suc m)
-      with len eq have "length (show x) = Suc (Suc m) \<and> length (show y) = Suc (Suc m)" by auto
-      then have "length (show x) > 1 \<and> length (show y) > 1" by simp
-      then have large: "\<not> x < 10 \<and> \<not> y < 10" using show_nat_len_3 by simp
-      let ?e = "\<lambda>x::nat. show (x div 10) @ string_of_digit (x mod 10)"
-      from large have id: "show x = ?e x \<and> show y = ?e y"
-        using show_nat_simp1[of x] show_nat_simp1[of y] by auto
-      from string_of_digit_inj_2 have one: "length (string_of_digit(x mod 10)) = 1
-        \<and> length(string_of_digit(y mod 10)) = 1" by auto
-      from one have "\<exists>xx. string_of_digit(x mod 10) = [xx]"
-        by (cases "string_of_digit (x mod 10)",simp,cases "tl (string_of_digit (x mod 10))",simp,simp)
-      from this obtain xx where xx: "string_of_digit(x mod 10) = [xx]" ..
-      from one have "\<exists>xx. string_of_digit(y mod 10) = [xx]"
-        by (cases "string_of_digit (y mod 10)",simp,cases "tl (string_of_digit (y mod 10))",simp,simp)
-      from this obtain yy where yy: "string_of_digit(y mod 10) = [yy]" ..
-      from id have "length (show x) = length (show (x div 10)) + length (string_of_digit (x mod 10))" unfolding length_append[symmetric] by simp
-      with one len have shorter: "length (show (x div 10)) = n" by simp
-      from eq id xx yy
-      have "(show (x div 10) @ [xx]) = (show (y div 10) @ [yy])" by simp
-      then have "(show (x div 10) = show(y div 10)) \<and> xx = yy" by clarify
-      then have nearly: "show (x div 10) = show (y div 10)
-        \<and> string_of_digit(x mod 10) = string_of_digit(y mod 10)" using xx yy by simp
-      with shorter and
-        \<open>length (show (x div 10)) = n \<and> show (x div 10) = show (y div 10) \<Longrightarrow> x div 10 = y div 10\<close>
-      have div: "x div 10 = y div 10" by blast
-      from nearly string_of_digit_inj_1 have mod:  "x mod 10 = y mod 10"
-        by (cases "x mod 10 = y mod 10", simp, simp)
-      have "x = 10 * (x div 10) + (x mod 10)" by auto
-      also have "\<dots> = 10 * (y div 10) + (y mod 10)" using div mod by auto
-      also have "\<dots> = y" by auto
-      finally show ?thesis .
-    qed
-  qed
-qed
-
 end