--- a/Nominal/Ex/Lambda.thy	Wed Sep 29 16:36:31 2010 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Sep 29 07:39:06 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*}
 

--- a/Nominal/Ex/Let.thy	Wed Sep 29 16:36:31 2010 +0900
+++ b/Nominal/Ex/Let.thy	Wed Sep 29 07:39:06 2010 -0400
@@ -28,6 +28,7 @@
 thm trm_assn.distinct
 thm trm_assn.supp
 thm trm_assn.fresh
+thm trm_assn.exhaust
 
 
 lemma fin_bn:
@@ -60,7 +61,7 @@
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu:
-  shows "alpha_bn (permute_bn p as) as"
+  shows "alpha_bn as (permute_bn p as)"
 apply(induct as rule: trm_assn.inducts(2))
 apply(auto)[4]
 apply(simp add: permute_bn)
@@ -78,72 +79,64 @@
 apply(simp add: atom_eqvt)
 done
 
-thm trm_assn.supp
-
-lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)"
-apply(simp add: fresh_def)
-apply(simp add: fresh_star_def)
-oops
-
-inductive
-    test_trm :: "trm \<Rightarrow> bool"
-and test_assn :: "assn \<Rightarrow> bool"
-where
-  "test_trm (Var x)"
-| "\<lbrakk>test_trm t1; test_trm t2\<rbrakk> \<Longrightarrow> test_trm (App t1 t2)"
-| "\<lbrakk>test_trm t; {atom x} \<sharp>* Lam x t\<rbrakk> \<Longrightarrow> test_trm (Lam x t)"
-| "\<lbrakk>test_assn as; test_trm t; set (bn as) \<sharp>* Let as t\<rbrakk> \<Longrightarrow> test_trm (Let as t)"
-| "test_assn ANil"
-| "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)"
-
-declare trm_assn.fv_bn_eqvt[eqvt]
-equivariance test_trm
-
-lemma 
-  fixes p::"perm"
-  shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)"
-apply(induct t and as arbitrary: p and p rule: trm_assn.inducts)
+lemma strong_exhaust1:
+  fixes c::"'a::fs"
+  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>assn trm ca. \<lbrakk>set (bn assn) \<sharp>* ca; c = ca; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in trm_assn.exhaust(1))
+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 trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(3))
+apply(perm_simp)
+apply(assumption)
+apply(rule refl)
+apply(drule supp_perm_eq[symmetric])
 apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
 apply(simp add: trm_assn.fresh fresh_star_def)
-apply(simp)
-defer
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(simp)
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
-apply(assumption)
-apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))")
-apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))")
-apply(drule_tac c="()" in at_set_avoiding2)
-apply(simp add: supp_Unit)
-prefer 2
-apply(assumption)
-apply(simp add: finite_supp)
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* c \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
-apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and
-               s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst)
-apply(rule trm_assn.eq_iff(4)[THEN iffD2])
-apply(simp add: uu)
-apply(drule supp_perm_eq)
+apply(rule assms(4))
+apply(simp add: set_eqvt)
 apply(simp add: tt)
-apply(rule test_trm_test_assn.intros(4))
-defer
-apply(subst permute_plus[symmetric])
-apply(blast)
-oops
+apply(rule refl)
+apply(simp)
+apply(simp add: trm_assn.eq_iff)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+apply(simp add: tt uu)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: Abs_fresh_star)
+done
 
 
-(* 
+lemma strong_exhaust2:
+  assumes "\<And>ca. \<lbrakk>c = ca; as = ANil\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>x t assn ca. \<lbrakk>c = ca; as = ACons x t assn\<rbrakk> \<Longrightarrow> P" 
+  shows "P"
+apply(rule_tac y="as" in trm_assn.exhaust(2))
+apply(rule assms(1))
+apply(auto)[2]
+apply(rule assms(2))
+apply(auto)[2]
+done
+
+
 lemma 
   fixes t::trm
   and   as::assn
@@ -154,7 +147,26 @@
   and     a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)"
   and     a5: "\<And>c. P2 c ANil"
   and     a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)"
-  shows "P1 c t" and "P2 c as"
+  shows "P1 c t" "P2 c as"
+using assms
+apply(induction_schema)
+apply(rule_tac y="t" in strong_exhaust1)
+apply(blast)
+apply(blast)
+apply(blast)
+apply(blast)
+apply(rule_tac as="as" in strong_exhaust2)
+apply(blast)
+apply(blast)
+apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
+apply(auto)[1]
+apply(simp_all add: trm_assn.size)[7]
+done
+
+text {* *}
+
+
+(*
 proof -
   have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" 
    and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)"