src/HOL/Nominal/Examples/SN.thy
changeset 18378 35fba71ec6ef
parent 18348 b5d7649f8aca
child 18382 44578c918349
     1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Fri Dec 09 09:06:45 2005 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Fri Dec 09 12:38:49 2005 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  
     1.5  section {* Beta Reduction *}
     1.6  
     1.7 -
     1.8  lemma subst_rename[rule_format]: 
     1.9    shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
    1.10  apply(nominal_induct t1 avoiding: a c t2 rule: lam_induct)
    1.11 @@ -129,10 +128,13 @@
    1.12    thus ?thesis by simp
    1.13  qed
    1.14  
    1.15 -lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)"
    1.16 -apply(erule Beta.induct)
    1.17 -apply(auto intro!: simp add: abs_supp lam.supp subst_supp)
    1.18 -done
    1.19 +lemma supp_beta: 
    1.20 +  assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
    1.21 +  shows "(supp s)\<subseteq>((supp t)::name set)"
    1.22 +using a
    1.23 +by (induct)
    1.24 +   (auto intro!: simp add: abs_supp lam.supp subst_supp)
    1.25 +
    1.26  
    1.27  lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
    1.28  apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
    1.29 @@ -221,8 +223,10 @@
    1.30  lemma fresh_context[rule_format]: 
    1.31    fixes  \<Gamma> :: "(name\<times>ty)list"
    1.32    and    a :: "name"
    1.33 -  shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
    1.34 -apply(induct_tac \<Gamma>)
    1.35 +  assumes a: "a\<sharp>\<Gamma>"
    1.36 +  shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
    1.37 +using a
    1.38 +apply(induct \<Gamma>)
    1.39  apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
    1.40  done
    1.41  
    1.42 @@ -236,8 +240,12 @@
    1.43  done
    1.44  
    1.45  lemma valid_unicity[rule_format]: 
    1.46 -  shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>" 
    1.47 -apply(induct_tac \<Gamma>)
    1.48 +  assumes a: "valid \<Gamma>"
    1.49 +  and     b: "(c,\<sigma>)\<in>set \<Gamma>"
    1.50 +  and     c: "(c,\<tau>)\<in>set \<Gamma>"
    1.51 +  shows "\<sigma>=\<tau>" 
    1.52 +using a b c
    1.53 +apply(induct \<Gamma>)
    1.54  apply(auto dest!: valid_elim fresh_context)
    1.55  done
    1.56  
    1.57 @@ -351,8 +359,11 @@
    1.58  apply(auto)
    1.59  done
    1.60  
    1.61 -lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))"
    1.62 -apply(induct_tac \<Gamma>)
    1.63 +lemma in_ctxt: 
    1.64 +  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
    1.65 +  shows "a\<in>set(dom_ty \<Gamma>)"
    1.66 +using a
    1.67 +apply(induct \<Gamma>)
    1.68  apply(auto)
    1.69  done
    1.70  
    1.71 @@ -390,134 +401,124 @@
    1.72    shows "valid \<Gamma>"
    1.73  using a by (induct, auto dest!: valid_elim)
    1.74  
    1.75 -lemma ty_subs[rule_format]:
    1.76 -  fixes \<Gamma> ::"(name\<times>ty) list"
    1.77 -  and   t1 ::"lam"
    1.78 -  and   t2 ::"lam"
    1.79 -  and   \<tau>  ::"ty"
    1.80 -  and   \<sigma>  ::"ty" 
    1.81 -  and   c  ::"name"
    1.82 -  shows  "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
    1.83 +lemma ty_subs:
    1.84 +  assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
    1.85 +  and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
    1.86 +  shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
    1.87 +using a b
    1.88  proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam_induct)
    1.89    case (Var a) 
    1.90 -  show ?case
    1.91 -  proof(intro strip)
    1.92 -    assume a1: "\<Gamma> \<turnstile>t2:\<sigma>"
    1.93 -    assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>"
    1.94 -    hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
    1.95 -    from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
    1.96 -    from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
    1.97 -    show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
    1.98 -    proof (cases "a=c", simp_all)
    1.99 -      assume case1: "a=c"
   1.100 -      show "\<Gamma> \<turnstile> t2:\<tau>" using a1
   1.101 -      proof (cases "\<sigma>=\<tau>")
   1.102 -	assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
   1.103 -      next
   1.104 -	assume a3: "\<sigma>\<noteq>\<tau>"
   1.105 -	show ?thesis
   1.106 -	proof (rule ccontr)
   1.107 -	  from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
   1.108 -	  with case1 a25 show False by force 
   1.109 -	qed
   1.110 +  have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
   1.111 +  have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
   1.112 +  hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
   1.113 +  from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
   1.114 +  from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
   1.115 +  show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
   1.116 +  proof (cases "a=c", simp_all)
   1.117 +    assume case1: "a=c"
   1.118 +    show "\<Gamma> \<turnstile> t2:\<tau>" using a1
   1.119 +    proof (cases "\<sigma>=\<tau>")
   1.120 +      assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
   1.121 +    next
   1.122 +      assume a3: "\<sigma>\<noteq>\<tau>"
   1.123 +      show ?thesis
   1.124 +      proof (rule ccontr)
   1.125 +	from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
   1.126 +	with case1 a25 show False by force 
   1.127        qed
   1.128 -    next
   1.129 -      assume case2: "a\<noteq>c"
   1.130 -      with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
   1.131 -      from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
   1.132      qed
   1.133 +  next
   1.134 +    assume case2: "a\<noteq>c"
   1.135 +    with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
   1.136 +    from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
   1.137    qed
   1.138  next
   1.139    case (App s1 s2)
   1.140 -  show ?case
   1.141 -  proof (intro strip, simp)
   1.142 -    assume b1: "\<Gamma> \<turnstile>t2:\<sigma>" 
   1.143 -    assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>"
   1.144 -    hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
   1.145 -    then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
   1.146 -    show "\<Gamma> \<turnstile>  App (s1[c::=t2]) (s2[c::=t2]) : \<tau>" 
   1.147 -      using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto)
   1.148 -  qed
   1.149 +  have b1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
   1.150 +  have b2: "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
   1.151 +  hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
   1.152 +  then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
   1.153 +  show "\<Gamma> \<turnstile>  (App s1 s2)[c::=t2] : \<tau>" 
   1.154 +    using b1 b3a b3b prems by (simp, rule_tac \<tau>="\<tau>'" in t2, auto)
   1.155  next
   1.156    case (Lam a s)
   1.157    have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
   1.158    hence f1: "a\<sharp>\<Gamma>" and f2: "a\<noteq>c" and f2': "c\<sharp>a" and f3: "a\<sharp>t2" and f4: "a\<sharp>((c,\<sigma>)#\<Gamma>)"
   1.159      by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
   1.160 -  show ?case using f2 f3
   1.161 -  proof(intro strip, simp)
   1.162 -    assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>"
   1.163 -    hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
   1.164 -    then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force
   1.165 -    from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
   1.166 -    hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
   1.167 -      by (auto dest: valid_elim simp add: fresh_list_cons) 
   1.168 -    from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
   1.169 -    proof -
   1.170 -      have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   1.171 -      have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
   1.172 -	by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
   1.173 -      from c12 c2 c3 show ?thesis by (force intro: weakening)
   1.174 -    qed
   1.175 -    assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
   1.176 -    have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
   1.177 -    proof -
   1.178 -      have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   1.179 -      have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
   1.180 -      with c8 c82 c83 show ?thesis by (force intro: weakening)
   1.181 -    qed
   1.182 -    show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>"
   1.183 -      using c11 Lam c14 c81 f1 by force
   1.184 +  have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
   1.185 +  hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
   1.186 +  then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force
   1.187 +  from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
   1.188 +  hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
   1.189 +    by (auto dest: valid_elim simp add: fresh_list_cons) 
   1.190 +  from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
   1.191 +  proof -
   1.192 +    have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   1.193 +    have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
   1.194 +      by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
   1.195 +    from c12 c2 c3 show ?thesis by (force intro: weakening)
   1.196    qed
   1.197 +  assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
   1.198 +  have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
   1.199 +  proof -
   1.200 +    have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   1.201 +    have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
   1.202 +    with c8 c82 c83 show ?thesis by (force intro: weakening)
   1.203 +  qed
   1.204 +  show "\<Gamma> \<turnstile> (Lam [a].s)[c::=t2] : \<tau>"
   1.205 +    using c11 prems c14 c81 f1 by force
   1.206  qed
   1.207  
   1.208 -lemma subject[rule_format]: 
   1.209 +lemma subject: 
   1.210    fixes \<Gamma>  ::"(name\<times>ty) list"
   1.211    and   t1 ::"lam"
   1.212    and   t2 ::"lam"
   1.213    and   \<tau>  ::"ty"
   1.214    assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   1.215 -  shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)"
   1.216 -using a
   1.217 -proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct, auto)
   1.218 +  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
   1.219 +  shows "\<Gamma> \<turnstile> t2:\<tau>"
   1.220 +using a b
   1.221 +proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
   1.222    case (b1 t s1 s2)
   1.223 -  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   1.224 -  assume "\<Gamma> \<turnstile> App s1 t : \<tau>" 
   1.225 -  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim)
   1.226 -  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force
   1.227 -  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force
   1.228 +  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   1.229 +  have "\<Gamma> \<turnstile> App s1 t : \<tau>" by fact 
   1.230 +  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>" by (rule t2_elim)
   1.231 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by blast
   1.232 +  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by blast
   1.233  next
   1.234    case (b2 t s1 s2)
   1.235 -  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
   1.236 -  assume "\<Gamma> \<turnstile> App t s1 : \<tau>" 
   1.237 -  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim)
   1.238 -  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force
   1.239 -  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force
   1.240 +  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
   1.241 +  have "\<Gamma> \<turnstile> App t s1 : \<tau>" by fact
   1.242 +  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>" by (rule t2_elim)
   1.243 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by blast
   1.244 +  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by blast
   1.245  next
   1.246    case (b3 a s1 s2)
   1.247 -  have f: "a\<sharp>\<Gamma>" and "a\<sharp>\<tau>" by fact+
   1.248 -  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   1.249 -  assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>"
   1.250 -  with f have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (force dest: t3_elim)
   1.251 -  then obtain \<tau>1 \<tau>2 where a1: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and a2: "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by force
   1.252 -  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force 
   1.253 +  have f: "a\<sharp>\<Gamma>" and "a\<sharp>\<tau>" by fact
   1.254 +  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   1.255 +  have "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" by fact
   1.256 +  with f have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (blast dest: t3_elim)
   1.257 +  then obtain \<tau>1 \<tau>2 where a1: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and a2: "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by blast
   1.258 +  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by blast
   1.259  next
   1.260    case (b4 a s1 s2)
   1.261    have f: "a\<sharp>\<Gamma>" by fact
   1.262 -  assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>"
   1.263 +  have "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" by fact
   1.264    hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim)
   1.265 -  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force
   1.266 -  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim)
   1.267 -  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (force intro: ty_subs)
   1.268 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by blast
   1.269 +  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (blast dest!: t3_elim)
   1.270 +  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (blast intro: ty_subs)
   1.271  qed
   1.272  
   1.273 -lemma subject[rule_format]: 
   1.274 +lemma subject_automatic: 
   1.275    fixes \<Gamma>  ::"(name\<times>ty) list"
   1.276    and   t1 ::"lam"
   1.277    and   t2 ::"lam"
   1.278    and   \<tau>  ::"ty"
   1.279    assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   1.280 -  shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>"
   1.281 -using a
   1.282 +  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
   1.283 +  shows "\<Gamma> \<turnstile> t2:\<tau>"
   1.284 +using a b
   1.285  apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
   1.286  apply(auto dest!: t2_elim t3_elim intro: ty_subs)
   1.287  done
   1.288 @@ -544,7 +545,6 @@
   1.289  apply(auto)
   1.290  done
   1.291  
   1.292 -
   1.293  section {* Candidates *}
   1.294  
   1.295  consts
   1.296 @@ -565,10 +565,11 @@
   1.297  translations 
   1.298    "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
   1.299  inductive FST
   1.300 -intros
   1.301 +  intros
   1.302  fst[intro!]:  "(App t s) \<guillemotright> t"
   1.303  
   1.304 -lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
   1.305 +lemma fst_elim[elim!]: 
   1.306 +  shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
   1.307  apply(ind_cases "App t s \<guillemotright> t'")
   1.308  apply(simp add: lam.inject)
   1.309  done
   1.310 @@ -826,8 +827,11 @@
   1.311  apply(force simp add: RED_props)
   1.312  done
   1.313  
   1.314 -lemma fresh_domain[rule_format]: "a\<sharp>\<theta>\<longrightarrow>a\<notin>set(domain \<theta>)"
   1.315 -apply(induct_tac \<theta>)
   1.316 +lemma fresh_domain: 
   1.317 +  assumes a: "a\<sharp>\<theta>"
   1.318 +  shows "a\<notin>set(domain \<theta>)"
   1.319 +using a
   1.320 +apply(induct \<theta>)
   1.321  apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
   1.322  done
   1.323