# HG changeset patch
# User urbanc
# Date 1134128329 -3600
# Node ID 35fba71ec6ef550178e5f5e44d95d96c6f36eae6
# Parent  0e1d025d57b3a90ad1d37cf08d024e338268d8af
tuned

diff -r 0e1d025d57b3 -r 35fba71ec6ef src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Fri Dec 09 09:06:45 2005 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Fri Dec 09 12:38:49 2005 +0100
@@ -28,7 +28,7 @@
   thus "(Lam [c].t)[a::=t2] = Lam [c].t" using a b by simp
 qed
 
-lemma forget: 
+lemma forget_automatic: 
   assumes a: "a\<sharp>t1"
   shows "t1[a::=t2] = t1"
   using a
@@ -36,10 +36,7 @@
      (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
-  fixes   b :: "name"
-  and    a  :: "name"
-  and    t1 :: "lam"
-  and    t2 :: "lam"
+  fixes a :: "name"
   assumes a: "a\<sharp>t1"
   and     b: "a\<sharp>t2"
   shows "a\<sharp>(t1[b::=t2])"
@@ -61,7 +58,7 @@
   thus "a\<sharp>(Lam [c].t)[b::=t2]" using fr  by (simp add: abs_fresh)
 qed
 
-lemma fresh_fact: 
+lemma fresh_fact_automatic: 
   fixes a::"name"
   assumes a: "a\<sharp>t1"
   and     b: "a\<sharp>t2"
@@ -130,12 +127,7 @@
   thus ?case by simp
 qed
 
-lemma subs_lemma:  
-  fixes x::"name"
-  and   y::"name"
-  and   L::"lam"
-  and   M::"lam"
-  and   N::"lam"
+lemma subs_lemma_automatic:  
   assumes a: "x\<noteq>y"
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
@@ -144,10 +136,6 @@
    (auto simp add: fresh_fact forget)
 
 lemma subst_rename: 
-  fixes  c  :: "name"
-  and    a  :: "name"
-  and    t1 :: "lam"
-  and    t2 :: "lam"
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
@@ -174,11 +162,7 @@
   qed
 qed
 
-lemma subst_rename: 
-  fixes  c  :: "name"
-  and    a  :: "name"
-  and    t1 :: "lam"
-  and    t2 :: "lam"
+lemma subst_rename_automatic: 
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
@@ -382,9 +366,7 @@
 qed
 
 lemma one_fresh_preserv:
-  fixes    t :: "lam"
-  and      s :: "lam"
-  and      a :: "name"
+  fixes a :: "name"
   assumes a: "t\<longrightarrow>\<^isub>1s"
   and     b: "a\<sharp>t"
   shows "a\<sharp>s"
@@ -488,10 +470,6 @@
 text {* first case in Lemma 3.2.4*}
 
 lemma one_subst_aux:
-  fixes    M :: "lam"
-  and      N :: "lam"
-  and      N':: "lam"
-  and      x :: "name"
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
@@ -506,11 +484,7 @@
   thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 by simp
 qed
 
-lemma one_subst_aux:
-  fixes    M :: "lam"
-  and      N :: "lam"
-  and      N':: "lam"
-  and      x :: "name"
+lemma one_subst_aux_automatic:
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
@@ -519,11 +493,6 @@
 done
 
 lemma one_subst: 
-  fixes    M :: "lam"
-  and      M':: "lam"
-  and      N :: "lam"
-  and      N':: "lam"
-  and      x :: "name"
   assumes a: "M\<longrightarrow>\<^isub>1M'"
   and     b: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
@@ -551,7 +520,7 @@
   qed
 qed
 
-lemma one_subst: 
+lemma one_subst_automatic: 
   assumes a: "M\<longrightarrow>\<^isub>1M'" 
   and     b: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
@@ -674,45 +643,45 @@
 qed
 
 lemma one_abs_cong: 
-  fixes a :: "name"
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)"
   using a
 proof induct
-  case 1 thus ?case by force
+  case 1 thus ?case by simp
 next
   case (2 y z) 
-  thus ?case by (force dest: b3 intro: rtrancl_trans)
+  thus ?case by (blast dest: b3 intro: rtrancl_trans)
 qed
 
-lemma one_pr_congL: 
+lemma one_app_congL: 
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
   using a
 proof induct
-  case 1 thus ?case by (force)
+  case 1 thus ?case by simp
 next
-  case 2 thus ?case by (force dest: b1 intro: rtrancl_trans)
+  case 2 thus ?case by (blast dest: b1 intro: rtrancl_trans)
 qed
   
-lemma one_pr_congR: 
+lemma one_app_congR: 
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
 using a
 proof induct
-  case 1 thus ?case by (force)
+  case 1 thus ?case by simp
 next 
-  case 2 thus ?case by (force dest: b2 intro: rtrancl_trans)
+  case 2 thus ?case by (blast dest: b2 intro: rtrancl_trans)
 qed
 
-lemma one_pr_cong: 
+lemma one_app_cong: 
   assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" 
   shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
 proof -
-  have b1: "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_pr_congL)
-  have b2: "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_pr_congR)
-  show ?thesis using b1 b2 by (force intro: rtrancl_trans)
+  have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL)
+  moreover
+  have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR)
+  ultimately show ?thesis by (blast intro: rtrancl_trans)
 qed
 
 lemma one_beta_star: 
@@ -720,29 +689,28 @@
   shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"
   using a
 proof induct
-  case o1 thus ?case by (force)
+  case o1 thus ?case by simp
 next
-  case o2 thus ?case by (force intro!: one_pr_cong)
+  case o2 thus ?case by (blast intro!: one_app_cong)
 next
-  case o3 thus ?case by (force intro!: one_abs_cong)
+  case o3 thus ?case by (blast intro!: one_abs_cong)
 next 
   case (o4 a s1 s2 t1 t2)
-  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" .
+  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact
   have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" by (rule b4)
   from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 
-    by (force intro!: one_pr_cong one_abs_cong)
-  show ?case using c1 c2 by (force intro: rtrancl_trans)
+    by (blast intro!: one_app_cong one_abs_cong)
+  show ?case using c1 c2 by (blast intro: rtrancl_trans)
 qed
  
 lemma one_star_abs_cong: 
-  fixes a :: "name"
   assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
   shows "(Lam  [a].t1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [a].t2)"
   using a
 proof induct
-  case 1 thus ?case by (force)
+  case 1 thus ?case by simp
 next
-  case 2 thus ?case by (force intro: rtrancl_trans)
+  case 2 thus ?case by (blast intro: rtrancl_trans)
 qed
 
 lemma one_star_pr_congL: 
@@ -750,9 +718,9 @@
   shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
   using a
 proof induct
-  case 1 thus ?case by (force)
+  case 1 thus ?case by simp
 next
-  case 2 thus ?case by (force intro: rtrancl_trans)
+  case 2 thus ?case by (blast intro: rtrancl_trans)
 qed
 
 lemma one_star_pr_congR: 
@@ -760,9 +728,9 @@
   shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
   using a
 proof induct
-  case 1 thus ?case by (force)
+  case 1 thus ?case by simp
 next
-  case 2 thus ?case by (force intro: rtrancl_trans)
+  case 2 thus ?case by (blast intro: rtrancl_trans)
 qed
 
 lemma beta_one_star: 
@@ -770,13 +738,13 @@
   shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
   using a
 proof induct
-  case b1 thus ?case by (force intro!: one_star_pr_congL)
+  case b1 thus ?case by (blast intro!: one_star_pr_congL)
 next
-  case b2 thus ?case by (force intro!: one_star_pr_congR)
+  case b2 thus ?case by (blast intro!: one_star_pr_congR)
 next
-  case b3 thus ?case by (force intro!: one_star_abs_cong)
+  case b3 thus ?case by (blast intro!: one_star_abs_cong)
 next
-  case b4 thus ?case by (force)
+  case b4 thus ?case by blast
 qed
 
 lemma trans_closure: 
@@ -785,7 +753,7 @@
   assume "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
   thus "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
   proof induct
-    case 1 thus ?case by (force)
+    case 1 thus ?case by simp
   next
     case 2 thus ?case by (force intro: rtrancl_trans simp add: one_beta_star)
   qed
@@ -793,7 +761,7 @@
   assume "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
   thus "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
   proof induct
-    case 1 thus ?case by (force)
+    case 1 thus ?case by simp
   next
     case 2 thus ?case by (force intro: rtrancl_trans simp add: beta_one_star)
   qed
@@ -811,19 +779,19 @@
   have b: "s1 \<longrightarrow>\<^isub>1 s2" by fact
   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
   have c: "t \<longrightarrow>\<^isub>1 t2" by fact
-  show "(\<exists>t3.  s2 \<longrightarrow>\<^isub>1 t3 \<and>  t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" 
+  show "\<exists>t3. s2 \<longrightarrow>\<^isub>1 t3 \<and>  t2 \<longrightarrow>\<^isub>1\<^sup>* t3" 
   proof -
-    from c h have "(\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" by force
-    then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (force)
-    have "(\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4)" using b c1 by (force intro: diamond)
-    thus ?thesis using c2 by (force intro: rtrancl_trans)
+    from c h have "\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
+    then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
+    have "\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4" using b c1 by (blast intro: diamond)
+    thus ?thesis using c2 by (blast intro: rtrancl_trans)
   qed
 qed
 
 lemma cr_one_star: 
   assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2"
       and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1"
-    shows "(\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3)"
+    shows "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3"
 using a
 proof induct
   case 1
@@ -833,26 +801,27 @@
   assume d: "s1 \<longrightarrow>\<^isub>1 s2"
   assume "\<exists>t3.  t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and>  s1 \<longrightarrow>\<^isub>1\<^sup>* t3"
   then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
-                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" by force
-  from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by force
+                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
+  from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
   then obtain t4 where g1: "t3\<longrightarrow>\<^isub>1t4"
-                   and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by force
-  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (force intro: rtrancl_trans)
-  thus ?case using g2 by (force)
+                   and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
+  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: rtrancl_trans)
+  thus ?case using g2 by blast
 qed
   
 lemma cr_beta_star: 
   assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1" 
   and a2: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
-  shows "(\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3)"
+  shows "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3"
 proof -
   from a1 have b1: "t\<longrightarrow>\<^isub>1\<^sup>*t1" by (simp add: trans_closure[symmetric])
   from a2 have b2: "t\<longrightarrow>\<^isub>1\<^sup>*t2" by (simp add: trans_closure[symmetric])
-  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) 
-  from c obtain t3 where d1: "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and d2: "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by force
-  from d1 have e1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp add: trans_closure)
-  from d2 have e2: "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp add: trans_closure)
-  show ?thesis using e1 and e2 by (force)
+  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) 
+  from c obtain t3 where d1: "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and d2: "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by blast
+  have "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" using d1 by (simp add: trans_closure)
+  moreover
+  have "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" using d2 by (simp add: trans_closure)
+  ultimately show ?thesis by blast
 qed
 
 end
diff -r 0e1d025d57b3 -r 35fba71ec6ef src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Fri Dec 09 09:06:45 2005 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Fri Dec 09 12:38:49 2005 +0100
@@ -8,7 +8,6 @@
 
 section {* Beta Reduction *}
 
-
 lemma subst_rename[rule_format]: 
   shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
 apply(nominal_induct t1 avoiding: a c t2 rule: lam_induct)
@@ -129,10 +128,13 @@
   thus ?thesis by simp
 qed
 
-lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)"
-apply(erule Beta.induct)
-apply(auto intro!: simp add: abs_supp lam.supp subst_supp)
-done
+lemma supp_beta: 
+  assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
+  shows "(supp s)\<subseteq>((supp t)::name set)"
+using a
+by (induct)
+   (auto intro!: simp add: abs_supp lam.supp subst_supp)
+
 
 lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
 apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
@@ -221,8 +223,10 @@
 lemma fresh_context[rule_format]: 
   fixes  \<Gamma> :: "(name\<times>ty)list"
   and    a :: "name"
-  shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
-apply(induct_tac \<Gamma>)
+  assumes a: "a\<sharp>\<Gamma>"
+  shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
+using a
+apply(induct \<Gamma>)
 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
 done
 
@@ -236,8 +240,12 @@
 done
 
 lemma valid_unicity[rule_format]: 
-  shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>" 
-apply(induct_tac \<Gamma>)
+  assumes a: "valid \<Gamma>"
+  and     b: "(c,\<sigma>)\<in>set \<Gamma>"
+  and     c: "(c,\<tau>)\<in>set \<Gamma>"
+  shows "\<sigma>=\<tau>" 
+using a b c
+apply(induct \<Gamma>)
 apply(auto dest!: valid_elim fresh_context)
 done
 
@@ -351,8 +359,11 @@
 apply(auto)
 done
 
-lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))"
-apply(induct_tac \<Gamma>)
+lemma in_ctxt: 
+  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
+  shows "a\<in>set(dom_ty \<Gamma>)"
+using a
+apply(induct \<Gamma>)
 apply(auto)
 done
 
@@ -390,134 +401,124 @@
   shows "valid \<Gamma>"
 using a by (induct, auto dest!: valid_elim)
 
-lemma ty_subs[rule_format]:
-  fixes \<Gamma> ::"(name\<times>ty) list"
-  and   t1 ::"lam"
-  and   t2 ::"lam"
-  and   \<tau>  ::"ty"
-  and   \<sigma>  ::"ty" 
-  and   c  ::"name"
-  shows  "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
+lemma ty_subs:
+  assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
+  and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
+  shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
+using a b
 proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam_induct)
   case (Var a) 
-  show ?case
-  proof(intro strip)
-    assume a1: "\<Gamma> \<turnstile>t2:\<sigma>"
-    assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>"
-    hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
-    from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
-    from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
-    show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
-    proof (cases "a=c", simp_all)
-      assume case1: "a=c"
-      show "\<Gamma> \<turnstile> t2:\<tau>" using a1
-      proof (cases "\<sigma>=\<tau>")
-	assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
-      next
-	assume a3: "\<sigma>\<noteq>\<tau>"
-	show ?thesis
-	proof (rule ccontr)
-	  from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
-	  with case1 a25 show False by force 
-	qed
+  have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
+  have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
+  hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
+  from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
+  from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
+  show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
+  proof (cases "a=c", simp_all)
+    assume case1: "a=c"
+    show "\<Gamma> \<turnstile> t2:\<tau>" using a1
+    proof (cases "\<sigma>=\<tau>")
+      assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
+    next
+      assume a3: "\<sigma>\<noteq>\<tau>"
+      show ?thesis
+      proof (rule ccontr)
+	from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
+	with case1 a25 show False by force 
       qed
-    next
-      assume case2: "a\<noteq>c"
-      with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
-      from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
     qed
+  next
+    assume case2: "a\<noteq>c"
+    with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
+    from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
   qed
 next
   case (App s1 s2)
-  show ?case
-  proof (intro strip, simp)
-    assume b1: "\<Gamma> \<turnstile>t2:\<sigma>" 
-    assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>"
-    hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
-    then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
-    show "\<Gamma> \<turnstile>  App (s1[c::=t2]) (s2[c::=t2]) : \<tau>" 
-      using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto)
-  qed
+  have b1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
+  have b2: "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
+  hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
+  then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
+  show "\<Gamma> \<turnstile>  (App s1 s2)[c::=t2] : \<tau>" 
+    using b1 b3a b3b prems by (simp, rule_tac \<tau>="\<tau>'" in t2, auto)
 next
   case (Lam a s)
   have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
   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>)"
     by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
-  show ?case using f2 f3
-  proof(intro strip, simp)
-    assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>"
-    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) 
-    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
-    from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
-    hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
-      by (auto dest: valid_elim simp add: fresh_list_cons) 
-    from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
-    proof -
-      have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
-      have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
-	by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
-      from c12 c2 c3 show ?thesis by (force intro: weakening)
-    qed
-    assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
-    have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
-    proof -
-      have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
-      have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
-      with c8 c82 c83 show ?thesis by (force intro: weakening)
-    qed
-    show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>"
-      using c11 Lam c14 c81 f1 by force
+  have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
+  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) 
+  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
+  from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
+  hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
+    by (auto dest: valid_elim simp add: fresh_list_cons) 
+  from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
+  proof -
+    have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
+    have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
+      by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
+    from c12 c2 c3 show ?thesis by (force intro: weakening)
   qed
+  assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
+  have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
+  proof -
+    have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
+    have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
+    with c8 c82 c83 show ?thesis by (force intro: weakening)
+  qed
+  show "\<Gamma> \<turnstile> (Lam [a].s)[c::=t2] : \<tau>"
+    using c11 prems c14 c81 f1 by force
 qed
 
-lemma subject[rule_format]: 
+lemma subject: 
   fixes \<Gamma>  ::"(name\<times>ty) list"
   and   t1 ::"lam"
   and   t2 ::"lam"
   and   \<tau>  ::"ty"
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
-  shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)"
-using a
-proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct, auto)
+  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
+  shows "\<Gamma> \<turnstile> t2:\<tau>"
+using a b
+proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
   case (b1 t s1 s2)
-  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
-  assume "\<Gamma> \<turnstile> App s1 t : \<tau>" 
-  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim)
-  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force
-  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force
+  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
+  have "\<Gamma> \<turnstile> App s1 t : \<tau>" by fact 
+  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>" by (rule t2_elim)
+  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by blast
+  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by blast
 next
   case (b2 t s1 s2)
-  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
-  assume "\<Gamma> \<turnstile> App t s1 : \<tau>" 
-  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim)
-  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force
-  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force
+  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
+  have "\<Gamma> \<turnstile> App t s1 : \<tau>" by fact
+  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>" by (rule t2_elim)
+  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by blast
+  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by blast
 next
   case (b3 a s1 s2)
-  have f: "a\<sharp>\<Gamma>" and "a\<sharp>\<tau>" by fact+
-  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
-  assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>"
-  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)
-  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
-  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force 
+  have f: "a\<sharp>\<Gamma>" and "a\<sharp>\<tau>" by fact
+  have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
+  have "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" by fact
+  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)
+  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
+  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by blast
 next
   case (b4 a s1 s2)
   have f: "a\<sharp>\<Gamma>" by fact
-  assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>"
+  have "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" by fact
   hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim)
-  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force
-  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim)
-  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (force intro: ty_subs)
+  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by blast
+  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (blast dest!: t3_elim)
+  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (blast intro: ty_subs)
 qed
 
-lemma subject[rule_format]: 
+lemma subject_automatic: 
   fixes \<Gamma>  ::"(name\<times>ty) list"
   and   t1 ::"lam"
   and   t2 ::"lam"
   and   \<tau>  ::"ty"
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
-  shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>"
-using a
+  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
+  shows "\<Gamma> \<turnstile> t2:\<tau>"
+using a b
 apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
 apply(auto dest!: t2_elim t3_elim intro: ty_subs)
 done
@@ -544,7 +545,6 @@
 apply(auto)
 done
 
-
 section {* Candidates *}
 
 consts
@@ -565,10 +565,11 @@
 translations 
   "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
 inductive FST
-intros
+  intros
 fst[intro!]:  "(App t s) \<guillemotright> t"
 
-lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
+lemma fst_elim[elim!]: 
+  shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
 apply(ind_cases "App t s \<guillemotright> t'")
 apply(simp add: lam.inject)
 done
@@ -826,8 +827,11 @@
 apply(force simp add: RED_props)
 done
 
-lemma fresh_domain[rule_format]: "a\<sharp>\<theta>\<longrightarrow>a\<notin>set(domain \<theta>)"
-apply(induct_tac \<theta>)
+lemma fresh_domain: 
+  assumes a: "a\<sharp>\<theta>"
+  shows "a\<notin>set(domain \<theta>)"
+using a
+apply(induct \<theta>)
 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
 done