tuned
authorurbanc
Fri Dec 09 12:38:49 2005 +0100 (2005-12-09)
changeset 1837835fba71ec6ef
parent 18377 0e1d025d57b3
child 18379 87cb7e641ba5
tuned
src/HOL/Nominal/Examples/CR.thy
src/HOL/Nominal/Examples/SN.thy
     1.1 --- a/src/HOL/Nominal/Examples/CR.thy	Fri Dec 09 09:06:45 2005 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/CR.thy	Fri Dec 09 12:38:49 2005 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    thus "(Lam [c].t)[a::=t2] = Lam [c].t" using a b by simp
     1.5  qed
     1.6  
     1.7 -lemma forget: 
     1.8 +lemma forget_automatic: 
     1.9    assumes a: "a\<sharp>t1"
    1.10    shows "t1[a::=t2] = t1"
    1.11    using a
    1.12 @@ -36,10 +36,7 @@
    1.13       (auto simp add: abs_fresh fresh_atm)
    1.14  
    1.15  lemma fresh_fact: 
    1.16 -  fixes   b :: "name"
    1.17 -  and    a  :: "name"
    1.18 -  and    t1 :: "lam"
    1.19 -  and    t2 :: "lam"
    1.20 +  fixes a :: "name"
    1.21    assumes a: "a\<sharp>t1"
    1.22    and     b: "a\<sharp>t2"
    1.23    shows "a\<sharp>(t1[b::=t2])"
    1.24 @@ -61,7 +58,7 @@
    1.25    thus "a\<sharp>(Lam [c].t)[b::=t2]" using fr  by (simp add: abs_fresh)
    1.26  qed
    1.27  
    1.28 -lemma fresh_fact: 
    1.29 +lemma fresh_fact_automatic: 
    1.30    fixes a::"name"
    1.31    assumes a: "a\<sharp>t1"
    1.32    and     b: "a\<sharp>t2"
    1.33 @@ -130,12 +127,7 @@
    1.34    thus ?case by simp
    1.35  qed
    1.36  
    1.37 -lemma subs_lemma:  
    1.38 -  fixes x::"name"
    1.39 -  and   y::"name"
    1.40 -  and   L::"lam"
    1.41 -  and   M::"lam"
    1.42 -  and   N::"lam"
    1.43 +lemma subs_lemma_automatic:  
    1.44    assumes a: "x\<noteq>y"
    1.45    and     b: "x\<sharp>L"
    1.46    shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
    1.47 @@ -144,10 +136,6 @@
    1.48     (auto simp add: fresh_fact forget)
    1.49  
    1.50  lemma subst_rename: 
    1.51 -  fixes  c  :: "name"
    1.52 -  and    a  :: "name"
    1.53 -  and    t1 :: "lam"
    1.54 -  and    t2 :: "lam"
    1.55    assumes a: "c\<sharp>t1"
    1.56    shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
    1.57  using a
    1.58 @@ -174,11 +162,7 @@
    1.59    qed
    1.60  qed
    1.61  
    1.62 -lemma subst_rename: 
    1.63 -  fixes  c  :: "name"
    1.64 -  and    a  :: "name"
    1.65 -  and    t1 :: "lam"
    1.66 -  and    t2 :: "lam"
    1.67 +lemma subst_rename_automatic: 
    1.68    assumes a: "c\<sharp>t1"
    1.69    shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
    1.70  using a
    1.71 @@ -382,9 +366,7 @@
    1.72  qed
    1.73  
    1.74  lemma one_fresh_preserv:
    1.75 -  fixes    t :: "lam"
    1.76 -  and      s :: "lam"
    1.77 -  and      a :: "name"
    1.78 +  fixes a :: "name"
    1.79    assumes a: "t\<longrightarrow>\<^isub>1s"
    1.80    and     b: "a\<sharp>t"
    1.81    shows "a\<sharp>s"
    1.82 @@ -488,10 +470,6 @@
    1.83  text {* first case in Lemma 3.2.4*}
    1.84  
    1.85  lemma one_subst_aux:
    1.86 -  fixes    M :: "lam"
    1.87 -  and      N :: "lam"
    1.88 -  and      N':: "lam"
    1.89 -  and      x :: "name"
    1.90    assumes a: "N\<longrightarrow>\<^isub>1N'"
    1.91    shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
    1.92  using a
    1.93 @@ -506,11 +484,7 @@
    1.94    thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 by simp
    1.95  qed
    1.96  
    1.97 -lemma one_subst_aux:
    1.98 -  fixes    M :: "lam"
    1.99 -  and      N :: "lam"
   1.100 -  and      N':: "lam"
   1.101 -  and      x :: "name"
   1.102 +lemma one_subst_aux_automatic:
   1.103    assumes a: "N\<longrightarrow>\<^isub>1N'"
   1.104    shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
   1.105  using a
   1.106 @@ -519,11 +493,6 @@
   1.107  done
   1.108  
   1.109  lemma one_subst: 
   1.110 -  fixes    M :: "lam"
   1.111 -  and      M':: "lam"
   1.112 -  and      N :: "lam"
   1.113 -  and      N':: "lam"
   1.114 -  and      x :: "name"
   1.115    assumes a: "M\<longrightarrow>\<^isub>1M'"
   1.116    and     b: "N\<longrightarrow>\<^isub>1N'"
   1.117    shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
   1.118 @@ -551,7 +520,7 @@
   1.119    qed
   1.120  qed
   1.121  
   1.122 -lemma one_subst: 
   1.123 +lemma one_subst_automatic: 
   1.124    assumes a: "M\<longrightarrow>\<^isub>1M'" 
   1.125    and     b: "N\<longrightarrow>\<^isub>1N'"
   1.126    shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
   1.127 @@ -674,45 +643,45 @@
   1.128  qed
   1.129  
   1.130  lemma one_abs_cong: 
   1.131 -  fixes a :: "name"
   1.132    assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   1.133    shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)"
   1.134    using a
   1.135  proof induct
   1.136 -  case 1 thus ?case by force
   1.137 +  case 1 thus ?case by simp
   1.138  next
   1.139    case (2 y z) 
   1.140 -  thus ?case by (force dest: b3 intro: rtrancl_trans)
   1.141 +  thus ?case by (blast dest: b3 intro: rtrancl_trans)
   1.142  qed
   1.143  
   1.144 -lemma one_pr_congL: 
   1.145 +lemma one_app_congL: 
   1.146    assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   1.147    shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
   1.148    using a
   1.149  proof induct
   1.150 -  case 1 thus ?case by (force)
   1.151 +  case 1 thus ?case by simp
   1.152  next
   1.153 -  case 2 thus ?case by (force dest: b1 intro: rtrancl_trans)
   1.154 +  case 2 thus ?case by (blast dest: b1 intro: rtrancl_trans)
   1.155  qed
   1.156    
   1.157 -lemma one_pr_congR: 
   1.158 +lemma one_app_congR: 
   1.159    assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   1.160    shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
   1.161  using a
   1.162  proof induct
   1.163 -  case 1 thus ?case by (force)
   1.164 +  case 1 thus ?case by simp
   1.165  next 
   1.166 -  case 2 thus ?case by (force dest: b2 intro: rtrancl_trans)
   1.167 +  case 2 thus ?case by (blast dest: b2 intro: rtrancl_trans)
   1.168  qed
   1.169  
   1.170 -lemma one_pr_cong: 
   1.171 +lemma one_app_cong: 
   1.172    assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   1.173    and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" 
   1.174    shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
   1.175  proof -
   1.176 -  have b1: "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_pr_congL)
   1.177 -  have b2: "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_pr_congR)
   1.178 -  show ?thesis using b1 b2 by (force intro: rtrancl_trans)
   1.179 +  have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL)
   1.180 +  moreover
   1.181 +  have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR)
   1.182 +  ultimately show ?thesis by (blast intro: rtrancl_trans)
   1.183  qed
   1.184  
   1.185  lemma one_beta_star: 
   1.186 @@ -720,29 +689,28 @@
   1.187    shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"
   1.188    using a
   1.189  proof induct
   1.190 -  case o1 thus ?case by (force)
   1.191 +  case o1 thus ?case by simp
   1.192  next
   1.193 -  case o2 thus ?case by (force intro!: one_pr_cong)
   1.194 +  case o2 thus ?case by (blast intro!: one_app_cong)
   1.195  next
   1.196 -  case o3 thus ?case by (force intro!: one_abs_cong)
   1.197 +  case o3 thus ?case by (blast intro!: one_abs_cong)
   1.198  next 
   1.199    case (o4 a s1 s2 t1 t2)
   1.200 -  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" .
   1.201 +  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact
   1.202    have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" by (rule b4)
   1.203    from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 
   1.204 -    by (force intro!: one_pr_cong one_abs_cong)
   1.205 -  show ?case using c1 c2 by (force intro: rtrancl_trans)
   1.206 +    by (blast intro!: one_app_cong one_abs_cong)
   1.207 +  show ?case using c1 c2 by (blast intro: rtrancl_trans)
   1.208  qed
   1.209   
   1.210  lemma one_star_abs_cong: 
   1.211 -  fixes a :: "name"
   1.212    assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
   1.213    shows "(Lam  [a].t1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [a].t2)"
   1.214    using a
   1.215  proof induct
   1.216 -  case 1 thus ?case by (force)
   1.217 +  case 1 thus ?case by simp
   1.218  next
   1.219 -  case 2 thus ?case by (force intro: rtrancl_trans)
   1.220 +  case 2 thus ?case by (blast intro: rtrancl_trans)
   1.221  qed
   1.222  
   1.223  lemma one_star_pr_congL: 
   1.224 @@ -750,9 +718,9 @@
   1.225    shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
   1.226    using a
   1.227  proof induct
   1.228 -  case 1 thus ?case by (force)
   1.229 +  case 1 thus ?case by simp
   1.230  next
   1.231 -  case 2 thus ?case by (force intro: rtrancl_trans)
   1.232 +  case 2 thus ?case by (blast intro: rtrancl_trans)
   1.233  qed
   1.234  
   1.235  lemma one_star_pr_congR: 
   1.236 @@ -760,9 +728,9 @@
   1.237    shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
   1.238    using a
   1.239  proof induct
   1.240 -  case 1 thus ?case by (force)
   1.241 +  case 1 thus ?case by simp
   1.242  next
   1.243 -  case 2 thus ?case by (force intro: rtrancl_trans)
   1.244 +  case 2 thus ?case by (blast intro: rtrancl_trans)
   1.245  qed
   1.246  
   1.247  lemma beta_one_star: 
   1.248 @@ -770,13 +738,13 @@
   1.249    shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
   1.250    using a
   1.251  proof induct
   1.252 -  case b1 thus ?case by (force intro!: one_star_pr_congL)
   1.253 +  case b1 thus ?case by (blast intro!: one_star_pr_congL)
   1.254  next
   1.255 -  case b2 thus ?case by (force intro!: one_star_pr_congR)
   1.256 +  case b2 thus ?case by (blast intro!: one_star_pr_congR)
   1.257  next
   1.258 -  case b3 thus ?case by (force intro!: one_star_abs_cong)
   1.259 +  case b3 thus ?case by (blast intro!: one_star_abs_cong)
   1.260  next
   1.261 -  case b4 thus ?case by (force)
   1.262 +  case b4 thus ?case by blast
   1.263  qed
   1.264  
   1.265  lemma trans_closure: 
   1.266 @@ -785,7 +753,7 @@
   1.267    assume "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
   1.268    thus "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
   1.269    proof induct
   1.270 -    case 1 thus ?case by (force)
   1.271 +    case 1 thus ?case by simp
   1.272    next
   1.273      case 2 thus ?case by (force intro: rtrancl_trans simp add: one_beta_star)
   1.274    qed
   1.275 @@ -793,7 +761,7 @@
   1.276    assume "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
   1.277    thus "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
   1.278    proof induct
   1.279 -    case 1 thus ?case by (force)
   1.280 +    case 1 thus ?case by simp
   1.281    next
   1.282      case 2 thus ?case by (force intro: rtrancl_trans simp add: beta_one_star)
   1.283    qed
   1.284 @@ -811,19 +779,19 @@
   1.285    have b: "s1 \<longrightarrow>\<^isub>1 s2" by fact
   1.286    have h: "\<And>t2. t \<longrightarrow>\<^isub>1 t2 \<Longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact
   1.287    have c: "t \<longrightarrow>\<^isub>1 t2" by fact
   1.288 -  show "(\<exists>t3.  s2 \<longrightarrow>\<^isub>1 t3 \<and>  t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" 
   1.289 +  show "\<exists>t3. s2 \<longrightarrow>\<^isub>1 t3 \<and>  t2 \<longrightarrow>\<^isub>1\<^sup>* t3" 
   1.290    proof -
   1.291 -    from c h have "(\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" by force
   1.292 -    then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (force)
   1.293 -    have "(\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4)" using b c1 by (force intro: diamond)
   1.294 -    thus ?thesis using c2 by (force intro: rtrancl_trans)
   1.295 +    from c h have "\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
   1.296 +    then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
   1.297 +    have "\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4" using b c1 by (blast intro: diamond)
   1.298 +    thus ?thesis using c2 by (blast intro: rtrancl_trans)
   1.299    qed
   1.300  qed
   1.301  
   1.302  lemma cr_one_star: 
   1.303    assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2"
   1.304        and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1"
   1.305 -    shows "(\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3)"
   1.306 +    shows "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3"
   1.307  using a
   1.308  proof induct
   1.309    case 1
   1.310 @@ -833,26 +801,27 @@
   1.311    assume d: "s1 \<longrightarrow>\<^isub>1 s2"
   1.312    assume "\<exists>t3.  t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and>  s1 \<longrightarrow>\<^isub>1\<^sup>* t3"
   1.313    then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
   1.314 -                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" by force
   1.315 -  from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by force
   1.316 +                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
   1.317 +  from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
   1.318    then obtain t4 where g1: "t3\<longrightarrow>\<^isub>1t4"
   1.319 -                   and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by force
   1.320 -  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (force intro: rtrancl_trans)
   1.321 -  thus ?case using g2 by (force)
   1.322 +                   and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
   1.323 +  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: rtrancl_trans)
   1.324 +  thus ?case using g2 by blast
   1.325  qed
   1.326    
   1.327  lemma cr_beta_star: 
   1.328    assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1" 
   1.329    and a2: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   1.330 -  shows "(\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3)"
   1.331 +  shows "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3"
   1.332  proof -
   1.333    from a1 have b1: "t\<longrightarrow>\<^isub>1\<^sup>*t1" by (simp add: trans_closure[symmetric])
   1.334    from a2 have b2: "t\<longrightarrow>\<^isub>1\<^sup>*t2" by (simp add: trans_closure[symmetric])
   1.335 -  from b1 and b2 have c: "\<exists>t3. (t1\<longrightarrow>\<^isub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3)" by (force intro!: cr_one_star) 
   1.336 -  from c obtain t3 where d1: "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and d2: "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by force
   1.337 -  from d1 have e1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp add: trans_closure)
   1.338 -  from d2 have e2: "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp add: trans_closure)
   1.339 -  show ?thesis using e1 and e2 by (force)
   1.340 +  from b1 and b2 have c: "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3" by (blast intro!: cr_one_star) 
   1.341 +  from c obtain t3 where d1: "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and d2: "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by blast
   1.342 +  have "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" using d1 by (simp add: trans_closure)
   1.343 +  moreover
   1.344 +  have "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" using d2 by (simp add: trans_closure)
   1.345 +  ultimately show ?thesis by blast
   1.346  qed
   1.347  
   1.348  end
     2.1 --- a/src/HOL/Nominal/Examples/SN.thy	Fri Dec 09 09:06:45 2005 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Fri Dec 09 12:38:49 2005 +0100
     2.3 @@ -8,7 +8,6 @@
     2.4  
     2.5  section {* Beta Reduction *}
     2.6  
     2.7 -
     2.8  lemma subst_rename[rule_format]: 
     2.9    shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
    2.10  apply(nominal_induct t1 avoiding: a c t2 rule: lam_induct)
    2.11 @@ -129,10 +128,13 @@
    2.12    thus ?thesis by simp
    2.13  qed
    2.14  
    2.15 -lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)"
    2.16 -apply(erule Beta.induct)
    2.17 -apply(auto intro!: simp add: abs_supp lam.supp subst_supp)
    2.18 -done
    2.19 +lemma supp_beta: 
    2.20 +  assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
    2.21 +  shows "(supp s)\<subseteq>((supp t)::name set)"
    2.22 +using a
    2.23 +by (induct)
    2.24 +   (auto intro!: simp add: abs_supp lam.supp subst_supp)
    2.25 +
    2.26  
    2.27  lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
    2.28  apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
    2.29 @@ -221,8 +223,10 @@
    2.30  lemma fresh_context[rule_format]: 
    2.31    fixes  \<Gamma> :: "(name\<times>ty)list"
    2.32    and    a :: "name"
    2.33 -  shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
    2.34 -apply(induct_tac \<Gamma>)
    2.35 +  assumes a: "a\<sharp>\<Gamma>"
    2.36 +  shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
    2.37 +using a
    2.38 +apply(induct \<Gamma>)
    2.39  apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
    2.40  done
    2.41  
    2.42 @@ -236,8 +240,12 @@
    2.43  done
    2.44  
    2.45  lemma valid_unicity[rule_format]: 
    2.46 -  shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>" 
    2.47 -apply(induct_tac \<Gamma>)
    2.48 +  assumes a: "valid \<Gamma>"
    2.49 +  and     b: "(c,\<sigma>)\<in>set \<Gamma>"
    2.50 +  and     c: "(c,\<tau>)\<in>set \<Gamma>"
    2.51 +  shows "\<sigma>=\<tau>" 
    2.52 +using a b c
    2.53 +apply(induct \<Gamma>)
    2.54  apply(auto dest!: valid_elim fresh_context)
    2.55  done
    2.56  
    2.57 @@ -351,8 +359,11 @@
    2.58  apply(auto)
    2.59  done
    2.60  
    2.61 -lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))"
    2.62 -apply(induct_tac \<Gamma>)
    2.63 +lemma in_ctxt: 
    2.64 +  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
    2.65 +  shows "a\<in>set(dom_ty \<Gamma>)"
    2.66 +using a
    2.67 +apply(induct \<Gamma>)
    2.68  apply(auto)
    2.69  done
    2.70  
    2.71 @@ -390,134 +401,124 @@
    2.72    shows "valid \<Gamma>"
    2.73  using a by (induct, auto dest!: valid_elim)
    2.74  
    2.75 -lemma ty_subs[rule_format]:
    2.76 -  fixes \<Gamma> ::"(name\<times>ty) list"
    2.77 -  and   t1 ::"lam"
    2.78 -  and   t2 ::"lam"
    2.79 -  and   \<tau>  ::"ty"
    2.80 -  and   \<sigma>  ::"ty" 
    2.81 -  and   c  ::"name"
    2.82 -  shows  "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
    2.83 +lemma ty_subs:
    2.84 +  assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
    2.85 +  and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
    2.86 +  shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
    2.87 +using a b
    2.88  proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam_induct)
    2.89    case (Var a) 
    2.90 -  show ?case
    2.91 -  proof(intro strip)
    2.92 -    assume a1: "\<Gamma> \<turnstile>t2:\<sigma>"
    2.93 -    assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>"
    2.94 -    hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
    2.95 -    from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
    2.96 -    from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
    2.97 -    show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
    2.98 -    proof (cases "a=c", simp_all)
    2.99 -      assume case1: "a=c"
   2.100 -      show "\<Gamma> \<turnstile> t2:\<tau>" using a1
   2.101 -      proof (cases "\<sigma>=\<tau>")
   2.102 -	assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
   2.103 -      next
   2.104 -	assume a3: "\<sigma>\<noteq>\<tau>"
   2.105 -	show ?thesis
   2.106 -	proof (rule ccontr)
   2.107 -	  from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
   2.108 -	  with case1 a25 show False by force 
   2.109 -	qed
   2.110 +  have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
   2.111 +  have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
   2.112 +  hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
   2.113 +  from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
   2.114 +  from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
   2.115 +  show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
   2.116 +  proof (cases "a=c", simp_all)
   2.117 +    assume case1: "a=c"
   2.118 +    show "\<Gamma> \<turnstile> t2:\<tau>" using a1
   2.119 +    proof (cases "\<sigma>=\<tau>")
   2.120 +      assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
   2.121 +    next
   2.122 +      assume a3: "\<sigma>\<noteq>\<tau>"
   2.123 +      show ?thesis
   2.124 +      proof (rule ccontr)
   2.125 +	from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
   2.126 +	with case1 a25 show False by force 
   2.127        qed
   2.128 -    next
   2.129 -      assume case2: "a\<noteq>c"
   2.130 -      with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
   2.131 -      from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
   2.132      qed
   2.133 +  next
   2.134 +    assume case2: "a\<noteq>c"
   2.135 +    with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
   2.136 +    from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
   2.137    qed
   2.138  next
   2.139    case (App s1 s2)
   2.140 -  show ?case
   2.141 -  proof (intro strip, simp)
   2.142 -    assume b1: "\<Gamma> \<turnstile>t2:\<sigma>" 
   2.143 -    assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>"
   2.144 -    hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
   2.145 -    then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
   2.146 -    show "\<Gamma> \<turnstile>  App (s1[c::=t2]) (s2[c::=t2]) : \<tau>" 
   2.147 -      using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto)
   2.148 -  qed
   2.149 +  have b1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
   2.150 +  have b2: "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
   2.151 +  hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
   2.152 +  then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
   2.153 +  show "\<Gamma> \<turnstile>  (App s1 s2)[c::=t2] : \<tau>" 
   2.154 +    using b1 b3a b3b prems by (simp, rule_tac \<tau>="\<tau>'" in t2, auto)
   2.155  next
   2.156    case (Lam a s)
   2.157    have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
   2.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>)"
   2.159      by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
   2.160 -  show ?case using f2 f3
   2.161 -  proof(intro strip, simp)
   2.162 -    assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>"
   2.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) 
   2.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
   2.165 -    from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
   2.166 -    hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
   2.167 -      by (auto dest: valid_elim simp add: fresh_list_cons) 
   2.168 -    from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
   2.169 -    proof -
   2.170 -      have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   2.171 -      have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
   2.172 -	by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
   2.173 -      from c12 c2 c3 show ?thesis by (force intro: weakening)
   2.174 -    qed
   2.175 -    assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
   2.176 -    have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
   2.177 -    proof -
   2.178 -      have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   2.179 -      have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
   2.180 -      with c8 c82 c83 show ?thesis by (force intro: weakening)
   2.181 -    qed
   2.182 -    show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>"
   2.183 -      using c11 Lam c14 c81 f1 by force
   2.184 +  have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
   2.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) 
   2.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
   2.187 +  from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
   2.188 +  hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
   2.189 +    by (auto dest: valid_elim simp add: fresh_list_cons) 
   2.190 +  from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
   2.191 +  proof -
   2.192 +    have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   2.193 +    have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
   2.194 +      by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
   2.195 +    from c12 c2 c3 show ?thesis by (force intro: weakening)
   2.196    qed
   2.197 +  assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
   2.198 +  have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
   2.199 +  proof -
   2.200 +    have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   2.201 +    have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
   2.202 +    with c8 c82 c83 show ?thesis by (force intro: weakening)
   2.203 +  qed
   2.204 +  show "\<Gamma> \<turnstile> (Lam [a].s)[c::=t2] : \<tau>"
   2.205 +    using c11 prems c14 c81 f1 by force
   2.206  qed
   2.207  
   2.208 -lemma subject[rule_format]: 
   2.209 +lemma subject: 
   2.210    fixes \<Gamma>  ::"(name\<times>ty) list"
   2.211    and   t1 ::"lam"
   2.212    and   t2 ::"lam"
   2.213    and   \<tau>  ::"ty"
   2.214    assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   2.215 -  shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)"
   2.216 -using a
   2.217 -proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct, auto)
   2.218 +  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
   2.219 +  shows "\<Gamma> \<turnstile> t2:\<tau>"
   2.220 +using a b
   2.221 +proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
   2.222    case (b1 t s1 s2)
   2.223 -  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   2.224 -  assume "\<Gamma> \<turnstile> App s1 t : \<tau>" 
   2.225 -  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim)
   2.226 -  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force
   2.227 -  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force
   2.228 +  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   2.229 +  have "\<Gamma> \<turnstile> App s1 t : \<tau>" by fact 
   2.230 +  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>" by (rule t2_elim)
   2.231 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by blast
   2.232 +  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by blast
   2.233  next
   2.234    case (b2 t s1 s2)
   2.235 -  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
   2.236 -  assume "\<Gamma> \<turnstile> App t s1 : \<tau>" 
   2.237 -  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim)
   2.238 -  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force
   2.239 -  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force
   2.240 +  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
   2.241 +  have "\<Gamma> \<turnstile> App t s1 : \<tau>" by fact
   2.242 +  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>" by (rule t2_elim)
   2.243 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by blast
   2.244 +  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by blast
   2.245  next
   2.246    case (b3 a s1 s2)
   2.247 -  have f: "a\<sharp>\<Gamma>" and "a\<sharp>\<tau>" by fact+
   2.248 -  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   2.249 -  assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>"
   2.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)
   2.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
   2.252 -  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force 
   2.253 +  have f: "a\<sharp>\<Gamma>" and "a\<sharp>\<tau>" by fact
   2.254 +  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   2.255 +  have "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" by fact
   2.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)
   2.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
   2.258 +  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by blast
   2.259  next
   2.260    case (b4 a s1 s2)
   2.261    have f: "a\<sharp>\<Gamma>" by fact
   2.262 -  assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>"
   2.263 +  have "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" by fact
   2.264    hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim)
   2.265 -  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force
   2.266 -  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim)
   2.267 -  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (force intro: ty_subs)
   2.268 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by blast
   2.269 +  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (blast dest!: t3_elim)
   2.270 +  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (blast intro: ty_subs)
   2.271  qed
   2.272  
   2.273 -lemma subject[rule_format]: 
   2.274 +lemma subject_automatic: 
   2.275    fixes \<Gamma>  ::"(name\<times>ty) list"
   2.276    and   t1 ::"lam"
   2.277    and   t2 ::"lam"
   2.278    and   \<tau>  ::"ty"
   2.279    assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   2.280 -  shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>"
   2.281 -using a
   2.282 +  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
   2.283 +  shows "\<Gamma> \<turnstile> t2:\<tau>"
   2.284 +using a b
   2.285  apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
   2.286  apply(auto dest!: t2_elim t3_elim intro: ty_subs)
   2.287  done
   2.288 @@ -544,7 +545,6 @@
   2.289  apply(auto)
   2.290  done
   2.291  
   2.292 -
   2.293  section {* Candidates *}
   2.294  
   2.295  consts
   2.296 @@ -565,10 +565,11 @@
   2.297  translations 
   2.298    "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
   2.299  inductive FST
   2.300 -intros
   2.301 +  intros
   2.302  fst[intro!]:  "(App t s) \<guillemotright> t"
   2.303  
   2.304 -lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
   2.305 +lemma fst_elim[elim!]: 
   2.306 +  shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
   2.307  apply(ind_cases "App t s \<guillemotright> t'")
   2.308  apply(simp add: lam.inject)
   2.309  done
   2.310 @@ -826,8 +827,11 @@
   2.311  apply(force simp add: RED_props)
   2.312  done
   2.313  
   2.314 -lemma fresh_domain[rule_format]: "a\<sharp>\<theta>\<longrightarrow>a\<notin>set(domain \<theta>)"
   2.315 -apply(induct_tac \<theta>)
   2.316 +lemma fresh_domain: 
   2.317 +  assumes a: "a\<sharp>\<theta>"
   2.318 +  shows "a\<notin>set(domain \<theta>)"
   2.319 +using a
   2.320 +apply(induct \<theta>)
   2.321  apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
   2.322  done
   2.323