diff -r 577e5d19b33c -r b18fabea0fd0 src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Nov 30 16:59:19 2005 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Nov 30 17:56:08 2005 +0100
@@ -8,21 +8,22 @@
 
 lemma forget[rule_format]: 
   shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
-proof (nominal_induct t1 rule: lam_induct)
+proof (nominal_induct t1 fresh: a t2 rule: lam_induct)
   case (Var a t2 b) 
   show ?case by (simp, simp add: fresh_atm)
 next 
   case App
   thus ?case by (simp add: fresh_prod)
 next
-  case (Lam a t2 c t)
-  have i: "\<forall>a b. a\<sharp>t \<longrightarrow>  t[a::=b] = t" by fact
-  have "c\<sharp>(a,t2)" by fact
-  hence a: "a\<noteq>c" and b: "c\<sharp>t2" by (auto simp add: fresh_prod fresh_atm)
+  case (Lam c t a t2)
+  have i: "\<And>c t2. c\<sharp>t \<longrightarrow>  t[c::=t2] = t" by fact
+  have a: "c\<sharp>t2" by fact
+  have "c\<sharp>a" by fact
+  hence b: "a\<noteq>c" by (simp add: fresh_atm)
   show ?case
   proof 
     assume "a\<sharp>Lam [c].t" 
-    hence "a\<sharp>t" using a by (force simp add: abs_fresh)
+    hence "a\<sharp>t" using b by (simp add: abs_fresh)
     hence "t[a::=t2] = t" using i by simp
     thus "(Lam [c].t)[a::=t2] = Lam [c].t" using a b by (simp add: alpha)
   qed
@@ -30,8 +31,8 @@
 
 lemma forget[rule_format]: 
   shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
-apply (nominal_induct t1 rule: lam_induct)
-apply(auto simp add: abs_fresh fresh_atm fresh_prod)
+apply (nominal_induct t1 fresh: a t2 rule: lam_induct)
+apply(auto simp add: abs_fresh fresh_atm)
 done
 
 lemma fresh_fact[rule_format]: 
@@ -40,24 +41,23 @@
   and    t1 :: "lam"
   and    t2 :: "lam" 
   shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
-proof (nominal_induct t1 rule: lam_induct)
-  case (Var a b t2 c) 
-  show ?case by (simp)
+proof (nominal_induct t1 fresh: a b t2 rule: lam_induct)
+  case (Var c a b t2) 
+  show ?case by simp
 next
-  case App 
-  thus ?case by (simp add: fresh_prod)
+  case App thus ?case by simp 
 next
-  case (Lam a b t2 c t)
-  have  i: "\<forall>(a::name) b t2. a\<sharp>t\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t[b::=t2])" by fact
-  have "c\<sharp>(a,b,t2)" by fact
-  hence b: "c\<noteq>a \<and> c\<noteq>b \<and> c\<sharp>t2" by (simp add: fresh_prod fresh_atm) 
+  case (Lam c t a b t2)
+  have  i: "\<And>(a::name) b t2. a\<sharp>t\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t[b::=t2])" by fact
+  have fr: "c\<sharp>a" "c\<sharp>b" "c\<sharp>t2" by fact+
+  hence fr': "c\<noteq>a" by (simp add: fresh_atm) 
   show ?case 
   proof (intro strip)
     assume a1: "a\<sharp>t2"
     assume a2: "a\<sharp>Lam [c].t"
-    hence "a\<sharp>t" using b by (force simp add: abs_fresh)
+    hence "a\<sharp>t" using fr' by (simp add: abs_fresh)
     hence "a\<sharp>t[b::=t2]" using a1 i by simp
-    thus "a\<sharp>(Lam [c].t)[b::=t2]" using b by (simp add: abs_fresh)
+    thus "a\<sharp>(Lam [c].t)[b::=t2]" using fr  by (simp add: abs_fresh)
   qed
 qed
 
@@ -67,7 +67,7 @@
   and    t1 :: "lam"
   and    t2 :: "lam" 
   shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
-apply(nominal_induct t1 rule: lam_induct)
+apply(nominal_induct t1 fresh: a b t2 rule: lam_induct)
 apply(auto simp add: abs_fresh fresh_prod fresh_atm)
 done
 
@@ -77,101 +77,57 @@
   and   L::"lam"
   and   M::"lam"
   and   N::"lam"
-  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
-proof (nominal_induct M rule: lam_induct)
-  case (Var L N x y z) (* case 1: Variables*)
-  show ?case
-  proof (intro strip)
-    assume a1: "x\<noteq>y"
-    and    a2: "x\<sharp>L"
-    show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
-    proof -
-      have "z=x \<or> (z\<noteq>x \<and> z=y) \<or> (z\<noteq>x \<and> z\<noteq>y)" by force 
-      moreover (*Case 1.1*)
-      { assume c1: "z=x"
-	have c1l: "?LHS = N[y::=L]"    using c1    by simp
-	have c1r: "?RHS = N[y::=L]"    using c1 a1 by simp
-	from c1l and c1r have "?LHS = ?RHS"  by simp
-      }
-      moreover (*Case 1.2*)
-      { assume c2: "z\<noteq>x \<and> z=y"
-	have c2l: "?LHS = L"               using c2 by force
-	have c2r: "?RHS = L[x::=N[y::=L]]" using c2 by force
-	have c2x: "L[x::=N[y::=L]] = L"    using a2 by (simp add: forget)
-	from c2l and c2r and c2x have "?LHS = ?RHS" by simp
-      }
-      moreover (*Case 1.3*)
-      { assume c3: "z\<noteq>x \<and> z\<noteq>y"
-	have c3l: "?LHS = Var z" using c3 by force
-	have c3r: "?RHS = Var z" using c3 by force
-	from c3l and c3r have "?LHS = ?RHS" by simp
-      }
-      ultimately show "?LHS = ?RHS" by blast
-    qed
+  assumes a: "x\<noteq>y"
+  and     b: "x\<sharp>L"
+  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
+using a b
+proof (nominal_induct M fresh: x y N L rule: lam_induct)
+  case (Var z) (* case 1: Variables*)
+  have "x\<noteq>y" by fact
+  have "x\<sharp>L" by fact
+  show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
+  proof -
+    { (*Case 1.1*)
+      assume  "z=x"
+      have "(1)": "?LHS = N[y::=L]" using `z=x` by simp
+      have "(2)": "?RHS = N[y::=L]" using `z=x` `x\<noteq>y` by simp
+      from "(1)" "(2)" have "?LHS = ?RHS"  by simp
+    }
+    moreover 
+    { (*Case 1.2*)
+      assume "z\<noteq>x" and "z=y"
+      have "(1)": "?LHS = L"               using `z\<noteq>x` `z=y` by force
+      have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by force
+      have "(3)": "L[x::=N[y::=L]] = L"    using `x\<sharp>L` by (simp add: forget)
+      from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp
+    }
+    moreover 
+    { (*Case 1.3*)
+      assume "z\<noteq>x" and "z\<noteq>y"
+      have "(1)": "?LHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force
+      have "(2)": "?RHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force
+      from "(1)" "(2)" have "?LHS = ?RHS" by simp
+    }
+    ultimately show "?LHS = ?RHS" by blast
   qed
 next
-  case (Lam L N x y z M1) (* case 2: lambdas *)
-  assume f1: "z\<sharp>(L,N,x,y)"
-  from f1 have f2: "z \<sharp> N[y::=L]" by (simp add: fresh_fact fresh_prod)
-  show ?case
-  proof (intro strip)
-    assume  a1: "x\<noteq>y"
-    and     a2: "x\<sharp>L"
-    show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
-    proof -
-      have "?LHS = Lam [z].(M1[x::=N][y::=L])"             using f1 
-	by (simp add: fresh_prod fresh_atm)
-      also have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])"   using a1 a2 Lam(2)  by simp
-      also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using f1 f2 
-	by (simp add: fresh_prod fresh_atm)
-      also have "\<dots> = ?RHS" using f1 by (simp add: fresh_prod fresh_atm)
-      finally show "?LHS = ?RHS" .
-    qed
+  case (Lam z M1) (* case 2: lambdas *)
+  have ih: "\<And>x y N L. x\<noteq>y \<Longrightarrow> x\<sharp>L \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
+  have "x\<noteq>y" by fact
+  have "x\<sharp>L" by fact
+  have "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
+  hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
+  show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
+  proof -
+    have "?LHS = Lam [z].(M1[x::=N][y::=L])" using `z\<sharp>x` `z\<sharp>y` `z\<sharp>N` `z\<sharp>L` by simp
+    also from ih have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])" using `x\<noteq>y` `x\<sharp>L` by simp
+    also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using `z\<sharp>x` `z\<sharp>N[y::=L]` by simp
+    also have "\<dots> = ?RHS" using  `z\<sharp>y` `z\<sharp>L` by simp
+    finally show "?LHS = ?RHS" .
   qed
 next
-  case (App L N x y M1 M2) (* case 3: applications *)
-  show ?case
-  proof (intro strip)
-    assume a1: "x\<noteq>y"
-    and    a2: "x\<sharp>L"
-    from a1 a2 App show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
-  qed
-qed
-
-lemma subs_lemma: 
-  fixes x::"name"
-  and   y::"name"
-  and   L::"lam"
-  and   M::"lam"
-  and   N::"lam"
-  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
-proof (nominal_induct M rule: lam_induct)
-  case (Var L N x y z) (* case 1: Variables*)
-  show ?case
-  proof -
-    have "z=x \<or> (z\<noteq>x \<and> z=y) \<or> (z\<noteq>x \<and> z\<noteq>y)" by force
-    thus "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" 
-    using forget by force
-  qed
-next
-  case (Lam L N x y z M1) (* case 2: lambdas *)
-  assume f1: "z\<sharp>(L,N,x,y)" 
-  hence f2: "z\<sharp>N[y::=L]" by (simp add: fresh_fact fresh_prod)
-  show ?case
-  proof (intro strip)
-    assume a1: "x\<noteq>y"
-    and    a2: "x\<sharp>L"
-    show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
-    proof -
-      have "?LHS = Lam [z].(M1[x::=N][y::=L])" using f1 by (simp add: fresh_prod fresh_atm)
-      also have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])"   using a1 a2 Lam(2)  by simp
-      also have "\<dots> = ?RHS" using f1 f2 by (simp add: fresh_prod fresh_atm)
-      finally show "?LHS = ?RHS" .
-    qed
-  qed
-next
-  case (App L N x y M1 M2) (* case 3: applications *)
-  thus "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
+  case (App M1 M2) (* case 3: applications *)
+  thus ?case by simp
 qed
 
 lemma subs_lemma:  
@@ -180,10 +136,12 @@
   and   L::"lam"
   and   M::"lam"
   and   N::"lam"
-  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
-apply(nominal_induct M rule: lam_induct)
-apply(auto simp add: fresh_fact forget fresh_prod fresh_atm)
-done
+  assumes "x\<noteq>y"
+  and     "x\<sharp>L"
+  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
+using prems
+by (nominal_induct M fresh: x y N L rule: lam_induct)
+   (auto simp add: fresh_fact forget)
 
 lemma subst_rename[rule_format]: 
   fixes  c  :: "name"
@@ -191,25 +149,25 @@
   and    t1 :: "lam"
   and    t2 :: "lam"
   shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
-proof (nominal_induct t1 rule: lam_induct)
-  case (Var a c t2 b)
+proof (nominal_induct t1 fresh: a c t2 rule: lam_induct)
+  case (Var b)
   show "c\<sharp>(Var b) \<longrightarrow> (Var b)[a::=t2] = ([(c,a)]\<bullet>(Var b))[c::=t2]" by (simp add: calc_atm fresh_atm)
 next
-  case App thus ?case by (force simp add: fresh_prod)
+  case App thus ?case by force
 next
-  case (Lam a c t2 b s)
-  have i: "\<forall>a c t2. c\<sharp>s \<longrightarrow> (s[a::=t2] = ([(c,a)]\<bullet>s)[c::=t2])" by fact
-  have f: "b\<sharp>(a,c,t2)" by fact
-  from f have a:"b\<noteq>c" and b: "b\<noteq>a" and c: "b\<sharp>t2" by (simp add: fresh_prod fresh_atm)+
+  case (Lam b s)
+  have i: "\<And>a c t2. c\<sharp>s \<longrightarrow> (s[a::=t2] = ([(c,a)]\<bullet>s)[c::=t2])" by fact
+  have f: "b\<sharp>a" "b\<sharp>c" "b\<sharp>t2" by fact
+  from f have a:"b\<noteq>c" and b: "b\<noteq>a" and c: "b\<sharp>t2" by (simp add: fresh_atm)+
   show "c\<sharp>Lam [b].s \<longrightarrow> (Lam [b].s)[a::=t2] = ([(c,a)]\<bullet>(Lam [b].s))[c::=t2]" (is "_ \<longrightarrow> ?LHS = ?RHS")
   proof
     assume "c\<sharp>Lam [b].s"
-    hence "c\<sharp>s" using a by (force simp add: abs_fresh)
+    hence "c\<sharp>s" using a by (simp add: abs_fresh)
     hence d: "s[a::=t2] = ([(c,a)]\<bullet>s)[c::=t2]" using i by simp
     have    "?LHS = Lam [b].(s[a::=t2])" using b c by simp
     also have "\<dots> = Lam [b].(([(c,a)]\<bullet>s)[c::=t2])" using d by simp
     also have "\<dots> = (Lam [b].([(c,a)]\<bullet>s))[c::=t2]" using a c by simp
-    also have "\<dots> = ?RHS" using a b by (force simp add: calc_atm)
+    also have "\<dots> = ?RHS" using a b by (simp add: calc_atm)
     finally show "?LHS = ?RHS" by simp
   qed
 qed
@@ -220,8 +178,8 @@
   and    t1 :: "lam"
   and    t2 :: "lam"
   shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
-apply(nominal_induct t1 rule: lam_induct)
-apply(auto simp add: calc_atm fresh_atm fresh_prod abs_fresh)
+apply(nominal_induct t1 fresh: a c t2 rule: lam_induct)
+apply(auto simp add: calc_atm fresh_atm abs_fresh)
 done
 
 section {* Beta Reduction *}
@@ -245,89 +203,69 @@
   fixes pi :: "name prm"
   and   t  :: "lam"
   and   s  :: "lam"
-  shows "t\<longrightarrow>\<^isub>\<beta>s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
-  apply(erule Beta.induct)
-  apply(auto)
-  done
+  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
+  shows "(pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
+  using a by (induct, auto)
 
-lemma beta_induct_aux[rule_format]:
-  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
-  and    t :: "lam"
-  and    s :: "lam"
-  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
-  and a1:    "\<And>x t s1 s2. 
-              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
-  and a2:    "\<And>x t s1 s2. 
-              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
-  and a3:    "\<And>x (a::name) s1 s2. 
-              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
-  and a4:    "\<And>x (a::name) t1 s1. a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
-  shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"
-using a
-proof (induct)
-  case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
-next
-  case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
-next
-  case (b3 a s1 s2)
-  assume j1: "s1 \<longrightarrow>\<^isub>\<beta> s2"
-  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"
-  show ?case 
-  proof (simp, intro strip)
-    fix pi::"name prm" and x::"'a::fs_name"
-     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
-      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
-    then obtain c::"name" 
-      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
-      by (force simp add: fresh_prod fresh_atm)
-    have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2)) x"
-      using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
-    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
-      by (simp add: lam.inject alpha)
-    have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
-      by (simp add: lam.inject alpha)
-    show " P (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2)) x"
-      using x alpha1 alpha2 by (simp only: pt_name2)
-  qed
-next
-  case (b4 a s1 s2)
-  show ?case
-  proof (simp add: subst_eqvt, intro strip)
-    fix pi::"name prm" and x::"'a::fs_name" 
-    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
-      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
-    then obtain c::"name" 
-      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
-      by (force simp add: fresh_prod fresh_atm)
-    have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)]) x"
-      using a4 f2 by (blast intro!: eqvt_beta)
-    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
-      by (simp add: lam.inject alpha)
-    have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
-      using f3 by (simp only: subst_rename[symmetric] pt_name2)
-    show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"
-      using x alpha1 alpha2 by (simp only: pt_name2)
-  qed
-qed
-
-
-lemma beta_induct[case_names b1 b2 b3 b4]:
-  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]:
+  fixes  P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool"
   and    t :: "lam"
   and    s :: "lam"
   and    x :: "'a::fs_name"
   assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
-  and a1:    "\<And>x t s1 s2. 
-              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
-  and a2:    "\<And>x t s1 s2. 
-              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
-  and a3:    "\<And>x (a::name) s1 s2. 
-              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
-  and a4:    "\<And>x (a::name) t1 s1. 
-              a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
-  shows "P t s x"
-using a a1 a2 a3 a4
-by (auto intro!: beta_induct_aux[of "t" "s" "P" "[]" "x", simplified])
+  and a1:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App s1 t) (App s2 t)"
+  and a2:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App t s1) (App t s2)"
+  and a3:    "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
+  and a4:    "\<And>a t1 s1 x. a\<sharp>(s1,x) \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
+  shows "P x t s"
+proof -
+  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
+  proof (induct)
+    case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
+  next
+    case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
+  next
+    case (b3 a s1 s2)
+    have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
+    have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
+    show ?case 
+    proof (simp)
+      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
+	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+      then obtain c::"name" 
+	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
+	by (force simp add: fresh_prod fresh_atm)
+      have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2))"
+	using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
+      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
+	by (simp add: lam.inject alpha)
+      have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
+	by (simp add: lam.inject alpha)
+      show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2))"
+	using x alpha1 alpha2 by (simp only: pt_name2)
+    qed
+  next
+    case (b4 a s1 s2)
+    show ?case
+    proof (simp add: subst_eqvt)
+      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
+	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+      then obtain c::"name" 
+	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
+	by (force simp add: fresh_prod fresh_atm)
+      have x: "P x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)])"
+	using a4 f2 by (blast intro!: eqvt_beta)
+      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
+	by (simp add: lam.inject alpha)
+      have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
+	using f3 by (simp only: subst_rename[symmetric] pt_name2)
+      show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
+	using x alpha1 alpha2 by (simp only: pt_name2)
+    qed
+  qed
+  hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast 
+  thus ?thesis by simp
+qed
 
 section {* One-Reduction *}
 
@@ -350,109 +288,93 @@
   fixes pi :: "name prm"
   and   t  :: "lam"
   and   s  :: "lam"
-  shows "t\<longrightarrow>\<^isub>1s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>1(pi\<bullet>s)"
-  apply(erule One.induct)
-  apply(auto)
-  done
+  assumes a: "t\<longrightarrow>\<^isub>1s"
+  shows "(pi\<bullet>t)\<longrightarrow>\<^isub>1(pi\<bullet>s)"
+  using a by (induct, auto)
 
-lemma one_induct_aux[rule_format]:
-  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
-  and    t :: "lam"
-  and    s :: "lam"
-  assumes a: "t\<longrightarrow>\<^isub>1s"
-  and a1:    "\<forall>x t. P t t x"
-  and a2:    "\<forall>x t1 t2 s1 s2. 
-              (t1\<longrightarrow>\<^isub>1t2 \<and> (\<forall>z. P t1 t2 z) \<and> s1\<longrightarrow>\<^isub>1s2 \<and> (\<forall>z. P s1 s2 z)) 
-              \<longrightarrow> P (App t1 s1) (App t2 s2) x"
-  and a3:    "\<forall>x (a::name) s1 s2. (a\<sharp>x \<and> s1\<longrightarrow>\<^isub>1s2 \<and> (\<forall>z. P s1 s2 z)) 
-             \<longrightarrow>  P (Lam [a].s1) (Lam [a].s2) x"
-  and a4:    "\<forall>x (a::name) t1 t2 s1 s2. 
-              (a\<sharp>(s1,s2,x) \<and> t1\<longrightarrow>\<^isub>1t2 \<and> (\<forall>z. P t1 t2 z) \<and> s1\<longrightarrow>\<^isub>1s2 \<and> (\<forall>z. P s1 s2 z)) 
-              \<longrightarrow> P (App (Lam [a].t1) s1) (t2[a::=s2]) x"
-  shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"
-using a
-proof (induct)
-  case o1 show ?case using a1 by force
-next
-  case (o2 s1 s2 t1 t2) 
-  thus ?case using a2 by (simp, blast intro: eqvt_one)
-next
-  case (o3 a t1 t2)
-  assume j1: "t1 \<longrightarrow>\<^isub>1 t2"
-  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>t1) (pi\<bullet>t2) x"
-  show ?case 
-  proof (simp, intro strip)
-    fix pi::"name prm" and x::"'a::fs_name"
-     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,x)"
-      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
-    then obtain c::"name" 
-      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
-      by (force simp add: fresh_prod fresh_atm)
-    have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t2)) x"
-      using a3 f2 j1 j2 by (simp, blast intro: eqvt_one)
-    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3
-      by (simp add: lam.inject alpha)
-    have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t2))" using f1 f3
-      by (simp add: lam.inject alpha)
-    show " P (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (Lam [(pi\<bullet>a)].(pi\<bullet>t2)) x"
-      using x alpha1 alpha2 by (simp only: pt_name2)
-  qed
-next
-case (o4 a s1 s2 t1 t2)
-  assume j0: "t1 \<longrightarrow>\<^isub>1 t2"
-  assume j1: "s1 \<longrightarrow>\<^isub>1 s2"
-  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>t1) (pi\<bullet>t2) x"
-  assume j3: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"
-  show ?case
-  proof (simp, intro strip)
-    fix pi::"name prm" and x::"'a::fs_name" 
-    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,pi\<bullet>s1,pi\<bullet>s2,x)"
-      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
-    then obtain c::"name" 
-      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s1,pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
-      by (force simp add: fresh_prod at_fresh[OF at_name_inst])
-    have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (pi\<bullet>s1)) ((([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)]) x"
-      using a4 f2 j0 j1 j2 j3 by (simp, blast intro!: eqvt_one)
-    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3
-      by (simp add: lam.inject alpha)
-    have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)] = (pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
-      using f4 by (simp only: subst_rename[symmetric] pt_name2)
-    show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (pi\<bullet>s1)) ((pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"
-      using x alpha1 alpha2 by (simp only: pt_name2)
-  qed
-qed
-
-lemma one_induct[rule_format, case_names o1 o2 o3 o4]:
-  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+lemma one_induct[consumes 1, case_names o1 o2 o3 o4]:
+  fixes  P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool"
   and    t :: "lam"
   and    s :: "lam"
   and    x :: "'a::fs_name"
   assumes a: "t\<longrightarrow>\<^isub>1s"
-  and a1:    "\<And>x t. P t t x"
-  and a2:    "\<And>x t1 t2 s1 s2. 
-              t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P t1 t2 z) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P s1 s2 z) \<Longrightarrow> 
-              P (App t1 s1) (App t2 s2) x"
-  and a3:    "\<And>x (a::name) s1 s2. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P s1 s2 z) 
-              \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
-  and a4:    "\<And>x (a::name) t1 t2 s1 s2. 
-              a\<sharp>(s1,s2,x) \<Longrightarrow> t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P t1 t2 z) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P s1 s2 z) 
-              \<Longrightarrow> P (App (Lam [a].t1) s1) (t2[a::=s2]) x"
-  shows "P t s x"
-using a a1 a2 a3 a4
-by (auto intro!: one_induct_aux[of "t" "s" "P" "[]" "x", simplified])
+  and a1:    "\<And>t x. P x t t"
+  and a2:    "\<And>t1 t2 s1 s2 x. t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P z t1 t2) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> 
+              P x (App t1 s1) (App t2 s2)"
+  and a3:    "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
+  and a4:    "\<And>a t1 t2 s1 s2 x. 
+              a\<sharp>(s1,s2,x) \<Longrightarrow> t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P z t1 t2) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P z s1 s2) 
+              \<Longrightarrow> P x (App (Lam [a].t1) s1) (t2[a::=s2])"
+  shows "P x t s"
+proof -
+  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
+  proof (induct)
+    case o1 show ?case using a1 by force
+  next
+    case (o2 s1 s2 t1 t2) 
+    thus ?case using a2 by (simp, blast intro: eqvt_one)
+  next
+    case (o3 a t1 t2)
+    have j1: "t1 \<longrightarrow>\<^isub>1 t2" by fact
+    have j2: "\<And>(pi::name prm) x. P x (pi\<bullet>t1) (pi\<bullet>t2)" by fact
+    show ?case 
+    proof (simp)
+      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,x)"
+	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+      then obtain c::"name" 
+	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
+	by (force simp add: fresh_prod fresh_atm)
+      have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t2))"
+	using a3 f2 j1 j2 by (simp, blast intro: eqvt_one)
+      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3
+	by (simp add: lam.inject alpha)
+      have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t2))" using f1 f3
+	by (simp add: lam.inject alpha)
+      show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (Lam [(pi\<bullet>a)].(pi\<bullet>t2))"
+	using x alpha1 alpha2 by (simp only: pt_name2)
+    qed
+  next
+    case (o4 a s1 s2 t1 t2)
+    have j0: "t1 \<longrightarrow>\<^isub>1 t2" by fact
+    have j1: "s1 \<longrightarrow>\<^isub>1 s2" by fact
+    have j2: "\<And>(pi::name prm) x. P x (pi\<bullet>t1) (pi\<bullet>t2)" by fact
+    have j3: "\<And>(pi::name prm) x. P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
+    show ?case
+    proof (simp)
+      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,pi\<bullet>s1,pi\<bullet>s2,x)"
+	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+      then obtain c::"name" 
+	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s1,pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
+	by (force simp add: fresh_prod at_fresh[OF at_name_inst])
+      have x: "P x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (pi\<bullet>s1)) ((([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)])"
+	using a4 f2 j0 j1 j2 j3 by (simp, blast intro!: eqvt_one)
+      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3
+	by (simp add: lam.inject alpha)
+      have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)] = (pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
+	using f4 by (simp only: subst_rename[symmetric] pt_name2)
+      show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (pi\<bullet>s1)) ((pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
+	using x alpha1 alpha2 by (simp only: pt_name2)
+    qed
+  qed
+  hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast
+  thus ?thesis by simp
+qed
 
-lemma fresh_fact'[rule_format]:  
-  shows "a\<sharp>t2 \<longrightarrow> a\<sharp>(t1[a::=t2])" 
-proof (nominal_induct t1 rule: lam_induct)
-  case (Var a t2 b) 
-  show ?case by (cases "b=a") (force simp add: at_fresh[OF at_name_inst])+ 
+lemma fresh_fact':  
+  assumes a: "a\<sharp>t2" 
+  shows "a\<sharp>(t1[a::=t2])"
+using a 
+proof (nominal_induct t1 fresh: a t2 rule: lam_induct)
+  case (Var b) 
+  thus ?case by (simp add: fresh_atm)
 next
-  case App
-  thus ?case by (simp add: fresh_prod)
+  case App thus ?case by simp
 next
-  case (Lam a t2 c t) 
-  from Lam(1) have "c\<noteq>a \<and> c\<sharp>t2" by (simp add: fresh_prod fresh_atm) 
-  thus ?case using Lam(2) by (force simp add: abs_fresh)
+  case (Lam c t)
+  have "a\<sharp>t2" "c\<sharp>a" "c\<sharp>t2" by fact
+  moreover
+  have ih: "\<And>a t2. a\<sharp>t2 \<Longrightarrow> a\<sharp>(t[a::=t2])" by fact
+  ultimately show ?case by (simp add: abs_fresh)
 qed
 
 lemma one_fresh_preserv[rule_format]:
@@ -561,33 +483,36 @@
   apply(force intro: eqvt_one)
   done
 
-(* first case in Lemma 3.2.4*)
+text {* first case in Lemma 3.2.4*}
 
-lemma one_subst_aux[rule_format]:
+lemma one_subst_aux:
   fixes    M :: "lam"
   and      N :: "lam"
   and      N':: "lam"
   and      x :: "name"
-  shows "N\<longrightarrow>\<^isub>1N'\<longrightarrow>M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
-proof (nominal_induct M rule: lam_induct)
-  case (Var N N' x y) 
-  show "N\<longrightarrow>\<^isub>1N' \<longrightarrow> Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto)
+  assumes a: "N\<longrightarrow>\<^isub>1N'"
+  shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+using a
+proof (nominal_induct M fresh: x N N' rule: lam_induct)
+  case (Var y) 
+  show "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto)
 next
-  case (App N N' x P Q) (* application case - third line *)
-  thus "N\<longrightarrow>\<^isub>1N' \<longrightarrow> (App P Q)[x::=N] \<longrightarrow>\<^isub>1  (App P Q)[x::=N']" using o2 by simp
+  case (App P Q) (* application case - third line *)
+  thus "(App P Q)[x::=N] \<longrightarrow>\<^isub>1  (App P Q)[x::=N']" using o2 by simp
 next 
-  case (Lam N N' x y P) (* abstraction case - fourth line *)
-  thus "N\<longrightarrow>\<^isub>1N' \<longrightarrow> (Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 
-    by (simp add: fresh_prod fresh_atm)
+  case (Lam y P) (* abstraction case - fourth line *)
+  thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 by simp
 qed
 
-lemma one_subst_aux[rule_format]:
+lemma one_subst_aux:
   fixes    M :: "lam"
   and      N :: "lam"
   and      N':: "lam"
   and      x :: "name"
-  shows "N\<longrightarrow>\<^isub>1N'\<longrightarrow>M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
-apply(nominal_induct M rule: lam_induct)
+  assumes a: "N\<longrightarrow>\<^isub>1N'"
+  shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+using a
+apply(nominal_induct M fresh: x N N' rule: lam_induct)
 apply(auto simp add: fresh_prod fresh_atm)
 done
 
@@ -597,40 +522,40 @@
   and      N :: "lam"
   and      N':: "lam"
   and      x :: "name"
-  assumes a: "M\<longrightarrow>\<^isub>1M'" 
-  shows "N\<longrightarrow>\<^isub>1N' \<longrightarrow> M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
-using a
-proof (nominal_induct M M' rule: one_induct)
-  case (o1 x N N' M)
-  show ?case by (simp add: one_subst_aux)
+  assumes a: "M\<longrightarrow>\<^isub>1M'"
+  and     b: "N\<longrightarrow>\<^isub>1N'"
+  shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
+using prems
+proof (nominal_induct M M' fresh: N N' x rule: one_induct)
+  case (o1 M)
+  thus ?case by (simp add: one_subst_aux)
 next
-  case (o2 x N N' M1 M2 N1 N2)
+  case (o2 M1 M2 N1 N2)
   thus ?case by simp
 next
-  case (o3 x N N' a M1 M2)
-  thus ?case by (simp add: fresh_prod fresh_atm)
+  case (o3 a M1 M2)
+  thus ?case by simp
 next
-  case (o4 N N' x a M1 M2 N1 N2)
-  assume e3: "a\<sharp>(N1,N2,N,N',x)"
+  case (o4 a M1 M2 N1 N2)
+  have e3: "a\<sharp>N1" "a\<sharp>N2" "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" by fact
   show ?case
-  proof  
-    assume a1: "N\<longrightarrow>\<^isub>1N'"
-    have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" 
-      using e3 by (simp add: fresh_prod fresh_atm)
+  proof -
+    have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using e3 by simp
     also have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^isub>1 M2[x::=N'][a::=N2[x::=N']]" 
-      using  o4 a1 by force
+      using  o4 b by force
     also have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" 
-      using e3 by (simp add: subs_lemma fresh_prod fresh_atm)
+      using e3 by (simp add: subs_lemma fresh_atm)
     ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^isub>1 M2[a::=N2][x::=N']" by simp
   qed
 qed
 
 lemma one_subst[rule_format]: 
   assumes a: "M\<longrightarrow>\<^isub>1M'" 
-  shows "N\<longrightarrow>\<^isub>1N' \<longrightarrow> M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
-using a
-apply(nominal_induct M M' rule: one_induct)
-apply(auto simp add: one_subst_aux subs_lemma fresh_prod fresh_atm)
+  and     b: "N\<longrightarrow>\<^isub>1N'"
+  shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
+using a b
+apply(nominal_induct M M' fresh: N N' x rule: one_induct)
+apply(auto simp add: one_subst_aux subs_lemma fresh_atm)
 done
 
 lemma diamond[rule_format]: