23 sorry |
23 sorry |
24 |
24 |
25 abbreviation |
25 abbreviation |
26 "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r" |
26 "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r" |
27 |
27 |
28 lemma Abs1_eq_fdest: |
|
29 fixes x y :: "'a :: at_base" |
|
30 and S T :: "'b :: fs" |
|
31 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
|
32 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T" |
|
33 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T" |
|
34 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S" |
|
35 and "sort_of (atom x) = sort_of (atom y)" |
|
36 shows "f x T = f y S" |
|
37 using assms apply - |
|
38 thm Abs1_eq_iff' |
|
39 apply (subst (asm) Abs1_eq_iff') |
|
40 apply simp_all |
|
41 apply (elim conjE disjE) |
|
42 apply simp |
|
43 apply(rule trans) |
|
44 apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric]) |
|
45 apply(rule fresh_star_supp_conv) |
|
46 apply(simp add: supp_swap fresh_star_def) |
|
47 apply(simp add: swap_commute) |
|
48 done |
|
49 |
|
50 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
28 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
51 frees_set :: "lam \<Rightarrow> atom set" |
29 frees_set :: "lam \<Rightarrow> atom set" |
52 where |
30 where |
53 "frees_set (Var x) = {atom x}" |
31 "frees_set (Var x) = {atom x}" |
54 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
32 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
62 apply(rule_tac y="x" in lam.exhaust) |
40 apply(rule_tac y="x" in lam.exhaust) |
63 apply(auto)[6] |
41 apply(auto)[6] |
64 apply(simp) |
42 apply(simp) |
65 apply(simp) |
43 apply(simp) |
66 apply(simp) |
44 apply(simp) |
67 apply (erule Abs1_eq_fdest) |
45 apply (erule Abs_lst1_fcb) |
68 apply(simp add: fresh_def) |
46 apply(simp add: fresh_def) |
69 apply(subst supp_of_finite_sets) |
47 apply(subst supp_of_finite_sets) |
70 apply(simp) |
48 apply(simp) |
71 apply(simp add: supp_atom) |
49 apply(simp add: supp_atom) |
72 apply(simp add: fresh_def) |
50 apply(simp add: fresh_def) |
121 apply (perm_simp) |
99 apply (perm_simp) |
122 apply(simp add: eq[simplified eqvt_def]) |
100 apply(simp add: eq[simplified eqvt_def]) |
123 apply(rule TrueI) |
101 apply(rule TrueI) |
124 apply(rule_tac y="x" in lam.exhaust) |
102 apply(rule_tac y="x" in lam.exhaust) |
125 apply(auto simp add: fresh_star_def) |
103 apply(auto simp add: fresh_star_def) |
126 apply(erule Abs1_eq_fdest) |
104 apply(erule Abs_lst1_fcb) |
127 apply simp_all |
105 apply simp_all |
128 apply(simp add: fcb) |
106 apply(simp add: fcb) |
129 apply (rule fresh_fun_eqvt_app3[OF eq(3)]) |
107 apply (rule fresh_fun_eqvt_app3[OF eq(3)]) |
130 apply (simp add: fresh_at_base) |
108 apply (simp add: fresh_at_base) |
131 apply assumption |
109 apply assumption |
209 unfolding eqvt_def height_graph_def |
187 unfolding eqvt_def height_graph_def |
210 apply (rule, perm_simp, rule) |
188 apply (rule, perm_simp, rule) |
211 apply(rule TrueI) |
189 apply(rule TrueI) |
212 apply(rule_tac y="x" in lam.exhaust) |
190 apply(rule_tac y="x" in lam.exhaust) |
213 apply(auto simp add: lam.distinct lam.eq_iff) |
191 apply(auto simp add: lam.distinct lam.eq_iff) |
214 apply (erule Abs1_eq_fdest) |
192 apply (erule Abs_lst1_fcb) |
215 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
193 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
216 done |
194 done |
217 |
195 |
218 termination |
196 termination |
219 by (relation "measure size") (simp_all add: lam.size) |
197 by (relation "measure size") (simp_all add: lam.size) |
232 unfolding eqvt_def frees_lst_graph_def |
210 unfolding eqvt_def frees_lst_graph_def |
233 apply (rule, perm_simp, rule) |
211 apply (rule, perm_simp, rule) |
234 apply(rule TrueI) |
212 apply(rule TrueI) |
235 apply(rule_tac y="x" in lam.exhaust) |
213 apply(rule_tac y="x" in lam.exhaust) |
236 apply(auto) |
214 apply(auto) |
237 apply (erule Abs1_eq_fdest) |
215 apply (erule Abs_lst1_fcb) |
238 apply(simp add: supp_removeAll fresh_def) |
216 apply(simp add: supp_removeAll fresh_def) |
239 apply(drule supp_eqvt_at) |
217 apply(drule supp_eqvt_at) |
240 apply(simp add: finite_supp) |
218 apply(simp add: finite_supp) |
241 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
219 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
242 done |
220 done |
264 apply(rule TrueI) |
242 apply(rule TrueI) |
265 apply(auto simp add: lam.distinct lam.eq_iff) |
243 apply(auto simp add: lam.distinct lam.eq_iff) |
266 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
244 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
267 apply(blast)+ |
245 apply(blast)+ |
268 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
246 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
269 apply (erule Abs1_eq_fdest) |
247 apply (erule Abs_lst1_fcb) |
270 apply(simp_all add: Abs_fresh_iff) |
248 apply(simp_all add: Abs_fresh_iff) |
271 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
249 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
272 apply(simp_all add: finite_supp fresh_Pair) |
250 apply(simp_all add: finite_supp fresh_Pair) |
273 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
251 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
274 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
252 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
453 apply (simp add: supp_lookup_fresh) |
431 apply (simp add: supp_lookup_fresh) |
454 apply (simp add: fresh_star_def ln.fresh) |
432 apply (simp add: fresh_star_def ln.fresh) |
455 apply (simp add: ln.fresh fresh_star_def) |
433 apply (simp add: ln.fresh fresh_star_def) |
456 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
434 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
457 apply (auto simp add: fresh_star_def)[3] |
435 apply (auto simp add: fresh_star_def)[3] |
458 apply (erule Abs1_eq_fdest) |
436 apply (erule Abs_lst1_fcb) |
459 apply (simp_all add: fresh_star_def) |
437 apply (simp_all add: fresh_star_def) |
460 apply (drule supp_eqvt_at) |
438 apply (drule supp_eqvt_at) |
461 apply (rule finite_supp) |
439 apply (rule finite_supp) |
462 apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1] |
440 apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1] |
463 apply (simp add: eqvt_at_def swap_fresh_fresh) |
441 apply (simp add: eqvt_at_def swap_fresh_fresh) |
477 apply(rule, perm_simp, rule) |
455 apply(rule, perm_simp, rule) |
478 apply(simp_all) |
456 apply(simp_all) |
479 apply(case_tac x) |
457 apply(case_tac x) |
480 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
458 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
481 apply(auto simp add: fresh_star_def) |
459 apply(auto simp add: fresh_star_def) |
482 apply(erule Abs1_eq_fdest) |
460 apply(erule Abs_lst1_fcb) |
483 apply(simp_all add: pure_fresh) |
461 apply(simp_all add: pure_fresh) |
484 apply (simp add: eqvt_at_def swap_fresh_fresh) |
462 apply (simp add: eqvt_at_def swap_fresh_fresh) |
485 done |
463 done |
486 |
464 |
487 termination |
465 termination |
547 apply(rule TrueI) |
525 apply(rule TrueI) |
548 apply (case_tac x) |
526 apply (case_tac x) |
549 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
527 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
550 apply (auto simp add: fresh_star_def fresh_at_list) |
528 apply (auto simp add: fresh_star_def fresh_at_list) |
551 apply (rule_tac f="dblam_in" in arg_cong) |
529 apply (rule_tac f="dblam_in" in arg_cong) |
552 apply (erule Abs1_eq_fdest) |
530 apply (erule Abs_lst1_fcb) |
553 apply (simp_all add: pure_fresh) |
531 apply (simp_all add: pure_fresh) |
554 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
532 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
555 apply (simp add: eqvt_at_def) |
533 apply (simp add: eqvt_at_def) |
556 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
534 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
557 done |
535 done |
649 apply simp_all[3] |
627 apply simp_all[3] |
650 apply blast |
628 apply blast |
651 apply blast |
629 apply blast |
652 apply (simp add: Abs1_eq_iff fresh_star_def) |
630 apply (simp add: Abs1_eq_iff fresh_star_def) |
653 apply(simp_all) |
631 apply(simp_all) |
654 apply(erule Abs1_eq_fdest) |
632 apply(erule Abs_lst1_fcb) |
655 apply (simp add: Abs_fresh_iff) |
633 apply (simp add: Abs_fresh_iff) |
656 apply (simp add: Abs_fresh_iff) |
634 apply (simp add: Abs_fresh_iff) |
657 apply (erule fresh_eqvt_at) |
635 apply (erule fresh_eqvt_at) |
658 apply (simp add: finite_supp) |
636 apply (simp add: finite_supp) |
659 apply (simp add: fresh_Inl) |
637 apply (simp add: fresh_Inl) |
660 apply (simp add: eqvt_at_def) |
638 apply (simp add: eqvt_at_def) |
661 apply simp |
639 apply simp |
662 defer |
640 defer |
663 apply clarify |
641 apply clarify |
664 apply(erule Abs1_eq_fdest) |
642 apply(erule Abs_lst1_fcb) |
665 apply (erule fresh_eqvt_at) |
643 apply (erule fresh_eqvt_at) |
666 apply (simp add: finite_supp) |
644 apply (simp add: finite_supp) |
667 apply (simp add: fresh_Inl var_fresh_subst) |
645 apply (simp add: fresh_Inl var_fresh_subst) |
668 apply (erule fresh_eqvt_at) |
646 apply (erule fresh_eqvt_at) |
669 apply (simp add: finite_supp) |
647 apply (simp add: finite_supp) |
670 apply (simp add: fresh_Inl) |
648 apply (simp add: fresh_Inl) |
671 apply (simp add: fresh_def) |
649 apply (simp add: fresh_def) |
672 using supp_subst apply blast |
650 using supp_subst apply blast |
673 apply (simp add: eqvt_at_def subst_eqvt) |
651 apply (simp add: eqvt_at_def subst_eqvt) |
674 apply (subst swap_fresh_fresh) |
652 apply (subst (2) swap_fresh_fresh) |
675 apply assumption+ |
653 apply assumption+ |
676 apply rule |
654 apply rule |
677 apply simp |
655 apply simp |
678 oops (* can this be defined ? *) |
656 oops (* can this be defined ? *) |
679 |
657 |
707 apply (simp add: eqvt_def map_term_graph_def) |
685 apply (simp add: eqvt_def map_term_graph_def) |
708 apply (rule, perm_simp, rule) |
686 apply (rule, perm_simp, rule) |
709 apply(rule TrueI) |
687 apply(rule TrueI) |
710 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
688 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
711 apply auto |
689 apply auto |
712 apply (erule Abs1_eq_fdest) |
690 apply (erule Abs_lst1_fcb) |
713 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
691 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
714 apply (simp add: eqvt_def permute_fun_app_eq) |
692 apply (simp add: eqvt_def permute_fun_app_eq) |
715 done |
693 done |
716 |
694 |
717 termination |
695 termination |