--- a/Nominal/Ex/Lambda.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Lambda.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -3,7 +3,6 @@
 begin
 
 atom_decl name
-declare [[STEPS = 100]]
 
 nominal_datatype lam =
   Var "name"
@@ -12,53 +11,27 @@
 
 thm lam.distinct
 thm lam.induct
-thm lam.exhaust
+thm lam.exhaust lam.strong_exhaust
 thm lam.fv_defs
 thm lam.bn_defs
 thm lam.perm_simps
 thm lam.eq_iff
-thm lam.eq_iff[folded alphas]
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
 
-section {* Strong Exhausts Lemma and Strong Induction Lemma via Induct_schema *}
-
-lemma strong_exhaust:
-  fixes c::"'a::fs"
-  assumes "\<And>name. \<lbrakk>y = Var name\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>lam1 lam2. \<lbrakk>y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>name lam. \<lbrakk>atom name \<sharp> c; y = Lam name lam\<rbrakk> \<Longrightarrow> P"
-  shows "P"
-apply(rule_tac y="y" in lam.exhaust)
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(3))
-apply(simp add: atom_eqvt)
-apply(clarify)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(rule at_set_avoiding2_atom)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: lam.fresh)
-done
+section {* Strong Induction Lemma via Induct_schema *}
 
 
 lemma strong_induct:
   fixes c::"'a::fs"
   assumes a1: "\<And>name c. P c (Var name)"
   and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
-  and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
+  and     a3: "\<And>name lam c. \<lbrakk>{atom name} \<sharp>* c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
   shows "P c lam"
 using assms
 apply(induction_schema)
-apply(rule_tac y="lam" in strong_exhaust)
+apply(rule_tac y="lam" in lam.strong_exhaust)
 apply(blast)
 apply(blast)
 apply(blast)
@@ -66,99 +39,6 @@
 apply(simp_all add: lam.size)
 done
 
-section {* Strong Induction Principles*}
-
-(*
-  Old way of establishing strong induction
-  principles by chosing a fresh name.
-*)
-(*
-lemma
-  fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Var name)"
-  and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
-  and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
-  shows "P c lam"
-proof -
-  have "\<And>p. P c (p \<bullet> lam)"
-    apply(induct lam arbitrary: c rule: lam.induct)
-    apply(perm_simp)
-    apply(rule a1)
-    apply(perm_simp)
-    apply(rule a2)
-    apply(assumption)
-    apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
-    defer
-    apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base)
-    apply(simp add: supp_Pair finite_supp)
-    apply(blast)
-    apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lam name lam" and 
-                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst)
-    apply(simp del: lam.perm)
-    apply(subst lam.perm)
-    apply(subst (2) lam.perm)
-    apply(rule flip_fresh_fresh)
-    apply(simp add: fresh_def)
-    apply(simp only: supp_fn')
-    apply(simp)
-    apply(simp add: fresh_Pair)
-    apply(simp)
-    apply(rule a3)
-    apply(simp add: fresh_Pair)
-    apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
-    apply(simp)
-    done
-  then have "P c (0 \<bullet> lam)" by blast
-  then show "P c lam" by simp
-qed
-*)
-(* 
-  New way of establishing strong induction
-  principles by using a appropriate permutation.
-*)
-(*
-lemma
-  fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Var name)"
-  and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
-  and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
-  shows "P c lam"
-proof -
-  have "\<And>p. P c (p \<bullet> lam)"
-    apply(induct lam arbitrary: c rule: lam.induct)
-    apply(perm_simp)
-    apply(rule a1)
-    apply(perm_simp)
-    apply(rule a2)
-    apply(assumption)
-    apply(assumption)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
-    apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lam name lam" and 
-                   s="q \<bullet> p \<bullet> Lam name lam" in subst)
-    defer
-    apply(simp)
-    apply(rule a3)
-    apply(simp add: eqvts fresh_star_def)
-    apply(drule_tac x="q + p" in meta_spec)
-    apply(simp)
-    apply(rule at_set_avoiding2)
-    apply(simp add: finite_supp)
-    apply(simp add: finite_supp)
-    apply(simp add: finite_supp)
-    apply(perm_simp)
-    apply(simp add: fresh_star_def fresh_def supp_fn')
-    apply(rule supp_perm_eq)
-    apply(simp)
-    done
-  then have "P c (0 \<bullet> lam)" by blast
-  then show "P c lam" by simp
-qed
-*)
-
 section {* Typing *}
 
 nominal_datatype ty =