83 | "bv_tvs TvsNil = []" |
84 | "bv_tvs TvsNil = []" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
85 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
85 | "bv_cvs CvsNil = []" |
86 | "bv_cvs CvsNil = []" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
87 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
87 |
88 |
88 (* can lift *) |
89 (* generated theorems *) |
89 |
90 |
90 thm distinct |
91 thm core_haskell.distinct |
91 thm induct |
92 thm core_haskell.induct |
92 thm exhaust |
93 thm core_haskell.exhaust |
93 thm fv_defs |
94 thm core_haskell.fv_defs |
94 thm bn_defs |
95 thm core_haskell.bn_defs |
95 thm perm_simps |
96 thm core_haskell.perm_simps |
96 thm eq_iff |
97 thm core_haskell.eq_iff |
97 thm fv_bn_eqvt |
98 thm core_haskell.fv_bn_eqvt |
98 thm size_eqvt |
99 thm core_haskell.size_eqvt |
99 |
100 |
100 |
101 (* |
101 |
|
102 |
|
103 |
|
104 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
|
105 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
|
106 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
|
107 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
|
108 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts |
|
109 |
|
110 lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts |
|
111 lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros |
|
112 |
|
113 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
102 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
114 unfolding fresh_star_def Ball_def |
103 unfolding fresh_star_def Ball_def |
115 by auto (simp_all add: fresh_minus_perm) |
104 by auto (simp_all add: fresh_minus_perm) |
116 |
105 |
117 primrec permute_bv_vs_raw |
106 primrec permute_bv_vs_raw |
395 have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))" |
384 have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))" |
396 apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts) |
385 apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts) |
397 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
386 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
398 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
387 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
399 |
388 |
400 (* GOAL1 *) |
389 --"GOAL1" |
401 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> |
390 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> |
402 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
391 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
403 apply clarify |
392 apply clarify |
404 apply (simp only: perm) |
393 apply (simp only: perm) |
405 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
394 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
433 apply (simp add: finite_supp) |
422 apply (simp add: finite_supp) |
434 apply (simp add: fresh_def) |
423 apply (simp add: fresh_def) |
435 apply (simp only: supp_abs eqvts) |
424 apply (simp only: supp_abs eqvts) |
436 apply blast |
425 apply blast |
437 |
426 |
438 (* GOAL2 *) |
427 --"GOAL2" |
439 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and> |
428 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and> |
440 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)") |
429 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)") |
441 apply clarify |
430 apply clarify |
442 apply (simp only: perm) |
431 apply (simp only: perm) |
443 apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)" |
432 apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)" |
472 apply (simp add: fresh_def) |
461 apply (simp add: fresh_def) |
473 apply (simp only: supp_abs eqvts) |
462 apply (simp only: supp_abs eqvts) |
474 apply blast |
463 apply blast |
475 |
464 |
476 |
465 |
477 (* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *) |
466 --"GOAL3 a copy-and-paste of Goal2 with consts and variable names changed" |
478 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
467 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
479 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
468 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
480 apply clarify |
469 apply clarify |
481 apply (simp only: perm) |
470 apply (simp only: perm) |
482 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
471 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
510 apply (simp add: finite_supp) |
499 apply (simp add: finite_supp) |
511 apply (simp add: fresh_def) |
500 apply (simp add: fresh_def) |
512 apply (simp only: supp_abs eqvts) |
501 apply (simp only: supp_abs eqvts) |
513 apply blast |
502 apply blast |
514 |
503 |
515 (* GOAL4 a copy-and-paste *) |
504 --"GOAL4 a copy-and-paste" |
516 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and> |
505 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and> |
517 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)") |
506 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)") |
518 apply clarify |
507 apply clarify |
519 apply (simp only: perm) |
508 apply (simp only: perm) |
520 apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)" |
509 apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)" |
549 apply (simp add: fresh_def) |
538 apply (simp add: fresh_def) |
550 apply (simp only: supp_abs eqvts) |
539 apply (simp only: supp_abs eqvts) |
551 apply blast |
540 apply blast |
552 |
541 |
553 |
542 |
554 (* GOAL5 a copy-and-paste *) |
543 --"GOAL5 a copy-and-paste" |
555 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
544 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
556 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)") |
545 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)") |
557 apply clarify |
546 apply clarify |
558 apply (simp only: perm) |
547 apply (simp only: perm) |
559 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
548 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
588 apply (simp add: fresh_def) |
577 apply (simp add: fresh_def) |
589 apply (simp only: supp_abs eqvts) |
578 apply (simp only: supp_abs eqvts) |
590 apply blast |
579 apply blast |
591 |
580 |
592 |
581 |
593 (* GOAL6 a copy-and-paste *) |
582 --"GOAL6 a copy-and-paste" |
594 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
583 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
595 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)") |
584 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)") |
596 apply clarify |
585 apply clarify |
597 apply (simp only: perm) |
586 apply (simp only: perm) |
598 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
587 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
627 apply (simp add: finite_supp) |
616 apply (simp add: finite_supp) |
628 apply (simp add: fresh_def) |
617 apply (simp add: fresh_def) |
629 apply (simp only: supp_abs eqvts) |
618 apply (simp only: supp_abs eqvts) |
630 apply blast |
619 apply blast |
631 |
620 |
632 (* MAIN ACons Goal *) |
621 --"MAIN ACons Goal" |
633 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and> |
622 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and> |
634 supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
623 supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
635 apply clarify |
624 apply clarify |
636 apply (simp only: perm eqvts) |
625 apply (simp only: perm eqvts) |
637 apply (subst ACons_subst) |
626 apply (subst ACons_subst) |
653 done |
642 done |
654 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+) |
643 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 moreover have "P9 i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+) |
644 moreover have "P9 i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+) |
656 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
645 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
657 qed |
646 qed |
|
647 *) |
658 |
648 |
659 section {* test about equivariance for alpha *} |
649 section {* test about equivariance for alpha *} |
660 |
650 |
661 (* this should not be an equivariance rule *) |
651 (* this should not be an equivariance rule *) |
662 (* for the moment, we force it to be *) |
652 (* for the moment, we force it to be *) |