# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1713713490 -3600
# Node ID 6d56e85f674e77ccd8527d32b89376e9bd435db4
# Parent  fec5a23017b55f7c7f85f021c361088c63830f5d
More proof tidying for Nominal

diff -r fec5a23017b5 -r 6d56e85f674e src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sat Apr 20 23:02:47 2024 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Apr 21 16:31:30 2024 +0100
@@ -62,21 +62,23 @@
   by (simp add: supp_def Collect_disj_eq del: disj_not1)
 
 instance pat :: pt_name
-proof (standard, goal_cases)
-  case (1 x)
-  show ?case by (induct x) simp_all
-next
-  case (2 _ _ x)
-  show ?case by (induct x) (simp_all add: pt_name2)
-next
-  case (3 _ _ x)
-  then show ?case by (induct x) (simp_all add: pt_name3)
+proof
+  fix x :: pat
+  show "([]::(name \<times> _) list) \<bullet> x = x"
+    by (induct x) simp_all
+  fix pi1 pi2 :: "(name \<times> name) list"
+  show "(pi1 @ pi2) \<bullet> x = pi1 \<bullet> pi2 \<bullet> x"
+    by (induct x) (simp_all add: pt_name2)
+  assume "pi1 \<triangleq> pi2"
+  then show "pi1 \<bullet> x = pi2 \<bullet> x"
+    by (induct x) (simp_all add: pt_name3)
 qed
 
 instance pat :: fs_name
-proof (standard, goal_cases)
-  case (1 x)
-  show ?case by (induct x) (simp_all add: fin_supp)
+proof
+  fix x :: pat
+  show "finite (supp x::name set)"
+    by (induct x) (simp_all add: fin_supp)
 qed
 
 (* the following function cannot be defined using nominal_primrec, *)
@@ -255,21 +257,15 @@
 lemma weakening: 
   assumes "\<Gamma>\<^sub>1 \<turnstile> t : T" and "valid \<Gamma>\<^sub>2" and "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2"
   shows "\<Gamma>\<^sub>2 \<turnstile> t : T" using assms
-  apply (nominal_induct \<Gamma>\<^sub>1 t T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct)
-  apply auto
-  apply (drule_tac x="(x, T) # \<Gamma>\<^sub>2" in meta_spec)
-  apply (auto intro: valid_typing)
-  apply (drule_tac x="\<Gamma>\<^sub>2" in meta_spec)
-  apply (drule_tac x="\<Delta> @ \<Gamma>\<^sub>2" in meta_spec)
-  apply (auto intro: valid_typing)
-  apply (rule typing.Let)
-  apply assumption+
-  apply (drule meta_mp)
-  apply (rule valid_app_mono)
-  apply (rule valid_typing)
-  apply assumption
-  apply (auto simp add: pat_freshs)
-  done
+proof (nominal_induct \<Gamma>\<^sub>1 t T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct)
+  case (Abs x T \<Gamma> t U)
+  then show ?case
+    by (simp add: typing.Abs valid.Cons)
+next
+  case (Let p t \<Gamma> T \<Delta> u U)
+  then show ?case
+    by (smt (verit, ccfv_threshold) Un_iff pat_freshs set_append typing.simps valid_app_mono valid_typing) 
+qed auto
 
 inductive
   match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool"  ("\<turnstile> _ \<rhd> _ \<Rightarrow> _" [50, 50, 50] 50)
@@ -301,27 +297,20 @@
 | "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>x:T. t\<rparr> = (\<lambda>x:T. \<theta>\<lparr>t\<rparr>)"
 | "\<theta>\<lparr>Base t\<rparr>\<^sub>b = Base (\<theta>\<lparr>t\<rparr>)"
 | "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>Bind T x t\<rparr>\<^sub>b = Bind T x (\<theta>\<lparr>t\<rparr>\<^sub>b)"
-  apply finite_guess+
-  apply (simp add: abs_fresh | fresh_guess)+
-  done
+  by (finite_guess | simp add: abs_fresh | fresh_guess)+
 
 lemma lookup_fresh:
   "x = y \<longrightarrow> x \<in> set (map fst \<theta>) \<Longrightarrow> \<forall>(y, t)\<in>set \<theta>. x \<sharp> t \<Longrightarrow> x \<sharp> lookup \<theta> y"
-  apply (induct \<theta>)
-  apply (simp_all add: split_paired_all fresh_atm)
-  apply (case_tac "x = y")
-  apply (auto simp add: fresh_atm)
-  done
+  by (induct \<theta>) (use fresh_atm in force)+
 
 lemma psubst_fresh:
   assumes "x \<in> set (map fst \<theta>)" and "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t"
   shows "x \<sharp> \<theta>\<lparr>t\<rparr>" and "x \<sharp> \<theta>\<lparr>t'\<rparr>\<^sub>b" using assms
-  apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
-  apply simp
-  apply (rule lookup_fresh)
-  apply (rule impI)
-  apply (simp_all add: abs_fresh)
-  done
+proof (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
+  case (Var name)
+  then show ?case
+    by (metis lookup_fresh simps(1))
+qed (auto simp: abs_fresh)
 
 lemma psubst_eqvt[eqvt]:
   fixes pi :: "name prm" 
@@ -350,23 +339,21 @@
 lemma psubst_forget:
   "(supp (map fst \<theta>)::name set) \<sharp>* t \<Longrightarrow> \<theta>\<lparr>t\<rparr> = t"
   "(supp (map fst \<theta>)::name set) \<sharp>* t' \<Longrightarrow> \<theta>\<lparr>t'\<rparr>\<^sub>b = t'"
-  apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
-  apply (auto simp add: fresh_star_def lookup_forget abs_fresh)
-  apply (drule_tac x=\<theta> in meta_spec)
-  apply (drule meta_mp)
-  apply (rule ballI)
-  apply (drule_tac x=x in bspec)
-  apply assumption
-  apply (drule supp_fst)
-  apply (auto simp add: fresh_def)
-  apply (drule_tac x=\<theta> in meta_spec)
-  apply (drule meta_mp)
-  apply (rule ballI)
-  apply (drule_tac x=x in bspec)
-  apply assumption
-  apply (drule supp_fst)
-  apply (auto simp add: fresh_def)
-  done
+proof (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
+  case (Var name)
+  then show ?case
+    by (simp add: fresh_star_set lookup_forget)
+next
+  case (Abs ty name trm)
+  then show ?case
+    apply (simp add: fresh_def)
+    by (metis abs_fresh(1) fresh_star_set supp_fst trm.fresh(3))
+next
+  case (Bind ty name btrm)
+  then show ?case
+    apply (simp add: fresh_def)
+    by (metis abs_fresh(1) btrm.fresh(2) fresh_star_set supp_fst)
+qed (auto simp: fresh_star_set)
 
 lemma psubst_nil: "[]\<lparr>t\<rparr> = t" "[]\<lparr>t'\<rparr>\<^sub>b = t'"
   by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil)
@@ -557,17 +544,15 @@
   Abs: "{x}"
 | Beta: "{x}"
 | Let: "(supp p)::name set"
-  apply (simp_all add: fresh_star_def abs_fresh fin_supp)
-  apply (rule psubst_fresh)
-  apply simp
-  apply simp
-  apply (rule ballI)
-  apply (rule psubst_fresh)
-  apply (rule match_vars)
-  apply assumption+
-  apply (rule match_fresh_mono)
-  apply auto
-  done
+proof (simp_all add: fresh_star_def abs_fresh fin_supp)
+  show "x \<sharp> t[x\<mapsto>u]" if "x \<sharp> u" for x t u
+    by (simp add: \<open>x \<sharp> u\<close> psubst_fresh(1))
+next
+  show "\<forall>x\<in>supp p. (x::name) \<sharp> \<theta>\<lparr>u\<rparr>" 
+    if "\<forall>x\<in>supp p. (x::name) \<sharp> t" and "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>"
+    for p t \<theta> u
+    by (meson that match_fresh_mono match_vars psubst_fresh(1))
+qed
 
 lemma typing_case_Abs:
   assumes ty: "\<Gamma> \<turnstile> (\<lambda>x:T. t) : S"
@@ -636,13 +621,16 @@
 proof
   fix x assume "x \<in> pi \<bullet> B"
   then show "x \<in> A \<union> B" using pi
-    apply (induct pi arbitrary: x B rule: rev_induct)
-    apply simp
-    apply (simp add: split_paired_all supp_eqvt)
-    apply (drule perm_mem_left)
-    apply (simp add: calc_atm split: if_split_asm)
-    apply (auto dest: perm_mem_right)
-    done
+  proof (induct pi arbitrary: x B rule: rev_induct)
+    case Nil
+    then show ?case
+      by simp
+  next
+    case (snoc y xs)
+    then show ?case
+      apply simp
+      by (metis SigmaE perm_mem_left perm_pi_simp(2) pt_name2 swap_simps(3))
+  qed
 qed
 
 lemma abs_pat_alpha':
diff -r fec5a23017b5 -r 6d56e85f674e src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Sat Apr 20 23:02:47 2024 +0100
+++ b/src/HOL/Nominal/Examples/W.thy	Sun Apr 21 16:31:30 2024 +0100
@@ -13,17 +13,15 @@
 
 lemma difference_eqvt_tvar[eqvt]:
   fixes pi::"tvar prm"
-  and   Xs Ys::"tvar list"
+    and   Xs Ys::"tvar list"
   shows "pi\<bullet>(Xs - Ys) = (pi\<bullet>Xs) - (pi\<bullet>Ys)"
-by (induct Xs) (simp_all add: eqvts)
+  by (induct Xs) (simp_all add: eqvts)
 
-lemma difference_fresh:
+lemma difference_fresh [simp]:
   fixes X::"tvar"
-  and   Xs Ys::"tvar list"
-  assumes a: "X\<in>set Ys"
-  shows "X\<sharp>(Xs - Ys)"
-using a
-by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)
+    and   Xs Ys::"tvar list"
+  shows "X\<sharp>(Xs - Ys) \<longleftrightarrow> X\<sharp>Xs \<or> X\<in>set Ys"
+  by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)
 
 lemma difference_supset:
   fixes xs::"'a list"
@@ -114,10 +112,8 @@
 where
   "ftv_tyS (Ty T)    = ((ftv (T::ty))::tvar list)"
 | "ftv_tyS (\<forall>[X].S) = (ftv_tyS S) - [X]"
-apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+
-apply(rule TrueI)+
-apply(rule difference_fresh)
-apply(simp)
+apply(finite_guess add: ftv_ty_eqvt fs_tvar1 | rule TrueI)+
+  apply (metis difference_fresh list.set_intros(1))
 apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
 done
 
@@ -127,18 +123,21 @@
   fixes pi::"tvar prm"
   and   S::"tyS"
   shows "pi\<bullet>(ftv S) = ftv (pi\<bullet>S)"
-apply(nominal_induct S rule: tyS.strong_induct)
-apply(simp add: eqvts)
-apply(simp only: ftv_tyS.simps)
-apply(simp only: eqvts)
-apply(simp add: eqvts)
-done 
+proof (nominal_induct S rule: tyS.strong_induct)
+  case (Ty ty)
+  then show ?case
+    by (simp add: ftv_ty_eqvt)
+next
+  case (ALL tvar tyS)
+  then show ?case 
+    by (metis difference_eqvt_tvar ftv_ty.simps(1) ftv_tyS.simps(2) ftv_ty_eqvt ty.perm(3) tyS.perm(4))
+qed
 
 lemma ftv_Ctxt_eqvt[eqvt]:
   fixes pi::"tvar prm"
-  and   \<Gamma>::"Ctxt"
+    and   \<Gamma>::"Ctxt"
   shows "pi\<bullet>(ftv \<Gamma>) = ftv (pi\<bullet>\<Gamma>)"
-by (induct \<Gamma>) (auto simp add: eqvts)
+  by (induct \<Gamma>) (auto simp add: eqvts)
 
 text \<open>Valid\<close>
 inductive
@@ -157,7 +156,7 @@
 lemma gen_eqvt[eqvt]:
   fixes pi::"tvar prm"
   shows "pi\<bullet>(gen T Xs) = gen (pi\<bullet>T) (pi\<bullet>Xs)"
-by (induct Xs) (simp_all add: eqvts)
+  by (induct Xs) (simp_all add: eqvts)
 
 
 
@@ -169,7 +168,7 @@
 lemma close_eqvt[eqvt]:
   fixes pi::"tvar prm"
   shows "pi\<bullet>(close \<Gamma> T) = close (pi\<bullet>\<Gamma>) (pi\<bullet>T)"
-by (simp_all only: eqvts)
+  by (simp_all only: eqvts)
   
 text \<open>Substitution\<close>
 
@@ -183,8 +182,7 @@
 where
   "smth[X::=T] \<equiv> ([(X,T)])<smth>" 
 
-fun
-  lookup :: "Subst \<Rightarrow> tvar \<Rightarrow> ty"   
+fun lookup :: "Subst \<Rightarrow> tvar \<Rightarrow> ty"   
 where
   "lookup [] X        = TVar X"
 | "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
@@ -192,15 +190,15 @@
 lemma lookup_eqvt[eqvt]:
   fixes pi::"tvar prm"
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
-by (induct \<theta>) (auto simp add: eqvts)
+  by (induct \<theta>) (auto simp add: eqvts)
 
 lemma lookup_fresh:
   fixes X::"tvar"
   assumes a: "X\<sharp>\<theta>"
   shows "lookup \<theta> X = TVar X"
-using a
-by (induct \<theta>)
-   (auto simp add: fresh_list_cons fresh_prod fresh_atm)
+  using a
+  by (induct \<theta>)
+    (auto simp add: fresh_list_cons fresh_prod fresh_atm)
 
 overloading 
   psubst_ty \<equiv> "psubst :: Subst \<Rightarrow> ty \<Rightarrow> ty"
@@ -231,9 +229,7 @@
 where 
   "\<theta><(Ty T)> = Ty (\<theta><T>)"
 | "X\<sharp>\<theta> \<Longrightarrow> \<theta><(\<forall>[X].S)> = \<forall>[X].(\<theta><S>)"
-apply(finite_guess add: psubst_ty_eqvt fs_tvar1)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh)
+apply(finite_guess add: psubst_ty_eqvt fs_tvar1 | simp add: abs_fresh)+
 apply(fresh_guess add: psubst_ty_eqvt fs_tvar1)+
 done
 
@@ -330,26 +326,26 @@
   assumes a: "X\<sharp>\<theta>" 
   shows "\<theta><T[X::=T']> = (\<theta><T>)[X::=\<theta><T'>]"
 using a
-apply(nominal_induct T avoiding: \<theta> X T' rule: ty.strong_induct)
-apply(auto simp add: ty.inject lookup_fresh)
-apply(rule sym)
-apply(rule subst_forget_ty)
-apply(rule fresh_lookup)
-apply(simp_all add: fresh_atm)
-done
+proof (nominal_induct T avoiding: \<theta> X T' rule: ty.strong_induct)
+  case (TVar tvar)
+  then show ?case
+    by (simp add: fresh_atm(1) fresh_lookup lookup_fresh subst_forget_ty)
+qed auto
 
 lemma general_preserved:
   fixes \<theta>::"Subst"
   assumes a: "T \<prec> S"
   shows "\<theta><T> \<prec> \<theta><S>"
-using a
-apply(nominal_induct T S avoiding: \<theta> rule: inst.strong_induct)
-apply(auto)[1]
-apply(simp add: psubst_ty_lemma)
-apply(rule_tac I_All)
-apply(simp add: fresh_psubst_ty)
-apply(simp)
-done
+  using a
+proof (nominal_induct T S avoiding: \<theta> rule: inst.strong_induct)
+  case (I_Ty T)
+  then show ?case
+    by (simp add: inst.I_Ty)
+next
+  case (I_All X T' T S)
+  then show ?case
+    by (simp add: fresh_psubst_ty inst.I_All psubst_ty_lemma)
+qed
 
 
 text\<open>typing judgements\<close>
@@ -386,74 +382,72 @@
 lemma ftv_Ctxt: 
   fixes \<Gamma>::"Ctxt"
   shows "supp \<Gamma> = set (ftv \<Gamma>)"
-apply (induct \<Gamma>)
-apply (simp_all add: supp_list_nil supp_list_cons)
-apply (rename_tac a \<Gamma>')
-apply (case_tac a)
-apply (simp add: supp_prod supp_atm ftv_tyS)
-done
+proof (induct \<Gamma>)
+  case Nil
+  then show ?case
+    by (simp add: supp_list_nil)
+next
+  case (Cons c \<Gamma>)
+  show ?case
+  proof (cases c)
+    case (Pair a b)
+    with Cons show ?thesis
+      by (simp add: ftv_tyS supp_atm(3) supp_list_cons supp_prod)
+  qed
+qed
 
-lemma ftv_tvars: 
+lemma ftv_tvars:
   fixes Tvs::"tvar list"
   shows "supp Tvs = set Tvs"
-by (induct Tvs) 
-   (simp_all add: supp_list_nil supp_list_cons supp_atm)
+  by (induct Tvs) (simp_all add: supp_list_nil supp_list_cons supp_atm)
 
 lemma difference_supp: 
   fixes xs ys::"tvar list"
   shows "((supp (xs - ys))::tvar set) = supp xs - supp ys"
-by (induct xs) 
-   (auto simp add: supp_list_nil supp_list_cons ftv_tvars)
+  by (induct xs) (auto simp add: supp_list_nil supp_list_cons ftv_tvars)
 
 lemma set_supp_eq: 
   fixes xs::"tvar list"
   shows "set xs = supp xs"
-by (induct xs) 
-   (simp_all add: supp_list_nil supp_list_cons supp_atm)
+  by (induct xs) (simp_all add: supp_list_nil supp_list_cons supp_atm)
 
 nominal_inductive2 typing
   avoids T_LET: "set (ftv T\<^sub>1 - ftv \<Gamma>)"
-apply (simp add: fresh_star_def fresh_def ftv_Ctxt)
-apply (simp add: fresh_star_def fresh_tvar_trm)
-apply assumption
-apply simp
-done
+     apply (simp_all add: fresh_star_def fresh_def ftv_Ctxt fresh_tvar_trm)
+  by (meson fresh_def fresh_tvar_trm)
+
 
 lemma perm_fresh_fresh_aux:
   "\<forall>(x,y)\<in>set (pi::tvar prm). x \<sharp> z \<and> y \<sharp> z \<Longrightarrow> pi \<bullet> (z::'a::pt_tvar) = z"
-  apply (induct pi rule: rev_induct)
-  apply simp
+proof (induct pi rule: rev_induct)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (snoc x xs)
+  then show ?case
   apply (simp add: split_paired_all pt_tvar2)
-  apply (frule_tac x="(a, b)" in bspec)
-  apply simp
-  apply (simp add: perm_fresh_fresh)
-  done
+    using perm_fresh_fresh(1) by fastforce
+qed
 
 lemma freshs_mem:
   fixes S::"tvar set"
   assumes "x \<in> S"
-  and     "S \<sharp>* z"
+    and     "S \<sharp>* z"
   shows  "x \<sharp> z"
-using assms by (simp add: fresh_star_def)
+  using assms by (simp add: fresh_star_def)
 
 lemma fresh_gen_set:
   fixes X::"tvar"
   and   Xs::"tvar list"
-  assumes asm: "X\<in>set Xs" 
+  assumes "X\<in>set Xs" 
   shows "X\<sharp>gen T Xs"
-using asm
-apply(induct Xs)
-apply(simp)
-apply(rename_tac a Xs')
-apply(case_tac "X=a")
-apply(simp add: abs_fresh)
-apply(simp add: abs_fresh)
-done
+  using assms by (induct Xs) (auto simp: abs_fresh)
 
 lemma close_fresh:
   fixes \<Gamma>::"Ctxt"
   shows "\<forall>(X::tvar)\<in>set ((ftv T) - (ftv \<Gamma>)). X\<sharp>(close \<Gamma> T)"
-by (simp add: fresh_gen_set)
+  by (meson fresh_gen_set)
 
 lemma gen_supp: 
   shows "(supp (gen T Xs)::tvar set) = supp T - supp Xs"
@@ -466,9 +460,7 @@
 
 lemma close_supp: 
   shows "supp (close \<Gamma> T) = set (ftv T) \<inter> set (ftv \<Gamma>)"
-  apply (simp add: gen_supp difference_supp ftv_ty ftv_Ctxt)
-  apply (simp only: set_supp_eq minus_Int_eq)
-  done
+  using difference_supp ftv_ty gen_supp set_supp_eq by auto
 
 lemma better_T_LET:
   assumes x: "x\<sharp>\<Gamma>"
@@ -483,22 +475,12 @@
   from pi1 have pi1': "(pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)) \<sharp>* \<Gamma>"
     by (simp add: fresh_star_prod)
   have Gamma_fresh: "\<forall>(x,y)\<in>set pi. x \<sharp> \<Gamma> \<and> y \<sharp> \<Gamma>"
-    apply (rule ballI)
-    apply (simp add: split_paired_all)
-    apply (drule subsetD [OF pi2])
-    apply (erule SigmaE)
-    apply (drule freshs_mem [OF _ pi1'])
-    apply (simp add: ftv_Ctxt [symmetric] fresh_def)
-    done
-  have close_fresh': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1"
-    apply (rule ballI)
-    apply (simp add: split_paired_all)
-    apply (drule subsetD [OF pi2])
-    apply (erule SigmaE)
-    apply (drule bspec [OF close_fresh])
-    apply (drule freshs_mem [OF _ pi1'])
-    apply (simp add: fresh_def close_supp ftv_Ctxt)
-    done
+    using freshs_mem [OF _ pi1'] subsetD [OF pi2] ftv_Ctxt fresh_def by fastforce
+  have "\<And>x y. \<lbrakk>x \<in> set (ftv T\<^sub>1 - ftv \<Gamma>); y \<in> pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)\<rbrakk>
+              \<Longrightarrow> x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1"
+    by (metis DiffE filter_set fresh_def fresh_gen_set freshs_mem ftv_Ctxt ftv_ty gen_supp member_filter pi1')
+  then have close_fresh': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1"
+    using pi2 by auto
   note x
   moreover from Gamma_fresh perm_boolI [OF t1, of pi]
   have "\<Gamma> \<turnstile> t\<^sub>1 : pi \<bullet> T\<^sub>1"
@@ -518,96 +500,81 @@
   fixes T::"ty"
   and   \<theta>::"Subst"
   and   X Y ::"tvar"
-  assumes a1: "X \<in> set (ftv T)"
-  and     a2: "Y \<in> set (ftv (lookup \<theta> X))"
+  assumes "X \<in> set (ftv T)"
+  and     "Y \<in> set (ftv (lookup \<theta> X))"
   shows "Y \<in> set (ftv (\<theta><T>))"
-using a1 a2
-by (nominal_induct T rule: ty.strong_induct) (auto)
+  using assms
+  by (nominal_induct T rule: ty.strong_induct) (auto)
 
 lemma ftv_tyS_subst:
   fixes S::"tyS"
   and   \<theta>::"Subst"
   and   X Y::"tvar"
-  assumes a1: "X \<in> set (ftv S)"
-  and     a2: "Y \<in> set (ftv (lookup \<theta> X))"
+  assumes "X \<in> set (ftv S)"
+  and     "Y \<in> set (ftv (lookup \<theta> X))"
   shows "Y \<in> set (ftv (\<theta><S>))"
-using a1 a2
+  using assms
 by (nominal_induct S avoiding: \<theta> Y rule: tyS.strong_induct) 
    (auto simp add: ftv_ty_subst fresh_atm)
 
 lemma ftv_Ctxt_subst:
   fixes \<Gamma>::"Ctxt"
   and   \<theta>::"Subst"
-  assumes a1: "X \<in> set (ftv \<Gamma>)"
-  and     a2: "Y \<in> set (ftv (lookup \<theta> X))"
+assumes "X \<in> set (ftv \<Gamma>)"
+  and   "Y \<in> set (ftv (lookup \<theta> X))"
   shows "Y \<in> set (ftv (\<theta><\<Gamma>>))"
-using a1 a2
-by (induct \<Gamma>)
-   (auto simp add: ftv_tyS_subst)
+  using assms by (induct \<Gamma>) (auto simp add: ftv_tyS_subst)
 
 lemma gen_preserved1:
-  assumes asm: "Xs \<sharp>* \<theta>"
+  assumes "Xs \<sharp>* \<theta>"
   shows "\<theta><gen T Xs> = gen (\<theta><T>) Xs"
-using asm
-by (induct Xs) 
-   (auto simp add: fresh_star_def)
+  using assms by (induct Xs) (auto simp add: fresh_star_def)
 
 lemma gen_preserved2:
   fixes T::"ty"
   and   \<Gamma>::"Ctxt"
-  assumes asm: "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>"
+  assumes "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>"
   shows "((ftv (\<theta><T>)) - (ftv (\<theta><\<Gamma>>))) = ((ftv T) - (ftv \<Gamma>))"
-using asm
-apply(nominal_induct T rule: ty.strong_induct)
-apply(auto simp add: fresh_star_def)
-apply(simp add: lookup_fresh)
-apply(simp add: ftv_Ctxt[symmetric])
-apply(fold fresh_def)
-apply(rule fresh_psubst_Ctxt)
-apply(assumption)
-apply(assumption)
-apply(rule difference_supset)
-apply(auto)
-apply(simp add: ftv_Ctxt_subst)
-done
+  using assms
+proof(nominal_induct T rule: ty.strong_induct)
+  case (TVar tvar)
+  then show ?case
+    apply(auto simp add: fresh_star_def ftv_Ctxt_subst)
+    by (metis filter.simps fresh_def fresh_psubst_Ctxt ftv_Ctxt ftv_ty.simps(1) lookup_fresh)
+next
+  case (Fun ty1 ty2)
+  then show ?case
+    by (simp add: fresh_star_list) 
+qed
 
 lemma close_preserved:
   fixes \<Gamma>::"Ctxt"
-  assumes asm: "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>"
+  assumes "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>"
   shows "\<theta><close \<Gamma> T> = close (\<theta><\<Gamma>>) (\<theta><T>)"
-using asm
-by (simp add: gen_preserved1 gen_preserved2)
+  using assms by (simp add: gen_preserved1 gen_preserved2)
 
 lemma var_fresh_for_ty:
   fixes x::"var"
-  and   T::"ty"
+    and   T::"ty"
   shows "x\<sharp>T"
-by (nominal_induct T rule: ty.strong_induct)
-   (simp_all add: fresh_atm)
+  by (nominal_induct T rule: ty.strong_induct) (simp_all add: fresh_atm)
 
 lemma var_fresh_for_tyS:
-  fixes x::"var"
-  and   S::"tyS"
+  fixes x::"var" and S::"tyS"
   shows "x\<sharp>S"
-by (nominal_induct S rule: tyS.strong_induct)
-   (simp_all add: abs_fresh var_fresh_for_ty)
+  by (nominal_induct S rule: tyS.strong_induct) (simp_all add: abs_fresh var_fresh_for_ty)
 
 lemma psubst_fresh_Ctxt:
-  fixes x::"var"
-  and   \<Gamma>::"Ctxt"
-  and   \<theta>::"Subst"
+  fixes x::"var" and \<Gamma>::"Ctxt" and \<theta>::"Subst"
   shows "x\<sharp>\<theta><\<Gamma>> = x\<sharp>\<Gamma>"
-by (induct \<Gamma>)
-   (auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS)
+  by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS)
 
 lemma psubst_valid:
   fixes \<theta>::Subst
-  and   \<Gamma>::Ctxt
-  assumes a: "valid \<Gamma>"
+    and   \<Gamma>::Ctxt
+  assumes "valid \<Gamma>"
   shows "valid (\<theta><\<Gamma>>)"
-using a
-by (induct) 
-   (auto simp add: psubst_fresh_Ctxt)
+  using assms by (induct) (auto simp add: psubst_fresh_Ctxt)
 
 lemma psubst_in:
   fixes \<Gamma>::"Ctxt"
@@ -616,17 +583,14 @@
   and   S::"tyS"
   assumes a: "(x,S)\<in>set \<Gamma>"
   shows "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)"
-using a
-by (induct \<Gamma>)
-   (auto simp add: calc_atm)
-
+  using a by (induct \<Gamma>) (auto simp add: calc_atm)
 
 lemma typing_preserved:
   fixes \<theta>::"Subst"
-  and   pi::"tvar prm"
-  assumes a: "\<Gamma> \<turnstile> t : T"
+    and   pi::"tvar prm"
+  assumes "\<Gamma> \<turnstile> t : T"
   shows "(\<theta><\<Gamma>>) \<turnstile> t : (\<theta><T>)"
-using a
+  using assms
 proof (nominal_induct \<Gamma> t T avoiding: \<theta> rule: typing.strong_induct)
   case (T_VAR \<Gamma> x S T)
   have a1: "valid \<Gamma>" by fact
@@ -662,14 +626,7 @@
   have a2: "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1>" by fact 
   have a3: "\<theta><((x, close \<Gamma> T1)#\<Gamma>)> \<turnstile> t2 : \<theta><T2>" by fact
   from a2 a3 show "\<theta><\<Gamma>> \<turnstile> Let x be t1 in t2 : \<theta><T2>"
-    apply -
-    apply(rule better_T_LET)
-    apply(rule a1)
-    apply(rule a2)
-    apply(simp add: close_preserved vc)
-    done
+    by (simp add: a1 better_T_LET close_preserved vc)
 qed
 
-
-
 end