214 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
214 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
215 apply(blast) |
215 apply(blast) |
216 apply(blast) |
216 apply(blast) |
217 done |
217 done |
218 |
218 |
219 |
219 termination |
|
220 by lexicographic_order |
|
221 |
|
222 nominal_primrec |
|
223 nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
|
224 where |
|
225 "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" |
|
226 | "atom x \<sharp> (u, v) \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" |
|
227 | "atom x \<sharp> (u, v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" |
|
228 | "(NotL <a>.M x)[u\<turnstile>n>v] = (if x=u then NotL <a>.(M[u\<turnstile>n>v]) v else NotL <a>.(M[u\<turnstile>n>v]) x)" |
|
229 | "(AndR <a>.M <b>.N c)[u\<turnstile>n>v] = AndR <a>.(M[u\<turnstile>n>v]) <b>.(N[u\<turnstile>n>v]) c" |
|
230 | "atom x \<sharp> (u, v) \<Longrightarrow> (AndL1 (x).M y)[u\<turnstile>n>v] = |
|
231 (if y=u then AndL1 (x).(M[u\<turnstile>n>v]) v else AndL1 (x).(M[u\<turnstile>n>v]) y)" |
|
232 | "atom x \<sharp> (u, v) \<Longrightarrow> (AndL2 (x).M y)[u\<turnstile>n>v] = |
|
233 (if y=u then AndL2 (x).(M[u\<turnstile>n>v]) v else AndL2 (x).(M[u\<turnstile>n>v]) y)" |
|
234 | "(OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b" |
|
235 | "(OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b" |
|
236 | "\<lbrakk>atom x \<sharp> (u, v); atom y \<sharp> (u, v)\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[u\<turnstile>n>v] = |
|
237 (if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)" |
|
238 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b" |
|
239 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = |
|
240 (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)" |
|
241 apply(simp only: eqvt_def) |
|
242 apply(simp only: nrename_graph_def) |
|
243 apply (rule, perm_simp, rule) |
|
244 apply(rule TrueI) |
|
245 -- "covered all cases" |
|
246 apply(case_tac x) |
|
247 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
|
248 apply (simp_all add: fresh_star_def)[12] |
|
249 apply(metis)+ |
|
250 -- "compatibility" |
|
251 apply(simp_all) |
|
252 apply(rule conjI) |
|
253 apply(elim conjE) |
|
254 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
|
255 apply(simp add: Abs_fresh_iff) |
|
256 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
257 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
258 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
259 apply(elim conjE) |
|
260 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
|
261 apply(simp add: Abs_fresh_iff) |
|
262 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
263 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
264 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
265 apply(elim conjE) |
|
266 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
|
267 apply(simp add: Abs_fresh_iff) |
|
268 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
269 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
270 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
271 apply(elim conjE) |
|
272 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
|
273 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
|
274 apply(erule Abs_lst1_fcb2) |
|
275 apply(simp add: Abs_fresh_iff) |
|
276 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
277 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
278 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
279 apply(blast) |
|
280 apply(blast) |
|
281 apply(elim conjE) |
|
282 apply(rule conjI) |
|
283 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
|
284 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
|
285 apply(erule Abs_lst1_fcb2) |
|
286 apply(simp add: Abs_fresh_iff) |
|
287 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
288 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
289 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
290 apply(blast) |
|
291 apply(blast) |
|
292 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
|
293 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
|
294 apply(erule Abs_lst1_fcb2) |
|
295 apply(simp add: Abs_fresh_iff) |
|
296 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
297 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
298 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
299 apply(blast) |
|
300 apply(blast) |
|
301 apply(elim conjE) |
|
302 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
|
303 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
|
304 apply(erule Abs_lst1_fcb2) |
|
305 apply(simp add: Abs_fresh_iff) |
|
306 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
307 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
308 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
309 apply(blast) |
|
310 apply(blast) |
|
311 apply(elim conjE)+ |
|
312 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
|
313 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
|
314 apply(erule Abs_lst1_fcb2) |
|
315 apply(simp add: Abs_fresh_iff) |
|
316 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
317 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
318 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
319 apply(blast) |
|
320 apply(blast) |
|
321 apply(elim conjE)+ |
|
322 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
|
323 apply(simp add: Abs_fresh_iff) |
|
324 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
325 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
326 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
327 apply(elim conjE) |
|
328 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
|
329 apply(simp add: Abs_fresh_iff) |
|
330 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
331 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
332 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
333 apply(elim conjE) |
|
334 apply(rule conjI) |
|
335 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
|
336 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
|
337 apply(erule Abs_lst1_fcb2) |
|
338 apply(simp add: Abs_fresh_iff) |
|
339 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
340 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
341 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
342 apply(blast) |
|
343 apply(blast) |
|
344 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
|
345 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
|
346 apply(erule Abs_lst1_fcb2) |
|
347 apply(simp add: Abs_fresh_iff) |
|
348 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
349 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
350 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
351 apply(blast) |
|
352 apply(blast) |
|
353 apply(erule conjE)+ |
|
354 apply(erule Abs_lst_fcb2) |
|
355 apply(simp add: Abs_fresh_star) |
|
356 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
357 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
358 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
359 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
360 apply(erule conjE)+ |
|
361 apply(rule conjI) |
|
362 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
|
363 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
|
364 apply(erule Abs_lst1_fcb2) |
|
365 apply(simp add: Abs_fresh_iff) |
|
366 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
367 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
368 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
369 apply(blast) |
|
370 apply(blast) |
|
371 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
|
372 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
|
373 apply(erule Abs_lst1_fcb2) |
|
374 apply(simp add: Abs_fresh_iff) |
|
375 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
376 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
377 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
378 apply(blast) |
|
379 apply(blast) |
|
380 done |
|
381 |
|
382 termination |
|
383 by lexicographic_order |
|
384 |
|
385 lemma crename_name_eqvt[eqvt]: |
|
386 shows "p \<bullet> (M[d\<turnstile>c>e]) = (p \<bullet> M)[(p \<bullet> d)\<turnstile>c>(p \<bullet> e)]" |
|
387 apply(nominal_induct M avoiding: d e rule: trm.strong_induct) |
|
388 apply(auto) |
|
389 done |
|
390 |
|
391 lemma nrename_name_eqvt[eqvt]: |
|
392 shows "p \<bullet> (M[x\<turnstile>n>y]) = (p \<bullet> M)[(p \<bullet> x)\<turnstile>n>(p \<bullet> y)]" |
|
393 apply(nominal_induct M avoiding: x y rule: trm.strong_induct) |
|
394 apply(auto) |
|
395 done |
|
396 |
|
397 nominal_primrec |
|
398 substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) |
|
399 where |
|
400 "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" |
|
401 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = |
|
402 (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" |
|
403 | "atom x\<sharp> (y, P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" |
|
404 | "\<lbrakk>atom a\<sharp> (c, P); atom x' \<sharp> (M, y, P)\<rbrakk> \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = |
|
405 (if x=y then Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x' else NotL <a>.(M{y:=<c>.P}) x)" |
|
406 | "\<lbrakk>atom a \<sharp> (c, P); atom b \<sharp> (c, P)\<rbrakk> \<Longrightarrow> |
|
407 (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" |
|
408 | "atom x \<sharp> (y, P) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = |
|
409 (if z=y then Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z' else AndL1 (x).(M{y:=<c>.P}) z)" |
|
410 | "atom x \<sharp> (y, P) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = |
|
411 (if z=y then Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z' else AndL2 (x).(M{y:=<c>.P}) z)" |
|
412 | "atom a \<sharp> (c, P) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b" |
|
413 | "atom a \<sharp> (c, P) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b" |
|
414 | "\<lbrakk>atom x \<sharp> (y, P); atom u \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = |
|
415 (if z=y then Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z' |
|
416 else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)" |
|
417 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b" |
|
418 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = |
|
419 (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' |
|
420 else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)" |
|
421 apply(simp only: eqvt_def) |
|
422 apply(simp only: substn_graph_def) |
|
423 apply (rule, perm_simp, rule) |
|
424 apply(rule TrueI) |
|
425 -- "covered all cases" |
|
426 apply(case_tac x) |
|
427 apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust) |
|
428 apply (simp_all add: fresh_star_def fresh_Pair)[12] |
|
429 apply(metis)+ |
|
430 apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)") |
|
431 apply(auto simp add: fresh_Pair)[1] |
|
432 apply(metis)+ |
|
433 apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)") |
|
434 apply(auto simp add: fresh_Pair)[1] |
|
435 apply(rule obtain_fresh) |
|
436 apply(auto)[1] |
|
437 apply(metis)+ |
|
438 -- "compatibility" |
|
439 apply(all_trivials) |
|
440 apply(simp) |
|
441 oops |
220 |
442 |
221 end |
443 end |
222 |
444 |
223 |
445 |
224 |
446 |