equal
deleted
inserted
replaced
463 by (metis permute_atom_def) |
463 by (metis permute_atom_def) |
464 |
464 |
465 lemma |
465 lemma |
466 fixes t1 s1::"'a::fs" |
466 fixes t1 s1::"'a::fs" |
467 and t2 s2::"'b::fs" |
467 and t2 s2::"'b::fs" |
468 assumes asm: "finite as" |
468 shows "Abs as t1 = Abs bs s1 \<longrightarrow> Abs (as \<union> cs) t1 = Abs (bs \<union> cs) s1" |
|
469 apply(subst abs_eq_iff) |
|
470 apply(subst abs_eq_iff) |
|
471 apply(subst alphas_abs) |
|
472 apply(subst alphas_abs) |
|
473 apply(subst alphas) |
|
474 apply(subst alphas) |
|
475 apply(rule impI) |
|
476 apply(erule exE | erule conjE)+ |
|
477 apply(rule_tac x="p" in exI) |
|
478 apply(simp) |
|
479 apply(rule conjI) |
|
480 apply(auto)[1] |
|
481 apply(rule conjI) |
|
482 apply(auto)[1] |
|
483 apply(simp add: fresh_star_def) |
|
484 apply(auto)[1] |
|
485 apply(simp add: union_eqvt) |
|
486 oops |
|
487 |
|
488 |
|
489 lemma |
|
490 fixes t1 s1::"'a::fs" |
|
491 and t2 s2::"'b::fs" |
469 shows "(Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)" |
492 shows "(Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)" |
470 apply(subst abs_eq_iff) |
493 apply(subst abs_eq_iff) |
471 apply(subst abs_eq_iff) |
494 apply(subst abs_eq_iff) |
472 apply(subst alphas_abs) |
495 apply(subst alphas_abs) |
473 apply(subst alphas_abs) |
496 apply(subst alphas_abs) |
483 oops |
506 oops |
484 |
507 |
485 |
508 |
486 |
509 |
487 (* support of concrete atom sets *) |
510 (* support of concrete atom sets *) |
|
511 |
|
512 lemma |
|
513 shows "Abs as t = Abs (supp t \<inter> as) t" |
|
514 apply(simp add: abs_eq_iff) |
|
515 apply(simp add: alphas_abs) |
|
516 apply(rule_tac x="0" in exI) |
|
517 apply(simp add: alphas) |
|
518 apply(auto) |
|
519 oops |
|
520 |
|
521 lemma |
|
522 assumes "finite S" |
|
523 shows "\<exists>q. supp q \<subseteq> S \<union> p \<bullet> S \<and> (\<forall>a \<in> S. q \<bullet> a = p \<bullet> a)" |
|
524 using assms |
|
525 apply(induct) |
|
526 apply(rule_tac x="0" in exI) |
|
527 apply(simp add: supp_zero_perm) |
|
528 apply(auto) |
|
529 apply(simp add: insert_eqvt) |
|
530 apply(rule_tac x="((p \<bullet> x) \<rightleftharpoons> x) + q" in exI) |
|
531 apply(rule conjI) |
|
532 apply(rule subset_trans) |
|
533 apply(rule supp_plus_perm) |
|
534 apply(simp add: supp_swap) |
|
535 apply(auto)[1] |
|
536 apply(simp) |
|
537 apply(rule conjI) |
|
538 apply(case_tac "q \<bullet> x = x") |
|
539 apply(simp) |
|
540 apply(simp add: supp_perm) |
|
541 apply(case_tac "x \<in> p \<bullet> F") |
|
542 sorry |
|
543 |
488 |
544 |
489 lemma supp_atom_image: |
545 lemma supp_atom_image: |
490 fixes as::"'a::at_base set" |
546 fixes as::"'a::at_base set" |
491 shows "supp (atom ` as) = supp as" |
547 shows "supp (atom ` as) = supp as" |
492 apply(simp add: supp_def) |
548 apply(simp add: supp_def) |