1157 |
1156 |
1158 lemma supp_Cons: |
1157 lemma supp_Cons: |
1159 shows "supp (x # xs) = supp x \<union> supp xs" |
1158 shows "supp (x # xs) = supp x \<union> supp xs" |
1160 by (simp add: supp_def Collect_imp_eq Collect_neg_eq) |
1159 by (simp add: supp_def Collect_imp_eq Collect_neg_eq) |
1161 |
1160 |
|
1161 lemma supp_append: |
|
1162 shows "supp (xs @ ys) = supp xs \<union> supp ys" |
|
1163 by (induct xs) (auto simp add: supp_Nil supp_Cons) |
|
1164 |
1162 lemma fresh_Nil: |
1165 lemma fresh_Nil: |
1163 shows "a \<sharp> []" |
1166 shows "a \<sharp> []" |
1164 by (simp add: fresh_def supp_Nil) |
1167 by (simp add: fresh_def supp_Nil) |
1165 |
1168 |
1166 lemma fresh_Cons: |
1169 lemma fresh_Cons: |
1167 shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs" |
1170 shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs" |
1168 by (simp add: fresh_def supp_Cons) |
1171 by (simp add: fresh_def supp_Cons) |
|
1172 |
|
1173 lemma fresh_append: |
|
1174 shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys" |
|
1175 by (induct xs) (simp_all add: fresh_Nil fresh_Cons) |
|
1176 |
1169 |
1177 |
1170 instance list :: (fs) fs |
1178 instance list :: (fs) fs |
1171 apply default |
1179 apply default |
1172 apply (induct_tac x) |
1180 apply (induct_tac x) |
1173 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1181 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1310 assumes fin: "finite S" |
1318 assumes fin: "finite S" |
1311 shows "a \<sharp> (insert x S) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S" |
1319 shows "a \<sharp> (insert x S) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S" |
1312 using fin unfolding fresh_def |
1320 using fin unfolding fresh_def |
1313 by (simp add: supp_of_finite_insert) |
1321 by (simp add: supp_of_finite_insert) |
1314 |
1322 |
|
1323 lemma supp_set_empty: |
|
1324 shows "supp {} = {}" |
|
1325 unfolding supp_def |
|
1326 by (simp add: empty_eqvt) |
|
1327 |
|
1328 lemma fresh_set_empty: |
|
1329 shows "a \<sharp> {}" |
|
1330 by (simp add: fresh_def supp_set_empty) |
|
1331 |
|
1332 lemma supp_set: |
|
1333 fixes xs :: "('a::fs) list" |
|
1334 shows "supp (set xs) = supp xs" |
|
1335 apply(induct xs) |
|
1336 apply(simp add: supp_set_empty supp_Nil) |
|
1337 apply(simp add: supp_Cons supp_of_finite_insert) |
|
1338 done |
|
1339 |
|
1340 lemma fresh_set: |
|
1341 fixes xs :: "('a::fs) list" |
|
1342 shows "a \<sharp> (set xs) \<longleftrightarrow> a \<sharp> xs" |
|
1343 unfolding fresh_def |
|
1344 by (simp add: supp_set) |
|
1345 |
1315 |
1346 |
1316 subsection {* Type @{typ "'a fset"} is finitely supported *} |
1347 subsection {* Type @{typ "'a fset"} is finitely supported *} |
1317 |
1348 |
1318 lemma fset_eqvt: |
1349 lemma fset_eqvt: |
1319 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
1350 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
1362 |
1393 |
1363 lemma fresh_star_supp_conv: |
1394 lemma fresh_star_supp_conv: |
1364 shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x" |
1395 shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x" |
1365 by (auto simp add: fresh_star_def fresh_def) |
1396 by (auto simp add: fresh_star_def fresh_def) |
1366 |
1397 |
1367 lemma fresh_star_prod: |
1398 lemma fresh_star_Pair: |
1368 fixes as::"atom set" |
|
1369 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1399 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1370 by (auto simp add: fresh_star_def fresh_Pair) |
1400 by (auto simp add: fresh_star_def fresh_Pair) |
1371 |
1401 |
1372 lemma fresh_star_union: |
1402 lemma fresh_star_list: |
|
1403 shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys" |
|
1404 and "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs" |
|
1405 and "as \<sharp>* []" |
|
1406 by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append) |
|
1407 |
|
1408 lemma fresh_star_set: |
|
1409 fixes xs::"('a::fs) list" |
|
1410 shows "as \<sharp>* set xs \<longleftrightarrow> as \<sharp>* xs" |
|
1411 unfolding fresh_star_def |
|
1412 by (simp add: fresh_set) |
|
1413 |
|
1414 lemma fresh_star_Un: |
1373 shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)" |
1415 shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)" |
1374 by (auto simp add: fresh_star_def) |
1416 by (auto simp add: fresh_star_def) |
1375 |
1417 |
1376 lemma fresh_star_insert: |
1418 lemma fresh_star_insert: |
1377 shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)" |
1419 shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)" |
1396 |
1438 |
1397 lemma fresh_star_unit_elim: |
1439 lemma fresh_star_unit_elim: |
1398 shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C" |
1440 shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C" |
1399 by (simp add: fresh_star_def fresh_Unit) |
1441 by (simp add: fresh_star_def fresh_Unit) |
1400 |
1442 |
1401 lemma fresh_star_prod_elim: |
1443 lemma fresh_star_Pair_elim: |
1402 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |
1444 shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)" |
1403 by (rule, simp_all add: fresh_star_prod) |
1445 by (rule, simp_all add: fresh_star_Pair) |
1404 |
1446 |
1405 lemma fresh_star_zero: |
1447 lemma fresh_star_zero: |
1406 shows "as \<sharp>* (0::perm)" |
1448 shows "as \<sharp>* (0::perm)" |
1407 unfolding fresh_star_def |
1449 unfolding fresh_star_def |
1408 by (simp add: fresh_zero_perm) |
1450 by (simp add: fresh_zero_perm) |
1424 unfolding Ball_def |
1466 unfolding Ball_def |
1425 apply(simp add: all_eqvt) |
1467 apply(simp add: all_eqvt) |
1426 apply(subst permute_fun_def) |
1468 apply(subst permute_fun_def) |
1427 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |
1469 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |
1428 done |
1470 done |
|
1471 |
|
1472 lemma at_fresh_star_inter: |
|
1473 assumes a: "(p \<bullet> bs) \<sharp>* bs" |
|
1474 and b: "finite bs" |
|
1475 shows "p \<bullet> bs \<inter> bs = {}" |
|
1476 using a b |
|
1477 unfolding fresh_star_def |
|
1478 unfolding fresh_def |
|
1479 by (auto simp add: supp_finite_atom_set) |
1429 |
1480 |
1430 |
1481 |
1431 section {* Induction principle for permutations *} |
1482 section {* Induction principle for permutations *} |
1432 |
1483 |
1433 |
1484 |
1522 case (plus p1 p2) |
1573 case (plus p1 p2) |
1523 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
1574 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
1524 then show "(p1 + p2) \<bullet> x = x" by simp |
1575 then show "(p1 + p2) \<bullet> x = x" by simp |
1525 qed |
1576 qed |
1526 qed |
1577 qed |
|
1578 |
|
1579 lemma perm_supp_eq: |
|
1580 assumes a: "(supp p) \<sharp>* x" |
|
1581 shows "p \<bullet> x = x" |
|
1582 by (rule supp_perm_eq) |
|
1583 (simp add: fresh_star_supp_conv a) |
1527 |
1584 |
1528 |
1585 |
1529 section {* Avoiding of atom sets *} |
1586 section {* Avoiding of atom sets *} |
1530 |
1587 |
1531 text {* |
1588 text {* |
1605 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p" |
1662 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p" |
1606 using assms |
1663 using assms |
1607 apply(erule_tac c="(c, x)" in at_set_avoiding) |
1664 apply(erule_tac c="(c, x)" in at_set_avoiding) |
1608 apply(simp add: supp_Pair) |
1665 apply(simp add: supp_Pair) |
1609 apply(rule_tac x="p" in exI) |
1666 apply(rule_tac x="p" in exI) |
1610 apply(simp add: fresh_star_prod) |
1667 apply(simp add: fresh_star_Pair) |
1611 apply(rule fresh_star_supp_conv) |
1668 apply(rule fresh_star_supp_conv) |
1612 apply(auto simp add: fresh_star_def) |
1669 apply(auto simp add: fresh_star_def) |
1613 done |
1670 done |
1614 |
1671 |
1615 lemma at_set_avoiding3: |
1672 lemma at_set_avoiding3: |
1619 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p \<subseteq> xs \<union> (p \<bullet> xs)" |
1676 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p \<subseteq> xs \<union> (p \<bullet> xs)" |
1620 using assms |
1677 using assms |
1621 apply(erule_tac c="(c, x)" in at_set_avoiding) |
1678 apply(erule_tac c="(c, x)" in at_set_avoiding) |
1622 apply(simp add: supp_Pair) |
1679 apply(simp add: supp_Pair) |
1623 apply(rule_tac x="p" in exI) |
1680 apply(rule_tac x="p" in exI) |
1624 apply(simp add: fresh_star_prod) |
1681 apply(simp add: fresh_star_Pair) |
1625 apply(rule fresh_star_supp_conv) |
1682 apply(rule fresh_star_supp_conv) |
1626 apply(auto simp add: fresh_star_def) |
1683 apply(auto simp add: fresh_star_def) |
1627 done |
1684 done |
1628 |
1685 |
1629 |
1686 |