386 alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100) |
386 alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100) |
387 where |
387 where |
388 a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)" |
388 a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)" |
389 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2" |
389 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2" |
390 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s" |
390 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s" |
391 | a4: "(\<exists>pi. (((bv2 bt), t) \<approx>gen alpha2 fv_rtrm2 pi ((bv2 bs), s))) \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s" |
391 | a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s)); |
392 | a5: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rAs a t \<approx>2a rAs b s" |
392 \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk> |
|
393 \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s" |
|
394 | a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *) |
393 |
395 |
394 lemma alpha2_equivp: |
396 lemma alpha2_equivp: |
395 "equivp alpha2" |
397 "equivp alpha2" |
396 "equivp alpha2a" |
398 "equivp alpha2a" |
397 sorry |
399 sorry |
472 |
475 |
473 end |
476 end |
474 |
477 |
475 inductive |
478 inductive |
476 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
479 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
|
480 and |
|
481 alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100) |
477 where |
482 where |
478 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
483 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
479 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
484 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
480 | a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and> |
485 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
481 (fv_trm3 t - {atom a})\<sharp>* pi \<and> |
486 | a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s)); |
482 (pi \<bullet> t) \<approx>3 s \<and> |
487 \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk> |
483 (pi \<bullet> a) = b) |
488 \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s" |
484 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
489 | a5: "ANil \<approx>3a ANil" |
485 | a4: "\<exists>pi. ( |
490 | a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st" |
486 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and> |
491 |
487 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and> |
492 lemma alpha3_equivp: |
488 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
493 "equivp alpha3" |
489 ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2" |
494 "equivp alpha3a" |
490 |
|
491 lemma alpha3_equivp: "equivp alpha3" |
|
492 sorry |
495 sorry |
493 |
496 |
494 quotient_type qtrm3 = trm3 / alpha3 |
497 quotient_type |
495 by (rule alpha3_equivp) |
498 qtrm3 = trm3 / alpha3 |
|
499 and |
|
500 qassigns = assigns / alpha3a |
|
501 by (auto intro: alpha3_equivp) |
496 |
502 |
497 |
503 |
498 section {*** lam with indirect list recursion ***} |
504 section {*** lam with indirect list recursion ***} |
499 |
505 |
500 datatype trm4 = |
506 datatype trm4 = |
572 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
578 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
573 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
579 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
574 where |
580 where |
575 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
581 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
576 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
582 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
577 | a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and> |
583 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
578 (fv_trm4 t - {atom a})\<sharp>* pi \<and> |
|
579 (pi \<bullet> t) \<approx>4 s \<and> |
|
580 (pi \<bullet> a) = b) |
|
581 \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
|
582 | a5: "[] \<approx>4list []" |
584 | a5: "[] \<approx>4list []" |
583 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
585 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
584 |
586 |
585 lemma alpha4_equivp: "equivp alpha4" sorry |
587 lemma alpha4_equivp: "equivp alpha4" sorry |
586 lemma alpha4list_equivp: "equivp alpha4list" sorry |
588 lemma alpha4list_equivp: "equivp alpha4list" sorry |
739 quotient_definition |
741 quotient_definition |
740 "bv5 :: lts \<Rightarrow> atom set" |
742 "bv5 :: lts \<Rightarrow> atom set" |
741 as |
743 as |
742 "rbv5" |
744 "rbv5" |
743 |
745 |
|
746 lemma rbv5_eqvt: |
|
747 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
|
748 sorry |
|
749 |
|
750 lemma rfv_trm5_eqvt: |
|
751 "pi \<bullet> (rfv_trm5 x) = rfv_trm5 (pi \<bullet> x)" |
|
752 sorry |
|
753 |
|
754 lemma rfv_lts_eqvt: |
|
755 "pi \<bullet> (rfv_lts x) = rfv_lts (pi \<bullet> x)" |
|
756 sorry |
|
757 |
|
758 lemma alpha5_eqvt: |
|
759 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
|
760 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
|
761 apply(induct rule: alpha5_alphalts.inducts) |
|
762 apply (simp_all add: alpha5_inj) |
|
763 apply (erule exE)+ |
|
764 apply(unfold alpha_gen) |
|
765 apply (erule conjE)+ |
|
766 apply (rule conjI) |
|
767 apply (rule_tac x="x \<bullet> pi" in exI) |
|
768 apply (rule conjI) |
|
769 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
770 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt) |
|
771 apply(rule conjI) |
|
772 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
773 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt) |
|
774 apply (subst permute_eqvt[symmetric]) |
|
775 apply (simp) |
|
776 apply (rule_tac x="x \<bullet> pia" in exI) |
|
777 apply (rule conjI) |
|
778 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
779 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt) |
|
780 apply(rule conjI) |
|
781 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
782 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt) |
|
783 apply (subst permute_eqvt[symmetric]) |
|
784 apply (simp) |
|
785 done |
|
786 |
744 lemma alpha5_rfv: |
787 lemma alpha5_rfv: |
745 "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)" |
788 "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)" |
746 "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)" |
789 "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)" |
747 apply(induct rule: alpha5_alphalts.inducts) |
790 apply(induct rule: alpha5_alphalts.inducts) |
748 apply(simp_all add: alpha_gen) |
791 apply(simp_all add: alpha_gen) |
749 done |
792 done |
750 |
793 |
751 lemma [quot_respect]: |
|
752 "(op = ===> alpha5 ===> alpha5) permute permute" |
|
753 "(op = ===> alphalts ===> alphalts) permute permute" |
|
754 "(op = ===> alpha5) rVr5 rVr5" |
|
755 "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5" |
|
756 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
757 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
758 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" |
|
759 "(alpha5 ===> op =) rfv_trm5 rfv_trm5" |
|
760 "(alphalts ===> op =) rfv_lts rfv_lts" |
|
761 "(alphalts ===> op =) rbv5 rbv5" |
|
762 sorry |
|
763 |
|
764 lemma bv_list_rsp: |
794 lemma bv_list_rsp: |
765 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
795 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
766 apply(induct rule: alpha5_alphalts.inducts(2)) |
796 apply(induct rule: alpha5_alphalts.inducts(2)) |
767 apply(simp_all) |
797 apply(simp_all) |
768 done |
798 done |
769 |
799 |
770 |
800 lemma [quot_respect]: |
771 lemma |
801 "(alphalts ===> op =) rfv_lts rfv_lts" |
|
802 "(alpha5 ===> op =) rfv_trm5 rfv_trm5" |
|
803 "(alphalts ===> op =) rbv5 rbv5" |
|
804 "(op = ===> alpha5) rVr5 rVr5" |
|
805 "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5" |
|
806 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
807 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
808 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" |
|
809 "(op = ===> alpha5 ===> alpha5) permute permute" |
|
810 "(op = ===> alphalts ===> alphalts) permute permute" |
|
811 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
|
812 apply (auto) |
|
813 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
814 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
815 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
816 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
817 done |
|
818 |
|
819 lemma |
772 shows "(alphalts ===> op =) rbv5 rbv5" |
820 shows "(alphalts ===> op =) rbv5 rbv5" |
773 by (simp add: bv_list_rsp) |
821 by (simp add: bv_list_rsp) |
774 |
822 |
775 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
823 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
776 |
824 |