717 | a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and> |
717 | a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and> |
718 (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and> |
718 (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and> |
719 (pi \<bullet> (bv5 l1) = bv5 l2)) |
719 (pi \<bullet> (bv5 l1) = bv5 l2)) |
720 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
720 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
721 | a4: "rLnil \<approx>l rLnil" |
721 | a4: "rLnil \<approx>l rLnil" |
722 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
722 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
723 |
723 |
724 thm a3[simplified alpha_gen] |
724 print_theorems |
|
725 |
|
726 lemma alpha5_inj: |
|
727 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)" |
|
728 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)" |
|
729 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and> |
|
730 (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and> |
|
731 (pi \<bullet> (bv5 l1) = bv5 l2)))" |
|
732 "rLnil \<approx>l rLnil" |
|
733 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)" |
|
734 apply - |
|
735 apply (simp_all add: alpha5_alphalts.intros) |
|
736 apply rule |
|
737 apply (erule alpha5.cases) |
|
738 apply (simp_all add: alpha5_alphalts.intros) |
|
739 apply rule |
|
740 apply (erule alpha5.cases) |
|
741 apply (simp_all add: alpha5_alphalts.intros) |
|
742 apply rule |
|
743 apply (erule alpha5.cases) |
|
744 apply (simp_all add: alpha5_alphalts.intros) |
|
745 apply rule |
|
746 apply (erule alphalts.cases) |
|
747 apply (simp_all add: alpha5_alphalts.intros) |
|
748 done |
|
749 |
|
750 lemma alpha5_equivps: |
|
751 shows "equivp alpha5" |
|
752 and "equivp alphalts" |
|
753 sorry |
|
754 |
|
755 quotient_type |
|
756 trm5 = rtrm5 / alpha5 |
|
757 and |
|
758 lts = rlts / alphalts |
|
759 by (auto intro: alpha5_equivps) |
|
760 |
|
761 |
725 end |
762 end |