1078 section {* Support and freshness for applications *}

  1108 section {* Support and Freshness for Applications *}

  1106 text {* support of equivariant functions *}

  1136 text {* Support of Equivariant Functions *}

  1197 section {* Concrete atoms types *}

  1227 section {* Fresh-Star *}

  1228 

  1229 

  1230 text {* The fresh-star generalisation of fresh is used in strong

  1231   induction principles. *}

  1232 

  1233 definition 

  1234   fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)

  1235 where 

  1236   "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"

  1237 

  1238 lemma fresh_star_prod:

  1239   fixes as::"atom set"

  1240   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 

  1241   by (auto simp add: fresh_star_def fresh_Pair)

  1242 

  1243 lemma fresh_star_union:

  1244   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"

  1245   by (auto simp add: fresh_star_def)

  1246 

  1247 lemma fresh_star_insert:

  1248   shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"

  1249   by (auto simp add: fresh_star_def)

  1250 

  1251 lemma fresh_star_Un_elim:

  1252   "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"

  1253   unfolding fresh_star_def

  1254   apply(rule)

  1255   apply(erule meta_mp)

  1256   apply(auto)

  1257   done

  1258 

  1259 lemma fresh_star_insert_elim:

  1260   "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"

  1261   unfolding fresh_star_def

  1262   by rule (simp_all add: fresh_star_def)

  1263 

  1264 lemma fresh_star_empty_elim:

  1265   "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"

  1266   by (simp add: fresh_star_def)

  1267 

  1268 lemma fresh_star_unit_elim: 

  1269   shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"

  1270   by (simp add: fresh_star_def fresh_Unit) 

  1271 

  1272 lemma fresh_star_prod_elim: 

  1273   shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"

  1274   by (rule, simp_all add: fresh_star_prod)

  1275 

  1276 lemma fresh_star_zero:

  1277   shows "as \<sharp>* (0::perm)"

  1278   unfolding fresh_star_def

  1279   by (simp add: fresh_zero_perm)

  1280 

  1281 lemma fresh_star_plus:

  1282   fixes p q::perm

  1283   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"

  1284   unfolding fresh_star_def

  1285   by (simp add: fresh_plus_perm)

  1286 

  1287 lemma fresh_star_permute_iff:

  1288   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"

  1289   unfolding fresh_star_def

  1290   by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)

  1291 

  1292 lemma fresh_star_eqvt:

  1293   shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"

  1294 unfolding fresh_star_def

  1295 unfolding Ball_def

  1296 apply(simp add: all_eqvt)

  1297 apply(subst permute_fun_def)

  1298 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)

  1299 done

  1300 

  1301 

  1302 section {* Induction principle for permutations *}

  1303 

  1304 

  1305 lemma perm_struct_induct[consumes 1, case_names zero swap]:

  1306   assumes S: "supp p \<subseteq> S"

  1307   and zero: "P 0"

  1308   and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"

  1309   shows "P p"

  1310 proof -

  1311   have "finite (supp p)" by (simp add: finite_supp)

  1312   then show "P p" using S

  1313   proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)

  1314     case (psubset p)

  1315     then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto

  1316     have as: "supp p \<subseteq> S" by fact

  1317     { assume "supp p = {}"

  1318       then have "p = 0" by (simp add: supp_perm expand_perm_eq)

  1319       then have "P p" using zero by simp

  1320     }

  1321     moreover

  1322     { assume "supp p \<noteq> {}"

  1323       then obtain a where a0: "a \<in> supp p" by blast

  1324       then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"

  1325         using as by (auto simp add: supp_atom supp_perm swap_atom)

  1326       let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"

  1327       have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)

  1328       moreover

  1329       have "a \<notin> supp ?q" by (simp add: supp_perm)

  1330       then have "supp ?q \<noteq> supp p" using a0 by auto

  1331       ultimately have "supp ?q \<subset> supp p" using a2 by auto

  1332       then have "P ?q" using ih by simp

  1333       moreover

  1334       have "supp ?q \<subseteq> S" using as a2 by simp

  1335       ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 

  1336       moreover 

  1337       have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)

  1338       ultimately have "P p" by simp

  1339     }

  1340     ultimately show "P p" by blast

  1341   qed

  1342 qed

  1343 

  1344 lemma perm_simple_struct_induct[case_names zero swap]:

  1345   assumes zero: "P 0"

  1346   and     swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"

  1347   shows "P p"

  1348 by (rule_tac S="supp p" in perm_struct_induct)

  1349    (auto intro: zero swap)

  1350 

  1351 lemma perm_subset_induct[consumes 1, case_names zero swap plus]:

  1352   assumes S: "supp p \<subseteq> S"

  1353   assumes zero: "P 0"

  1354   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"

  1355   assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"

  1356   shows "P p"

  1357 using S

  1358 by (induct p rule: perm_struct_induct)

  1359    (auto intro: zero plus swap simp add: supp_swap)

  1360 

  1361 lemma supp_perm_eq:

  1362   assumes "(supp x) \<sharp>* p"

  1363   shows "p \<bullet> x = x"

  1364 proof -

  1365   from assms have "supp p \<subseteq> {a. a \<sharp> x}"

  1366     unfolding supp_perm fresh_star_def fresh_def by auto

  1367   then show "p \<bullet> x = x"

  1368   proof (induct p rule: perm_struct_induct)

  1369     case zero

  1370     show "0 \<bullet> x = x" by simp

  1371   next

  1372     case (swap p a b)

  1373     then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all

  1374     then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)

  1375   qed

  1376 qed

  1377 

  1378 lemma supp_perm_eq_test:

  1379   assumes "(supp x) \<sharp>* p"

  1380   shows "p \<bullet> x = x"

  1381 proof -

  1382   from assms have "supp p \<subseteq> {a. a \<sharp> x}"

  1383     unfolding supp_perm fresh_star_def fresh_def by auto

  1384   then show "p \<bullet> x = x"

  1385   proof (induct p rule: perm_subset_induct)

  1386     case zero

  1387     show "0 \<bullet> x = x" by simp

  1388   next

  1389     case (swap a b)

  1390     then have "a \<sharp> x" "b \<sharp> x" by simp_all

  1391     then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)

  1392   next

  1393     case (plus p1 p2)

  1394     have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+

  1395     then show "(p1 + p2) \<bullet> x = x" by simp

  1396   qed

  1397 qed

  1398 

  1399 

  1400 section {* Avoiding of atom sets *}

  1401 

  1402 text {* 

  1403   For every set of atoms, there is another set of atoms

  1404   avoiding a finitely supported c and there is a permutation

  1405   which 'translates' between both sets.

  1406 *}

  1407 

  1408 lemma at_set_avoiding_aux:

  1409   fixes Xs::"atom set"

  1410   and   As::"atom set"

  1411   assumes b: "Xs \<subseteq> As"

  1412   and     c: "finite As"

  1413   shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"

  1414 proof -

  1415   from b c have "finite Xs" by (rule finite_subset)

  1416   then show ?thesis using b

  1417   proof (induct rule: finite_subset_induct)

  1418     case empty

  1419     have "0 \<bullet> {} \<inter> As = {}" by simp

  1420     moreover

  1421     have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)

  1422     ultimately show ?case by blast

  1423   next

  1424     case (insert x Xs)

  1425     then obtain p where

  1426       p1: "(p \<bullet> Xs) \<inter> As = {}" and 

  1427       p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast

  1428     from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast

  1429     with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast

  1430     hence px: "p \<bullet> x = x" unfolding supp_perm by simp

  1431     have "finite (As \<union> p \<bullet> Xs)"

  1432       using `finite As` `finite Xs`

  1433       by (simp add: permute_set_eq_image)

  1434     then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"

  1435       by (rule obtain_atom)

  1436     hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"

  1437       by simp_all

  1438     let ?q = "(x \<rightleftharpoons> y) + p"

  1439     have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"

  1440       unfolding insert_eqvt

  1441       using `p \<bullet> x = x` `sort_of y = sort_of x`

  1442       using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`

  1443       by (simp add: swap_atom swap_set_not_in)

  1444     have "?q \<bullet> insert x Xs \<inter> As = {}"

  1445       using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`

  1446       unfolding q by simp

  1447     moreover

  1448     have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"

  1449       using p2 unfolding q

  1450       by (intro subset_trans [OF supp_plus_perm])

  1451          (auto simp add: supp_swap)

  1452     ultimately show ?case by blast

  1453   qed

  1454 qed

  1455 

  1456 lemma at_set_avoiding:

  1457   assumes a: "finite Xs"

  1458   and     b: "finite (supp c)"

  1459   obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"

  1460   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]

  1461   unfolding fresh_star_def fresh_def by blast

  1462 

  1463 lemma at_set_avoiding2:

  1464   assumes "finite xs"

  1465   and     "finite (supp c)" "finite (supp x)"

  1466   and     "xs \<sharp>* x"

  1467   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"

  1468 using assms

  1469 apply(erule_tac c="(c, x)" in at_set_avoiding)

  1470 apply(simp add: supp_Pair)

  1471 apply(rule_tac x="p" in exI)

  1472 apply(simp add: fresh_star_prod)

  1473 apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")

  1474 apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]

  1475 apply(auto simp add: fresh_star_def fresh_def)

  1476 done

  1477 

  1478 lemma at_set_avoiding2_atom:

  1479   assumes "finite (supp c)" "finite (supp x)"

  1480   and     b: "a \<sharp> x"

  1481   shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"

  1482 proof -

  1483   have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)

  1484   obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"

  1485     using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast

  1486   have c: "(p \<bullet> a) \<sharp> c" using p1

  1487     unfolding fresh_star_def Ball_def 

  1488     by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)

  1489   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast

  1490   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast

  1491 qed

  1492 

  1493 

  1494 section {* Concrete Atoms Types *}