50 fixes a b :: "'a :: at" |
50 fixes a b :: "'a :: at" |
51 and S T :: "'b :: fs" |
51 and S T :: "'b :: fs" |
52 and c::"'c::fs" |
52 and c::"'c::fs" |
53 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
53 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
54 and fcb1: "atom a \<sharp> f a T c" |
54 and fcb1: "atom a \<sharp> f a T c" |
55 and fcb2: "atom b \<sharp> f b S c" |
|
56 and fresh: "{atom a, atom b} \<sharp>* c" |
55 and fresh: "{atom a, atom b} \<sharp>* c" |
57 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) 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" |
58 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) 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" |
59 shows "f a T c = f b S c" |
58 shows "f a T c = f b S c" |
60 proof - |
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 |
61 have fin1: "finite (supp (f a T c))" |
73 have fin1: "finite (supp (f a T c))" |
62 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
74 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
63 apply(simp add: supports_def) |
75 apply(simp add: supports_def) |
64 apply(simp add: fresh_def[symmetric]) |
76 apply(simp add: fresh_def[symmetric]) |
65 apply(clarify) |
77 apply(clarify) |
131 apply(simp add: fresh_Pair) |
143 apply(simp add: fresh_Pair) |
132 done |
144 done |
133 finally show ?thesis by simp |
145 finally show ?thesis by simp |
134 qed |
146 qed |
135 |
147 |
136 |
148 (* |
|
149 lemma Abs_lst_fcb2: |
|
150 fixes as bs :: "atom list" |
|
151 and x y :: "'b :: fs" |
|
152 and c::"'c::fs" |
|
153 assumes e: "(Abs_lst as x) = (Abs_lst bs y)" |
|
154 and fcb1: "(set as) \<sharp>* f as x c" |
|
155 and fcb2: "(set bs) \<sharp>* f bs y c" |
|
156 and fresh1: "set as \<sharp>* c" |
|
157 and fresh2: "set bs \<sharp>* c" |
|
158 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
159 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
160 shows "f as x c = f bs y c" |
|
161 *) |
137 |
162 |
138 nominal_primrec |
163 nominal_primrec |
139 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
164 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
140 where |
165 where |
141 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
166 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
167 apply(simp_all) |
192 apply(simp_all) |
168 apply(rule conjI) |
193 apply(rule conjI) |
169 apply(elim conjE) |
194 apply(elim conjE) |
170 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
195 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
171 apply(simp add: Abs_fresh_iff) |
196 apply(simp add: Abs_fresh_iff) |
172 apply(simp add: Abs_fresh_iff) |
197 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
173 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
198 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
174 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
199 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
175 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
200 apply(elim conjE) |
176 apply(elim conjE) |
201 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
177 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
202 apply(simp add: Abs_fresh_iff) |
178 apply(simp add: Abs_fresh_iff) |
203 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
179 apply(simp add: Abs_fresh_iff) |
204 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
180 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
205 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
181 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
206 apply(elim conjE) |
182 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
207 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
183 apply(elim conjE) |
208 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
184 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
209 apply(erule Abs_lst1_fcb2) |
185 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
210 apply(simp add: Abs_fresh_iff) |
186 apply(erule Abs_lst1_fcb2) |
211 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
187 apply(simp add: Abs_fresh_iff) |
212 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
188 apply(simp add: Abs_fresh_iff) |
213 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
189 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
214 apply(blast) |
190 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
215 apply(blast) |
191 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
216 apply(elim conjE) |
192 apply(blast) |
217 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
193 apply(blast) |
|
194 apply(elim conjE) |
|
195 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
|
196 apply(simp add: Abs_fresh_iff) |
|
197 apply(simp add: Abs_fresh_iff) |
218 apply(simp add: Abs_fresh_iff) |
198 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
219 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
199 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
220 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
200 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
221 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
201 apply(rule conjI) |
222 apply(rule conjI) |
202 apply(elim conjE) |
223 apply(elim conjE) |
203 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
224 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
204 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
225 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
205 apply(erule Abs_lst1_fcb2) |
226 apply(erule Abs_lst1_fcb2) |
206 apply(simp add: Abs_fresh_iff) |
|
207 apply(simp add: Abs_fresh_iff) |
227 apply(simp add: Abs_fresh_iff) |
208 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
228 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
209 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
229 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
210 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
230 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
211 apply(blast) |
231 apply(blast) |
213 apply(erule conjE)+ |
233 apply(erule conjE)+ |
214 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
234 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
215 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
235 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
216 apply(erule Abs_lst1_fcb2) |
236 apply(erule Abs_lst1_fcb2) |
217 apply(simp add: Abs_fresh_iff) |
237 apply(simp add: Abs_fresh_iff) |
218 apply(simp add: Abs_fresh_iff) |
238 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
219 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
239 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
220 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
240 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
221 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
241 apply(blast) |
222 apply(blast) |
242 apply(blast) |
223 apply(blast) |
243 apply(elim conjE) |
224 apply(elim conjE) |
244 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
225 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
245 apply(simp add: Abs_fresh_iff) |
226 apply(simp add: Abs_fresh_iff) |
246 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
227 apply(simp add: Abs_fresh_iff) |
247 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
228 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
248 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
229 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
249 apply(elim conjE) |
230 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
250 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
231 apply(elim conjE) |
251 apply(simp add: Abs_fresh_iff) |
232 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
252 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
233 apply(simp add: Abs_fresh_iff) |
253 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
234 apply(simp add: Abs_fresh_iff) |
254 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
235 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
255 apply(elim conjE) |
236 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
256 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
237 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
257 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
238 apply(elim conjE) |
258 apply(erule Abs_lst1_fcb2) |
239 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
259 apply(simp add: Abs_fresh_iff) |
240 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
260 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
241 apply(erule Abs_lst1_fcb2) |
261 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
242 apply(simp add: Abs_fresh_iff) |
262 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
243 apply(simp add: Abs_fresh_iff) |
263 apply(blast) |
244 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
264 apply(blast) |
245 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
265 apply(erule conjE)+ |
246 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
266 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
247 apply(blast) |
267 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
248 apply(blast) |
268 apply(erule Abs_lst1_fcb2) |
249 apply(erule conjE)+ |
|
250 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
251 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
|
252 apply(erule Abs_lst1_fcb2) |
|
253 apply(simp add: Abs_fresh_iff) |
|
254 apply(simp add: Abs_fresh_iff) |
269 apply(simp add: Abs_fresh_iff) |
255 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
270 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
256 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
271 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
257 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
272 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
258 apply(blast) |
273 apply(blast) |
260 apply(rule conjI) |
275 apply(rule conjI) |
261 apply(erule conjE)+ |
276 apply(erule conjE)+ |
262 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
277 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
263 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
278 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
264 apply(erule Abs_lst1_fcb2) |
279 apply(erule Abs_lst1_fcb2) |
265 apply(simp add: Abs_fresh_iff) |
|
266 apply(simp add: Abs_fresh_iff) |
280 apply(simp add: Abs_fresh_iff) |
267 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
281 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
268 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
282 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
269 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
283 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
270 apply(blast) |
284 apply(blast) |
272 apply(erule conjE)+ |
286 apply(erule conjE)+ |
273 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
287 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
274 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
288 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
275 apply(erule Abs_lst1_fcb2) |
289 apply(erule Abs_lst1_fcb2) |
276 apply(simp add: Abs_fresh_iff) |
290 apply(simp add: Abs_fresh_iff) |
277 apply(simp add: Abs_fresh_iff) |
|
278 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
291 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
279 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
292 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
280 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
293 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
281 apply(blast) |
294 apply(blast) |
282 apply(blast) |
295 apply(blast) |
284 apply(erule conjE)+ |
297 apply(erule conjE)+ |
285 apply(rule conjI) |
298 apply(rule conjI) |
286 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
299 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
287 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
300 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
288 apply(erule Abs_lst1_fcb2) |
301 apply(erule Abs_lst1_fcb2) |
289 apply(simp add: Abs_fresh_iff) |
|
290 apply(simp add: Abs_fresh_iff) |
302 apply(simp add: Abs_fresh_iff) |
291 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
303 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
292 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
304 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
293 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
305 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
294 apply(blast) |
306 apply(blast) |
295 apply(blast) |
307 apply(blast) |
296 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
308 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
297 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
309 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
298 apply(erule Abs_lst1_fcb2) |
310 apply(erule Abs_lst1_fcb2) |
299 apply(simp add: Abs_fresh_iff) |
311 apply(simp add: Abs_fresh_iff) |
300 apply(simp add: Abs_fresh_iff) |
|
301 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
312 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
302 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
313 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
303 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
314 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
304 apply(blast) |
315 apply(blast) |
305 apply(blast) |
316 apply(blast) |