1261 lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8" |
1259 lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8" |
1262 apply simp apply clarify |
1260 apply simp apply clarify |
1263 apply (erule alpha8f_alpha8b.inducts(1)) |
1261 apply (erule alpha8f_alpha8b.inducts(1)) |
1264 apply (simp_all add: alpha_gen rfv_bar8_rsp_hlp) |
1262 apply (simp_all add: alpha_gen rfv_bar8_rsp_hlp) |
1265 done |
1263 done |
|
1264 |
|
1265 |
|
1266 |
|
1267 |
|
1268 |
|
1269 |
|
1270 datatype rlam9 = |
|
1271 Var9 "name" |
|
1272 | Lam9 "name" "rlam9" --"bind name in rlam" |
|
1273 and rbla9 = |
|
1274 Bla9 "rlam9" "rlam9" --"bind bv(first) in second" |
|
1275 |
|
1276 primrec |
|
1277 rbv9 |
|
1278 where |
|
1279 "rbv9 (Var9 x) = {}" |
|
1280 | "rbv9 (Lam9 x b) = {atom x}" |
|
1281 |
|
1282 primrec |
|
1283 rfv_lam9 and rfv_bla9 |
|
1284 where |
|
1285 "rfv_lam9 (Var9 x) = {atom x}" |
|
1286 | "rfv_lam9 (Lam9 b t) = (rfv_lam9 t - {atom b})" |
|
1287 | "rfv_bla9 (Bla9 l r) = (rfv_lam9 r - rbv9 l) \<union> rfv_lam9 l" |
|
1288 |
|
1289 instantiation |
|
1290 rlam9 and rbla9 :: pt |
|
1291 begin |
|
1292 |
|
1293 primrec |
|
1294 permute_rlam9 and permute_rbla9 |
|
1295 where |
|
1296 "permute_rlam9 pi (Var9 a) = Var9 (pi \<bullet> a)" |
|
1297 | "permute_rlam9 pi (Lam9 b t) = Lam9 (pi \<bullet> b) (permute_rlam9 pi t)" |
|
1298 | "permute_rbla9 pi (Bla9 l r) = Bla9 (permute_rlam9 pi l) (permute_rlam9 pi r)" |
|
1299 |
|
1300 instance sorry |
|
1301 |
|
1302 end |
|
1303 |
|
1304 inductive |
|
1305 alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100) |
|
1306 and |
|
1307 alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100) |
|
1308 where |
|
1309 a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)" |
|
1310 | a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l rfv_lam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2" |
|
1311 | a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l rfv_lam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2" |
|
1312 |
|
1313 quotient_type |
|
1314 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
|
1315 sorry |
|
1316 |
|
1317 quotient_definition |
|
1318 "qVar9 :: name \<Rightarrow> lam9" |
|
1319 as |
|
1320 "Var9" |
|
1321 |
|
1322 quotient_definition |
|
1323 "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9" |
|
1324 as |
|
1325 "Lam9" |
|
1326 |
|
1327 quotient_definition |
|
1328 "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9" |
|
1329 as |
|
1330 "Bla9" |
|
1331 |
|
1332 quotient_definition |
|
1333 "fv_lam9 :: lam9 \<Rightarrow> atom set" |
|
1334 as |
|
1335 "rfv_lam9" |
|
1336 |
|
1337 quotient_definition |
|
1338 "fv_bla9 :: bla9 \<Rightarrow> atom set" |
|
1339 as |
|
1340 "rfv_bla9" |
|
1341 |
|
1342 quotient_definition |
|
1343 "bv9 :: lam9 \<Rightarrow> atom set" |
|
1344 as |
|
1345 "rbv9" |
|
1346 |
|
1347 instantiation lam9 and bla9 :: pt |
|
1348 begin |
|
1349 |
|
1350 quotient_definition |
|
1351 "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9" |
|
1352 as |
|
1353 "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9" |
|
1354 |
|
1355 quotient_definition |
|
1356 "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9" |
|
1357 as |
|
1358 "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9" |
|
1359 |
|
1360 instance |
|
1361 sorry |
|
1362 |
|
1363 end |
|
1364 |
|
1365 lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk> |
|
1366 \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2" |
|
1367 apply (lifting a3[unfolded alpha_gen]) |
|
1368 apply injection |
|
1369 sorry |
|
1370 |
|
1371 |
|
1372 |
1266 |
1373 |
1267 |
1374 |
1268 |
1375 |
1269 |
1376 |
1270 |
1377 |