1193 datatype rfoo8 =

  1194   Foo0 "name"

  1195 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"

  1196 and rbar8 =

  1197   Bar0 "name"

  1198 | Bar1 "name" "name" "rbar8" --"bind second name in b"

  1199 

  1200 primrec

  1201   rbv8

  1202 where

  1203   "rbv8 (Bar0 x) = {}"

  1204 | "rbv8 (Bar1 v x b) = {atom v}"

  1205 

  1206 primrec 

  1207   rfv_foo8 and rfv_bar8

  1208 where

  1209   "rfv_foo8 (Foo0 x) = {atom x}"

  1210 | "rfv_foo8 (Foo1 b t) = (rfv_foo8 t - rbv8 b) \<union> (rfv_bar8 b)"

  1211 | "rfv_bar8 (Bar0 x) = {atom x}"

  1212 | "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})"

  1213 

  1214 instantiation

  1215   rfoo8 and rbar8 :: pt

  1216 begin

  1217 

  1218 primrec

  1219   permute_rfoo8 and permute_rbar8

  1220 where

  1221   "permute_rfoo8 pi (Foo0 a) = Foo0 (pi \<bullet> a)"

  1222 | "permute_rfoo8 pi (Foo1 b t) = Foo1 (permute_rbar8 pi b) (permute_rfoo8 pi t)"

  1223 | "permute_rbar8 pi (Bar0 a) = Bar0 (pi \<bullet> a)"

  1224 | "permute_rbar8 pi (Bar1 v x t) = Bar1 (pi \<bullet> v) (pi \<bullet> x) (permute_rbar8 pi t)"

  1225 

  1226 instance sorry

  1227 

  1228 end

  1229 

  1230 inductive

  1231   alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)

  1232 and

  1233   alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)

  1234 where

  1235   a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"

  1236 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"

  1237 | a3: "(\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"

  1238 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b rfv_bar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"

  1239 

  1240 lemma "(alpha8b ===> op =) rbv8 rbv8"

  1241   apply simp apply clarify

  1242   apply (erule alpha8f_alpha8b.inducts(2))

  1243   apply (simp_all)

  1244 done

  1245 

  1246 lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8"

  1247   apply simp apply clarify

  1248   apply (erule alpha8f_alpha8b.inducts(2))

  1249   apply (simp_all add:alpha_gen)

  1250 done

  1251 

  1252 lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8"

  1253   apply simp apply clarify

  1254   apply (erule alpha8f_alpha8b.inducts(1))

  1255   apply (simp_all add:alpha_gen)

  1256   apply (clarify)

  1257 sorry (* ??? *)

  1258 

  1259 

  1260 

  1261 

  1262