--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Classical_Test.thy	Mon Jun 27 08:42:02 2011 +0900
@@ -0,0 +1,115 @@
+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
+
+
+