448 |
449 |
449 lemma all_eqvt: |
450 lemma all_eqvt: |
450 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
451 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
451 unfolding permute_fun_def permute_bool_def |
452 unfolding permute_fun_def permute_bool_def |
452 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
453 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
|
454 |
|
455 lemma ex1_eqvt: |
|
456 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
|
457 unfolding Ex1_def |
|
458 apply(simp add: ex_eqvt) |
|
459 unfolding permute_fun_def |
|
460 apply(simp add: conj_eqvt all_eqvt) |
|
461 unfolding permute_fun_def |
|
462 apply(simp add: imp_eqvt permute_bool_def) |
|
463 done |
453 |
464 |
454 lemma permute_boolE: |
465 lemma permute_boolE: |
455 fixes P::"bool" |
466 fixes P::"bool" |
456 shows "p \<bullet> P \<Longrightarrow> P" |
467 shows "p \<bullet> P \<Longrightarrow> P" |
457 by (simp add: permute_bool_def) |
468 by (simp add: permute_bool_def) |
1231 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1241 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1232 using fresh_fun_app |
1242 using fresh_fun_app |
1233 unfolding fresh_def |
1243 unfolding fresh_def |
1234 by auto |
1244 by auto |
1235 |
1245 |
1236 text {* Support of Equivariant Functions *} |
1246 text {* Equivariant Functions *} |
|
1247 |
|
1248 definition |
|
1249 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
|
1250 |
|
1251 lemma eqvtI: |
|
1252 shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f" |
|
1253 unfolding eqvt_def |
|
1254 by simp |
1237 |
1255 |
1238 lemma supp_fun_eqvt: |
1256 lemma supp_fun_eqvt: |
1239 assumes a: "\<And>p. p \<bullet> f = f" |
1257 assumes a: "eqvt f" |
1240 shows "supp f = {}" |
1258 shows "supp f = {}" |
|
1259 using a |
|
1260 unfolding eqvt_def |
1241 unfolding supp_def |
1261 unfolding supp_def |
1242 using a by simp |
1262 by simp |
1243 |
1263 |
1244 lemma fresh_fun_eqvt_app: |
1264 lemma fresh_fun_eqvt_app: |
1245 assumes a: "\<And>p. p \<bullet> f = f" |
1265 assumes a: "eqvt f" |
1246 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1266 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1247 proof - |
1267 proof - |
1248 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1268 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1249 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1269 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1250 unfolding fresh_def |
1270 unfolding fresh_def |
1251 using supp_fun_app by auto |
1271 using supp_fun_app by auto |
1252 qed |
1272 qed |
|
1273 |
|
1274 text {* equivariance of a function at a given argument *} |
|
1275 definition |
|
1276 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
|
1277 |
|
1278 lemma supp_eqvt_at: |
|
1279 assumes asm: "eqvt_at f x" |
|
1280 and fin: "finite (supp x)" |
|
1281 shows "supp (f x) \<subseteq> supp x" |
|
1282 apply(rule supp_is_subset) |
|
1283 unfolding supports_def |
|
1284 unfolding fresh_def[symmetric] |
|
1285 using asm |
|
1286 apply(simp add: eqvt_at_def) |
|
1287 apply(simp add: swap_fresh_fresh) |
|
1288 apply(rule fin) |
|
1289 done |
|
1290 |
|
1291 lemma finite_supp_eqvt_at: |
|
1292 assumes asm: "eqvt_at f x" |
|
1293 and fin: "finite (supp x)" |
|
1294 shows "finite (supp (f x))" |
|
1295 apply(rule finite_subset) |
|
1296 apply(rule supp_eqvt_at[OF asm fin]) |
|
1297 apply(rule fin) |
|
1298 done |
|
1299 |
|
1300 lemma fresh_eqvt_at: |
|
1301 assumes asm: "eqvt_at f x" |
|
1302 and fin: "finite (supp x)" |
|
1303 and fresh: "a \<sharp> x" |
|
1304 shows "a \<sharp> f x" |
|
1305 using fresh |
|
1306 unfolding fresh_def |
|
1307 using supp_eqvt_at[OF asm fin] |
|
1308 by auto |
|
1309 |
|
1310 text {* helper functions for nominal_functions *} |
|
1311 |
|
1312 lemma the_default_eqvt: |
|
1313 assumes unique: "\<exists>!x. P x" |
|
1314 shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))" |
|
1315 apply(rule THE_default1_equality [symmetric]) |
|
1316 apply(rule_tac p="-p" in permute_boolE) |
|
1317 apply(simp add: ex1_eqvt) |
|
1318 apply(rule unique) |
|
1319 apply(rule_tac p="-p" in permute_boolE) |
|
1320 apply(rule subst[OF permute_fun_app_eq]) |
|
1321 apply(simp) |
|
1322 apply(rule THE_defaultI'[OF unique]) |
|
1323 done |
|
1324 |
|
1325 lemma fundef_ex1_eqvt: |
|
1326 fixes x::"'a::pt" |
|
1327 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
1328 assumes eqvt: "eqvt G" |
|
1329 assumes ex1: "\<exists>!y. G x y" |
|
1330 shows "(p \<bullet> (f x)) = f (p \<bullet> x)" |
|
1331 apply(simp only: f_def) |
|
1332 apply(subst the_default_eqvt) |
|
1333 apply(rule ex1) |
|
1334 using eqvt |
|
1335 unfolding eqvt_def |
|
1336 apply(simp add: permute_fun_app_eq) |
|
1337 done |
|
1338 |
|
1339 lemma fundef_ex1_eqvt_at: |
|
1340 fixes x::"'a::pt" |
|
1341 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
1342 assumes eqvt: "eqvt G" |
|
1343 assumes ex1: "\<exists>!y. G x y" |
|
1344 shows "eqvt_at f x" |
|
1345 unfolding eqvt_at_def |
|
1346 using assms |
|
1347 by (auto intro: fundef_ex1_eqvt) |
1253 |
1348 |
1254 |
1349 |
1255 section {* Support of Finite Sets of Finitely Supported Elements *} |
1350 section {* Support of Finite Sets of Finitely Supported Elements *} |
1256 |
1351 |
1257 text {* support and freshness for atom sets *} |
1352 text {* support and freshness for atom sets *} |
1272 assumes "finite S" |
1367 assumes "finite S" |
1273 shows "a \<sharp> S \<longleftrightarrow> a \<notin> S" |
1368 shows "a \<sharp> S \<longleftrightarrow> a \<notin> S" |
1274 unfolding fresh_def |
1369 unfolding fresh_def |
1275 by (simp add: supp_finite_atom_set[OF assms]) |
1370 by (simp add: supp_finite_atom_set[OF assms]) |
1276 |
1371 |
1277 |
|
1278 lemma Union_fresh: |
1372 lemma Union_fresh: |
1279 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
1373 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
1280 unfolding Union_image_eq[symmetric] |
1374 unfolding Union_image_eq[symmetric] |
1281 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
1375 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
1282 apply(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt) |
1376 unfolding eqvt_def |
1283 apply(subst permute_fun_app_eq) |
1377 unfolding permute_fun_def |
1284 back |
1378 apply(simp) |
1285 apply(simp add: supp_eqvt) |
1379 unfolding UNION_def |
|
1380 unfolding Collect_def |
|
1381 unfolding Bex_def |
|
1382 apply(simp add: ex_eqvt) |
|
1383 unfolding permute_fun_def |
|
1384 apply(simp add: conj_eqvt) |
|
1385 apply(simp add: mem_eqvt) |
|
1386 apply(simp add: supp_eqvt) |
|
1387 unfolding permute_fun_def |
|
1388 apply(simp) |
1286 apply(assumption) |
1389 apply(assumption) |
1287 done |
1390 done |
1288 |
1391 |
1289 lemma Union_supports_set: |
1392 lemma Union_supports_set: |
1290 shows "(\<Union>x \<in> S. supp x) supports S" |
1393 shows "(\<Union>x \<in> S. supp x) supports S" |
1545 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
1648 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
1546 unfolding fresh_star_def |
1649 unfolding fresh_star_def |
1547 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
1650 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
1548 |
1651 |
1549 lemma fresh_star_eqvt: |
1652 lemma fresh_star_eqvt: |
1550 shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
1653 shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
1551 unfolding fresh_star_def |
1654 unfolding fresh_star_def |
1552 unfolding Ball_def |
1655 unfolding Ball_def |
1553 apply(simp add: all_eqvt) |
1656 apply(simp add: all_eqvt) |
1554 apply(subst permute_fun_def) |
1657 apply(subst permute_fun_def) |
1555 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |
1658 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |