--- a/Nominal/Ex/Lambda.thy	Tue Sep 28 08:21:47 2010 -0400
+++ b/Nominal/Ex/Lambda.thy	Wed Sep 29 04:42:37 2010 -0400
@@ -22,6 +22,53 @@
 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 ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>lam1 lam2 ca. \<lbrakk>c = ca; y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>name lam ca. \<lbrakk>c = ca; atom name \<sharp> ca; y = Lam name lam\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in lam.exhaust)
+apply(rule assms(1))
+apply(auto)[2]
+apply(rule assms(2))
+apply(auto)[2]
+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(rule refl)
+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
+
+
+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)"
+  shows "P c lam"
+using assms
+apply(induction_schema)
+apply(rule_tac y="lam" in strong_exhaust)
+apply(blast)
+apply(blast)
+apply(blast)
+apply(relation "measure (\<lambda>(x,y). size y)")
+apply(auto)[1]
+apply(simp add: lam.size)
+apply(simp add: lam.size)
+apply(simp add: lam.size)
+done
 
 section {* Strong Induction Principles*}