src/HOL/Nominal/Examples/CR.thy

 next
   case (Lam z M)
   have vc: "z\<sharp>x" "z\<sharp>P" by fact
   have ih: "x\<sharp>M \<Longrightarrow>  M[x::=P] = M" by fact
   have asm: "x\<sharp>Lam [z].M" by fact
-  with vc have "x\<sharp>M" by (simp add: fresh_atm abs_fresh)
-  hence "M[x::=P] = M" using ih by simp
-  thus "(Lam [z].M)[x::=P] = Lam [z].M" using vc by simp
+  then have "x\<sharp>M" using vc by (simp add: fresh_atm abs_fresh)
+  then have "M[x::=P] = M" using ih by simp
+  then show "(Lam [z].M)[x::=P] = Lam [z].M" using vc by simp
 qed
 
 lemma forget_automatic: 
   assumes asm: "x\<sharp>L"
   shows "L[x::=P] = L"
-  using asm by (nominal_induct L avoiding: x P rule: lam.induct)
-               (auto simp add: abs_fresh fresh_atm)
+  using asm 
+by (nominal_induct L avoiding: x P rule: lam.induct)
+   (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
   fixes z::"name"
   assumes asms: "z\<sharp>N" "z\<sharp>L"
   shows "z\<sharp>(N[y::=L])"

 
 lemma fresh_fact_automatic: 
   fixes z::"name"
   assumes asms: "z\<sharp>N" "z\<sharp>L"
   shows "z\<sharp>(N[y::=L])"
-using asms by (nominal_induct N avoiding: z y L rule: lam.induct)
-              (auto simp add: abs_fresh fresh_atm)
+  using asms 
+by (nominal_induct N avoiding: z y L rule: lam.induct)
+   (auto simp add: abs_fresh fresh_atm)
 
 lemma substitution_lemma:  
   assumes a: "x\<noteq>y"
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

     also have "\<dots> = ?RHS" using  `z\<sharp>y` `z\<sharp>L` by simp
     finally show "?LHS = ?RHS" .
   qed
 next
   case (App M1 M2) (* case 3: applications *)
-  thus ?case by simp
+  thus "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
 qed
 
 lemma substitution_lemma_automatic:  
   assumes asm: "x\<noteq>y" "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
-using asm by (nominal_induct M avoiding: x y N L rule: lam.induct)
-             (auto simp add: fresh_fact forget)
+  using asm 
+by (nominal_induct M avoiding: x y N L rule: lam.induct)
+   (auto simp add: fresh_fact forget)
 
 lemma subst_rename: 
-  assumes a: "c\<sharp>t1"
-  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
+  assumes a: "y\<sharp>N"
+  shows "N[x::=L] = ([(y,x)]\<bullet>N)[y::=L]"
 using a
-proof (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
+proof (nominal_induct N avoiding: x y L rule: lam.induct)
   case (Var b)
-  thus "(Var b)[a::=t2] = ([(c,a)]\<bullet>(Var b))[c::=t2]" by (simp add: calc_atm fresh_atm)
+  thus "(Var b)[x::=L] = ([(y,x)]\<bullet>(Var b))[y::=L]" by (simp add: calc_atm fresh_atm)
 next
   case App thus ?case by force
 next
-  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)+
-  have "c\<sharp>Lam [b].s" by fact
-  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
-  show "(Lam [b].s)[a::=t2] = ([(c,a)]\<bullet>(Lam [b].s))[c::=t2]" (is "?LHS = ?RHS")
+  case (Lam b N1)
+  have ih: "y\<sharp>N1 \<Longrightarrow> (N1[x::=L] = ([(y,x)]\<bullet>N1)[y::=L])" by fact
+  have f: "b\<sharp>y" "b\<sharp>x" "b\<sharp>L" by fact
+  from f have a:"b\<noteq>y" and b: "b\<noteq>x" and c: "b\<sharp>L" by (simp add: fresh_atm)+
+  have "y\<sharp>Lam [b].N1" by fact
+  hence "y\<sharp>N1" using a by (simp add: abs_fresh)
+  hence d: "N1[x::=L] = ([(y,x)]\<bullet>N1)[y::=L]" using ih by simp
+  show "(Lam [b].N1)[x::=L] = ([(y,x)]\<bullet>(Lam [b].N1))[y::=L]" (is "?LHS = ?RHS")
   proof -
-    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
+    have    "?LHS = Lam [b].(N1[x::=L])" using b c by simp
+    also have "\<dots> = Lam [b].(([(y,x)]\<bullet>N1)[y::=L])" using d by simp
+    also have "\<dots> = (Lam [b].([(y,x)]\<bullet>N1))[y::=L]" using a c by simp
     also have "\<dots> = ?RHS" using a b by (simp add: calc_atm)
     finally show "?LHS = ?RHS" by simp
   qed
 qed
 
 lemma subst_rename_automatic: 
-  assumes a: "c\<sharp>t1"
-  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
-using a
-apply(nominal_induct t1 avoiding: a c t2 rule: lam.induct)
-apply(auto simp add: calc_atm fresh_atm abs_fresh)
-done
+  assumes a: "y\<sharp>N"
+  shows "N[x::=L] = ([(y,x)]\<bullet>N)[y::=L]"
+  using a
+by (nominal_induct N avoiding: y x L rule: lam.induct)
+   (auto simp add: calc_atm fresh_atm abs_fresh)
 
 section {* Beta Reduction *}
 
-consts
-  Beta :: "(lam\<times>lam) set"
-syntax 
-  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
-  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
-translations 
-  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
-  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
-inductive Beta
-  intros
-  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
-  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
-  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
-  b4[intro!]: "(App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
-
-lemma eqvt_beta: 
+inductive2
+  "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+intros
+  b1[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
+  b2[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
+  b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
+  b4[intro]: "(App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+
+inductive2
+  "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
+intros 
+  bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
+  bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+
+lemma beta_star_trans:
+  assumes a1: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
+  and     a2: "M2\<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+  shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+using a2 a1
+by (induct) (auto)
+
+lemma eqvt_beta:  
   fixes pi :: "name prm"
-  and   t  :: "lam"
-  and   s  :: "lam"
   assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
   shows "(pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
-  using a by (induct, auto)
+  using a 
+by (induct) (auto)
 
 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>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 a1:    "\<And>t s1 s2 x. \<lbrakk>s1\<longrightarrow>\<^isub>\<beta>s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (App s1 t) (App s2 t)"
+  and a2:    "\<And>t s1 s2 x. \<lbrakk>s1\<longrightarrow>\<^isub>\<beta>s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (App t s1) (App t s2)"
+  and a3:    "\<And>a s1 s2 x. \<lbrakk>a\<sharp>x; s1\<longrightarrow>\<^isub>\<beta>s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
   and a4:    "\<And>a t1 s1 x. a\<sharp>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)
+    case (b3 s1 s2 a)
     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)"

   thus ?thesis by simp
 qed
 
 section {* One-Reduction *}
 
-consts
-  One :: "(lam\<times>lam) set"
-syntax 
-  "_One"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
-  "_One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
-translations 
-  "t1 \<longrightarrow>\<^isub>1 t2" \<rightleftharpoons> "(t1,t2) \<in> One"
-  "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> One\<^sup>*"
-inductive One
+inductive2
+  One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
   intros
   o1[intro!]:      "M\<longrightarrow>\<^isub>1M"
   o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2;s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^isub>1(App t2 s2)"
   o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)"
   o4[simp,intro!]: "\<lbrakk>s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])"
+
+inductive2
+  "One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
+intros 
+  os1[intro, simp]: "M \<longrightarrow>\<^isub>1\<^sup>* M"
+  os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1\<^sup>* M2; M2 \<longrightarrow>\<^isub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>1\<^sup>* M3"
 
 lemma eqvt_one: 
   fixes pi :: "name prm"
   and   t  :: "lam"
   and   s  :: "lam"
   assumes a: "t\<longrightarrow>\<^isub>1s"
   shows "(pi\<bullet>t)\<longrightarrow>\<^isub>1(pi\<bullet>s)"
   using a by (induct, auto)
 
+lemma one_star_trans:
+  assumes a1: "M1\<longrightarrow>\<^isub>1\<^sup>* M2" 
+  and     a2: "M2\<longrightarrow>\<^isub>1\<^sup>* M3"
+  shows "M1\<longrightarrow>\<^isub>1\<^sup>* M3"
+using a2 a1
+by (induct) (auto)
+
 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>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> 
+  and a2:    "\<And>t1 t2 s1 s2 x. \<lbrakk>t1\<longrightarrow>\<^isub>1t2; (\<And>z. P z t1 t2); s1\<longrightarrow>\<^isub>1s2; (\<And>z. P z s1 s2)\<rbrakk> \<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 a3:    "\<And>a s1 s2 x. \<lbrakk>a\<sharp>x; s1\<longrightarrow>\<^isub>1s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
   and a4:    "\<And>a t1 t2 s1 s2 x. 
-              a\<sharp>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) 
+              \<lbrakk>a\<sharp>x; t1\<longrightarrow>\<^isub>1t2; (\<And>z. P z t1 t2); s1\<longrightarrow>\<^isub>1s2; (\<And>z. P z s1 s2)\<rbrakk> 
               \<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)
+    case (o3 t1 t2 a)
     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 (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)
+    case (o4 s1 s2 t1 t2 a)
     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 (induct)
   case o1 thus ?case by simp
 next
   case o2 thus ?case by simp
 next
-  case (o3 c s1 s2)
+  case (o3 s1 s2 c)
   have ih: "a\<sharp>s1 \<Longrightarrow>  a\<sharp>s2" by fact
   have c: "a\<sharp>Lam [c].s1" by fact
   show ?case
   proof (cases "a=c")
     assume "a=c" thus "a\<sharp>Lam [c].s2" by (simp add: abs_fresh)

     with c have "a\<sharp>s1" by (simp add: abs_fresh)
     hence "a\<sharp>s2" using ih by simp
     thus "a\<sharp>Lam [c].s2" using d by (simp add: abs_fresh) 
   qed
 next 
-  case (o4 c t1 t2 s1 s2)
+  case (o4 t1 t2 s1 s2 c)
   have i1: "a\<sharp>t1 \<Longrightarrow> a\<sharp>t2" by fact
   have i2: "a\<sharp>s1 \<Longrightarrow> a\<sharp>s2" by fact
   have as: "a\<sharp>App (Lam [c].s1) t1" by fact
   hence c1: "a\<sharp>Lam [c].s1" and c2: "a\<sharp>t1" by (simp add: fresh_prod)+
   from c2 i1 have c3: "a\<sharp>t2" by simp

 
 lemma one_abs: 
   fixes    t :: "lam"
   and      t':: "lam"
   and      a :: "name"
-  shows "(Lam [a].t)\<longrightarrow>\<^isub>1t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
-  apply(ind_cases "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
+  assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
+  shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
+  using a
+  apply -
+  apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
   apply(auto simp add: lam.distinct lam.inject alpha)
   apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   apply(rule conjI)
   apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst, symmetric])
   apply(simp)

   apply(simp add: calc_atm)
   apply(force intro!: eqvt_one)
   done
 
 lemma one_app: 
-  "App t1 t2 \<longrightarrow>\<^isub>1 t' \<Longrightarrow> 
-  (\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
-  (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
-  apply(ind_cases "App t1 s1 \<longrightarrow>\<^isub>1 t'")
+  assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
+  shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
+         (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
+  using a
+  apply -
+  apply(ind_cases2 "App t1 s1 \<longrightarrow>\<^isub>1 t'")
   apply(auto simp add: lam.distinct lam.inject)
   done
 
 lemma one_red: 
-  "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M \<Longrightarrow>
-  (\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
-  (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
-  apply(ind_cases "App (Lam [a].t1) s1 \<longrightarrow>\<^isub>1 M")
+  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M"
+  shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
+         (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
+  using a
+  apply -
+  apply(ind_cases2 "App (Lam [a].t1) s1 \<longrightarrow>\<^isub>1 M")
   apply(simp_all add: lam.inject)
   apply(force)
   apply(erule conjE)
   apply(drule sym[of "Lam [a].t1"])
   apply(simp)

   using a b
 proof (induct arbitrary: M2)
   case (o1 M) (* case 1 --- M1 = M *)
   thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and>  M2\<longrightarrow>\<^isub>1M3" by blast
 next
-  case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
+  case (o4 Q Q' P P' x) (* case 2 --- a beta-reduction occurs*)
   have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact
   hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q') \<or> 
          (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" by (simp add: one_red)

       by (force simp add: one_subst)
     hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
   }
   ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
 next
-  case (o2 Q Q' P P') (* case 3 *)
+  case (o2 P P' Q Q') (* case 3 *)
   have i0: "P\<longrightarrow>\<^isub>1P'" by fact
   have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   assume "App P Q \<longrightarrow>\<^isub>1 M2"
   hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q'') \<or> 

     have "App P' Q'\<longrightarrow>\<^isub>1R1[x::=Q'''] \<and> P1''[x::=Q'']\<longrightarrow>\<^isub>1R1[x::=Q''']" by (simp add: one_subst)
     hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
   }
   ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
 next
-  case (o3 x P P') (* case 4 *)
+  case (o3 P P' x) (* case 4 *)
   have i1: "P\<longrightarrow>\<^isub>1P'" by fact
   have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have "(Lam [x].P)\<longrightarrow>\<^isub>1 M2" by fact
   hence "\<exists>P''. M2=Lam [x].P'' \<and> P\<longrightarrow>\<^isub>1P''" by (simp add: one_abs)
   then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P\<longrightarrow>\<^isub>1P''" by blast

 lemma one_lam_cong: 
   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 simp
-next
-  case (2 y z) 
-  thus ?case by (blast dest: b3 intro: rtrancl_trans)
+  case bs1 thus ?case by simp
+next
+  case (bs2 y z) 
+  thus ?case by (blast dest: b3)
 qed
 
 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 simp
-next
-  case 2 thus ?case by (blast dest: b1 intro: rtrancl_trans)
+  case bs1 thus ?case by simp
+next
+  case bs2 thus ?case by (blast dest: b1)
 qed
   
 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 simp
+  case bs1 thus ?case by simp
 next 
-  case 2 thus ?case by (blast dest: b2 intro: rtrancl_trans)
+  case bs2 thus ?case by (blast dest: b2)
 qed
 
 lemma one_app_cong: 
   assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
-  and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" 
+  and     a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" 
   shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
 proof -
   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)
+  ultimately show ?thesis by (rule beta_star_trans)
 qed
 
 lemma one_beta_star: 
   assumes a: "(t1\<longrightarrow>\<^isub>1t2)" 
   shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"

 next
   case o2 thus ?case by (blast intro!: one_app_cong)
 next
   case o3 thus ?case by (blast intro!: one_lam_cong)
 next 
-  case (o4 a s1 s2 t1 t2)
+  case (o4 s1 s2 t1 t2 a)
   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 (blast intro!: one_app_cong one_lam_cong)
-  show ?case using c1 c2 by (blast intro: rtrancl_trans)
+  show ?case using c2 c1 by (blast intro: beta_star_trans)
 qed
  
 lemma one_star_lam_cong: 
   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 simp
-next
-  case 2 thus ?case by (blast intro: rtrancl_trans)
+  case os1 thus ?case by simp
+next
+  case os2 thus ?case by (blast intro: one_star_trans)
 qed
 
 lemma one_star_app_congL: 
   assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
   shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
   using a
 proof induct
-  case 1 thus ?case by simp
-next
-  case 2 thus ?case by (blast intro: rtrancl_trans)
+  case os1 thus ?case by simp
+next
+  case os2 thus ?case by (blast intro: one_star_trans)
 qed
 
 lemma one_star_app_congR: 
   assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
   shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
   using a
 proof induct
-  case 1 thus ?case by simp
-next
-  case 2 thus ?case by (blast intro: rtrancl_trans)
+  case os1 thus ?case by simp
+next
+  case os2 thus ?case by (blast intro: one_star_trans)
 qed
 
 lemma beta_one_star: 
   assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" 
   shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2"

 next
   case b4 thus ?case by blast
 qed
 
 lemma trans_closure: 
-  shows "(t1\<longrightarrow>\<^isub>1\<^sup>*t2) = (t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"
+  shows "(M1\<longrightarrow>\<^isub>1\<^sup>*M2) = (M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2)"
 proof
-  assume "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
-  then show "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
+  assume "M1 \<longrightarrow>\<^isub>1\<^sup>* M2"
+  then show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2"
   proof induct
-    case 1 thus ?case by simp
-  next
-    case 2 thus ?case by (force intro: rtrancl_trans simp add: one_beta_star)
-  qed
-next
-  assume "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
-  then show "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
+    case (os1 M1) thus "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M1" by simp
+  next
+    case (os2 M1 M2 M3)
+    have "M2\<longrightarrow>\<^isub>1M3" by fact
+    then have "M2\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (rule one_beta_star)
+    moreover have "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" by fact
+    ultimately show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (auto intro: beta_star_trans)
+  qed
+next
+  assume "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2" 
+  then show "M1\<longrightarrow>\<^isub>1\<^sup>*M2"
   proof induct
-    case 1 thus ?case by simp
-  next
-    case 2 thus ?case by (force intro: rtrancl_trans simp add: beta_one_star)
+    case (bs1 M1) thus  "M1\<longrightarrow>\<^isub>1\<^sup>*M1" by simp
+  next
+    case (bs2 M1 M2 M3) 
+    have "M2\<longrightarrow>\<^isub>\<beta>M3" by fact
+    then have "M2\<longrightarrow>\<^isub>1\<^sup>*M3" by (rule beta_one_star)
+    moreover have "M1\<longrightarrow>\<^isub>1\<^sup>*M2" by fact
+    ultimately show "M1\<longrightarrow>\<^isub>1\<^sup>*M3" by (auto intro: one_star_trans)
   qed
 qed
 
 lemma cr_one:
   assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t1" 
   and     b: "t\<longrightarrow>\<^isub>1t2"
   shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3"
   using a b
 proof (induct arbitrary: t2)
-  case 1 thus ?case by force
-next
-  case (2 s1 s2)
+  case os1 thus ?case by force
+next
+  case (os2 t s1 s2 t2)  
   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" 
   proof -
     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)
+    thus ?thesis using c2 by (blast intro: one_star_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"
-using a
-proof induct
-  case 1
-  show ?case using b by force
+using a b
+proof (induct arbitrary: t1)
+  case (os1 t) then show ?case by force
 next 
-  case (2 s1 s2)
+  case (os2 t s1 s2 t1)
+  have c: "t \<longrightarrow>\<^isub>1\<^sup>* s1" by fact
+  have c': "t \<longrightarrow>\<^isub>1\<^sup>* t1" by fact
   have d: "s1 \<longrightarrow>\<^isub>1 s2" by fact
-  have "\<exists>t3.  t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and>  s1 \<longrightarrow>\<^isub>1\<^sup>* t3" by fact
+  have "t \<longrightarrow>\<^isub>1\<^sup>* t1 \<Longrightarrow> (\<exists>t3.  t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> s1 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact
   then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
-                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
+                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" using c' 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 blast
-  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: rtrancl_trans)
+  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: one_star_trans)
   thus ?case using g2 by blast
 qed
   
 lemma cr_beta_star: 
   assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1"