diff --git a/src/HOL/Nominal/Examples/SN.thy b/src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy
+++ b/src/HOL/Nominal/Examples/SN.thy
@@ -1,581 +1,533 @@
 theory SN
 imports Lam_Funs
 begin
 
 text \<open>Strong Normalisation proof from the Proofs and Types book\<close>
 
 section \<open>Beta Reduction\<close>
 
 lemma subst_rename: 
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
 by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
    (auto simp add: calc_atm fresh_atm abs_fresh)
 
 lemma forget: 
   assumes a: "a\<sharp>t1"
   shows "t1[a::=t2] = t1"
   using a
 by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
   fixes a::"name"
   assumes a: "a\<sharp>t1" "a\<sharp>t2"
   shows "a\<sharp>t1[b::=t2]"
 using a
 by (nominal_induct t1 avoiding: a b t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact': 
   fixes a::"name"
   assumes a: "a\<sharp>t2"
   shows "a\<sharp>t1[a::=t2]"
 using a 
 by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma subst_lemma:  
   assumes a: "x\<noteq>y"
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
    (auto simp add: fresh_fact forget)
 
 lemma id_subs: 
   shows "t[x::=Var x] = t"
   by (nominal_induct t avoiding: x rule: lam.strong_induct)
      (simp_all add: fresh_atm)
 
 lemma lookup_fresh:
   fixes z::"name"
   assumes "z\<sharp>\<theta>" "z\<sharp>x"
   shows "z\<sharp> lookup \<theta> x"
 using assms 
 by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)
 
 lemma lookup_fresh':
   assumes "z\<sharp>\<theta>"
   shows "lookup \<theta> z = Var z"
 using assms 
 by (induct rule: lookup.induct)
    (auto simp add: fresh_list_cons fresh_prod fresh_atm)
 
 lemma psubst_subst:
   assumes h:"c\<sharp>\<theta>"
   shows "(\<theta><t>)[c::=s] = ((c,s)#\<theta>)<t>"
   using h
 by (nominal_induct t avoiding: \<theta> c s rule: lam.strong_induct)
    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')
  
 inductive 
   Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta> _" [80,80] 80)
 where
   b1[intro!]: "s1 \<longrightarrow>\<^sub>\<beta> s2 \<Longrightarrow> App s1 t \<longrightarrow>\<^sub>\<beta> App s2 t"
 | b2[intro!]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^sub>\<beta> App t s2"
 | b3[intro!]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> Lam [a].s1 \<longrightarrow>\<^sub>\<beta> Lam [a].s2"
 | b4[intro!]: "a\<sharp>s2 \<Longrightarrow> App (Lam [a].s1) s2\<longrightarrow>\<^sub>\<beta> (s1[a::=s2])"
 
 equivariance Beta
 
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
 lemma beta_preserves_fresh: 
   fixes a::"name"
   assumes a: "t\<longrightarrow>\<^sub>\<beta> s"
   shows "a\<sharp>t \<Longrightarrow> a\<sharp>s"
 using a
-apply(nominal_induct t s avoiding: a rule: Beta.strong_induct)
-apply(auto simp add: abs_fresh fresh_fact fresh_atm)
-done
+  by (nominal_induct t s avoiding: a rule: Beta.strong_induct)
+     (auto simp add: abs_fresh fresh_fact fresh_atm)
 
 lemma beta_abs: 
   assumes a: "Lam [a].t\<longrightarrow>\<^sub>\<beta> t'" 
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^sub>\<beta> t''"
 proof -
   have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
   with a have "a\<sharp>t'" by (simp add: beta_preserves_fresh)
   with a show ?thesis
     by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
        (auto simp add: lam.inject abs_fresh alpha)
 qed
 
 lemma beta_subst: 
   assumes a: "M \<longrightarrow>\<^sub>\<beta> M'"
   shows "M[x::=N]\<longrightarrow>\<^sub>\<beta> M'[x::=N]" 
 using a
 by (nominal_induct M M' avoiding: x N rule: Beta.strong_induct)
    (auto simp add: fresh_atm subst_lemma fresh_fact)
 
 section \<open>types\<close>
 
 nominal_datatype ty =
     TVar "nat"
   | TArr "ty" "ty" (infix "\<rightarrow>" 200)
 
 lemma fresh_ty:
   fixes a ::"name"
   and   \<tau>  ::"ty"
   shows "a\<sharp>\<tau>"
 by (nominal_induct \<tau> rule: ty.strong_induct)
    (auto simp add: fresh_nat)
 
 (* valid contexts *)
 
 inductive 
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
 where
   v1[intro]: "valid []"
 | v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
 
 equivariance valid 
 
 (* typing judgements *)
 
 lemma fresh_context: 
   fixes  \<Gamma> :: "(name\<times>ty)list"
   and    a :: "name"
   assumes a: "a\<sharp>\<Gamma>"
   shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
 using a
 by (induct \<Gamma>)
    (auto simp add: fresh_prod fresh_list_cons fresh_atm)
 
 inductive 
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
 where
   t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
 | t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
 | t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
 
 equivariance typing
 
 nominal_inductive typing
   by (simp_all add: abs_fresh fresh_ty)
 
 subsection \<open>a fact about beta\<close>
 
 definition "NORMAL" :: "lam \<Rightarrow> bool" where
   "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^sub>\<beta> t')"
 
 lemma NORMAL_Var:
   shows "NORMAL (Var a)"
 proof -
   { assume "\<exists>t'. (Var a) \<longrightarrow>\<^sub>\<beta> t'"
     then obtain t' where "(Var a) \<longrightarrow>\<^sub>\<beta> t'" by blast
     hence False by (cases) (auto) 
   }
   thus "NORMAL (Var a)" by (auto simp add: NORMAL_def)
 qed
 
 text \<open>Inductive version of Strong Normalisation\<close>
 inductive 
   SN :: "lam \<Rightarrow> bool"
 where
   SN_intro: "(\<And>t'. t \<longrightarrow>\<^sub>\<beta> t' \<Longrightarrow> SN t') \<Longrightarrow> SN t"
 
 lemma SN_preserved: 
   assumes a: "SN t1" "t1\<longrightarrow>\<^sub>\<beta> t2"
   shows "SN t2"
 using a 
 by (cases) (auto)
 
 lemma double_SN_aux:
   assumes a: "SN a"
   and b: "SN b"
   and hyp: "\<And>x z.
     \<lbrakk>\<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> SN y; \<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> P y z;
      \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> SN u; \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z"
   shows "P a b"
 proof -
   from a
   have r: "\<And>b. SN b \<Longrightarrow> P a b"
   proof (induct a rule: SN.SN.induct)
     case (SN_intro x)
     note SNI' = SN_intro
     have "SN b" by fact
     thus ?case
     proof (induct b rule: SN.SN.induct)
       case (SN_intro y)
-      show ?case
-        apply (rule hyp)
-        apply (erule SNI')
-        apply (erule SNI')
-        apply (rule SN.SN_intro)
-        apply (erule SN_intro)+
-        done
+      with SNI' show ?case
+        by (metis SN.simps hyp)
     qed
   qed
   from b show ?thesis by (rule r)
 qed
 
 lemma double_SN[consumes 2]:
   assumes a: "SN a"
   and     b: "SN b" 
   and     c: "\<And>x z. \<lbrakk>\<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> P y z; \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z"
   shows "P a b"
 using a b c
-apply(rule_tac double_SN_aux)
-apply(assumption)+
-apply(blast)
-done
+  by (smt (verit, best) double_SN_aux)
 
 section \<open>Candidates\<close>
 
 nominal_primrec
   RED :: "ty \<Rightarrow> lam set"
 where
   "RED (TVar X) = {t. SN(t)}"
 | "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
 by (rule TrueI)+
 
 text \<open>neutral terms\<close>
 definition NEUT :: "lam \<Rightarrow> bool" where
   "NEUT t \<equiv> (\<exists>a. t = Var a) \<or> (\<exists>t1 t2. t = App t1 t2)" 
 
 (* a slight hack to get the first element of applications *)
 (* this is needed to get (SN t) from SN (App t s)         *) 
 inductive 
   FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
 where
   fst[intro!]:  "(App t s) \<guillemotright> t"
 
 nominal_primrec
   fst_app_aux::"lam\<Rightarrow>lam option"
 where
   "fst_app_aux (Var a)     = None"
 | "fst_app_aux (App t1 t2) = Some t1"
 | "fst_app_aux (Lam [x].t) = None"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: fresh_none)
-apply(fresh_guess)+
-done
+by (finite_guess | simp add: fresh_none | fresh_guess)+
 
 definition
   fst_app_def[simp]: "fst_app t = the (fst_app_aux t)"
 
 lemma SN_of_FST_of_App: 
   assumes a: "SN (App t s)"
   shows "SN (fst_app (App t s))"
 using a
 proof - 
   from a have "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> SN z"
     by (induct rule: SN.SN.induct)
        (blast elim: FST.cases intro: SN_intro)
   then have "SN t" by blast
   then show "SN (fst_app (App t s))" by simp
 qed
 
 section \<open>Candidates\<close>
 
 definition "CR1" :: "ty \<Rightarrow> bool" where
   "CR1 \<tau> \<equiv> \<forall>t. (t\<in>RED \<tau> \<longrightarrow> SN t)"
 
 definition "CR2" :: "ty \<Rightarrow> bool" where
   "CR2 \<tau> \<equiv> \<forall>t t'. (t\<in>RED \<tau> \<and> t \<longrightarrow>\<^sub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>"
 
 definition "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool" where
   "CR3_RED t \<tau> \<equiv> \<forall>t'. t\<longrightarrow>\<^sub>\<beta> t' \<longrightarrow>  t'\<in>RED \<tau>" 
 
 definition "CR3" :: "ty \<Rightarrow> bool" where
   "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"
    
 definition "CR4" :: "ty \<Rightarrow> bool" where
   "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
 
 lemma CR3_implies_CR4: 
   assumes a: "CR3 \<tau>" 
   shows "CR4 \<tau>"
 using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def)
 
 (* sub_induction in the arrow-type case for the next proof *) 
 lemma sub_induction: 
   assumes a: "SN(u)"
   and     b: "u\<in>RED \<tau>"
   and     c1: "NEUT t"
   and     c2: "CR2 \<tau>"
   and     c3: "CR3 \<sigma>"
   and     c4: "CR3_RED t (\<tau>\<rightarrow>\<sigma>)"
   shows "(App t u)\<in>RED \<sigma>"
 using a b
 proof (induct)
   fix u
   assume as: "u\<in>RED \<tau>"
   assume ih: " \<And>u'. \<lbrakk>u \<longrightarrow>\<^sub>\<beta> u'; u' \<in> RED \<tau>\<rbrakk> \<Longrightarrow> App t u' \<in> RED \<sigma>"
   have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def)
   moreover
   have "CR3_RED (App t u) \<sigma>" unfolding CR3_RED_def
   proof (intro strip)
     fix r
     assume red: "App t u \<longrightarrow>\<^sub>\<beta> r"
     moreover
     { assume "\<exists>t'. t \<longrightarrow>\<^sub>\<beta> t' \<and> r = App t' u"
       then obtain t' where a1: "t \<longrightarrow>\<^sub>\<beta> t'" and a2: "r = App t' u" by blast
       have "t'\<in>RED (\<tau>\<rightarrow>\<sigma>)" using c4 a1 by (simp add: CR3_RED_def)
       then have "App t' u\<in>RED \<sigma>" using as by simp
       then have "r\<in>RED \<sigma>" using a2 by simp
     }
     moreover
     { assume "\<exists>u'. u \<longrightarrow>\<^sub>\<beta> u' \<and> r = App t u'"
       then obtain u' where b1: "u \<longrightarrow>\<^sub>\<beta> u'" and b2: "r = App t u'" by blast
       have "u'\<in>RED \<tau>" using as b1 c2 by (auto simp add: CR2_def)
       with ih have "App t u' \<in> RED \<sigma>" using b1 by simp
       then have "r\<in>RED \<sigma>" using b2 by simp
     }
     moreover
     { assume "\<exists>x t'. t = Lam [x].t'"
       then obtain x t' where "t = Lam [x].t'" by blast
       then have "NEUT (Lam [x].t')" using c1 by simp
       then have "False" by (simp add: NEUT_def)
       then have "r\<in>RED \<sigma>" by simp
     }
     ultimately show "r \<in> RED \<sigma>" by (cases) (auto simp add: lam.inject)
   qed
   ultimately show "App t u \<in> RED \<sigma>" using c3 by (simp add: CR3_def)
 qed 
 
 text \<open>properties of the candiadates\<close>
 lemma RED_props: 
   shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
 proof (nominal_induct \<tau> rule: ty.strong_induct)
   case (TVar a)
   { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
   next
     case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def)
   next
     case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def)
   }
 next
   case (TArr \<tau>1 \<tau>2)
   { case 1
     have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
     have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
     have "\<And>t. t \<in> RED (\<tau>1 \<rightarrow> \<tau>2) \<Longrightarrow> SN t" 
     proof - 
       fix t
       assume "t \<in> RED (\<tau>1 \<rightarrow> \<tau>2)"
       then have a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2" by simp
       from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4) 
       moreover
       fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
       moreover
       have "NORMAL (Var a)" by (rule NORMAL_Var)
       ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
       with a have "App t (Var a) \<in> RED \<tau>2" by simp
       hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
       thus "SN t" by (auto dest: SN_of_FST_of_App)
     qed
     then show "CR1 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR1_def by simp
   next
     case 2
     have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
     then show "CR2 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR2_def by auto 
   next
     case 3
     have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
     have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
     have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
     show "CR3 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR3_def
     proof (simp, intro strip)
       fix t u
       assume a1: "u \<in> RED \<tau>1"
       assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
       have "SN(u)" using a1 ih_CR1_\<tau>1 by (simp add: CR1_def)
       then show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 a1 a2 by (blast intro: sub_induction)
     qed
   }
 qed
    
 text \<open>
   the next lemma not as simple as on paper, probably because of 
   the stronger double_SN induction 
 \<close> 
 lemma abs_RED: 
   assumes asm: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>"
   shows "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
 proof -
   have b1: "SN t" 
   proof -
     have "Var x\<in>RED \<tau>"
     proof -
       have "CR4 \<tau>" by (simp add: RED_props CR3_implies_CR4)
       moreover
       have "NEUT (Var x)" by (auto simp add: NEUT_def)
       moreover
       have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def)
       ultimately show "Var x\<in>RED \<tau>" by (simp add: CR4_def)
     qed
     then have "t[x::=Var x]\<in>RED \<sigma>" using asm by simp
     then have "t\<in>RED \<sigma>" by (simp add: id_subs)
     moreover 
     have "CR1 \<sigma>" by (simp add: RED_props)
     ultimately show "SN t" by (simp add: CR1_def)
   qed
   show "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
   proof (simp, intro strip)
     fix u
     assume b2: "u\<in>RED \<tau>"
     then have b3: "SN u" using RED_props by (auto simp add: CR1_def)
     show "App (Lam [x].t) u \<in> RED \<sigma>" using b1 b3 b2 asm
     proof(induct t u rule: double_SN)
       fix t u
       assume ih1: "\<And>t'.  \<lbrakk>t \<longrightarrow>\<^sub>\<beta> t'; u\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t'[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t') u \<in> RED \<sigma>" 
       assume ih2: "\<And>u'.  \<lbrakk>u \<longrightarrow>\<^sub>\<beta> u'; u'\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t) u' \<in> RED \<sigma>"
-      assume as1: "u \<in> RED \<tau>"
-      assume as2: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>"
+      assume u: "u \<in> RED \<tau>"
+      assume t: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>"
       have "CR3_RED (App (Lam [x].t) u) \<sigma>" unfolding CR3_RED_def
       proof(intro strip)
         fix r
         assume red: "App (Lam [x].t) u \<longrightarrow>\<^sub>\<beta> r"
         moreover
         { assume "\<exists>t'. t \<longrightarrow>\<^sub>\<beta> t' \<and> r = App (Lam [x].t') u"
-          then obtain t' where a1: "t \<longrightarrow>\<^sub>\<beta> t'" and a2: "r = App (Lam [x].t') u" by blast
-          have "App (Lam [x].t') u\<in>RED \<sigma>" using ih1 a1 as1 as2
-            apply(auto)
-            apply(drule_tac x="t'" in meta_spec)
-            apply(simp)
-            apply(drule meta_mp)
-            prefer 2
-            apply(auto)[1]
-            apply(rule ballI)
-            apply(drule_tac x="s" in bspec)
-            apply(simp)
-            apply(subgoal_tac "CR2 \<sigma>")(*A*)
-            apply(unfold CR2_def)[1]
-            apply(drule_tac x="t[x::=s]" in spec)
-            apply(drule_tac x="t'[x::=s]" in spec)
-            apply(simp add: beta_subst)
-            (*A*)
-            apply(simp add: RED_props)
-            done
-          then have "r\<in>RED \<sigma>" using a2 by simp
+          then obtain t' where "t \<longrightarrow>\<^sub>\<beta> t'" and t': "r = App (Lam [x].t') u" 
+            by blast
+          then have "\<forall>s\<in>RED \<tau>. t'[x::=s] \<in> RED \<sigma>"
+            using CR2_def RED_props(2) t beta_subst by blast
+          then have "App (Lam [x].t') u\<in>RED \<sigma>"
+            using \<open>t \<longrightarrow>\<^sub>\<beta> t'\<close> u ih1 by blast 
+          then have "r\<in>RED \<sigma>" using t' by simp
         }
         moreover
         { assume "\<exists>u'. u \<longrightarrow>\<^sub>\<beta> u' \<and> r = App (Lam [x].t) u'"
-          then obtain u' where b1: "u \<longrightarrow>\<^sub>\<beta> u'" and b2: "r = App (Lam [x].t) u'" by blast
-          have "App (Lam [x].t) u'\<in>RED \<sigma>" using ih2 b1 as1 as2
-            apply(auto)
-            apply(drule_tac x="u'" in meta_spec)
-            apply(simp)
-            apply(drule meta_mp)
-            apply(subgoal_tac "CR2 \<tau>")
-            apply(unfold CR2_def)[1]
-            apply(drule_tac x="u" in spec)
-            apply(drule_tac x="u'" in spec)
-            apply(simp)
-            apply(simp add: RED_props)
-            apply(simp)
-            done
-          then have "r\<in>RED \<sigma>" using b2 by simp
+          then obtain u' where "u \<longrightarrow>\<^sub>\<beta> u'" and u': "r = App (Lam [x].t) u'" by blast
+          have "CR2 \<tau>"
+            by (simp add: RED_props(2))
+          then
+          have "App (Lam [x].t) u'\<in>RED \<sigma>"
+            using CR2_def ih2 \<open>u \<longrightarrow>\<^sub>\<beta> u'\<close> t u by blast
+          then have "r\<in>RED \<sigma>" using u' by simp
         }
         moreover
         { assume "r = t[x::=u]"
-          then have "r\<in>RED \<sigma>" using as1 as2 by auto
+          then have "r\<in>RED \<sigma>" using u t by auto
         }
-        ultimately show "r \<in> RED \<sigma>" 
+        ultimately show "r \<in> RED \<sigma>"
+          by cases (auto simp: alpha subst_rename lam.inject dest: beta_abs)
           (* one wants to use the strong elimination principle; for this one 
              has to know that x\<sharp>u *)
-        apply(cases) 
-        apply(auto simp add: lam.inject)
-        apply(drule beta_abs)
-        apply(auto)[1]
-        apply(auto simp add: alpha subst_rename)
-        done
     qed
     moreover 
     have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto)
     ultimately show "App (Lam [x].t) u \<in> RED \<sigma>"  using RED_props by (simp add: CR3_def)
   qed
 qed
 qed
 
 abbreviation 
  mapsto :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> bool" ("_ maps _ to _" [55,55,55] 55) 
 where
  "\<theta> maps x to e \<equiv> (lookup \<theta> x) = e"
 
 abbreviation 
   closes :: "(name\<times>lam) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ closes _" [55,55] 55) 
 where
   "\<theta> closes \<Gamma> \<equiv> \<forall>x T. ((x,T) \<in> set \<Gamma> \<longrightarrow> (\<exists>t. \<theta> maps x to t \<and> t \<in> RED T))"
 
 lemma all_RED: 
   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   and     b: "\<theta> closes \<Gamma>"
   shows "\<theta><t> \<in> RED \<tau>"
 using a b
 proof(nominal_induct  avoiding: \<theta> rule: typing.strong_induct)
   case (t3 a \<Gamma> \<sigma> t \<tau> \<theta>) \<comment> \<open>lambda case\<close>
   have ih: "\<And>\<theta>. \<theta> closes ((a,\<sigma>)#\<Gamma>) \<Longrightarrow> \<theta><t> \<in> RED \<tau>" by fact
   have \<theta>_cond: "\<theta> closes \<Gamma>" by fact
   have fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" by fact+
   from ih have "\<forall>s\<in>RED \<sigma>. ((a,s)#\<theta>)<t> \<in> RED \<tau>" using fresh \<theta>_cond fresh_context by simp
   then have "\<forall>s\<in>RED \<sigma>. \<theta><t>[a::=s] \<in> RED \<tau>" using fresh by (simp add: psubst_subst)
   then have "Lam [a].(\<theta><t>) \<in> RED (\<sigma> \<rightarrow> \<tau>)" by (simp only: abs_RED)
   then show "\<theta><(Lam [a].t)> \<in> RED (\<sigma> \<rightarrow> \<tau>)" using fresh by simp
 qed auto
 
 section \<open>identity substitution generated from a context \<Gamma>\<close>
 fun
   "id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list"
 where
   "id []    = []"
 | "id ((x,\<tau>)#\<Gamma>) = (x,Var x)#(id \<Gamma>)"
 
 lemma id_maps:
   shows "(id \<Gamma>) maps a to (Var a)"
 by (induct \<Gamma>) (auto)
 
 lemma id_fresh:
   fixes a::"name"
   assumes a: "a\<sharp>\<Gamma>"
   shows "a\<sharp>(id \<Gamma>)"
 using a
 by (induct \<Gamma>)
    (auto simp add: fresh_list_nil fresh_list_cons)
 
 lemma id_apply:  
   shows "(id \<Gamma>)<t> = t"
 by (nominal_induct t avoiding: \<Gamma> rule: lam.strong_induct)
    (auto simp add: id_maps id_fresh)
 
 lemma id_closes:
   shows "(id \<Gamma>) closes \<Gamma>"
-apply(auto)
-apply(simp add: id_maps)
-apply(subgoal_tac "CR3 T") \<comment> \<open>A\<close>
-apply(drule CR3_implies_CR4)
-apply(simp add: CR4_def)
-apply(drule_tac x="Var x" in spec)
-apply(force simp add: NEUT_def NORMAL_Var)
-\<comment> \<open>A\<close>
-apply(rule RED_props)
-done
+  by (metis CR3_implies_CR4 CR4_def NEUT_def NORMAL_Var RED_props(3) id_maps)
 
-lemma typing_implies_RED:  
+lemma typing_implies_RED:
   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   shows "t \<in> RED \<tau>"
 proof -
   have "(id \<Gamma>)<t>\<in>RED \<tau>" 
   proof -
     have "(id \<Gamma>) closes \<Gamma>" by (rule id_closes)
     with a show ?thesis by (rule all_RED)
   qed
   thus"t \<in> RED \<tau>" by (simp add: id_apply)
 qed
 
 lemma typing_implies_SN: 
   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   shows "SN(t)"
 proof -
   from a have "t \<in> RED \<tau>" by (rule typing_implies_RED)
   moreover
   have "CR1 \<tau>" by (rule RED_props)
   ultimately show "SN(t)" by (simp add: CR1_def)
 qed
 
 end