# HG changeset patch
# User urbanc
# Date 1223873665 -7200
# Node ID e1659c30f48d6d18afdfaeab6fb51da575aee7e0
# Parent  3caee0cd91d882f9c6ca7dcb3e9e13c4e1ceba38
tuned

diff -r 3caee0cd91d8 -r e1659c30f48d src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Sat Oct 11 03:54:34 2008 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Mon Oct 13 06:54:25 2008 +0200
@@ -12,7 +12,7 @@
 (* Christian Urban.                                       *)
 
 theory SOS
-  imports "../Nominal"
+  imports "Nominal"
 begin
 
 atom_decl name
@@ -43,8 +43,6 @@
 
 lemma lookup_eqvt[eqvt]:
   fixes pi::"name prm"
-  and   \<theta>::"(name\<times>trm) list"
-  and   X::"name"
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
 by (induct \<theta>) (auto simp add: eqvts)
 
@@ -63,6 +61,7 @@
    (auto simp add: fresh_list_cons fresh_prod fresh_atm)
 
 (* parallel substitution *)
+
 consts
   psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [95,95] 105)
  
@@ -111,20 +110,9 @@
 
 lemma fresh_subst:
   fixes z::"name"
-  and   t\<^isub>1::"trm"
-  and   t2::"trm"
-  assumes a: "z\<sharp>t\<^isub>1" "z\<sharp>t\<^isub>2"
-  shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
-using a
-by (nominal_induct t\<^isub>1 avoiding: z y t\<^isub>2 rule: trm.strong_induct)
-   (auto simp add: abs_fresh fresh_atm)
-
-lemma fresh_subst':
-  assumes "x\<sharp>e'"
-  shows "x\<sharp>e[x::=e']"
-  using assms 
-by (nominal_induct e avoiding: x e' rule: trm.strong_induct)
-   (auto simp add: fresh_atm abs_fresh fresh_nat) 
+  shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
+by (nominal_induct t avoiding: z y s rule: trm.strong_induct)
+   (auto simp add: abs_fresh fresh_prod fresh_atm)
 
 lemma forget: 
   assumes a: "x\<sharp>e" 
@@ -151,37 +139,26 @@
 equivariance valid 
 
 inductive_cases
-  valid_cons_inv_auto[elim]: "valid ((x,T)#\<Gamma>)"
+  valid_elim[elim]: "valid ((x,T)#\<Gamma>)"
 
-lemma type_unicity_in_context:
-  assumes asm1: "(x,t\<^isub>2) \<in> set ((x,t\<^isub>1)#\<Gamma>)" 
-  and     asm2: "valid ((x,t\<^isub>1)#\<Gamma>)"
-  shows "t\<^isub>1=t\<^isub>2"
-proof -
-  from asm2 have "x\<sharp>\<Gamma>" by (cases, auto)
-  then have "(x,t\<^isub>2) \<notin> set \<Gamma>"
-    by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm)
-  then have "(x,t\<^isub>2) = (x,t\<^isub>1)" using asm1 by auto
-  then show "t\<^isub>1 = t\<^isub>2" by auto
-qed
+lemma valid_insert:
+  assumes a: "valid (\<Delta>@[(x,T)]@\<Gamma>)"
+  shows "valid (\<Delta> @ \<Gamma>)" 
+using a
+by (induct \<Delta>)
+   (auto simp add:  fresh_list_append fresh_list_cons elim!: valid_elim)
 
-lemma case_distinction_on_context:
-  fixes \<Gamma>::"(name\<times>ty) list"
-  assumes asm1: "valid ((m,t)#\<Gamma>)" 
-  and     asm2: "(n,U) \<in> set ((m,T)#\<Gamma>)"
-  shows "(n,U) = (m,T) \<or> ((n,U) \<in> set \<Gamma> \<and> n \<noteq> m)"
-proof -
-  from asm2 have "(n,U) \<in> set [(m,T)] \<or> (n,U) \<in> set \<Gamma>" by auto
-  moreover
-  { assume eq: "m=n"
-    assume "(n,U) \<in> set \<Gamma>" 
-    then have "\<not> n\<sharp>\<Gamma>" 
-      by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm)
-    moreover have "m\<sharp>\<Gamma>" using asm1 by auto
-    ultimately have False using eq by auto
-  }
-  ultimately show ?thesis by auto
-qed
+lemma fresh_set: 
+  shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)"
+by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)
+
+lemma context_unique:
+  assumes a1: "valid \<Gamma>"
+  and     a2: "(x,T) \<in> set \<Gamma>"
+  and     a3: "(x,U) \<in> set \<Gamma>"
+  shows "T = U" 
+using a1 a2 a3
+by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)
 
 text {* Typing Relation *}
 
@@ -200,8 +177,14 @@
 lemma typing_implies_valid:
   assumes a: "\<Gamma> \<turnstile> t : T"
   shows "valid \<Gamma>"
-  using a
-  by (induct) (auto)
+using a by (induct) (auto)
+
+
+lemma t_App_elim:
+  assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
+  obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" and "\<Gamma> \<turnstile> t2 : T'"
+using a
+by (cases) (auto simp add: trm.inject)
 
 lemma t_Lam_elim: 
   assumes a: "\<Gamma> \<turnstile> Lam [x].t : T" "x\<sharp>\<Gamma>"
@@ -233,82 +216,35 @@
   with vc show "\<Gamma>\<^isub>2 \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
 qed (auto)
 
-lemma context_exchange:
-  assumes a: "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<turnstile> e : T"
-  shows "(x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma> \<turnstile> e : T"
-proof -
-  from  a have "valid ((x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma>)" by (simp add: typing_implies_valid)
-  then have "x\<^isub>1\<noteq>x\<^isub>2" "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" "valid \<Gamma>"
-    by (auto simp: fresh_list_cons fresh_atm[symmetric])
-  then have "valid ((x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>)"
-    by (auto simp: fresh_list_cons fresh_atm fresh_ty)
-  moreover 
-  have "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<subseteq> (x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>" by auto
-  ultimately show "(x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma> \<turnstile> e : T" using a by (auto intro: weakening)
-qed
+lemma type_substitutivity_aux:
+  assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T"
+  and     b: "\<Gamma> \<turnstile> e' : T'"
+  shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
+using a b 
+proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: e' \<Delta> rule: typing.strong_induct)
+  case (t_Var \<Gamma>' y T e' \<Delta>)
+  then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
+       and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
+       and  a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
+  from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
+  { assume eq: "x=y"
+    from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
+    with a3 have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
+  }
+  moreover
+  { assume ineq: "x\<noteq>y"
+    from a2 have "(y,T) \<in> set (\<Delta>@\<Gamma>)" using ineq by simp
+    then have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto
+  }
+  ultimately show "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
+qed (force simp add: fresh_list_append fresh_list_cons)+
 
-lemma typing_var_unicity: 
-  assumes a: "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x : T\<^isub>2"
-  shows "T\<^isub>1=T\<^isub>2"
-proof - 
-  have "(x,T\<^isub>2) \<in> set ((x,T\<^isub>1)#\<Gamma>)" using a
-    by (cases) (auto simp add: trm.inject)
-  moreover 
-  have "valid ((x,T\<^isub>1)#\<Gamma>)" using a by (simp add: typing_implies_valid)
-  ultimately show "T\<^isub>1=T\<^isub>2" by (simp only: type_unicity_in_context)
-qed
-
-lemma typing_substitution: 
-  fixes \<Gamma>::"(name \<times> ty) list"
-  assumes "(x,T')#\<Gamma> \<turnstile> e : T" 
-  and     "\<Gamma> \<turnstile> e': T'" 
+corollary type_substitutivity:
+  assumes a: "(x,T')#\<Gamma> \<turnstile> e : T"
+  and     b: "\<Gamma> \<turnstile> e' : T'"
   shows "\<Gamma> \<turnstile> e[x::=e'] : T"
-  using assms
-proof (nominal_induct e avoiding: \<Gamma> e' x arbitrary: T rule: trm.strong_induct)
-  case (Var y \<Gamma> e' x T)
-  have h1: "(x,T')#\<Gamma> \<turnstile> Var y : T" by fact
-  have h2: "\<Gamma> \<turnstile> e' : T'" by fact
-  show "\<Gamma> \<turnstile> (Var y)[x::=e'] : T"
-  proof (cases "x=y")
-    case True
-    assume as: "x=y"
-    then have "T=T'" using h1 typing_var_unicity by auto
-    then show "\<Gamma> \<turnstile> (Var y)[x::=e'] : T" using as h2 by simp
-  next
-    case False
-    assume as: "x\<noteq>y" 
-    have "(y,T) \<in> set ((x,T')#\<Gamma>)" using h1 by (cases) (auto simp add: trm.inject)
-    then have "(y,T) \<in> set \<Gamma>" using as by auto
-    moreover 
-    have "valid \<Gamma>" using h2 by (simp only: typing_implies_valid)
-    ultimately show "\<Gamma> \<turnstile> (Var y)[x::=e'] : T" using as by (simp add: t_Var)
-  qed
-next
-  case (Lam y t \<Gamma> e' x T)
-  have vc: "y\<sharp>\<Gamma>" "y\<sharp>x" "y\<sharp>e'" by fact
-  have pr1: "\<Gamma> \<turnstile> e' : T'" by fact
-  have pr2: "(x,T')#\<Gamma> \<turnstile> Lam [y].t : T" by fact
-  then obtain T\<^isub>1 T\<^isub>2 where pr2': "(y,T\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t : T\<^isub>2" and eq: "T = T\<^isub>1\<rightarrow>T\<^isub>2" 
-    using vc by (auto elim: t_Lam_elim simp add: fresh_list_cons fresh_ty)
-  then have pr2'':"(x,T')#(y,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" by (simp add: context_exchange)
-  have ih: "\<lbrakk>(x,T')#(y,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2; (y,T\<^isub>1)#\<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> (y,T\<^isub>1)#\<Gamma> \<turnstile> t[x::=e'] : T\<^isub>2" by fact
-  have "valid \<Gamma>" using pr1 by (simp add: typing_implies_valid)
-  then have "valid ((y,T\<^isub>1)#\<Gamma>)" using vc by auto
-  then have "(y,T\<^isub>1)#\<Gamma> \<turnstile> e' : T'" using pr1 by (simp add: weakening)
-  then have "(y,T\<^isub>1)#\<Gamma> \<turnstile> t[x::=e'] : T\<^isub>2" using ih pr2'' by simp
-  then have "\<Gamma> \<turnstile> Lam [y].(t[x::=e']) : T\<^isub>1\<rightarrow>T\<^isub>2" using vc by auto
-  then show "\<Gamma> \<turnstile> (Lam [y].t)[x::=e'] : T" using vc eq by simp
-next
-  case (App e1 e2 \<Gamma> e' x T)
-  have "(x,T')#\<Gamma> \<turnstile> App e1 e2 : T" by fact
-  then obtain Tn where a1: "(x,T')#\<Gamma> \<turnstile> e1 : Tn \<rightarrow> T"
-                   and a2: "(x,T')#\<Gamma> \<turnstile> e2 : Tn"
-    by (cases) (auto simp add: trm.inject)
-  have a3: "\<Gamma> \<turnstile> e' : T'" by fact
-  have ih1: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> e1 : Tn\<rightarrow>T; \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e1[x::=e'] : Tn\<rightarrow>T" by fact
-  have ih2: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> e2 : Tn; \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> e2[x::=e'] : Tn" by fact
-  then show "\<Gamma> \<turnstile> (App e1 e2)[x::=e'] : T" using a1 a2 a3 ih1 ih2 by auto 
-qed
+using a b type_substitutivity_aux[where \<Delta>="[]"]
+by (auto)
 
 text {* Values *}
 inductive
@@ -368,9 +304,16 @@
     by (auto elim: t_Lam_elim simp add: ty.inject)
   moreover
   have "\<Gamma> \<turnstile> e\<^isub>2': T'" using ih2 a2 by simp
-  ultimately have "\<Gamma> \<turnstile> e[x::=e\<^isub>2'] : T" by (simp add: typing_substitution)
+  ultimately have "\<Gamma> \<turnstile> e[x::=e\<^isub>2'] : T" by (simp add: type_substitutivity)
   thus "\<Gamma> \<turnstile> e' : T" using ih3 by simp
-qed (blast)+
+qed (blast)
+
+lemma subject_reduction2:
+  assumes a: "e \<Down> e'" and b: "\<Gamma> \<turnstile> e : T"
+  shows "\<Gamma> \<turnstile> e' : T"
+  using a b
+by (nominal_induct avoiding: \<Gamma> T rule: big.strong_induct)
+   (force elim: t_App_elim t_Lam_elim simp add: ty.inject type_substitutivity)+
 
 lemma unicity_of_evaluation:
   assumes a: "e \<Down> e\<^isub>1" 
@@ -390,8 +333,7 @@
   have vc: "x\<sharp>e\<^isub>1" "x\<sharp>e\<^isub>2" "x\<sharp>t\<^isub>2" by fact
   then have "x\<sharp>App e\<^isub>1 e\<^isub>2" by auto
   from app vc obtain f\<^isub>1 f\<^isub>2 where x1: "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" and x2: "e\<^isub>2 \<Down> f\<^isub>2" and x3: "f\<^isub>1[x::=f\<^isub>2] \<Down> t\<^isub>2"
-    by (cases rule: big.strong_cases[where x="x" and xa="x"])
-       (auto simp add: trm.inject)
+    by (auto elim!: b_App_elim)
   then have "Lam [x]. f\<^isub>1 = Lam [x]. e\<^isub>1'" using ih1 by simp
   then 
   have "f\<^isub>1 = e\<^isub>1'" by (auto simp add: trm.inject alpha) 
@@ -402,9 +344,9 @@
 qed
 
 lemma reduces_evaluates_to_values:
-  assumes h:"t \<Down> t'"
+  assumes h: "t \<Down> t'"
   shows "val t'"
-  using h by (induct) (auto)
+using h by (induct) (auto)
 
 (* Valuation *)
 consts
@@ -415,7 +357,6 @@
   "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}"
   by (rule TrueI)+ 
 
-(* can go with strong inversion rules *)
 lemma V_eqvt:
   fixes pi::"name prm"
   assumes a: "x\<in>V T"
@@ -439,13 +380,13 @@
 
 lemma V_arrow_elim_weak:
   assumes h:"u \<in> V (T\<^isub>1 \<rightarrow> T\<^isub>2)"
-  obtains a t where "u = Lam[a].t" and "\<forall> v \<in> (V T\<^isub>1). \<exists> v'. t[a::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2"
+  obtains a t where "u = Lam [a].t" and "\<forall> v \<in> (V T\<^isub>1). \<exists> v'. t[a::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2"
 using h by (auto)
 
 lemma V_arrow_elim_strong:
   fixes c::"'a::fs_name"
   assumes h: "u \<in> V (T\<^isub>1 \<rightarrow> T\<^isub>2)"
-  obtains a t where "a\<sharp>c" "u = Lam[a].t" "\<forall>v \<in> (V T\<^isub>1). \<exists> v'. t[a::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2"
+  obtains a t where "a\<sharp>c" "u = Lam [a].t" "\<forall>v \<in> (V T\<^isub>1). \<exists> v'. t[a::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2"
 using h
 apply -
 apply(erule V_arrow_elim_weak)
@@ -500,6 +441,24 @@
 where
   "\<theta> Vcloses \<Gamma> \<equiv> \<forall>x T. (x,T) \<in> set \<Gamma> \<longrightarrow> (\<exists>v. \<theta> maps x to v \<and> v \<in> V T)"
 
+lemma case_distinction_on_context:
+  fixes \<Gamma>::"(name\<times>ty) list"
+  assumes asm1: "valid ((m,t)#\<Gamma>)" 
+  and     asm2: "(n,U) \<in> set ((m,T)#\<Gamma>)"
+  shows "(n,U) = (m,T) \<or> ((n,U) \<in> set \<Gamma> \<and> n \<noteq> m)"
+proof -
+  from asm2 have "(n,U) \<in> set [(m,T)] \<or> (n,U) \<in> set \<Gamma>" by auto
+  moreover
+  { assume eq: "m=n"
+    assume "(n,U) \<in> set \<Gamma>" 
+    then have "\<not> n\<sharp>\<Gamma>" 
+      by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm)
+    moreover have "m\<sharp>\<Gamma>" using asm1 by auto
+    ultimately have False using eq by auto
+  }
+  ultimately show ?thesis by auto
+qed
+
 lemma monotonicity:
   fixes m::"name"
   fixes \<theta>::"(name \<times> trm) list" 
@@ -533,23 +492,22 @@
 using h2 h1
 proof(nominal_induct e avoiding: \<Gamma> \<theta> arbitrary: T rule: trm.strong_induct)
   case (App e\<^isub>1 e\<^isub>2 \<Gamma> \<theta> T)
-  have ih\<^isub>1:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>1> \<Down> v \<and> v \<in> V T" by fact
-  have ih\<^isub>2:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>2> \<Down> v \<and> v \<in> V T" by fact
-  have as\<^isub>1:"\<theta> Vcloses \<Gamma>" by fact 
+  have ih\<^isub>1: "\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>1> \<Down> v \<and> v \<in> V T" by fact
+  have ih\<^isub>2: "\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>2> \<Down> v \<and> v \<in> V T" by fact
+  have as\<^isub>1: "\<theta> Vcloses \<Gamma>" by fact 
   have as\<^isub>2: "\<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T" by fact
-  then obtain T' where "\<Gamma> \<turnstile> e\<^isub>1 : T' \<rightarrow> T" and "\<Gamma> \<turnstile> e\<^isub>2 : T'" 
-    by (cases) (auto simp add: trm.inject)
+  then obtain T' where "\<Gamma> \<turnstile> e\<^isub>1 : T' \<rightarrow> T" and "\<Gamma> \<turnstile> e\<^isub>2 : T'" by (auto elim: t_App_elim)
   then obtain v\<^isub>1 v\<^isub>2 where "(i)": "\<theta><e\<^isub>1> \<Down> v\<^isub>1" "v\<^isub>1 \<in> V (T' \<rightarrow> T)"
-                      and "(ii)":"\<theta><e\<^isub>2> \<Down> v\<^isub>2" "v\<^isub>2 \<in> V T'" using ih\<^isub>1 ih\<^isub>2 as\<^isub>1 by blast
+                      and "(ii)": "\<theta><e\<^isub>2> \<Down> v\<^isub>2" "v\<^isub>2 \<in> V T'" using ih\<^isub>1 ih\<^isub>2 as\<^isub>1 by blast
   from "(i)" obtain x e' 
-            where "v\<^isub>1 = Lam[x].e'" 
+            where "v\<^isub>1 = Lam [x].e'" 
             and "(iii)": "(\<forall>v \<in> (V T').\<exists> v'. e'[x::=v] \<Down> v' \<and> v' \<in> V T)"
             and "(iv)":  "\<theta><e\<^isub>1> \<Down> Lam [x].e'" 
             and fr: "x\<sharp>(\<theta>,e\<^isub>1,e\<^isub>2)" by (blast elim: V_arrow_elim_strong)
   from fr have fr\<^isub>1: "x\<sharp>\<theta><e\<^isub>1>" and fr\<^isub>2: "x\<sharp>\<theta><e\<^isub>2>" by (simp_all add: fresh_psubst)
   from "(ii)" "(iii)" obtain v\<^isub>3 where "(v)": "e'[x::=v\<^isub>2] \<Down> v\<^isub>3" "v\<^isub>3 \<in> V T" by auto
   from fr\<^isub>2 "(ii)" have "x\<sharp>v\<^isub>2" by (simp add: big_preserves_fresh)
-  then have "x\<sharp>e'[x::=v\<^isub>2]" by (simp add: fresh_subst')
+  then have "x\<sharp>e'[x::=v\<^isub>2]" by (simp add: fresh_subst)
   then have fr\<^isub>3: "x\<sharp>v\<^isub>3" using "(v)" by (simp add: big_preserves_fresh)
   from fr\<^isub>1 fr\<^isub>2 fr\<^isub>3 have "x\<sharp>(\<theta><e\<^isub>1>,\<theta><e\<^isub>2>,v\<^isub>3)" by simp
   with "(iv)" "(ii)" "(v)" have "App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>) \<Down> v\<^isub>3" by auto
@@ -562,8 +520,7 @@
   have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact
   from as\<^isub>2 fs obtain T\<^isub>1 T\<^isub>2 
     where "(i)": "(x,T\<^isub>1)#\<Gamma> \<turnstile> e:T\<^isub>2" and "(ii)": "T = T\<^isub>1 \<rightarrow> T\<^isub>2" using fs
-    by (cases rule: typing.strong_cases[where x="x"])
-       (auto simp add: trm.inject alpha abs_fresh fresh_ty)
+    by (auto elim: t_Lam_elim)
   from "(i)" have "(iii)": "valid ((x,T\<^isub>1)#\<Gamma>)" by (simp add: typing_implies_valid)
   have "\<forall>v \<in> (V T\<^isub>1). \<exists>v'. (\<theta><e>)[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2"
   proof
@@ -575,7 +532,7 @@
     then show "\<exists>v'. \<theta><e>[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2" by auto
   qed
   then have "Lam[x].\<theta><e> \<in> V (T\<^isub>1 \<rightarrow> T\<^isub>2)" by auto
-  then have "\<theta><Lam [x].e> \<Down> Lam[x].\<theta><e> \<and> Lam[x].\<theta><e> \<in> V (T\<^isub>1\<rightarrow>T\<^isub>2)" using fs by auto
+  then have "\<theta><Lam [x].e> \<Down> Lam [x].\<theta><e> \<and> Lam [x].\<theta><e> \<in> V (T\<^isub>1\<rightarrow>T\<^isub>2)" using fs by auto
   thus "\<exists>v. \<theta><Lam [x].e> \<Down> v \<and> v \<in> V T" using "(ii)" by auto
 next
   case (Var x \<Gamma> \<theta> T)