equal
deleted
inserted
replaced
585 also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp |
585 also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp |
586 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" . |
586 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" . |
587 then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast |
587 then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast |
588 qed |
588 qed |
589 |
589 |
590 lemma Abs_rename_list: |
590 lemma Abs_rename_lst: |
591 fixes x::"'a::fs" |
591 fixes x::"'a::fs" |
592 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
592 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
593 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
593 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
594 proof - |
594 proof - |
595 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |
595 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |