--- a/Nominal/Ex/SingleLet.thy	Thu Sep 02 01:16:26 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Thu Sep 02 18:10:06 2010 +0800
@@ -9,7 +9,7 @@
 nominal_datatype single_let: trm  =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
+| Lam x::"name" t::"trm"  bind (set) x in t
 | Let a::"assg" t::"trm"  bind (set) "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
@@ -21,7 +21,6 @@
 where
   "bn (As x y t) = {atom x}"
 
-thm Ball_def Bex_def mem_def
 
 thm single_let.distinct
 thm single_let.induct
@@ -35,24 +34,37 @@
 thm single_let.supports
 thm single_let.fsupp
 
-
+lemma supp_abs_sum:
+  fixes a b::"'a::fs"
+  shows "supp (Abs x a) \<union> supp (Abs x b) = supp (Abs x (a, b))"
+  and   "supp (Abs_res x a) \<union> supp (Abs_res x b) = supp (Abs_res x (a, b))"
+  and   "supp (Abs_lst y a) \<union> supp (Abs_lst y b) = supp (Abs_lst y (a, b))"
+  apply (simp_all add: supp_abs supp_Pair)
+  apply blast+
+  done
 
 
-(*
 lemma test: 
-  "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
-oops
+  "(\<exists>p. (bs, x) \<approx>gen (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+sorry
 
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
   by (lifting alphas_abs)
-*)
+
+lemma test2:
+  assumes "fv_trm t = supp t" 
+  shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)"
+sorry
 
-(*
+lemma yy:
+  "X = Y \<Longrightarrow> finite X = finite Y" by simp
+
+
 lemma supp_fv:
-  "supp t = fv_trm t \<and> supp b = fv_bn b"
+  "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = {a. infinite {b. \<not>alpha_bn ((a \<rightleftharpoons> b) \<bullet> as) as}}"
 apply(rule single_let.induct)
 apply(simp_all only: single_let.fv_defs)[2]
 apply(simp_all only: supp_def)[2]
@@ -63,19 +75,115 @@
 apply(simp_all only: finite_Un)[2]
 apply(simp_all only: de_Morgan_conj)[2]
 apply(simp_all only: Collect_disj_eq)[2]
-apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)")
+--" 1 "
+apply(simp only: single_let.fv_defs)
+apply(simp add: supp_abs(1)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(simp only: single_let.perm_simps)
+apply(simp only: single_let.eq_iff)
+apply(simp only: permute_abs atom_eqvt permute_list.simps)
+apply(perm_simp)
+apply(simp only: Abs_eq_iff)
+apply(simp add: alphas)
+apply(drule test2)
+apply(simp)
+-- " 2 "
+apply(erule conjE)+
 apply(simp only: single_let.fv_defs)
-apply(simp only: supp_abs)
+apply(simp add: supp_abs(1)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(simp only: single_let.perm_simps)
+apply(simp only: single_let.eq_iff)
+apply(simp only: permute_abs atom_eqvt permute_list.simps)
+apply(perm_simp add: single_let.fv_bn_eqvt)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: Abs_eq_iff)
+apply(simp only: finite_Un)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp add: alphas)
+apply(drule test2)
 apply(simp)
+-- " 3 "
+apply(simp only: single_let.fv_defs)
+apply(simp only: supp_Pair[symmetric])
+apply(simp add: supp_abs(1)[symmetric])
 apply(simp (no_asm) only: supp_def)
 apply(simp only: single_let.perm_simps)
 apply(simp only: single_let.eq_iff)
 apply(simp only: permute_abs atom_eqvt permute_list.simps)
+apply(perm_simp add: single_let.fv_bn_eqvt)
 apply(simp only: Abs_eq_iff)
-apply(subst test)
-apply(rule refl)
-sorry
-*)
+apply(simp add: alphas)
+apply(simp add: supp_Pair)
+apply(drule test2)+
+apply(simp)
+apply(simp add: prod_alpha_def)
+apply(simp add: Un_assoc)
+apply(rule Collect_cong)
+apply(rule arg_cong)
+back
+apply(rule yy)
+apply(rule Collect_cong)
+apply(auto)[1]
+-- " Bar "
+apply(simp only: single_let.fv_defs)
+apply(simp only: supp_Pair[symmetric])
+apply(simp add: supp_abs(1)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(simp only: single_let.perm_simps)
+apply(simp only: single_let.eq_iff)
+apply(simp only: permute_abs atom_eqvt permute_list.simps)
+apply(perm_simp add: single_let.fv_bn_eqvt)
+apply(simp only: Abs_eq_iff)
+apply(simp add: alphas prod_alpha_def)
+apply(drule test2)
+apply(simp add: supp_Pair)
+apply(subst atom_eqvt)
+apply(simp)
+apply(simp add: Un_assoc)
+apply(rule Collect_cong)
+apply(rule arg_cong)
+back
+apply(rule yy)
+apply(rule Collect_cong)
+-- "last"
+prefer 3
+apply(rule conjI)
+apply(simp only: single_let.fv_defs)
+apply(perm_simp add: single_let.fv_bn_eqvt)
+apply(simp add: supp_abs(1)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(simp only: single_let.perm_simps)
+apply(simp only: single_let.eq_iff)
+apply(simp only: permute_abs atom_eqvt permute_list.simps)
+apply(perm_simp add: single_let.fv_bn_eqvt)
+apply(simp only: Abs_eq_iff)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: finite_Un)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp add: alphas prod_alpha_def)
+apply(drule test2)
+apply(simp add: supp_Pair)
+apply(simp only: permute_set_eq)
+apply(simp)
+apply(perm_simp add: single_let.fv_bn_eqvt)
+apply(simp only: single_let.eq_iff)
+apply(simp only: single_let.fv_defs)
+apply(simp add: supp_abs(1)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp)
+oops
+
+
+
+
+
+text {* *}
+
 (*
 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"