1132   "rfv_trm7 (rVr7 n) = {}"

  1133   "rfv_trm7 (rVr7 n) = {atom n}"

  1133 | "rfv_trm7 (rLm7 n t) = {atom n} \<union> (rfv_trm7 t)"

  1134 | "rfv_trm7 (rLm7 n t) = (rfv_trm7 t) - {atom n}"

  1134 | "rfv_trm7 (rLt7 l r) = (rfv_trm7 r) \<union> (rfv_trm7 l)"

  1135 | "rfv_trm7 (rLt7 l r) = (rfv_trm7 l) \<union> (rfv_trm7 r - rbv7 l)"

  1135 

  1136 

  1136 

  1137 instantiation

  1137 

  1138   rtrm7 :: pt

  1138 

  1139 begin

  1140 

  1141 primrec

  1142   permute_rtrm7

  1143 where

  1144   "permute_rtrm7 pi (rVr7 a) = rVr7 (pi \<bullet> a)"

  1145 | "permute_rtrm7 pi (rLm7 a t) = rLm7 (pi \<bullet> a) (permute_rtrm7 pi t)"

  1146 | "permute_rtrm7 pi (rLt7 t1 t2) = rLt7 (permute_rtrm7 pi t1) (permute_rtrm7 pi t2)"

  1147 

  1148 lemma pt_rtrm7_zero:

  1149   fixes t::rtrm7

  1150   shows "0 \<bullet> t = t"

  1151 apply(induct t)

  1152 apply(simp_all)

  1153 done

  1154 

  1155 lemma pt_rtrm7_plus:

  1156   fixes t::rtrm7

  1157   shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"

  1158 apply(induct t)

  1159 apply(simp_all)

  1160 done

  1161 

  1162 instance

  1163 apply default

  1164 apply(simp_all add: pt_rtrm7_zero pt_rtrm7_plus)

  1165 done

  1166 

  1167 end

  1168 

  1169 inductive

  1170   alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)

  1171 where

  1172   a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"

  1173 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 rfv_trm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"

  1174 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 rfv_trm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"

  1175 

  1176 lemma bvfv7: "rbv7 x = rfv_trm7 x"

  1177   apply induct

  1178   apply simp_all

  1179 done

  1180 

  1181 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"

  1182   apply simp

  1183   apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)

  1184   apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)

  1185   apply simp

  1186   apply (rule a3)

  1187   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

  1188   apply (simp_all add: alpha_gen fresh_star_def)

  1189   apply (rule a1)

  1190   apply (rule refl)

  1191 done