diff -r e26c6c728b9e -r 9448945a1e60 Nominal/Ex/Classical_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/Classical_Test.thy Mon Jun 27 08:38:54 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 + + +