192 apply (simp only: eq_iff) |
192 apply (simp only: eq_iff) |
193 apply (rule_tac x="q" in exI) |
193 apply (rule_tac x="q" in exI) |
194 apply (simp add: alphas) |
194 apply (simp add: alphas) |
195 apply (simp add: perm_bv2[symmetric]) |
195 apply (simp add: perm_bv2[symmetric]) |
196 apply (simp add: eqvts[symmetric]) |
196 apply (simp add: eqvts[symmetric]) |
197 apply (simp add: supp_Abs) |
197 apply (simp add: supp_abs) |
198 apply (simp add: fv_supp) |
198 apply (simp add: fv_supp) |
199 apply (simp add: alpha_perm_bn) |
199 apply (simp add: alpha_perm_bn) |
200 apply (rule supp_perm_eq[symmetric]) |
200 apply (rule supp_perm_eq[symmetric]) |
201 apply (subst supp_finite_atom_set) |
201 apply (subst supp_finite_atom_set) |
202 apply (rule finite_Diff) |
202 apply (rule finite_Diff) |
392 apply (simp only: perm) |
392 apply (simp only: perm) |
393 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
393 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
394 and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
394 and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
395 apply (simp only: eq_iff) |
395 apply (simp only: eq_iff) |
396 apply (rule_tac x="-pa" in exI) |
396 apply (rule_tac x="-pa" in exI) |
397 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
397 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
398 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
398 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
399 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
399 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
400 apply (simp add: eqvts) |
400 apply (simp add: eqvts) |
401 apply (simp add: eqvts[symmetric]) |
401 apply (simp add: eqvts[symmetric]) |
402 apply (rule conjI) |
402 apply (rule conjI) |
420 apply (simp add: eqvts eqvts_raw) |
420 apply (simp add: eqvts eqvts_raw) |
421 apply (rule at_set_avoiding2_atom) |
421 apply (rule at_set_avoiding2_atom) |
422 apply (simp add: finite_supp) |
422 apply (simp add: finite_supp) |
423 apply (simp add: finite_supp) |
423 apply (simp add: finite_supp) |
424 apply (simp add: fresh_def) |
424 apply (simp add: fresh_def) |
425 apply (simp only: supp_Abs eqvts) |
425 apply (simp only: supp_abs eqvts) |
426 apply blast |
426 apply blast |
427 |
427 |
428 (* GOAL2 *) |
428 (* GOAL2 *) |
429 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> e \<and> |
429 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> e \<and> |
430 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> co)) \<sharp>* pa)") |
430 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> co)) \<sharp>* pa)") |
432 apply (simp only: perm) |
432 apply (simp only: perm) |
433 apply(rule_tac t="CAll (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> co)" |
433 apply(rule_tac t="CAll (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> co)" |
434 and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
434 and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
435 apply (simp only: eq_iff) |
435 apply (simp only: eq_iff) |
436 apply (rule_tac x="-pa" in exI) |
436 apply (rule_tac x="-pa" in exI) |
437 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
437 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
438 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}" |
438 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}" |
439 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst) |
439 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst) |
440 apply (simp add: eqvts) |
440 apply (simp add: eqvts) |
441 apply (simp add: eqvts[symmetric]) |
441 apply (simp add: eqvts[symmetric]) |
442 apply (rule conjI) |
442 apply (rule conjI) |
460 apply (simp add: eqvts eqvts_raw) |
460 apply (simp add: eqvts eqvts_raw) |
461 apply (rule at_set_avoiding2_atom) |
461 apply (rule at_set_avoiding2_atom) |
462 apply (simp add: finite_supp) |
462 apply (simp add: finite_supp) |
463 apply (simp add: finite_supp) |
463 apply (simp add: finite_supp) |
464 apply (simp add: fresh_def) |
464 apply (simp add: fresh_def) |
465 apply (simp only: supp_Abs eqvts) |
465 apply (simp only: supp_abs eqvts) |
466 apply blast |
466 apply blast |
467 |
467 |
468 |
468 |
469 (* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *) |
469 (* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *) |
470 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
470 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
473 apply (simp only: perm) |
473 apply (simp only: perm) |
474 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
474 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
475 and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst) |
475 and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst) |
476 apply (simp only: eq_iff) |
476 apply (simp only: eq_iff) |
477 apply (rule_tac x="-pa" in exI) |
477 apply (rule_tac x="-pa" in exI) |
478 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
478 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
479 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
479 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
480 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
480 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
481 apply (simp add: eqvts) |
481 apply (simp add: eqvts) |
482 apply (simp add: eqvts[symmetric]) |
482 apply (simp add: eqvts[symmetric]) |
483 apply (rule conjI) |
483 apply (rule conjI) |
501 apply (simp add: eqvts eqvts_raw) |
501 apply (simp add: eqvts eqvts_raw) |
502 apply (rule at_set_avoiding2_atom) |
502 apply (rule at_set_avoiding2_atom) |
503 apply (simp add: finite_supp) |
503 apply (simp add: finite_supp) |
504 apply (simp add: finite_supp) |
504 apply (simp add: finite_supp) |
505 apply (simp add: fresh_def) |
505 apply (simp add: fresh_def) |
506 apply (simp only: supp_Abs eqvts) |
506 apply (simp only: supp_abs eqvts) |
507 apply blast |
507 apply blast |
508 |
508 |
509 (* GOAL4 a copy-and-paste *) |
509 (* GOAL4 a copy-and-paste *) |
510 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
510 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
511 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
511 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
513 apply (simp only: perm) |
513 apply (simp only: perm) |
514 apply(rule_tac t="LAMC (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> trm)" |
514 apply(rule_tac t="LAMC (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> trm)" |
515 and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
515 and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
516 apply (simp only: eq_iff) |
516 apply (simp only: eq_iff) |
517 apply (rule_tac x="-pa" in exI) |
517 apply (rule_tac x="-pa" in exI) |
518 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
518 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
519 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
519 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
520 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
520 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
521 apply (simp add: eqvts) |
521 apply (simp add: eqvts) |
522 apply (simp add: eqvts[symmetric]) |
522 apply (simp add: eqvts[symmetric]) |
523 apply (rule conjI) |
523 apply (rule conjI) |
541 apply (simp add: eqvts eqvts_raw) |
541 apply (simp add: eqvts eqvts_raw) |
542 apply (rule at_set_avoiding2_atom) |
542 apply (rule at_set_avoiding2_atom) |
543 apply (simp add: finite_supp) |
543 apply (simp add: finite_supp) |
544 apply (simp add: finite_supp) |
544 apply (simp add: finite_supp) |
545 apply (simp add: fresh_def) |
545 apply (simp add: fresh_def) |
546 apply (simp only: supp_Abs eqvts) |
546 apply (simp only: supp_abs eqvts) |
547 apply blast |
547 apply blast |
548 |
548 |
549 |
549 |
550 (* GOAL5 a copy-and-paste *) |
550 (* GOAL5 a copy-and-paste *) |
551 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
551 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
554 apply (simp only: perm) |
554 apply (simp only: perm) |
555 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
555 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
556 and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst) |
556 and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst) |
557 apply (simp only: eq_iff) |
557 apply (simp only: eq_iff) |
558 apply (rule_tac x="-pa" in exI) |
558 apply (rule_tac x="-pa" in exI) |
559 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
559 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
560 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
560 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
561 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
561 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
562 apply (simp add: eqvts) |
562 apply (simp add: eqvts) |
563 apply (simp add: eqvts[symmetric]) |
563 apply (simp add: eqvts[symmetric]) |
564 apply (rule conjI) |
564 apply (rule conjI) |
582 apply (simp add: eqvts eqvts_raw) |
582 apply (simp add: eqvts eqvts_raw) |
583 apply (rule at_set_avoiding2_atom) |
583 apply (rule at_set_avoiding2_atom) |
584 apply (simp add: finite_supp) |
584 apply (simp add: finite_supp) |
585 apply (simp add: finite_supp) |
585 apply (simp add: finite_supp) |
586 apply (simp add: fresh_def) |
586 apply (simp add: fresh_def) |
587 apply (simp only: supp_Abs eqvts) |
587 apply (simp only: supp_abs eqvts) |
588 apply blast |
588 apply blast |
589 |
589 |
590 |
590 |
591 (* GOAL6 a copy-and-paste *) |
591 (* GOAL6 a copy-and-paste *) |
592 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
592 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
595 apply (simp only: perm) |
595 apply (simp only: perm) |
596 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
596 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
597 and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst) |
597 and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst) |
598 apply (simp only: eq_iff) |
598 apply (simp only: eq_iff) |
599 apply (rule_tac x="-pa" in exI) |
599 apply (rule_tac x="-pa" in exI) |
600 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
600 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
601 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
601 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
602 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
602 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
603 apply (simp add: eqvts) |
603 apply (simp add: eqvts) |
604 apply (simp add: eqvts[symmetric]) |
604 apply (simp add: eqvts[symmetric]) |
605 apply (rule conjI) |
605 apply (rule conjI) |
624 apply (simp add: eqvts eqvts_raw) |
624 apply (simp add: eqvts eqvts_raw) |
625 apply (rule at_set_avoiding2_atom) |
625 apply (rule at_set_avoiding2_atom) |
626 apply (simp add: finite_supp) |
626 apply (simp add: finite_supp) |
627 apply (simp add: finite_supp) |
627 apply (simp add: finite_supp) |
628 apply (simp add: fresh_def) |
628 apply (simp add: fresh_def) |
629 apply (simp only: supp_Abs eqvts) |
629 apply (simp only: supp_abs eqvts) |
630 apply blast |
630 apply blast |
631 |
631 |
632 (* MAIN ACons Goal *) |
632 (* MAIN ACons Goal *) |
633 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and> |
633 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and> |
634 supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
634 supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
645 apply (simp add: perm_bv2[symmetric]) |
645 apply (simp add: perm_bv2[symmetric]) |
646 apply (simp add: eqvts eqvts_raw) |
646 apply (simp add: eqvts eqvts_raw) |
647 apply (rule at_set_avoiding2) |
647 apply (rule at_set_avoiding2) |
648 apply (simp add: fin_bv) |
648 apply (simp add: fin_bv) |
649 apply (simp add: finite_supp) |
649 apply (simp add: finite_supp) |
650 apply (simp add: supp_Abs) |
650 apply (simp add: supp_abs) |
651 apply (rule finite_Diff) |
651 apply (rule finite_Diff) |
652 apply (simp add: finite_supp) |
652 apply (simp add: finite_supp) |
653 apply (simp add: fresh_star_def fresh_def supp_Abs eqvts) |
653 apply (simp add: fresh_star_def fresh_def supp_abs eqvts) |
654 done |
654 done |
655 then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+) |
655 then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+) |
656 moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+) |
656 moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+) |
657 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
657 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
658 qed |
658 qed |