418 

   418 lemma perm_zero:

   419 thm supp_perm

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

   420 

   420   shows "p = 0"

   421 (* 

   421 using a

   422 by (simp add: expand_perm_eq)

   423 

   424 fun

   425   add_perm 

   426 where

   427   "add_perm [] = 0"

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

   429 

   430 lemma add_perm_apend:

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

   432 apply(induct xs arbitrary: ys)

   433 apply(auto simp add: add_assoc)

   434 done

   435 

   436 lemma

   437   fixes p::perm

   438   shows "\<exists>xs. p = add_perm xs"

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

   440 apply(rename_tac p)

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

   442 apply(simp)

   443 apply(simp add: supp_perm)

   444 apply(drule perm_zero)

   445 apply(simp)

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

   447 apply(simp)

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

   449 defer

   450 apply(auto)[1]

   451 apply(erule exE)

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

   453 apply(drule mp)

   454 defer

   455 apply(erule exE)

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

   457 apply(simp add: add_perm_apend)

   458 apply(drule sym)

   459 apply(simp)

   460 apply(simp add: expand_perm_eq)

   461 apply(rule psubset_card_mono)

   462 apply(simp add: finite_supp)

   463 apply(rule psubsetI)

   464 defer

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

   466 apply(blast)

   467 apply(simp add: supp_perm)

   468 apply(auto simp add: supp_perm)

   469 apply(case_tac "x = xa")

   470 apply(simp)

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

   472 apply(simp)

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

   474 apply(simp)

   475 apply(auto)[1]

   476 apply(simp)

   477 apply(simp)

   478 done

   479 

   480 lemma tt1:

   481   shows "(supp x) \<sharp>* add_perm xs \<Longrightarrow> (add_perm xs) \<bullet> x = x"

   482 apply(induct xs rule: add_perm.induct)

   483 apply(simp)

   484 apply(simp)

   485 apply(case_tac "a = b")

   486 apply(simp)

   487 apply(drule meta_mp)

   488 defer

   489 apply(simp)

   490 apply(rule swap_fresh_fresh)

   491 apply(simp add: fresh_def)

   492 apply(auto)[1]

   493 apply(simp add: fresh_star_def fresh_def supp_perm)

   494 apply(drule_tac x="a" in bspec)

   495 apply(simp)

   496 oops

   497 

   498 

   426   assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"

   504   assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"

   430 lemma tt1:

   514 

   431   assumes a: "finite (supp p)"

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

   433 using a

   434 unfolding fresh_star_def fresh_def

   435 apply(induct F\<equiv>"supp p" arbitrary: p rule: finite.induct)

   436 apply(simp add: supp_perm)

   437 defer

   438 apply(case_tac "a \<in> A")

   439 apply(simp add: insert_absorb)

   440 apply(subgoal_tac "A = supp p - {a}")

   441 prefer 2

   442 apply(blast)

   443 apply(case_tac "p \<bullet> a = a")

   444 apply(simp add: supp_perm)

   445 apply(drule_tac x="p + (((- p) \<bullet> a) \<rightleftharpoons> a)" in meta_spec)

   446 apply(simp)

   447 apply(drule meta_mp)

   448 apply(rule subset_antisym)

   449 apply(rule subsetI)

   450 apply(simp)

   451 apply(simp add: supp_perm)

   452 apply(case_tac "xa = p \<bullet> a")

   453 apply(simp)

   454 apply(case_tac "p \<bullet> a = (- p) \<bullet> a")

   455 apply(simp)

   456 defer

   457 apply(simp)

   458 oops