diff -r 2e174807c891 -r 11133eb76f61 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Mon Sep 27 12:19:17 2010 -0400
+++ b/Nominal/Ex/Let.thy	Tue Sep 28 05:56:11 2010 -0400
@@ -18,7 +18,7 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-
+thm at_set_avoiding2
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff 
 thm trm_assn.bn_defs
@@ -36,6 +36,54 @@
   apply(simp_all)
   done
 
+primrec
+  permute_bn_raw
+where
+  "permute_bn_raw p (ANil_raw) = ANil_raw"
+| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)"
+
+quotient_definition
+  "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
+is
+  "permute_bn_raw"
+
+lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
+  apply (rule TrueI)+
+  apply simp_all
+  apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)
+  apply simp_all
+  done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma uu:
+  shows "alpha_bn (permute_bn p as) as"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+done
+
+lemma tt:
+  shows "(p \<bullet> bn as) = bn (permute_bn p as)"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn trm_assn.bn_defs)
+apply(simp add: permute_bn trm_assn.bn_defs)
+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"
@@ -51,7 +99,6 @@
 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)"
@@ -74,23 +121,29 @@
 apply(rule test_trm_test_assn.intros)
 apply(assumption)
 apply(assumption)
-apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
+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(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(simp add: tt)
+apply(rule test_trm_test_assn.intros(4))
 defer
-apply(rule test_trm_test_assn.intros)
-prefer 3
-apply(simp add: fresh_star_def trm_assn.fresh)
-thm freshs
---"HERE"
-
-thm supps
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
-
-apply(assumption)
+apply(subst permute_plus[symmetric])
+apply(blast)
+oops
 
 
-
+(* 
 lemma 
   fixes t::trm
   and   as::assn