# HG changeset patch
# User urbanc
# Date 1133694843 -3600
# Node ID 95083a68cbbb2046c008102604e81ce10bd78311
# Parent  e36238ac5359896dad9c771c0a15dc6c7ce12e1f
tuning

diff -r e36238ac5359 -r 95083a68cbbb src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Fri Dec 02 22:57:36 2005 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Sun Dec 04 12:14:03 2005 +0100
@@ -32,9 +32,8 @@
   assumes a: "a\<sharp>t1"
   shows "t1[a::=t2] = t1"
   using a
-apply (nominal_induct t1 avoiding: a t2 rule: lam_induct)
-apply(auto simp add: abs_fresh fresh_atm)
-done
+  by (nominal_induct t1 avoiding: a t2 rule: lam_induct)
+     (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
   fixes   b :: "name"
@@ -63,17 +62,14 @@
 qed
 
 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])"
 using a b
-apply(nominal_induct t1 avoiding: a b t2 rule: lam_induct)
-apply(auto simp add: abs_fresh fresh_atm)
-done
+by (nominal_induct t1 avoiding: a b t2 rule: lam_induct)
+   (auto simp add: abs_fresh fresh_atm)
+
 
 lemma subs_lemma:  
   fixes x::"name"
@@ -147,27 +143,29 @@
 by (nominal_induct M avoiding: x y N L rule: lam_induct)
    (auto simp add: fresh_fact forget)
 
-lemma subst_rename[rule_format]: 
+lemma subst_rename: 
   fixes  c  :: "name"
   and    a  :: "name"
   and    t1 :: "lam"
   and    t2 :: "lam"
-  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
+  assumes a: "c\<sharp>t1"
+  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
+using a
 proof (nominal_induct t1 avoiding: 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)
+  thus "(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
 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 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 (simp add: abs_fresh)
-    hence d: "s[a::=t2] = ([(c,a)]\<bullet>s)[c::=t2]" using i by simp
+  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")
+  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
@@ -176,12 +174,14 @@
   qed
 qed
 
-lemma subst_rename[rule_format]: 
+lemma subst_rename: 
   fixes  c  :: "name"
   and    a  :: "name"
   and    t1 :: "lam"
   and    t2 :: "lam"
-  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
+  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
@@ -551,7 +551,7 @@
   qed
 qed
 
-lemma one_subst[rule_format]: 
+lemma one_subst: 
   assumes a: "M\<longrightarrow>\<^isub>1M'" 
   and     b: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
@@ -560,131 +560,117 @@
 apply(auto simp add: one_subst_aux subs_lemma fresh_atm)
 done
 
-(* FIXME: change to make use of the new induction facilities *)
 lemma diamond[rule_format]:
   fixes    M :: "lam"
   and      M1:: "lam"
   assumes a: "M\<longrightarrow>\<^isub>1M1" 
-  shows "\<forall>M2. (M\<longrightarrow>\<^isub>1M2) \<longrightarrow> (\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  using a
-proof (induct)
+  and     b: "M\<longrightarrow>\<^isub>1M2"
+  shows "\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3"
+  using a b
+proof (induct fixing: M2)
   case (o1 M) (* case 1 --- M1 = M *)
-  show "\<forall>M2. M\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and>  M2\<longrightarrow>\<^isub>1M3)" by force
+  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*)
-  assume i1: "\<forall>M2. Q \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  assume i2: "\<forall>M2. P \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  show "\<forall>M2. App (Lam [x].P) Q\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  proof (intro strip)
-    fix M2
-    assume "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2"
-    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)
-    moreover (* subcase 2.1 *)
-    { assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
-      then obtain P'' and Q'' where 
-	b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by force
-      from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain P''' where
-	c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
-      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain Q''' where
-	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
-      from c1 c2 d1 d2 
-      have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^isub>1 P'''[x::=Q''']" 
-	by (force simp add: one_subst)
-      hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by force
-    }
-    moreover (* subcase 2.2 *)
-    { assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
-      then obtain P'' Q'' where
-	b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^isub>1P''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" by force
-      from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain P''' where
-	c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
-      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain Q''' where
-	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
-      from c1 c2 d1 d2 
-      have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^isub>1P'''[x::=Q''']" 
-	by (force simp add: one_subst)
-      hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by force
-    }
-    ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
-  qed
+  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)
+  moreover (* subcase 2.1 *)
+  { assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
+    then obtain P'' and Q'' where 
+      b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast
+    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+    then obtain P''' where
+      c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
+    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+    then obtain Q''' where
+      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
+    from c1 c2 d1 d2 
+    have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^isub>1 P'''[x::=Q''']" 
+      by (force simp add: one_subst)
+    hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
+  }
+  moreover (* subcase 2.2 *)
+  { assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
+    then obtain P'' Q'' where
+      b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^isub>1P''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" by blast
+    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+    then obtain P''' where
+      c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast
+    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+    then obtain Q''' where
+      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast
+    from c1 c2 d1 d2 
+    have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^isub>1P'''[x::=Q''']" 
+      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 *)
-  assume i0: "P\<longrightarrow>\<^isub>1P'"
-  assume i1: "\<forall>M2. Q \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  assume i2: "\<forall>M2. P \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  show "\<forall>M2. App P Q\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  proof (intro strip)
-    fix M2
-    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> 
-           (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q')" 
-      by (simp add: one_app[simplified])
-    moreover (* subcase 3.1 *)
-    { assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
-      then obtain P'' and Q'' where 
-	b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by force
-      from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain P''' where
-	c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
-      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain Q''' where
-	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
-      from c1 c2 d1 d2 
-      have "App P' Q'\<longrightarrow>\<^isub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^isub>1 App P''' Q'''" by force
-      hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by force
-    }
-    moreover (* subcase 3.2 *)
-    { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
-      then obtain x P1 P1'' Q'' where
-	b0: "P=Lam [x].P1" and b1: "M2=P1''[x::=Q'']" and 
-        b2: "P1\<longrightarrow>\<^isub>1P1''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" by force
-      from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)
-      then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by force 
-      from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain P1''' where
-	c1: "(Lam [x].P1')\<longrightarrow>\<^isub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^isub>1P1'''" by force
-      from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
-      then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^isub>1R1" by force
-      from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
-      then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^isub>1R2" by force
-      from r1 r3 have r5: "R1=R2" 
-	by (simp add: lam.inject alpha)
-      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
-      then obtain Q''' where
-	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
-      from g1 r2 d1 r4 r5 d2 
-      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 force
-    }
-    ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
-  qed
+  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> 
+         (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q')" 
+    by (simp add: one_app[simplified])
+  moreover (* subcase 3.1 *)
+  { assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+    then obtain P'' and Q'' where 
+      b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast
+    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+    then obtain P''' where
+      c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast
+    from b3 i1 have "\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3" by simp
+    then obtain Q''' where
+      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast
+    from c1 c2 d1 d2 
+    have "App P' Q'\<longrightarrow>\<^isub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^isub>1 App P''' Q'''" by blast
+    hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
+  }
+  moreover (* subcase 3.2 *)
+  { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+    then obtain x P1 P1'' Q'' where
+      b0: "P=Lam [x].P1" and b1: "M2=P1''[x::=Q'']" and 
+      b2: "P1\<longrightarrow>\<^isub>1P1''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" by blast
+    from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)
+    then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by blast 
+    from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp
+    then obtain P1''' where
+      c1: "(Lam [x].P1')\<longrightarrow>\<^isub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^isub>1P1'''" by blast
+    from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
+    then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^isub>1R1" by blast
+    from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
+    then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^isub>1R2" by blast
+    from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha)
+    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+    then obtain Q''' where
+      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast
+    from g1 r2 d1 r4 r5 d2 
+    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 *)
-  assume i1: "P\<longrightarrow>\<^isub>1P'"
-  assume i2: "\<forall>M2. P \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  show "\<forall>M2. (Lam [x].P)\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
-  proof (intro strip)
-    fix M2
-    assume "(Lam [x].P)\<longrightarrow>\<^isub>1 M2"
-    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 force
-    from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1M3" by force
-    then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^isub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^isub>1M3" by force
-    from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
-    then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^isub>1R1" by force
-    from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
-    then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^isub>1R2" by force
-    from r1 r3 have r5: "R1=R2" 
-      by (simp add: lam.inject alpha)
-    from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^isub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1(Lam [x].R2)" 
-      by (simp add: one_subst)
-    thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 r5 by force
-  qed
+  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
+  from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast
+  then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^isub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast
+  from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
+  then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^isub>1R1" by blast
+  from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
+  then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^isub>1R2" by blast
+  from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha)
+  from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^isub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1(Lam [x].R2)" 
+    by (simp add: one_subst)
+  thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 r5 by blast
 qed
 
 lemma one_abs_cong: 
@@ -726,7 +712,7 @@
 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 and b2 by (force intro: rtrancl_trans)
+  show ?thesis using b1 b2 by (force intro: rtrancl_trans)
 qed
 
 lemma one_beta_star: 
@@ -815,35 +801,25 @@
 
 lemma cr_one:
   assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t1" 
-  and b: "t\<longrightarrow>\<^isub>1t2"
+  and     b: "t\<longrightarrow>\<^isub>1t2"
   shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3"
-proof -
-  have stronger: "\<forall>t2. t\<longrightarrow>\<^isub>1t2\<longrightarrow>(\<exists>t3. t1\<longrightarrow>\<^isub>1t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3)"
-    using a 
-  proof induct
-    case 1 show ?case by (force)
-  next
-    case (2 s1 s2)
-    assume b: "s1 \<longrightarrow>\<^isub>1 s2"
-    assume h: "\<forall>t2. t \<longrightarrow>\<^isub>1 t2 \<longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)"
-    show ?case
-    proof (rule allI, rule impI)
-      fix t2
-      assume  c: "t \<longrightarrow>\<^isub>1 t2"
-      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)
-      qed
-    qed
+  using a b
+proof (induct fixing: t2)
+  case 1 thus ?case by force
+next
+  case (2 s1 s2)
+  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 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)
   qed
-  from a b stronger show ?thesis by force
 qed
 
-
 lemma cr_one_star: 
   assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2"
       and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1"