369 assumes "\<And>name b. P b (Vr1 name)" |
369 assumes "\<And>name b. P b (Vr1 name)" |
370 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
370 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
371 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
371 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
372 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
372 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
373 shows "P a rtrma" |
373 shows "P a rtrma" |
374 |
374 sorry |
375 |
375 |
376 section {*** lets with single assignments ***} |
376 section {*** lets with single assignments ***} |
377 |
377 |
378 datatype trm2 = |
378 datatype trm2 = |
379 Vr2 "name" |
379 Vr2 "name" |
647 qtrm4 = trm4 / alpha4 and |
647 qtrm4 = trm4 / alpha4 and |
648 qtrm4list = "trm4 list" / alpha4list |
648 qtrm4list = "trm4 list" / alpha4list |
649 by (simp_all add: alpha4_equivp alpha4list_equivp) |
649 by (simp_all add: alpha4_equivp alpha4list_equivp) |
650 |
650 |
651 |
651 |
|
652 datatype rtrm5 = |
|
653 rVr5 "name" |
|
654 | rAp5 "rtrm5" "rtrm5" |
|
655 | rLt5 "rlts" "rtrm5" |
|
656 and rlts = |
|
657 rLnil |
|
658 | rLcons "name" "rtrm5" "rlts" |
|
659 |
|
660 primrec |
|
661 bv5 |
|
662 where |
|
663 "bv5 rLnil = {}" |
|
664 | "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
|
665 |
|
666 primrec |
|
667 rfv_trm5 and rfv_lts |
|
668 where |
|
669 "rfv_trm5 (rVr5 n) = {atom n}" |
|
670 | "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)" |
|
671 | "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)" |
|
672 | "rfv_lts (rLnil) = {}" |
|
673 | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)" |
|
674 |
|
675 instantiation |
|
676 rtrm5 and rlts :: pt |
|
677 begin |
|
678 |
|
679 primrec |
|
680 permute_rtrm5 and permute_rlts |
|
681 where |
|
682 "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)" |
|
683 | "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)" |
|
684 | "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)" |
|
685 | "permute_rlts pi (rLnil) = rLnil" |
|
686 | "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)" |
|
687 |
|
688 lemma pt_rtrm5_zero: |
|
689 fixes t::rtrm5 |
|
690 and l::rlts |
|
691 shows "0 \<bullet> t = t" |
|
692 and "0 \<bullet> l = l" |
|
693 apply(induct t and l rule: rtrm5_rlts.inducts) |
|
694 apply(simp_all) |
|
695 done |
|
696 |
|
697 lemma pt_rtrm5_plus: |
|
698 fixes t::rtrm5 |
|
699 and l::rlts |
|
700 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
|
701 and "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)" |
|
702 apply(induct t and l rule: rtrm5_rlts.inducts) |
|
703 apply(simp_all) |
|
704 done |
|
705 |
|
706 instance |
|
707 apply default |
|
708 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus) |
|
709 done |
|
710 |
652 |
711 |
653 end |
712 end |
|
713 |
|
714 |
|
715 end |