332 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
332 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
333 defer |
333 defer |
334 apply(case_tac x) |
334 apply(case_tac x) |
335 apply(simp) |
335 apply(simp) |
336 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
336 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
337 apply(simp_all)[3] |
337 apply(simp_all add: fresh_star_def)[3] |
338 apply(blast) |
338 apply(blast) |
339 apply(blast) |
339 apply(blast) |
340 apply(simp add: fresh_star_def) |
|
341 apply(simp_all add: lam.distinct) |
340 apply(simp_all add: lam.distinct) |
342 apply(simp add: lam.eq_iff) |
341 apply(simp add: lam.eq_iff) |
343 apply(simp add: lam.eq_iff) |
342 apply(simp add: lam.eq_iff) |
344 apply(simp add: lam.eq_iff) |
343 apply(simp add: lam.eq_iff) |
345 apply(erule conjE) |
344 apply(erule conjE) |
346 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
345 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
347 prefer 2 |
346 prefer 2 |
348 apply(rule conjI) |
|
349 apply(simp add: Abs_fresh_iff) |
|
350 apply(drule sym) |
|
351 apply(simp add: Abs_fresh_iff) |
347 apply(simp add: Abs_fresh_iff) |
352 apply(subst (asm) Abs_eq_iff2) |
348 apply(subst (asm) Abs_eq_iff2) |
353 apply(auto) |
349 apply(auto) |
354 apply(simp add: alphas) |
350 apply(simp add: alphas) |
355 apply(simp add: atom_eqvt) |
351 apply(simp add: atom_eqvt) |
356 apply(clarify) |
352 apply(clarify) |
357 apply(rule trans) |
353 apply(rule trans) |
358 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
354 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
355 prefer 2 |
|
356 apply (subgoal_tac "p \<bullet> xsa = xsa") |
|
357 apply (simp add: eqvt_at_def) |
|
358 apply (rule supp_perm_eq) |
|
359 apply (rule fresh_star_supp_conv) |
|
360 apply (subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* xsa") |
|
361 apply (simp add: fresh_star_def fresh_def) |
|
362 apply blast |
|
363 apply (simp add: fresh_star_def fresh_def) |
|
364 apply (simp add: ln.supp) |
359 apply(rule fresh_star_supp_conv) |
365 apply(rule fresh_star_supp_conv) |
360 apply(drule fresh_star_perm_set_conv) |
366 apply (subst (asm) supp_perm_pair) |
361 apply(simp add: finite_supp) |
367 apply (elim disjE) |
362 apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* LNLam (trans_sumC (t, x # xsa))") |
368 apply (simp add: fresh_star_def supp_zero_perm) |
363 apply(auto simp add: fresh_star_def)[1] |
369 apply (simp add: flip_def[symmetric]) |
364 apply(simp (no_asm) add: fresh_star_def ln.fresh) |
370 apply(subgoal_tac "supp (x \<leftrightarrow> p \<bullet> x) \<sharp>* trans_sumC (t, x # xsa)") |
365 apply(rule conjI) |
371 apply simp |
|
372 apply (subst flip_def) |
|
373 apply (simp add: supp_swap) |
|
374 apply (simp add: fresh_star_def) |
|
375 apply (rule) |
|
376 apply rule |
|
377 prefer 2 |
366 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
378 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
367 apply(simp add: finite_supp) |
379 apply(simp add: finite_supp) |
368 apply(simp (no_asm_use) add: fresh_Pair) |
380 apply(simp (no_asm_use) add: fresh_Pair) |
369 apply(simp add: Abs_fresh_iff fresh_Cons)[1] |
381 apply(simp add: Abs_fresh_iff fresh_Cons)[1] |
370 apply(erule disjE) |
382 apply (metis Rep_name_inverse atom_name_def fresh_at_base) |
371 apply(erule disjE) |
383 apply assumption |
372 apply(simp) |
|
373 oops |
384 oops |
|
385 |
|
386 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
|
387 apply (case_tac "x = xa") |
|
388 apply simp |
|
389 apply (simp add: lam.eq_iff Abs1_eq_iff flip_def[symmetric]) |
|
390 by (metis atom_eqvt flip_at_simps(2) fresh_permute_iff) |
|
391 |
|
392 lemma supp_lookup: "supp (lookup l n name) = {atom name} - supp l" |
|
393 apply (induct l arbitrary: n) |
|
394 apply (simp_all add: ln.supp supp_at_base supp_Nil supp_Cons pure_supp) |
|
395 done |
|
396 |
|
397 lemma trans_eqvt[eqvt]: "p \<bullet> (trans t l) = trans (p \<bullet> t) (p \<bullet> l)" |
|
398 apply (induct t l rule: trans.induct) |
|
399 apply simp_all |
|
400 apply (simp add: eqvts permute_pure) |
|
401 done |
|
402 |
|
403 lemma diff_un: "a - (b \<union> c) = a - b - c" |
|
404 by blast |
|
405 |
|
406 lemma supp_trans: "supp (trans t l) = supp t - supp l" |
|
407 apply (induct t arbitrary: l rule: lam.induct) |
|
408 apply (simp_all add: lam.supp supp_at_base supp_lookup ln.supp) |
|
409 apply blast |
|
410 apply (rule_tac x="(lam, l)" and ?'a="name" in obtain_fresh) |
|
411 apply (simp add: fresh_Pair) |
|
412 apply clarify |
|
413 apply (subgoal_tac "supp (Lambda.trans (Lam [a]. ((name \<leftrightarrow> a) \<bullet> lam)) l) = |
|
414 supp lam - {atom name} - supp l") |
|
415 using helpr |
|
416 apply simp |
|
417 apply (simp add: ln.supp) |
|
418 apply (subgoal_tac "supp ((name \<leftrightarrow> a) \<bullet> (Lambda.trans lam ((name \<leftrightarrow> a) \<bullet> (a # l)))) = supp lam - {atom name} - supp l") |
|
419 apply (simp add: trans_eqvt) |
|
420 apply (simp add: supp_eqvt[symmetric]) |
|
421 apply (simp add: Diff_eqvt) |
|
422 apply (simp add: supp_eqvt supp_Cons union_eqvt) |
|
423 apply (simp add: diff_un) |
|
424 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*}) |
|
425 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*}) |
|
426 apply rule |
|
427 prefer 2 |
|
428 apply rule |
|
429 apply (simp add: supp_at_base) |
|
430 apply (subgoal_tac "(name \<leftrightarrow> a) \<bullet> (supp lam - {atom name}) = supp lam - {atom name}") |
|
431 apply (simp add: eqvts) |
|
432 unfolding flip_def |
|
433 apply (rule swap_fresh_fresh) |
|
434 apply (metis fresh_at_base fresh_def fresh_minus_atom_set lam.fsupp supp_at_base) |
|
435 by (metis fresh_def fresh_finite_atom_set fresh_minus_atom_set lam.fsupp) |
|
436 |
|
437 lemma "atom x \<sharp> trans_sumC (t, x # xsa)" |
|
438 by (simp add: fresh_def meta_eq_to_obj_eq[OF trans_def, symmetric, unfolded fun_eq_iff] supp_trans supp_Cons supp_at_base) |
|
439 *) |
374 |
440 |
375 nominal_datatype db = |
441 nominal_datatype db = |
376 DBVar nat |
442 DBVar nat |
377 | DBApp db db |
443 | DBApp db db |
378 | DBLam db |
444 | DBLam db |