|
1 theory Classical |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 lemma supp_zero_perm_zero: |
|
6 shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0" |
|
7 by (metis supp_perm_singleton supp_zero_perm) |
|
8 |
|
9 lemma permute_atom_list_id: |
|
10 shows "p \<bullet> l = l \<longleftrightarrow> supp p \<inter> set l = {}" |
|
11 by (induct l) (auto simp add: supp_Nil supp_perm) |
|
12 |
|
13 lemma permute_length_eq: |
|
14 shows "p \<bullet> xs = ys \<Longrightarrow> length xs = length ys" |
|
15 by (auto simp add: length_eqvt[symmetric] permute_pure) |
|
16 |
|
17 lemma Abs_lst_binder_length: |
|
18 shows "[xs]lst. T = [ys]lst. S \<Longrightarrow> length xs = length ys" |
|
19 by (auto simp add: Abs_eq_iff alphas length_eqvt[symmetric] permute_pure) |
|
20 |
|
21 lemma Abs_lst_binder_eq: |
|
22 shows "Abs_lst l T = Abs_lst l S \<longleftrightarrow> T = S" |
|
23 by (rule, simp_all add: Abs_eq_iff2 alphas) |
|
24 (metis fresh_star_zero inf_absorb1 permute_atom_list_id supp_perm_eq |
|
25 supp_zero_perm_zero) |
|
26 |
|
27 lemma in_permute_list: |
|
28 shows "py \<bullet> p \<bullet> xs = px \<bullet> xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> py \<bullet> p \<bullet> x = px \<bullet> x" |
|
29 by (induct xs) auto |
|
30 |
|
31 lemma obtain_atom_list: |
|
32 assumes eq: "p \<bullet> xs = ys" |
|
33 and fin: "finite (supp c)" |
|
34 and sorts: "map sort_of xs = map sort_of ys" |
|
35 shows "\<exists>ds px py. (set ds \<sharp>* c) \<and> (px \<bullet> xs = ds) \<and> (py \<bullet> ys = ds) |
|
36 \<and> (supp px - set xs) \<sharp>* c \<and> (supp py - set ys) \<sharp>* c" |
|
37 sorry |
|
38 |
|
39 lemma Abs_lst_fcb2: |
|
40 fixes S T :: "'b :: fs" |
|
41 and c::"'c::fs" |
|
42 assumes e: "[xs]lst. T = [ys]lst. S" |
|
43 and sorts: "map sort_of xs = map sort_of ys" |
|
44 and fcb1: "\<And>x. x \<in> set xs \<Longrightarrow> x \<sharp> f xs T c" |
|
45 and fcb2: "\<And>x. x \<in> set ys \<Longrightarrow> x \<sharp> f ys S c" |
|
46 and fresh: "(set xs \<union> set ys) \<sharp>* c" |
|
47 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f xs T c) = f (p \<bullet> xs) (p \<bullet> T) c" |
|
48 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f ys S c) = f (p \<bullet> ys) (p \<bullet> S) c" |
|
49 shows "f xs T c = f ys S c" |
|
50 proof - |
|
51 have fin1: "finite (supp (f xs T c))" |
|
52 apply(rule_tac S="supp (xs, T, c)" in supports_finite) |
|
53 apply(simp add: supports_def) |
|
54 apply(simp add: fresh_def[symmetric]) |
|
55 apply(clarify) |
|
56 apply(subst perm1) |
|
57 apply(simp add: supp_swap fresh_star_def) |
|
58 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
59 apply(simp add: finite_supp) |
|
60 done |
|
61 have fin2: "finite (supp (f ys S c))" |
|
62 apply(rule_tac S="supp (ys, S, c)" in supports_finite) |
|
63 apply(simp add: supports_def) |
|
64 apply(simp add: fresh_def[symmetric]) |
|
65 apply(clarify) |
|
66 apply(subst perm2) |
|
67 apply(simp add: supp_swap fresh_star_def) |
|
68 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
69 apply(simp add: finite_supp) |
|
70 done |
|
71 obtain p :: perm where xs_ys: "p \<bullet> xs = ys" using e |
|
72 by (auto simp add: Abs_eq_iff alphas) |
|
73 obtain ds::"atom list" and px and py |
|
74 where fr: "set ds \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)" |
|
75 and pxd: "px \<bullet> xs = ds" and pyd: "py \<bullet> ys = ds" |
|
76 and spx: "(supp px - set xs) \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)" |
|
77 and spy: "(supp py - set ys) \<sharp>* (xs, ys, S, T, c, f xs T c, f ys S c)" |
|
78 using obtain_atom_list[OF xs_ys, of "(xs, ys, S, T, c, f xs T c, f ys S c)"] |
|
79 sorts by (auto simp add: finite_supp supp_Pair fin1 fin2) |
|
80 have "px \<bullet> (Abs_lst xs T) = py \<bullet> (Abs_lst ys S)" |
|
81 apply (subst perm_supp_eq) |
|
82 using spx apply (auto simp add: fresh_star_def Abs_fresh_iff)[1] |
|
83 apply (subst perm_supp_eq) |
|
84 using spy apply (auto simp add: fresh_star_def Abs_fresh_iff)[1] |
|
85 by(rule e) |
|
86 then have "Abs_lst ds (px \<bullet> T) = Abs_lst ds (py \<bullet> S)" by (simp add: pxd pyd) |
|
87 then have eq: "px \<bullet> T = py \<bullet> S" by (simp add: Abs_lst_binder_eq) |
|
88 have "f xs T c = px \<bullet> f xs T c" |
|
89 apply(rule perm_supp_eq[symmetric]) |
|
90 using spx unfolding fresh_star_def |
|
91 apply (intro ballI) |
|
92 by (case_tac "a \<in> set xs") (simp_all add: fcb1) |
|
93 also have "... = f (px \<bullet> xs) (px \<bullet> T) c" |
|
94 apply(rule perm1) |
|
95 using spx fresh unfolding fresh_star_def |
|
96 apply (intro ballI) |
|
97 by (case_tac "a \<in> set xs") (simp_all add: fcb1) |
|
98 also have "... = f (py \<bullet> ys) (py \<bullet> S) c" using eq pxd pyd by simp |
|
99 also have "... = py \<bullet> f ys S c" |
|
100 apply(rule perm2[symmetric]) |
|
101 using spy fresh unfolding fresh_star_def |
|
102 apply (intro ballI) |
|
103 by (case_tac "a \<in> set ys") (simp_all add: fcb1) |
|
104 also have "... = f ys S c" |
|
105 apply(rule perm_supp_eq) |
|
106 using spy unfolding fresh_star_def |
|
107 apply (intro ballI) |
|
108 by (case_tac "a \<in> set ys") (simp_all add: fcb2) |
|
109 finally show ?thesis by simp |
|
110 qed |
|
111 |
|
112 end |
|
113 |
|
114 |
|
115 |