equal
deleted
inserted
replaced
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 |
|
653 |
|
654 |
|
655 |
|
656 |
|
657 |
652 datatype rtrm5 = |
658 datatype rtrm5 = |
653 rVr5 "name" |
659 rVr5 "name" |
654 | rAp5 "rtrm5" "rtrm5" |
660 | rAp5 "rtrm5" "rtrm5" |
655 | rLt5 "rlts" "rtrm5" |
661 | rLt5 "rlts" "rtrm5" |
656 and rlts = |
662 and rlts = |
706 instance |
712 instance |
707 apply default |
713 apply default |
708 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus) |
714 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus) |
709 done |
715 done |
710 |
716 |
711 |
|
712 end |
717 end |
713 |
718 |
714 |
719 inductive |
|
720 alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100) |
|
721 and |
|
722 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100) |
|
723 where |
|
724 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)" |
|
725 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2" |
|
726 | a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and> |
|
727 (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and> |
|
728 (pi \<bullet> (bv5 l1) = bv5 l2)) |
|
729 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
|
730 | a4: "rLnil \<approx>l rLnil" |
|
731 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
|
732 |
|
733 thm a3[simplified alpha_gen] |
715 end |
734 end |