diff --git a/thys/Higher_Order_Terms/Term_Class.thy b/thys/Higher_Order_Terms/Term_Class.thy
--- a/thys/Higher_Order_Terms/Term_Class.thy
+++ b/thys/Higher_Order_Terms/Term_Class.thy
@@ -1,1294 +1,1294 @@
 chapter \<open>Terms\<close>
 
 theory Term_Class
 imports
   Datatype_Order_Generator.Order_Generator
   Name
   Term_Utils
   Disjoint_Sets
 begin
 
 hide_type (open) "term"
 
 section \<open>A simple term type, modelled after Pure's \<open>term\<close> type\<close>
 
 datatype "term" =
   Const name |
   Free name |
   Abs "term" ("\<Lambda> _" [71] 71) |
   Bound nat |
   App "term" "term" (infixl "$" 70)
 
 derive linorder "term"
 
 section \<open>A type class describing terms\<close>
 
 text \<open>
   The type class is split into two parts, \<^emph>\<open>pre-terms\<close> and \<^emph>\<open>terms\<close>. The only difference is that
   terms assume more axioms about substitution (see below).
 
   A term must provide the following generic constructors that behave like regular free constructors:
 
   \<^item> \<open>const :: name \<Rightarrow> \<tau>\<close>
   \<^item> \<open>free :: name \<Rightarrow> \<tau>\<close>
   \<^item> \<open>app :: \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>\<close>
 \<close>
 
 text \<open>
   Conversely, there are also three corresponding destructors that could be defined in terms of
   Hilbert's choice operator. However, I have instead opted to let instances define destructors
   directly, which is simpler for execution purposes.
 
   Besides the generic constructors, terms may also contain other constructors. Those are abstractly
   called \<^emph>\<open>abstractions\<close>, even though that name is not entirely accurate (bound variables may also
   fall under this).
 
   Additionally, there must be operations that compute the list of all free variables (\<open>frees\<close>),
   constants (\<open>consts\<close>), and substitutions (\<open>subst\<close>). Pre-terms only assume some basic properties of
   substitution on the generic constructors.
 
   Most importantly, substitution is not specified for environments containing terms with free
   variables. Term types are not required to implement \<open>\<alpha>\<close>-renaming to prevent capturing of
   variables.
 \<close>
 
 class pre_term = size +
   fixes
     frees :: "'a \<Rightarrow> name fset" and
     subst :: "'a \<Rightarrow> (name, 'a) fmap \<Rightarrow> 'a" and
     "consts" :: "'a \<Rightarrow> name fset"
   fixes
     app :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and unapp :: "'a \<Rightarrow> ('a \<times> 'a) option"
   fixes
     const :: "name \<Rightarrow> 'a" and unconst :: "'a \<Rightarrow> name option"
   fixes
     free :: "name \<Rightarrow> 'a" and unfree :: "'a \<Rightarrow> name option"
   assumes unapp_app[simp]: "unapp (app u\<^sub>1 u\<^sub>2) = Some (u\<^sub>1, u\<^sub>2)"
   assumes app_unapp[dest]: "unapp u = Some (u\<^sub>1, u\<^sub>2) \<Longrightarrow> u = app u\<^sub>1 u\<^sub>2"
   assumes app_size[simp]: "size (app u\<^sub>1 u\<^sub>2) = size u\<^sub>1 + size u\<^sub>2 + 1"
   assumes unconst_const[simp]: "unconst (const name) = Some name"
   assumes const_unconst[dest]: "unconst u = Some name \<Longrightarrow> u = const name"
   assumes unfree_free[simp]: "unfree (free name) = Some name"
   assumes free_unfree[dest]: "unfree u = Some name \<Longrightarrow> u = free name"
   assumes app_const_distinct: "app u\<^sub>1 u\<^sub>2 \<noteq> const name"
   assumes app_free_distinct: "app u\<^sub>1 u\<^sub>2 \<noteq> free name"
   assumes free_const_distinct: "free name\<^sub>1 \<noteq> const name\<^sub>2"
   assumes frees_const[simp]: "frees (const name) = fempty"
   assumes frees_free[simp]: "frees (free name) = {| name |}"
   assumes frees_app[simp]: "frees (app u\<^sub>1 u\<^sub>2) = frees u\<^sub>1 |\<union>| frees u\<^sub>2"
   assumes consts_free[simp]: "consts (free name) = fempty"
   assumes consts_const[simp]: "consts (const name) = {| name |}"
   assumes consts_app[simp]: "consts (app u\<^sub>1 u\<^sub>2) = consts u\<^sub>1 |\<union>| consts u\<^sub>2"
   assumes subst_app[simp]: "subst (app u\<^sub>1 u\<^sub>2) env = app (subst u\<^sub>1 env) (subst u\<^sub>2 env)"
   assumes subst_const[simp]: "subst (const name) env = const name"
   assumes subst_free[simp]: "subst (free name) env = (case fmlookup env name of Some t \<Rightarrow> t | _ \<Rightarrow> free name)"
   assumes free_inject: "free name\<^sub>1 = free name\<^sub>2 \<Longrightarrow> name\<^sub>1 = name\<^sub>2"
   assumes const_inject: "const name\<^sub>1 = const name\<^sub>2 \<Longrightarrow> name\<^sub>1 = name\<^sub>2"
   assumes app_inject: "app u\<^sub>1 u\<^sub>2 = app u\<^sub>3 u\<^sub>4 \<Longrightarrow> u\<^sub>1 = u\<^sub>3 \<and> u\<^sub>2 = u\<^sub>4"
 
 instantiation "term" :: pre_term begin
 
 definition app_term where
 "app_term t u = t $ u"
 
 fun unapp_term where
 "unapp_term (t $ u) = Some (t, u)" |
 "unapp_term _ = None"
 
 definition const_term where
 "const_term = Const"
 
 fun unconst_term where
 "unconst_term (Const name) = Some name" |
 "unconst_term _ = None"
 
 definition free_term where
 "free_term = Free"
 
 fun unfree_term where
 "unfree_term (Free name) = Some name" |
 "unfree_term _ = None"
 
 fun frees_term :: "term \<Rightarrow> name fset" where
 "frees_term (Free x) = {| x |}" |
 "frees_term (t\<^sub>1 $ t\<^sub>2) = frees_term t\<^sub>1 |\<union>| frees_term t\<^sub>2" |
 "frees_term (\<Lambda> t) = frees_term t" |
 "frees_term _ = {||}"
 
 fun subst_term :: "term \<Rightarrow> (name, term) fmap \<Rightarrow> term" where
 "subst_term (Free s) env = (case fmlookup env s of Some t \<Rightarrow> t | None \<Rightarrow> Free s)" |
 "subst_term (t\<^sub>1 $ t\<^sub>2) env = subst_term t\<^sub>1 env $ subst_term t\<^sub>2 env" |
 "subst_term (\<Lambda> t) env = \<Lambda> subst_term t env" |
 "subst_term t env = t"
 
 fun consts_term :: "term \<Rightarrow> name fset" where
 "consts_term (Const x) = {| x |}" |
 "consts_term (t\<^sub>1 $ t\<^sub>2) = consts_term t\<^sub>1 |\<union>| consts_term t\<^sub>2" |
 "consts_term (\<Lambda> t) = consts_term t" |
 "consts_term _ = {||}"
 
 instance
   by standard
       (auto
         simp: app_term_def const_term_def free_term_def
         elim: unapp_term.elims unconst_term.elims unfree_term.elims
         split: option.splits)
 
 end
 
 context pre_term begin
 
 definition freess :: "'a list \<Rightarrow> name fset" where
 "freess = ffUnion \<circ> fset_of_list \<circ> map frees"
 
 lemma freess_cons[simp]: "freess (x # xs) = frees x |\<union>| freess xs"
 unfolding freess_def by simp
 
 lemma freess_single: "freess [x] = frees x"
 unfolding freess_def by simp
 
 lemma freess_empty[simp]: "freess [] = {||}"
 unfolding freess_def by simp
 
 lemma freess_app[simp]: "freess (xs @ ys) = freess xs |\<union>| freess ys"
 unfolding freess_def by simp
 
 lemma freess_subset: "set xs \<subseteq> set ys \<Longrightarrow> freess xs |\<subseteq>| freess ys"
 unfolding freess_def comp_apply
 by (intro ffunion_mono fset_of_list_subset) auto
 
 abbreviation id_env :: "(name, 'a) fmap \<Rightarrow> bool" where
 "id_env \<equiv> fmpred (\<lambda>x y. y = free x)"
 
 definition closed_except :: "'a \<Rightarrow> name fset \<Rightarrow> bool" where
 "closed_except t S \<longleftrightarrow> frees t |\<subseteq>| S"
 
 abbreviation closed :: "'a \<Rightarrow> bool" where
 "closed t \<equiv> closed_except t {||}"
 
 lemmas term_inject = free_inject const_inject app_inject
 
 lemmas term_distinct[simp] =
   app_const_distinct app_const_distinct[symmetric]
   app_free_distinct app_free_distinct[symmetric]
   free_const_distinct free_const_distinct[symmetric]
 
 lemma app_size1: "size u\<^sub>1 < size (app u\<^sub>1 u\<^sub>2)"
 by simp
 
 lemma app_size2: "size u\<^sub>2 < size (app u\<^sub>1 u\<^sub>2)"
 by simp
 
 lemma unx_some_lemmas:
   "unapp u = Some x \<Longrightarrow> unconst u = None"
   "unapp u = Some x \<Longrightarrow> unfree u = None"
   "unconst u = Some y \<Longrightarrow> unapp u = None"
   "unconst u = Some y \<Longrightarrow> unfree u = None"
   "unfree u = Some z \<Longrightarrow> unconst u = None"
   "unfree u = Some z \<Longrightarrow> unapp u = None"
 subgoal by (metis app_unapp const_unconst app_const_distinct not_None_eq surj_pair)
 subgoal by (metis app_free_distinct app_unapp free_unfree option.exhaust surj_pair)
 subgoal by (metis app_unapp const_unconst app_const_distinct old.prod.exhaust option.distinct(1) option.expand option.sel)
 subgoal by (metis const_unconst free_const_distinct free_unfree option.exhaust)
 subgoal by (metis const_unconst free_const_distinct free_unfree option.exhaust)
 subgoal by (metis app_free_distinct app_unapp free_unfree not_Some_eq surj_pair)
 done
 
 lemma unx_none_simps[simp]:
   "unapp (const name) = None"
   "unapp (free name) = None"
   "unconst (app t u) = None"
   "unconst (free name) = None"
   "unfree (const name) = None"
   "unfree (app t u) = None"
 subgoal by (metis app_unapp app_const_distinct not_None_eq surj_pair)
 subgoal by (metis app_free_distinct app_unapp option.exhaust surj_pair)
 subgoal by (metis const_unconst app_const_distinct option.distinct(1) option.expand option.sel)
 subgoal by (metis const_unconst free_const_distinct option.exhaust)
 subgoal by (metis free_const_distinct free_unfree option.exhaust)
 subgoal by (metis app_free_distinct free_unfree not_Some_eq)
 done
 
 lemma term_cases:
   obtains (free) name where "t = free name"
         | (const) name where "t = const name"
         | (app) u\<^sub>1 u\<^sub>2 where "t = app u\<^sub>1 u\<^sub>2"
         | (other) "unfree t = None" "unapp t = None" "unconst t = None"
 apply (cases "unfree t")
 apply (cases "unconst t")
 apply (cases "unapp t")
 subgoal by auto
 subgoal for x by (cases x) auto
 subgoal by auto
 subgoal by auto
 done
 
 definition is_const where
 "is_const t \<longleftrightarrow> (unconst t \<noteq> None)"
 
 definition const_name where
 "const_name t = (case unconst t of Some name \<Rightarrow> name)"
 
 lemma is_const_simps[simp]:
   "is_const (const name)"
   "\<not> is_const (app t u)"
   "\<not> is_const (free name)"
 unfolding is_const_def by simp+
 
 lemma const_name_simps[simp]:
   "const_name (const name) = name"
   "is_const t \<Longrightarrow> const (const_name t) = t"
 unfolding const_name_def is_const_def by auto
 
 definition is_free where
 "is_free t \<longleftrightarrow> (unfree t \<noteq> None)"
 
 definition free_name where
 "free_name t = (case unfree t of Some name \<Rightarrow> name)"
 
 lemma is_free_simps[simp]:
   "is_free (free name)"
   "\<not> is_free (const name)"
   "\<not> is_free (app t u)"
 unfolding is_free_def by simp+
 
 lemma free_name_simps[simp]:
   "free_name (free name) = name"
   "is_free t \<Longrightarrow> free (free_name t) = t"
 unfolding free_name_def is_free_def by auto
 
 definition is_app where
 "is_app t \<longleftrightarrow> (unapp t \<noteq> None)"
 
 definition left where
 "left t = (case unapp t of Some (l, _) \<Rightarrow> l)"
 
 definition right where
 "right t = (case unapp t of Some (_, r) \<Rightarrow> r)"
 
 lemma app_simps[simp]:
   "\<not> is_app (const name)"
   "\<not> is_app (free name)"
   "is_app (app t u)"
 unfolding is_app_def by simp+
 
 lemma left_right_simps[simp]:
   "left (app l r) = l"
   "right (app l r) = r"
   "is_app t \<Longrightarrow> app (left t) (right t) = t"
 unfolding is_app_def left_def right_def by auto
 
 definition ids :: "'a \<Rightarrow> name fset" where
 "ids t = frees t |\<union>| consts t"
 
 lemma closed_except_const[simp]: "closed_except (const name) S"
 unfolding closed_except_def by auto
 
 abbreviation closed_env :: "(name, 'a) fmap \<Rightarrow> bool" where
 "closed_env \<equiv> fmpred (\<lambda>_. closed)"
 
 lemma closed_except_self: "closed_except t (frees t)"
 unfolding closed_except_def by simp
 
 end
 
 class "term" = pre_term + size +
   fixes
     abs_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   assumes
     raw_induct[case_names const free app abs]:
       "(\<And>name. P (const name)) \<Longrightarrow>
         (\<And>name. P (free name)) \<Longrightarrow>
         (\<And>t\<^sub>1 t\<^sub>2. P t\<^sub>1 \<Longrightarrow> P t\<^sub>2 \<Longrightarrow> P (app t\<^sub>1 t\<^sub>2)) \<Longrightarrow>
         (\<And>t. abs_pred P t) \<Longrightarrow>
         P t"
   assumes
     raw_subst_id: "abs_pred (\<lambda>t. \<forall>env. id_env env \<longrightarrow> subst t env = t) t" and
     raw_subst_drop: "abs_pred (\<lambda>t. x |\<notin>| frees t \<longrightarrow> (\<forall>env. subst t (fmdrop x env) = subst t env)) t" and
     raw_subst_indep: "abs_pred (\<lambda>t. \<forall>env\<^sub>1 env\<^sub>2. closed_env env\<^sub>2 \<longrightarrow> fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2) \<longrightarrow> subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t env\<^sub>2) env\<^sub>1) t" and
     raw_subst_frees: "abs_pred (\<lambda>t. \<forall>env. closed_env env \<longrightarrow> frees (subst t env) = frees t |-| fmdom env) t" and
     raw_subst_consts': "abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t" and
     abs_pred_trivI: "P t \<Longrightarrow> abs_pred P t"
 begin
 
 lemma subst_id: "id_env env \<Longrightarrow> subst t env = t"
 proof (induction t arbitrary: env rule: raw_induct)
   case (abs t)
   show ?case
     by (rule raw_subst_id)
 qed (auto split: option.splits)
 
 lemma subst_drop: "x |\<notin>| frees t \<Longrightarrow> subst t (fmdrop x env) = subst t env"
 proof (induction t arbitrary: env rule: raw_induct)
   case (abs t)
   show ?case
     by (rule raw_subst_drop)
 qed (auto split: option.splits)
 
 lemma subst_frees: "fmpred (\<lambda>_. closed) env \<Longrightarrow> frees (subst t env) = frees t |-| fmdom env"
 proof (induction t arbitrary: env rule: raw_induct)
   case (abs t)
   show ?case
     by (rule raw_subst_frees)
 qed (auto split: option.splits simp: closed_except_def)
 
 lemma subst_consts': "consts (subst t env) = consts t |\<union>| ffUnion (consts |`| fmimage env (frees t))"
 proof (induction t arbitrary: env rule: raw_induct)
   case (free name)
   then show ?case
     by (auto
           split: option.splits
           simp: ffUnion_alt_def fmlookup_ran_iff fmlookup_image_iff fmlookup_dom_iff
           intro!: fBexI)
 next
   case (abs t)
   show ?case
     by (rule raw_subst_consts')
 qed (auto simp: funion_image_bind_eq finter_funion_distrib fbind_funion)
 
 fun match :: "term \<Rightarrow> 'a \<Rightarrow> (name, 'a) fmap option" where
 "match (t\<^sub>1 $ t\<^sub>2) u = do {
   (u\<^sub>1, u\<^sub>2) \<leftarrow> unapp u;
   env\<^sub>1 \<leftarrow> match t\<^sub>1 u\<^sub>1;
   env\<^sub>2 \<leftarrow> match t\<^sub>2 u\<^sub>2;
   Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)
 }" |
 "match (Const name) u =
   (case unconst u of
     None \<Rightarrow> None
   | Some name' \<Rightarrow> if name = name' then Some fmempty else None)" |
 "match (Free name) u = Some (fmap_of_list [(name, u)])" |
 "match (Bound n) u = None" |
 "match (Abs t) u = None"
 
 lemma match_simps[simp]:
   "match (t\<^sub>1 $ t\<^sub>2) (app u\<^sub>1 u\<^sub>2) = do {
     env\<^sub>1 \<leftarrow> match t\<^sub>1 u\<^sub>1;
     env\<^sub>2 \<leftarrow> match t\<^sub>2 u\<^sub>2;
     Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)
   }"
   "match (Const name) (const name') = (if name = name' then Some fmempty else None)"
 by auto
 
 lemma match_some_induct[consumes 1, case_names app const free]:
   assumes "match t u = Some env"
   assumes "\<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2. P t\<^sub>1 u\<^sub>1 env\<^sub>1 \<Longrightarrow> match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1 \<Longrightarrow> P t\<^sub>2 u\<^sub>2 env\<^sub>2 \<Longrightarrow> match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2 \<Longrightarrow> P (t\<^sub>1 $ t\<^sub>2) (app u\<^sub>1 u\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2)"
   assumes "\<And>name. P (Const name) (const name) fmempty"
   assumes "\<And>name u. P (Free name) u (fmupd name u fmempty)"
   shows "P t u env"
 using assms
 by (induction t u arbitrary: env rule: match.induct)
    (auto split: option.splits if_splits elim!: option_bindE)
 
 lemma match_dom: "match p t = Some env \<Longrightarrow> fmdom env = frees p"
 by (induction p arbitrary: t env)
    (fastforce split: option.splits if_splits elim: option_bindE)+
 
 lemma match_vars: "match p t = Some env \<Longrightarrow> fmpred (\<lambda>_ u. frees u |\<subseteq>| frees t) env"
 proof (induction p t env rule: match_some_induct)
   case (app t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2)
   show ?case
     apply rule
     using app
     by (fastforce intro: fmpred_mono_strong)+
 qed auto
 
 lemma match_appE_split:
   assumes "match (t\<^sub>1 $ t\<^sub>2) u = Some env"
   obtains u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2 where
     "u = app u\<^sub>1 u\<^sub>2" "match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1" "match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2" "env = env\<^sub>1 ++\<^sub>f env\<^sub>2"
 using assms
 by (auto split: option.splits elim!: option_bindE)
 
 lemma subst_consts:
   assumes "consts t |\<subseteq>| S" "fmpred (\<lambda>_ u. consts u |\<subseteq>| S) env"
   shows "consts (subst t env) |\<subseteq>| S"
 apply (subst subst_consts')
 using assms by (auto intro!: ffUnion_least)
 
 lemma subst_empty[simp]: "subst t fmempty = t"
 by (auto simp: subst_id)
 
 lemma subst_drop_fset: "fdisjnt S (frees t) \<Longrightarrow> subst t (fmdrop_fset S env) = subst t env"
 by (induct S) (auto simp: subst_drop fdisjnt_alt_def)
 
 lemma subst_restrict:
   assumes "frees t |\<subseteq>| M"
   shows "subst t (fmrestrict_fset M env) = subst t env"
 proof -
   have *: "fmrestrict_fset M env = fmdrop_fset (fmdom env - M) env"
     by (rule fmap_ext) auto
 
   show ?thesis
     apply (subst *)
     apply (subst subst_drop_fset)
     unfolding fdisjnt_alt_def
     using assms by auto
 qed
 
 corollary subst_restrict'[simp]: "subst t (fmrestrict_fset (frees t) env) = subst t env"
 by (simp add: subst_restrict)
 
 corollary subst_cong:
   assumes "\<And>x. x |\<in>| frees t \<Longrightarrow> fmlookup \<Gamma>\<^sub>1 x = fmlookup \<Gamma>\<^sub>2 x"
   shows "subst t \<Gamma>\<^sub>1 = subst t \<Gamma>\<^sub>2"
 proof -
   have "fmrestrict_fset (frees t) \<Gamma>\<^sub>1 = fmrestrict_fset (frees t) \<Gamma>\<^sub>2"
     apply (rule fmap_ext)
     using assms by simp
   thus ?thesis
     by (metis subst_restrict')
 qed
 
 corollary subst_add_disjnt:
   assumes "fdisjnt (frees t) (fmdom env\<^sub>1)"
   shows "subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst t env\<^sub>2"
 proof -
   have "subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst t (fmrestrict_fset (frees t) (env\<^sub>1 ++\<^sub>f env\<^sub>2))"
     by (metis subst_restrict')
   also have "\<dots> = subst t (fmrestrict_fset (frees t) env\<^sub>1 ++\<^sub>f fmrestrict_fset (frees t) env\<^sub>2)"
     by simp
   also have "\<dots> = subst t (fmempty ++\<^sub>f fmrestrict_fset (frees t) env\<^sub>2)"
     unfolding fmfilter_alt_defs
     apply (subst fmfilter_false)
     using assms
     by (auto simp: fdisjnt_alt_def intro: fmdomI)
   also have "\<dots> = subst t (fmrestrict_fset (frees t) env\<^sub>2)"
     by simp
   also have "\<dots> = subst t env\<^sub>2"
     by simp
   finally show ?thesis .
 qed
 
 corollary subst_add_shadowed_env:
   assumes "frees t |\<subseteq>| fmdom env\<^sub>2"
   shows "subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst t env\<^sub>2"
 proof -
   have "subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst t (fmdrop_fset (fmdom env\<^sub>2) env\<^sub>1 ++\<^sub>f env\<^sub>2)"
     by (subst fmadd_drop_left_dom) rule
   also have "\<dots> = subst t (fmrestrict_fset (frees t) (fmdrop_fset (fmdom env\<^sub>2) env\<^sub>1 ++\<^sub>f env\<^sub>2))"
     by (metis subst_restrict')
   also have "\<dots> = subst t (fmrestrict_fset (frees t) (fmdrop_fset (fmdom env\<^sub>2) env\<^sub>1) ++\<^sub>f fmrestrict_fset (frees t) env\<^sub>2)"
     by simp
   also have "\<dots> = subst t (fmempty ++\<^sub>f fmrestrict_fset (frees t) env\<^sub>2)"
     unfolding fmfilter_alt_defs
     using fsubsetD[OF assms]
     by auto
   also have "\<dots> = subst t env\<^sub>2"
     by simp
   finally show ?thesis .
 qed
 
 corollary subst_restrict_closed: "closed_except t S \<Longrightarrow> subst t (fmrestrict_fset S env) = subst t env"
 by (metis subst_restrict closed_except_def)
 
 lemma subst_closed_except_id:
   assumes "closed_except t S" "fdisjnt (fmdom env) S"
   shows "subst t env = t"
 using assms
 by (metis fdisjnt_subset_right fmdom_drop_fset fminus_cancel fmrestrict_fset_dom
           fmrestrict_fset_null closed_except_def subst_drop_fset subst_empty)
 
 lemma subst_closed_except_preserved:
   assumes "closed_except t S" "fdisjnt (fmdom env) S"
   shows "closed_except (subst t env) S"
 using assms
 by (metis subst_closed_except_id)
 
 corollary subst_closed_id: "closed t \<Longrightarrow> subst t env = t"
 by (simp add: subst_closed_except_id fdisjnt_alt_def)
 
 corollary subst_closed_preserved: "closed t \<Longrightarrow> closed (subst t env)"
 by (simp add: subst_closed_except_preserved fdisjnt_alt_def)
 
 
 context begin
 
 private lemma subst_indep0:
   assumes "closed_env env\<^sub>2" "fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)"
   shows "subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t env\<^sub>2) env\<^sub>1"
 using assms proof (induction t arbitrary: env\<^sub>1 env\<^sub>2 rule: raw_induct)
   case (free name)
   show ?case
     using \<open>closed_env env\<^sub>2\<close>
     by (cases rule: fmpred_cases[where x = name]) (auto simp: subst_closed_id)
 next
   case (abs t)
   show ?case
     by (rule raw_subst_indep)
 qed auto
 
 lemma subst_indep:
   assumes "closed_env \<Gamma>'"
   shows "subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>"
 proof -
   have "subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>'))"
     by (metis subst_restrict')
   also have "\<dots> = subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>')"
     by (smt fmlookup_add fmlookup_restrict_fset subst_cong)
   also have "\<dots> = subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>')"
     by (rule subst_cong) (simp add: fmfilter_alt_defs(5))
   also have "\<dots> = subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>)"
     apply (rule subst_indep0[OF assms])
     using fmdom_restrict_fset
     unfolding fdisjnt_alt_def
     by auto
   also have "\<dots> = subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>)"
     using assms by (auto simp: subst_frees)
   also have "\<dots> = subst (subst t \<Gamma>') \<Gamma>"
     by simp
   finally show ?thesis .
 qed
 
 lemma subst_indep':
   assumes "closed_env \<Gamma>'" "fdisjnt (fmdom \<Gamma>') (fmdom \<Gamma>)"
   shows "subst t (\<Gamma>' ++\<^sub>f \<Gamma>) = subst (subst t \<Gamma>') \<Gamma>"
 using assms by (metis subst_indep fmadd_disjnt)
 
 lemma subst_twice:
   assumes "\<Gamma>' \<subseteq>\<^sub>f \<Gamma>" "closed_env \<Gamma>'"
   shows "subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>"
 proof -
   have "subst (subst t \<Gamma>') \<Gamma> = subst t (\<Gamma> ++\<^sub>f \<Gamma>')"
     apply (rule subst_indep[symmetric])
     apply fact
     done
   also have "\<dots> = subst t \<Gamma>"
     apply (rule subst_cong)
     using \<open>\<Gamma>' \<subseteq>\<^sub>f \<Gamma>\<close> unfolding fmsubset_alt_def
     by fastforce
   finally show ?thesis .
 qed
 
 end
 
 fun matchs :: "term list \<Rightarrow> 'a list \<Rightarrow> (name, 'a) fmap option" where
 "matchs [] [] = Some fmempty" |
 "matchs (t # ts) (u # us) = do { env\<^sub>1 \<leftarrow> match t u; env\<^sub>2 \<leftarrow> matchs ts us; Some (env\<^sub>1 ++\<^sub>f env\<^sub>2) }" |
 "matchs _ _ = None"
 
 lemmas matchs_induct = matchs.induct[case_names empty cons]
 
 context begin
 
 private lemma matchs_alt_def0:
   assumes "length ps = length vs"
   shows "map_option (\<lambda>env. m ++\<^sub>f env) (matchs ps vs) = map_option (foldl (++\<^sub>f) m) (those (map2 match ps vs))"
 using assms proof (induction arbitrary: m rule: list_induct2)
   case (Cons x xs y ys)
   show ?case
     proof (cases "match x y")
       case x_y: Some
       show ?thesis
         proof (cases "matchs xs ys")
           case None
           with x_y Cons show ?thesis
             by simp
         next
           case Some
           with x_y show ?thesis
             apply simp
             using Cons(2) apply simp
             apply (subst option.map_comp)
             by (auto cong: map_option_cong)
         qed
     qed simp
 qed simp
 
 lemma matchs_alt_def:
   assumes "length ps = length vs"
   shows "matchs ps vs = map_option (foldl (++\<^sub>f) fmempty) (those (map2 match ps vs))"
 by (subst matchs_alt_def0[where m = fmempty, simplified, symmetric, OF assms])
    (simp add: option.map_ident)
 
 end
 
 lemma matchs_neq_length_none[simp]: "length xs \<noteq> length ys \<Longrightarrow> matchs xs ys = None"
 by (induct xs ys rule: matchs.induct) fastforce+
 
 corollary matchs_some_eq_length: "matchs xs ys = Some env \<Longrightarrow> length xs = length ys"
 by (metis option.distinct(1) matchs_neq_length_none)
 
 lemma matchs_app[simp]:
   assumes "length xs\<^sub>2 = length ys\<^sub>2"
   shows "matchs (xs\<^sub>1 @ xs\<^sub>2) (ys\<^sub>1 @ ys\<^sub>2) =
           matchs xs\<^sub>1 ys\<^sub>1 \<bind> (\<lambda>env\<^sub>1. matchs xs\<^sub>2 ys\<^sub>2 \<bind> (\<lambda>env\<^sub>2. Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)))"
 using assms
 by (induct xs\<^sub>1 ys\<^sub>1 rule: matchs.induct) fastforce+
 
 corollary matchs_appI:
   assumes "matchs xs ys = Some env\<^sub>1" "matchs xs' ys' = Some env\<^sub>2"
   shows "matchs (xs @ xs') (ys @ ys') = Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)"
 using assms
 by (metis (no_types, lifting) Option.bind_lunit matchs_app matchs_some_eq_length)
 
 corollary matchs_dom:
   assumes "matchs ps ts = Some env"
   shows "fmdom env = freess ps"
 using assms
 by (induction ps ts arbitrary: env rule: matchs_induct)
    (auto simp: match_dom elim!: option_bindE)
 
 fun find_match :: "(term \<times> 'a) list \<Rightarrow> 'a \<Rightarrow> ((name, 'a) fmap \<times> term \<times> 'a) option" where
 "find_match [] _ = None" |
 "find_match ((pat, rhs) # cs) t =
   (case match pat t of
     Some env \<Rightarrow> Some (env, pat, rhs)
   | None \<Rightarrow> find_match cs t)"
 
 lemma find_match_map:
   "find_match (map (\<lambda>(pat, t). (pat, f pat t)) cs) t =
     map_option (\<lambda>(env, pat, rhs). (env, pat, f pat rhs)) (find_match cs t)"
 by (induct cs) (auto split: option.splits)
 
 lemma find_match_elem:
   assumes "find_match cs t = Some (env, pat, rhs)"
   shows "(pat, rhs) \<in> set cs" "match pat t = Some env"
 using assms
 by (induct cs) (auto split: option.splits)
 
 lemma match_subst_closed:
   assumes "match pat t = Some env" "closed_except rhs (frees pat)" "closed t"
   shows "closed (subst rhs env)"
 using assms
 by (smt fminusE fmpred_iff fset_mp fsubsetI closed_except_def match_vars match_dom subst_frees)
 
 fun rewrite_step :: "(term \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
 "rewrite_step (t\<^sub>1, t\<^sub>2) u = map_option (subst t\<^sub>2) (match t\<^sub>1 u)"
 
 abbreviation rewrite_step' :: "(term \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("_/ \<turnstile>/ _ \<rightarrow>/ _" [50,0,50] 50) where
 "r \<turnstile> t \<rightarrow> u \<equiv> rewrite_step r t = Some u"
 
 lemma rewrite_step_closed:
   assumes "frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1" "(t\<^sub>1, t\<^sub>2) \<turnstile> u \<rightarrow> u'" "closed u"
   shows "closed u'"
 proof -
   from assms obtain env where *: "match t\<^sub>1 u = Some env"
     by auto
   then have "closed (subst t\<^sub>2 env)"
     apply (rule match_subst_closed[where pat = t\<^sub>1 and t = u])
     using assms unfolding closed_except_def by auto
   with * show ?thesis
     using assms by auto
 qed
 
 definition matches :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<lesssim>" 50) where
 "t \<lesssim> u \<longleftrightarrow> (\<exists>env. subst t env = u)"
 
 lemma matchesI[intro]: "subst t env = u \<Longrightarrow> t \<lesssim> u"
 unfolding matches_def by auto
 
 lemma matchesE[elim]:
   assumes "t \<lesssim> u"
   obtains env where "subst t env = u"
 using assms unfolding matches_def by blast
 
 definition overlapping :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 "overlapping s t \<longleftrightarrow> (\<exists>u. s \<lesssim> u \<and> t \<lesssim> u)"
 
 lemma overlapping_refl: "overlapping t t"
 unfolding overlapping_def matches_def by blast
 
 lemma overlapping_sym: "overlapping t u \<Longrightarrow> overlapping u t"
 unfolding overlapping_def by auto
 
 lemma overlappingI[intro]: "s \<lesssim> u \<Longrightarrow> t \<lesssim> u \<Longrightarrow> overlapping s t"
 unfolding overlapping_def by auto
 
 lemma overlappingE[elim]:
   assumes "overlapping s t"
   obtains u where "s \<lesssim> u" "t \<lesssim> u"
 using assms unfolding overlapping_def by blast
 
 abbreviation "non_overlapping s t \<equiv> \<not> overlapping s t"
 
 corollary non_overlapping_implies_neq: "non_overlapping t u \<Longrightarrow> t \<noteq> u"
 by (metis overlapping_refl)
 
 end
 
 inductive rewrite_first :: "(term \<times> 'a::term) list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
 match: "match pat t = Some env \<Longrightarrow> rewrite_first ((pat, rhs) # _) t (subst rhs env)" |
 nomatch: "match pat t = None \<Longrightarrow> rewrite_first cs t t' \<Longrightarrow> rewrite_first ((pat, _) # cs) t t'"
 
 code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool) rewrite_first .
 
 lemma rewrite_firstE:
   assumes "rewrite_first cs t t'"
   obtains pat rhs env where "(pat, rhs) \<in> set cs" "match pat t = Some env" "t' = subst rhs env"
 using assms by induction auto
 
 text \<open>
   This doesn't follow from @{thm [source] find_match_elem}, because @{const rewrite_first} requires
   the first match, not just any.
 \<close>
 
 lemma find_match_rewrite_first:
   assumes "find_match cs t = Some (env, pat, rhs)"
   shows "rewrite_first cs t (subst rhs env)"
 using assms proof (induction cs)
   case (Cons c cs)
   obtain pat0 rhs0 where "c = (pat0, rhs0)"
     by fastforce
   thus ?case
     using Cons
     by (cases "match pat0 t") (auto intro: rewrite_first.intros)
 qed simp
 
 definition term_cases :: "(name \<Rightarrow> 'b) \<Rightarrow> (name \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a::term \<Rightarrow> 'b" where
 "term_cases if_const if_free if_app otherwise t =
   (case unconst t of
     Some name \<Rightarrow> if_const name |
     None \<Rightarrow> (case unfree t of
       Some name \<Rightarrow> if_free name |
       None \<Rightarrow>
         (case unapp t of
           Some (t, u) \<Rightarrow> if_app t u
         | None \<Rightarrow> otherwise)))"
 
 lemma term_cases_cong[fundef_cong]:
   assumes "t = u" "otherwise1 = otherwise2"
   assumes "(\<And>name. t = const name \<Longrightarrow> if_const1 name = if_const2 name)"
   assumes "(\<And>name. t = free name \<Longrightarrow> if_free1 name = if_free2 name)"
   assumes "(\<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> if_app1 u\<^sub>1 u\<^sub>2 = if_app2 u\<^sub>1 u\<^sub>2)"
   shows "term_cases if_const1 if_free1 if_app1 otherwise1 t = term_cases if_const2 if_free2 if_app2 otherwise2 u"
 using assms
 unfolding term_cases_def
 by (auto split: option.splits)
 
 lemma term_cases[simp]:
   "term_cases if_const if_free if_app otherwise (const name) = if_const name"
   "term_cases if_const if_free if_app otherwise (free name) = if_free name"
   "term_cases if_const if_free if_app otherwise (app t u) = if_app t u"
 unfolding term_cases_def
 by (auto split: option.splits)
 
 lemma term_cases_template:
   assumes "\<And>x. f x = term_cases if_const if_free if_app otherwise x"
   shows "f (const name) = if_const name"
     and "f (free name) = if_free name"
     and "f (app t u) = if_app t u"
 unfolding assms by (rule term_cases)+
 
 context "term" begin
 
 function (sequential) strip_comb :: "'a \<Rightarrow> 'a \<times> 'a list" where
 [simp del]: "strip_comb t =
   (case unapp t of
     Some (t, u) \<Rightarrow>
       (let (f, args) = strip_comb t in (f, args @ [u]))
   | None \<Rightarrow> (t, []))"
 by pat_completeness auto
 
 (* FIXME why is this not automatic? *)
 termination
   apply (relation "measure size")
   apply rule
   apply auto
   done
 
 lemma strip_comb_simps[simp]:
   "strip_comb (app t u) = (let (f, args) = strip_comb t in (f, args @ [u]))"
   "unapp t = None \<Longrightarrow> strip_comb t = (t, [])"
 by (subst strip_comb.simps; auto)+
 
 lemma strip_comb_induct[case_names app no_app]:
   assumes "\<And>x y. P x \<Longrightarrow> P (app x y)"
   assumes "\<And>t. unapp t = None \<Longrightarrow> P t"
   shows "P t"
 proof (rule strip_comb.induct, goal_cases)
   case (1 t)
   show ?case
     proof (cases "unapp t")
       case None
       with assms show ?thesis by metis
     next
       case (Some a)
       then show ?thesis
         apply (cases a)
         using 1 assms by auto
     qed
 qed
 
 lemma strip_comb_size: "t' \<in> set (snd (strip_comb t)) \<Longrightarrow> size t' < size t"
 by (induction t rule: strip_comb_induct) (auto split: prod.splits)
 
 lemma sstrip_comb_termination[termination_simp]:
   "(f, ts) = strip_comb t \<Longrightarrow> t' \<in> set ts \<Longrightarrow> size t' < size t"
 by (metis snd_conv strip_comb_size)
 
 lemma strip_comb_empty: "snd (strip_comb t) = [] \<Longrightarrow> fst (strip_comb t) = t"
 by (induction t rule: strip_comb_induct) (auto split: prod.splits)
 
 lemma strip_comb_app: "fst (strip_comb (app t u)) = fst (strip_comb t)"
 by (simp split: prod.splits)
 
 primrec list_comb :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a" where
 "list_comb f [] = f" |
 "list_comb f (t # ts) = list_comb (app f t) ts"
 
 lemma list_comb_app[simp]: "list_comb f (xs @ ys) = list_comb (list_comb f xs) ys"
 by (induct xs arbitrary: f) auto
 
 corollary list_comb_snoc: "app (list_comb f xs) y = list_comb f (xs @ [y])"
 by simp
 
 lemma list_comb_size[simp]: "size (list_comb f xs) = size f + size_list size xs"
 by (induct xs arbitrary: f) auto
 
 lemma subst_list_comb: "subst (list_comb f xs) env = list_comb (subst f env) (map (\<lambda>t. subst t env) xs)"
 by (induct xs arbitrary: f) auto
 
 abbreviation const_list_comb :: "name \<Rightarrow> 'a list \<Rightarrow> 'a" (infixl "$$" 70) where
 "const_list_comb name \<equiv> list_comb (const name)"
 
 lemma list_strip_comb[simp]: "list_comb (fst (strip_comb t)) (snd (strip_comb t)) = t"
 by (induction t rule: strip_comb_induct) (auto split: prod.splits)
 
 lemma strip_list_comb: "strip_comb (list_comb f ys) = (fst (strip_comb f), snd (strip_comb f) @ ys)"
 by (induct ys arbitrary: f) (auto simp: split_beta)
 
 lemma strip_list_comb_const: "strip_comb (name $$ xs) = (const name, xs)"
 by (simp add: strip_list_comb)
 
 lemma frees_list_comb[simp]: "frees (list_comb t xs) = frees t |\<union>| freess xs"
 by (induct xs arbitrary: t) (auto simp: freess_def)
 
 lemma consts_list_comb: "consts (list_comb f xs) = consts f |\<union>| ffUnion (fset_of_list (map consts xs))"
 by (induct xs arbitrary: f) auto
 
 lemma ids_list_comb: "ids (list_comb f xs) = ids f |\<union>| ffUnion (fset_of_list (map ids xs))"
 unfolding ids_def frees_list_comb consts_list_comb freess_def
 apply auto
 apply (smt fbind_iff finsert_absorb finsert_fsubset funion_image_bind_eq inf_sup_ord(3))
 apply (metis fbind_iff funionCI funion_image_bind_eq)
 by (smt fbind_iff funionE funion_image_bind_eq)
 
 lemma frees_strip_comb: "frees t = frees (fst (strip_comb t)) |\<union>| freess (snd (strip_comb t))"
 by (metis list_strip_comb frees_list_comb)
 
 lemma list_comb_cases':
   obtains (app) "is_app (list_comb f xs)"
         | (empty) "list_comb f xs = f" "xs = []"
 by (induction xs arbitrary: f) auto
 
 (* FIXME case names? *)
 lemma list_comb_cases[consumes 1]:
   assumes "t = list_comb f xs"
   obtains (head) "t = f" "xs = []"
         | (app) u v where "t = app u v"
 using assms by (metis list_comb_cases' left_right_simps(3))
 
 end
 
 fun left_nesting :: "'a::term \<Rightarrow> nat" where
 [simp del]: "left_nesting t = term_cases (\<lambda>_. 0) (\<lambda>_. 0) (\<lambda>t u. Suc (left_nesting t)) 0 t"
 
 lemmas left_nesting_simps[simp] = term_cases_template[OF left_nesting.simps]
 
 lemma list_comb_nesting[simp]: "left_nesting (list_comb f xs) = left_nesting f + length xs"
 by (induct xs arbitrary: f) auto
 
 lemma list_comb_cond_inj:
   assumes "list_comb f xs = list_comb g ys" "left_nesting f = left_nesting g"
   shows "xs = ys" "f = g"
 using assms proof (induction xs arbitrary: f g ys)
   case Nil
   fix f g :: 'a
   fix ys
   assume prems: "list_comb f [] = list_comb g ys" "left_nesting f = left_nesting g"
 
   hence "left_nesting f = left_nesting g + length ys"
     by simp
   with prems show "[] = ys" "f = g"
     by simp+
 next
   case (Cons x xs)
   fix f g ys
   assume prems: "list_comb f (x # xs) = list_comb g ys" "left_nesting f = left_nesting g"
 
   hence "left_nesting (list_comb f (x # xs)) = left_nesting (list_comb g ys)"
     by simp
   hence "Suc (left_nesting f + length xs) = left_nesting g + length ys"
     by simp
   with prems have "length ys = Suc (length xs)"
     by linarith
   then obtain z zs where "ys = z # zs"
     by (metis length_Suc_conv)
 
   thus "x # xs = ys" "f = g"
     using prems Cons[where ys = zs and f = "app f x" and g = "app g z"]
     by (auto dest: app_inject)
 qed
 
 lemma list_comb_inj_second: "inj (list_comb f)"
 by (metis injI list_comb_cond_inj)
 
 lemma list_comb_semi_inj:
   assumes "length xs = length ys"
   assumes "list_comb f xs = list_comb g ys"
   shows "xs = ys" "f = g"
 proof -
   from assms have "left_nesting (list_comb f xs) = left_nesting (list_comb g ys)"
     by simp
   with assms have "left_nesting f = left_nesting g"
     unfolding list_comb_nesting by simp
   with assms show "xs = ys" "f = g"
     by (metis list_comb_cond_inj)+
 qed
 
 fun no_abs :: "'a::term \<Rightarrow> bool" where
 [simp del]: "no_abs t = term_cases (\<lambda>_. True) (\<lambda>_. True) (\<lambda>t u. no_abs t \<and> no_abs u) False t"
 
 lemmas no_abs_simps[simp] = term_cases_template[OF no_abs.simps]
 
 lemma no_abs_induct[consumes 1, case_names free const app, induct pred: no_abs]:
   assumes "no_abs t"
   assumes "\<And>name. P (free name)"
   assumes "\<And>name. P (const name)"
   assumes "\<And>t\<^sub>1 t\<^sub>2. P t\<^sub>1 \<Longrightarrow> no_abs t\<^sub>1 \<Longrightarrow> P t\<^sub>2 \<Longrightarrow> no_abs t\<^sub>2 \<Longrightarrow> P (app t\<^sub>1 t\<^sub>2)"
   shows "P t"
 using assms(1) proof (induction rule: no_abs.induct)
   case (1 t)
   show ?case
     proof (cases rule: pre_term_class.term_cases[where t = t])
       case (free name)
       then show ?thesis
         using assms by auto
     next
       case (const name)
       then show ?thesis
         using assms by auto
     next
       case (app u\<^sub>1 u\<^sub>2)
       with assms have "P u\<^sub>1" "P u\<^sub>2"
         using 1 by auto
       with assms \<open>no_abs t\<close> show ?thesis
         unfolding \<open>t = _\<close> by auto
     next
       case other
       then show ?thesis
         using \<open>no_abs t\<close>
         apply (subst (asm) no_abs.simps)
         apply (subst (asm) term_cases_def)
         by simp
     qed
 qed
 
 lemma no_abs_cases[consumes 1, cases pred: no_abs]:
   assumes "no_abs t"
   obtains (free) name where "t = free name"
         | (const) name where "t = const name"
         | (app) t\<^sub>1 t\<^sub>2 where "t = app t\<^sub>1 t\<^sub>2" "no_abs t\<^sub>1" "no_abs t\<^sub>2"
 proof (cases rule: pre_term_class.term_cases[where t = t])
   case (app u\<^sub>1 u\<^sub>2)
   show ?thesis
     apply (rule that(3))
     apply fact
     using \<open>no_abs t\<close> unfolding \<open>t = _\<close> by auto
 next
   case other
   then have False
     using \<open>no_abs t\<close>
     apply (subst (asm) no_abs.simps)
     by (auto simp: term_cases_def)
   then show ?thesis ..
 qed
 
 definition is_abs :: "'a::term \<Rightarrow> bool" where
 "is_abs t = term_cases (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_ _. False) True t"
 
 lemmas is_abs_simps[simp] = term_cases_template[OF is_abs_def]
 
 definition abs_ish :: "term list \<Rightarrow> 'a::term \<Rightarrow> bool" where
 "abs_ish pats rhs \<longleftrightarrow> pats \<noteq> [] \<or> is_abs rhs"
 
 locale simple_syntactic_and =
   fixes P :: "'a::term \<Rightarrow> bool"
   assumes app: "P (app t u) \<longleftrightarrow> P t \<and> P u"
 begin
 
 context
   notes app[simp]
 begin
 
 lemma list_comb: "P (list_comb f xs) \<longleftrightarrow> P f \<and> list_all P xs"
 by (induction xs arbitrary: f) auto
 
 corollary list_combE:
   assumes "P (list_comb f xs)"
   shows "P f" "x \<in> set xs \<Longrightarrow> P x"
 using assms
 by (auto simp: list_comb list_all_iff)
 
 lemma match:
   assumes "match pat t = Some env" "P t"
   shows "fmpred (\<lambda>_. P) env"
 using assms
 by (induction pat t env rule: match_some_induct) auto
 
 lemma matchs:
   assumes "matchs pats ts = Some env" "list_all P ts"
   shows "fmpred (\<lambda>_. P) env"
 using assms
 by (induction pats ts arbitrary: env rule: matchs.induct) (auto elim!: option_bindE intro: match)
 
 end
 
 end
 
 locale subst_syntactic_and = simple_syntactic_and +
   assumes subst: "P t \<Longrightarrow> fmpred (\<lambda>_. P) env \<Longrightarrow> P (subst t env)"
 begin
 
 lemma rewrite_step:
   assumes "(lhs, rhs) \<turnstile> t \<rightarrow> t'" "P t" "P rhs"
   shows "P t'"
 using assms by (auto intro: match subst)
 
 end
 
 locale simple_syntactic_or =
   fixes P :: "'a::term \<Rightarrow> bool"
   assumes app: "P (app t u) \<longleftrightarrow> P t \<or> P u"
 begin
 
 context
   notes app[simp]
 begin
 
 lemma list_comb: "P (list_comb f xs) \<longleftrightarrow> P f \<or> list_ex P xs"
 by (induction xs arbitrary: f) auto
 
 lemma match:
   assumes "match pat t = Some env" "\<not> P t"
   shows "fmpred (\<lambda>_ t. \<not> P t) env"
 using assms
 by (induction pat t env rule: match_some_induct) auto
 
 end
 
 sublocale neg: simple_syntactic_and "\<lambda>t. \<not> P t"
 by standard (auto simp: app)
 
 end
 
 global_interpretation no_abs: simple_syntactic_and no_abs
 by standard simp
 
 global_interpretation closed: simple_syntactic_and "\<lambda>t. closed_except t S" for S
 by standard (simp add: closed_except_def)
 
 global_interpretation closed: subst_syntactic_and closed
 by standard (rule subst_closed_preserved)
 
 corollary closed_list_comb: "closed (name $$ args) \<longleftrightarrow> list_all closed args"
 by (simp add: closed.list_comb)
 
 locale term_struct_rel =
   fixes P :: "'a::term \<Rightarrow> 'b::term \<Rightarrow> bool"
   assumes P_t_const: "P t (const name) \<Longrightarrow> t = const name"
   assumes P_const_const: "P (const name) (const name)"
   assumes P_t_app: "P t (app u\<^sub>1 u\<^sub>2) \<Longrightarrow> \<exists>t\<^sub>1 t\<^sub>2. t = app t\<^sub>1 t\<^sub>2 \<and> P t\<^sub>1 u\<^sub>1 \<and> P t\<^sub>2 u\<^sub>2"
   assumes P_app_app: "P t\<^sub>1 u\<^sub>1 \<Longrightarrow> P t\<^sub>2 u\<^sub>2 \<Longrightarrow> P (app t\<^sub>1 t\<^sub>2) (app u\<^sub>1 u\<^sub>2)"
 begin
 
 abbreviation P_env :: "('k, 'a) fmap \<Rightarrow> ('k, 'b) fmap \<Rightarrow> bool" where
 "P_env \<equiv> fmrel P"
 
 lemma related_match:
   assumes "match x u = Some env" "P t u"
   obtains env' where "match x t = Some env'" "P_env env' env"
 using assms proof (induction x u env arbitrary: t thesis rule: match_some_induct)
   case (app v\<^sub>1 v\<^sub>2 w\<^sub>1 w\<^sub>2 env\<^sub>1 env\<^sub>2)
   obtain u\<^sub>1 u\<^sub>2 where "t = app u\<^sub>1 u\<^sub>2" "P u\<^sub>1 w\<^sub>1" "P u\<^sub>2 w\<^sub>2"
     using P_t_app[OF \<open>P t (app w\<^sub>1 w\<^sub>2)\<close>] by auto
   with app obtain env\<^sub>1' env\<^sub>2'
     where "match v\<^sub>1 u\<^sub>1 = Some env\<^sub>1'" "P_env env\<^sub>1' env\<^sub>1"
       and "match v\<^sub>2 u\<^sub>2 = Some env\<^sub>2'" "P_env env\<^sub>2' env\<^sub>2"
     by metis
   hence "match (v\<^sub>1 $ v\<^sub>2) (app u\<^sub>1 u\<^sub>2) = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')"
     by simp
 
   show ?case
     proof (rule app.prems)
       show "match (v\<^sub>1 $ v\<^sub>2) t = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')"
         unfolding \<open>t = _\<close> by fact
     next
       show "P_env (env\<^sub>1' ++\<^sub>f env\<^sub>2') (env\<^sub>1 ++\<^sub>f env\<^sub>2)"
         by rule fact+
     qed
 qed (auto split: option.splits if_splits dest: P_t_const)
 
 lemma list_combI:
   assumes "list_all2 P us\<^sub>1 us\<^sub>2" "P t\<^sub>1 t\<^sub>2"
   shows "P (list_comb t\<^sub>1 us\<^sub>1) (list_comb t\<^sub>2 us\<^sub>2)"
 using assms
 by (induction arbitrary: t\<^sub>1 t\<^sub>2 rule: list.rel_induct) (auto intro: P_app_app)
 
 lemma list_combE:
   assumes "P t (name $$ args)"
   obtains args' where "t = name $$ args'" "list_all2 P args' args"
 using assms proof (induction args arbitrary: t thesis rule: rev_induct)
   case Nil
   hence "P t (const name)"
     by simp
   hence "t = const name"
     using P_t_const by auto
   with Nil show ?case
     by simp
 next
   case (snoc x xs)
   hence "P t (app (name $$ xs) x)"
     by simp
   obtain t' y where "t = app t' y" "P t' (name $$ xs)" "P y x"
     using P_t_app[OF \<open>P t (app (name $$ xs) x)\<close>] by auto
   with snoc obtain ys where "t' = name $$ ys" "list_all2 P ys xs"
     by blast
   show ?case
     proof (rule snoc.prems)
       show "t = name $$ (ys @ [y])"
         unfolding \<open>t = app t' y\<close> \<open>t' = name $$ ys\<close>
         by simp
     next
       have "list_all2 P [y] [x]"
         using \<open>P y x\<close> by simp
       thus "list_all2 P (ys @ [y]) (xs @ [x])"
         using \<open>list_all2 P ys xs\<close>
         by (metis list_all2_appendI)
     qed
 qed
 
 end
 
 locale term_struct_rel_strong = term_struct_rel +
   assumes P_const_t: "P (const name) t \<Longrightarrow> t = const name"
   assumes P_app_t: "P (app u\<^sub>1 u\<^sub>2) t \<Longrightarrow> \<exists>t\<^sub>1 t\<^sub>2. t = app t\<^sub>1 t\<^sub>2 \<and> P u\<^sub>1 t\<^sub>1 \<and> P u\<^sub>2 t\<^sub>2"
 begin
 
 lemma unconst_rel: "P t u \<Longrightarrow> unconst t = unconst u"
 by (metis P_const_t P_t_const const_name_simps(2) is_const_def unconst_const)
 
 lemma unapp_rel: "P t u \<Longrightarrow> rel_option (rel_prod P P) (unapp t) (unapp u)"
 by (smt P_app_t P_t_app is_app_def left_right_simps(3) option.rel_sel option.sel option.simps(3) rel_prod_inject unapp_app)
 
 lemma match_rel:
   assumes "P t u"
   shows "rel_option P_env (match p t) (match p u)"
 using assms proof (induction p arbitrary: t u)
   case (Const name)
   thus ?case
     by (auto split: option.splits simp: unconst_rel)
 next
   case (App p1 p2)
   hence "rel_option (rel_prod P P) (unapp t) (unapp u)"
     by (metis unapp_rel)
   thus ?case
     using App
     by cases (auto split: option.splits intro!: rel_option_bind)
 qed auto
 
 lemma find_match_rel:
   assumes "list_all2 (rel_prod (=) P) cs cs'" "P t t'"
   shows "rel_option (rel_prod P_env (rel_prod (=) P)) (find_match cs t) (find_match cs' t')"
 using assms proof induction
   case (Cons x xs y ys)
   moreover obtain px tx py ty where "x = (px, tx)" "y = (py, ty)"
     by (cases x, cases y) auto
   moreover note match_rel[OF Cons(4), where p = px]
   ultimately show ?case
     by (auto elim: option.rel_cases)
 qed auto
 
 end
 
 fun convert_term :: "'a::term \<Rightarrow> 'b::term" where
 [simp del]: "convert_term t = term_cases const free (\<lambda>t u. app (convert_term t) (convert_term u)) undefined t"
 
 lemmas convert_term_simps[simp] = term_cases_template[OF convert_term.simps]
 
 lemma convert_term_id:
   assumes "no_abs t"
   shows "convert_term t = t"
 using assms by induction auto
 
 lemma convert_term_no_abs:
   assumes "no_abs t"
   shows "no_abs (convert_term t)"
 using assms by induction auto
 
 lemma convert_term_inj:
   assumes "no_abs t" "no_abs t'" "convert_term t = convert_term t'"
   shows "t = t'"
 using assms proof (induction t arbitrary: t')
   case (free name)
   then show ?case
     by cases (auto dest: term_inject)
 next
   case (const name)
   then show ?case
     by cases (auto dest: term_inject)
 next
   case (app t\<^sub>1 t\<^sub>2)
   from \<open>no_abs t'\<close> show ?case
     apply cases
     using app by (auto dest: term_inject)
 qed
 
 lemma convert_term_idem:
   assumes "no_abs t"
   shows "convert_term (convert_term t) = convert_term t"
 using assms by (induction t) auto
 
 lemma convert_term_frees[simp]:
   assumes "no_abs t"
   shows "frees (convert_term t) = frees t"
 using assms by induction auto
 
 lemma convert_term_consts[simp]:
   assumes "no_abs t"
   shows "consts (convert_term t) = consts t"
 using assms by induction auto
 
 text \<open>
   The following lemma does not generalize to when @{prop \<open>match t u = None\<close>}. Assume matching
   return @{const None}, because the pattern is an application and the object is a term satisfying
   @{const is_abs}. Now, @{const convert_term} applied to the object will produce @{const undefined}.
   Of course we don't know anything about that and whether or not that matches. A workaround would
   be to require implementations of @{class term} to prove @{prop \<open>\<exists>t. is_abs t\<close>}, such that
   @{const convert_term} could use that instead of @{const undefined}. This seems to be too much of a
   special case in order to be useful.
 \<close>
 
 lemma convert_term_match:
   assumes "match t u = Some env"
   shows "match t (convert_term u) = Some (fmmap convert_term env)"
 using assms by (induction t u env rule: match_some_induct) auto
 
 section \<open>Related work\<close>
 
 text \<open>
-  Schmidt-Schauß and Siekmann @{cite schmidt1988unification} discuss the concept of
+  Schmidt-Schau{\ss} and Siekmann @{cite schmidt1988unification} discuss the concept of
   \<^emph>\<open>unification algebras\<close>. They generalize terms to \<^emph>\<open>objects\<close> and substitutions to \<^emph>\<open>mappings\<close>.
   A unification problem can be rephrased to finding a mapping such that a set of objects are mapped
   to the same object. The advantage of this generalization is that other -- superficially unrelated
   -- problems like solving algebraic equations or querying logic programs can be seen as unification
   problems.
 
   In particular, the authors note that among the similarities of such problems are that ``objects
   [have] variables'' whose ``names do not matter'' and ``there exists an operation like substituting
   objects into variables''. The major difference between this formalization and their work is that I
   use concrete types for variables and mappings. Otherwise, some similarities to here can be found.
 
   Eder @{cite eder1985properties} discusses properties of substitutions with a special focus on a
   partial ordering between substitutions. However, Eder constructs and uses a concrete type of
   first-order terms, similarly to Sternagel and Thiemann @{cite sternagel2018terms}.
 
   Williams @{cite williams1991instantiation} defines substitutions as elements in a monoid.
   In this setting, instantiations can be represented as \<^emph>\<open>monoid actions\<close>. Williams then proceeds to
   define -- for arbitrary sets of terms and variables -- the notion of \<^emph>\<open>instantiation systems,\<close>
-  heavily drawing on notation from Schmidt-Schauß and Siekmann. Some of the presented axioms
+  heavily drawing on notation from Schmidt-Schau{\ss} and Siekmann. Some of the presented axioms
   are also present in this formalization, as are some theorems that have a direct correspondence.
 \<close>
 
 end
\ No newline at end of file
diff --git a/thys/Minkowskis_Theorem/Minkowskis_Theorem.thy b/thys/Minkowskis_Theorem/Minkowskis_Theorem.thy
--- a/thys/Minkowskis_Theorem/Minkowskis_Theorem.thy
+++ b/thys/Minkowskis_Theorem/Minkowskis_Theorem.thy
@@ -1,526 +1,526 @@
 (*
   File:    Minkowskis_Theorem.thy
   Author:  Manuel Eberl <eberlm@in.tum.de>
 
   A proof of Blichfeldt's and Minkowski's theorem about the relation between
   subsets of the Euclidean space, the Lebesgue measure, and the integer lattice.
 *)
 section \<open>Minkowski's theorem\<close>
 theory Minkowskis_Theorem
   imports "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
 begin
 
 (* Could be generalised to arbitrary euclidean spaces and full-dimensional lattices *)
 
 subsection \<open>Miscellaneous material\<close>
 
 lemma bij_betw_UN:
   assumes "bij_betw f A B"
   shows   "(\<Union>n\<in>A. g (f n)) = (\<Union>n\<in>B. g n)"
   using assms by (auto simp: bij_betw_def)
 
 definition of_int_vec where
   "of_int_vec v = (\<chi> i. of_int (v $ i))"
 
 lemma of_int_vec_nth [simp]: "of_int_vec v $ n = of_int (v $ n)"
   by (simp add: of_int_vec_def)
 
 lemma of_int_vec_eq_iff [simp]:
   "(of_int_vec a :: ('a :: ring_char_0) ^ 'n) = of_int_vec b \<longleftrightarrow> a = b"
   by (simp add: of_int_vec_def vec_eq_iff)
 
 lemma inj_axis:
   assumes "c \<noteq> 0"
   shows   "inj (\<lambda>k. axis k c :: ('a :: {zero}) ^ 'n)"
 proof
   fix x y :: 'n
   assume *: "axis x c = axis y c"
   have "axis x c $ x = axis x c $ y"
     by (subst *) simp
   thus "x = y" using assms
     by (auto simp: axis_def split: if_splits)
 qed
 
 lemma compactD:
   assumes "compact (A :: 'a :: metric_space set)" "range f \<subseteq> A"
   shows   "\<exists>h l. strict_mono (h::nat\<Rightarrow>nat) \<and> (f \<circ> h) \<longlonglongrightarrow> l"
   using assms unfolding compact_def by blast
 
 lemma closed_lattice:
   fixes A :: "(real ^ 'n) set"
   assumes "\<And>v i. v \<in> A \<Longrightarrow> v $ i \<in> \<int>"
   shows   "closed A"
 proof (rule discrete_imp_closed[OF zero_less_one], safe, goal_cases)
   case (1 x y)
   have "x $ i = y $ i" for i
   proof -
     from 1 and assms have "x $ i - y $ i \<in> \<int>"
       by auto
     then obtain m where m: "of_int m = (x $ i - y $ i)"
       by (elim Ints_cases) auto
     hence "of_int (abs m) = abs ((x - y) $ i)"
       by simp
     also have "\<dots> \<le> norm (x - y)"
       by (rule component_le_norm_cart)
     also have "\<dots> < of_int 1"
       using 1 by (simp add: dist_norm norm_minus_commute)
     finally have "abs m < 1"
       by (subst (asm) of_int_less_iff)
     thus "x $ i = y $ i"
       using m by simp
   qed
   thus "y = x"
     by (simp add: vec_eq_iff)
 qed
 
 
 subsection \<open>Auxiliary theorems about measure theory\<close>
 
 lemma emeasure_lborel_cbox_eq':
   "emeasure lborel (cbox a b) = ennreal (\<Prod>e\<in>Basis. max 0 ((b - a) \<bullet> e))"
 proof (cases "\<forall>ba\<in>Basis. a \<bullet> ba \<le> b \<bullet> ba")
   case True
   hence "emeasure lborel (cbox a b) = ennreal (prod ((\<bullet>) (b - a)) Basis)"
     unfolding emeasure_lborel_cbox_eq by auto
   also have "prod ((\<bullet>) (b - a)) Basis = (\<Prod>e\<in>Basis. max 0 ((b - a) \<bullet> e))"
     using True by (intro prod.cong refl) (auto simp: max_def inner_simps)
   finally show ?thesis .
 next
   case False
   hence "emeasure lborel (cbox a b) = ennreal 0"
     by (auto simp: emeasure_lborel_cbox_eq)
   also from False have "0 = (\<Prod>e\<in>Basis. max 0 ((b - a) \<bullet> e))"
     by (auto simp: max_def inner_simps)
   finally show ?thesis .
 qed
 
 lemma emeasure_lborel_cbox_cart_eq:
   fixes a b :: "real ^ ('n :: finite)"
   shows "emeasure lborel (cbox a b) = ennreal (\<Prod>i \<in> UNIV. max 0 ((b - a) $ i))"
 proof -
   have "emeasure lborel (cbox a b) = ennreal (\<Prod>e\<in>Basis. max 0 ((b - a) \<bullet> e))"
     unfolding emeasure_lborel_cbox_eq' ..
   also have "(Basis :: (real ^ 'n) set) = range (\<lambda>k. axis k 1)"
     unfolding Basis_vec_def by auto
   also have "(\<Prod>e\<in>\<dots>. max 0 ((b - a) \<bullet> e)) = (\<Prod> i \<in> UNIV . max 0 ((b - a) $ i))"
     by (subst prod.reindex) (auto intro!: inj_axis simp: algebra_simps inner_axis)
   finally show ?thesis .
 qed
 
 lemma sum_emeasure':
   assumes [simp]: "finite A"
   assumes [measurable]: "\<And>x. x \<in> A \<Longrightarrow> B x \<in> sets M"
   assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> emeasure M (B x \<inter> B y) = 0"
   shows   "(\<Sum>x\<in>A. emeasure M (B x)) = emeasure M (\<Union>x\<in>A. B x)"
 proof -
   define C where "C = (\<Union>x\<in>A. \<Union>y\<in>(A-{x}). B x \<inter> B y)"
   have C: "C \<in> null_sets M"
     unfolding C_def using assms
     by (intro null_sets.finite_UN) (auto simp: null_sets_def)
   hence [measurable]: "C \<in> sets M" and [simp]: "emeasure M C = 0"
     by (simp_all add: null_sets_def)
   have "(\<Union>x\<in>A. B x) = (\<Union>x\<in>A. B x - C) \<union> C"
     by (auto simp: C_def)
   also have "emeasure M \<dots> = emeasure M (\<Union>x\<in>A. B x - C)"
     by (subst emeasure_Un_null_set) (auto intro!: sets.Un sets.Diff)
   also from assms have "\<dots> = (\<Sum>x\<in>A. emeasure M (B x - C))"
     by (subst sum_emeasure)
        (auto simp: disjoint_family_on_def C_def intro!: sets.Diff sets.finite_UN)
   also have "\<dots> = (\<Sum>x\<in>A. emeasure M (B x))"
     by (intro sum.cong refl emeasure_Diff_null_set) auto
   finally show ?thesis ..
 qed
 
 lemma sums_emeasure':
   assumes [measurable]: "\<And>x. B x \<in> sets M"
   assumes "\<And>x y. x \<noteq> y \<Longrightarrow> emeasure M (B x \<inter> B y) = 0"
   shows   "(\<lambda>x. emeasure M (B x)) sums emeasure M (\<Union>x. B x)"
 proof -
   define C where "C = (\<Union>x. \<Union>y\<in>-{x}. B x \<inter> B y)"
   have C: "C \<in> null_sets M"
     unfolding C_def using assms
     by (intro null_sets_UN') (auto simp: null_sets_def)
   hence [measurable]: "C \<in> sets M" and [simp]: "emeasure M C = 0"
     by (simp_all add: null_sets_def)
   have "(\<Union>x. B x) = (\<Union>x. B x - C) \<union> C"
     by (auto simp: C_def)
   also have "emeasure M \<dots> = emeasure M (\<Union>x. B x - C)"
     by (subst emeasure_Un_null_set) (auto intro!: sets.Un sets.Diff)
   also from assms have "(\<lambda>x. emeasure M (B x - C)) sums \<dots>  "
     by (intro sums_emeasure)
        (auto simp: disjoint_family_on_def C_def intro!: sets.Diff sets.finite_UN)
   also have "(\<lambda>x. emeasure M (B x - C)) = (\<lambda>x. emeasure M (B x))"
     by (intro ext emeasure_Diff_null_set) auto
   finally show ?thesis .
 qed
 
 
 subsection \<open>Blichfeldt's theorem\<close>
 
 text \<open>
   Blichfeldt's theorem states that, given a subset of $\mathbb{R}^n$ with $n > 0$ and a
   volume of more than 1, there exist two different points in that set whose difference
   vector has integer components.
 
   This will be the key ingredient in proving Minkowski's theorem.
 
   Note that in the HOL Light version, it is additionally required -- both for
   Blichfeldt's theorem and for Minkowski's theorem -- that the set is bounded,
   which we do not need.
 \<close>
 proposition blichfeldt:
   fixes S :: "(real ^ 'n) set"
   assumes [measurable]: "S \<in> sets lebesgue"
   assumes "emeasure lebesgue S > 1"
   obtains x y where "x \<noteq> y" and "x \<in> S" and "y \<in> S" and "\<And>i. (x - y) $ i \<in> \<int>"
 proof -
   \<comment> \<open>We define for each lattice point in $\mathbb{Z}^n$ the corresponding cell in $\mathbb{R}^n$.\<close>
   define R :: "int ^ 'n \<Rightarrow> (real ^ 'n) set"
     where "R = (\<lambda>a. cbox (of_int_vec a) (of_int_vec (a + 1)))"
 
   \<comment> \<open>For each lattice point, we can intersect the cell it defines with our set @{term S}
       to obtain a partitioning of @{term S}.\<close>
   define T :: "int ^ 'n \<Rightarrow> (real ^ 'n) set"
     where "T = (\<lambda>a. S \<inter> R a)"
 
   \<comment> \<open>We can then translate each such partition into the cell at the origin, i.\,e. the
       unit box @{term "R 0"}.\<close>
   define T' :: "int ^ 'n \<Rightarrow> (real ^ 'n) set"
     where "T' = (\<lambda>a. (\<lambda>x. x - of_int_vec a) ` T a)"
   have T'_altdef: "T' a = (\<lambda>x. x + of_int_vec a) -` T a" for a
     unfolding T'_def by force
 
   \<comment> \<open>We need to show measurability of all the defined sets.\<close>
   have [measurable, simp]: "R a \<in> sets lebesgue" for a
     unfolding R_def by simp
   have [measurable, simp]: "T a \<in> sets lebesgue" for a
     unfolding T_def by auto
   have "(\<lambda>x::real^'n. x + of_int_vec a) \<in> lebesgue \<rightarrow>\<^sub>M lebesgue" for a
     using lebesgue_affine_measurable[of "\<lambda>_. 1" "of_int_vec a"]
     by (auto simp: euclidean_representation add_ac)
   from measurable_sets[OF this, of "T a" a for a]
     have [measurable, simp]: "T' a \<in> sets lebesgue" for a
       unfolding T'_altdef by simp
 
   \<comment> \<open>Obviously, the original set @{term S} is the union of all the lattice
       point cell partitions.\<close>
   have S_decompose: "S = (\<Union>a. T a)" unfolding T_def
   proof safe
     fix x assume x: "x \<in> S"
     define a where "a = (\<chi> i. \<lfloor>x $ i\<rfloor>)"
     have "x \<in> R a"
       unfolding R_def
       by (auto simp: cbox_interval less_eq_vec_def of_int_vec_def a_def)
     with x show "x \<in> (\<Union>a. S \<inter> R a)" by auto
   qed
 
   \<comment> \<open>Translating the partitioned subsets does not change their volume.\<close>
   have emeasure_T': "emeasure lebesgue (T' a) = emeasure lebesgue (T a)" for a
   proof -
     have "T' a = (\<lambda>x. 1 *\<^sub>R x + (- of_int_vec a)) ` T a"
       by (simp add: T'_def)
     also have "emeasure lebesgue \<dots> = emeasure lebesgue (T a)"
       by (subst emeasure_lebesgue_affine) auto
     finally show ?thesis
       by simp
   qed
 
   \<comment> \<open>Each translated partition of @{term S} is a subset of the unit cell at the origin.\<close>
   have T'_subset: "T' a \<subseteq> cbox 0 1" for a
     unfolding T'_def T_def R_def
     by (auto simp: algebra_simps cbox_interval of_int_vec_def less_eq_vec_def)
 
   \<comment> \<open>It is clear that the intersection of two different lattice point cells is a null set.\<close>
   have R_Int: "R a \<inter> R b \<in> null_sets lebesgue" if "a \<noteq> b" for a b
   proof -
     from that obtain i where i: "a $ i \<noteq> b $ i"
       by (auto simp: vec_eq_iff)
     have "R a \<inter> R b = cbox (\<chi> i. max (a $ i) (b $ i)) (\<chi> i. min (a $ i + 1) (b $ i + 1))"
       unfolding Int_interval_cart R_def interval_cbox
       by (simp add: of_int_vec_def max_def min_def if_distrib cong: if_cong)
     hence "emeasure lebesgue (R a \<inter> R b) = emeasure lborel \<dots>"
       by simp
     also have "\<dots> = ennreal (\<Prod>i\<in>UNIV. max 0 (((\<chi> x. real_of_int (min (a $ x + 1) (b $ x + 1))) -
                                   (\<chi> x. real_of_int (max (a $ x) (b $ x)))) $ i))"
       (is "_ = ennreal ?P")
       unfolding emeasure_lborel_cbox_cart_eq by simp
     also have "?P = 0"
       using i by (auto simp: max_def intro!: exI[of _ i])
     finally show ?thesis
       by (auto simp: null_sets_def R_def)
   qed
 
   \<comment> \<open>Therefore, the intersection of two lattice point cell partitionings of @{term S} is
       also a null set.\<close>
   have T_Int: "T a \<inter> T b \<in> null_sets lebesgue" if "a \<noteq> b" for a b
   proof -
     have "T a \<inter> T b = (R a \<inter> R b) \<inter> S"
       by (auto simp: T_def)
     also have "\<dots> \<in> null_sets lebesgue"
       by (rule null_set_Int2) (insert that, auto intro: R_Int assms)
     finally show ?thesis .
   qed
   have emeasure_T_Int: "emeasure lebesgue (T a \<inter> T b) = 0" if "a \<noteq> b" for a b
     using T_Int[OF that] unfolding null_sets_def by blast
 
   \<comment> \<open>The set of lattice points $\mathbb{Z}^n$ is countably infinite, so there exists
       a bijection $f: \mathbb{N} \to \mathbb{Z}^n$. We need this for summing over all
       lattice points.\<close>
   define f :: "nat \<Rightarrow> int ^ 'n" where "f = from_nat_into UNIV"
   have "countable (UNIV :: (int ^ 'n) set)" "infinite (UNIV :: (int ^ 'n) set)"
     using infinite_UNIV_char_0 by simp_all
   from bij_betw_from_nat_into [OF this] have f: "bij f"
     by (simp add: f_def)
 
   \<comment> \<open>Suppose all the translated cell partitions @{term T'} are disjoint.\<close>
   {
     assume disjoint: "\<And>a b. a \<noteq> b \<Longrightarrow> T' a \<inter> T' b = {}"
     \<comment> \<open>We know by assumption that the volume of @{term S} is greater than 1.\<close>
     have "1 < emeasure lebesgue S" by fact
     also have "emeasure lebesgue S = emeasure lebesgue (\<Union>n. T' (f n))"
     proof -
       \<comment> \<open>The sum of the volumes of all the @{term T'} is precisely the volume
           of their union, which is @{term "S"}.\<close>
       have "S = (\<Union>a. T a)" by (rule S_decompose)
       also have "\<dots> = (\<Union>n. T (f n))"
         by (rule bij_betw_UN [OF f, symmetric])
       also have "(\<lambda>n. emeasure lebesgue (T (f n))) sums emeasure lebesgue \<dots>"
         by (intro sums_emeasure' emeasure_T_Int) (insert f, auto simp: bij_betw_def inj_on_def)
       also have "(\<lambda>n. emeasure lebesgue (T (f n))) = (\<lambda>n. emeasure lebesgue (T' (f n)))"
         by (simp add: emeasure_T')
       finally have "(\<lambda>n. emeasure lebesgue (T' (f n))) sums emeasure lebesgue S" .
       moreover have "(\<lambda>n. emeasure lebesgue (T' (f n))) sums emeasure lebesgue (\<Union>n. T' (f n))"
         using disjoint by (intro sums_emeasure)
                           (insert f, auto simp: disjoint_family_on_def bij_betw_def inj_on_def)
       ultimately show ?thesis
         by (auto simp: sums_iff)
     qed
     \<comment> \<open>On the other hand, all the translated partitions lie in the unit cell
         @{term "cbox (0 :: real ^ 'n) 1"}, so their combined volume cannot be
         greater than 1.\<close>
     also have "emeasure lebesgue (\<Union>n. T' (f n)) \<le> emeasure lebesgue (cbox 0 (1 :: real ^ 'n))"
       using T'_subset by (intro emeasure_mono) auto
     also have "\<dots> = 1"
       by (simp add: emeasure_lborel_cbox_cart_eq)
     \<comment> \<open>This leads to a contradiction.\<close>
     finally have False by simp
   }
   \<comment> \<open>Therefore, there exists a point that lies in two different translated partitions,
       which obviously corresponds two two points in the non-translated partitions
       whose difference is the difference between two lattice points and therefore
       has integer components.\<close>
   then obtain a b x where "a \<noteq> b" "x \<in> T' a" "x \<in> T' b"
     by auto
   thus ?thesis
     by (intro that[of "x + of_int_vec a" "x + of_int_vec b"])
        (auto simp: T'_def T_def algebra_simps)
 qed
 
 
 subsection \<open>Minkowski's theorem\<close>
 
 text \<open>
   Minkowski's theorem now states that, given a convex subset of $\mathbb{R}^n$ that is
   symmetric around the origin and has a volume greater than $2^n$, that set must contain
   a non-zero point with integer coordinates.
 \<close>
 theorem minkowski:
   fixes B :: "(real ^ 'n) set"
   assumes "convex B" and symmetric: "uminus ` B \<subseteq> B"
   assumes meas_B [measurable]: "B \<in> sets lebesgue"
   assumes measure_B: "emeasure lebesgue B > 2 ^ CARD('n)"
   obtains x where "x \<in> B" and "x \<noteq> 0" and "\<And>i. x $ i \<in> \<int>"
 proof -
   \<comment> \<open>We scale @{term B} with $\frac{1}{2}$.\<close>
   define B' where "B' = (\<lambda>x. 2 *\<^sub>R x) -` B"
   have meas_B' [measurable]: "B' \<in> sets lebesgue"
     using measurable_sets[OF lebesgue_measurable_scaling[of 2] meas_B]
     by (simp add: B'_def)
   have B'_altdef: "B' = (\<lambda>x. (1/2) *\<^sub>R x) ` B"
     unfolding B'_def by force
 
   \<comment> \<open>The volume of the scaled set is $2^n$ times smaller than the original set, and
       therefore still has a volume greater than 1.\<close>
   have "1 < ennreal ((1 / 2) ^ CARD('n)) * emeasure lebesgue B"
   proof (cases "emeasure lebesgue B")
     case (real x)
     have "ennreal (2 ^ CARD('n)) = 2 ^ CARD('n)"
       by (subst ennreal_power [symmetric]) auto
     also from measure_B and real have "\<dots> < ennreal x" by simp
     finally have "(2 ^ CARD('n)) < x"
       by (subst (asm) ennreal_less_iff) auto
     thus ?thesis
       using real by (simp add: ennreal_1 [symmetric] ennreal_mult' [symmetric]
                        ennreal_less_iff field_simps del: ennreal_1)
   qed (simp_all add: ennreal_mult_top)
   also have "\<dots> = emeasure lebesgue B'"
     unfolding B'_altdef using emeasure_lebesgue_affine[of "1/2" 0 B] by simp
   finally have *: "emeasure lebesgue B' > 1" .
 
   \<comment> \<open>We apply Blichfeldt's theorem to get two points whose difference vector has
       integer coefficients. It only remains to show that that difference vector is
       itself a point in the original set.\<close>
   obtain x y
     where xy: "x \<noteq> y" "x \<in> B'" "y \<in> B'" "\<And>i. (x - y) $ i \<in> \<int>"
     by (erule blichfeldt [OF meas_B' *])
   hence "2 *\<^sub>R x \<in> B" "2 *\<^sub>R y \<in> B" by (auto simp: B'_def)
   \<comment> \<open>Exploiting the symmetric of @{term B}, the reflection of @{term "2 *\<^sub>R y"} is
       also in @{term B}.\<close>
   moreover from this and symmetric have "-(2 *\<^sub>R y) \<in> B" by blast
   \<comment> \<open>Since @{term B} is convex, the mid-point between @{term "2 *\<^sub>R x"} and @{term "-2 *\<^sub>R y"}
       is also in @{term B}, and that point is simply @{term "x - y"} as desired.\<close>
   ultimately have "(1 / 2) *\<^sub>R 2 *\<^sub>R x + (1 / 2) *\<^sub>R (- 2 *\<^sub>R y) \<in> B"
     using \<open>convex B\<close> by (intro convexD) auto
   also have "(1 / 2) *\<^sub>R 2 *\<^sub>R x + (1 / 2) *\<^sub>R (- 2 *\<^sub>R y) = x - y"
     by simp
   finally show ?thesis using xy
     by (intro that[of "x - y"]) auto
 qed
 
 text \<open>
   If the set in question is compact, the restriction to the volume can be weakened
   to ``at least 1'' from ``greater than 1''.
 \<close>
 theorem minkowski_compact:
   fixes B :: "(real ^ 'n) set"
   assumes "convex B" and "compact B" and symmetric: "uminus ` B \<subseteq> B"
   assumes measure_B: "emeasure lebesgue B \<ge> 2 ^ CARD('n)"
   obtains x where "x \<in> B" and "x \<noteq> 0" and "\<And>i. x $ i \<in> \<int>"
 proof (cases "emeasure lebesgue B = 2 ^ CARD('n)")
   \<comment> \<open>If the volume is greater than 1, we can just apply the theorem from before.\<close>
   case False
   with measure_B have less: "emeasure lebesgue B > 2 ^ CARD('n)"
     by simp
   from \<open>compact B\<close> have meas: "B \<in> sets lebesgue"
     by (intro sets_completionI_sets lborelD borel_closed compact_imp_closed)
   from minkowski[OF assms(1) symmetric meas less] and that
     show ?thesis by blast
 next
   case True
   \<comment> \<open>If the volume is precisely one, we look at what happens when @{term B} is
       scaled with a factor of $1 + \varepsilon$.\<close>
   define B' where "B' = (\<lambda>\<epsilon>. (*\<^sub>R) (1 + \<epsilon>) ` B)"
   from \<open>compact B\<close> have compact': "compact (B' \<epsilon>)" for \<epsilon>
     unfolding B'_def by (intro compact_scaling)
   have B'_altdef: "B' \<epsilon> = (*\<^sub>R) (inverse (1 + \<epsilon>)) -` B" if \<epsilon>: "\<epsilon> > 0" for \<epsilon>
     using \<epsilon> unfolding B'_def by force
 
   \<comment> \<open>Since the scaled sets are convex, they are stable under scaling.\<close>
   have B_scale: "a *\<^sub>R x \<in> B" if "x \<in> B" "a \<in> {0..1}" for a x
   proof -
     have "((a + 1) / 2) *\<^sub>R x + (1 - ((a + 1) / 2)) *\<^sub>R (-x) \<in> B"
       using that and \<open>convex B\<close> and symmetric by (intro convexD) auto
     also have "((a + 1) / 2) *\<^sub>R x + (1 - ((a + 1) / 2)) *\<^sub>R (-x) =
                  (1 + a) *\<^sub>R ((1/2) *\<^sub>R (x + x)) - x"
       by (simp add: algebra_simps del: scaleR_half_double)
     also have "\<dots> = a *\<^sub>R x"
       by (subst scaleR_half_double) (simp add: algebra_simps)
     finally show "\<dots> \<in> B" .
   qed
 
   \<comment> \<open>This means that @{term B'} is monotonic.\<close>
   have B'_subset: "B' a \<subseteq> B' b" if "0 \<le> a" "a \<le> b" for a b
   proof
     fix x assume "x \<in> B' a"
     then obtain y where "x = (1 + a) *\<^sub>R y" "y \<in> B"
       by (auto simp: B'_def)
     moreover then have "(inverse (1 + b) * (1 + a)) *\<^sub>R y \<in> B"
       using that by (intro B_scale) (auto simp: field_simps)
     ultimately show "x \<in> B' b"
       using that by (force simp: B'_def)
   qed
 
   \<comment> \<open>We obtain some upper bound on the norm of @{term B}.\<close>
   from \<open>compact B\<close> have "bounded B"
     by (rule compact_imp_bounded)
   then obtain C where C: "norm x \<le> C" if "x \<in> B" for x
     unfolding bounded_iff by blast
 
   \<comment> \<open>We can then bound the distance of any point in a scaled set to the original set.\<close>
   have setdist_le: "setdist {x} B \<le> \<epsilon> * C" if "x \<in> B' \<epsilon>" and "\<epsilon> \<ge> 0" for x \<epsilon>
   proof -
     from that obtain y where y: "y \<in> B" and [simp]: "x = (1 + \<epsilon>) *\<^sub>R y"
       by (auto simp: B'_def)
     from y have "setdist {x} B \<le> dist x y"
       by (intro setdist_le_dist) auto
     also from that have "dist x y = \<epsilon> * norm y"
       by (simp add: dist_norm algebra_simps)
     also from y have "norm y \<le> C"
       by (rule C)
     finally show "setdist {x} B \<le> \<epsilon> * C"
       using that by (simp add: mult_left_mono)
   qed
 
   \<comment> \<open>By applying the standard Minkowski theorem to the a scaled set, we can see that
       any scaled set contains a non-zero point with integer coordinates.\<close>
   have "\<exists>v. v \<in> B' \<epsilon> - {0} \<and> (\<forall>i. v $ i \<in> \<int>)" if \<epsilon>: "\<epsilon> > 0" for \<epsilon>
   proof -
     from \<open>convex B\<close> have convex': "convex (B' \<epsilon>)"
       unfolding B'_def by (rule convex_scaling)
     from \<open>compact B\<close> have meas: "B' \<epsilon> \<in> sets lebesgue" unfolding B'_def
       by (intro sets_completionI_sets lborelD borel_closed compact_imp_closed compact_scaling)
     from symmetric have symmetric': "uminus ` B' \<epsilon> \<subseteq> B' \<epsilon>"
       by (auto simp: B'_altdef[OF \<epsilon>])
 
     have "2 ^ CARD('n) = ennreal (2 ^ CARD('n))"
       by (subst ennreal_power [symmetric]) auto
     hence "1 * emeasure lebesgue B < ennreal ((1 + \<epsilon>) ^ CARD('n)) * emeasure lebesgue B"
       using True and \<epsilon> by (intro ennreal_mult_strict_right_mono) (auto)
     also have "\<dots> = emeasure lebesgue (B' \<epsilon>)"
       using emeasure_lebesgue_affine[of "1+\<epsilon>" 0 B] and \<epsilon> by (simp add: B'_def)
     finally have measure_B': "emeasure lebesgue (B' \<epsilon>) > 2 ^ CARD('n)"
       using True by simp
    
     obtain v where "v \<in> B' \<epsilon>" "v \<noteq> 0" "\<And>i. v $ i \<in> \<int>"
       by (erule minkowski[OF convex' symmetric' meas measure_B'])
     thus ?thesis
       by blast
   qed
   hence "\<forall>n. \<exists>v. v \<in> B' (1/Suc n) - {0} \<and> (\<forall>i. v $ i \<in> \<int>)"
     by auto
   \<comment> \<open>In particular, this means we can choose some sequence tending to zero
       -- say $\frac{1}{n+1}$ -- and always find a lattice point in the scaled set.\<close>
   hence "\<exists>v. \<forall>n. v n \<in> B' (1/Suc n) - {0} \<and> (\<forall>i. v n $ i \<in> \<int>)"
     by (subst (asm) choice_iff)
   then obtain v where v: "v n \<in> B' (1/Suc n) - {0}" "v n $ i \<in> \<int>" for i n
     by blast
 
-  \<comment> \<open>By the Bolzano--Weierstraß theorem, there exists a convergent subsequence of @{term v}.\<close>
+  \<comment> \<open>By the Bolzano--Weierstra{\ss} theorem, there exists a convergent subsequence of @{term v}.\<close>
   have "\<exists>h l. strict_mono (h::nat\<Rightarrow>nat) \<and> (v \<circ> h) \<longlonglongrightarrow> l"
   proof (rule compactD)
     show "compact (B' 1)" by (rule compact')
     show "range v \<subseteq> B' 1"
       using B'_subset[of "1/Suc n" 1 for n] and v by auto
   qed
   then obtain h l where h: "strict_mono h" and l: "(v \<circ> h) \<longlonglongrightarrow> l"
     by blast
 
   \<comment> \<open>Since the convergent subsequence tends to @{term l}, the distance of the
       sequence elements to @{term B} tends to the distance of @{term l} and @{term B}.
       Furthermore, the distance of the sequence elements is bounded by $(1+\varepsilon)C$,
       which tends to 0, so the distance of @{term l} to @{term B} must be 0.\<close>
   have "setdist {l} B \<le> 0"
   proof (rule tendsto_le)
     show "((\<lambda>x. setdist {x} B) \<circ> (v \<circ> h)) \<longlonglongrightarrow> setdist {l} B"
       by (intro continuous_imp_tendsto l continuous_at_setdist)
     show "(\<lambda>n. inverse (Suc (h n)) * C) \<longlonglongrightarrow> 0"
       by (intro tendsto_mult_left_zero filterlim_compose[OF _ filterlim_subseq[OF h]]
                 LIMSEQ_inverse_real_of_nat)
     show "\<forall>\<^sub>F x in sequentially. ((\<lambda>x. setdist {x} B) \<circ> (v \<circ> h)) x
                                   \<le> inverse (real (Suc (h x))) * C"
       using setdist_le and v unfolding o_def
       by (intro always_eventually allI setdist_le) (auto simp: field_simps)
   qed auto
   hence "setdist {l} B = 0"
     by (intro antisym setdist_pos_le)
   with assms and \<open>compact B\<close> have "l \<in> B"
     by (subst (asm) setdist_eq_0_closed) (auto intro: compact_imp_closed)
 
   \<comment> \<open>It is also easy to see that, since the lattice is a closed set and all sequence
       elements lie on it, the limit @{term l} also lies on it.\<close>
   moreover have "l \<in> {l. \<forall>i. l $ i \<in> \<int>} - {0}"
     using v by (intro closed_sequentially[OF closed_lattice _ l]) auto
   ultimately show ?thesis using that by blast
 qed
 
 end
diff --git a/thys/Nested_Multisets_Ordinals/Unary_PCF.thy b/thys/Nested_Multisets_Ordinals/Unary_PCF.thy
--- a/thys/Nested_Multisets_Ordinals/Unary_PCF.thy
+++ b/thys/Nested_Multisets_Ordinals/Unary_PCF.thy
@@ -1,659 +1,659 @@
 (*  Title:       Towards Decidability of Behavioral Equivalence for Unary PCF
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
     Maintainer:  Dmitriy Traytel <traytel at inf.ethz.ch>
 *)
 
 section \<open>Towards Decidability of Behavioral Equivalence for Unary PCF\<close>
 
 theory Unary_PCF
   imports
     "HOL-Library.FSet"
     "HOL-Library.Countable_Set_Type"
     "HOL-Library.Nat_Bijection"
     Hereditary_Multiset
     "List-Index.List_Index"
 begin
 
 subsection \<open>Preliminaries\<close>
 
 lemma prod_UNIV: "UNIV = UNIV \<times> UNIV"
   by auto
 
 lemma infinite_cartesian_productI1: "infinite A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> infinite (A \<times> B)"
   by (auto dest!: finite_cartesian_productD1)
 
 
 subsection \<open>Types\<close>
 
 datatype type = \<B> ("\<B>") | Fun type type (infixr "\<rightarrow>" 65)
 
 definition mk_fun  (infixr "\<rightarrow>\<rightarrow>" 65) where
   "Ts \<rightarrow>\<rightarrow> T = fold (\<rightarrow>) (rev Ts) T"
 
 primrec dest_fun where
   "dest_fun \<B> = []"
 | "dest_fun (T \<rightarrow> U) = T # dest_fun U"
 
 definition arity where
   "arity T = length (dest_fun T)"
 
 lemma mk_fun_dest_fun[simp]: "dest_fun T \<rightarrow>\<rightarrow> \<B> = T"
   by (induct T) (auto simp: mk_fun_def)
 
 lemma dest_fun_mk_fun[simp]: "dest_fun (Ts \<rightarrow>\<rightarrow> T) = Ts @ dest_fun T"
   by (induct Ts) (auto simp: mk_fun_def)
 
 primrec \<delta> where
   "\<delta> \<B> = HMSet {#}"
 | "\<delta> (T \<rightarrow> U) = HMSet (add_mset (\<delta> T) (hmsetmset (\<delta> U)))"
 
 lemma \<delta>_mk_fun: "\<delta> (Ts \<rightarrow>\<rightarrow> T) = HMSet (hmsetmset (\<delta> T) + mset (map \<delta> Ts))"
   by (induct Ts) (auto simp: mk_fun_def)
 
 lemma type_induct [case_names Fun]:
   assumes
    "(\<And>T. (\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
     (\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)"
   shows "P T"
 proof (induct T)
   case \<B>
   show ?case by (rule assms) simp_all
 next
   case Fun
   show ?case by (rule assms) (insert Fun, simp_all)
 qed
 
 
 subsection \<open>Terms\<close>
 
 type_synonym name = string
 type_synonym idx = nat
 datatype expr =
     Var "name * type" ("\<langle>_\<rangle>") | Bound idx | B bool
   | Seq expr expr  (infixr "?" 75) | App expr expr (infixl "\<cdot>" 75)
   | Abs type expr ("\<Lambda>\<langle>_\<rangle> _" [100, 100] 800)
 
 declare [[coercion_enabled]]
 declare [[coercion B]]
 declare [[coercion Bound]]
 
 notation (output) B ("_")
 notation (output) Bound ("_")
 
 primrec "open" :: "idx \<Rightarrow> expr \<Rightarrow> expr \<Rightarrow> expr" where
   "open i t (j :: idx) = (if i = j then t else j)"
 | "open i t \<langle>yU\<rangle> = \<langle>yU\<rangle>"
 | "open i t (b :: bool) = b"
 | "open i t (e1 ? e2) = open i t e1 ? open i t e2"
 | "open i t (e1 \<cdot> e2) = open i t e1 \<cdot> open i t e2"
 | "open i t (\<Lambda>\<langle>U\<rangle> e) = \<Lambda>\<langle>U\<rangle> (open (i + 1) t e)"
 
 abbreviation "open0 \<equiv> open 0"
 abbreviation "open_Var i xT \<equiv> open i \<langle>xT\<rangle>"
 abbreviation "open0_Var xT \<equiv> open 0 \<langle>xT\<rangle>"
 
 primrec "close_Var" :: "idx \<Rightarrow> name \<times> type \<Rightarrow> expr \<Rightarrow> expr" where
   "close_Var i xT (j :: idx) = j"
 | "close_Var i xT \<langle>yU\<rangle> = (if xT = yU then i else \<langle>yU\<rangle>)"
 | "close_Var i xT (b :: bool) = b"
 | "close_Var i xT (e1 ? e2) = close_Var i xT e1 ? close_Var i xT e2"
 | "close_Var i xT (e1 \<cdot> e2) = close_Var i xT e1 \<cdot> close_Var i xT e2"
 | "close_Var i xT (\<Lambda>\<langle>U\<rangle> e) = \<Lambda>\<langle>U\<rangle> (close_Var (i + 1) xT e)"
 
 abbreviation "close0_Var \<equiv> close_Var 0"
 
 primrec "fv" :: "expr \<Rightarrow> (name \<times> type) fset" where
   "fv (j :: idx) = {||}"
 | "fv \<langle>yU\<rangle> = {|yU|}"
 | "fv (b :: bool) = {||}"
 | "fv (e1 ? e2) = fv e1 |\<union>| fv e2"
 | "fv (e1 \<cdot> e2) = fv e1 |\<union>| fv e2"
 | "fv (\<Lambda>\<langle>U\<rangle> e) = fv e"
 
 abbreviation "fresh x e \<equiv> x |\<notin>| fv e"
 
 lemma ex_fresh: "\<exists>x. (x :: char list, T) |\<notin>| A"
 proof (rule ccontr, unfold not_ex not_not)
   assume "\<forall>x. (x, T) |\<in>| A"
   then have "infinite {x. (x, T) |\<in>| A}" (is "infinite ?P")
     by (auto simp add: infinite_UNIV_listI)
   moreover
   have "?P \<subseteq> fst ` fset A"
     by (force simp: fmember.rep_eq)
   from finite_surj[OF _ this] have "finite ?P"
     by simp
   ultimately show False by blast
 qed
 
 inductive lc where
   lc_Var[simp]: "lc \<langle>xT\<rangle>"
 | lc_B[simp]: "lc (b :: bool)"
 | lc_Seq: "lc e1 \<Longrightarrow> lc e2 \<Longrightarrow> lc (e1 ? e2)"
 | lc_App: "lc e1 \<Longrightarrow> lc e2 \<Longrightarrow> lc (e1 \<cdot> e2)"
 | lc_Abs: "(\<forall>x. (x, T) |\<notin>| X \<longrightarrow> lc (open0_Var (x, T) e)) \<Longrightarrow> lc (\<Lambda>\<langle>T\<rangle> e)"
 
 declare lc.intros[intro]
 
 definition "body T t \<equiv> (\<exists>X. \<forall>x. (x, T) |\<notin>| X \<longrightarrow> lc (open0_Var (x, T) t))"
 
 lemma lc_Abs_iff_body: "lc (\<Lambda>\<langle>T\<rangle> t) \<longleftrightarrow> body T t"
   unfolding body_def by (subst lc.simps) simp
 
 lemma fv_open_Var: "fresh xT t \<Longrightarrow> fv (open_Var i xT t) |\<subseteq>| finsert xT (fv t)"
   by (induct t arbitrary: i) auto
 
 lemma fv_close_Var[simp]: "fv (close_Var i xT t) = fv t |-| {|xT|}"
   by (induct t arbitrary: i) auto
 
 lemma close_Var_open_Var[simp]: "fresh xT t \<Longrightarrow> close_Var i xT (open_Var i xT t) = t"
   by (induct t arbitrary: i) auto
 
 lemma open_Var_inj: "fresh xT t \<Longrightarrow> fresh xT u \<Longrightarrow> open_Var i xT t = open_Var i xT u \<Longrightarrow> t = u"
   by (metis close_Var_open_Var)
 
 context begin
 
 private lemma open_Var_open_Var_close_Var: "i \<noteq> j \<Longrightarrow> xT \<noteq> yU \<Longrightarrow> fresh yU t \<Longrightarrow>
   open_Var i yU (open_Var j zV (close_Var j xT t)) = open_Var j zV (close_Var j xT (open_Var i yU t))"
   by (induct t arbitrary: i j) auto
 
 lemma open_Var_close_Var[simp]: "lc t \<Longrightarrow> open_Var i xT (close_Var i xT t) = t"
 proof (induction t arbitrary: i rule: lc.induct)
   case (lc_Abs T X e i)
   obtain x where x: "fresh (x, T) e" "(x, T) \<noteq> xT" "(x, T) |\<notin>| X"
     using ex_fresh[of _ "fv e |\<union>| finsert xT X"] by blast
   with lc_Abs.IH have "lc (open0_Var (x, T) e)"
     "open_Var (i + 1) xT (close_Var (i + 1) xT (open0_Var (x, T) e)) = open0_Var (x, T) e"
     by auto
   with x show ?case
     by (auto simp: open_Var_open_Var_close_Var
       dest: fset_mp[OF fv_open_Var, rotated]
       intro!: open_Var_inj[of "(x, T)" _ e 0])
 qed auto
 
 end
 
 lemma close_Var_inj: "lc t \<Longrightarrow> lc u \<Longrightarrow> close_Var i xT t = close_Var i xT u \<Longrightarrow> t = u"
   by (metis open_Var_close_Var)
 
 primrec Apps (infixl "\<bullet>" 75) where
   "f \<bullet> [] = f"
 | "f \<bullet> (x # xs) = f \<cdot> x \<bullet> xs"
 
 lemma Apps_snoc: "f \<bullet> (xs @ [x]) = f \<bullet> xs \<cdot> x"
   by (induct xs arbitrary: f) auto
 
 lemma Apps_append: "f \<bullet> (xs @ ys) = f \<bullet>  xs \<bullet>  ys"
   by (induct xs arbitrary: f) auto
 
 lemma Apps_inj[simp]: "f \<bullet> ts = g \<bullet> ts \<longleftrightarrow> f = g"
   by (induct ts arbitrary: f g) auto
 
 lemma eq_Apps_conv[simp]:
   fixes i :: idx and b :: bool and f :: expr and ts :: "expr list"
   shows
     "(\<langle>m\<rangle> = f \<bullet> ts) = (\<langle>m\<rangle> = f \<and> ts = [])"
     "(f  \<bullet> ts = \<langle>m\<rangle>) = (\<langle>m\<rangle> = f \<and> ts = [])"
     "(i = f \<bullet> ts) = (i = f \<and> ts = [])"
     "(f \<bullet> ts = i) = (i = f \<and> ts = [])"
     "(b = f \<bullet> ts) = (b = f \<and> ts = [])"
     "(f \<bullet> ts = b) = (b = f \<and> ts = [])"
     "(e1 ? e2 = f \<bullet> ts) = (e1 ? e2 = f \<and> ts = [])"
     "(f \<bullet> ts = e1 ? e2) = (e1 ? e2 = f \<and> ts = [])"
     "(\<Lambda>\<langle>T\<rangle> t = f \<bullet> ts) = (\<Lambda>\<langle>T\<rangle> t = f \<and> ts = [])"
     "(f \<bullet> ts = \<Lambda>\<langle>T\<rangle> t) = (\<Lambda>\<langle>T\<rangle> t = f \<and> ts = [])"
   by (induct ts arbitrary: f) auto
 
 lemma Apps_Var_eq[simp]: "\<langle>xT\<rangle> \<bullet> ss = \<langle>yU\<rangle> \<bullet> ts \<longleftrightarrow> xT = yU \<and> ss = ts"
 proof (induct ss arbitrary: ts rule: rev_induct)
   case snoc
   then show ?case by (induct ts rule: rev_induct) (auto simp: Apps_snoc)
 qed auto
 
 lemma Apps_Abs_neq_Apps[simp, symmetric, simp]:
   "\<Lambda>\<langle>T\<rangle> r \<cdot> t \<noteq> \<langle>xT\<rangle> \<bullet> ss"
   "\<Lambda>\<langle>T\<rangle> r \<cdot> t \<noteq> (i :: idx) \<bullet> ss"
   "\<Lambda>\<langle>T\<rangle> r \<cdot> t \<noteq> (b :: bool) \<bullet> ss"
   "\<Lambda>\<langle>T\<rangle> r \<cdot> t \<noteq> (e1 ? e2) \<bullet> ss"
   by (induct ss rule: rev_induct) (auto simp: Apps_snoc)
 
 lemma App_Abs_eq_Apps_Abs[simp]: "\<Lambda>\<langle>T\<rangle> r \<cdot> t = \<Lambda>\<langle>T'\<rangle> r' \<bullet> ss \<longleftrightarrow> T = T' \<and> r = r' \<and> ss = [t]"
   by (induct ss rule: rev_induct) (auto simp: Apps_snoc)
 
 lemma Apps_Var_neq_Apps_Abs[simp, symmetric, simp]: "\<langle>xT\<rangle> \<bullet> ss \<noteq> \<Lambda>\<langle>T\<rangle> r \<bullet> ts"
 proof (induct ss arbitrary: ts rule: rev_induct)
   case (snoc a ss)
   then show ?case by (induct ts rule: rev_induct) (auto simp: Apps_snoc)
 qed simp
 
 lemma Apps_Var_neq_Apps_beta[simp, THEN not_sym, simp]:
   "\<langle>xT\<rangle> \<bullet> ss \<noteq> \<Lambda>\<langle>T\<rangle> r \<cdot> s \<bullet> ts"
   by (metis Apps_Var_neq_Apps_Abs Apps_append Apps_snoc eq_Apps_conv(9))
 
 lemma [simp]:
   "(\<Lambda>\<langle>T\<rangle> r \<bullet> ts = \<Lambda>\<langle>T'\<rangle> r' \<cdot> s' \<bullet> ts') = (T = T' \<and> r = r' \<and> ts = s' # ts')"
 proof (induct ts arbitrary: ts' rule: rev_induct)
   case Nil
   then show ?case by (induct ts' rule: rev_induct) (auto simp: Apps_snoc)
 next
   case snoc
   then show ?case by (induct ts' rule: rev_induct) (auto simp: Apps_snoc)
 qed
 
 lemma fold_eq_Bool_iff[simp]:
   "fold (\<rightarrow>) (rev Ts) T = \<B> \<longleftrightarrow> Ts = [] \<and> T = \<B>"
   "\<B> = fold (\<rightarrow>) (rev Ts) T \<longleftrightarrow> Ts = [] \<and> T = \<B>"
   by (induct Ts) auto
 
 lemma fold_eq_Fun_iff[simp]:
   "fold (\<rightarrow>) (rev Ts) T = U \<rightarrow> V \<longleftrightarrow>
    (Ts = [] \<and> T = U \<rightarrow> V \<or> (\<exists>Us. Ts = U # Us \<and> fold (\<rightarrow>) (rev Us) T = V))"
   by (induct Ts) auto
 
 
 subsection \<open>Substitution\<close>
 
 primrec subst where
   "subst xT t \<langle>yU\<rangle> = (if xT = yU then t else \<langle>yU\<rangle>)"
 | "subst xT t (i :: idx) = i"
 | "subst xT t (b :: bool) = b"
 | "subst xT t (e1 ? e2) = subst xT t e1 ? subst xT t e2"
 | "subst xT t (e1 \<cdot> e2) = subst xT t e1 \<cdot> subst xT t e2"
 | "subst xT t (\<Lambda>\<langle>T\<rangle> e) = \<Lambda>\<langle>T\<rangle> (subst xT t e)"
 
 lemma fv_subst:
   "fv (subst xT t u) = fv u |-| {|xT|} |\<union>| (if xT |\<in>| fv u then fv t else {||})"
   by (induct u) auto
 
 lemma subst_fresh: "fresh xT u \<Longrightarrow> subst xT t u = u"
   by (induct u) auto
 
 context begin
 
 private lemma open_open_id: "i \<noteq> j \<Longrightarrow> open i t (open j t' u) = open j t' u \<Longrightarrow> open i t u = u"
   by (induct u arbitrary: i j) (auto 6 0)
 
 lemma lc_open_id: "lc u \<Longrightarrow> open k t u = u"
 proof (induct u arbitrary: k rule: lc.induct)
   case (lc_Abs T X e)
   obtain x where x: "fresh (x, T) e" "(x, T) |\<notin>| X"
     using ex_fresh[of _ "fv e |\<union>| X"] by blast
   with lc_Abs show ?case
     by (auto intro: open_open_id dest: spec[of _ x] spec[of _ "Suc k"])
 qed auto
 
 lemma subst_open: "lc u \<Longrightarrow> subst xT u (open i t v) = open i (subst xT u t) (subst xT u v)"
   by (induction v arbitrary: i) (auto intro: lc_open_id[symmetric])
 
 lemma subst_open_Var:
   "xT \<noteq> yU \<Longrightarrow> lc u \<Longrightarrow> subst xT u (open_Var i yU v) = open_Var i yU (subst xT u v)"
   by (auto simp: subst_open)
 
 lemma subst_Apps[simp]:
   "subst xT u (f \<bullet> xs) = subst xT u f \<bullet> map (subst xT u) xs"
   by (induct xs arbitrary: f) auto
 
 end
 
 context begin
 
 private lemma fresh_close_Var_id: "fresh xT t \<Longrightarrow> close_Var k xT t = t"
   by (induct t arbitrary: k) auto
 
 lemma subst_close_Var:
   "xT \<noteq> yU \<Longrightarrow> fresh yU u \<Longrightarrow> subst xT u (close_Var i yU t) = close_Var i yU (subst xT u t)"
   by (induct t arbitrary: i) (auto simp: fresh_close_Var_id)
 
 end
 
 lemma subst_intro: "fresh xT t \<Longrightarrow> lc u \<Longrightarrow> open0 u t = subst xT u (open0_Var xT t)"
   by (auto simp: subst_fresh subst_open)
 
 lemma lc_subst[simp]: "lc u \<Longrightarrow> lc t \<Longrightarrow> lc (subst xT t u)"
 proof (induct u rule: lc.induct)
   case (lc_Abs T X e)
   then show ?case
     by (auto simp: subst_open_Var intro!: lc.lc_Abs[of _ "fv e |\<union>| X |\<union>| {|xT|}"])
 qed auto
 
 lemma body_subst[simp]: "body U u \<Longrightarrow> lc t \<Longrightarrow> body U (subst xT t u)"
 proof (subst (asm) body_def, elim conjE exE)
   fix X
   assume [simp]: "lc t" "\<forall>x. (x, U) |\<notin>| X \<longrightarrow> lc (open0_Var (x, U) u)"
   show "body U (subst xT t u)"
   proof (unfold body_def, intro exI[of _ "finsert xT X"] conjI allI impI)
     fix x
     assume "(x, U) |\<notin>| finsert xT X"
     then show "lc (open0_Var (x, U) (subst xT t u))"
       by (auto simp: subst_open_Var[symmetric])
   qed
 qed
 
 lemma lc_open_Var: "lc u \<Longrightarrow> lc (open_Var i xT u)"
   by (simp add: lc_open_id)
 
 lemma lc_open[simp]: "body U u \<Longrightarrow> lc t \<Longrightarrow> lc (open0 t u)"
 proof (unfold body_def, elim conjE exE)
   fix X
   assume [simp]: "lc t" "\<forall>x. (x, U) |\<notin>| X \<longrightarrow> lc (open0_Var (x, U) u)"
   with ex_fresh[of _ "fv u |\<union>| X"] obtain x where [simp]: "fresh (x, U) u" "(x, U) |\<notin>| X" by blast
   show ?thesis by (subst subst_intro[of "(x, U)"]) auto
 qed
 
 
 subsection \<open>Typing\<close>
 
 inductive welltyped :: "expr \<Rightarrow> type \<Rightarrow> bool" (infix ":::" 60) where
   welltyped_Var[intro!]: "\<langle>(x, T)\<rangle> ::: T"
 | welltyped_B[intro!]: "(b :: bool) ::: \<B>"
 | welltyped_Seq[intro!]: "e1 ::: \<B> \<Longrightarrow> e2 ::: \<B> \<Longrightarrow> e1 ? e2 ::: \<B>"
 | welltyped_App[intro]: "e1 ::: T \<rightarrow> U \<Longrightarrow> e2 ::: T \<Longrightarrow> e1 \<cdot> e2 ::: U"
 | welltyped_Abs[intro]: "(\<forall>x. (x, T) |\<notin>| X \<longrightarrow> open0_Var (x, T) e ::: U) \<Longrightarrow> \<Lambda>\<langle>T\<rangle> e ::: T \<rightarrow> U"
 
 inductive_cases welltypedE[elim!]:
    "\<langle>x\<rangle> ::: T"
    "(i :: idx) ::: T"
    "(b :: bool) ::: T"
    "e1 ? e2 ::: T"
    "e1 \<cdot> e2 ::: T"
    "\<Lambda>\<langle>T\<rangle> e ::: U"
 
 lemma welltyped_unique: "t ::: T \<Longrightarrow> t ::: U \<Longrightarrow> T = U"
 proof (induction t T arbitrary: U rule: welltyped.induct)
   case (welltyped_Abs T X t U T')
   from welltyped_Abs.prems show ?case
   proof (elim welltypedE)
     fix Y U'
     obtain x where [simp]: "(x, T) |\<notin>| X" "(x, T) |\<notin>| Y"
       using ex_fresh[of _ "X |\<union>| Y"] by blast
     assume [simp]: "T' = T \<rightarrow> U'" "\<forall>x. (x, T) |\<notin>| Y \<longrightarrow> open0_Var (x, T) t ::: U'"
     show "T \<rightarrow> U = T'"
       by (auto intro: conjunct2[OF welltyped_Abs.IH[rule_format], rule_format, of x])
   qed
 qed blast+
 
 lemma welltyped_lc[simp]: "t ::: T \<Longrightarrow> lc t"
   by (induction t T rule: welltyped.induct) auto
 
 lemma welltyped_subst[intro]:
   "u ::: U \<Longrightarrow> t ::: snd xT \<Longrightarrow> subst xT t u ::: U"
 proof (induction u U rule: welltyped.induct)
   case (welltyped_Abs T' X u U)
   then show ?case unfolding subst.simps
     by (intro welltyped.welltyped_Abs[of _ "finsert xT X"]) (auto simp: subst_open_Var[symmetric])
 qed auto
 
 lemma rename_welltyped: "u ::: U \<Longrightarrow> subst (x, T) \<langle>(y, T)\<rangle> u ::: U"
   by (rule welltyped_subst) auto
 
 lemma welltyped_Abs_fresh:
   assumes "fresh (x, T) u" "open0_Var (x, T) u ::: U"
   shows "\<Lambda>\<langle>T\<rangle> u ::: T \<rightarrow> U"
 proof (intro welltyped_Abs[of _ "fv u"] allI impI)
   fix y
   assume "fresh (y, T) u"
   with assms(2) have "subst (x, T) \<langle>(y, T)\<rangle> (open0_Var (x, T) u) ::: U" (is "?t ::: _")
     by (auto intro: rename_welltyped)
   also have "?t = open0_Var (y, T) u"
     by (subst subst_intro[symmetric]) (auto simp: assms(1))
   finally show "open0_Var (y, T) u ::: U" .
 qed
 
 lemma Apps_alt: "f \<bullet> ts ::: T \<longleftrightarrow>
   (\<exists>Ts. f ::: fold (\<rightarrow>) (rev Ts) T \<and> list_all2 (:::) ts Ts)"
 proof (induct ts arbitrary: f)
   case (Cons t ts)
   from Cons(1)[of "f \<cdot> t"] show ?case
     by (force simp: list_all2_Cons1)
 qed simp
 
 
-subsection \<open>Definition 10 and Lemma 11 from Schmidt-Schauß's paper\<close>
+subsection \<open>Definition 10 and Lemma 11 from Schmidt-Schau{\ss}'s paper\<close>
 
 abbreviation "closed t \<equiv> fv t = {||}"
 
 primrec constant0 where
   "constant0 \<B> = Var (''bool'', \<B>)"
 | "constant0 (T \<rightarrow> U) = \<Lambda>\<langle>T\<rangle> (constant0 U)"
 
 definition "constant T = \<Lambda>\<langle>\<B>\<rangle> (close0_Var (''bool'', \<B>) (constant0 T))"
 
 lemma fv_constant0[simp]: "fv (constant0 T) = {|(''bool'', \<B>)|}"
   by (induct T) auto
 
 lemma closed_constant[simp]: "closed (constant T)"
   unfolding constant_def by auto
 
 lemma welltyped_constant0[simp]: "constant0 T ::: T"
   by (induct T) (auto simp: lc_open_id)
 
 lemma lc_constant0[simp]: "lc (constant0 T)"
   using welltyped_constant0 welltyped_lc by blast
 
 lemma welltyped_constant[simp]: "constant T ::: \<B> \<rightarrow> T"
   unfolding constant_def by (auto intro: welltyped_Abs_fresh[of "''bool''"])
 
 definition nth_drop where
   "nth_drop i xs \<equiv> take i xs @ drop (Suc i) xs"
 
 definition nth_arg (infixl "!-" 100) where
   "nth_arg T i \<equiv> nth (dest_fun T) i"
 
 abbreviation ar where
   "ar T \<equiv> length (dest_fun T)"
 
 lemma size_nth_arg[simp]: "i < ar T \<Longrightarrow> size (T !- i) < size T"
   by (induct T arbitrary: i) (force simp: nth_Cons' nth_arg_def gr0_conv_Suc)+
 
 fun \<pi> :: "type \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> type" where
   "\<pi> T i 0 = (if i < ar T then nth_drop i (dest_fun T) \<rightarrow>\<rightarrow> \<B> else \<B>)"
 | "\<pi> T i (Suc j) = (if i < ar T \<and> j < ar (T!-i)
     then \<pi> (T!-i) j 0 \<rightarrow>
       map (\<pi> (T!-i) j o Suc) [0 ..< ar (T!-i!-j)] \<rightarrow>\<rightarrow> \<pi> T i 0 else \<B>)"
 
 theorem \<pi>_induct[rotated -2, consumes 2, case_names 0 Suc]:
   assumes "\<And>T i. i < ar T \<Longrightarrow> P T i 0"
     and "\<And>T i j. i < ar T \<Longrightarrow> j < ar (T !- i) \<Longrightarrow> P (T !- i) j 0 \<Longrightarrow>
        (\<forall>x < ar (T !- i !- j). P (T !- i) j (x + 1)) \<Longrightarrow> P T i (j + 1)"
   shows "i < ar T \<Longrightarrow> j \<le> ar (T !- i) \<Longrightarrow> P T i j"
   by (induct T i j rule: \<pi>.induct) (auto intro: assms[simplified])
 
 definition \<epsilon> :: "type \<Rightarrow> nat \<Rightarrow> type" where
   "\<epsilon> T i = \<pi> T i 0 \<rightarrow> map (\<pi> T i o Suc) [0 ..< ar (T!-i)] \<rightarrow>\<rightarrow> T"
 
 definition Abss ("\<Lambda>[_] _" [100, 100] 800) where
   "\<Lambda>[xTs] b = fold (\<lambda>xT t. \<Lambda>\<langle>snd xT\<rangle> close0_Var xT t) (rev xTs) b"
 
 definition Seqs (infixr "??" 75) where
   "ts ?? t = fold (\<lambda>u t. u ? t) (rev ts) t"
 
 definition "variant k base = base @ replicate k CHR ''*''"
 
 lemma variant_inj: "variant i base = variant j base \<Longrightarrow> i = j"
   unfolding variant_def by auto
 
 lemma variant_inj2:
   "CHR ''*'' \<notin> set b1 \<Longrightarrow> CHR ''*'' \<notin> set b2 \<Longrightarrow> variant i b1 = variant j b2 \<Longrightarrow> b1 = b2"
   unfolding variant_def
   by (auto simp: append_eq_append_conv2)
     (metis Nil_is_append_conv hd_append2 hd_in_set hd_rev last_ConsR
      last_snoc replicate_append_same rev_replicate)+
 
 fun E :: "type \<Rightarrow> nat \<Rightarrow> expr" and P :: "type \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> expr" where
   "E T i = (if i < ar T then (let
        Ti = T!-i;
        x = \<lambda>k. (variant k ''x'', T!-k);
        xs = map x [0 ..< ar T];
        xx_var = \<langle>nth xs i\<rangle>;
        x_vars = map (\<lambda>x. \<langle>x\<rangle>) (nth_drop i xs);
        yy = (''z'', \<pi> T i 0);
        yy_var = \<langle>yy\<rangle>;
        y = \<lambda>j. (variant j ''y'', \<pi> T i (j + 1));
        ys = map y [0 ..< ar Ti];
        e = \<lambda>j. \<langle>y j\<rangle> \<bullet> (P Ti j 0 \<cdot> xx_var # map (\<lambda>k. P Ti j (k + 1) \<cdot> xx_var) [0 ..< ar (Ti!-j)]);
        guards = map (\<lambda>i. xx_var \<bullet>
            map (\<lambda>j. constant (Ti!-j) \<cdot> (if i = j then e i \<bullet> x_vars else True)) [0 ..< ar Ti])
          [0 ..< ar Ti]
      in \<Lambda>[(yy # ys @ xs)] (guards ?? (yy_var \<bullet> x_vars))) else constant (\<epsilon> T i) \<cdot> False)"
 | "P T i 0 =
      (if i < ar T then (let
        f = (''f'', T);
        f_var = \<langle>f\<rangle>;
        x = \<lambda>k. (variant k ''x'', T!-k);
        xs = nth_drop i (map x [0 ..< ar T]);
        x_vars = insert_nth i (constant (T!-i) \<cdot> True) (map (\<lambda>x. \<langle>x\<rangle>) xs)
      in \<Lambda>[(f # xs)] (f_var \<bullet> x_vars)) else constant (T \<rightarrow> \<pi> T i 0) \<cdot> False)"
 | "P T i (Suc j) = (if i < ar T \<and> j < ar (T!-i) then (let
        Ti = T!-i;
        Tij = Ti!-j;
        f = (''f'', T);
        f_var = \<langle>f\<rangle>;
        x = \<lambda>k. (variant k ''x'', T!-k);
        xs = nth_drop i (map x [0 ..< ar T]);
        yy = (''z'', \<pi> Ti j 0);
        yy_var = \<langle>yy\<rangle>;
        y = \<lambda>k. (variant k ''y'', \<pi> Ti j (k + 1));
        ys = map y [0 ..< ar Tij];
        y_vars = yy_var # map (\<lambda>x. \<langle>x\<rangle>) ys;
        x_vars = insert_nth i (E Ti j \<bullet> y_vars) (map (\<lambda>x. \<langle>x\<rangle>) xs)
      in \<Lambda>[(f # yy # ys @ xs)] (f_var \<bullet> x_vars)) else constant (T \<rightarrow> \<pi> T i (j + 1)) \<cdot> False)"
 
 lemma Abss_Nil[simp]: "\<Lambda>[[]] b = b"
   unfolding Abss_def by simp
 
 lemma Abss_Cons[simp]: "\<Lambda>[(x#xs)] b = \<Lambda>\<langle>snd x\<rangle> (close0_Var x (\<Lambda>[xs] b))"
   unfolding Abss_def by simp
 
 lemma welltyped_Abss: "b ::: U \<Longrightarrow> T = map snd xTs \<rightarrow>\<rightarrow> U \<Longrightarrow> \<Lambda>[xTs] b ::: T"
   by (hypsubst_thin, induct xTs) (auto simp: mk_fun_def intro!: welltyped_Abs_fresh)
 
 lemma welltyped_Apps: "list_all2 (:::) ts Ts \<Longrightarrow> f ::: Ts \<rightarrow>\<rightarrow> U \<Longrightarrow> f \<bullet> ts ::: U"
   by (induct ts Ts arbitrary: f rule: list.rel_induct) (auto simp: mk_fun_def)
 
 lemma welltyped_open_Var_close_Var[intro!]:
   "t ::: T \<Longrightarrow> open0_Var xT (close0_Var xT t) ::: T"
   by auto
 
 lemma welltyped_Var_iff[simp]:
   "\<langle>(x, T)\<rangle> ::: U \<longleftrightarrow> T = U"
   by auto
 
 lemma welltyped_bool_iff[simp]: "(b :: bool) ::: T \<longleftrightarrow> T = \<B>"
   by auto
 
 lemma welltyped_constant0_iff[simp]: "constant0 T ::: U \<longleftrightarrow> (U = T)"
   by (induct T arbitrary: U) (auto simp: ex_fresh lc_open_id)
 
 lemma welltyped_constant_iff[simp]: "constant T ::: U \<longleftrightarrow> (U = \<B> \<rightarrow> T)"
   unfolding constant_def
 proof (intro iffI, elim welltypedE, hypsubst_thin, unfold type.inject simp_thms)
   fix X U
   assume "\<forall>x. (x, \<B>) |\<notin>| X \<longrightarrow> open0_Var (x, \<B>) (close0_Var (''bool'', \<B>) (constant0 T)) ::: U"
   moreover obtain x where "(x, \<B>) |\<notin>| X" using ex_fresh[of \<B> X] by blast
   ultimately have "open0_Var (x, \<B>) (close0_Var (''bool'', \<B>) (constant0 T)) ::: U" by simp
   then have "open0_Var (''bool'', \<B>) (close0_Var (''bool'', \<B>) (constant0 T)) ::: U"
     using rename_welltyped[of \<open>open0_Var (x, \<B>) (close0_Var (''bool'', \<B>) (constant0 T))\<close>
        U x \<B> "''bool''"]
     by (auto simp: subst_open subst_fresh)
   then show "U = T" by auto
 qed (auto intro!: welltyped_Abs_fresh)
 
 lemma welltyped_Seq_iff[simp]: "e1 ? e2 ::: T \<longleftrightarrow> (T = \<B> \<and> e1 ::: \<B> \<and> e2 ::: \<B>)"
   by auto
 
 lemma welltyped_Seqs_iff[simp]: "es ?? e ::: T \<longleftrightarrow>
   ((es \<noteq> [] \<longrightarrow> T = \<B>) \<and> (\<forall>e \<in> set es. e ::: \<B>) \<and> e ::: T)"
   by (induct es arbitrary: e) (auto simp: Seqs_def)
 
 lemma welltyped_App_iff[simp]: "f \<cdot> t ::: U \<longleftrightarrow> (\<exists>T. f ::: T \<rightarrow> U \<and> t ::: T)"
   by auto
 
 lemma welltyped_Apps_iff[simp]: "f \<bullet> ts ::: U \<longleftrightarrow> (\<exists>Ts. f ::: Ts \<rightarrow>\<rightarrow> U \<and> list_all2 (:::) ts Ts)"
   by (induct ts arbitrary: f) (auto 0 3 simp: mk_fun_def list_all2_Cons1 intro: exI[of _ "_ # _"])
 
 lemma eq_mk_fun_iff[simp]: "T = Ts \<rightarrow>\<rightarrow> \<B> \<longleftrightarrow> Ts = dest_fun T"
   by auto
 
 lemma map_nth_eq_drop_take[simp]: "j \<le> length xs \<Longrightarrow> map (nth xs) [i ..< j] = drop i (take j xs)"
   by (induct j) (auto simp: take_Suc_conv_app_nth)
 
 lemma dest_fun_\<pi>_0: "i < ar T \<Longrightarrow> dest_fun (\<pi> T i 0) = nth_drop i (dest_fun T)"
   by auto
 
 lemma welltyped_E: "E T i ::: \<epsilon> T i" and welltyped_P: "P T i j ::: T \<rightarrow> \<pi> T i j"
 proof (induct T i and T i j rule: E_P.induct)
   case (1 T i)
   note P.simps[simp del] \<pi>.simps[simp del] \<epsilon>_def[simp] nth_drop_def[simp] nth_arg_def[simp]
   from 1(1)[OF _ refl refl refl refl refl refl refl refl refl]
        1(2)[OF _ refl refl refl refl refl refl refl refl refl]
   show ?case
     by (auto 0 4 simp: Let_def o_def take_map[symmetric] drop_map[symmetric]
       list_all2_conv_all_nth nth_append min_def dest_fun_\<pi>_0 \<pi>.simps[of T i]
       intro!: welltyped_Abs_fresh welltyped_Abss[of _ \<B>])
 next
   case (2 T i)
   show ?case
     by (auto simp: Let_def take_map drop_map o_def list_all2_conv_all_nth nth_append nth_Cons'
        nth_drop_def nth_arg_def
       intro!: welltyped_constant welltyped_Abs_fresh welltyped_Abss[of _ \<B>])
 next
   case (3 T i j)
   note E.simps[simp del] \<pi>.simps[simp del] Abss_Cons[simp del] \<epsilon>_def[simp]
     nth_drop_def[simp] nth_arg_def[simp]
   from 3(1)[OF _ refl refl refl refl refl refl refl refl refl refl refl]
   show ?case
     by (auto 0 3 simp: Let_def o_def take_map[symmetric] drop_map[symmetric]
       list_all2_conv_all_nth nth_append nth_Cons' min_def \<pi>.simps[of T i]
       intro!: welltyped_Abs_fresh welltyped_Abss[of _ \<B>])
 qed
 
 lemma \<delta>_gt_0[simp]: "T \<noteq> \<B> \<Longrightarrow> HMSet {#} < \<delta> T"
   by (cases T) auto
 
 lemma mset_nth_drop_less: "i < length xs \<Longrightarrow> mset (nth_drop i xs) < mset xs"
   by (induct xs arbitrary: i) (auto simp: take_Cons' nth_drop_def gr0_conv_Suc)
 
 lemma map_nth_drop: "i < length xs \<Longrightarrow> map f (nth_drop i xs) = nth_drop i (map f xs)"
   by (induct xs arbitrary: i) (auto simp: take_Cons' nth_drop_def gr0_conv_Suc)
 
 lemma empty_less_mset: "{#} < mset xs \<longleftrightarrow> xs \<noteq> []"
   by auto
 
 lemma dest_fun_alt: "dest_fun T = map (\<lambda>i. T !- i) [0..<ar T]"
   unfolding list_eq_iff_nth_eq nth_arg_def by auto
 
 context notes \<pi>.simps[simp del] notes One_nat_def[simp del] begin
 
 lemma \<delta>_\<pi>:
   assumes "i < ar T" "j \<le> ar (T !- i)"
   shows "\<delta> (\<pi> T i j) < \<delta> T"
 using assms proof (induct T i j rule: \<pi>_induct)
   fix T i
   assume "i < ar T"
   then show "\<delta> (\<pi> T i 0) < \<delta> T"
     by (subst (2) mk_fun_dest_fun[symmetric, of T], unfold \<delta>_mk_fun)
       (auto simp: \<delta>_mk_fun mset_map[symmetric] take_map[symmetric] drop_map[symmetric] \<pi>.simps
         mset_nth_drop_less map_nth_drop simp del: mset_map)
 next
   fix T i j
   let ?Ti = "T !- i"
   assume [rule_format, simp]: "i < ar T" "j < ar ?Ti" "\<delta> (\<pi> ?Ti j 0) < \<delta> ?Ti"
     "\<forall>k < ar (?Ti !- j). \<delta> (\<pi> ?Ti j (k + 1)) < \<delta> ?Ti"
   define X and Y and M where
     [simp]: "X = {#\<delta> ?Ti#}" and
     [simp]: "Y = {#\<delta> (\<pi> ?Ti j 0)#} + {#\<delta> (\<pi> ?Ti j (k + 1)). k \<in># mset [0 ..< ar (?Ti !- j)]#}" and
     [simp]: "M \<equiv> {# \<delta> z. z \<in># mset (nth_drop i (dest_fun T))#}"
   have "\<delta> (\<pi> T i (j + 1)) = HMSet (Y + M)"
     by (auto simp: One_nat_def \<pi>.simps \<delta>_mk_fun)
   also have "Y + M < X + M"
     unfolding less_multiset\<^sub>D\<^sub>M by (rule exI[of _ "X"], rule exI[of _ "Y"]) auto
   also have "HMSet (X + M) = \<delta> T"
     unfolding M_def
     by (subst (2) mk_fun_dest_fun[symmetric, of T], subst (2) id_take_nth_drop[of i "dest_fun T"])
       (auto simp: \<delta>_mk_fun nth_arg_def nth_drop_def)
   finally show "\<delta> (\<pi> T i (j + 1)) < \<delta> T" by simp
 qed
 
 end
 
 end
diff --git a/thys/Pi_Transcendental/Pi_Transcendental.thy b/thys/Pi_Transcendental/Pi_Transcendental.thy
--- a/thys/Pi_Transcendental/Pi_Transcendental.thy
+++ b/thys/Pi_Transcendental/Pi_Transcendental.thy
@@ -1,641 +1,641 @@
 (*
     File:      Pi_Transcendendtal.thy
     Author:    Manuel Eberl, TU München
 
    A proof of the transcendence of pi
 *)
 section \<open>The Transcendence of $\pi$\<close>
 theory Pi_Transcendental
 imports
   "E_Transcendental.E_Transcendental"
   "Symmetric_Polynomials.Symmetric_Polynomials"
   "HOL-Real_Asymp.Real_Asymp" 
   Pi_Transcendental_Polynomial_Library
 begin
 
 lemma ring_homomorphism_to_poly [intro]: "ring_homomorphism (\<lambda>i. [:i:])"
   by standard auto
 
 lemma (in ring_closed) coeff_power_closed:
   "(\<And>m. coeff p m \<in> A) \<Longrightarrow> coeff (p ^ n) m \<in> A"
   by (induction n arbitrary: m)
      (auto simp: mpoly_coeff_1 coeff_mpoly_times intro!: prod_fun_closed)
 
 lemma (in ring_closed) coeff_prod_closed:
   "(\<And>x m. x \<in> X \<Longrightarrow> coeff (f x) m \<in> A) \<Longrightarrow> coeff (prod f X) m \<in> A"
   by (induction X arbitrary: m rule: infinite_finite_induct)
      (auto simp: mpoly_coeff_1 coeff_mpoly_times intro!: prod_fun_closed)
 
 lemma map_of_rat_of_int_poly [simp]: "map_poly of_rat (of_int_poly p) = of_int_poly p"
   by (intro poly_eqI) (auto simp: coeff_map_poly)
 
 text \<open>
   Given a polynomial with rational coefficients, we can obtain an integer polynomial that
   differs from it only by a nonzero constant by clearing the denominators.
 \<close>
 lemma ratpoly_to_intpoly:
   assumes "\<forall>i. poly.coeff p i \<in> \<rat>"
   obtains q c where "c \<noteq> 0" "p = Polynomial.smult (inverse (of_nat c)) (of_int_poly q)"
 proof (cases "p = 0")
   case True
   with that[of 1 0] show ?thesis by auto
 next
   case False
   from assms obtain p' where p': "p = map_poly of_rat p'"
     using ratpolyE by auto
   define c where "c = Lcm ((nat \<circ> snd \<circ> quotient_of \<circ> poly.coeff p') ` {..Polynomial.degree p'})"
   have "\<not>snd (quotient_of x) \<le> 0" for x
     using quotient_of_denom_pos[of x, OF surjective_pairing] by auto
   hence "c \<noteq> 0" by (auto simp: c_def)
   define q where "q = Polynomial.smult (of_nat c) p'"
 
   have "poly.coeff q i \<in> \<int>" for i
   proof (cases "i > Polynomial.degree p'")
     case False
     define m n 
       where "m = fst (quotient_of (poly.coeff p' i))"
         and "n = nat (snd (quotient_of (poly.coeff p' i)))"
     have mn: "n > 0" "poly.coeff p' i = of_int m / of_nat n"
       using quotient_of_denom_pos[of "poly.coeff p' i", OF surjective_pairing]
             quotient_of_div[of "poly.coeff p' i", OF surjective_pairing]
       by (auto simp: m_def n_def)
     from False have "n dvd c" unfolding c_def
       by (intro dvd_Lcm) (auto simp: c_def n_def o_def not_less)
     hence "of_nat c * (of_int m / of_nat n) = (of_nat (c div n) * of_int m :: rat)"
       by (auto simp: of_nat_div)
     also have "\<dots> \<in> \<int>" by auto
     finally show ?thesis using mn by (auto simp: q_def)
   qed (auto simp: q_def coeff_eq_0)
   with int_polyE obtain q' where q': "q = of_int_poly q'" by auto
   moreover have "p = Polynomial.smult (inverse (of_nat c)) (map_poly of_rat (of_int_poly q'))"
     unfolding smult_conv_map_poly q'[symmetric] p' using \<open>c \<noteq> 0\<close>
     by (intro poly_eqI) (auto simp: coeff_map_poly q_def of_rat_mult)
   ultimately show ?thesis
     using q' p' \<open>c \<noteq> 0\<close> by (auto intro!: that[of c q'])
 qed
 
 lemma symmetric_mpoly_symmetric_sum:
   assumes "\<And>\<pi>. \<pi> permutes A \<Longrightarrow> g \<pi> permutes X"
   assumes "\<And>x \<pi>. x \<in> X \<Longrightarrow> \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (f x) = f (g \<pi> x)"
   shows "symmetric_mpoly A (\<Sum>x\<in>X. f x)"
   unfolding symmetric_mpoly_def
 proof safe
   fix \<pi> assume \<pi>: "\<pi> permutes A"
   have "mpoly_map_vars \<pi> (sum f X) = (\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x))"
     by simp
   also have "\<dots> = (\<Sum>x\<in>X. f (g \<pi> x))"
     by (intro sum.cong assms \<pi> refl)
   also have "\<dots> = (\<Sum>x\<in>g \<pi>`X. f x)"
     using assms(1)[OF \<pi>] by (subst sum.reindex) (auto simp: permutes_inj_on)
   also have "g \<pi> ` X = X"
     using assms(1)[OF \<pi>] by (simp add: permutes_image)
   finally show "mpoly_map_vars \<pi> (sum f X) = sum f X" .
 qed
 
 (* TODO: The version of this theorem in the AFP is to weak and should be replaced by this one. *)
 lemma symmetric_mpoly_symmetric_prod:
   assumes "g permutes X"
   assumes "\<And>x \<pi>. x \<in> X \<Longrightarrow> \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (f x) = f (g x)"
   shows "symmetric_mpoly A (\<Prod>x\<in>X. f x)"
   unfolding symmetric_mpoly_def
 proof safe
   fix \<pi> assume \<pi>: "\<pi> permutes A"
   have "mpoly_map_vars \<pi> (prod f X) = (\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x))"
     by simp
   also have "\<dots> = (\<Prod>x\<in>X. f (g x))"
     by (intro prod.cong assms \<pi> refl)
   also have "\<dots> = (\<Prod>x\<in>g`X. f x)"
     using assms by (subst prod.reindex) (auto simp: permutes_inj_on)
   also have "g ` X = X"
     using assms by (simp add: permutes_image)
   finally show "mpoly_map_vars \<pi> (prod f X) = prod f X" .
 qed
 
 
 text \<open>
   We now prove the transcendence of $i\pi$, from which the transcendence of $\pi$ will follow
   as a trivial corollary. The first proof of this was given by von Lindemann~\cite{lindemann_pi82}.
   The central ingredient is the fundamental theorem of symmetric functions.
 
   The proof can, by now, be considered folklore and one can easily find many similar variants of
   it, but we mostly follows the nice exposition given by Niven~\cite{niven_pi39}.
 
   An independent previous formalisation in Coq that uses the same basic techniques was given by
   Bernard et al.~\cite{bernard_pi16}. They later also formalised the much stronger
-  Lindemann--Weierstraß theorem~\cite{bernard_lw17}.
+  Lindemann--Weierstra{\ss} theorem~\cite{bernard_lw17}.
 \<close>
 lemma transcendental_i_pi: "\<not>algebraic (\<i> * pi)"
 proof
   \<comment> \<open>Suppose $i\pi$ were algebraic.\<close>
   assume "algebraic (\<i> * pi)"
   \<comment> \<open>We obtain some nonzero integer polynomial that has $i\pi$ as a root. We can assume
       w.\,l.\,o.\,g.\ that the constant coefficient of this polynomial is nonzero.\<close>
   then obtain p
     where p: "poly (of_int_poly p) (\<i> * pi) = 0" "p \<noteq> 0" "poly.coeff p 0 \<noteq> 0"
     by (elim algebraicE'_nonzero) auto
   define n where "n = Polynomial.degree p"
 
   \<comment> \<open>We define the sequence of the roots of this polynomial:\<close>
   obtain root where "Polynomial.smult (Polynomial.lead_coeff (of_int_poly p))
                        (\<Prod>i<n. [:-root i :: complex, 1:]) = of_int_poly p"
     using complex_poly_decompose'[of "of_int_poly p"] unfolding n_def by auto
   note root = this [symmetric]
 
   \<comment> \<open>We note that $i\pi$ is, of course, among these roots.\<close>
   from p and root obtain idx where idx: "idx < n" "root idx = \<i> * pi"
     by (auto simp: poly_prod)
 
   \<comment> \<open>We now define a new polynomial \<open>P'\<close>, whose roots are all numbers that arise as a
       sum of any subset of roots of \<open>p\<close>. We also count all those subsets that sum up to 0
       and call their number \<open>A\<close>.\<close>
   define root' where "root' = (\<lambda>X. (\<Sum>j\<in>X. root j))"
   define P where "P = (\<lambda>i. \<Prod>X | X \<subseteq> {..<n} \<and> card X = i. [:-root' X, 1:])"
   define P' where "P' = (\<Prod>i\<in>{0<..n}. P i)"
   define A where "A = card {X\<in>Pow {..<n}. root' X = 0}"
   have [simp]: "P' \<noteq> 0" by (auto simp: P'_def P_def)
 
   \<comment> \<open>We give the name \<open>Roots'\<close> to those subsets that do not sum to zero and note that there
       is at least one, namely $\{i\pi\}$.\<close>
   define Roots' where "Roots' = {X. X \<subseteq> {..<n} \<and> root' X \<noteq> 0}"
   have [intro]: "finite Roots'" by (auto simp: Roots'_def)
   have "{idx} \<in> Roots'" using idx by (auto simp: Roots'_def root'_def)
   hence "Roots' \<noteq> {}" by auto
   hence card_Roots': "card Roots' > 0" by (auto simp: card_eq_0_iff)
 
   have P'_altdef: "P' = (\<Prod>X\<in>Pow {..<n} - {{}}. [:-root' X, 1:])"
   proof -
     have "P' = (\<Prod>(i, X)\<in>(SIGMA x:{0<..n}. {X. X \<subseteq> {..<n} \<and> card X = x}). [:- root' X, 1:])"
       unfolding P'_def P_def by (subst prod.Sigma) auto
     also have "\<dots> = (\<Prod>X\<in>Pow{..<n} - {{}}. [:- root' X, 1:])"
       using card_mono[of "{..<n}"]
       by (intro prod.reindex_bij_witness[of _ "\<lambda>X. (card X, X)" "\<lambda>(_, X). X"])
          (auto simp: case_prod_unfold card_gt_0_iff intro: finite_subset[of _ "{..<n}"])
     finally show ?thesis .
   qed
 
   \<comment> \<open>Clearly, @{term A} is nonzero, since the empty set sums to 0.\<close>
   have "A > 0"
   proof -
     have "{} \<in> {X\<in>Pow {..<n}. root' X = 0}"
       by (auto simp: root'_def)
     thus ?thesis by (auto simp: A_def card_gt_0_iff)
   qed
 
   \<comment> \<open>Since $e^{i\pi} + 1 = 0$, we know the following:\<close>
   have "0 = (\<Prod>i<n. exp (root i) + 1)"
     using idx by force
   \<comment> \<open>We rearrange this product of sums into a sum of products and collect all summands that are
       1 into a separate sum, which we call @{term A}:\<close>
   also have "\<dots> = (\<Sum>X\<in>Pow {..<n}. \<Prod>i\<in>X. exp (root i))"
     by (subst prod_add) auto
   also have "\<dots> = (\<Sum>X\<in>Pow {..<n}. exp (root' X))"
     by (intro sum.cong refl, subst exp_sum [symmetric])
        (auto simp: root'_def intro: finite_subset[of _ "{..<n}"])
   also have "Pow {..<n} = {X\<in>Pow {..<n}. root' X \<noteq> 0} \<union> {X\<in>Pow {..<n}. root' X = 0}"
     by auto
   also have "(\<Sum>X\<in>\<dots>. exp (root' X)) = (\<Sum>X | X \<subseteq> {..<n} \<and> root' X \<noteq> 0. exp (root' X)) +
                                        (\<Sum>X | X \<subseteq> {..<n} \<and> root' X = 0. exp (root' X))"
     by (subst sum.union_disjoint) auto
   also have "(\<Sum>X | X \<subseteq> {..<n} \<and> root' X = 0. exp (root' X)) = of_nat A"
     by (simp add: A_def)
   \<comment> \<open>Finally, we obtain the fact that the sum of $\exp(u)$ with $u$ ranging over all the non-zero
       roots of @{term P'} is a negative integer.\<close>
   finally have eq: "(\<Sum>X | X \<subseteq> {..<n} \<and> root' X \<noteq> 0. exp (root' X)) = -of_nat A"
     by (simp add: add_eq_0_iff2)
 
   \<comment> \<open>Next, we show that \<open>P'\<close> is a rational polynomial since it can be written as a symmetric
       polynomial expression (with rational coefficients) in the roots of \<open>p\<close>.\<close>
   define ratpolys where "ratpolys = {p::complex poly. \<forall>i. poly.coeff p i \<in> \<rat>}"
   have ratpolysI: "p \<in> ratpolys" if "\<And>i. poly.coeff p i \<in> \<rat>" for p
     using that by (auto simp: ratpolys_def)
 
   have "P' \<in> ratpolys"
   proof -
     define Pmv :: "nat \<Rightarrow> complex poly mpoly"
       where "Pmv = (\<lambda>i. \<Prod>X | X \<subseteq> {..<n} \<and> card X = i. Const ([:0,1:]) -
                           (\<Sum>i\<in>X. monom (Poly_Mapping.single i 1) 1))"
     define P'mv where "P'mv = (\<Prod>i\<in>{0<..n}. Pmv i)"
     have "insertion (\<lambda>i. [:root i:]) P'mv \<in> ratpolys"
     proof (rule symmetric_poly_of_roots_in_subring[where l = "\<lambda>x. [:x:]"])
       show "ring_closed ratpolys"
         by standard (auto simp: ratpolys_def coeff_mult)
       then interpret ring_closed ratpolys .
       show "\<forall>m. coeff P'mv m \<in> ratpolys"
         by (auto simp: P'mv_def Pmv_def coeff_monom when_def mpoly_coeff_Const coeff_pCons' ratpolysI
                  intro!: coeff_prod_closed minus_closed sum_closed uminus_closed)
       show "\<forall>i. [:poly.coeff (of_int_poly p) i:] \<in> ratpolys"
         by (intro ratpolysI allI) (auto simp: coeff_pCons')
       show "[:inverse (of_int (Polynomial.lead_coeff p)):] *
               [:of_int (Polynomial.lead_coeff p) :: complex:] = 1"
         using \<open>p \<noteq> 0\<close> by (auto intro!: poly_eqI simp: field_simps)
     next
       have "symmetric_mpoly {..<n} (Pmv k)" for k
         unfolding symmetric_mpoly_def
       proof safe
         fix \<pi> :: "nat \<Rightarrow> nat" assume \<pi>: "\<pi> permutes {..<n}"
         hence "mpoly_map_vars \<pi> (Pmv k) =
                  (\<Prod>X | X \<subseteq> {..<n} \<and> card X = k. Const [:0, 1:] -
                     (\<Sum>x\<in>X. MPoly_Type.monom (Poly_Mapping.single (\<pi> x) (Suc 0)) 1))"
           by (simp add: Pmv_def permutes_bij)
         also have "\<dots> = (\<Prod>X | X \<subseteq> {..<n} \<and> card X = k. Const [:0, 1:] -
                           (\<Sum>x\<in>\<pi>`X. MPoly_Type.monom (Poly_Mapping.single x (Suc 0)) 1))"
           using \<pi> by (subst sum.reindex) (auto simp: permutes_inj_on)
         also have "\<dots> = (\<Prod>X \<in> (\<lambda>X. \<pi>`X)`{X. X \<subseteq> {..<n} \<and> card X = k}. Const [:0, 1:] -
                           (\<Sum>x\<in>X. MPoly_Type.monom (Poly_Mapping.single x (Suc 0)) 1))"
           by (subst prod.reindex) (auto intro!: inj_on_image permutes_inj_on[OF \<pi>])
         also have "(\<lambda>X. \<pi>`X)`{X. X \<subseteq> {..<n} \<and> card X = k} = {X. X \<subseteq> \<pi> ` {..<n} \<and> card X = k}"
           using \<pi> by (subst image_image_fixed_card_subset) (auto simp: permutes_inj_on)
         also have "\<pi> ` {..<n} = {..<n}"
           by (intro permutes_image \<pi>)
         finally show "mpoly_map_vars \<pi> (Pmv k) = Pmv k" by (simp add: Pmv_def)
       qed
       thus "symmetric_mpoly {..<n} P'mv"
         unfolding P'mv_def by (intro symmetric_mpoly_prod) auto
     next
       show vars_P'mv: "vars P'mv \<subseteq> {..<n}"
         unfolding P'mv_def Pmv_def
         by (intro order.trans[OF vars_prod] UN_least order.trans[OF vars_diff]
                    Un_least order.trans[OF vars_sum] order.trans[OF vars_monom_subset]) auto
     qed (insert root, auto intro!: ratpolysI simp: coeff_pCons')
     also have "insertion (\<lambda>i. [:root i:]) (Pmv k) = P k" for k
       by (simp add: Pmv_def insertion_prod insertion_diff insertion_sum root'_def P_def
                     sum_to_poly del: insertion_monom)
       (* TODO: insertion_monom should not be a simp rule *)
     hence "insertion (\<lambda>i. [:root i:]) P'mv = P'"
       by (simp add: P'mv_def insertion_prod P'_def)
     finally show "P' \<in> ratpolys" .
   qed
 
   \<comment> \<open>We clear the denominators and remove all powers of $X$ from @{term P'} to obtain a new
       integer polynomial \<open>Q\<close>.\<close>
   define Q' where "Q' = (\<Prod>X\<in>Roots'. [:- root' X, 1:])"
   have "P' = (\<Prod>X\<in>Pow {..<n}-{{}}. [:-root' X, 1:])"
     by (simp add: P'_altdef)
   also have "Pow {..<n}-{{}} = Roots' \<union>
                {X. X \<in> Pow {..<n} - {{}} \<and> root' X = 0}" by (auto simp: root'_def Roots'_def)
   also have "(\<Prod>X\<in>\<dots>. [:-root' X, 1:]) =
                Q' * [:0, 1:] ^ card {X. X \<subseteq> {..<n} \<and> X \<noteq> {} \<and> root' X = 0}"
     by (subst prod.union_disjoint) (auto simp: Q'_def Roots'_def)
   also have "{X. X \<subseteq> {..<n} \<and> X \<noteq> {} \<and> root' X = 0} = {X. X \<subseteq> {..<n} \<and> root' X = 0} - {{}}"
     by auto
   also have "card \<dots> = A - 1"  unfolding A_def
     by (subst card_Diff_singleton) (auto simp: root'_def)
   finally have Q': "P' = Polynomial.monom 1 (A - 1) * Q'"
     by (simp add: Polynomial.monom_altdef)
   have degree_Q': "Polynomial.degree P' = Polynomial.degree Q' + (A - 1)"
     by (subst Q')
        (auto simp: Q'_def Roots'_def degree_mult_eq Polynomial.degree_monom_eq degree_prod_eq)
 
   have "\<forall>i. poly.coeff Q' i \<in> \<rat>"
   proof
     fix i :: nat
     have "poly.coeff Q' i = Polynomial.coeff P' (i + (A - 1))"
       by (simp add: Q' Polynomial.coeff_monom_mult)
     also have "\<dots> \<in> \<rat>" using \<open>P' \<in> ratpolys\<close> by (auto simp: ratpolys_def)
     finally show "poly.coeff Q' i \<in> \<rat>" .
   qed
   from ratpoly_to_intpoly[OF this] obtain c Q
     where [simp]: "c \<noteq> 0" and Q: "Q' = Polynomial.smult (inverse (of_nat c)) (of_int_poly Q)"
     by metis
   have [simp]: "Q \<noteq> 0" using Q Q' by auto
   have Q': "of_int_poly Q = Polynomial.smult (of_nat c) Q'"
     using Q by simp
   have degree_Q: "Polynomial.degree Q = Polynomial.degree Q'"
     by (subst Q) auto
   have "Polynomial.lead_coeff (of_int_poly Q :: complex poly) = c"
     by (subst Q') (simp_all add: degree_Q Q'_def lead_coeff_prod)
   hence lead_coeff_Q: "Polynomial.lead_coeff Q = int c"
     using of_int_eq_iff[of "Polynomial.lead_coeff Q" "of_nat c"] by (auto simp del: of_int_eq_iff)  
   have Q_decompose: "of_int_poly Q =
                Polynomial.smult (of_nat c) (\<Prod>X\<in>Roots'. [:- root' X, 1:])"
     by (subst Q') (auto simp: Q'_def lead_coeff_Q)
   have "poly (of_int_poly Q) (\<i> * pi) = 0"
     using \<open>{idx} \<in> Roots'\<close> \<open>finite Roots'\<close> idx 
     by (force simp: root'_def Q_decompose poly_prod)
   have degree_Q: "Polynomial.degree (of_int_poly Q :: complex poly) = card Roots'"
     by (subst Q') (auto simp: Q'_def degree_prod_eq)
   have "poly (of_int_poly Q) (0 :: complex) \<noteq> 0"
     by (subst Q') (auto simp: Q'_def Roots'_def poly_prod)
   hence [simp]: "poly Q 0 \<noteq> 0" by simp
   have [simp]: "poly (of_int_poly Q) (root' Y) = 0" if "Y \<in> Roots'" for Y
     using that \<open>finite Roots'\<close> by (auto simp: Q' Q'_def poly_prod)
 
   \<comment> \<open>We find some closed ball that contains all the roots of @{term Q}.\<close>
   define r where "r = Polynomial.degree Q"
   have "r > 0" using degree_Q card_Roots' by (auto simp: r_def)
   define Radius where "Radius = Max ((\<lambda>Y. norm (root' Y)) ` Roots')"
   have Radius: "norm (root' Y) \<le> Radius" if "Y \<in> Roots'" for Y
     using \<open>finite Roots'\<close> that by (auto simp: Radius_def)
   from Radius[of "{idx}"] have "Radius \<ge> pi"
     using idx by (auto simp: Roots'_def norm_mult root'_def)
   hence Radius_nonneg: "Radius \<ge> 0" and "Radius > 0" using pi_gt3 by linarith+
 
   \<comment> \<open>Since this ball is compact, @{term Q} is bounded on it. We obtain such a bound.\<close>
   have "compact (poly (of_int_poly Q :: complex poly) ` cball 0 Radius)"
     by (intro compact_continuous_image continuous_intros) auto
   then obtain Q_ub
     where Q_ub: "Q_ub > 0" 
                 "\<And>u :: complex. u \<in> cball 0 Radius \<Longrightarrow> norm (poly (of_int_poly Q) u) \<le> Q_ub"
     by (auto dest!: compact_imp_bounded simp: bounded_pos cball_def)
 
   \<comment> \<open>Using this, define another upper bound that we will need later.\<close>
   define fp_ub
     where "fp_ub = (\<lambda>p. \<bar>c\<bar> ^ (r * p - 1) / fact (p - 1) * (Radius ^ (p - 1) * Q_ub ^ p))"
   have fp_ub_nonneg: "fp_ub p \<ge> 0" for p
     unfolding fp_ub_def using \<open>Radius \<ge> 0\<close> Q_ub
     by (intro mult_nonneg_nonneg divide_nonneg_pos zero_le_power) auto
   define C where "C = card Roots' * Radius * exp Radius"
 
   \<comment> \<open>We will now show that any sufficiently large prime number leads to
       \<open>C * fp_ub p \<ge> 1\<close>, from which we will then derive a contradiction.\<close>
   define primes_at_top where "primes_at_top = inf_class.inf sequentially (principal {p. prime p})"
   have "eventually (\<lambda>p. \<forall>x\<in>{nat \<bar>poly Q 0\<bar>, c, A}. p > x) sequentially"
     by (intro eventually_ball_finite ballI eventually_gt_at_top) auto
   hence "eventually (\<lambda>p. \<forall>x\<in>{nat \<bar>poly Q 0\<bar>, c, A}. p > x) primes_at_top"
     unfolding primes_at_top_def eventually_inf_principal by eventually_elim auto
   moreover have "eventually (\<lambda>p. prime p) primes_at_top"
     by (auto simp: primes_at_top_def eventually_inf_principal)
   ultimately have "eventually (\<lambda>p. C * fp_ub p \<ge> 1) primes_at_top"
   proof eventually_elim
     case (elim p)
     hence p: "prime p" "p > nat \<bar>poly Q 0\<bar>" "p > c" "p > A" by auto
     hence "p > 1" by (auto dest: prime_gt_1_nat)
 
     \<comment> \<open>We define the polynomial $f(X) = \frac{c^s}{(p-1)!} X^{p-1} Q(X)^p$, where $c$ is
         the leading coefficient of $Q$. We also define $F(X)$ to be the sum of all its
         derivatives.\<close>
     define s where "s = r * p - 1"
     define fp :: "complex poly"
       where "fp = Polynomial.smult (of_nat c ^ s / fact (p - 1))
                     (Polynomial.monom 1 (p - 1) * of_int_poly Q ^ p)"
     define Fp where "Fp = (\<Sum>i\<le>s+p. (pderiv ^^ i) fp)"
     define f F where "f = poly fp" and "F = poly Fp"
     have degree_fp: "Polynomial.degree fp = s + p" using degree_Q card_Roots' \<open>p > 1\<close>
       by (simp add: fp_def s_def degree_mult_eq degree_monom_eq
                     degree_power_eq r_def algebra_simps)
 
     \<comment> \<open>Using the same argument as in the case of the transcendence of $e$, we now 
         consider the function
         \[I(u) := e^u F(0) - F(u) = u \int\limits_0^1 e^{(1-t)x} f(tx)\,\textrm{d}t\]
         whose absolute value can be bounded with a standard ``maximum times length'' estimate
         using our upper bound on $f$. All of this can be reused from the proof for $e$, so
         there is not much to do here. In particular, we will look at $\sum I(x_i)$ with the
         $x_i$ ranging over the roots of $Q$ and bound this sum in two different ways.\<close>
     interpret lindemann_weierstrass_aux fp .
     have I_altdef: "I = (\<lambda>u. exp u * F 0 - F u)"
       by (intro ext) (simp add: I_def degree_fp F_def Fp_def poly_sum)
 
     \<comment> \<open>We show that @{term fp_ub} is indeed an upper bound for $f$.\<close>
     have fp_ub:  "norm (poly fp u) \<le> fp_ub p" if "u \<in> cball 0 Radius" for u
     proof -
       have "norm (poly fp u) = \<bar>c\<bar> ^ (r * p - 1) / fact (p - 1) * (norm u ^ (p - 1) *
                                  norm (poly (of_int_poly Q) u) ^ p)"
         by (simp add: fp_def f_def s_def norm_mult poly_monom norm_divide norm_power)
       also have "\<dots> \<le> fp_ub p"
         unfolding fp_ub_def using that Q_ub \<open>Radius \<ge> 0\<close>
         by (intro mult_left_mono[OF mult_mono] power_mono zero_le_power) auto
       finally show ?thesis .
     qed    
 
     \<comment> \<open>We now show that the following sum is an integer multiple of $p$. This argument again
         uses the fundamental theorem of symmetric functions, exploiting that the inner sums are
         symmetric over the roots of $Q$.\<close>
     have "(\<Sum>i=p..s+p. \<Sum>Y\<in>Roots'. poly ((pderiv ^^ i) fp) (root' Y)) / p \<in> \<int>"
     proof (subst sum_divide_distrib, intro Ints_sum[of "{a..b}" for a b])
       fix i assume i: "i \<in> {p..s+p}"
       then obtain roots' where roots': "distinct roots'" "set roots' = Roots'"
         using finite_distinct_list \<open>finite Roots'\<close> by metis
       define l where "l = length roots'"
       define fp' where "fp' = (pderiv ^^ i) fp"
       define d where "d = Polynomial.degree fp'"
       \<comment> \<open>We define a multivariate polynomial for the inner sum $\sum f(x_i)/p$ in order
           to show that it is indeed a symmetric function over the $x_i$.\<close>
       define R where "R = (smult (1 / of_nat p) (\<Sum>k\<le>d. \<Sum>i<l. smult (poly.coeff fp' k)
                              (monom (Poly_Mapping.single i k) (1 / of_int (c ^ k)))) :: complex mpoly)"
 
       \<comment> \<open>The $j$-th coefficient of the $i$-th derivative of $f$ are integer multiples
           of $c^j p$ since $i \geq p$.\<close>
       have integer: "poly.coeff fp' j / (of_nat c ^ j * of_nat p) \<in> \<int>" if "j \<le> d" for j
       proof -
         define fp'' where "fp'' = Polynomial.monom 1 (p - 1) * Q ^ p"
         define x
           where "x = c ^ s * poly.coeff ((pderiv ^^ i) (Polynomial.monom 1 (p - 1) * Q ^ p)) j"
         have "[:fact p:] dvd ([:fact i:] :: int poly)" using i
           by (auto intro: fact_dvd)
         also have "[:fact i:] dvd ((pderiv ^^ i) (Polynomial.monom 1 (p - 1) * Q ^ p))"
           by (rule fact_dvd_higher_pderiv)
         finally have "c ^ j * fact p dvd x" unfolding x_def of_nat_mult using that i
           by (intro mult_dvd_mono)
              (auto intro!: le_imp_power_dvd simp: s_def d_def fp'_def degree_higher_pderiv degree_fp)
         hence "of_int x / (of_int (c ^ j * fact p) :: complex) \<in> \<int>"
           by (intro of_int_divide_in_Ints) auto
         also have "of_int x / (of_int (c ^ j * fact p) :: complex) =
                      poly.coeff fp' j / (of_nat c ^ j * of_nat p)" using \<open>p > 1\<close>
           by (auto simp: fact_reduce[of p] fp'_def fp_def higher_pderiv_smult x_def field_simps
                    simp flip: coeff_of_int_poly higher_pderiv_of_int_poly)
         finally show ?thesis .
       qed
 
       \<comment> \<open>Evaluating $R$ yields is an integer since it is symmetric.\<close>
       have "insertion (\<lambda>i. c * root' (roots' ! i)) R \<in> \<int>"
       proof (intro symmetric_poly_of_roots_in_subring_monic allI)
         define Q' where "Q' = of_int_poly Q \<circ>\<^sub>p [:0, 1 / of_nat c :: complex:]"
         show "symmetric_mpoly {..<l} R" unfolding R_def
           by (intro symmetric_mpoly_smult symmetric_mpoly_sum[of "{..d}"] symmetric_mpoly_symmetric_sum)
              (simp_all add: mpoly_map_vars_monom permutes_bij permutep_single bij_imp_bij_inv permutes_inv_inv)
         show "MPoly_Type.coeff R m \<in> \<int>" for m unfolding R_def coeff_sum coeff_smult sum_distrib_left
           using integer by (auto simp: R_def coeff_monom when_def intro!: Ints_sum)
         show "vars R \<subseteq> {..<l}" unfolding R_def
           by (intro order.trans[OF vars_smult] order.trans[OF vars_sum] UN_least
                     order.trans[OF vars_monom_subset]) auto
         show "ring_closed \<int>" by standard auto
   
         have "(\<Prod>i<l. [:- (of_nat c * root' (roots' ! i)), 1:]) =
                 (\<Prod>Y\<leftarrow>roots'. [:- (of_nat c * root' Y), 1:])"
           by (subst prod_list_prod_nth) (auto simp: atLeast0LessThan l_def)
         also have "\<dots> = (\<Prod>Y\<in>Roots'. [:- (of_nat c * root' Y), 1:])"
           using roots' by (subst prod.distinct_set_conv_list [symmetric]) auto
         also have "\<dots> = (\<Prod>Y\<in>Roots'. Polynomial.smult (of_nat c) ([:-root' Y, 1:])) \<circ>\<^sub>p [:0, 1 / c:]"
           by (simp add: pcompose_prod pcompose_pCons)
         also have "(\<Prod>Y\<in>Roots'. Polynomial.smult (of_nat c) ([:-root' Y, 1:])) =
                      Polynomial.smult (of_nat c ^ card Roots') (\<Prod>Y\<in>Roots'. [:-root' Y, 1:])"
           by (subst prod_smult) auto
         also have "\<dots> = Polynomial.smult (of_nat c ^ (card Roots' - 1))
                           (Polynomial.smult c (\<Prod>Y\<in>Roots'. [:-root' Y, 1:]))"
           using \<open>finite Roots'\<close> and \<open>Roots' \<noteq> {}\<close>
           by (subst power_diff) (auto simp: Suc_le_eq card_gt_0_iff)
         also have "Polynomial.smult c (\<Prod>Y\<in>Roots'. [:-root' Y, 1:]) = of_int_poly Q"
           using Q_decompose by simp
         finally show "Polynomial.smult (of_nat c ^ (card Roots' - 1)) Q' =
                         (\<Prod>i<l. [:- (of_nat c * root' (roots' ! i)), 1:])"
           by (simp add: pcompose_smult Q'_def)
         fix i :: nat
         show "poly.coeff (Polynomial.smult (of_nat c ^ (card Roots' - 1)) Q') i \<in> \<int>"
         proof (cases i "Polynomial.degree Q" rule: linorder_cases)
           case greater
           thus ?thesis by (auto simp: Q'_def coeff_pcompose_linear coeff_eq_0)
         next
           case equal
           thus ?thesis using \<open>Roots' \<noteq> {}\<close> degree_Q card_Roots' lead_coeff_Q
             by (auto simp: Q'_def coeff_pcompose_linear lead_coeff_Q power_divide power_diff)
         next
           case less
           have "poly.coeff (Polynomial.smult (of_nat c ^ (card Roots' - 1)) Q') i =
                   of_int (poly.coeff Q i) * (of_int (c ^ (card Roots' - 1)) / of_int (c ^ i))"
             by (auto simp: Q'_def coeff_pcompose_linear power_divide)
           also have "\<dots> \<in> \<int>" using less degree_Q
             by (intro Ints_mult of_int_divide_in_Ints) (auto intro!: le_imp_power_dvd)
           finally show ?thesis .
         qed
       qed auto
       \<comment> \<open>Moreover, by definition, evaluating @{term R} gives us $\sum f(x_i)/p$.\<close>
       also have "insertion (\<lambda>i. c * root' (roots' ! i)) R =
                    (\<Sum>Y\<leftarrow>roots'. poly fp' (root' Y)) / of_nat p"
         by (simp add: insertion_sum R_def poly_altdef d_def sum_list_sum_nth atLeast0LessThan
                     l_def power_mult_distrib algebra_simps 
                     sum.swap[of _ "{..Polynomial.degree fp'}"] del: insertion_monom)
       also have "\<dots> = (\<Sum>Y\<in>Roots'. poly ((pderiv ^^ i) fp) (root' Y)) / of_nat p"
         using roots' by (subst sum_list_distinct_conv_sum_set) (auto simp: fp'_def poly_pcompose)
       finally show "\<dots> \<in> \<int>" .
     qed
     then obtain K where K: "(\<Sum>i=p..s+p. \<Sum>Y\<in>Roots'. 
                                poly ((pderiv ^^ i) fp) (root' Y)) = of_int K * p"
       using \<open>p > 1\<close> by (auto elim!: Ints_cases simp: field_simps)
 
     \<comment> \<open>Next, we show that $F(0)$ is an integer and coprime to $p$.\<close>
     obtain F0 :: int where F0: "F 0 = of_int F0" "coprime (int p) F0"
     proof -
       have "(\<Sum>i=p..s + p. poly ((pderiv ^^ i) fp) 0) / of_nat p \<in> \<int>"
         unfolding sum_divide_distrib
       proof (intro Ints_sum)
         fix i assume i: "i \<in> {p..s+p}"
         hence "fact p dvd poly ((pderiv ^^ i) ([:0, 1:] ^ (p - 1) * Q ^ p)) 0"
           by (intro fact_dvd_poly_higher_pderiv_aux') auto
         then obtain k where k: "poly ((pderiv ^^ i) ([:0, 1:] ^ (p - 1) * Q ^ p)) 0 = k * fact p"
           by auto
   
         have "(pderiv ^^ i) fp = Polynomial.smult (of_nat c ^ s / fact (p - 1))
                 (of_int_poly ((pderiv ^^ i) ([:0, 1:] ^ (p - 1) * Q ^ p)))"
           by (simp add: fp_def higher_pderiv_smult Polynomial.monom_altdef
                    flip: higher_pderiv_of_int_poly)
         also have "poly \<dots> 0 / of_nat p = of_int (c ^ s * k)"
           using k \<open>p > 1\<close> by (simp add: fact_reduce[of p])
         also have "\<dots> \<in> \<int>" by simp
         finally show "poly ((pderiv ^^ i) fp) 0 / of_nat p \<in> \<int>" .
       qed
       then obtain S where S: "(\<Sum>i=p..s + p. poly ((pderiv ^^ i) fp) 0) = of_int S * p"
         using \<open>p > 1\<close> by (auto elim!: Ints_cases simp: field_simps)
   
       have "F 0 = (\<Sum>i\<le>s + p. poly ((pderiv ^^ i) fp) 0)"
         by (auto simp: F_def Fp_def poly_sum)
       also have "\<dots> = (\<Sum>i\<in>insert (p - 1) {p..s + p}. poly ((pderiv ^^ i) fp) 0)"
       proof (intro sum.mono_neutral_right ballI)
         fix i assume i: "i \<in> {..s + p} - insert (p - 1) {p..s + p}"
         hence "i < p - 1" by auto
         have "Polynomial.monom 1 (p - 1) dvd fp"
           by (auto simp: fp_def intro: dvd_smult)
         with i show "poly ((pderiv ^^ i) fp) 0 = 0"
           by (intro poly_higher_pderiv_aux1'[of _ "p - 1"]) (auto simp: Polynomial.monom_altdef)
       qed auto
       also have "\<dots> = poly ((pderiv ^^ (p - 1)) fp) 0 + of_int S * of_nat p"
         using \<open>p > 1\<close> S by (subst sum.insert) auto
       also have "poly ((pderiv ^^ (p - 1)) fp) 0 = of_int (c ^ s * poly Q 0 ^ p)"
         using poly_higher_pderiv_aux2[of "p - 1" 0 "of_int_poly Q ^ p :: complex poly"]
         by (simp add: fp_def higher_pderiv_smult Polynomial.monom_altdef)
       finally have "F 0 = of_int (S * int p + c ^ s * poly Q 0 ^ p)"
         by simp
       moreover have "coprime p c" "coprime (int p) (poly Q 0)"
         using p by (auto intro!: prime_imp_coprime dest: dvd_imp_le_int[rotated])
       hence "coprime (int p) (c ^ s * poly Q 0 ^ p)"
         by auto
       hence "coprime (int p) (S * int p + c ^ s * poly Q 0 ^ p)"
         unfolding coprime_iff_gcd_eq_1 gcd_add_mult by auto
       ultimately show ?thesis using that[of "S * int p + c ^ s * poly Q 0 ^ p"] by blast
     qed
 
     \<comment> \<open>Putting everything together, we have shown that $\sum I(x_i)$ is an integer coprime
         to $p$, and therefore a nonzero integer, and therefore has an absolute value of at least 1.\<close>
     have "(\<Sum>Y\<in>Roots'. I (root' Y)) = F 0 * (\<Sum>Y\<in>Roots'. exp (root' Y)) - (\<Sum>Y\<in>Roots'. F (root' Y))"
       by (simp add: I_altdef sum_subtractf sum_distrib_left sum_distrib_right algebra_simps)
     also have "\<dots> = -(of_int (F0 * int A) +
                       (\<Sum>i\<le>s+p. \<Sum>Y\<in>Roots'. poly ((pderiv ^^ i) fp) (root' Y)))"
       using F0 by (simp add: Roots'_def eq F_def Fp_def poly_sum sum.swap[of _ "{..s+p}"])
     also have "(\<Sum>i\<le>s+p. \<Sum>Y\<in>Roots'. poly ((pderiv ^^ i) fp) (root' Y)) =
                  (\<Sum>i=p..s+p. \<Sum>Y\<in>Roots'. poly ((pderiv ^^ i) fp) (root' Y))"
     proof (intro sum.mono_neutral_right ballI sum.neutral)
       fix i Y assume i: "i \<in> {..s+p} - {p..s+p}" and Y: "Y \<in> Roots'"
       have "[:-root' Y, 1:] ^ p dvd of_int_poly Q ^ p"
         by (intro dvd_power_same) (auto simp: dvd_iff_poly_eq_0 Y)
       hence "[:-root' Y, 1:] ^ p dvd fp"
         by (auto simp: fp_def intro!: dvd_smult)
       thus "poly ((pderiv ^^ i) fp) (root' Y) = 0"
         using i by (intro poly_higher_pderiv_aux1') auto
     qed auto
     also have "\<dots> = of_int (K * int p)" using K by simp
     finally have "(\<Sum>Y\<in>Roots'. I (root' Y)) = -of_int (K * int p + F0 * int A)"
       by simp
     moreover have "coprime p A"
       using p \<open>A > 0\<close> by (intro prime_imp_coprime) (auto dest!: dvd_imp_le)
     hence "coprime (int p) (F0 * int A)"
       using F0 by auto
     hence "coprime (int p) (K * int p + F0 * int A)"
       using F0 unfolding coprime_iff_gcd_eq_1 gcd_add_mult by auto
     hence "K * int p + F0 * int A \<noteq> 0"
       using p by (intro notI) auto
     hence "norm (-of_int (K * int p + F0 * int A) :: complex) \<ge> 1"
       unfolding norm_minus_cancel norm_of_int by linarith
     ultimately have "1 \<le> norm (\<Sum>Y\<in>Roots'. I (root' Y))" by metis
 
     \<comment> \<open>The M--L bound on the integral gives us an upper bound:\<close>
     also have "norm (\<Sum>Y\<in>Roots'. I (root' Y)) \<le>
                  (\<Sum>Y\<in>Roots'. norm (root' Y) * exp (norm (root' Y)) * fp_ub p)"
     proof (intro sum_norm_le lindemann_weierstrass_integral_bound fp_ub fp_ub_nonneg)
       fix Y u assume *: "Y \<in> Roots'" "u \<in> closed_segment 0 (root' Y)"
       hence "closed_segment 0 (root' Y) \<subseteq> cball 0 Radius"
         using \<open>Radius \<ge> 0\<close> Radius[of Y] by (intro closed_segment_subset) auto
       with * show "u \<in> cball 0 Radius" by auto
     qed
     also have "\<dots> \<le> (\<Sum>Y\<in>Roots'. Radius * exp (Radius) * fp_ub p)"
       using Radius by (intro sum_mono mult_right_mono mult_mono fp_ub_nonneg \<open>Radius \<ge> 0\<close>) auto
     also have "\<dots> = C * fp_ub p" by (simp add: C_def)
     finally show "1 \<le> C * fp_ub p" .
   qed
 
   \<comment> \<open>It now only remains to show that this inequality is inconsistent for large $p$.
       This is obvious, since the upper bound is an exponential divided by a factorial and 
       therefore clearly tends to zero.\<close>
   have "(\<lambda>p. C * fp_ub p) \<in> \<Theta>(\<lambda>p. (C / (Radius * \<bar>c\<bar>)) * (p / 2 ^ p) *
                                      ((2 * \<bar>c\<bar> ^ r * Radius * Q_ub) ^ p / fact p))"
     (is "_ \<in> \<Theta>(?f)") using degree_Q card_Roots' \<open>Radius > 0\<close>
     by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 0]])
        (auto simp: fact_reduce power_mult [symmetric] r_def
                    fp_ub_def power_diff power_mult_distrib)
   also have "?f \<in> o(\<lambda>p. 1 * 1 * 1)"
   proof (intro landau_o.big_small_mult landau_o.big_mult)
     have "(\<lambda>x. (real_of_int (2 * \<bar>c\<bar> ^ r) * Radius * Q_ub) ^ x / fact x) \<longlonglongrightarrow> 0"
       by (intro power_over_fact_tendsto_0)
     thus "(\<lambda>x. (real_of_int (2 * \<bar>c\<bar> ^ r) * Radius * Q_ub) ^ x / fact x) \<in> o(\<lambda>x. 1)"
       by (intro smalloI_tendsto) auto
   qed real_asymp+
   finally have "(\<lambda>p. C * fp_ub p) \<in> o(\<lambda>_. 1)" by simp
   from smalloD_tendsto[OF this] have "(\<lambda>p. C * fp_ub p) \<longlonglongrightarrow> 0" by simp
   hence "eventually (\<lambda>p. C * fp_ub p < 1) at_top"
     by (intro order_tendstoD) auto
   hence "eventually (\<lambda>p. C * fp_ub p < 1) primes_at_top"
     unfolding primes_at_top_def eventually_inf_principal by eventually_elim auto
   moreover note \<open>eventually (\<lambda>p. C * fp_ub p \<ge> 1) primes_at_top\<close>
   \<comment> \<open>We therefore have a contradiction for any sufficiently large prime.\<close>
   ultimately have "eventually (\<lambda>p. False) primes_at_top"
     by eventually_elim auto
 
   \<comment> \<open>Since sufficiently large primes always exist, this concludes the theorem.\<close>
   moreover have "frequently (\<lambda>p. prime p) sequentially"
     using primes_infinite by (simp add: cofinite_eq_sequentially[symmetric] Inf_many_def)
   ultimately show False
     by (auto simp: frequently_def eventually_inf_principal primes_at_top_def)
 qed
 
 theorem transcendental_pi: "\<not>algebraic pi"
   using transcendental_i_pi by (simp add: algebraic_times_i_iff)
 
 end
\ No newline at end of file
diff --git a/thys/Prime_Number_Theorem/Prime_Number_Theorem.thy b/thys/Prime_Number_Theorem/Prime_Number_Theorem.thy
--- a/thys/Prime_Number_Theorem/Prime_Number_Theorem.thy
+++ b/thys/Prime_Number_Theorem/Prime_Number_Theorem.thy
@@ -1,826 +1,826 @@
 (*
   File:       Prime Number Theorem.thy
   Authors:    Manuel Eberl (TU München), Larry Paulson (University of Cambridge)
 
   A proof of the Prime Number Theorem and some related properties
 *)
 section \<open>The Prime Number Theorem\<close>
 theory Prime_Number_Theorem
 imports 
   Newman_Ingham_Tauberian
   Prime_Counting_Functions
 begin
 
 (*<*)
 unbundle prime_counting_notation
 (*>*)
 
 subsection \<open>Constructing Newman's function\<close>
 
 text \<open>
   Starting from Mertens' first theorem, i.\,e.\ $\mathfrak M(x) = \ln x + O(1)$, we now 
   want to derive that $\mathfrak M(x) = \ln x + c + o(1)$. This result is considerably stronger
   and it implies the Prime Number Theorem quite directly.
 
   In order to do this, we define the Dirichlet series
   \[f(s) = \sum_{n=1}^\infty \frac{\mathfrak{M}(n)}{n^s}\ .\]
   We will prove that this series extends meromorphically to $\mathfrak{R}(s)\geq 1$ and
   apply Ingham's theorem to it (after we subtracted its pole at $s = 1$).
 \<close>
 definition fds_newman where
   "fds_newman = fds (\<lambda>n. complex_of_real (\<MM> n))"
 
 lemma fds_nth_newman:
   "fds_nth fds_newman n = of_real (\<MM> n)"
   by (simp add: fds_newman_def fds_nth_fds)
 
 lemma norm_fds_nth_newman:
   "norm (fds_nth fds_newman n) = \<MM> n"
   unfolding fds_nth_newman norm_of_real
   by (intro abs_of_nonneg sum_nonneg divide_nonneg_pos) (auto dest: prime_ge_1_nat)
 
 text \<open>
   The Dirichlet series $f(s) + \zeta'(s)$ has the coefficients $\mathfrak{M}(n) - \ln n$,
   so by Mertens' first theorem, $f(s) + \zeta'(s)$ has bounded coefficients.
 \<close>
 lemma bounded_coeffs_newman_minus_deriv_zeta:
   defines "f \<equiv> fds_newman + fds_deriv fds_zeta"
   shows   "Bseq (\<lambda>n. fds_nth f n)"
 proof -
   have "(\<lambda>n. \<MM> (real n) - ln (real n)) \<in> O(\<lambda>_. 1)"
     using mertens_bounded by (rule landau_o.big.compose) real_asymp
   from natfun_bigo_1E[OF this, of 1]
     obtain c where c: "c \<ge> 1" "\<And>n. \<bar>\<MM> (real n) - ln (real n)\<bar> \<le> c" by auto
 
   show ?thesis
   proof (intro BseqI[of c] allI)
     fix n :: nat
     show "norm (fds_nth f n) \<le> c"
     proof (cases "n = 0")
       case False
       hence "fds_nth f n = of_real (\<MM> n - ln n)"
         by (simp add: f_def fds_nth_newman fds_nth_deriv fds_nth_zeta scaleR_conv_of_real)
       also from \<open>n \<noteq> 0\<close> have "norm \<dots> \<le> c"
         using c(2)[of n] by (simp add: in_Reals_norm)
       finally show ?thesis .
     qed (insert c, auto)
   qed (insert c, auto)
 qed
 
 text \<open>
   A Dirichlet series with bounded coefficients converges for all $s$ with
   $\mathfrak{R}(s)>1$ and so does $\zeta'(s)$, so we can conclude that $f(s)$ does as well.
 \<close>
 lemma abs_conv_abscissa_newman: "abs_conv_abscissa fds_newman \<le> 1"
   and conv_abscissa_newman:     "conv_abscissa fds_newman \<le> 1"
 proof -
   define f where "f = fds_newman + fds_deriv fds_zeta"
   have "abs_conv_abscissa f \<le> 1"
     using bounded_coeffs_newman_minus_deriv_zeta unfolding f_def
     by (rule bounded_coeffs_imp_abs_conv_abscissa_le_1)
   hence "abs_conv_abscissa (f - fds_deriv fds_zeta) \<le> 1"
     by (intro abs_conv_abscissa_diff_leI) (auto simp: abs_conv_abscissa_deriv)
   also have "f - fds_deriv fds_zeta = fds_newman" by (simp add: f_def)
   finally show "abs_conv_abscissa fds_newman \<le> 1" .
   from conv_le_abs_conv_abscissa and this show "conv_abscissa fds_newman \<le> 1"
     by (rule order.trans)
 qed
 
 text \<open>
   We now change the order of summation to obtain an alternative form of $f(s)$ in terms of a 
   sum of Hurwitz $\zeta$ functions.
 \<close>
 lemma eval_fds_newman_conv_infsetsum:
   assumes s: "Re s > 1"
   shows   "eval_fds fds_newman s = (\<Sum>\<^sub>ap | prime p. (ln (real p) / real p) * hurwitz_zeta p s)"
           "(\<lambda>p. ln (real p) / real p * hurwitz_zeta p s) abs_summable_on {p. prime p}"
 proof -
   from s have conv: "fds_abs_converges fds_newman s"
     by (intro fds_abs_converges le_less_trans[OF abs_conv_abscissa_newman]) auto
   define f where "f = (\<lambda>n p. ln (real p) / real p / of_nat n powr s)"
 
   have eq: "(\<Sum>\<^sub>an\<in>{p..}. f n p) = ln (real p) / real p * hurwitz_zeta p s" if "prime p" for p
   proof -
     have "(\<Sum>\<^sub>an\<in>{p..}. f n p) = (\<Sum>\<^sub>ax\<in>{p..}. (ln (real p) / of_nat p) * (1 / of_nat x powr s))"
       by (simp add: f_def)
     also have "\<dots> = (ln (real p) / of_nat p) * (\<Sum>\<^sub>ax\<in>{p..}. 1 / of_nat x powr s)"
       using abs_summable_hurwitz_zeta[of s 0 p] that s
       by (intro infsetsum_cmult_right) (auto dest: prime_gt_0_nat)
     also have "(\<Sum>\<^sub>ax\<in>{p..}. 1 / of_nat x powr s) = hurwitz_zeta p s"
       using s that by (subst hurwitz_zeta_nat_conv_infsetsum(2))
                       (auto dest: prime_gt_0_nat simp: field_simps powr_minus)
     finally show ?thesis .
   qed
 
   have norm_f: "norm (f n p) = ln p / p / n powr Re s" if "prime p" for n p :: nat
     by (auto simp: f_def norm_divide norm_mult norm_powr_real_powr)
   from conv have "(\<lambda>n. norm (fds_nth fds_newman n / n powr s)) abs_summable_on UNIV"
     by (intro abs_summable_on_normI) (simp add: fds_abs_converges_altdef')
   also have "(\<lambda>n. norm (fds_nth fds_newman n / n powr s)) =
                (\<lambda>n. \<Sum>p | prime p \<and> p \<le> n. norm (f n p))"
     by (auto simp: norm_divide norm_fds_nth_newman sum_divide_distrib primes_M_def
                    prime_sum_upto_def norm_mult norm_f norm_powr_real_powr intro!: sum.cong)
   finally have summable1: "(\<lambda>(n,p). f n p) abs_summable_on (SIGMA n:UNIV. {p. prime p \<and> p \<le> n})"
     using conv by (subst abs_summable_on_Sigma_iff) auto
   also have "?this \<longleftrightarrow> (\<lambda>(p,n). f n p) abs_summable_on
                          (\<lambda>(n,p). (p,n)) ` (SIGMA n:UNIV. {p. prime p \<and> p \<le> n})"
     by (subst abs_summable_on_reindex_iff [symmetric]) (auto simp: case_prod_unfold inj_on_def)
   also have "(\<lambda>(n,p). (p,n)) ` (SIGMA n:UNIV. {p. prime p \<and> p \<le> n}) =
                (SIGMA p:{p. prime p}. {p..})" by auto
   finally have summable2: "(\<lambda>(p,n). f n p) abs_summable_on \<dots>" .
   from abs_summable_on_Sigma_project1'[OF this]
     have "(\<lambda>p. \<Sum>\<^sub>an\<in>{p..}. f n p) abs_summable_on {p. prime p}" by auto
   also have "?this \<longleftrightarrow> (\<lambda>p. ln (real p) / real p * hurwitz_zeta p s) abs_summable_on {p. prime p}"
     by (intro abs_summable_on_cong eq) auto
   finally show \<dots> .
 
   have "eval_fds fds_newman s =
           (\<Sum>\<^sub>an. \<Sum>p | prime p \<and> p \<le> n. ln (real p) / real p / of_nat n powr s)"
     using conv by (simp add: eval_fds_altdef fds_nth_newman sum_divide_distrib
                              primes_M_def prime_sum_upto_def)
   also have "\<dots> = (\<Sum>\<^sub>an. \<Sum>\<^sub>ap | prime p \<and> p \<le> n. f n p)"
     unfolding f_def by (subst infsetsum_finite) auto
   also have "\<dots> = (\<Sum>\<^sub>a(n, p) \<in> (SIGMA n:UNIV. {p. prime p \<and> p \<le> n}). f n p)"
     using summable1 by (subst infsetsum_Sigma) auto
   also have "\<dots> = (\<Sum>\<^sub>a(p, n) \<in> (\<lambda>(n,p). (p, n)) ` (SIGMA n:UNIV. {p. prime p \<and> p \<le> n}). f n p)"
     by (subst infsetsum_reindex) (auto simp: case_prod_unfold inj_on_def)
   also have "(\<lambda>(n,p). (p, n)) ` (SIGMA n:UNIV. {p. prime p \<and> p \<le> n}) =
                (SIGMA p:{p. prime p}. {p..})" by auto
   also have "(\<Sum>\<^sub>a(p,n)\<in>\<dots>. f n p) = (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>an\<in>{p..}. f n p)"
     using summable2 by (subst infsetsum_Sigma) auto
   also have "(\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>an\<in>{p..}. f n p) =
                (\<Sum>\<^sub>ap | prime p. ln (real p) / real p * hurwitz_zeta p s)"
     by (intro infsetsum_cong eq) auto
   finally show "eval_fds fds_newman s =
                   (\<Sum>\<^sub>ap | prime p. (ln (real p) / real p) * hurwitz_zeta p s)" .
 qed
 
 
 text \<open>
   We now define a meromorphic continuation of $f(s)$ on $\mathfrak{R}(s) > \frac{1}{2}$.
 
   To construct $f(s)$, we express it as
   \[f(s) = \frac{1}{z-1}\left(\bar f(s) - \frac{\zeta'(s)}{\zeta(s)}\right)\ ,\]
   where $\bar f(s)$ (which we shall call \<open>pre_newman\<close>) is a function that is analytic on
-  $\Re(s) > \frac{1}{2}$, which can be shown fairly easily using the Weierstraß M test.
+  $\Re(s) > \frac{1}{2}$, which can be shown fairly easily using the Weierstra{\ss} M test.
   
   $\zeta'(s)/\zeta(s)$ is meromorphic except for a single pole at $s = 1$ and one $k$-th order
   pole for any $k$-th order zero of $\zeta$, but for the Prime Number Theorem, we are only
   concerned with the area $\mathfrak{R}(s) \geq 1$, where $\zeta$ does not have any zeros.
 
   Taken together, this means that $f(s)$ is analytic for $\mathfrak{R}(s)\geq 1$ except for a
   double pole at $s = 1$, which we will take care of later.
 \<close>
 
 context
   fixes A :: "nat \<Rightarrow> complex \<Rightarrow> complex" and B :: "nat \<Rightarrow> complex \<Rightarrow> complex"
   defines "A \<equiv> (\<lambda>p s. (s - 1) * pre_zeta (real p) s - 
                          of_nat p / (of_nat p powr s * (of_nat p powr s - 1)))"
   defines "B \<equiv> (\<lambda>p s. of_real (ln (real p)) / of_nat p * A p s)"
 begin
 
 definition pre_newman :: "complex \<Rightarrow> complex" where
   "pre_newman s = (\<Sum>p. if prime p then B p s else 0)"
 
 definition newman where "newman s = 1 / (s - 1) * (pre_newman s - deriv zeta s / zeta s)"
 
 text \<open>
   The sum used in the definition of \<open>pre_newman\<close> converges uniformly on any disc within the
-  half-space with $\mathfrak{R}(s) > \frac{1}{2}$ by the Weierstraß M test.
+  half-space with $\mathfrak{R}(s) > \frac{1}{2}$ by the Weierstra{\ss} M test.
 \<close>
 lemma uniform_limit_pre_newman:
   assumes r: "r \<ge> 0" "Re s - r > 1 / 2"
   shows "uniform_limit (cball s r)
            (\<lambda>n s. \<Sum>p<n. if prime p then B p s else 0) pre_newman at_top"
 proof -
   from r have Re: "Re z > 1 / 2" if "dist s z \<le> r" for z
     using abs_Re_le_cmod[of "s - z"] r that
     by (auto simp: dist_norm abs_if split: if_splits)
 
   define x where "x = Re s - r" \<comment> \<open>The lower bound for the real part in the disc\<close>
   from r Re have "x > 1 / 2" by (auto simp: x_def)
 
   \<comment> \<open>The following sequence \<open>M\<close> bounds the summand, and it is obviously $O(n^{-1-\epsilon})$
       and therefore summable\<close>
   define C where "C = (norm s + r + 1) * (norm s + r) / x"
   define M where "M = (\<lambda>p::nat. ln p * (C / p powr (x + 1) + 1 / (p powr x * (p powr x - 1))))"
 
   show ?thesis unfolding pre_newman_def
   proof (intro Weierstrass_m_test_ev[OF eventually_mono[OF eventually_gt_at_top[of 1]]] ballI)
     show "summable M"
     proof (rule summable_comparison_test_bigo)
       define \<epsilon> where "\<epsilon> = min (2 * x - 1) x / 2"
       from \<open>x > 1 / 2\<close> have \<epsilon>: "\<epsilon> > 0" "1 + \<epsilon> < 2 * x" "1 + \<epsilon> < x + 1"
         by (auto simp: \<epsilon>_def min_def field_simps)
       show "M \<in> O(\<lambda>n. n powr (- 1 - \<epsilon>))" unfolding M_def distrib_left
         by (intro sum_in_bigo) (use \<epsilon> in real_asymp)+
       from \<epsilon> show "summable (\<lambda>n. norm (n powr (- 1 - \<epsilon>)))"
         by (simp add: summable_real_powr_iff)
     qed
   next
     fix p :: nat and z assume p: "p > 1" and z: "z \<in> cball s r"
     from z r Re[of z] have x: "Re z \<ge> x" "x > 1 / 2" and "Re z > 1 / 2"
       using abs_Re_le_cmod[of "s - z"] by (auto simp: x_def algebra_simps dist_norm)
     have norm_z: "norm z \<le> norm s + r"
       using z norm_triangle_ineq2[of z s] r by (auto simp: dist_norm norm_minus_commute)
     from \<open>p > 1\<close> and x and r have "M p \<ge> 0"
       by (auto simp: C_def M_def intro!: mult_nonneg_nonneg add_nonneg_nonneg divide_nonneg_pos)
 
     have bound: "norm ((z - 1) * pre_zeta p z) \<le> 
                    norm (z - 1) * (norm z / (Re z * p powr Re z))"
       using pre_zeta_bound'[of z p] p \<open>Re z > 1 / 2\<close>
       unfolding norm_mult by (intro mult_mono pre_zeta_bound) auto
 
     have "norm (B p z) = ln p / p * norm (A p z)"
       unfolding B_def using \<open>p > 1\<close> by (simp add: B_def norm_mult norm_divide)
     also have "\<dots> \<le> ln p / p * (norm (z - 1) * norm z / Re z / p powr Re z + 
                                  p / (p powr Re z * (p powr Re z - 1)))"
       unfolding A_def using \<open>p > 1\<close> and \<open>Re z > 1 / 2\<close> and bound
       by (intro mult_left_mono order.trans[OF norm_triangle_ineq4 add_mono] mult_left_mono)
          (auto simp: norm_divide norm_mult norm_powr_real_powr
                intro!: divide_left_mono order.trans[OF _ norm_triangle_ineq2])
     also have "\<dots> = ln p * (norm (z - 1) * norm z / Re z / p powr (Re z + 1) + 
                             1 / (p powr Re z * (p powr Re z - 1)))"
       using \<open>p > 1\<close> by (simp add: field_simps powr_add powr_minus)
     also have "norm (z - 1) * norm z / Re z / p powr (Re z + 1) \<le> C / p powr (x + 1)"
       unfolding C_def using r \<open>Re z > 1 / 2\<close> norm_z p x
       by (intro mult_mono frac_le powr_mono order.trans[OF norm_triangle_ineq4]) auto
     also have "1 / (p powr Re z * (p powr Re z - 1)) \<le>
                  1 / (p powr x * (p powr x - 1))" using \<open>p > 1\<close> x
       by (intro divide_left_mono mult_mono powr_mono diff_right_mono mult_pos_pos)
          (auto simp: ge_one_powr_ge_zero)
     finally have "norm (B p z) \<le> M p"
       using \<open>p > 1\<close> by (simp add: mult_left_mono M_def)
     with \<open>M p \<ge> 0\<close> show "norm (if prime p then B p z else 0) \<le> M p" by simp
   qed
 qed
 
 lemma sums_pre_newman: "Re s > 1 / 2 \<Longrightarrow> (\<lambda>p. if prime p then B p s else 0) sums pre_newman s"
   using tendsto_uniform_limitI[OF uniform_limit_pre_newman[of 0 s]] by (auto simp: sums_def)
 
 lemma analytic_pre_newman [THEN analytic_on_subset, analytic_intros]:
   "pre_newman analytic_on {s. Re s > 1 / 2}"
 proof -
   have holo: "(\<lambda>s::complex. if prime p then B p s else 0) holomorphic_on X"
     if "X \<subseteq> {s. Re s > 1 / 2}" for X and p :: nat using that
     by (cases "prime p")
        (auto intro!: holomorphic_intros simp: B_def A_def dest!: prime_gt_1_nat)
   have holo': "pre_newman holomorphic_on ball s r" if r: "r \<ge> 0" "Re s - r > 1 / 2" for s r
   proof -
     from r have Re: "Re z > 1 / 2" if "dist s z \<le> r" for z
       using abs_Re_le_cmod[of "s - z"] r that by (auto simp: dist_norm abs_if split: if_splits)
     show ?thesis
       by (rule holomorphic_uniform_limit[OF _ uniform_limit_pre_newman[of r s]])
          (insert that Re, auto intro!: always_eventually holomorphic_on_imp_continuous_on
                                        holomorphic_intros holo)
   qed
   show ?thesis unfolding analytic_on_def
   proof safe
     fix s assume "Re s > 1 / 2"
     thus "\<exists>r>0. pre_newman holomorphic_on ball s r"
       by (intro exI[of _ "(Re s - 1 / 2) / 2"] conjI holo') (auto simp: field_simps)
   qed
 qed
 
 lemma holomorphic_pre_newman [holomorphic_intros]:
   "X \<subseteq> {s. Re s > 1 / 2} \<Longrightarrow> pre_newman holomorphic_on X"
   using analytic_pre_newman by (rule analytic_imp_holomorphic)
 
 lemma eval_fds_newman:
   assumes s: "Re s > 1"
   shows   "eval_fds fds_newman s = newman s"
 proof -
   have eq: "(ln (real p) / real p) * hurwitz_zeta p s =
               1 / (s - 1) * (ln (real p) / (p powr s - 1) + B p s)"
     if p: "prime p" for p
   proof -
     have "(ln (real p) / real p) * hurwitz_zeta p s =
             ln (real p) / real p * (p powr (1 - s) / (s - 1) + pre_zeta p s)"
       using s by (auto simp add: hurwitz_zeta_def)
     also have "\<dots> = 1 / (s - 1) * (ln (real p) / (p powr s - 1) + B p s)"
       using p s by (simp add: divide_simps powr_diff B_def)
                    (auto simp: A_def field_simps dest: prime_gt_1_nat)?
     finally show ?thesis .
   qed
 
   have "(\<lambda>p. (ln (real p) / real p) * hurwitz_zeta p s) abs_summable_on {p. prime p}"
     using s by (intro eval_fds_newman_conv_infsetsum)
   hence "(\<lambda>p. 1 / (s - 1) * (ln (real p) / (p powr s - 1) + B p s))
             abs_summable_on {p. prime p}"
     by (subst (asm) abs_summable_on_cong[OF eq refl]) auto
   hence summable:
     "(\<lambda>p. ln (real p) / (p powr s - 1) + B p s) abs_summable_on {p. prime p}"
     using s by (subst (asm) abs_summable_on_cmult_right_iff) auto
 
   from s have [simp]: "s \<noteq> 1" by auto
   have "eval_fds fds_newman s =
           (\<Sum>\<^sub>ap | prime p. (ln (real p) / real p) * hurwitz_zeta p s)"
     using s by (rule eval_fds_newman_conv_infsetsum)
   also have "\<dots> = (\<Sum>\<^sub>ap | prime p. 1 / (s - 1) * (ln (real p) / (p powr s - 1) + B p s))"
     by (intro infsetsum_cong eq) auto
   also have "\<dots> = 1 / (s - 1) * (\<Sum>\<^sub>ap | prime p. ln (real p) / (p powr s - 1) + B p s)"
     (is "_ = _ * ?S") by (rule infsetsum_cmult_right[OF summable])
   also have "?S = (\<Sum>p. if prime p then 
                       ln (real p) / (p powr s - 1) + B p s else 0)"
     by (subst infsetsum_nat[OF summable]) auto
   also have "\<dots> = (\<Sum>p. (if prime p then ln (real p) / (p powr s - 1) else 0) + 
                         (if prime p then B p s else 0))"
     by (intro suminf_cong) auto
   also have "\<dots> = pre_newman s - deriv zeta s / zeta s"
     using sums_pre_newman[of s] sums_logderiv_zeta[of s] s
     by (subst suminf_add [symmetric]) (auto simp: sums_iff)
   finally show ?thesis by (simp add: newman_def)
 qed
 
 end
 
 text \<open>
   Next, we shall attempt to get rid of the pole by subtracting suitable multiples of $\zeta(s)$
   and $\zeta'(s)$. To this end, we shall first prove the following alternative definition of 
   $\zeta'(s)$:
 \<close>
 lemma deriv_zeta_eq':
   assumes "0 < Re s" "s \<noteq> 1"
   shows "deriv zeta s = deriv (\<lambda>z. pre_zeta 1 z * (z - 1)) s / (s - 1) -
                           (pre_zeta 1 s * (s - 1) + 1) / (s - 1)\<^sup>2"
     (is "_ = ?rhs")
 proof (rule DERIV_imp_deriv)
   have [derivative_intros]: "(pre_zeta 1 has_field_derivative deriv (pre_zeta 1) s) (at s)"
     by (intro holomorphic_derivI[of _ UNIV] holomorphic_intros) auto
   have *: "deriv (\<lambda>z. pre_zeta 1 z * (z - 1)) s = deriv (pre_zeta 1) s * (s - 1) + pre_zeta 1 s"
     by (subst deriv_mult)
        (auto intro!: holomorphic_on_imp_differentiable_at[of _ UNIV] holomorphic_intros)
   hence "((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative
            deriv (pre_zeta 1) s - 1 / ((s - 1) * (s - 1))) (at s)"
     using assms by (auto intro!: derivative_eq_intros)
   also have "deriv (pre_zeta 1) s - 1 / ((s - 1) * (s - 1)) = ?rhs"
     using * assms by (simp add: divide_simps power2_eq_square, simp add: field_simps)
   also have "((\<lambda>s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative ?rhs) (at s) \<longleftrightarrow>
                (zeta has_field_derivative ?rhs) (at s)"
     using assms
     by (intro has_field_derivative_cong_ev eventually_mono[OF t1_space_nhds[of _ 1]])
        (auto simp: zeta_def hurwitz_zeta_def)
   finally show \<dots> .
 qed
 
 text \<open>
   From this, it follows that $(s - 1) \zeta'(s) - \zeta'(s) / \zeta(s)$ is analytic 
   for $\mathfrak{R}(s) \geq 1$:
 \<close>
 lemma analytic_zeta_derivdiff:
   obtains a where
     "(\<lambda>z. if z = 1 then a else (z - 1) * deriv zeta z - deriv zeta z / zeta z)
           analytic_on {s. Re s \<ge> 1}" 
 proof 
   have neq: "pre_zeta 1 z * (z - 1) + 1 \<noteq> 0" if "Re z \<ge> 1" for z
     using zeta_Re_ge_1_nonzero[of z] that
     by (cases "z = 1") (auto simp: zeta_def hurwitz_zeta_def divide_simps)
   let ?g = "\<lambda>z. (1 - inverse (pre_zeta 1 z * (z - 1) + 1)) * ((z - 1) *
                 deriv ((\<lambda>u. pre_zeta 1 u * (u - 1))) z - (pre_zeta 1 z * (z - 1) + 1))"
   show "(\<lambda>z. if z = 1 then deriv ?g 1 else (z - 1) * deriv zeta z - deriv zeta z / zeta z)
           analytic_on {s. Re s \<ge> 1}" (is "?f analytic_on _")
   proof (rule pole_theorem_analytic_0)
     show "?g analytic_on {s. 1 \<le> Re s}" using neq
       by (auto intro!: analytic_intros)
   next
     show "\<exists>d>0. \<forall>w\<in>ball z d - {1}. ?g w = (w - 1) * ?f w"
       if z: "z \<in> {s. 1 \<le> Re s}" for z
     proof -
       have *: "isCont (\<lambda>z. pre_zeta 1 z * (z - 1) + 1) z"
         by (auto intro!: continuous_intros)
        obtain e where "e > 0" and e: "\<And>y. dist z y < e \<Longrightarrow> pre_zeta (Suc 0) y * (y-1) + 1 \<noteq> 0"
          using continuous_at_avoid [OF * neq[of z]] z by auto
       show ?thesis
       proof (intro exI ballI conjI)
         fix w
         assume w: "w \<in> ball z (min e 1) - {1}"
         then have "Re w > 0"
           using complex_Re_le_cmod [of "z-w"] z by (simp add: dist_norm)
         with w show "?g w = (w - 1) * (if w = 1 then deriv ?g 1 else
                         (w - 1) * deriv zeta w - deriv zeta w / zeta w)"
           by (subst (1 2) deriv_zeta_eq', 
               simp_all add: zeta_def hurwitz_zeta_def divide_simps e power2_eq_square)
              (simp_all add: algebra_simps)?
       qed (use \<open>e > 0\<close> in auto)
     qed
   qed auto
 qed
 
 text \<open>
   Finally, $f(s) + \zeta'(s) + c\zeta(s)$ is analytic.
 \<close>
 lemma analytic_newman_variant:
   obtains c a where
      "(\<lambda>z. if z = 1 then a else newman z + deriv zeta z + c * zeta z) analytic_on {s. Re s \<ge> 1}"
 proof -
   obtain c where (* -euler_mascheroni *)
     c: "(\<lambda>z. if z = 1 then c else (z - 1) * deriv zeta z - deriv zeta z / zeta z)
         analytic_on {s. Re s \<ge> 1}"
     using analytic_zeta_derivdiff by blast
   let ?g = "\<lambda>z. pre_newman z +
           (if z = 1 then c
            else (z - 1) * deriv zeta z -
                 deriv zeta z / zeta z) - (c + pre_newman 1) * (pre_zeta 1 z * (z - 1) + 1)"
   have "(\<lambda>z. if z = 1 then deriv ?g 1 else newman z + deriv zeta z + (-(c + pre_newman 1)) * zeta z)
         analytic_on {s. Re s \<ge> 1}"  (is "?f analytic_on _")
   proof (rule pole_theorem_analytic_0)
     show "?g analytic_on {s. 1 \<le> Re s}"
       by (intro c analytic_intros) auto
   next
     show "\<exists>d>0. \<forall>w\<in>ball z d - {1}. ?g w = (w - 1) * ?f w"
       if "z \<in> {s. 1 \<le> Re s}" for z using that
       by (intro exI[of _ 1], simp_all add: newman_def divide_simps zeta_def hurwitz_zeta_def)
          (auto simp: field_simps)?
   qed auto
   with that show ?thesis by blast
 qed
 
 
 subsection \<open>The asymptotic expansion of \<open>\<MM>\<close>\<close>
 
 text \<open>
   Our next goal is to show the key result that $\mathfrak{M}(x) = \ln n + c + o(1)$.
 
   As a first step, we invoke Ingham's Tauberian theorem on the function we have
   just defined and obtain that the sum
   \[\sum\limits_{n=1}^\infty \frac{\mathfrak{M}(n) - \ln n + c}{n}\]
   exists.
 \<close>
 lemma mertens_summable:
   obtains c :: real where "summable (\<lambda>n. (\<MM> n - ln n + c) / n)"
 proof -
   (* c = euler_mascheroni - pre_newman 1 *)
   from analytic_newman_variant obtain c a where
     analytic: "(\<lambda>z. if z = 1 then a else newman z + deriv zeta z + c * zeta z)
                  analytic_on {s. Re s \<ge> 1}" .
   define f where "f = (\<lambda>z. if z = 1 then a else newman z + deriv zeta z + c * zeta z)"
   have analytic: "f analytic_on {s. Re s \<ge> 1}" using analytic by (simp add: f_def)
   define F where "F = fds_newman + fds_deriv fds_zeta + fds_const c * fds_zeta"
 
   note le = conv_abscissa_add_leI conv_abscissa_deriv_le conv_abscissa_newman conv_abscissa_mult_const_left
   note intros = le le[THEN le_less_trans] le[THEN order.trans] fds_converges
   have eval_F: "eval_fds F s = f s" if s: "Re s > 1" for s
   proof -
     have "eval_fds F s = eval_fds (fds_newman + fds_deriv fds_zeta) s +
                            eval_fds (fds_const c * fds_zeta) s"
       unfolding F_def using s by (subst eval_fds_add) (auto intro!: intros)
     also have "\<dots> = f s" using s unfolding f_def
       by (subst eval_fds_add)
          (auto intro!: intros simp: eval_fds_newman eval_fds_deriv_zeta eval_fds_mult eval_fds_zeta)
     finally show ?thesis .
   qed
 
   have conv: "fds_converges F s" if "Re s \<ge> 1" for s
   proof (rule Newman_Ingham_1)
     have "(\<lambda>n. \<MM> (real n) - ln (real n)) \<in> O(\<lambda>_. 1)"
       using mertens_bounded by (rule landau_o.big.compose) real_asymp
     from natfun_bigo_1E[OF this, of 1]
       obtain c' where c': "c' \<ge> 1" "\<And>n. \<bar>\<MM> (real n) - ln (real n)\<bar> \<le> c'" by auto
     have "Bseq (fds_nth F)"
     proof (intro BseqI allI)
       fix n :: nat
       show "norm (fds_nth F n) \<le> (c' + norm c)" unfolding F_def using c'
         by (auto simp: fds_nth_zeta fds_nth_deriv fds_nth_newman scaleR_conv_of_real in_Reals_norm
                  intro!: order.trans[OF norm_triangle_ineq] add_mono)
     qed (insert c', auto intro: add_pos_nonneg)
     thus "fds_nth F \<in> O(\<lambda>_. 1)" by (simp add: natfun_bigo_iff_Bseq)
   next
     show "f analytic_on {s. Re s \<ge> 1}" by fact
   next
     show "eval_fds F s = f s" if "Re s > 1" for s using that by (rule eval_F)
   qed (insert that, auto simp: F_def intro!: intros)
   from conv[of 1] have "summable (\<lambda>n. fds_nth F n / of_nat n)"
     unfolding fds_converges_def by auto
   also have "?this \<longleftrightarrow> summable (\<lambda>n. (\<MM> n - Ln n + c) / n)"
     by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of 0]])
        (auto simp: F_def fds_nth_newman fds_nth_deriv fds_nth_zeta scaleR_conv_of_real
              intro!: sum.cong dest: prime_gt_0_nat)
   finally have "summable (\<lambda>n. (\<MM> n - Re (Ln (of_nat n)) + Re c) / n)"
     by (auto dest: summable_Re)
   also have "?this \<longleftrightarrow> summable (\<lambda>n. (\<MM> n - ln n + Re c) / n)"
     by (intro summable_cong eventually_mono[OF eventually_gt_at_top[of 0]]) (auto intro!: sum.cong)
   finally show ?thesis using that[of "Re c"] by blast
 qed
 
 text \<open>
   Next, we prove a lemma given by Newman stating that if the sum $\sum a_n / n$ exists and
   $a_n + \ln n$ is nondecreasing, then $a_n$ must tend to 0. Unfortunately, the proof is
   rather tedious, but so is the paper version by Newman.
 \<close>
 lemma sum_goestozero_lemma:
   fixes d::real
   assumes d: "\<bar>\<Sum>i = M..N. a i / i\<bar> < d" and le: "\<And>n. a n + ln n \<le> a (Suc n) + ln (Suc n)"
       and "0 < M" "M < N"
     shows "a M \<le> d * N / (real N - real M) + (real N - real M) / M \<and>
           -a N \<le> d * N / (real N - real M) + (real N - real M) / M"
 proof -
   have "0 \<le> d"
     using assms by linarith+
   then have "0 \<le> d * N / (N - M + 1)" by simp
   then have le_dN: "\<lbrakk>0 \<le> x \<Longrightarrow> x \<le> d * N / (N - M + 1)\<rbrakk> \<Longrightarrow> x \<le> d * N / (N - M + 1)" for x::real
     by linarith
   have le_a_ln: "a m + ln m \<le> a n + ln n" if "n \<ge> m" for n m
     by (rule transitive_stepwise_le) (use le that in auto)
   have *: "x \<le> b \<and> y \<le> b" if "a \<le> b" "x \<le> a" "y \<le> a" for a b x y::real
     using that by linarith
   show ?thesis
   proof (rule *)
     show "d * N / (N - M) + ln (N / M) \<le> d * N / (real N - real M) + (real N - real M) / M"
       using \<open>0 < M\<close> \<open>M < N\<close> ln_le_minus_one [of "N / M"]
       by (simp add: of_nat_diff) (simp add: divide_simps)
   next
     have "a M - ln (N / M) \<le> (d * N) / (N - M + 1)"
     proof (rule le_dN)
       assume 0: "0 \<le> a M - ln (N / M)"
       have "(Suc N - M) * (a M - ln (N / M)) / N = (\<Sum>i = M..N. (a M - ln (N / M)) / N)"
         by simp
       also have "\<dots> \<le> (\<Sum>i = M..N. a i / i)"
       proof (rule sum_mono)
         fix i
         assume i: "i \<in> {M..N}"
         with \<open>0 < M\<close> have "0 < i" by auto
         have "(a M - ln (N / M)) / N \<le> (a M - ln (N / M)) / i"
           using 0 using i \<open>0 < M\<close> by (simp add: frac_le_eq divide_simps mult_left_mono)
         also have "a M + ln (real M) \<le> a i + ln (real N)"
           by (rule order.trans[OF le_a_ln[of M i]]) (use i assms in auto)
         hence "(a M - ln (N / M)) / i \<le> a i / real i"
           using assms i by (intro divide_right_mono) (auto simp: ln_div field_simps)
         finally show "(a M - ln (N / M)) / real N \<le> a i / real i" .
       qed
       finally have "((Suc N) - M) * (a M - ln (N / M)) / N \<le> \<bar>\<Sum>i = M..N. a i / i\<bar>"
         by simp
       also have "\<dots> \<le> d" using d by simp
       finally have "((Suc N) - M) * (a M - ln (N / M)) / N \<le> d" .
       then show ?thesis
         using \<open>M < N\<close>  by (simp add: of_nat_diff field_simps)
     qed
     also have "\<dots> \<le> d * N / (N - M)"
       using assms(1,4) by (simp add: field_simps)
     finally show "a M \<le> d * N / (N - M) + ln (N / M)" by simp
   next
     have "- a N - ln (N / M) \<le> (d * N) / (N - M + 1)"
     proof (rule le_dN)
       assume 0: "0 \<le> - a N - ln (N / M)"
       have "(\<Sum>i = M..N. a i / i) \<le> (\<Sum>i = M..N. (a N + ln (N / M)) / N)"
       proof (rule sum_mono)
         fix i
         assume i: "i \<in> {M..N}"
         with \<open>0 < M\<close> have "0 < i" by auto
         have "a i + ln (real M) \<le> a N + ln (real N)"
           by (rule order.trans[OF _ le_a_ln[of i N]]) (use i assms in auto)
         hence "a i / i \<le> (a N + ln (N / M)) / i"
           using assms(3,4) by (intro divide_right_mono) (auto simp: field_simps ln_div)
         also have "\<dots> \<le> (a N + ln (N / M)) / N"
           using i \<open>i > 0\<close> 0 by (intro divide_left_mono_neg) auto
         finally show "a i / i \<le> (a N + ln (N / M)) / N" .
       qed
       also have "\<dots> = ((Suc N) - M) * (a N + ln (N / M)) / N"
         by simp
       finally have "(\<Sum>i = M..N. a i / i) \<le> (real (Suc N) - real M) * (a N + ln (N / M)) / N"
         using \<open>M < N\<close> by (simp add: of_nat_diff)
       then have "-((real (Suc N) - real M) * (a N + ln (N / M)) / N) \<le> \<bar>\<Sum>i = M..N. a i / i\<bar>"
         by linarith
       also have "\<dots> \<le> d" using d by simp
       finally have "- ((real (Suc N) - real M) * (a N + ln (N / M)) / N) \<le> d" .
       then show ?thesis
         using \<open>M < N\<close>  by (simp add: of_nat_diff field_simps)
     qed
     also have "\<dots> \<le> d * N / real (N - M)"
       using \<open>0 < M\<close> \<open>M < N\<close> \<open>0 \<le> d\<close> by (simp add: field_simps)
     finally show "-a N \<le> d * N / real (N - M) + ln (N / M)" by simp
   qed
 qed
 
 proposition sum_goestozero_theorem:
   assumes summ: "summable (\<lambda>i. a i / i)"
       and le:   "\<And>n. a n + ln n \<le> a (Suc n) + ln (Suc n)"
     shows "a \<longlonglongrightarrow> 0"
 proof (clarsimp simp: lim_sequentially)
   fix r::real
   assume "r > 0"
   have *: "\<exists>n0. \<forall>n\<ge>n0. \<bar>a n\<bar> < \<epsilon>" if \<epsilon>: "0 < \<epsilon>" "\<epsilon> < 1" for \<epsilon>
   proof -
     have "0 < (\<epsilon> / 8)\<^sup>2" using \<open>0 < \<epsilon>\<close>  by simp
     then obtain N0 where N0: "\<And>m n. m \<ge> N0 \<Longrightarrow> norm (\<Sum>k=m..n. (\<lambda>i. a i / i) k) < (\<epsilon> / 8)\<^sup>2"
       by (metis summable_partial_sum_bound summ)
     obtain N1 where "real N1 > 4 / \<epsilon>"
       using reals_Archimedean2[of "4 / \<epsilon>"] \<epsilon> by auto
     hence "N1 \<noteq> 0" and N1: "1 / real N1 < \<epsilon> / 4" using \<epsilon>
       by (auto simp: divide_simps mult_ac intro: Nat.gr0I)
 
     have "\<bar>a n\<bar> < \<epsilon>" if n: "n \<ge> 2 * N0 + N1 + 7" for n
     proof -
       define k where "k = \<lfloor>n * \<epsilon>/4\<rfloor>"
       have "n * \<epsilon> / 4 > 1" and "n * \<epsilon> / 4 \<le> n / 4" and "n / 4 < n"
         using less_le_trans[OF N1, of "n / N1 * \<epsilon> / 4"] \<open>N1 \<noteq> 0\<close> \<epsilon> n by (auto simp: field_simps)
       hence k: "k > 0" "4 * k \<le> n" "nat k < n" "(n * \<epsilon> / 4) - 1 < k" "k \<le> (n * \<epsilon> / 4)"
         unfolding k_def by linarith+
 
       have "-a n < \<epsilon>"
       proof -
         have "N0 \<le> n - nat k"
           using n k by linarith
         then have *: "\<bar>\<Sum>k = n - nat k .. n. a k / k\<bar> < (\<epsilon> / 8)\<^sup>2"
           using N0 [of "n - nat k" n] by simp
         have "-a n \<le> (\<epsilon> / 8)\<^sup>2 * n / \<lfloor>n * \<epsilon> / 4\<rfloor> + \<lfloor>n * \<epsilon> / 4\<rfloor> / (n - k)"
           using sum_goestozero_lemma [OF * le, THEN conjunct2] k by (simp add: of_nat_diff k_def)
         also have "\<dots>< \<epsilon>"
         proof -
           have "\<epsilon> / 16 * n / k < 2"
             using k by (auto simp: field_simps)
           then have "\<epsilon> * (\<epsilon> / 16 * n / k) < \<epsilon> * 2"
             using \<epsilon> mult_less_cancel_left_pos by blast
           then have "(\<epsilon> / 8)\<^sup>2 * n / k < \<epsilon> / 2"
             by (simp add: field_simps power2_eq_square)
           moreover have "k / (n - k) < \<epsilon> / 2"
           proof -
             have "(\<epsilon> + 2) * k < 4 * k" using k \<epsilon> by simp
             also have "\<dots> \<le> \<epsilon> * real n" using k by (auto simp: field_simps)
             finally show ?thesis using k by (auto simp: field_simps)
           qed
           ultimately show ?thesis unfolding k_def by linarith
         qed
         finally show ?thesis .
       qed
       moreover have "a n < \<epsilon>"
       proof -
         have "N0 \<le> n" using n k by linarith
         then have *: "\<bar>\<Sum>k = n .. n + nat k. a k / k\<bar> < (\<epsilon>/8)\<^sup>2"
           using N0 [of n "n + nat k"] by simp
         have "a n \<le> (\<epsilon>/8)\<^sup>2 * (n + nat k) / k + k / n"
           using sum_goestozero_lemma [OF * le, THEN conjunct1] k by (simp add: of_nat_diff)
         also have "\<dots>< \<epsilon>"
         proof -
           have "4 \<le> 28 * real_of_int k" using k by linarith
           then have "\<epsilon>/16 * n / k < 2" using k by (auto simp: field_simps)
           have "\<epsilon> * (real n + k) < 32 * k"
           proof -
             have "\<epsilon> * n / 4 < k + 1" by (simp add: mult.commute k_def)
             then have "\<epsilon> * n < 4 * k + 4" by (simp add: divide_simps)
             also have "\<dots> \<le> 8 * k" using k by auto
             finally have 1: "\<epsilon> * real n < 8 * k" .
             have 2: "\<epsilon> * k < k" using k \<epsilon> by simp
             show ?thesis using k add_strict_mono [OF 1 2] by (simp add: algebra_simps)
         qed
           then have "(\<epsilon> / 8)\<^sup>2 * real (n + nat k) / k < \<epsilon> / 2"
             using \<epsilon> k by (simp add: divide_simps mult_less_0_iff power2_eq_square)
           moreover have "k / n < \<epsilon> / 2"
             using k \<epsilon> by (auto simp: k_def field_simps)
           ultimately show ?thesis by linarith
         qed
         finally show ?thesis .
       qed
       ultimately show ?thesis by force
     qed
     then show ?thesis by blast
   qed
   show "\<exists>n0. \<forall>n\<ge>n0. \<bar>a n\<bar> < r"
     using * [of "min r (1/5)"] \<open>0 < r\<close> by force
 qed
 
 
 text \<open>
   This leads us to the main intermediate result:
 \<close>
 lemma Mertens_convergent: "convergent (\<lambda>n::nat. \<MM> n - ln n)"
 proof -
   obtain c where c: "summable (\<lambda>n. (\<MM> n - ln n + c) / n)"
     by (blast intro: mertens_summable)
   then obtain l where l: "(\<lambda>n. (\<MM> n - ln n + c) / n) sums l"
     by (auto simp: summable_def)
   have *: "(\<lambda>n. \<MM> n - ln n + c) \<longlonglongrightarrow> 0"
     by (rule sum_goestozero_theorem[OF c]) auto
   hence "(\<lambda>n. \<MM> n - ln n) \<longlonglongrightarrow> -c"
     by (simp add: tendsto_iff dist_norm)
   thus ?thesis by (rule convergentI)
 qed
 
 corollary \<MM>_minus_ln_limit:
   obtains c where "((\<lambda>x::real. \<MM> x - ln x) \<longlongrightarrow> c) at_top"
 proof -
   from Mertens_convergent obtain c where "(\<lambda>n. \<MM> n - ln n) \<longlonglongrightarrow> c"
     by (auto simp: convergent_def)
   hence 1: "((\<lambda>x::real. \<MM> (nat \<lfloor>x\<rfloor>) - ln (nat \<lfloor>x\<rfloor>)) \<longlongrightarrow> c) at_top" 
     by (rule filterlim_compose) real_asymp
   have 2: "((\<lambda>x::real. ln (nat \<lfloor>x\<rfloor>) - ln x) \<longlongrightarrow> 0) at_top"
     by real_asymp
   have 3: "((\<lambda>x. \<MM> x - ln x) \<longlongrightarrow> c) at_top"
     using tendsto_add[OF 1 2] by simp
   with that show ?thesis by blast
 qed
 
 
 subsection \<open>The asymptotics of the prime-counting functions\<close>
 
 text \<open>
   We will now use the above result to prove the asymptotics of the prime-counting functions
   $\vartheta(x) \sim x$, $\psi(x) \sim x$, and $\pi(x) \sim x / \ln x$. The last of these is 
   typically called the Prime Number Theorem, but since these functions can be expressed in terms 
   of one another quite easily, knowing the asymptotics of any of them immediately gives the 
   asymptotics of the other ones.
 
   In this sense, all of the above are equivalent formulations of the Prime Number Theorem.
   The one we shall tackle first, due to its strong connection to the $\mathfrak{M}$ function, is
   $\vartheta(x) \sim x$.
 
   We know that $\mathfrak{M}(x)$ has the asymptotic expansion
   $\mathfrak{M}(x) = \ln x + c + o(1)$. We also know that
   \[\vartheta(x) = x\mathfrak{M}(x) - \int\nolimits_2^x \mathfrak{M}(t) \,\mathrm{d}t\ .\]
   Substituting in the above asymptotic equation, we obtain:
   \begin{align*}
   \vartheta(x) &= x\ln x + cx + o(x) - \int\nolimits_2^x \ln t + c + o(1) \,\mathrm{d}t\\
             &= x\ln x + cx + o(x) - (x\ln x - x + cx + o(x))\\
             &= x + o(x)
   \end{align*}
   In conclusion, $\vartheta(x) \sim x$.
 \<close>
 theorem \<theta>_asymptotics: "\<theta> \<sim>[at_top] (\<lambda>x. x)"
 proof -
   from \<MM>_minus_ln_limit obtain c where c: "((\<lambda>x. \<MM> x - ln x) \<longlongrightarrow> c) at_top"
     by auto
   define r where "r = (\<lambda>x. \<MM> x - ln x - c)"
   have \<MM>_expand: "\<MM> = (\<lambda>x. ln x + c + r x)"
     by (simp add: r_def)
   have r: "r \<in> o(\<lambda>_. 1)" unfolding r_def
     using tendsto_add[OF c tendsto_const[of "-c"]] by (intro smalloI_tendsto) auto
 
   define r' where "r' = (\<lambda>x. integral {2..x} r)"
   have integrable_r: "r integrable_on {x..y}"
     if "2 \<le> x" for x y :: real using that unfolding r_def
     by (intro integrable_diff integrable_primes_M)
        (auto intro!: integrable_continuous_real continuous_intros)
   hence integral: "(r has_integral r' x) {2..x}" if "x \<ge> 2" for x
     by (auto simp: has_integral_iff r'_def)
   have r': "r' \<in> o(\<lambda>x. x)" using integrable_r unfolding r'_def
     by (intro integral_smallo[OF r]) (auto simp: filterlim_ident)
 
   define C where "C = 2 * (c + ln 2 - 1)"
   have "\<theta> \<sim>[at_top] (\<lambda>x. x + (r x * x + C - r' x))"
   proof (intro asymp_equiv_refl_ev eventually_mono[OF eventually_gt_at_top])
     fix x :: real assume x: "x > 2"
     have "(\<MM> has_integral ((x * ln x - x + c * x) - (2 * ln 2 - 2 + c * 2) + r' x)) {2..x}"
       unfolding \<MM>_expand using x
       by (intro has_integral_add[OF fundamental_theorem_of_calculus integral])
          (auto simp flip: has_field_derivative_iff_has_vector_derivative
                intro!: derivative_eq_intros continuous_intros)
     from has_integral_unique[OF \<theta>_conv_\<MM>_integral this]
       show "\<theta> x = x + (r x * x + C - r' x)" using x
       by (simp add: field_simps \<MM>_expand C_def)
   qed
   also have "(\<lambda>x. r x * x + C - r' x) \<in> o(\<lambda>x. x)"
   proof (intro sum_in_smallo r)
     show "(\<lambda>_. C) \<in> o(\<lambda>x. x)" by real_asymp
   qed (insert landau_o.small_big_mult[OF r, of "\<lambda>x. x"] r', simp_all)
   hence "(\<lambda>x. x + (r x * x + C - r' x)) \<sim>[at_top] (\<lambda>x. x)"
     by (subst asymp_equiv_add_right) auto
   finally show ?thesis by auto
 qed
 
 text \<open>
   The various other forms of the Prime Number Theorem follow as simple corollaries.
 \<close>
 corollary \<psi>_asymptotics: "\<psi> \<sim>[at_top] (\<lambda>x. x)"
   using \<theta>_asymptotics PNT4_imp_PNT5 by simp
   
 corollary prime_number_theorem: "\<pi> \<sim>[at_top] (\<lambda>x. x / ln x)"
   using \<theta>_asymptotics PNT4_imp_PNT1 by simp
 
 corollary ln_\<pi>_asymptotics: "(\<lambda>x. ln (\<pi> x)) \<sim>[at_top] ln"
   using prime_number_theorem PNT1_imp_PNT1' by simp
 
 corollary \<pi>_ln_\<pi>_asymptotics: "(\<lambda>x. \<pi> x * ln (\<pi> x)) \<sim>[at_top] (\<lambda>x. x)"
   using prime_number_theorem PNT1_imp_PNT2 by simp
 
 corollary nth_prime_asymptotics: "(\<lambda>n. real (nth_prime n)) \<sim>[at_top] (\<lambda>n. real n * ln (real n))"
   using \<pi>_ln_\<pi>_asymptotics PNT2_imp_PNT3 by simp
 
 
 text \<open>
   The following versions use a little less notation.
 \<close>
 corollary prime_number_theorem': "((\<lambda>x. \<pi> x / (x / ln x)) \<longlongrightarrow> 1) at_top"
   using prime_number_theorem
   by (rule asymp_equivD_strong[OF _ eventually_mono[OF eventually_gt_at_top[of 1]]]) auto
 
 corollary prime_number_theorem'':
   "(\<lambda>x. card {p. prime p \<and> real p \<le> x}) \<sim>[at_top] (\<lambda>x. x / ln x)"
 proof -
   have "\<pi> = (\<lambda>x. card {p. prime p \<and> real p \<le> x})"
     by (intro ext) (simp add: \<pi>_def prime_sum_upto_def)
   with prime_number_theorem show ?thesis by simp
 qed
 
 corollary prime_number_theorem''':
   "(\<lambda>n. card {p. prime p \<and> p \<le> n}) \<sim>[at_top] (\<lambda>n. real n / ln (real n))"
 proof -
   have "(\<lambda>n. card {p. prime p \<and> real p \<le> real n}) \<sim>[at_top] (\<lambda>n. real n / ln (real n))"
     using prime_number_theorem''
     by (rule asymp_equiv_compose') (simp add: filterlim_real_sequentially)
   thus ?thesis by simp
 qed
 
 (*<*)
 unbundle no_prime_counting_notation
 (*>*)
 
 end
\ No newline at end of file