equal
deleted
inserted
replaced
425 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
425 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
426 assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
426 assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
427 shows "P p" |
427 shows "P p" |
428 sorry |
428 sorry |
429 |
429 |
|
430 lemma tt1: |
|
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 |
430 |
459 |
431 lemma tt: |
460 lemma tt: |
432 "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
461 "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
433 apply(induct p rule: perm_induct_test) |
462 apply(induct p rule: perm_induct_test) |
434 apply(simp) |
463 apply(simp) |