diff --git a/thys/Incompleteness/Coding.thy b/thys/Incompleteness/Coding.thy
--- a/thys/Incompleteness/Coding.thy
+++ b/thys/Incompleteness/Coding.thy
@@ -1,860 +1,858 @@
 chapter\<open>De Bruijn Syntax, Quotations, Codes, V-Codes\<close>
 
 theory Coding
 imports SyntaxN
 begin
 
 declare fresh_Nil [iff]
 
 section \<open>de Bruijn Indices (locally-nameless version)\<close>
 
 nominal_datatype dbtm = DBZero | DBVar name | DBInd nat | DBEats dbtm dbtm
 
 nominal_datatype dbfm =
     DBMem dbtm dbtm
   | DBEq dbtm dbtm
   | DBDisj dbfm dbfm
   | DBNeg dbfm
   | DBEx dbfm
 
 declare dbtm.supp [simp]
 declare dbfm.supp [simp]
 
 fun lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> dbtm"
   where
     "lookup [] n x = DBVar x"
   | "lookup (y # ys) n x = (if x = y then DBInd n else (lookup ys (Suc n) x))"
 
 lemma fresh_imp_notin_env: "atom name \<sharp> e \<Longrightarrow> name \<notin> set e"
   by (metis List.finite_set fresh_finite_set_at_base fresh_set)
 
 lemma lookup_notin: "x \<notin> set e \<Longrightarrow> lookup e n x = DBVar x"
   by (induct e arbitrary: n) auto
 
 lemma lookup_in:
   "x \<in> set e \<Longrightarrow> \<exists>k. lookup e n x = DBInd k \<and> n \<le> k \<and> k < n + length e"
   by (induction e arbitrary: n) force+
 
 lemma lookup_fresh: "x \<sharp> lookup e n y \<longleftrightarrow> y \<in> set e \<or> x \<noteq> atom y"
   by (induct arbitrary: n rule: lookup.induct) (auto simp: pure_fresh fresh_at_base)
 
 lemma lookup_eqvt[eqvt]: "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
 lemma lookup_inject [iff]: "(lookup e n x = lookup e n y) \<longleftrightarrow> x = y"
 proof (induction e n x arbitrary: y rule: lookup.induct)
   case (2 y ys n x z)
   then show ?case
     by (metis dbtm.distinct(7) dbtm.eq_iff(3) lookup.simps(2) lookup_in lookup_notin not_less_eq_eq)
 qed auto
 
 nominal_function trans_tm :: "name list \<Rightarrow> tm \<Rightarrow> dbtm"
   where
    "trans_tm e Zero = DBZero"
  | "trans_tm e (Var k) = lookup e 0 k"
  | "trans_tm e (Eats t u) = DBEats (trans_tm e t) (trans_tm e u)"
 by (auto simp: eqvt_def trans_tm_graph_aux_def) (metis tm.strong_exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_trans_tm_iff [simp]: "i \<sharp> trans_tm e t \<longleftrightarrow> i \<sharp> t \<or> i \<in> atom ` set e"
   by (induct t rule: tm.induct, auto simp: lookup_fresh fresh_at_base)
 
 lemma trans_tm_forget: "atom i \<sharp> t \<Longrightarrow> trans_tm [i] t = trans_tm [] t"
   by (induct t rule: tm.induct, auto simp: fresh_Pair)
 
 nominal_function (invariant "\<lambda>(xs, _) y. atom ` set xs \<sharp>* y")
   trans_fm :: "name list \<Rightarrow> fm \<Rightarrow> dbfm"
   where
    "trans_fm e (Mem t u) = DBMem (trans_tm e t) (trans_tm e u)"
  | "trans_fm e (Eq t u)  = DBEq (trans_tm e t) (trans_tm e u)"
  | "trans_fm e (Disj A B) = DBDisj (trans_fm e A) (trans_fm e B)"
  | "trans_fm e (Neg A)   = DBNeg (trans_fm e A)"
  | "atom k \<sharp> e \<Longrightarrow> trans_fm e (Ex k A) = DBEx (trans_fm (k#e) A)"
                    supply [[simproc del: defined_all]]
                    apply(simp add: eqvt_def trans_fm_graph_aux_def)
                   apply(erule trans_fm_graph.induct)
   using [[simproc del: alpha_lst]]
                       apply(auto simp: fresh_star_def)
    apply (metis fm.strong_exhaust fresh_star_insert)
   apply(erule Abs_lst1_fcb2')
      apply (simp_all add: eqvt_at_def)
     apply (simp_all add: fresh_star_Pair perm_supp_eq)
   apply (simp add: fresh_star_def)
   done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_trans_fm [simp]: "i \<sharp> trans_fm e A \<longleftrightarrow> i \<sharp> A \<or> i \<in> atom ` set e"
   by (nominal_induct A avoiding: e rule: fm.strong_induct, auto simp: fresh_at_base)
 
 abbreviation DBConj :: "dbfm \<Rightarrow> dbfm \<Rightarrow> dbfm"
   where "DBConj t u \<equiv> DBNeg (DBDisj (DBNeg t) (DBNeg u))"
 
 lemma trans_fm_Conj [simp]: "trans_fm e (Conj A B) = DBConj (trans_fm e A) (trans_fm e B)"
   by (simp add: Conj_def)
 
 lemma trans_tm_inject [iff]: "(trans_tm e t = trans_tm e u) \<longleftrightarrow> t = u"
 proof (induct t arbitrary: u rule: tm.induct)
   case Zero show ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
     done
 next
   case (Var i) show ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
     apply (metis dbtm.distinct(10) dbtm.distinct(11) lookup_in lookup_notin)
     done
 next
   case (Eats tm1 tm2) thus ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (metis dbtm.distinct(12) dbtm.distinct(9) lookup_in lookup_notin)
     done
 qed
 
 lemma trans_fm_inject [iff]: "(trans_fm e A = trans_fm e B) \<longleftrightarrow> A = B"
 proof (nominal_induct A avoiding: e B rule: fm.strong_induct)
   case (Mem tm1 tm2) thus ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
 next
   case (Eq tm1 tm2) thus ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
 next
   case (Disj fm1 fm2) show ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Disj fresh_star_def)
 next
   case (Neg fm) show ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Neg fresh_star_def)
 next
   case (Ex name fm)
   thus ?case  using [[simproc del: alpha_lst]]
   proof (cases rule: fm.strong_exhaust [where y=B and c="(e, name)"], simp_all add: fresh_star_def)
     fix name'::name and fm'::fm
     assume name': "atom name' \<sharp> (e, name)"
     assume "atom name \<sharp> fm' \<or> name = name'"
     thus "(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')"
          (is "?lhs = ?rhs")
     proof (rule disjE)
       assume "name = name'"
       thus "?lhs = ?rhs"
         by (metis fresh_Pair fresh_at_base(2) name')
     next
       assume name: "atom name \<sharp> fm'"
       have eq1: "(name \<leftrightarrow> name') \<bullet> trans_fm (name' # e) fm' = trans_fm (name' # e) fm'"
         by (simp add: flip_fresh_fresh name)
       have eq2: "(name \<leftrightarrow> name') \<bullet> ([[atom name']]lst. fm') = [[atom name']]lst. fm'"
         by (rule flip_fresh_fresh) (auto simp: Abs_fresh_iff name)
       show "?lhs = ?rhs" using name' eq1 eq2 Ex(1) Ex(3) [of "name#e" "(name \<leftrightarrow> name') \<bullet> fm'"]
         by (simp add: flip_fresh_fresh) (metis Abs1_eq(3))
     qed
   qed
 qed
 
 lemma trans_fm_perm:
   assumes c: "atom c \<sharp> (i,j,A,B)"
   and     t: "trans_fm [i] A = trans_fm [j] B"
   shows "(i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B"
 proof -
   have c_fresh1: "atom c \<sharp> trans_fm [i] A"
     using c by (auto simp: supp_Pair)
   moreover
   have i_fresh: "atom i \<sharp> trans_fm [i] A"
     by auto
   moreover
   have c_fresh2: "atom c \<sharp> trans_fm [j] B"
     using c by (auto simp: supp_Pair)
   moreover
   have j_fresh: "atom j \<sharp> trans_fm [j] B"
     by auto
   ultimately have "((i \<leftrightarrow> c) \<bullet> (trans_fm [i] A)) = ((j \<leftrightarrow> c) \<bullet> trans_fm [j] B)"
     by (simp only: flip_fresh_fresh t)
   then have "trans_fm [c] ((i \<leftrightarrow> c) \<bullet> A) = trans_fm [c] ((j \<leftrightarrow> c) \<bullet> B)"
     by simp
   then show "(i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B" by simp
 qed
 
 section\<open>Abstraction and Substitution on de Bruijn Formulas\<close>
 
 nominal_function abst_dbtm :: "name \<Rightarrow> nat \<Rightarrow> dbtm \<Rightarrow> dbtm"
   where
    "abst_dbtm name i DBZero = DBZero"
  | "abst_dbtm name i (DBVar name') = (if name = name' then DBInd i else DBVar name')"
  | "abst_dbtm name i (DBInd j) = DBInd j"
  | "abst_dbtm name i (DBEats t1 t2) = DBEats (abst_dbtm name i t1) (abst_dbtm name i t2)"
 apply (simp add: eqvt_def abst_dbtm_graph_aux_def, auto)
 apply (metis dbtm.exhaust)
 done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 nominal_function subst_dbtm :: "dbtm \<Rightarrow> name \<Rightarrow> dbtm \<Rightarrow> dbtm"
   where
    "subst_dbtm u x DBZero = DBZero"
  | "subst_dbtm u x (DBVar name) = (if x = name then u else DBVar name)"
  | "subst_dbtm u x (DBInd j) = DBInd j"
  | "subst_dbtm u x (DBEats t1 t2) = DBEats (subst_dbtm u x t1) (subst_dbtm u x t2)"
 by (auto simp: eqvt_def subst_dbtm_graph_aux_def) (metis dbtm.exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_iff_non_subst_dbtm: "subst_dbtm DBZero i t = t \<longleftrightarrow> atom i \<sharp> t"
   by (induct t rule: dbtm.induct) (auto simp: pure_fresh fresh_at_base(2))
 
 lemma lookup_append: "lookup (e @ [i]) n j = abst_dbtm i (length e + n) (lookup e n j)"
   by (induct e arbitrary: n) (auto simp: fresh_Cons)
 
 lemma trans_tm_abs: "trans_tm (e@[name]) t = abst_dbtm name (length e) (trans_tm e t)"
   by (induct t rule: tm.induct) (auto simp: lookup_notin lookup_append)
 
 subsection\<open>Well-Formed Formulas\<close>
 
 nominal_function abst_dbfm :: "name \<Rightarrow> nat \<Rightarrow> dbfm \<Rightarrow> dbfm"
   where
    "abst_dbfm name i (DBMem t1 t2) = DBMem (abst_dbtm name i t1) (abst_dbtm name i t2)"
  | "abst_dbfm name i (DBEq t1 t2) =  DBEq (abst_dbtm name i t1) (abst_dbtm name i t2)"
  | "abst_dbfm name i (DBDisj A1 A2) = DBDisj (abst_dbfm name i A1) (abst_dbfm name i A2)"
  | "abst_dbfm name i (DBNeg A) = DBNeg (abst_dbfm name i A)"
  | "abst_dbfm name i (DBEx A) = DBEx (abst_dbfm name (i+1) A)"
 apply (simp add: eqvt_def abst_dbfm_graph_aux_def, auto)
 apply (metis dbfm.exhaust)
 done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 nominal_function subst_dbfm :: "dbtm \<Rightarrow> name \<Rightarrow> dbfm \<Rightarrow> dbfm"
   where
    "subst_dbfm u x (DBMem t1 t2) = DBMem (subst_dbtm u x t1) (subst_dbtm u x t2)"
  | "subst_dbfm u x (DBEq t1 t2) =  DBEq (subst_dbtm u x t1) (subst_dbtm u x t2)"
  | "subst_dbfm u x (DBDisj A1 A2) = DBDisj (subst_dbfm u x A1) (subst_dbfm u x A2)"
  | "subst_dbfm u x (DBNeg A) = DBNeg (subst_dbfm u x A)"
  | "subst_dbfm u x (DBEx A) = DBEx (subst_dbfm u x A)"
 by (auto simp: eqvt_def subst_dbfm_graph_aux_def) (metis dbfm.exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_iff_non_subst_dbfm: "subst_dbfm DBZero i t = t \<longleftrightarrow> atom i \<sharp> t"
   by (induct t rule: dbfm.induct) (auto simp: fresh_iff_non_subst_dbtm)
 
 
 section\<open>Well formed terms and formulas (de Bruijn representation)\<close>
 
 subsection\<open>Well-Formed Terms\<close>
 
 inductive wf_dbtm :: "dbtm \<Rightarrow> bool"
   where
     Zero:  "wf_dbtm DBZero"
   | Var:   "wf_dbtm (DBVar name)"
   | Eats:  "wf_dbtm t1 \<Longrightarrow> wf_dbtm t2 \<Longrightarrow> wf_dbtm (DBEats t1 t2)"
 
 equivariance wf_dbtm
 
 inductive_cases Zero_wf_dbtm [elim!]: "wf_dbtm DBZero"
 inductive_cases Var_wf_dbtm [elim!]:  "wf_dbtm (DBVar name)"
 inductive_cases Ind_wf_dbtm [elim!]:  "wf_dbtm (DBInd i)"
 inductive_cases Eats_wf_dbtm [elim!]: "wf_dbtm (DBEats t1 t2)"
 
 declare wf_dbtm.intros [intro]
 
 lemma wf_dbtm_imp_is_tm:
   assumes "wf_dbtm x"
   shows "\<exists>t::tm. x = trans_tm [] t"
 using assms
 proof (induct rule: wf_dbtm.induct)
   case Zero thus ?case
     by (metis trans_tm.simps(1))
 next
   case (Var i) thus ?case
     by (metis lookup.simps(1) trans_tm.simps(2))
 next
   case (Eats dt1 dt2) thus ?case
     by (metis trans_tm.simps(3))
 qed
 
 lemma wf_dbtm_trans_tm: "wf_dbtm (trans_tm [] t)"
   by (induct t rule: tm.induct) auto
 
 theorem wf_dbtm_iff_is_tm: "wf_dbtm x \<longleftrightarrow> (\<exists>t::tm. x = trans_tm [] t)"
   by (metis wf_dbtm_imp_is_tm wf_dbtm_trans_tm)
 
 subsection\<open>Well-Formed Formulas\<close>
 
 inductive wf_dbfm :: "dbfm \<Rightarrow> bool"
   where
     Mem:   "wf_dbtm t1 \<Longrightarrow> wf_dbtm t2 \<Longrightarrow> wf_dbfm (DBMem t1 t2)"
   | Eq:    "wf_dbtm t1 \<Longrightarrow> wf_dbtm t2 \<Longrightarrow> wf_dbfm (DBEq t1 t2)"
   | Disj:  "wf_dbfm A1 \<Longrightarrow> wf_dbfm A2 \<Longrightarrow> wf_dbfm (DBDisj A1 A2)"
   | Neg:   "wf_dbfm A \<Longrightarrow> wf_dbfm (DBNeg A)"
   | Ex:    "wf_dbfm A \<Longrightarrow> wf_dbfm (DBEx (abst_dbfm name 0 A))"
 
 equivariance wf_dbfm
 
 lemma atom_fresh_abst_dbtm [simp]: "atom i \<sharp> abst_dbtm i n t"
   by (induct t rule: dbtm.induct) (auto simp: pure_fresh)
 
 lemma atom_fresh_abst_dbfm [simp]: "atom i \<sharp> abst_dbfm i n A"
   by (nominal_induct A arbitrary: n rule: dbfm.strong_induct) auto
 
 text\<open>Setting up strong induction: "avoiding" for name. Necessary to allow some proofs to go through\<close>
 nominal_inductive wf_dbfm
   avoids Ex: name
   by (auto simp: fresh_star_def)
 
 inductive_cases Mem_wf_dbfm [elim!]:  "wf_dbfm (DBMem t1 t2)"
 inductive_cases Eq_wf_dbfm [elim!]:   "wf_dbfm (DBEq t1 t2)"
 inductive_cases Disj_wf_dbfm [elim!]: "wf_dbfm (DBDisj A1 A2)"
 inductive_cases Neg_wf_dbfm [elim!]:  "wf_dbfm (DBNeg A)"
 inductive_cases Ex_wf_dbfm [elim!]:   "wf_dbfm (DBEx z)"
 
 declare wf_dbfm.intros [intro]
 
 lemma trans_fm_abs: "trans_fm (e@[name]) A = abst_dbfm name (length e) (trans_fm e A)"
   apply (nominal_induct A avoiding: name e rule: fm.strong_induct)
   apply (auto simp: trans_tm_abs fresh_Cons fresh_append)
   by (metis append_Cons length_Cons)
 
 lemma abst_trans_fm: "abst_dbfm name 0 (trans_fm [] A) = trans_fm [name] A"
   by (metis append_Nil list.size(3) trans_fm_abs)
 
 lemma abst_trans_fm2: "i \<noteq> j \<Longrightarrow> abst_dbfm i (Suc 0) (trans_fm [j] A) = trans_fm [j,i] A"
   using trans_fm_abs [where e="[j]" and name=i]
   by auto
 
 lemma wf_dbfm_imp_is_fm:
   assumes "wf_dbfm x" shows "\<exists>A::fm. x = trans_fm [] A"
 using assms
 proof (induct rule: wf_dbfm.induct)
   case (Mem t1 t2) thus ?case
     by (metis trans_fm.simps(1) wf_dbtm_imp_is_tm)
 next
   case (Eq t1 t2) thus ?case
     by (metis trans_fm.simps(2) wf_dbtm_imp_is_tm)
 next
   case (Disj fm1 fm2) thus ?case
     by (metis trans_fm.simps(3))
 next
   case (Neg fm) thus ?case
     by (metis trans_fm.simps(4))
 next
   case (Ex fm name) thus ?case
     apply auto
     apply (rule_tac x="Ex name A" in exI)
     apply (auto simp: abst_trans_fm)
     done
 qed
 
 lemma wf_dbfm_trans_fm: "wf_dbfm (trans_fm [] A)"
   apply (nominal_induct A rule: fm.strong_induct)
   apply (auto simp: wf_dbtm_trans_tm abst_trans_fm)
   apply (metis abst_trans_fm wf_dbfm.Ex)
   done
 
 lemma wf_dbfm_iff_is_fm: "wf_dbfm x \<longleftrightarrow> (\<exists>A::fm. x = trans_fm [] A)"
   by (metis wf_dbfm_imp_is_fm wf_dbfm_trans_fm)
 
 lemma dbtm_abst_ignore [simp]:
   "abst_dbtm name i (abst_dbtm name j t) = abst_dbtm name j t"
   by (induct t rule: dbtm.induct) auto
 
 lemma abst_dbtm_fresh_ignore [simp]: "atom name \<sharp> u \<Longrightarrow> abst_dbtm name j u = u"
   by (induct u rule: dbtm.induct) auto
 
 lemma dbtm_subst_ignore [simp]:
   "subst_dbtm u name (abst_dbtm name j t) = abst_dbtm name j t"
   by (induct t rule: dbtm.induct) auto
 
 lemma dbtm_abst_swap_subst:
   "name \<noteq> name' \<Longrightarrow> atom name' \<sharp> u \<Longrightarrow>
    subst_dbtm u name (abst_dbtm name' j t) = abst_dbtm name' j (subst_dbtm u name t)"
   by (induct t rule: dbtm.induct) auto
 
 lemma dbfm_abst_swap_subst:
   "name \<noteq> name' \<Longrightarrow> atom name' \<sharp> u \<Longrightarrow>
    subst_dbfm u name (abst_dbfm name' j A) = abst_dbfm name' j (subst_dbfm u name A)"
   by (induct A arbitrary: j rule: dbfm.induct) (auto simp: dbtm_abst_swap_subst)
 
 lemma subst_trans_commute [simp]:
   "atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e t) = trans_tm e (subst i u t)"
   apply (induct t rule: tm.induct)
-  apply (auto simp: lookup_notin fresh_imp_notin_env)
-  apply (metis abst_dbtm_fresh_ignore dbtm_subst_ignore lookup_fresh lookup_notin subst_dbtm.simps(2))
-  done
+    apply (auto simp: lookup_notin fresh_imp_notin_env)
+  by (metis abst_dbtm_fresh_ignore atom_eq_iff dbtm_subst_ignore lookup_fresh)
 
 lemma subst_fm_trans_commute [simp]:
   "subst_dbfm (trans_tm [] u) name (trans_fm [] A) = trans_fm [] (A (name::= u))"
   apply (nominal_induct A avoiding: name u rule: fm.strong_induct)
-  apply (auto simp: lookup_notin abst_trans_fm [symmetric])
-  apply (metis dbfm_abst_swap_subst fresh_at_base(2) fresh_trans_tm_iff)
+  apply (auto simp: lookup_notin dbfm_abst_swap_subst simp flip: abst_trans_fm)
   done
 
 lemma subst_fm_trans_commute_eq:
   "du = trans_tm [] u \<Longrightarrow> subst_dbfm du i (trans_fm [] A) = trans_fm [] (A(i::=u))"
   by (metis subst_fm_trans_commute)
 
 
 section\<open>Quotations\<close>
 
 fun htuple :: "nat \<Rightarrow> hf"  where
    "htuple 0 = \<langle>0,0\<rangle>"
  | "htuple (Suc k) = \<langle>0, htuple k\<rangle>"
 
 fun HTuple :: "nat \<Rightarrow> tm"  where
    "HTuple 0 = HPair Zero Zero"
  | "HTuple (Suc k) = HPair Zero (HTuple k)"
 
 lemma eval_tm_HTuple [simp]:  "\<lbrakk>HTuple n\<rbrakk>e = htuple n"
   by (induct n) auto
 
 lemma fresh_HTuple [simp]: "x \<sharp> HTuple n"
   by (induct n) auto
 
 lemma HTuple_eqvt[eqvt]: "(p \<bullet> HTuple n) = HTuple (p \<bullet> n)"
   by (induct n, auto simp: HPair_eqvt permute_pure)
 
 lemma htuple_nonzero [simp]: "htuple k \<noteq> 0"
   by (induct k) auto
 
 lemma htuple_inject [iff]: "htuple i = htuple j \<longleftrightarrow> i=j"
 proof (induct i arbitrary: j)
   case 0 show ?case
     by (cases j) auto
 next
   case (Suc i) show ?case
     by (cases j) (auto simp: Suc)
 qed
 
 subsection \<open>Quotations of de Bruijn terms\<close>
 
 definition nat_of_name :: "name \<Rightarrow> nat"
   where "nat_of_name x = nat_of (atom x)"
 
 lemma nat_of_name_inject [simp]: "nat_of_name n1 = nat_of_name n2 \<longleftrightarrow> n1 = n2"
   by (metis nat_of_name_def atom_components_eq_iff atom_eq_iff sort_of_atom_eq)
 
 definition name_of_nat :: "nat \<Rightarrow> name"
   where "name_of_nat n \<equiv> Abs_name (Atom (Sort ''SyntaxN.name'' []) n)"
 
 lemma nat_of_name_Abs_eq [simp]: "nat_of_name (Abs_name (Atom (Sort ''SyntaxN.name'' []) n)) = n"
   by (auto simp: nat_of_name_def atom_name_def Abs_name_inverse)
 
 lemma nat_of_name_name_eq [simp]: "nat_of_name (name_of_nat n) = n"
   by (simp add: name_of_nat_def)
 
 lemma name_of_nat_nat_of_name [simp]: "name_of_nat (nat_of_name i) = i"
   by (metis nat_of_name_inject nat_of_name_name_eq)
 
 lemma HPair_neq_ORD_OF [simp]: "HPair x y \<noteq> ORD_OF i"
   by (metis Not_Ord_hpair Ord_ord_of eval_tm_HPair eval_tm_ORD_OF)
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function quot_dbtm :: "dbtm \<Rightarrow> tm"
   where
    "quot_dbtm DBZero = Zero"
  | "quot_dbtm (DBVar name) = ORD_OF (Suc (nat_of_name name))"
  | "quot_dbtm (DBInd k) = HPair (HTuple 6) (ORD_OF k)"
  | "quot_dbtm (DBEats t u) = HPair (HTuple 1) (HPair (quot_dbtm t) (quot_dbtm u))"
 by (rule dbtm.exhaust) auto
 
 termination
   by lexicographic_order
 
 lemma quot_dbtm_inject_lemma [simp]: "\<lbrakk>quot_dbtm t\<rbrakk>e = \<lbrakk>quot_dbtm u\<rbrakk>e \<longleftrightarrow> t=u"
 proof (induct t arbitrary: u rule: dbtm.induct)
   case DBZero show ?case
     by (induct u rule: dbtm.induct) auto
 next
   case (DBVar name) show ?case
     by (induct u rule: dbtm.induct) (auto simp: hpair_neq_Ord')
 next
   case (DBInd k) show ?case
     by (induct u rule: dbtm.induct) (auto simp: hpair_neq_Ord hpair_neq_Ord')
 next
   case (DBEats t1 t2) thus ?case
     by (induct u rule: dbtm.induct) (simp_all add: hpair_neq_Ord)
 qed
 
 lemma quot_dbtm_inject [iff]: "quot_dbtm t = quot_dbtm u \<longleftrightarrow> t=u"
   by (metis quot_dbtm_inject_lemma)
 
 subsection \<open>Quotations of de Bruijn formulas\<close>
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function quot_dbfm :: "dbfm \<Rightarrow> tm"
   where
    "quot_dbfm (DBMem t u) = HPair (HTuple 0) (HPair (quot_dbtm t) (quot_dbtm u))"
  | "quot_dbfm (DBEq t u) = HPair (HTuple 2) (HPair (quot_dbtm t) (quot_dbtm u))"
  | "quot_dbfm (DBDisj A B) = HPair (HTuple 3) (HPair (quot_dbfm A) (quot_dbfm B))"
  | "quot_dbfm (DBNeg A) = HPair (HTuple 4) (quot_dbfm A)"
  | "quot_dbfm (DBEx A) = HPair (HTuple 5) (quot_dbfm A)"
 by (rule_tac y=x in dbfm.exhaust, auto)
 
 termination
   by lexicographic_order
 
 lemma htuple_minus_1: "n > 0 \<Longrightarrow> htuple n = \<langle>0, htuple (n - 1)\<rangle>"
   by (metis Suc_diff_1 htuple.simps(2))
 
 lemma HTuple_minus_1: "n > 0 \<Longrightarrow> HTuple n = HPair Zero (HTuple (n - 1))"
   by (metis Suc_diff_1 HTuple.simps(2))
 
 lemmas HTS = HTuple_minus_1 HTuple.simps \<comment> \<open>for freeness reasoning on codes\<close>
 
 lemma quot_dbfm_inject_lemma [simp]: "\<lbrakk>quot_dbfm A\<rbrakk>e = \<lbrakk>quot_dbfm B\<rbrakk>e \<longleftrightarrow> A=B"
 proof (induct A arbitrary: B rule: dbfm.induct)
   case (DBMem t u) show ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 next
   case (DBEq t u) show ?case
     by (induct B rule: dbfm.induct) (auto simp: htuple_minus_1)
 next
   case (DBDisj A B') thus ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 next
   case (DBNeg A) thus ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 next
   case (DBEx A) thus ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 qed
 
 
 class quot =
   fixes quot :: "'a \<Rightarrow> tm"  ("\<guillemotleft>_\<guillemotright>")
 
 instantiation tm :: quot
 begin
   definition quot_tm :: "tm \<Rightarrow> tm"
     where "quot_tm t = quot_dbtm (trans_tm [] t)"
   
   instance ..
 end
 
 lemma quot_dbtm_fresh [simp]: "s \<sharp> (quot_dbtm t)"
   by (induct t rule: dbtm.induct) auto
 
 lemma quot_tm_fresh [simp]: fixes t::tm shows "s \<sharp> \<guillemotleft>t\<guillemotright>"
   by (simp add: quot_tm_def)
 
 lemma quot_Zero [simp]: "\<guillemotleft>Zero\<guillemotright> = Zero"
   by (simp add: quot_tm_def)
 
 lemma quot_Var: "\<guillemotleft>Var x\<guillemotright> = SUCC (ORD_OF (nat_of_name x))"
   by (simp add: quot_tm_def)
 
 lemma quot_Eats: "\<guillemotleft>Eats x y\<guillemotright> = HPair (HTuple 1) (HPair \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>)"
   by (simp add: quot_tm_def)
 
 text\<open>irrelevance of the environment for quotations, because they are ground terms\<close>
 lemma eval_quot_dbtm_ignore:
     "\<lbrakk>quot_dbtm t\<rbrakk>e = \<lbrakk>quot_dbtm t\<rbrakk>e'"
   by (induct t rule: dbtm.induct) auto
 
 lemma eval_quot_dbfm_ignore:
     "\<lbrakk>quot_dbfm A\<rbrakk>e = \<lbrakk>quot_dbfm A\<rbrakk>e'"
   by (induct A rule: dbfm.induct) (auto intro: eval_quot_dbtm_ignore)
 
 
 instantiation fm :: quot
 begin
   definition quot_fm :: "fm \<Rightarrow> tm"
     where "quot_fm A = quot_dbfm (trans_fm [] A)"
   
   instance ..
 end
 
 lemma quot_dbfm_fresh [simp]: "s \<sharp> (quot_dbfm A)"
   by (induct A rule: dbfm.induct) auto
 
 lemma quot_fm_fresh [simp]: fixes A::fm shows "s \<sharp> \<guillemotleft>A\<guillemotright>"
   by (simp add: quot_fm_def)
 
 lemma quot_fm_permute [simp]: fixes A:: fm shows "p \<bullet> \<guillemotleft>A\<guillemotright> = \<guillemotleft>A\<guillemotright>"
   by (metis fresh_star_def perm_supp_eq quot_fm_fresh)
 
 lemma quot_Mem: "\<guillemotleft>x IN y\<guillemotright> = HPair (HTuple 0) (HPair (\<guillemotleft>x\<guillemotright>) (\<guillemotleft>y\<guillemotright>))"
   by (simp add: quot_fm_def quot_tm_def)
 
 lemma quot_Eq: "\<guillemotleft>x EQ y\<guillemotright> = HPair (HTuple 2) (HPair (\<guillemotleft>x\<guillemotright>) (\<guillemotleft>y\<guillemotright>))"
   by (simp add: quot_fm_def quot_tm_def)
 
 lemma quot_Disj: "\<guillemotleft>A OR B\<guillemotright> = HPair (HTuple 3) (HPair (\<guillemotleft>A\<guillemotright>) (\<guillemotleft>B\<guillemotright>))"
   by (simp add: quot_fm_def)
 
 lemma quot_Neg: "\<guillemotleft>Neg A\<guillemotright> = HPair (HTuple 4) (\<guillemotleft>A\<guillemotright>)"
   by (simp add: quot_fm_def)
 
 lemma quot_Ex: "\<guillemotleft>Ex i A\<guillemotright> = HPair (HTuple 5) (quot_dbfm (trans_fm [i] A))"
   by (simp add: quot_fm_def)
 
 lemma eval_quot_fm_ignore: fixes A:: fm shows "\<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e'"
   by (metis eval_quot_dbfm_ignore quot_fm_def)
 
 lemmas quot_simps = quot_Var quot_Eats quot_Eq quot_Mem quot_Disj quot_Neg quot_Ex
 
 section\<open>Definitions Involving Coding\<close>
 
 definition q_Var :: "name \<Rightarrow> hf"
   where "q_Var i \<equiv> succ (ord_of (nat_of_name i))"
 
 definition q_Ind :: "hf \<Rightarrow> hf"
   where "q_Ind k \<equiv>  \<langle>htuple 6, k\<rangle>"
 
 abbreviation Q_Eats :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Eats t u \<equiv> HPair (HTuple (Suc 0)) (HPair t u)"
 
 definition q_Eats :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Eats x y \<equiv> \<langle>htuple 1, x, y\<rangle>"
 
 abbreviation Q_Succ :: "tm \<Rightarrow> tm"
   where "Q_Succ t \<equiv> Q_Eats t t"
 
 definition q_Succ :: "hf \<Rightarrow> hf"
   where "q_Succ x \<equiv> q_Eats x x"
 
 lemma quot_Succ: "\<guillemotleft>SUCC x\<guillemotright> = Q_Succ \<guillemotleft>x\<guillemotright>"
   by (auto simp: SUCC_def quot_Eats)
 
 abbreviation Q_HPair :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_HPair t u \<equiv>
            Q_Eats (Q_Eats Zero (Q_Eats (Q_Eats Zero u) t))
                   (Q_Eats (Q_Eats Zero t) t)"
 
 definition q_HPair :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_HPair x y \<equiv>
            q_Eats (q_Eats 0 (q_Eats (q_Eats 0 y) x))
                   (q_Eats (q_Eats 0 x) x)"
 
 abbreviation Q_Mem :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Mem t u \<equiv> HPair (HTuple 0) (HPair t u)"
 
 definition q_Mem :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Mem x y \<equiv> \<langle>htuple 0, x, y\<rangle>"
 
 abbreviation Q_Eq :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Eq t u \<equiv> HPair (HTuple 2) (HPair t u)"
 
 definition q_Eq :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Eq x y \<equiv> \<langle>htuple 2, x, y\<rangle>"
 
 abbreviation Q_Disj :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Disj t u \<equiv> HPair (HTuple 3) (HPair t u)"
 
 definition q_Disj :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Disj x y \<equiv> \<langle>htuple 3, x, y\<rangle>"
 
 abbreviation Q_Neg :: "tm \<Rightarrow> tm"
   where "Q_Neg t \<equiv> HPair (HTuple 4) t"
 
 definition q_Neg :: "hf \<Rightarrow> hf"
   where "q_Neg x \<equiv> \<langle>htuple 4, x\<rangle>"
 
 abbreviation Q_Conj :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Conj t u \<equiv> Q_Neg (Q_Disj (Q_Neg t) (Q_Neg u))"
 
 definition q_Conj :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Conj t u \<equiv> q_Neg (q_Disj (q_Neg t) (q_Neg u))"
 
 abbreviation Q_Imp :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Imp t u \<equiv> Q_Disj (Q_Neg t) u"
 
 definition q_Imp :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Imp t u \<equiv> q_Disj (q_Neg t) u"
 
 abbreviation Q_Ex :: "tm \<Rightarrow> tm"
   where "Q_Ex t \<equiv> HPair (HTuple 5) t"
 
 definition q_Ex :: "hf \<Rightarrow> hf"
   where "q_Ex x \<equiv> \<langle>htuple 5, x\<rangle>"
 
 abbreviation Q_All :: "tm \<Rightarrow> tm"
   where "Q_All t \<equiv> Q_Neg (Q_Ex (Q_Neg t))"
 
 definition q_All :: "hf \<Rightarrow> hf"
   where "q_All x \<equiv> q_Neg (q_Ex (q_Neg x))"
 
 lemmas q_defs = q_Var_def q_Ind_def q_Eats_def q_HPair_def q_Eq_def q_Mem_def
                 q_Disj_def q_Neg_def q_Conj_def q_Imp_def q_Ex_def q_All_def
 
 lemma q_Eats_iff [iff]: "q_Eats x y = q_Eats x' y' \<longleftrightarrow> x=x' \<and> y=y'"
   by (metis hpair_iff q_Eats_def)
 
 lemma quot_subst_eq: "\<guillemotleft>A(i::=t)\<guillemotright> = quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))"
   by (metis quot_fm_def subst_fm_trans_commute)
 
 lemma Q_Succ_cong: "H \<turnstile> x EQ x' \<Longrightarrow> H \<turnstile> Q_Succ x EQ Q_Succ x'"
   by (metis HPair_cong Refl)
 
   
 section\<open>Quotations are Injective\<close>
 
 subsection\<open>Terms\<close>
 
 lemma eval_tm_inject [simp]: fixes t::tm shows "\<lbrakk>\<guillemotleft>t\<guillemotright>\<rbrakk> e = \<lbrakk>\<guillemotleft>u\<guillemotright>\<rbrakk> e \<longleftrightarrow> t=u"
 proof (induct t arbitrary: u rule: tm.induct)
   case Zero thus ?case
     by (cases u rule: tm.exhaust) (auto simp: quot_Var quot_Eats)
 next
   case (Var i) thus ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (auto simp: quot_Var quot_Eats)
     done
 next
   case (Eats t1 t2) thus ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (auto simp: quot_Eats quot_Var)
     done
 qed
 
 subsection\<open>Formulas\<close>
 
 lemma eval_fm_inject [simp]: fixes A::fm shows "\<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk> e = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk> e \<longleftrightarrow> A=B"
 proof (nominal_induct B arbitrary: A rule: fm.strong_induct)
   case (Mem tm1 tm2) thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Eq tm1 tm2) thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Neg \<alpha>) thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Disj fm1 fm2)
   thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Ex i \<alpha>)
   thus ?case
     apply (induct A arbitrary: i rule: fm.induct)
     apply (auto simp: trans_fm_perm quot_simps htuple_minus_1 Abs1_eq_iff_all)
     by (metis (no_types) Abs1_eq_iff_all(3) dbfm.eq_iff(5) fm.eq_iff(5) fresh_Nil trans_fm.simps(5))
 qed
 
 subsection\<open>The set \<open>\<Gamma>\<close> of Definition 1.1, constant terms used for coding\<close>
 
 inductive coding_tm :: "tm \<Rightarrow> bool"
   where
     Ord:    "\<exists>i. x = ORD_OF i \<Longrightarrow> coding_tm x"
   | HPair:  "coding_tm x \<Longrightarrow> coding_tm y \<Longrightarrow> coding_tm (HPair x y)"
 
 declare coding_tm.intros [intro]
 
 lemma coding_tm_Zero [intro]: "coding_tm Zero"
   by (metis ORD_OF.simps(1) Ord)
 
 lemma coding_tm_HTuple [intro]: "coding_tm (HTuple k)"
   by (induct k, auto)
 
 inductive_simps coding_tm_HPair [simp]: "coding_tm (HPair x y)"
 
 lemma quot_dbtm_coding [simp]: "coding_tm (quot_dbtm t)"
   apply (induct t rule: dbtm.induct, auto)
   apply (metis ORD_OF.simps(2) Ord)
   done
 
 lemma quot_dbfm_coding [simp]: "coding_tm (quot_dbfm fm)"
   by (induct fm rule: dbfm.induct, auto)
 
 lemma quot_fm_coding: fixes A::fm shows "coding_tm \<guillemotleft>A\<guillemotright>"
   by (metis quot_dbfm_coding quot_fm_def)
 
 inductive coding_hf :: "hf \<Rightarrow> bool"
   where
     Ord:    "\<exists>i. x = ord_of i \<Longrightarrow> coding_hf x"
   | HPair:  "coding_hf x \<Longrightarrow> coding_hf y \<Longrightarrow> coding_hf (\<langle>x,y\<rangle>)"
 
 declare coding_hf.intros [intro]
 
 lemma coding_hf_0 [intro]: "coding_hf 0"
   by (metis coding_hf.Ord ord_of.simps(1))
 
 inductive_simps coding_hf_hpair [simp]: "coding_hf (\<langle>x,y\<rangle>)"
 
 lemma coding_tm_hf [simp]: "coding_tm t \<Longrightarrow> coding_hf \<lbrakk>t\<rbrakk>e"
   by (induct t rule: coding_tm.induct) auto
 
   
 section \<open>V-Coding for terms and formulas, for the Second Theorem\<close>
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function vquot_dbtm :: "name set \<Rightarrow> dbtm \<Rightarrow> tm"
   where
    "vquot_dbtm V DBZero = Zero"
  | "vquot_dbtm V (DBVar name) = (if name \<in> V then Var name
                                  else ORD_OF (Suc (nat_of_name name)))"
  | "vquot_dbtm V (DBInd k) = HPair (HTuple 6) (ORD_OF k)"
  | "vquot_dbtm V (DBEats t u) = HPair (HTuple 1) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
 by (auto, rule_tac y=b in dbtm.exhaust, auto)
 
 termination
   by lexicographic_order
 
 lemma fresh_vquot_dbtm [simp]: "i \<sharp> vquot_dbtm V tm \<longleftrightarrow> i \<sharp> tm \<or> i \<notin> atom ` V"
   by (induct tm rule: dbtm.induct) (auto simp: fresh_at_base pure_fresh)
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function vquot_dbfm :: "name set \<Rightarrow> dbfm \<Rightarrow> tm"
   where
    "vquot_dbfm V (DBMem t u) = HPair (HTuple 0) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
  | "vquot_dbfm V (DBEq t u) = HPair (HTuple 2) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
  | "vquot_dbfm V (DBDisj A B) = HPair (HTuple 3) (HPair (vquot_dbfm V A) (vquot_dbfm V B))"
  | "vquot_dbfm V (DBNeg A) = HPair (HTuple 4) (vquot_dbfm V A)"
  | "vquot_dbfm V (DBEx A) = HPair (HTuple 5) (vquot_dbfm V A)"
 by (auto, rule_tac y=b in dbfm.exhaust, auto)
 
 termination
   by lexicographic_order
 
 lemma fresh_vquot_dbfm [simp]: "i \<sharp> vquot_dbfm V fm \<longleftrightarrow> i \<sharp> fm \<or> i \<notin> atom ` V"
   by (induct fm rule: dbfm.induct) (auto simp: HPair_def HTuple_minus_1)
 
 class vquot =
   fixes vquot :: "'a \<Rightarrow> name set \<Rightarrow> tm"  ("\<lfloor>_\<rfloor>_"  [0,1000]1000)
 
 instantiation tm :: vquot
 begin
   definition vquot_tm :: "tm \<Rightarrow> name set \<Rightarrow> tm"
     where "vquot_tm t V = vquot_dbtm V (trans_tm [] t)"
   instance ..
 end
 
 lemma vquot_dbtm_empty [simp]: "vquot_dbtm {} t = quot_dbtm t"
   by (induct t rule: dbtm.induct) auto
 
 lemma vquot_tm_empty [simp]: fixes t::tm shows "\<lfloor>t\<rfloor>{} = \<guillemotleft>t\<guillemotright>"
   by (simp add: vquot_tm_def quot_tm_def)
 
 lemma vquot_dbtm_eq: "atom ` V \<inter> supp t = atom ` W \<inter> supp t \<Longrightarrow> vquot_dbtm V t = vquot_dbtm W t"
   by (induct t rule: dbtm.induct) (auto simp: image_iff, blast+)
 
 instantiation fm :: vquot
 begin
   definition vquot_fm :: "fm \<Rightarrow> name set \<Rightarrow> tm"
     where "vquot_fm A V = vquot_dbfm V (trans_fm [] A)"
   instance ..
 end
 
 lemma vquot_fm_fresh [simp]: fixes A::fm shows "i \<sharp> \<lfloor>A\<rfloor>V \<longleftrightarrow> i \<sharp> A \<or> i \<notin> atom ` V"
   by (simp add: vquot_fm_def)
 
 lemma vquot_dbfm_empty [simp]: "vquot_dbfm {} A = quot_dbfm A"
   by (induct A rule: dbfm.induct) auto
 
 lemma vquot_fm_empty [simp]: fixes A::fm shows "\<lfloor>A\<rfloor>{} = \<guillemotleft>A\<guillemotright>"
   by (simp add: vquot_fm_def quot_fm_def)
 
 lemma vquot_dbfm_eq: "atom ` V \<inter> supp A = atom ` W \<inter> supp A \<Longrightarrow> vquot_dbfm V A = vquot_dbfm W A"
   by (induct A rule: dbfm.induct) (auto simp: intro!: vquot_dbtm_eq, blast+)
 
 lemma vquot_fm_insert:
   fixes A::fm shows "atom i \<notin> supp A \<Longrightarrow> \<lfloor>A\<rfloor>(insert i V) = \<lfloor>A\<rfloor>V"
   by (auto simp: vquot_fm_def supp_conv_fresh intro: vquot_dbfm_eq)
 
 declare HTuple.simps [simp del]
 
 end
diff --git a/thys/Sophomores_Dream/Sophomores_Dream.thy b/thys/Sophomores_Dream/Sophomores_Dream.thy
--- a/thys/Sophomores_Dream/Sophomores_Dream.thy
+++ b/thys/Sophomores_Dream/Sophomores_Dream.thy
@@ -1,522 +1,442 @@
 (*
   File:    Sophomores_Dream.thy
   Author:  Manuel Eberl, University of Innsbruck
 *)
 section \<open>The Sophomore's Dream\<close>
 theory Sophomores_Dream
   imports "HOL-Analysis.Analysis" "HOL-Real_Asymp.Real_Asymp"
 begin
 
 text \<open>
   This formalisation mostly follows the very clear proof sketch from Wikipedia~\cite{wikipedia}.
   That article also provides an interesting historical perspective. A more detailed 
   exploration of Bernoulli's historical proof can be found in the book by Dunham~\cite{dunham}.
 
   The name `Sophomore's Dream' apparently comes from a book by Borwein et al., in analogy to
   the `Freshman's Dream' equation $(x+y)^n = x^n + y^n$ (which is generally \<^emph>\<open>not\<close> true except
   in rings of characteristic $n$).
 \<close>
 
-subsection \<open>Auxiliary material\<close>
-
-(* TODO: Move to library! *)
-lemma integrable_cong:
-  assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
-  shows   "f integrable_on A \<longleftrightarrow> g integrable_on A"
-  using has_integral_cong [OF assms] by fast
-
-lemma has_integral_cmul_iff':
-  assumes "c \<noteq> 0"
-  shows   "((\<lambda>x. c *\<^sub>R f x) has_integral I) A \<longleftrightarrow> (f has_integral I /\<^sub>R c) A"
-  using assms by (metis divideR_right has_integral_cmul_iff)
-
-lemma has_integral_Icc_iff_Ioo:
-  fixes f :: "real \<Rightarrow> 'a :: banach"
-  shows "(f has_integral I) {a..b} \<longleftrightarrow> (f has_integral I) {a<..<b}"
-proof (rule has_integral_spike_set_eq)
-  show "negligible {x \<in> {a..b} - {a<..<b}. f x \<noteq> 0}"
-    by (rule negligible_subset [of "{a,b}"]) auto
-  show "negligible {x \<in> {a<..<b} - {a..b}. f x \<noteq> 0}"
-    by (rule negligible_subset [of "{}"]) auto
-qed
-
-lemma integrable_on_Icc_iff_Ioo:
-  fixes f :: "real \<Rightarrow> 'a :: banach"
-  shows "f integrable_on {a..b} \<longleftrightarrow> f integrable_on {a<..<b}"
-  using has_integral_Icc_iff_Ioo by blast
-
-lemma norm_summable_imp_has_sum:
-  fixes f :: "nat \<Rightarrow> 'a :: banach"
-  assumes "summable (\<lambda>n. norm (f n))" and "f sums S"
-  shows   "has_sum f (UNIV :: nat set) S"
-  unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top
-proof (safe, goal_cases)
-  case (1 \<epsilon>)
-  from assms(1) obtain S' where S': "(\<lambda>n. norm (f n)) sums S'"
-    by (auto simp: summable_def)
-  with 1 obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> \<bar>S' - (\<Sum>i<n. norm (f i))\<bar> < \<epsilon>"
-    by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute)
-  
-  show ?case
-  proof (rule exI[of _ "{..<N}"], safe, goal_cases)
-    case (2 Y)
-    from 2 have "(\<lambda>n. if n \<in> Y then 0 else f n) sums (S - sum f Y)"
-      by (intro sums_If_finite_set'[OF \<open>f sums S\<close>]) (auto simp: sum_negf)
-    hence "S - sum f Y = (\<Sum>n. if n \<in> Y then 0 else f n)"
-      by (simp add: sums_iff)
-    also have "norm \<dots> \<le> (\<Sum>n. norm (if n \<in> Y then 0 else f n))"
-      by (rule summable_norm[OF summable_comparison_test'[OF assms(1)]]) auto
-    also have "\<dots> \<le> (\<Sum>n. if n < N then 0 else norm (f n))"
-      using 2 by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto
-    also have "(\<lambda>n. if n \<in> {..<N} then 0 else norm (f n)) sums (S' - (\<Sum>i<N. norm (f i)))" 
-      by (intro sums_If_finite_set'[OF S']) (auto simp: sum_negf)
-    hence "(\<Sum>n. if n < N then 0 else norm (f n)) = S' - (\<Sum>i<N. norm (f i))"
-      by (simp add: sums_iff)
-    also have "S' - (\<Sum>i<N. norm (f i)) \<le> \<bar>S' - (\<Sum>i<N. norm (f i))\<bar>" by simp
-    also have "\<dots> < \<epsilon>" by (rule N) auto
-    finally show ?case by (simp add: dist_norm norm_minus_commute)
-  qed auto
-qed
-
-lemma norm_summable_imp_summable_on:
-  fixes f :: "nat \<Rightarrow> 'a :: banach"
-  assumes "summable (\<lambda>n. norm (f n))"
-  shows   "f summable_on UNIV"
-  using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms
-  by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel)
-
-lemma summable_comparison_test_bigo:
-  fixes f :: "nat \<Rightarrow> real"
-  assumes "summable (\<lambda>n. norm (g n))" "f \<in> O(g)"
-  shows   "summable f"
-proof -
-  from \<open>f \<in> O(g)\<close> obtain C where C: "eventually (\<lambda>x. norm (f x) \<le> C * norm (g x)) at_top"
-    by (auto elim: landau_o.bigE)
-  thus ?thesis
-    by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
-qed
-
-
 subsection \<open>Continuity and bounds for $x \log x$\<close>
 
 lemma x_log_x_continuous: "continuous_on {0..1} (\<lambda>x::real. x * ln x)"
 proof -
   have "continuous (at x within {0..1}) (\<lambda>x::real. x * ln x)" if "x \<in> {0..1}" for x
   proof (cases "x = 0")
     case True
     have "((\<lambda>x::real. x * ln x) \<longlongrightarrow> 0) (at_right 0)"
       by real_asymp
     thus ?thesis using True
       by (simp add: continuous_def Lim_ident_at at_within_Icc_at_right)
   qed (auto intro!: continuous_intros)
   thus ?thesis
     using continuous_on_eq_continuous_within by blast
 qed
 
 lemma x_log_x_within_01_le:
   assumes "x \<in> {0..(1::real)}"
   shows   "x * ln x \<in> {-exp (-1)..0}"
 proof -
   have "x * ln x \<le> 0"
     using assms by (cases "x = 0") (auto simp: mult_nonneg_nonpos)
   let ?f = "\<lambda>x::real. x * ln x"
   have diff: "(?f has_field_derivative (ln x + 1)) (at x)" if "x > 0" for x
     using that by (auto intro!: derivative_eq_intros)
   have diff': "?f differentiable at x" if "x > 0" for x
     using diff[OF that] real_differentiable_def by blast
 
   consider "x = 0" | "x = 1" | "x = exp (-1)" | "0 < x" "x < exp (-1)" | "exp (-1) < x" "x < 1"
     using assms unfolding atLeastAtMost_iff by linarith
   hence "x * ln x \<ge> -exp (-1)"
   proof cases
     assume x: "0 < x" "x < exp (-1)"
     have "\<exists>l z. x < z \<and> z < exp (-1) \<and> (?f has_real_derivative l) (at z) \<and>
              ?f (exp (-1)) - ?f x = (exp (-1) - x) * l"
       using x by (intro MVT continuous_on_subset [OF x_log_x_continuous] diff') auto
     then obtain l z where lz:
       "x < z" "z < exp (-1)" "(?f has_real_derivative l) (at z)"
       "?f x = -exp (-1) - (exp (-1) - x) * l"
       by (auto simp: algebra_simps)
     have [simp]: "l = ln z + 1"
       using DERIV_unique[OF diff[of z] lz(3)] lz(1) x by auto
     have "ln z \<le> ln (exp (-1))"
       using lz x by (subst ln_le_cancel_iff) auto
     hence "(exp (- 1) - x) * l \<le> 0"
       using x lz by (intro mult_nonneg_nonpos) auto
     with lz show ?thesis
       by linarith
   next
     assume x: "exp (-1) < x" "x < 1"
     have "\<exists>l z. exp (-1) < z \<and> z < x \<and> (?f has_real_derivative l) (at z) \<and>
              ?f x - ?f (exp (-1)) = (x - exp (-1)) * l"
     proof (intro MVT continuous_on_subset [OF x_log_x_continuous] diff')
       fix t :: real assume t: "exp (-1) < t"
       show "t > 0"
         by (rule less_trans [OF _ t]) auto
     qed (use x in auto)
     then obtain l z where lz:
       "exp (-1) < z" "z < x" "(?f has_real_derivative l) (at z)"
       "?f x = -exp (-1) - (exp (-1) - x) * l"
       by (auto simp: algebra_simps)
     have "z > 0"
       by (rule less_trans [OF _ lz(1)]) auto
     have [simp]: "l = ln z + 1"
       using DERIV_unique[OF diff[of z] lz(3)] \<open>z > 0\<close> by auto
     have "ln z \<ge> ln (exp (-1))"
       using lz \<open>z > 0\<close> by (subst ln_le_cancel_iff) auto
     hence "(exp (- 1) - x) * l \<le> 0"
       using x lz by (intro mult_nonpos_nonneg) auto
     with lz show ?thesis
       by linarith
   qed auto
 
   with \<open>x * ln x \<le> 0\<close> show ?thesis
     by auto
 qed
 
 
 subsection \<open>Convergence, Summability, Integrability\<close>
 
 text \<open>
   As a first result we can show that the two sums that occur in the two different versions
   of the Sophomore's Dream are absolutely summable. This is achieved by a simple comparison 
   test with the series $\sum_{k=1}^\infty k^{-2}$, as $k^{-k} \in O(k^{-2})$.
 \<close>
 theorem abs_summable_sophomores_dream: "summable (\<lambda>k. 1 / real (k ^ k))"
 proof (rule summable_comparison_test_bigo)
   show "(\<lambda>k. 1 / real (k ^ k)) \<in> O(\<lambda>k. 1 / real k ^ 2)"
     by real_asymp
   show "summable (\<lambda>n. norm (1 / real n ^ 2))"
     using inverse_power_summable[of 2, where ?'a = real] by (simp add: field_simps)
 qed
 
 text \<open>
   The existence of the integral is also fairly easy to show since the integrand is continuous
   and the integration domain is compact. There is, however, one hiccup: The integrand is not
   actually continuous.
 
   We have $\lim_{x\to 0} x^x = 1$, but in Isabelle $0^0$ is defined as \<open>0\<close> (for real numbers).
   Thus, there is a discontinuity at \<open>x = 0\<close>
 
   However, this is a removable discontinuity since for any $x>0$ we have $x^x = e^{x\log x}$, and
   as we have just shown, $e^{x \log x}$ \<^emph>\<open>is\<close> continuous on $[0, 1]$. Since the two integrands
   differ only for \<open>x = 0\<close> (which is negligible), the integral still exists.
 \<close>
 theorem integrable_sophomores_dream: "(\<lambda>x::real. x powr x) integrable_on {0..1}"
 proof -
   have "(\<lambda>x::real. exp (x * ln x)) integrable_on {0..1}"
     by (intro integrable_continuous_real continuous_on_exp x_log_x_continuous)
   also have "?this \<longleftrightarrow> (\<lambda>x::real. exp (x * ln x)) integrable_on {0<..<1}"
     by (simp add: integrable_on_Icc_iff_Ioo)
   also have "\<dots> \<longleftrightarrow> (\<lambda>x::real. x powr x) integrable_on {0<..<1}"
     by (intro integrable_cong) (auto simp: powr_def)
   also have "\<dots> \<longleftrightarrow> ?thesis"
     by (simp add: integrable_on_Icc_iff_Ioo)
   finally show ?thesis .
 qed
 
 text \<open>
   Next, we have to show the absolute convergence of the two auxiliary sums that will occur in
   our proofs so that we can exchange the order of integration and summation. This is done
   with a straightforward application of the Weierstra\ss\ \<open>M\<close> test.
 \<close>
 lemma uniform_limit_sophomores_dream1:
   "uniform_limit {0..(1::real)}
       (\<lambda>n x. \<Sum>k<n. (x * ln x) ^ k / fact k)
       (\<lambda>x. \<Sum>k. (x * ln x) ^ k / fact k)
       sequentially"
 proof (rule Weierstrass_m_test)
   show "summable (\<lambda>k. exp (-1) ^ k / fact k :: real)"
     using summable_exp[of "exp (-1)"] by (simp add: field_simps)
 next
   fix k :: nat and x :: real
   assume x: "x \<in> {0..1}"
   have "norm ((x * ln x) ^ k / fact k) = norm (x * ln x) ^ k / fact k"
     by (simp add: power_abs)
   also have "\<dots> \<le> exp (-1) ^ k / fact k"
     by (intro divide_right_mono power_mono) (use x_log_x_within_01_le [of x] x in auto)
   finally show "norm ((x * ln x) ^ k / fact k) \<le> exp (- 1) ^ k / fact k" .
 qed
 
 lemma uniform_limit_sophomores_dream2:
   "uniform_limit {0..(1::real)}
       (\<lambda>n x. \<Sum>k<n. (-(x * ln x)) ^ k / fact k)
       (\<lambda>x. \<Sum>k. (-(x * ln x)) ^ k / fact k)
       sequentially"
 proof (rule Weierstrass_m_test)
   show "summable (\<lambda>k. exp (-1) ^ k / fact k :: real)"
     using summable_exp[of "exp (-1)"] by (simp add: field_simps)
 next
   fix k :: nat and x :: real
   assume x: "x \<in> {0..1}"
   have "norm ((-x * ln x) ^ k / fact k) = norm (x * ln x) ^ k / fact k"
     by (simp add: power_abs)
   also have "\<dots> \<le> exp (-1) ^ k / fact k"
     by (intro divide_right_mono power_mono) (use x_log_x_within_01_le [of x] x in auto)
   finally show "norm ((-(x * ln x)) ^ k / fact k) \<le> exp (- 1) ^ k / fact k" by simp
 qed
 
 
 subsection \<open>An auxiliary integral\<close>
 
 text \<open>
   Next we compute the integral
     \[\int_0^1 (x\log x)^n\,\text{d}x = \frac{(-1)^n\, n!}{(n+1)^{n+1}}\ ,\]
   which is a key ingredient in our proof.
 \<close>
 lemma sophomores_dream_aux_integral:
   "((\<lambda>x. (x * ln x) ^ n) has_integral (- 1) ^ n * fact n / real ((n + 1) ^ (n + 1))) {0<..<1}"
 proof -
   have "((\<lambda>t. t powr real n / exp t) has_integral fact n) {0..}"
     using Gamma_integral_real[of "n + 1"] by (auto simp: Gamma_fact powr_realpow)
   also have "?this \<longleftrightarrow> ((\<lambda>t. t powr real n / exp t) has_integral fact n) {0<..}"
   proof (rule has_integral_spike_set_eq)
     have eq: "{x \<in> {0<..} - {0..}. x powr real n / exp x \<noteq> 0} = {}"
       by auto
     thus "negligible {x \<in> {0<..} - {0..}. x powr real n / exp x \<noteq> 0}"
       by (subst eq) auto
     have "{x \<in> {0..} - {0<..}. x powr real n / exp x \<noteq> 0} \<subseteq> {0}"
       by auto
     moreover have "negligible {0::real}"
       by simp
     ultimately show "negligible {x \<in> {0..} - {0<..}. x powr real n / exp x \<noteq> 0}"
       by (meson negligible_subset)
   qed
   also have "\<dots> \<longleftrightarrow> ((\<lambda>t::real. t ^ n / exp t) has_integral fact n) {0<..}"
     by (intro has_integral_spike_eq) (auto simp: powr_realpow)
   finally have 1: "((\<lambda>t::real. t ^ n / exp t) has_integral fact n) {0<..}" .
 
   have "(\<lambda>x::real. \<bar>x\<bar> ^ n / exp x) integrable_on {0<..} \<longleftrightarrow>
         (\<lambda>x::real. x ^ n / exp x) integrable_on {0<..}"
     by (intro integrable_cong) auto
   hence 2: "(\<lambda>t::real. t ^ n / exp t) absolutely_integrable_on {0<..}"
     using 1 by (simp add: absolutely_integrable_on_def power_abs has_integral_iff)
 
   define g :: "real \<Rightarrow> real" where "g = (\<lambda>x. -ln x * (n + 1))"
   define g' :: "real \<Rightarrow> real" where "g' = (\<lambda>x. -(n + 1) / x)"
   define h :: "real \<Rightarrow> real" where "h = (\<lambda>u. exp (-u / (n + 1)))"
   have bij: "bij_betw g {0<..<1} {0<..}"
     by (rule bij_betwI[of _ _ _ h]) (auto simp: g_def h_def mult_neg_pos)
   have deriv: "(g has_real_derivative g' x) (at x within {0<..<1})"
     if "x \<in> {0<..<1}" for x
     unfolding g_def g'_def using that by (auto intro!: derivative_eq_intros simp: field_simps)
 
   have "(\<lambda>t::real. t ^ n / exp t) absolutely_integrable_on g ` {0<..<1} \<and>
         integral (g ` {0<..<1}) (\<lambda>t::real. t ^ n / exp t) = fact n"
     using 1 2 bij by (simp add: bij_betw_def has_integral_iff)
   also have "?this \<longleftrightarrow> ((\<lambda>x. \<bar>g' x\<bar> *\<^sub>R (g x ^ n / exp (g x))) absolutely_integrable_on {0<..<1} \<and>
                        integral {0<..<1} (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R (g x ^ n / exp (g x))) = fact n)"
     by (intro has_absolute_integral_change_of_variables_1' [symmetric] deriv)
        (auto simp: inj_on_def g_def)
   finally have "((\<lambda>x. \<bar>g' x\<bar> *\<^sub>R (g x ^ n / exp (g x))) has_integral fact n) {0<..<1}"
     using eq_integralD set_lebesgue_integral_eq_integral(1) by blast
   also have "?this \<longleftrightarrow>
      ((\<lambda>x::real. ((-1)^n*(n+1)^(n+1)) *\<^sub>R (ln x ^ n * x ^ n)) has_integral fact n) {0<..<1}"
   proof (rule has_integral_cong)
     fix x :: real assume x: "x \<in> {0<..<1}"
     have "\<bar>g' x\<bar> *\<^sub>R (g x ^ n / exp (g x)) =
             (-1) ^ n * (real n + 1) ^ (n + 1) * ln x ^ n * (exp (ln x * (n + 1)) / x)"
       using x by (simp add: g_def g'_def exp_minus power_minus' divide_simps add_ac)
     also have "exp (ln x * (n + 1)) = x powr real (n + 1)"
       using x by (simp add: powr_def)
     also have "\<dots> / x = x ^ n"
       using x by (subst powr_realpow) auto
     finally show "\<bar>g' x\<bar> *\<^sub>R (g x ^ n / exp (g x)) =
                     ((-1)^n*(n+1)^(n+1)) *\<^sub>R (ln x ^ n * x ^ n)"
       by (simp add: algebra_simps)
   qed
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x::real. ln x ^ n * x ^ n) has_integral
                       fact n /\<^sub>R real_of_int ((- 1) ^ n * int ((n + 1) ^ (n + 1)))) {0<..<1}"
     by (intro has_integral_cmul_iff') (auto simp del: power_Suc)
   also have "fact n /\<^sub>R real_of_int ((- 1) ^ n * int ((n + 1) ^ (n + 1))) =
              (-1) ^ n * fact n / (n+1) ^ (n+1)"
     by (auto simp: divide_simps)
   finally show ?thesis
     by (simp add: power_mult_distrib mult_ac)
 qed
 
 subsection \<open>Main proofs\<close>
 
 
 text \<open>
   We can now show the first formula: $\int_0^1 x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n}$
 \<close>
 lemma sophomores_dream_aux1:
   "summable (\<lambda>k. 1 / real ((k+1)^(k+1)))"
   "integral {0..1} (\<lambda>x. x powr (-x)) = (\<Sum>n. 1 / (n+1)^(n+1))"
 proof -
   define S where "S = (\<lambda>x::real. \<Sum>k. (-(x * ln x)) ^ k / fact k)"
   have S_eq: "S x = x powr (-x)" if "x > 0" for x
   proof -
     have "S x = exp (-x * ln x)"
       by (simp add: S_def exp_def field_simps)
     also have "\<dots> = x powr (-x)"
       using \<open>x > 0\<close> by (simp add: powr_def)
     finally show ?thesis .
   qed
 
   have cont: "continuous_on {0..1} (\<lambda>x::real. \<Sum>k<n. (-(x * ln x)) ^ k / fact k)" for n
     by (intro continuous_on_sum continuous_on_divide x_log_x_continuous continuous_on_power
               continuous_on_const continuous_on_minus) auto
 
   obtain I J where IJ: "\<And>n. ((\<lambda>x. \<Sum>k<n. (-(x * ln x)) ^ k / fact k) has_integral I n) {0..1}"
                        "(S has_integral J) {0..1}" "I \<longlonglongrightarrow> J"
     using uniform_limit_integral [OF uniform_limit_sophomores_dream2 cont] by (auto simp: S_def)
 
   note \<open>(S has_integral J) {0..1}\<close>
   also have "(S has_integral J) {0..1} \<longleftrightarrow> (S has_integral J) {0<..<1}"
     by (simp add: has_integral_Icc_iff_Ioo)
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. x powr (-x)) has_integral J) {0<..<1}"
     by (intro has_integral_cong) (use S_eq in auto)
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. x powr (-x)) has_integral J) {0..1}"
     by (simp add: has_integral_Icc_iff_Ioo)
   finally have integral: "((\<lambda>x. x powr (-x)) has_integral J) {0..1}" .
 
   have I_eq: "I = (\<lambda>n. \<Sum>k<n. 1 / real ((k+1)^(k+1)))"
   proof
     fix n :: nat
     have "((\<lambda>x::real. \<Sum>k<n. (-1)^k * ((x * ln x) ^ k / fact k)) has_integral
             (\<Sum>k<n. (-1)^k * ((-1)^k * fact k / real ((k + 1) ^ (k + 1)) / fact k))) {0<..<1}"
       by (intro has_integral_sum[OF _ has_integral_mult_right] has_integral_divide
                 sophomores_dream_aux_integral) auto
     also have "(\<lambda>x::real. \<Sum>k<n. (-1)^k * ((x * ln x) ^ k / fact k)) =
                (\<lambda>x::real. \<Sum>k<n. (-(x * ln x)) ^ k / fact k)"
       by (simp add: power_minus')
     also have "(\<Sum>k<n. (-1)^k * ((-1) ^ k * fact k / real ((k + 1) ^ (k + 1)) / fact k)) =
                (\<Sum>k<n. 1 / real ((k + 1) ^ (k + 1)))"
       by simp
     also note has_integral_Icc_iff_Ioo [symmetric]
     finally show "I n = (\<Sum>k<n. 1 / real ((k+1)^(k+1)))"
       by (rule has_integral_unique [OF IJ(1)[of n]])
   qed
   hence sums: "(\<lambda>k. 1 / real ((k + 1) ^ (k + 1))) sums J"
     using IJ(3) I_eq by (simp add: sums_def)
   
   from sums show "summable (\<lambda>k. 1 / real ((k+1)^(k+1)))"
     by (simp add: sums_iff)
   from integral sums show "integral {0..1} (\<lambda>x. x powr (-x)) = (\<Sum>n. 1 / (n+1)^(n+1))"
     by (simp add: sums_iff has_integral_iff)
 qed
 
 theorem sophomores_dream1:
   "(\<lambda>k::nat. norm (k powi (-k))) summable_on {1..}"
   "integral {0..1} (\<lambda>x. x powr (-x)) = (\<Sum>\<^sub>\<infinity> k\<in>{(1::nat)..}. k powi (-k))"
 proof -
   let ?I = "integral {0..1} (\<lambda>x. x powr (-x))"
   have "(\<lambda>k::nat. norm (k powi (-k))) summable_on UNIV"
     using abs_summable_sophomores_dream
     by (intro norm_summable_imp_summable_on) (auto simp: power_int_minus field_simps)
   thus "(\<lambda>k::nat. norm (k powi (-k))) summable_on {1..}"
     by (rule summable_on_subset_banach) auto
 
   have "(\<lambda>n. 1 / (n+1)^(n+1)) sums ?I"
     using sophomores_dream_aux1 by (simp add: sums_iff)
   moreover have "summable (\<lambda>n. norm (1 / real (Suc n ^ Suc n)))"
     by (subst summable_Suc_iff) (use abs_summable_sophomores_dream in \<open>auto simp: field_simps\<close>)
   ultimately have "has_sum (\<lambda>n::nat. 1 / (n+1)^(n+1)) UNIV ?I"
     by (intro norm_summable_imp_has_sum) auto
   also have "?this \<longleftrightarrow> has_sum ((\<lambda>n::nat. 1 / n^n) \<circ> Suc) UNIV ?I"
     by (simp add: o_def field_simps)
   also have "\<dots> \<longleftrightarrow> has_sum (\<lambda>n::nat. 1 / n ^ n) (Suc ` UNIV) ?I"
     by (intro has_sum_reindex [symmetric]) auto
   also have "Suc ` UNIV = {1..}"
     using greaterThan_0 by auto
   also have "has_sum (\<lambda>n::nat. (1 / real (n ^ n))) {1..} ?I \<longleftrightarrow>
              has_sum (\<lambda>n::nat. n powi (-n)) {1..} ?I"
     by (intro has_sum_cong) (auto simp: power_int_minus field_simps power_minus')
   finally show "integral {0..1} (\<lambda>x. x powr (-x)) = (\<Sum>\<^sub>\<infinity>k\<in>{(1::nat)..}. k powi (-k))"
     by (auto dest!: infsumI simp: algebra_simps)
 qed
 
 
 text \<open>
   Next, we show the second formula: $\int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}$
 \<close>
 lemma sophomores_dream_aux2:
   "summable (\<lambda>k. (-1) ^ k / real ((k+1)^(k+1)))"
   "integral {0..1} (\<lambda>x. x powr x) = (\<Sum>n. (-1)^n / (n+1)^(n+1))"
 proof -
   define S where "S = (\<lambda>x::real. \<Sum>k. (x * ln x) ^ k / fact k)"
   have S_eq: "S x = x powr x" if "x > 0" for x
   proof -
     have "S x = exp (x * ln x)"
       by (simp add: S_def exp_def field_simps)
     also have "\<dots> = x powr x"
       using \<open>x > 0\<close> by (simp add: powr_def)
     finally show ?thesis .
   qed
 
   have cont: "continuous_on {0..1} (\<lambda>x::real. \<Sum>k<n. (x * ln x) ^ k / fact k)" for n
     by (intro continuous_on_sum continuous_on_divide x_log_x_continuous continuous_on_power
               continuous_on_const) auto
 
   obtain I J where IJ: "\<And>n. ((\<lambda>x. \<Sum>k<n. (x * ln x) ^ k / fact k) has_integral I n) {0..1}"
                        "(S has_integral J) {0..1}" "I \<longlonglongrightarrow> J"
     using uniform_limit_integral [OF uniform_limit_sophomores_dream1 cont] by (auto simp: S_def)
 
   note \<open>(S has_integral J) {0..1}\<close>
   also have "(S has_integral J) {0..1} \<longleftrightarrow> (S has_integral J) {0<..<1}"
     by (simp add: has_integral_Icc_iff_Ioo)
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. x powr x) has_integral J) {0<..<1}"
     by (intro has_integral_cong) (use S_eq in auto)
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. x powr x) has_integral J) {0..1}"
     by (simp add: has_integral_Icc_iff_Ioo)
   finally have integral: "((\<lambda>x. x powr x) has_integral J) {0..1}" .
 
   have I_eq: "I = (\<lambda>n. \<Sum>k<n. (-1) ^ k / real ((k+1)^(k+1)))"
   proof
     fix n :: nat
     have "((\<lambda>x::real. \<Sum>k<n. (x * ln x) ^ k / fact k) has_integral
             (\<Sum>k<n. (-1) ^ k * fact k / real ((k + 1) ^ (k + 1)) / fact k)) {0<..<1}"
       by (intro has_integral_sum has_integral_divide sophomores_dream_aux_integral) auto
     also have "(\<Sum>k<n. (- 1) ^ k * fact k / real ((k + 1) ^ (k + 1)) / fact k) =
                (\<Sum>k<n. (- 1) ^ k / real ((k + 1) ^ (k + 1)))"
       by simp
     also note has_integral_Icc_iff_Ioo [symmetric]
     finally show "I n = (\<Sum>k<n. (-1) ^ k / real ((k+1)^(k+1)))"
       by (rule has_integral_unique [OF IJ(1)[of n]])
   qed
   hence sums: "(\<lambda>k. (-1) ^ k / real ((k + 1) ^ (k + 1))) sums J"
     using IJ(3) I_eq by (simp add: sums_def)
   
   from sums show "summable (\<lambda>k. (-1) ^ k / real ((k+1)^(k+1)))"
     by (simp add: sums_iff)
   from integral sums show "integral {0..1} (\<lambda>x. x powr x) = (\<Sum>n. (-1)^n / (n+1)^(n+1))"
     by (simp add: sums_iff has_integral_iff)
 qed
 
 theorem sophomores_dream2:
   "(\<lambda>k::nat. norm ((-k) powi (-k))) summable_on {1..}"
   "integral {0..1} (\<lambda>x. x powr x) = -(\<Sum>\<^sub>\<infinity> k\<in>{(1::nat)..}. (-k) powi (-k))"
 proof -
   let ?I = "integral {0..1} (\<lambda>x. x powr x)"
   have "(\<lambda>k::nat. norm ((-k) powi (-k))) summable_on UNIV"
     using abs_summable_sophomores_dream
     by (intro norm_summable_imp_summable_on) (auto simp: power_int_minus field_simps)
   thus "(\<lambda>k::nat. norm ((-k) powi (-k))) summable_on {1..}"
     by (rule summable_on_subset_banach) auto
 
   have "(\<lambda>n. (-1)^n / (n+1)^(n+1)) sums ?I"
     using sophomores_dream_aux2 by (simp add: sums_iff)
   moreover have "summable (\<lambda>n. 1 / real (Suc n ^ Suc n))"
     by (subst summable_Suc_iff) (use abs_summable_sophomores_dream in \<open>auto simp: field_simps\<close>)
   hence "summable (\<lambda>n. norm ((- 1) ^ n / real (Suc n ^ Suc n)))"
     by simp
   ultimately have "has_sum (\<lambda>n::nat. (-1)^n / (n+1)^(n+1)) UNIV ?I"
     by (intro norm_summable_imp_has_sum) auto
   also have "?this \<longleftrightarrow> has_sum ((\<lambda>n::nat. -((-1)^n / n^n)) \<circ> Suc) UNIV ?I"
     by (simp add: o_def field_simps)
   also have "\<dots> \<longleftrightarrow> has_sum (\<lambda>n::nat. -((-1)^n / n ^ n)) (Suc ` UNIV) ?I"
     by (intro has_sum_reindex [symmetric]) auto
   also have "Suc ` UNIV = {1..}"
     using greaterThan_0 by auto
   also have "has_sum (\<lambda>n::nat. -((- 1) ^ n / real (n ^ n))) {1..} ?I \<longleftrightarrow>
              has_sum (\<lambda>n::nat. -((-n) powi (-n))) {1..} ?I"
     by (intro has_sum_cong) (auto simp: power_int_minus field_simps power_minus')
   also have "\<dots> \<longleftrightarrow> has_sum (\<lambda>n::nat. (-n) powi (-n)) {1..} (-?I)"
     by (simp add: has_sum_uminus)
   finally show "integral {0..1} (\<lambda>x. x powr x) = -(\<Sum>\<^sub>\<infinity>k\<in>{(1::nat)..}. (-k) powi (-k))"
     by (auto dest!: infsumI simp: algebra_simps)
 qed
 
 end
\ No newline at end of file