diff -r 9253984db291 -r 660a4f5adee8 Nominal/Ex/BetaCR.thy
--- a/Nominal/Ex/BetaCR.thy	Tue Dec 20 16:12:32 2011 +0900
+++ b/Nominal/Ex/BetaCR.thy	Tue Dec 20 16:49:03 2011 +0900
@@ -52,31 +52,14 @@
 
 equivariance beta
 
-(* HERE 1 *)
 nominal_inductive beta
   avoids b3: x
+       | b4: x
   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
 
-(* This also works, but we cannot have them together: *)
-(*nominal_inductive beta
-  avoids b4: x
-  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)*)
 
-(* But I need a combination, possibly with an 'and' syntax:
-nominal_inductive beta
-  avoids b3: x and b4: x
-  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
-*)
 
 (* The combination should look like this: *)
-lemma beta_strong_induct:
-  assumes "x1 \<longrightarrow>b x2"
-  and "\<And>t1 t2 s c. \<lbrakk> t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (App t1 s) (App t2 s)"
-  and "\<And>s1 s2 t c. \<lbrakk> s1 \<longrightarrow>b s2; \<And>c. P c s1 s2\<rbrakk> \<Longrightarrow> P c (App t s1) (App t s2)"
-  and "\<And>t1 t2 x c. \<lbrakk>{atom x} \<sharp>* c;  t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (Lam [x]. t1) (Lam [x]. t2)"
-  and "\<And>x s t c. \<lbrakk>{atom x} \<sharp>* c; atom x \<sharp> s\<rbrakk> \<Longrightarrow> P c (App (Lam [x]. t) s) (t [x ::= s])"
-  shows "P (c\<Colon>'a\<Colon>fs) x1 x2"
-  sorry
 
 inductive
   beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80)
@@ -201,10 +184,7 @@
 lemma beta_subst2_pre:
   assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]"
   using assms
-(* HERE 3: nominal_induct doesn't work - leaves the assumption *)
-(*  apply (nominal_induct avoiding: x C rule: beta_strong_induct)*)
-  apply -
-  apply (erule beta_strong_induct[of A B "\<lambda>c A B. A [(fst c) ::= (snd c)] \<longrightarrow>b* B [(fst c) ::= (snd c)]" "(x, C)", simplified])
+  apply (nominal_induct avoiding: x C rule: beta.strong_induct)
   apply (auto simp add: App_beta fresh_star_def fresh_Pair Lam_beta)[3]
   apply (subst substitution_lemma)
   apply (auto simp add: fresh_star_def fresh_Pair fresh_at_base)[2]