diff -r 8fbc7d38d6cf -r 7711d60a5293 src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Fri Jan 04 09:34:11 2008 +0100
@@ -265,66 +265,29 @@
    (auto simp add: calc_atm fresh_atm abs_fresh)
 
 lemma one_abs: 
-  fixes    t :: "lam"
-  and      t':: "lam"
-  and      a :: "name"
-  assumes a: "(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_cases "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
-  apply(auto simp add: lam.inject alpha)
-  apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
-  apply(rule conjI)
-  apply(perm_simp)
-  apply(simp add: fresh_left calc_atm)
-  apply(simp add: One.eqvt)
-  apply(simp add: one_fresh_preserv)
-done  
-
+proof -
+  have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
+  with a have "a\<sharp>t'" by (simp add: one_fresh_preserv)
+  with a show ?thesis
+    by (cases rule: One.strong_cases[where a="a" and aa="a"])
+       (auto simp add: lam.inject abs_fresh alpha)
+qed
 
 lemma one_app: 
   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> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
-  using a
-  apply -
-  apply(ind_cases "App t1 t2 \<longrightarrow>\<^isub>1 t'")
-  apply(auto simp add: lam.distinct lam.inject)
-  done
+         (\<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 \<and> a\<sharp>(t2,s2))"
+using a by (erule_tac One.cases) (auto simp add: lam.inject)
 
 lemma one_red: 
-  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M"
+  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M" "a\<sharp>(t2,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_cases "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
-  apply(simp_all add: lam.inject)
-  apply(force)
-  apply(erule conjE)
-  apply(drule sym[of "Lam [a].t1"])
-  apply(simp)
-  apply(drule one_abs)
-  apply(erule exE)
-  apply(simp)
-  apply(force simp add: alpha)
-  apply(erule conjE)
-  apply(simp add: lam.inject alpha)
-  apply(erule disjE)
-  apply(simp)
-  apply(force)
-  apply(simp)
-  apply(rule disjI2)
-  apply(rule_tac x="[(a,aa)]\<bullet>t2a" in exI)
-  apply(rule_tac x="s2" in exI)
-  apply(auto)
-  apply(subgoal_tac "a\<sharp>t2a")(*A*)
-  apply(simp add: subst_rename)
-  (*A*)
-  apply(force intro: one_fresh_preserv)
-  apply(force intro: One.eqvt)
-  done
+using a
+by (cases rule: One.strong_cases [where a="a" and aa="a"])
+   (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod)
 
 text {* first case in Lemma 3.2.4*}
 
@@ -347,9 +310,8 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-apply(nominal_induct M avoiding: x N N' rule: lam.induct)
-apply(auto simp add: fresh_prod fresh_atm)
-done
+by (nominal_induct M avoiding: x N N' rule: lam.induct)
+   (auto simp add: fresh_prod fresh_atm)
 
 lemma one_subst: 
   assumes a: "M\<longrightarrow>\<^isub>1M'"
@@ -385,9 +347,8 @@
   and     b: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
 using a b
-apply(nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
-apply(auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
-done
+by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
+   (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
 
 lemma diamond[rule_format]:
   fixes    M :: "lam"
@@ -401,12 +362,12 @@
   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*)
-  have vc: "x\<sharp>Q" "x\<sharp>Q'" by fact+
+  have vc: "x\<sharp>Q" "x\<sharp>Q'" "x\<sharp>M2" 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
   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)
+         (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" using vc 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 
@@ -446,7 +407,7 @@
   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> x\<sharp>(Q,Q') \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q')" 
+         (\<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' \<and> x\<sharp>(Q,Q'))" 
     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''"
@@ -463,11 +424,11 @@
     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> x\<sharp>(Q,Q'') \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+  { 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'' \<and> x\<sharp>(Q,Q'')"
     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''" and vc: "x\<sharp>(Q,Q'')" by blast
-    from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)
+    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