--- a/Nominal/Ex/Classical_Test.thy	Tue Jun 28 12:36:34 2011 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-theory Classical
-imports "../Nominal2"
-begin
-
-lemma supp_zero_perm_zero:
-  shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0"
-  by (metis supp_perm_singleton supp_zero_perm)
-
-lemma permute_atom_list_id:
-  shows "p \<bullet> l = l \<longleftrightarrow> supp p \<inter> set l = {}"
-  by (induct l) (auto simp add: supp_Nil supp_perm)
-
-lemma permute_length_eq:
-  shows "p \<bullet> xs = ys \<Longrightarrow> length xs = length ys"
-  by (auto simp add: length_eqvt[symmetric] permute_pure)
-
-lemma Abs_lst_binder_length:
-  shows "[xs]lst. T = [ys]lst. S \<Longrightarrow> length xs = length ys"
-  by (auto simp add: Abs_eq_iff alphas length_eqvt[symmetric] permute_pure)
-
-lemma Abs_lst_binder_eq:
-  shows "Abs_lst l T = Abs_lst l S \<longleftrightarrow> T = S"
-  by (rule, simp_all add: Abs_eq_iff2 alphas)
-     (metis fresh_star_zero inf_absorb1 permute_atom_list_id supp_perm_eq
-       supp_zero_perm_zero)
-
-lemma in_permute_list:
-  shows "py \<bullet> p \<bullet> xs = px \<bullet> xs \<Longrightarrow>  x \<in> set xs \<Longrightarrow> py \<bullet> p \<bullet> x = px \<bullet> x"
-  by (induct xs) auto
-
-lemma obtain_atom_list:
-  assumes eq: "p \<bullet> xs = ys"
-      and fin: "finite (supp c)"
-      and sorts: "map sort_of xs = map sort_of ys"
-  shows "\<exists>ds px py. (set ds \<sharp>* c) \<and> (px \<bullet> xs = ds) \<and> (py \<bullet> ys = ds)
-    \<and> (supp px - set xs) \<sharp>* c \<and> (supp py - set ys) \<sharp>* c"
-  sorry
-
-lemma Abs_lst_fcb2:
-  fixes S T :: "'b :: fs"
-    and c::"'c::fs"
-  assumes e: "[xs]lst. T = [ys]lst. S"
-  and sorts: "map sort_of xs = map sort_of ys"
-  and fcb1: "\<And>x. x \<in> set xs \<Longrightarrow> x \<sharp> f xs T c"
-  and fcb2: "\<And>x. x \<in> set ys \<Longrightarrow> x \<sharp> f ys S c"
-  and fresh: "(set xs \<union> set ys) \<sharp>* c"
-  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f xs T c) = f (p \<bullet> xs) (p \<bullet> T) c"
-  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f ys S c) = f (p \<bullet> ys) (p \<bullet> S) c"
-  shows "f xs T c = f ys S c"
-proof -
-  have fin1: "finite (supp (f xs T c))"
-    apply(rule_tac S="supp (xs, T, c)" in supports_finite)
-    apply(simp add: supports_def)
-    apply(simp add: fresh_def[symmetric])
-    apply(clarify)
-    apply(subst perm1)
-    apply(simp add: supp_swap fresh_star_def)
-    apply(simp add: swap_fresh_fresh fresh_Pair)
-    apply(simp add: finite_supp)
-    done
-  have fin2: "finite (supp (f ys S c))"
-    apply(rule_tac S="supp (ys, S, c)" in supports_finite)
-    apply(simp add: supports_def)
-    apply(simp add: fresh_def[symmetric])
-    apply(clarify)
-    apply(subst perm2)
-    apply(simp add: supp_swap fresh_star_def)
-    apply(simp add: swap_fresh_fresh fresh_Pair)
-    apply(simp add: finite_supp)
-    done
-  obtain p :: perm where xs_ys: "p \<bullet> xs = ys" using e
-    by (auto simp add: Abs_eq_iff alphas)
-  obtain ds::"atom list" and px and py
-    where fr: "set ds \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)"
-    and pxd: "px \<bullet> xs = ds"     and pyd: "py \<bullet> ys = ds"
-    and spx: "(supp px - set xs) \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)"
-    and spy: "(supp py - set ys) \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)"
-    using obtain_atom_list[OF xs_ys, of "(xs, ys, S, T, c, f xs T c, f ys S c)"]
-    sorts by (auto simp add: finite_supp supp_Pair fin1 fin2)
-  have "px \<bullet> (Abs_lst xs T) = py \<bullet> (Abs_lst ys S)"
-    apply (subst perm_supp_eq)
-    using spx apply (auto simp add: fresh_star_def Abs_fresh_iff)[1]
-    apply (subst perm_supp_eq)
-    using spy apply (auto simp add: fresh_star_def Abs_fresh_iff)[1]
-    by(rule e)
-  then have "Abs_lst ds (px \<bullet> T) = Abs_lst ds (py \<bullet> S)" by (simp add: pxd pyd)
-  then have eq: "px \<bullet> T = py \<bullet> S" by (simp add: Abs_lst_binder_eq)
-  have "f xs T c = px \<bullet> f xs T c"
-    apply(rule perm_supp_eq[symmetric])
-    using spx unfolding fresh_star_def
-    apply (intro ballI)
-    by (case_tac "a \<in> set xs") (simp_all add: fcb1)
-  also have "... = f (px \<bullet> xs) (px \<bullet> T) c"
-    apply(rule perm1)
-    using spx fresh unfolding fresh_star_def
-    apply (intro ballI)
-    by (case_tac "a \<in> set xs") (simp_all add: fcb1)
-  also have "... = f (py \<bullet> ys) (py \<bullet> S) c" using eq pxd pyd by simp
-  also have "... = py \<bullet> f ys S c"
-    apply(rule perm2[symmetric])
-    using spy fresh unfolding fresh_star_def
-    apply (intro ballI)
-    by (case_tac "a \<in> set ys") (simp_all add: fcb1)
-  also have "... = f ys S c"
-    apply(rule perm_supp_eq)
-    using spy unfolding fresh_star_def
-    apply (intro ballI)
-    by (case_tac "a \<in> set ys") (simp_all add: fcb2)
-  finally show ?thesis by simp
-qed
-
-end
-
-
-