equal
deleted
inserted
replaced
820 "(alpha5 ===> op =) rfv_trm5 rfv_trm5" |
820 "(alpha5 ===> op =) rfv_trm5 rfv_trm5" |
821 "(alphalts ===> op =) rfv_lts rfv_lts" |
821 "(alphalts ===> op =) rfv_lts rfv_lts" |
822 "(alphalts ===> op =) rbv5 rbv5" |
822 "(alphalts ===> op =) rbv5 rbv5" |
823 sorry |
823 sorry |
824 |
824 |
|
825 lemma bv_list_rsp: |
|
826 shows "t \<approx>5 s \<Longrightarrow> True" |
|
827 and "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
|
828 apply(induct rule: alpha5_alphalts.inducts) |
|
829 apply(simp_all) |
|
830 done |
|
831 |
|
832 lemma |
|
833 shows "(alphalts ===> op =) rbv5 rbv5" |
|
834 by (simp add: bv_list_rsp) |
|
835 |
|
836 |
825 instantiation trm5 and lts :: pt |
837 instantiation trm5 and lts :: pt |
826 begin |
838 begin |
827 |
839 |
828 quotient_definition |
840 quotient_definition |
829 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
841 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |