diff --git a/thys/CakeML/generated/LemExtraDefs.thy b/thys/CakeML/generated/LemExtraDefs.thy
--- a/thys/CakeML/generated/LemExtraDefs.thy
+++ b/thys/CakeML/generated/LemExtraDefs.thy
@@ -1,1255 +1,1257 @@
 (*========================================================================*)
 (*                        Lem                                             *)
 (*                                                                        *)
 (*          Dominic Mulligan, University of Cambridge                     *)
 (*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
 (*          Gabriel Kerneis, University of Cambridge                      *)
 (*          Kathy Gray, University of Cambridge                           *)
 (*          Peter Boehm, University of Cambridge (while working on Lem)   *)
 (*          Peter Sewell, University of Cambridge                         *)
 (*          Scott Owens, University of Kent                               *)
 (*          Thomas Tuerk, University of Cambridge                         *)
 (*          Brian Campbell, University of Edinburgh                       *)
 (*          Shaked Flur, University of Cambridge                          *)
 (*          Thomas Bauereiss, University of Cambridge                     *)
 (*          Stephen Kell, University of Cambridge                         *)
 (*          Thomas Williams                                               *)
 (*          Lars Hupel                                                    *)
 (*          Basile Clement                                                *)
 (*                                                                        *)
 (*  The Lem sources are copyright 2010-2018                               *)
 (*  by the authors above and Institut National de Recherche en            *)
 (*  Informatique et en Automatique (INRIA).                               *)
 (*                                                                        *)
 (*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
 (*  are distributed under the license below.  The former are distributed  *)
 (*  under the LGPLv2, as in the LICENSE file.                             *)
 (*                                                                        *)
 (*                                                                        *)
 (*  Redistribution and use in source and binary forms, with or without    *)
 (*  modification, are permitted provided that the following conditions    *)
 (*  are met:                                                              *)
 (*  1. Redistributions of source code must retain the above copyright     *)
 (*  notice, this list of conditions and the following disclaimer.         *)
 (*  2. Redistributions in binary form must reproduce the above copyright  *)
 (*  notice, this list of conditions and the following disclaimer in the   *)
 (*  documentation and/or other materials provided with the distribution.  *)
 (*  3. The names of the authors may not be used to endorse or promote     *)
 (*  products derived from this software without specific prior written    *)
 (*  permission.                                                           *)
 (*                                                                        *)
 (*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
 (*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
 (*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
 (*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
 (*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
 (*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
 (*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
 (*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  *)
 (*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
 (*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (*========================================================================*)
 
 chapter \<open>Auxiliary Definitions needed by Lem\<close>
 
 theory "LemExtraDefs"
 
 imports
-   Main
-   "HOL-Library.List_Permutation"
-   "HOL-Library.While_Combinator"
+  Main
+  "HOL-Library.While_Combinator"
+  "HOL-Library.List_Permutation"
 begin
 
+hide_const (open) sign
+
 subsection \<open>General\<close>
 
 consts failwith :: " 'a \<Rightarrow> 'b"
 
 subsection \<open>Lists\<close>
 
 fun index :: " 'a list \<Rightarrow> nat \<Rightarrow> 'a option "  where
    "index [] n = None"
  | "index (x # xs) 0 = Some x"
  | "index (x # xs) (Suc n) = index xs n"
 
 lemma index_eq_some [simp]:
    "index l n = Some x \<longleftrightarrow> (n < length l \<and> (x = l ! n))"
 proof (induct l arbitrary: n x)
   case Nil thus ?case by simp
 next
   case (Cons e es n x)
   note ind_hyp = this
 
   show ?case
   proof (cases n)
     case 0 thus ?thesis by auto
   next
     case (Suc n')
     with ind_hyp show ?thesis by simp
   qed
 qed
 
 lemma index_eq_none [simp]:
    "index l n = None \<longleftrightarrow> length l \<le> n"
 by (rule iffD1[OF Not_eq_iff]) auto
 
 
 lemma index_simps [simp]:
    "length l \<le> n \<Longrightarrow> index l n = None"
    "n < length l \<Longrightarrow> index l n = Some (l ! n)"
 by (simp_all)
 
 fun find_indices :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat list" where
    "find_indices P [] = []"
  | "find_indices P (x # xs) = (if P x then 0 # (map Suc (find_indices P xs)) else (map Suc (find_indices P xs)))"
 
 lemma length_find_indices :
   "length (find_indices P l) \<le> length l"
 by (induct l) auto
 
 lemma sorted_map_suc :
   "sorted l \<Longrightarrow> sorted (map Suc l)"
 by (induct l) (simp_all)
 
 lemma sorted_find_indices :
   "sorted (find_indices P xs)"
 proof (induct xs)
   case Nil thus ?case by simp
 next
   case (Cons x xs)
   from sorted_map_suc[OF this]
   show ?case
     by (simp)
 qed
 
 lemma find_indices_set [simp] :
   "set (find_indices P l) = {i. i < length l \<and> P (l ! i)}"
 proof (intro set_eqI)
   fix i
   show "i \<in> set (find_indices P l) \<longleftrightarrow> (i \<in> {i. i < length l \<and> P (l ! i)})"
   proof (induct l arbitrary: i)
     case Nil thus ?case by simp
   next
     case (Cons x l' i)
     note ind_hyp = this
     show ?case
     proof (cases i)
       case 0 thus ?thesis by auto
     next
       case (Suc i') with ind_hyp[of i'] show ?thesis by auto
     qed
   qed
 qed
 
 definition find_index where
   "find_index P xs = (case find_indices P xs of
       []    \<Rightarrow> None
     | i # _ \<Rightarrow> Some i)"
 
 lemma find_index_eq_some [simp] :
   "(find_index P xs = Some ii) \<longleftrightarrow> (ii < length xs \<and> P (xs ! ii) \<and> (\<forall>i' < ii. \<not>(P (xs ! i'))))"
   (is "?lhs = ?rhs")
 proof (cases "find_indices P xs")
   case Nil
   with find_indices_set[of P xs]
   show ?thesis
     unfolding find_index_def by auto
 next
   case (Cons i il) note find_indices_eq = this
 
   from sorted_find_indices[of P xs] find_indices_eq
   have "sorted (i # il)" by simp
   hence i_leq: "\<And>i'. i' \<in> set (i # il) \<Longrightarrow> i \<le> i'" by auto
 
   from find_indices_set[of P xs, unfolded find_indices_eq]
   have set_i_il_eq:"\<And>i'. i' \<in> set (i # il) = (i' < length xs \<and> P (xs ! i'))"
     by simp
 
   have lhs_eq: "find_index P xs = Some i"
     unfolding find_index_def find_indices_eq by simp
 
   show ?thesis
   proof (intro iffI)
     assume ?lhs
     with lhs_eq have ii_eq[simp]: "ii = i" by simp
 
     from set_i_il_eq[of i] i_leq[unfolded set_i_il_eq]
     show ?rhs by auto (metis leD less_trans)
   next
     assume ?rhs
     with set_i_il_eq[of ii]
     have "ii \<in> set (i # il) \<and> (ii \<le> i)"
       by (metis leI length_pos_if_in_set nth_Cons_0 nth_mem set_i_il_eq)
 
     with i_leq [of ii] have "i = ii" by simp
     thus ?lhs unfolding lhs_eq by simp
   qed
 qed
 
 lemma find_index_eq_none [simp] :
   "(find_index P xs = None) \<longleftrightarrow> (\<forall>x \<in> set xs. \<not>(P x))" (is "?lhs = ?rhs")
 proof (rule iffD1[OF Not_eq_iff], intro iffI)
   assume "\<not> ?lhs"
   then obtain i where "find_index P xs = Some i" by auto
   hence "i < length xs \<and> P (xs ! i)" by simp
   thus "\<not> ?rhs" by auto
 next
   let ?p = "(\<lambda>i. i < length xs \<and> P(xs ! i))"
 
   assume "\<not> ?rhs"
   then obtain i where "?p i"
     by (metis in_set_conv_nth)
 
   from LeastI [of ?p, OF \<open>?p i\<close>]
   have "?p (Least ?p)" .
 
   hence "find_index P xs = Some (Least ?p)"
     by (subst find_index_eq_some) (metis (mono_tags) less_trans not_less_Least)
 
   thus "\<not> ?lhs" by blast
 qed
 
 definition genlist where
   "genlist f n = map f (upt 0 n)"
 
 lemma genlist_length [simp] :
   "length (genlist f n) = n"
 unfolding genlist_def by simp
 
 lemma genlist_simps [simp]:
    "genlist f 0 = []"
    "genlist f (Suc n) = genlist f n @ [f n]"
 unfolding genlist_def by auto
 
 definition split_at where
   "split_at n l = (take n l, drop n l)"
 
 fun delete_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list) option "  where
     "delete_first P [] = None"
   | "delete_first P (x # xs) =
      (if (P x) then Some xs else
       map_option (\<lambda>xs'. x # xs') (delete_first P xs))"
 declare delete_first.simps [simp del]
 
 lemma delete_first_simps [simp] :
    "delete_first P [] = None"
    "P x \<Longrightarrow> delete_first P (x # xs) = Some xs"
    "\<not>(P x) \<Longrightarrow> delete_first P (x # xs) = map_option (\<lambda>xs'. x # xs') (delete_first P xs)"
 unfolding delete_first.simps by auto
 
 lemmas delete_first_unroll = delete_first.simps(2)
 
 
 lemma delete_first_eq_none [simp] :
   "delete_first P l = None \<longleftrightarrow> (\<forall>x \<in> set l. \<not> (P x))"
 by (induct l) (auto simp add: delete_first_unroll)
 
 lemma delete_first_eq_some :
   "delete_first P l = (Some l') \<longleftrightarrow> (\<exists>l1 x l2. P x \<and> (\<forall>x \<in> set l1. \<not>(P x)) \<and> (l = l1 @ (x # l2)) \<and> (l' = l1 @ l2))"
   (is "?lhs l l' = (\<exists>l1 x l2. ?rhs_body l1 x l2 l l')")
 proof (induct l arbitrary: l')
   case Nil thus ?case by simp
 next
   case (Cons e l l')
   note ind_hyp = this
 
   show ?case
   proof (cases "P e")
     case True
     show ?thesis
     proof (rule iffI)
       assume "?lhs (e # l) l'"
       with \<open>P e\<close> have "l = l'" by simp
       with \<open>P e\<close> have "?rhs_body [] e l' (e # l) l'" by simp
       thus "\<exists>l1 x l2. ?rhs_body l1 x l2 (e # l) l'" by blast
     next
       assume "\<exists>l1 x l2. ?rhs_body l1 x l2 (e # l) l'"
       then obtain l1 x l2 where body_ok: "?rhs_body l1 x l2 (e # l) l'" by blast
 
       from body_ok \<open>P e\<close> have l1_eq[simp]: "l = l'"
         by (cases l1) (simp_all)
       with \<open>P e\<close> show "?lhs (e # l) l'" by simp
     qed
   next
     case False
     define rhs_pred where "rhs_pred \<equiv> \<lambda>l1 x l2 l l'. ?rhs_body l1 x l2 l l'"
     have rhs_fold: "\<And>l1 x l2 l l'. ?rhs_body l1 x l2 l l' = rhs_pred l1 x l2 l l'"
        unfolding rhs_pred_def by simp
 
     have "(\<exists>z l1 x l2. rhs_pred l1 x l2 l z \<and> e # z = l') = (\<exists>l1 x l2. rhs_pred l1 x l2 (e # l) l')"
     proof (intro iffI)
       assume "\<exists>z l1 x l2. rhs_pred l1 x l2 l z \<and> e # z = l'"
       then obtain z l1 x l2 where "rhs_pred l1 x l2 l z" and l'_eq: "l' = e # z" by auto
       with \<open>\<not>(P e)\<close> have "rhs_pred (e # l1) x l2 (e # l) l'"
         unfolding rhs_pred_def by simp
       thus "\<exists>l1 x l2. rhs_pred l1 x l2 (e # l) l'" by blast
     next
       assume "\<exists>l1 x l2. rhs_pred l1 x l2 (e # l) l'"
       then obtain l1 x l2 where "rhs_pred l1 x l2 (e # l) l'" by blast
       with \<open>\<not> (P e)\<close> obtain l1' where l1_eq[simp]: "l1 = e # l1'"
         unfolding rhs_pred_def by (cases l1) (auto)
 
       with \<open>rhs_pred l1 x l2 (e # l) l'\<close>
       have "rhs_pred l1' x l2 l (l1' @ l2) \<and> e # (l1' @ l2) = l'"
         unfolding rhs_pred_def by (simp)
       thus "\<exists>z l1 x l2. rhs_pred l1 x l2 l z \<and> e # z = l'" by blast
     qed
     with \<open>\<not> P e\<close> show ?thesis
       unfolding rhs_fold
       by (simp add: ind_hyp[unfolded rhs_fold])
   qed
 qed
 
 
 lemma perm_eval [code] :
   "perm [] l \<longleftrightarrow> l = []" (is ?g1)
   "perm (x # xs) l \<longleftrightarrow> (case delete_first (\<lambda>e. e = x) l of
        None => False
      | Some l' => perm xs l')" (is ?g2)
 proof -
   show ?g1 by auto
 next
   show ?g2
   proof (cases "delete_first (\<lambda>e. e = x) l")
     case None note del_eq = this
     hence "x \<notin> set l" by auto
     with perm_set_eq [of "x # xs" l]
     have "\<not> perm (x # xs) l" by auto
     thus ?thesis unfolding del_eq by simp
   next
     case (Some l') note del_eq = this
 
     from del_eq[unfolded delete_first_eq_some]
     obtain l1 l2 where l_eq: "l = l1 @ [x] @ l2" and l'_eq: "l' = l1 @ l2" by auto
 
     have "(x # xs <~~> l1 @ x # l2) = (xs <~~> l1 @ l2)"
     proof -
       from perm_append_swap [of l1 "[x]"]
            perm_append2 [of "l1 @ [x]" "x # l1" l2]
       have "l1 @ x # l2 <~~> x # (l1 @ l2)" by simp
       hence "x # xs <~~> l1 @ x # l2 \<longleftrightarrow> x # xs <~~> x # (l1 @ l2)"
         by (metis perm.trans perm_sym)
       thus ?thesis by simp
     qed
     with del_eq l_eq l'_eq show ?thesis by simp
   qed
 qed
 
 
 fun sorted_by  :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> bool "  where
    "sorted_by cmp [] = True"
  | "sorted_by cmp [_] = True"
  | "sorted_by cmp (x1 # x2 # xs) = ((cmp x1 x2) \<and> sorted_by cmp (x2 # xs))"
 
 lemma sorted_by_lesseq [simp] :
   "sorted_by ((\<le>) :: ('a::{linorder}) => 'a => bool) = sorted"
 proof (rule ext)
   fix l :: "'a list"
   show "sorted_by (\<le>) l = sorted l"
   proof (induct l)
     case Nil thus ?case by simp
   next
     case (Cons x xs)
     thus ?case by (cases xs) (simp_all del: sorted.simps(2) add: sorted2_simps)
   qed
 qed
 
 lemma sorted_by_cons_imp :
   "sorted_by cmp (x # xs) \<Longrightarrow> sorted_by cmp xs"
 by (cases xs) simp_all
 
 lemma sorted_by_cons_trans :
   assumes trans_cmp: "transp cmp"
   shows "sorted_by cmp (x # xs) = ((\<forall>x' \<in> set xs . cmp x x') \<and> sorted_by cmp xs)"
 proof (induct xs arbitrary: x)
   case Nil thus ?case by simp
 next
   case (Cons x2 xs x1)
   note ind_hyp = this
 
   from trans_cmp
   show ?case
     by (auto simp add: ind_hyp transp_def)
 qed
 
 
 fun insert_sort_insert_by  :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list "  where
   "insert_sort_insert_by cmp e ([]) = ( [e])"
 | "insert_sort_insert_by cmp e (x # xs) = ( if cmp e x then (e # (x # xs)) else x # (insert_sort_insert_by cmp e xs))"
 
 
 lemma insert_sort_insert_by_length [simp] :
   "length (insert_sort_insert_by cmp e l) = Suc (length l)"
 by (induct l) auto
 
 lemma insert_sort_insert_by_set [simp] :
   "set (insert_sort_insert_by cmp e l) = insert e (set l)"
 by (induct l) auto
 
 lemma insert_sort_insert_by_perm :
   "(insert_sort_insert_by cmp e l) <~~> (e # l)"
 proof (induct l)
   case Nil thus ?case by simp
 next
   case (Cons e2 l')
   note ind_hyp = this
 
   have "e2 # e # l' <~~> e # e2 # l'" by (rule perm.swap)
   hence "e2 # insert_sort_insert_by cmp e l' <~~> e # e2 # l'"
     using ind_hyp by (metis cons_perm_eq perm.trans)
   thus ?case by simp
 qed
 
 
 lemma insert_sort_insert_by_sorted_by :
 assumes cmp_cases: "\<And>y. y \<in> set l \<Longrightarrow> \<not> (cmp e y) \<Longrightarrow> cmp y e"
 assumes cmp_trans: "transp cmp"
 shows "sorted_by cmp l \<Longrightarrow> sorted_by cmp (insert_sort_insert_by cmp e l)"
 using cmp_cases
 proof (induct l)
   case Nil thus ?case by simp
 next
   case (Cons x1 l')
   note ind_hyp = Cons(1)
   note sorted_x1_l' = Cons(2)
   note cmp_cases = Cons(3)
 
   show ?case
   proof (cases l')
     case Nil with cmp_cases show ?thesis by simp
   next
     case (Cons x2 l'') note l'_eq = this
 
     from l'_eq sorted_x1_l' have "cmp x1 x2" "sorted_by cmp l'" by simp_all
 
     show ?thesis
     proof (cases "cmp e x1")
       case True
       with \<open>cmp x1 x2\<close> \<open>sorted_by cmp l'\<close>
       have "sorted_by cmp (x1 # l')"
         unfolding l'_eq by (simp)
       with \<open>cmp e x1\<close>
       show ?thesis by simp
     next
       case False
 
       with cmp_cases have "cmp x1 e" by simp
       have "\<And>x'.  x' \<in> set l' \<Longrightarrow> cmp x1 x'"
       proof -
         fix x'
         assume "x' \<in> set l'"
         hence "x' = x2 \<or> cmp x2 x'"
           using \<open>sorted_by cmp l'\<close> l'_eq sorted_by_cons_trans [OF cmp_trans, of x2 l'']
           by auto
         with transpD[OF cmp_trans, of x1 x2 x'] \<open>cmp x1 x2\<close>
         show "cmp x1 x'" by blast
       qed
       hence "sorted_by cmp (x1 # insert_sort_insert_by cmp e l')"
         using ind_hyp [OF \<open>sorted_by cmp l'\<close>] \<open>cmp x1 e\<close> cmp_cases
         unfolding sorted_by_cons_trans[OF cmp_trans]
         by simp
       with \<open>\<not>(cmp e x1)\<close>
       show ?thesis by simp
     qed
   qed
 qed
 
 
 
 fun insert_sort_by :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list "  where
     "insert_sort_by cmp [] = []"
   | "insert_sort_by cmp (x # xs) = insert_sort_insert_by cmp x (insert_sort_by cmp xs)"
 
 
 lemma insert_sort_by_perm :
   "(insert_sort_by cmp l) <~~> l"
 proof (induct l)
   case Nil thus ?case by simp
 next
   case (Cons x l)
   thus ?case
    by simp (metis cons_perm_eq insert_sort_insert_by_perm perm.trans)
 qed
 
 lemma insert_sort_by_length [simp]:
   "length (insert_sort_by cmp l) = length l"
 by (induct l) auto
 
 lemma insert_sort_by_set [simp]:
   "set (insert_sort_by cmp l) = set l"
 by (induct l) auto
 
 definition sort_by where
   "sort_by = insert_sort_by"
 
 lemma sort_by_simps [simp]:
   "length (sort_by cmp l) = length l"
   "set (sort_by cmp l) = set l"
 unfolding sort_by_def by simp_all
 
 lemma sort_by_perm :
   "sort_by cmp l <~~> l"
 unfolding sort_by_def
 by (simp add: insert_sort_by_perm)
 
 subsection \<open>Maps\<close>
 
 definition map_image :: "('v \<Rightarrow> 'w) \<Rightarrow> ('k, 'v) map \<Rightarrow> ('k, 'w) map" where
   "map_image f m = (\<lambda>k. map_option f (m k))"
 
 definition map_domain_image :: "('k \<Rightarrow> 'v \<Rightarrow> 'w) \<Rightarrow> ('k, 'v) map \<Rightarrow> ('k, 'w) map" where
   "map_domain_image f m = (\<lambda>k. map_option (f k) (m k))"
 
 
 lemma map_image_simps [simp]:
   "(map_image f m) k = None \<longleftrightarrow> m k = None"
   "(map_image f m) k = Some x \<longleftrightarrow> (\<exists>x'. (m k = Some x') \<and> (x = f x'))"
   "(map_image f Map.empty) = Map.empty"
   "(map_image f (m (k \<mapsto> v)) = (map_image f m) (k \<mapsto> f v))"
 unfolding map_image_def by auto
 
 lemma map_image_dom_ran [simp]:
   "dom (map_image f m) = dom m"
   "ran (map_image f m) = f ` (ran m)"
 unfolding dom_def ran_def by auto
 
 definition map_to_set :: "('k, 'v) map \<Rightarrow> ('k * 'v) set" where
   "map_to_set m = { (k, v) . m k = Some v }"
 
 lemma map_to_set_simps [simp] :
   "map_to_set Map.empty = {}"  (is ?g1)
   "map_to_set (m ((k::'k) \<mapsto> (v::'v))) = (insert (k, v) (map_to_set (m |` (- {k}))))" (is ?g2)
 proof -
   show ?g1 unfolding map_to_set_def by simp
 next
   show ?g2
   proof (rule set_eqI)
     fix kv :: "('k * 'v)"
     obtain k' v' where kv_eq[simp]: "kv = (k', v')" by (rule prod.exhaust)
 
     show "(kv \<in> map_to_set (m(k \<mapsto> v))) = (kv \<in> insert (k, v) (map_to_set (m |` (- {k}))))"
       by (auto simp add: map_to_set_def)
   qed
 qed
 
 
 subsection \<open>Sets\<close>
 
 definition "set_choose s \<equiv> (SOME x. (x \<in> s))"
   
 definition without_trans_edges :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
   "without_trans_edges S \<equiv>
      let ts = trancl S in
        { (x, y) \<in> S. \<forall>z \<in> snd ` S. x \<noteq> z \<and> y \<noteq> z \<longrightarrow> \<not> ((x, z) \<in> ts \<and> (z, y) \<in> ts)}"
   
 definition unbounded_lfp :: "'a set \<Rightarrow> ('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set" where
   "unbounded_lfp S f \<equiv>
      while (\<lambda>x. x \<subset> S) f S"
   
 definition unbounded_gfp :: "'a set \<Rightarrow> ('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set" where
   "unbounded_gfp S f \<equiv>
      while (\<lambda>x. S \<subset> x) f S"
 
 lemma set_choose_thm[simp]:
   "s \<noteq> {} \<Longrightarrow> (set_choose s) \<in> s"
 unfolding set_choose_def
 by (rule someI_ex) auto
 
 lemma set_choose_sing [simp]:
   "set_choose {x} = x"
   unfolding set_choose_def
   by auto
 
 lemma set_choose_code [code]:
   "set_choose (set [x]) = x"
 by auto
 
 lemma set_choose_in [intro] :
   assumes "s \<noteq> {}"
   shows "set_choose s \<in> s"
 proof -
   from \<open>s \<noteq> {}\<close>
   obtain x where "x \<in> s" by auto
   thus ?thesis
     unfolding set_choose_def
     by (rule someI)
 qed
 
 
 definition set_case where
   "set_case s c_empty c_sing c_else =
     (if (s = {}) then c_empty else
     (if (card s = 1) then c_sing (set_choose s) else
        c_else))"
 
 lemma set_case_simps [simp] :
   "set_case {} c_empty c_sing c_else = c_empty"
   "set_case {x} c_empty c_sing c_else = c_sing x"
   "card s > 1 \<Longrightarrow> set_case s c_empty c_sing c_else = c_else"
   "\<not>(finite s) \<Longrightarrow> set_case s c_empty c_sing c_else = c_else"
 unfolding set_case_def by auto
 
 lemma set_case_simp_insert2 [simp] :
 assumes x12_neq: "x1 \<noteq> x2"
 shows "set_case (insert x1 (insert x2 xs))  c_empty c_sing c_else = c_else"
 proof (cases "finite xs")
   case False thus ?thesis by (simp)
 next
   case True note fin_xs = this
 
   have "card {x1,x2} \<le> card (insert x1 (insert x2 xs))"
     by (rule card_mono) (auto simp add: fin_xs)
   with x12_neq have "1 < card (insert x1 (insert x2 xs))" by simp
   thus ?thesis by auto
 qed
 
 lemma set_case_code [code] :
   "set_case (set []) c_empty c_sing c_else = c_empty"
   "set_case (set [x]) c_empty c_sing c_else = c_sing x"
   "set_case (set (x1 # x2 # xs)) c_empty c_sing c_else =
    (if (x1 = x2) then
      set_case (set (x2 # xs)) c_empty c_sing c_else
    else
      c_else)"
 by auto
 
 definition set_lfp:: "'a set \<Rightarrow> ('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set" where
   "set_lfp s f = lfp (\<lambda>s'. f s' \<union> s)"
 
 lemma set_lfp_tail_rec_def :
 assumes mono_f: "mono f"
 shows "set_lfp s f = (if (f s) \<subseteq> s then s else (set_lfp (s \<union> f s) f))" (is "?ls = ?rs")
 proof (cases "f s \<subseteq> s")
   case True note fs_sub_s = this
 
   from fs_sub_s have "\<Inter>{u. f u \<union> s \<subseteq> u} = s" by auto
   hence "?ls = s" unfolding set_lfp_def lfp_def .
   with fs_sub_s show "?ls = ?rs" by simp
 next
   case False note not_fs_sub_s = this
 
   from mono_f have mono_f': "mono (\<lambda>s'. f s' \<union> s)"
     unfolding mono_def by auto
 
   have "\<Inter>{u. f u \<union> s \<subseteq> u} = \<Inter>{u. f u \<union> (s \<union> f s) \<subseteq> u}" (is "\<Inter>?S1 = \<Inter>?S2")
   proof
     have "?S2 \<subseteq> ?S1" by auto
     thus "\<Inter>?S1 \<subseteq> \<Inter>?S2" by (rule Inf_superset_mono)
   next
     { fix e
       assume "e \<in> \<Inter>?S2"
       hence S2_prop: "\<And>s'. f s' \<subseteq> s' \<Longrightarrow> s \<subseteq> s' \<Longrightarrow> f s \<subseteq> s' \<Longrightarrow> e \<in> s'" by simp
 
       { fix s'
         assume "f s' \<subseteq> s'" "s \<subseteq> s'"
 
         from mono_f \<open>s \<subseteq> s'\<close>
         have "f s \<subseteq> f s'" unfolding mono_def by simp
         with \<open>f s' \<subseteq> s'\<close> have "f s \<subseteq> s'" by simp
         with \<open>f s' \<subseteq> s'\<close> \<open>s \<subseteq> s'\<close> S2_prop
         have "e \<in> s'" by simp
       }
       hence "e \<in> \<Inter>?S1" by simp
     }
     thus "\<Inter>?S2 \<subseteq> \<Inter>?S1" by auto
   qed
   hence "?ls = (set_lfp (s \<union> f s) f)"
      unfolding set_lfp_def lfp_def .
   with not_fs_sub_s show "?ls = ?rs" by simp
 qed
 
 lemma set_lfp_simps [simp] :
 "mono f \<Longrightarrow> f s \<subseteq> s \<Longrightarrow> set_lfp s f = s"
 "mono f \<Longrightarrow> \<not>(f s \<subseteq> s) \<Longrightarrow> set_lfp s f = (set_lfp (s \<union> f s) f)"
 by (metis set_lfp_tail_rec_def)+
 
 
 fun insert_in_list_at_arbitrary_pos where
    "insert_in_list_at_arbitrary_pos x [] = {[x]}"
  | "insert_in_list_at_arbitrary_pos x (y # ys) =
     insert (x # y # ys) ((\<lambda>l. y # l) ` (insert_in_list_at_arbitrary_pos x ys))"
 
 lemma insert_in_list_at_arbitrary_pos_thm :
   "xl \<in> insert_in_list_at_arbitrary_pos x l \<longleftrightarrow>
    (\<exists>l1 l2. l = l1 @ l2 \<and> xl = l1 @ [x] @ l2)"
 proof (induct l arbitrary: xl)
   case Nil thus ?case by simp
 next
   case (Cons y l xyl)
   note ind_hyp = this
 
   show ?case
   proof (rule iffI)
     assume xyl_in: "xyl \<in> insert_in_list_at_arbitrary_pos x (y # l)"
     show "\<exists>l1 l2. y # l = l1 @ l2 \<and> xyl = l1 @ [x] @ l2"
     proof (cases "xyl = x # y # l")
       case True
       hence "y # l = [] @ (y # l) \<and> xyl = [] @ [x] @ (y # l)" by simp
       thus ?thesis by blast
     next
       case False
       with xyl_in have "xyl \<in> (#) y ` insert_in_list_at_arbitrary_pos x l" by simp
       with ind_hyp obtain l1 l2 where "l = l1 @ l2 \<and> xyl = y # l1 @ x # l2"
          by (auto simp add: image_def Bex_def)
       hence "y # l = (y # l1) @ l2 \<and> xyl = (y # l1) @ [x] @ l2" by simp
       thus ?thesis by blast
     qed
   next
     assume "\<exists>l1 l2. y # l = l1 @ l2 \<and> xyl = l1 @ [x] @ l2"
     then obtain l1 l2 where yl_eq: "y # l = l1 @ l2" and xyl_eq: "xyl = l1 @ [x] @ l2" by blast
     show "xyl \<in> insert_in_list_at_arbitrary_pos x (y # l)"
     proof (cases l1)
       case Nil
       with yl_eq xyl_eq
       have "xyl = x # y # l" by simp
       thus ?thesis by simp
     next
       case (Cons y' l1')
       with yl_eq have l1_eq: "l1 = y # l1'" and l_eq: "l = l1' @ l2" by simp_all
 
       have "\<exists>l1'' l2''. l = l1'' @ l2'' \<and> l1' @ [x] @ l2 = l1'' @ [x] @ l2''"
         apply (rule_tac exI[where x = l1'])
         apply (rule_tac exI [where x = l2])
         apply (simp add: l_eq)
       done
       hence "(l1' @ [x] @ l2) \<in> insert_in_list_at_arbitrary_pos x l"
         unfolding ind_hyp by blast
       hence "\<exists>l'. l' \<in> insert_in_list_at_arbitrary_pos x l \<and> l1 @ x # l2 = y # l'"
         by (rule_tac exI [where x = "l1' @ [x] @ l2"]) (simp add: l1_eq)
       thus ?thesis
         by (simp add: image_def Bex_def xyl_eq)
     qed
   qed
 qed
 
 definition list_of_set_set :: "'a set \<Rightarrow> ('a list) set" where
 "list_of_set_set s = { l . (set l = s) \<and> distinct l }"
 
 lemma list_of_set_set_empty [simp]:
   "list_of_set_set {} = {[]}"
 unfolding list_of_set_set_def by auto
 
 lemma list_of_set_set_insert [simp] :
   "list_of_set_set (insert x s) =
      \<Union> ((insert_in_list_at_arbitrary_pos x) ` (list_of_set_set (s - {x})))"
    (is "?lhs = ?rhs")
 proof (intro set_eqI)
   fix l
 
   have "(set l = insert x s \<and> distinct l) \<longleftrightarrow> (\<exists>l1 l2. set (l1 @ l2) = s - {x} \<and> distinct (l1 @ l2) \<and> l = l1 @ x # l2)"
   proof (intro iffI)
     assume "set l = insert x s \<and> distinct l"
     hence set_l_eq: "set l = insert x s" and "distinct l" by simp_all
 
     from \<open>set l = insert x s\<close>
     have "x \<in> set l" by simp
     then obtain l1 l2 where l_eq: "l = l1 @ x # l2"
       unfolding in_set_conv_decomp by blast
 
     from \<open>distinct l\<close>  l_eq
     have "distinct (l1 @ l2)" and x_nin: "x \<notin> set (l1 @ l2)"
       by auto
 
     from x_nin set_l_eq[unfolded l_eq]
     have set_l12_eq: "set (l1 @ l2) = s - {x}"
       by auto
 
     from \<open>distinct (l1 @ l2)\<close> l_eq set_l12_eq
     show "\<exists>l1 l2. set (l1 @ l2) = s - {x} \<and> distinct (l1 @ l2) \<and> l = l1 @ x # l2"
       by blast
   next
     assume "\<exists>l1 l2. set (l1 @ l2) = s - {x} \<and> distinct (l1 @ l2) \<and> l = l1 @ x # l2"
     then obtain l1 l2 where "set (l1 @ l2) = s - {x}"  "distinct (l1 @ l2)" "l = l1 @ x # l2"
       by blast
     thus "set l = insert x s \<and> distinct l"
        by auto
   qed
 
   thus "l \<in> list_of_set_set (insert x s) \<longleftrightarrow> l \<in> (\<Union> ((insert_in_list_at_arbitrary_pos x) ` (list_of_set_set (s - {x}))))"
      unfolding list_of_set_set_def
      by (simp add: insert_in_list_at_arbitrary_pos_thm ex_simps[symmetric] del: ex_simps)
 qed
 
 lemma list_of_set_set_code [code]:
   "list_of_set_set (set []) = {[]}"
   "list_of_set_set (set (x # xs)) =
      \<Union> ((insert_in_list_at_arbitrary_pos x) ` (list_of_set_set ((set xs) - {x})))"
 by simp_all
 
 lemma list_of_set_set_is_empty :
   "list_of_set_set s = {} \<longleftrightarrow> \<not> (finite s)"
 proof -
   have "finite s \<longleftrightarrow> (\<exists>l. set l = s \<and> distinct l)"
   proof (rule iffI)
     assume "\<exists>l. set l = s \<and> distinct l" then
     obtain l where "s = set l" by blast
     thus "finite s" by simp
   next
     assume "finite s"
     thus "\<exists>l. set l = s \<and> distinct l"
     proof (induct s)
       case empty
       show ?case by auto
     next
       case (insert e s)
       note e_nin_s = insert(2)
       from insert(3) obtain l where set_l: "set l = s" and dist_l: "distinct l" by blast
 
       from set_l have set_el: "set (e # l) = insert e s" by auto
       from dist_l set_l e_nin_s have dist_el: "distinct (e # l)" by simp
 
       from set_el dist_el show ?case by blast
     qed
   qed
   thus ?thesis
     unfolding list_of_set_set_def by simp
 qed
 
 definition list_of_set :: "'a set \<Rightarrow> 'a list" where
    "list_of_set s = set_choose (list_of_set_set s)"
 
 lemma list_of_set [simp] :
   assumes fin_s: "finite s"
   shows "set (list_of_set s) = s"
         "distinct (list_of_set s)"
 proof -
   from fin_s list_of_set_set_is_empty[of s]
   have "\<not> (list_of_set_set s = {})" by simp
   hence "list_of_set s \<in> list_of_set_set s"
     unfolding list_of_set_def
     by (rule set_choose_thm)
   thus "set (list_of_set s) = s"
        "distinct (list_of_set s)" unfolding list_of_set_set_def
   by simp_all
 qed
 
 lemma list_of_set_in:
   "finite s \<Longrightarrow> list_of_set s \<in> list_of_set_set s"
 unfolding list_of_set_def
 by (metis list_of_set_set_is_empty set_choose_thm)
 
 definition ordered_list_of_set where
   "ordered_list_of_set cmp s = set_choose (sort_by cmp ` list_of_set_set s)"
 
 subsection \<open>sum\<close>
 
 find_consts "'a list => ('a list * _)"
 
 fun sum_partition :: "('a + 'b) list \<Rightarrow> 'a list * 'b list"  where
   "sum_partition [] = ([], [])"
 | "sum_partition ((Inl l) # lrs) =
      (let (ll, rl) = sum_partition lrs in
      (l # ll, rl))"
 | "sum_partition ((Inr r) # lrs) =
      (let (ll, rl) = sum_partition lrs in
      (ll, r # rl))"
 
 lemma sum_partition_length :
   "List.length lrs = List.length (fst (sum_partition lrs)) + List.length (snd (sum_partition lrs))"
 proof (induct lrs)
   case Nil thus ?case by simp
 next
   case (Cons lr lrs) thus ?case
     by (cases lr) (auto split: prod.split)
 qed
 
 subsection \<open>sorting\<close>
 
 subsection \<open>Strings\<close>
 
 declare String.literal.explode_inverse [simp]
 
 subsection \<open>num to string conversions\<close>
 
 definition nat_list_to_string :: "nat list \<Rightarrow> string" where
   "nat_list_to_string nl = map char_of nl"
 
 definition is_digit where
   "is_digit (n::nat) = (n < 10)"
 
 lemma is_digit_simps[simp] :
   "n < 10 \<Longrightarrow> is_digit n"
   "\<not>(n < 10) \<Longrightarrow> \<not>(is_digit n)"
 unfolding is_digit_def by simp_all
 
 lemma is_digit_expand :
   "is_digit n \<longleftrightarrow>
      (n = 0) \<or> (n = 1) \<or> (n = 2) \<or> (n = 3) \<or>  (n = 4) \<or>
      (n = 5) \<or> (n = 6) \<or> (n = 7) \<or> (n = 8) \<or>  (n = 9)"
 unfolding is_digit_def by auto
 
 lemmas is_digitE = is_digit_expand[THEN iffD1,elim_format]
 lemmas is_digitI = is_digit_expand[THEN iffD2,rule_format]
 
 definition is_digit_char where
   "is_digit_char c \<longleftrightarrow>
      (c = CHR ''0'') \<or> (c = CHR ''5'') \<or>
      (c = CHR ''1'') \<or> (c = CHR ''6'') \<or>
      (c = CHR ''2'') \<or> (c = CHR ''7'') \<or>
      (c = CHR ''3'') \<or> (c = CHR ''8'') \<or>
      (c = CHR ''4'') \<or> (c = CHR ''9'')"
 
 lemma is_digit_char_simps[simp] :
   "is_digit_char (CHR ''0'')"
   "is_digit_char (CHR ''1'')"
   "is_digit_char (CHR ''2'')"
   "is_digit_char (CHR ''3'')"
   "is_digit_char (CHR ''4'')"
   "is_digit_char (CHR ''5'')"
   "is_digit_char (CHR ''6'')"
   "is_digit_char (CHR ''7'')"
   "is_digit_char (CHR ''8'')"
   "is_digit_char (CHR ''9'')"
 unfolding is_digit_char_def by simp_all
 
 lemmas is_digit_charE = is_digit_char_def[THEN iffD1,elim_format]
 lemmas is_digit_charI = is_digit_char_def[THEN iffD2,rule_format]
 
 definition digit_to_char :: "nat \<Rightarrow> char" where
   "digit_to_char n = (
      if n = 0 then CHR ''0''
      else if n = 1 then CHR ''1''
      else if n = 2 then CHR ''2''
      else if n = 3 then CHR ''3''
      else if n = 4 then CHR ''4''
      else if n = 5 then CHR ''5''
      else if n = 6 then CHR ''6''
      else if n = 7 then CHR ''7''
      else if n = 8 then CHR ''8''
      else if n = 9 then CHR ''9''
      else CHR ''X'')"
 
 lemma digit_to_char_simps [simp]:
   "digit_to_char 0 = CHR ''0''"
   "digit_to_char (Suc 0) = CHR ''1''"
   "digit_to_char 2 = CHR ''2''"
   "digit_to_char 3 = CHR ''3''"
   "digit_to_char 4 = CHR ''4''"
   "digit_to_char 5 = CHR ''5''"
   "digit_to_char 6 = CHR ''6''"
   "digit_to_char 7 = CHR ''7''"
   "digit_to_char 8 = CHR ''8''"
   "digit_to_char 9 = CHR ''9''"
   "n > 9 \<Longrightarrow> digit_to_char n = CHR ''X''"
 unfolding digit_to_char_def
 by simp_all
 
 definition char_to_digit :: "char \<Rightarrow> nat" where
   "char_to_digit c = (
      if c = CHR ''0'' then 0
      else if c = CHR ''1'' then 1
      else if c = CHR ''2'' then 2
      else if c = CHR ''3'' then 3
      else if c = CHR ''4'' then 4
      else if c = CHR ''5'' then 5
      else if c = CHR ''6'' then 6
      else if c = CHR ''7'' then 7
      else if c = CHR ''8'' then 8
      else if c = CHR ''9'' then 9
      else 10)"
 
 lemma char_to_digit_simps [simp]:
   "char_to_digit (CHR ''0'') = 0"
   "char_to_digit (CHR ''1'') = 1"
   "char_to_digit (CHR ''2'') = 2"
   "char_to_digit (CHR ''3'') = 3"
   "char_to_digit (CHR ''4'') = 4"
   "char_to_digit (CHR ''5'') = 5"
   "char_to_digit (CHR ''6'') = 6"
   "char_to_digit (CHR ''7'') = 7"
   "char_to_digit (CHR ''8'') = 8"
   "char_to_digit (CHR ''9'') = 9"
 unfolding char_to_digit_def by simp_all
 
 
 lemma diget_to_char_inv[simp]:
 assumes is_digit: "is_digit n"
 shows "char_to_digit (digit_to_char n) = n"
 using is_digit unfolding is_digit_expand by auto
 
 lemma char_to_diget_inv[simp]:
 assumes is_digit: "is_digit_char c"
 shows "digit_to_char (char_to_digit c) = c"
 using is_digit
 unfolding char_to_digit_def is_digit_char_def
 by auto
 
 lemma char_to_digit_div_mod [simp]:
 assumes is_digit: "is_digit_char c"
 shows "char_to_digit c < 10"
 using is_digit
 unfolding char_to_digit_def is_digit_char_def
 by auto
 
 
 lemma is_digit_char_intro[simp]:
   "is_digit (char_to_digit c) = is_digit_char c"
 unfolding char_to_digit_def is_digit_char_def is_digit_expand
 by auto
 
 lemma is_digit_intro[simp]:
   "is_digit_char (digit_to_char n) = is_digit n"
 unfolding digit_to_char_def is_digit_char_def is_digit_expand
 by auto
 
 lemma digit_to_char_11:
 "digit_to_char n1 = digit_to_char n2 \<Longrightarrow>
  (is_digit n1 = is_digit n2) \<and> (is_digit n1 \<longrightarrow> (n1 = n2))"
 by (metis diget_to_char_inv is_digit_intro)
 
 lemma char_to_digit_11:
 "char_to_digit c1 = char_to_digit c2 \<Longrightarrow>
  (is_digit_char c1 = is_digit_char c2) \<and> (is_digit_char c1 \<longrightarrow> (c1 = c2))"
 by (metis char_to_diget_inv is_digit_char_intro)
 
 function nat_to_string :: "nat \<Rightarrow> string" where
   "nat_to_string n =
      (if (is_digit n) then [digit_to_char n] else
       nat_to_string (n div 10) @ [digit_to_char (n mod 10)])"
 by auto
 termination
   by (relation "measure id") (auto simp add: is_digit_def)
 
 definition int_to_string :: "int \<Rightarrow> string" where
   "int_to_string i \<equiv>
      if i < 0 then
        ''-'' @ nat_to_string (nat (abs i))
      else
        nat_to_string (nat i)"
 
 lemma nat_to_string_simps[simp]:
    "is_digit n \<Longrightarrow> nat_to_string n = [digit_to_char n]"
   "\<not>(is_digit n) \<Longrightarrow> nat_to_string n = nat_to_string (n div 10) @ [digit_to_char (n mod 10)]"
 by simp_all
 declare nat_to_string.simps[simp del]
 
 lemma nat_to_string_neq_nil[simp]:
   "nat_to_string n \<noteq> []"
   by (cases "is_digit n") simp_all
 
 lemmas nat_to_string_neq_nil2[simp] = nat_to_string_neq_nil[symmetric]
 
 lemma nat_to_string_char_to_digit [simp]:
   "is_digit_char c \<Longrightarrow> nat_to_string (char_to_digit c) = [c]"
 by auto
 
 lemma nat_to_string_11[simp] :
   "(nat_to_string n1 = nat_to_string n2) \<longleftrightarrow> n1 = n2"
 proof (rule iffI)
   assume "n1 = n2"
   thus "nat_to_string n1 = nat_to_string n2" by simp
 next
   assume "nat_to_string n1 = nat_to_string n2"
   thus "n1 = n2"
   proof (induct n2 arbitrary: n1 rule: less_induct)
     case (less n2')
     note ind_hyp = this(1)
     note n2s_eq = less(2)
 
     have is_dig_eq: "is_digit n2' = is_digit n1" using n2s_eq
       apply (cases "is_digit n2'")
       apply (case_tac [!] "is_digit n1")
       apply (simp_all)
     done
 
     show ?case
     proof (cases "is_digit n2'")
       case True with n2s_eq is_dig_eq show ?thesis by simp (metis digit_to_char_11)
     next
       case False
       with is_dig_eq have not_digs : "\<not> (is_digit n1)"  "\<not> (is_digit n2')" by simp_all
 
       from not_digs(2) have "n2' div 10 < n2'" unfolding is_digit_def by auto
       note ind_hyp' = ind_hyp [OF this, of "n1 div 10"]
 
       from not_digs n2s_eq ind_hyp' digit_to_char_11[of "n1 mod 10" "n2' mod 10"]
       have "(n1 mod 10) = (n2' mod 10)" "n1 div 10 = n2' div 10" by simp_all
       thus "n1 = n2'" by (metis div_mult_mod_eq)
     qed
   qed
 qed
 
 definition "is_nat_string s \<equiv> (\<forall>c\<in>set s. is_digit_char c)"
 definition "is_strong_nat_string s \<equiv> is_nat_string s \<and> (s \<noteq> []) \<and> (hd s = CHR ''0'' \<longrightarrow> length s = 1)"
 
 lemma is_nat_string_simps[simp]:
   "is_nat_string []"
   "is_nat_string (c # s) \<longleftrightarrow> is_digit_char c \<and> is_nat_string s"
 unfolding is_nat_string_def by simp_all
 
 lemma is_strong_nat_string_simps[simp]:
   "\<not>(is_strong_nat_string [])"
   "is_strong_nat_string (c # s) \<longleftrightarrow> is_digit_char c \<and> is_nat_string s \<and>
                                     (c = CHR ''0'' \<longrightarrow> s = [])"
 unfolding is_strong_nat_string_def by simp_all
 
 fun string_to_nat_aux :: "nat \<Rightarrow> string \<Rightarrow> nat" where
    "string_to_nat_aux n [] = n"
  | "string_to_nat_aux n (d#ds) =
     string_to_nat_aux (n*10 + char_to_digit d) ds"
 
 definition string_to_nat :: "string \<Rightarrow> nat option" where
    "string_to_nat s \<equiv>
     (if is_nat_string s then Some (string_to_nat_aux 0 s) else None)"
 
 definition string_to_nat' :: "string \<Rightarrow> nat" where
   "string_to_nat' s \<equiv> the (string_to_nat s)"
 
 lemma string_to_nat_aux_inv :
 assumes "is_nat_string s"
 assumes "n > 0 \<or> is_strong_nat_string s"
 shows "nat_to_string (string_to_nat_aux n s) =
 (if n = 0 then '''' else nat_to_string n) @ s"
 using assms
 proof (induct s arbitrary: n)
   case Nil
   thus ?case
     by (simp add: is_strong_nat_string_def)
 next
   case (Cons c s n)
   from Cons(2) have "is_digit_char c" "is_nat_string s" by simp_all
   note cs_ok = Cons(3)
   let ?m = "n*10 + char_to_digit c"
   note ind_hyp = Cons(1)[OF \<open>is_nat_string s\<close>, of ?m]
 
   from \<open>is_digit_char c\<close> have m_div: "?m div 10 = n" and
                               m_mod: "?m mod 10 = char_to_digit c"
     unfolding is_digit_char_def
     by auto
 
   show ?case
   proof (cases "?m = 0")
     case True
     with \<open>is_digit_char c\<close>
     have "n = 0" "c = CHR ''0''" unfolding is_digit_char_def by auto
     moreover with cs_ok have "s = []" by simp
     ultimately show ?thesis by simp
   next
     case False note m_neq_0 = this
     with ind_hyp have ind_hyp':
       "nat_to_string (string_to_nat_aux ?m s) = (nat_to_string ?m) @ s" by auto
 
     hence "nat_to_string (string_to_nat_aux n (c # s)) = (nat_to_string ?m) @ s"
       by simp
 
     with \<open>is_digit_char c\<close> m_div show ?thesis by simp
   qed
 qed
 
 lemma string_to_nat_inv :
 assumes strong_nat_s: "is_strong_nat_string s"
 assumes s2n_s: "string_to_nat s = Some n"
 shows "nat_to_string n = s"
 proof -
   from strong_nat_s have nat_s: "is_nat_string s" unfolding is_strong_nat_string_def by simp
   with s2n_s have n_eq: "n = string_to_nat_aux 0 s" unfolding string_to_nat_def by simp
 
   from string_to_nat_aux_inv[of s 0, folded n_eq] nat_s strong_nat_s
   show ?thesis by simp
 qed
 
 lemma nat_to_string_induct [case_names "digit" "non_digit"]:
 assumes digit: "\<And>d. is_digit d \<Longrightarrow> P d"
 assumes not_digit: "\<And>n. \<not>(is_digit n) \<Longrightarrow> P (n div 10) \<Longrightarrow> P (n mod 10) \<Longrightarrow> P n"
 shows "P n"
 proof (induct n rule: less_induct)
   case (less n)
   note ind_hyp = this
 
   show ?case
   proof (cases "is_digit n")
     case True with digit show ?thesis by simp
   next
     case False note not_dig = this
     hence "n div 10 < n" "n mod 10 < n" unfolding is_digit_def by auto
     with not_dig ind_hyp not_digit show ?thesis by simp
   qed
 qed
 
 lemma nat_to_string___is_nat_string [simp]:
   "is_nat_string (nat_to_string n)"
 unfolding is_nat_string_def
 proof (induct n rule: nat_to_string_induct)
   case (digit d)
   thus ?case by simp
 next
   case (non_digit n)
   thus ?case by simp
 qed
 
 lemma nat_to_string___eq_0 [simp]:
   "(nat_to_string n = (CHR ''0'')#s) \<longleftrightarrow> (n = 0 \<and> s = [])"
 unfolding is_nat_string_def
 proof (induct n arbitrary: s rule: nat_to_string_induct)
   case (digit d) thus ?case unfolding is_digit_expand by auto
 next
   case (non_digit n)
 
   obtain c s' where ns_eq: "nat_to_string (n div 10) = c # s'"
      by (cases "nat_to_string (n div 10)") auto
 
   from non_digit(1) have "n div 10 \<noteq> 0" unfolding is_digit_def by auto
   with non_digit(2) ns_eq have c_neq: "c \<noteq> CHR ''0''" by auto
 
   from \<open>\<not> (is_digit n)\<close> c_neq ns_eq
   show ?case by auto
 qed
 
 lemma nat_to_string___is_strong_nat_string:
   "is_strong_nat_string (nat_to_string n)"
 proof (cases "is_digit n")
   case True thus ?thesis by simp
 next
   case False note not_digit = this
 
   obtain c s' where ns_eq: "nat_to_string n = c # s'"
      by (cases "nat_to_string n") auto
 
   from not_digit have "0 < n" unfolding is_digit_def by simp
   with ns_eq have c_neq: "c \<noteq> CHR ''0''" by auto
   hence "hd (nat_to_string n) \<noteq> CHR ''0''" unfolding ns_eq by simp
 
   thus ?thesis unfolding is_strong_nat_string_def
     by simp
 qed
 
 lemma nat_to_string_inv :
   "string_to_nat (nat_to_string n) = Some n"
 by (metis nat_to_string_11
           nat_to_string___is_nat_string
           nat_to_string___is_strong_nat_string
           string_to_nat_def
           string_to_nat_inv)
 
 definition The_opt where
   "The_opt p = (if (\<exists>!x. p x) then Some (The p) else None)"
 
 lemma The_opt_eq_some [simp] :
 "((The_opt p) = (Some x)) \<longleftrightarrow> ((p x) \<and> ((\<forall> y.  p y \<longrightarrow> (x = y))))"
     (is "?lhs = ?rhs")
 proof (cases "\<exists>!x. p x")
   case True
   note exists_unique = this
   then obtain x where p_x: "p x" by auto
 
   from the1_equality[of p x] exists_unique p_x
   have the_opt_eq: "The_opt p = Some x"
     unfolding The_opt_def by simp
 
   from exists_unique the_opt_eq p_x show ?thesis
     by auto
 next
   case False
   note not_unique = this
 
   hence "The_opt p = None"
     unfolding The_opt_def by simp
   with not_unique show ?thesis by auto
 qed
 
 lemma The_opt_eq_none [simp] :
 "((The_opt p) = None) \<longleftrightarrow> \<not>(\<exists>!x. p x)"
 unfolding The_opt_def by auto
 
 
 end