44 thm trm.fv_bn_eqvt |
44 thm trm.fv_bn_eqvt |
45 thm trm.size_eqvt |
45 thm trm.size_eqvt |
46 thm trm.supp |
46 thm trm.supp |
47 thm trm.supp[simplified] |
47 thm trm.supp[simplified] |
48 |
48 |
49 lemma Abs_lst1_fcb2: |
|
50 fixes a b :: "'a :: at" |
|
51 and S T :: "'b :: fs" |
|
52 and c::"'c::fs" |
|
53 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
|
54 and fcb1: "atom a \<sharp> f a T c" |
|
55 and fresh: "{atom a, atom b} \<sharp>* c" |
|
56 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c" |
|
57 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c" |
|
58 shows "f a T c = f b S c" |
|
59 proof - |
|
60 have fcb2: "atom b \<sharp> f b S c" |
|
61 using e[symmetric] |
|
62 apply(simp add: Abs_eq_iff2) |
|
63 apply(erule exE) |
|
64 apply(simp add: alphas) |
|
65 apply(rule_tac p="p" in permute_boolE) |
|
66 apply(simp add: fresh_eqvt) |
|
67 apply(subst perm2) |
|
68 using fresh |
|
69 apply(auto simp add: fresh_star_def)[1] |
|
70 apply(simp add: atom_eqvt) |
|
71 apply(rule fcb1) |
|
72 done |
|
73 have fin1: "finite (supp (f a T c))" |
|
74 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
|
75 apply(simp add: supports_def) |
|
76 apply(simp add: fresh_def[symmetric]) |
|
77 apply(clarify) |
|
78 apply(subst perm1) |
|
79 apply(simp add: supp_swap fresh_star_def) |
|
80 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
81 apply(simp add: finite_supp) |
|
82 done |
|
83 have fin2: "finite (supp (f b S c))" |
|
84 apply(rule_tac S="supp (b, S, c)" in supports_finite) |
|
85 apply(simp add: supports_def) |
|
86 apply(simp add: fresh_def[symmetric]) |
|
87 apply(clarify) |
|
88 apply(subst perm2) |
|
89 apply(simp add: supp_swap fresh_star_def) |
|
90 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
91 apply(simp add: finite_supp) |
|
92 done |
|
93 obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" |
|
94 using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"] |
|
95 apply(auto simp add: finite_supp supp_Pair fin1 fin2) |
|
96 done |
|
97 have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" |
|
98 apply(simp (no_asm_use) only: flip_def) |
|
99 apply(subst swap_fresh_fresh) |
|
100 apply(simp add: Abs_fresh_iff) |
|
101 using fr |
|
102 apply(simp add: Abs_fresh_iff) |
|
103 apply(subst swap_fresh_fresh) |
|
104 apply(simp add: Abs_fresh_iff) |
|
105 using fr |
|
106 apply(simp add: Abs_fresh_iff) |
|
107 apply(rule e) |
|
108 done |
|
109 then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)" |
|
110 apply (simp add: swap_atom flip_def) |
|
111 done |
|
112 then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S" |
|
113 by (simp add: Abs1_eq_iff) |
|
114 have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c" |
|
115 unfolding flip_def |
|
116 apply(rule sym) |
|
117 apply(rule swap_fresh_fresh) |
|
118 using fcb1 |
|
119 apply(simp) |
|
120 using fr |
|
121 apply(simp add: fresh_Pair) |
|
122 done |
|
123 also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c" |
|
124 unfolding flip_def |
|
125 apply(subst perm1) |
|
126 using fresh fr |
|
127 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
128 apply(simp) |
|
129 done |
|
130 also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp |
|
131 also have "... = (b \<leftrightarrow> d) \<bullet> f b S c" |
|
132 unfolding flip_def |
|
133 apply(subst perm2) |
|
134 using fresh fr |
|
135 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
136 apply(simp) |
|
137 done |
|
138 also have "... = f b S c" |
|
139 apply(rule flip_fresh_fresh) |
|
140 using fcb2 |
|
141 apply(simp) |
|
142 using fr |
|
143 apply(simp add: fresh_Pair) |
|
144 done |
|
145 finally show ?thesis by simp |
|
146 qed |
|
147 |
|
148 lemma Abs_lst_fcb2: |
49 lemma Abs_lst_fcb2: |
149 fixes as bs :: "atom list" |
50 fixes as bs :: "atom list" |
150 and x y :: "'b :: fs" |
51 and x y :: "'b :: fs" |
151 and c::"'c::fs" |
52 and c::"'c::fs" |
152 assumes e: "(Abs_lst as x) = (Abs_lst bs y)" |
53 assumes eq: "[as]lst. x = [bs]lst. y" |
153 and fcb1: "(set as) \<sharp>* f as x c" |
54 and fcb1: "(set as) \<sharp>* f as x c" |
154 and fcb2: "(set bs) \<sharp>* f bs y c" |
|
155 and fresh1: "set as \<sharp>* c" |
55 and fresh1: "set as \<sharp>* c" |
156 and fresh2: "set bs \<sharp>* c" |
56 and fresh2: "set bs \<sharp>* c" |
157 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
57 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
158 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
58 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
159 shows "f as x c = f bs y c" |
59 shows "f as x c = f bs y c" |
160 proof - |
60 proof - |
161 have fin1: "finite (supp (f as x c))" |
61 have "supp (as, x, c) supports (f as x c)" |
162 apply(rule_tac S="supp (as, x, c)" in supports_finite) |
62 unfolding supports_def fresh_def[symmetric] |
163 apply(simp add: supports_def) |
63 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
164 apply(simp add: fresh_def[symmetric]) |
64 then have fin1: "finite (supp (f as x c))" |
165 apply(clarify) |
65 by (auto intro: supports_finite simp add: finite_supp) |
166 apply(subst perm1) |
66 have "supp (bs, y, c) supports (f bs y c)" |
167 apply(simp add: supp_swap fresh_star_def) |
67 unfolding supports_def fresh_def[symmetric] |
168 apply(simp add: swap_fresh_fresh fresh_Pair) |
68 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
169 apply(simp add: finite_supp) |
69 then have fin2: "finite (supp (f bs y c))" |
170 done |
70 by (auto intro: supports_finite simp add: finite_supp) |
171 have fin2: "finite (supp (f bs y c))" |
|
172 apply(rule_tac S="supp (bs, y, c)" in supports_finite) |
|
173 apply(simp add: supports_def) |
|
174 apply(simp add: fresh_def[symmetric]) |
|
175 apply(clarify) |
|
176 apply(subst perm2) |
|
177 apply(simp add: supp_swap fresh_star_def) |
|
178 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
179 apply(simp add: finite_supp) |
|
180 done |
|
181 obtain q::"perm" where |
71 obtain q::"perm" where |
182 fr1: "(q \<bullet> (set as)) \<sharp>* (as, bs, x, y, c, f as x c, f bs y c)" and |
72 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
183 fr2: "supp q \<sharp>* Abs_lst as x" and |
73 fr2: "supp q \<sharp>* Abs_lst as x" and |
184 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
74 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
185 using at_set_avoiding3[where xs="set as" and c="(as, bs, x, y, c, f as x c, f bs y c)" |
75 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
186 and x="Abs_lst as x"] |
76 fin1 fin2 |
187 apply(simp add: supp_Pair finite_supp fin1 fin2 Abs_fresh_star) |
77 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
188 apply(erule exE) |
|
189 apply(erule conjE)+ |
|
190 apply(drule fresh_star_supp_conv) |
|
191 apply(blast) |
|
192 done |
|
193 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
78 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
194 also have "\<dots> = Abs_lst as x" |
79 also have "\<dots> = Abs_lst as x" |
195 apply(rule perm_supp_eq) |
80 by (simp only: fr2 perm_supp_eq) |
196 apply(simp add: fr2) |
81 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
197 done |
|
198 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using e by simp |
|
199 then obtain r::perm where |
82 then obtain r::perm where |
200 qq1: "q \<bullet> x = r \<bullet> y" and |
83 qq1: "q \<bullet> x = r \<bullet> y" and |
201 qq2: "q \<bullet> as = r \<bullet> bs" and |
84 qq2: "q \<bullet> as = r \<bullet> bs" and |
202 qq3: "supp r \<subseteq> (set (q \<bullet> as) \<union> set bs)" |
85 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
203 apply - |
|
204 apply(drule_tac sym) |
86 apply(drule_tac sym) |
205 apply(simp only: Abs_eq_iff2 alphas) |
87 apply(simp only: Abs_eq_iff2 alphas) |
206 apply(erule exE) |
88 apply(erule exE) |
207 apply(erule conjE)+ |
89 apply(erule conjE)+ |
208 apply(drule_tac x="p" in meta_spec) |
90 apply(drule_tac x="p" in meta_spec) |
209 apply(simp) |
91 apply(simp add: set_eqvt) |
210 apply(blast) |
92 apply(blast) |
211 done |
93 done |
|
94 have "(set as) \<sharp>* f as x c" by (rule fcb1) |
|
95 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
|
96 by (simp add: permute_bool_def) |
|
97 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
98 apply(simp add: fresh_star_eqvt set_eqvt) |
|
99 apply(subst (asm) perm1) |
|
100 using inc fresh1 fr1 |
|
101 apply(auto simp add: fresh_star_def fresh_Pair) |
|
102 done |
|
103 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
104 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
|
105 apply(simp add: fresh_star_eqvt set_eqvt) |
|
106 apply(subst (asm) perm2[symmetric]) |
|
107 using qq3 fresh2 fr1 |
|
108 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
|
109 done |
|
110 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
212 have "f as x c = q \<bullet> (f as x c)" |
111 have "f as x c = q \<bullet> (f as x c)" |
213 apply(rule sym) |
112 apply(rule perm_supp_eq[symmetric]) |
214 apply(rule perm_supp_eq) |
113 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
215 using inc fcb1 fr1 |
|
216 apply(simp add: set_eqvt) |
|
217 apply(simp add: fresh_star_Pair) |
|
218 apply(auto simp add: fresh_star_def) |
|
219 done |
|
220 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
114 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
221 apply(subst perm1) |
115 apply(rule perm1) |
222 using inc fresh1 fr1 |
116 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
223 apply(simp add: set_eqvt) |
|
224 apply(simp add: fresh_star_Pair) |
|
225 apply(auto simp add: fresh_star_def) |
|
226 done |
|
227 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
117 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
228 also have "\<dots> = r \<bullet> (f bs y c)" |
118 also have "\<dots> = r \<bullet> (f bs y c)" |
229 apply(rule sym) |
119 apply(rule perm2[symmetric]) |
230 apply(subst perm2) |
120 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
231 using qq3 fresh2 fr1 |
121 also have "... = f bs y c" |
232 apply(simp add: set_eqvt) |
|
233 apply(simp add: fresh_star_Pair) |
|
234 apply(auto simp add: fresh_star_def) |
|
235 done |
|
236 also have "... = f bs y c" |
|
237 apply(rule perm_supp_eq) |
122 apply(rule perm_supp_eq) |
238 using qq3 fr1 fcb2 |
123 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
239 apply(simp add: set_eqvt) |
|
240 apply(simp add: fresh_star_Pair) |
|
241 apply(auto simp add: fresh_star_def) |
|
242 done |
|
243 finally show ?thesis by simp |
124 finally show ?thesis by simp |
244 qed |
125 qed |
|
126 |
|
127 lemma Abs_lst1_fcb2: |
|
128 fixes a b :: "atom" |
|
129 and x y :: "'b :: fs" |
|
130 and c::"'c :: fs" |
|
131 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
|
132 and fcb1: "a \<sharp> f a x c" |
|
133 and fresh: "{a, b} \<sharp>* c" |
|
134 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
135 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
136 shows "f a x c = f b y c" |
|
137 using e |
|
138 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"]) |
|
139 apply(simp_all) |
|
140 using fcb1 fresh perm1 perm2 |
|
141 apply(simp_all add: fresh_star_def) |
|
142 done |
245 |
143 |
246 lemma supp_zero_perm_zero: |
144 lemma supp_zero_perm_zero: |
247 shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0" |
145 shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0" |
248 by (metis supp_perm_singleton supp_zero_perm) |
146 by (metis supp_perm_singleton supp_zero_perm) |
249 |
147 |