1214 where |
1214 where |
1215 "rfv_foo8 (Foo0 x) = {atom x}" |
1215 "rfv_foo8 (Foo0 x) = {atom x}" |
1216 | "rfv_foo8 (Foo1 b t) = (rfv_foo8 t - rbv8 b) \<union> (rfv_bar8 b)" |
1216 | "rfv_foo8 (Foo1 b t) = (rfv_foo8 t - rbv8 b) \<union> (rfv_bar8 b)" |
1217 | "rfv_bar8 (Bar0 x) = {atom x}" |
1217 | "rfv_bar8 (Bar0 x) = {atom x}" |
1218 | "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})" |
1218 | "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})" |
|
1219 print_theorems |
1219 |
1220 |
1220 instantiation |
1221 instantiation |
1221 rfoo8 and rbar8 :: pt |
1222 rfoo8 and rbar8 :: pt |
1222 begin |
1223 begin |
1223 |
1224 |
1238 and |
1239 and |
1239 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
1240 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
1240 where |
1241 where |
1241 a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)" |
1242 a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)" |
1242 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)" |
1243 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)" |
1243 | a3: "(\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2" |
1244 | a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2" |
1244 | 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" |
1245 | 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" |
1245 |
1246 |
1246 lemma "(alpha8b ===> op =) rbv8 rbv8" |
1247 lemma "(alpha8b ===> op =) rbv8 rbv8" |
1247 apply simp apply clarify |
1248 apply simp apply clarify |
1248 apply (erule alpha8f_alpha8b.inducts(2)) |
1249 apply (erule alpha8f_alpha8b.inducts(2)) |
1249 apply (simp_all) |
1250 apply (simp_all) |
1250 done |
1251 done |
1251 lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8" |
1252 |
1252 apply simp apply clarify |
1253 lemma rfv_bar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> rfv_bar8 x = rfv_bar8 y" |
1253 apply (erule alpha8f_alpha8b.inducts(2)) |
1254 apply (erule alpha8f_alpha8b.inducts(2)) |
1254 apply (simp_all add: alpha_gen) |
1255 apply (simp_all add: alpha_gen) |
1255 done |
1256 done |
1256 |
1257 lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8" |
1257 lemma "(c :: name2) \<noteq> b \<Longrightarrow> (atom (a :: name)) \<noteq> (atom b) \<Longrightarrow> \<not> (alpha8f ===> op =) rfv_foo8 rfv_foo8" |
1258 apply simp apply clarify apply (simp add: rfv_bar8_rsp_hlp) |
1258 apply (simp_all) |
1259 done |
1259 apply (rule_tac x="Foo1 (Bar1 a c (Bar0 c)) (Foo0 a)" in exI) |
1260 |
1260 apply (rule_tac x="Foo1 (Bar1 a c (Bar0 b)) (Foo0 a)" in exI) |
1261 lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8" |
1261 apply (rule conjI) |
1262 apply simp apply clarify |
1262 apply (rule a3) |
1263 apply (erule alpha8f_alpha8b.inducts(1)) |
1263 apply (rule_tac x="0 :: perm" in exI) |
1264 apply (simp_all add: alpha_gen rfv_bar8_rsp_hlp) |
1264 apply (simp add: alpha_gen fresh_star_def) |
1265 done |
1265 apply (rule a1) |
1266 |
1266 apply (rule refl) |
|
1267 apply simp |
|
1268 done |
|
1269 |
1267 |
1270 |
1268 |
1271 |
1269 |
1272 |
1270 |
1273 text {* type schemes *} |
1271 text {* type schemes *} |