--- a/Nominal/Test.thy	Thu Mar 18 15:32:49 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 16:22:10 2010 +0100
@@ -62,7 +62,7 @@
   fixes c::"'a::fs"
   assumes a1: "\<And>name c. P c (Vr name)"
   and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
   shows "P c lm"
 proof -
   have "\<And>p. P c (p \<bullet> lm)"
@@ -87,6 +87,7 @@
     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)
     apply(simp add: fresh_def)
@@ -99,6 +100,38 @@
 qed
 
 
+lemma
+  fixes c::"'a::fs"
+  assumes a1: "\<And>name c. P c (Vr name)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+  shows "P c lm"
+proof -
+  have "\<And>p. P c (p \<bullet> lm)"
+    apply(induct lm arbitrary: c rule: lm_induct)
+    apply(simp only: lm_perm)
+    apply(rule a1)
+    apply(simp only: lm_perm)
+    apply(rule a2)
+    apply(blast)[1]
+    apply(assumption)
+    thm at_set_avoiding
+    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
+    apply(erule exE)
+    apply(rule_tac t="p \<bullet> Lm name lm" and 
+                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
+    defer
+    apply(simp add: lm_perm)
+    apply(rule a3)
+    apply(simp add: eqvts fresh_star_def)
+    apply(drule_tac x="q + p" in meta_spec)
+    apply(simp)
+    sorry
+  then have "P c (0 \<bullet> lm)" by blast
+  then show "P c lm" by simp
+qed
+
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -418,14 +451,6 @@
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
 
-lemma supports_subset:
-  fixes S1 S2 :: "atom set"
-  assumes  a: "S1 supports x"
-  and      b: "S1 \<subseteq> S2"
-  shows "S2 supports x"
-  using a b
-  by (auto simp add: supports_def)
-
 lemma finite_fv_t_tyS:
   fixes T::"t"
   and   S::"tyS"
@@ -473,6 +498,10 @@
 
 (* example 1 from Terms.thy *)
 
+
+  
+
+
 nominal_datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"