380 lemma perm_zero:

   381   assumes a: "\<forall>x::atom. p \<bullet> x = x"

   382   shows "p = 0"

   383 using a

   384 by (simp add: expand_perm_eq)

   385 

   386 fun

   387   add_perm 

   388 where

   389   "add_perm [] = 0"

   390 | "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"

   391 

   392 fun

   393   elem_perm

   394 where

   395   "elem_perm [] = {}"

   396 | "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"

   397 

   398 

   399 lemma add_perm_apend:

   400   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"

   401 apply(induct xs arbitrary: ys)

   402 apply(auto simp add: add_assoc)

   403 done

   404 

   405 lemma perm_list_exists:

   406   fixes p::perm

   407   shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"

   408 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)

   409 apply(rename_tac p)

   410 apply(case_tac "supp p = {}")

   411 apply(simp)

   412 apply(simp add: supp_perm)

   413 apply(drule perm_zero)

   414 apply(simp)

   415 apply(rule_tac x="[]" in exI)

   416 apply(simp add: supp_Nil)

   417 apply(subgoal_tac "\<exists>x. x \<in> supp p")

   418 defer

   419 apply(auto)[1]

   420 apply(erule exE)

   421 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)

   422 apply(drule mp)

   423 defer

   424 apply(erule exE)

   425 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)

   426 apply(simp add: add_perm_apend)

   427 apply(erule conjE)

   428 apply(drule sym)

   429 apply(simp)

   430 apply(simp add: expand_perm_eq)

   431 apply(simp add: supp_append)

   432 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)

   433 apply(rule conjI)

   434 prefer 2

   435 apply(auto)[1]

   436 apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))

   437 defer

   438 apply(rule psubset_card_mono)

   439 apply(simp add: finite_supp)

   440 apply(rule psubsetI)

   441 defer

   442 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")

   443 apply(blast)

   444 apply(simp add: supp_perm)

   445 defer

   446 apply(auto simp add: supp_perm)[1]

   447 apply(case_tac "x = xa")

   448 apply(simp)

   449 apply(case_tac "((- p) \<bullet> x) = xa")

   450 apply(simp)

   451 apply(case_tac "sort_of xa = sort_of x")

   452 apply(simp)

   453 apply(auto)[1]

   454 apply(simp)

   455 apply(simp)

   456 apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")

   457 apply(blast)

   458 apply(auto simp add: supp_perm)[1]

   459 apply(case_tac "x = xa")

   460 apply(simp)

   461 apply(case_tac "((- p) \<bullet> x) = xa")

   462 apply(simp)

   463 apply(case_tac "sort_of xa = sort_of x")

   464 apply(simp)

   465 apply(auto)[1]

   466 apply(simp)

   467 apply(simp)

   468 done

   469 

   470 lemma tt0:

   471   fixes p::perm

   472   shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"

   473 apply(auto simp add: fresh_star_def supp_perm fresh_def)

   474 done

   475 

   476 lemma uu0:

   477   shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"

   478 apply(induct xs rule: add_perm.induct)

   479 apply(simp)

   480 apply(simp add: swap_fresh_fresh)

   481 done

   482 

   483 lemma yy0:

   484   fixes xs::"(atom \<times> atom) list"

   485   shows "supp xs = elem_perm xs"

   486 apply(induct xs rule: elem_perm.induct)

   487 apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)

   488 done

   489 

   490 lemma tt1:

   491   shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"

   492 apply(drule tt0)

   493 apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")

   494 prefer 2

   495 apply(rule perm_list_exists)

   496 apply(erule exE)

   497 apply(simp only: yy0)

   498 apply(rule uu0)

   499 apply(auto)

   500 done

   501 

   512 apply(simp add: supp_perm)

   513 apply(drule perm_zero)

   514 apply(simp add: zero)

   515 apply(rotate_tac 3)