equal
deleted
inserted
replaced
1642 apply(rule at)+ |
1642 apply(rule at)+ |
1643 apply(rule cp_pt_inst) |
1643 apply(rule cp_pt_inst) |
1644 apply(rule pt) |
1644 apply(rule pt) |
1645 apply(rule at) |
1645 apply(rule at) |
1646 done |
1646 done |
|
1647 |
|
1648 lemma pt_fresh_star_eqvt: |
|
1649 fixes pi :: "'x prm" |
|
1650 and x :: "'a" |
|
1651 and a :: "'x set" |
|
1652 and b :: "'x list" |
|
1653 assumes pt: "pt TYPE('a) TYPE('x)" |
|
1654 and at: "at TYPE('x)" |
|
1655 shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)" |
|
1656 and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)" |
|
1657 by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at]) |
|
1658 |
|
1659 lemma pt_fresh_star_eqvt_ineq: |
|
1660 fixes pi::"'x prm" |
|
1661 and a::"'y set" |
|
1662 and b::"'y list" |
|
1663 and x::"'a" |
|
1664 assumes pta: "pt TYPE('a) TYPE('x)" |
|
1665 and ptb: "pt TYPE('y) TYPE('x)" |
|
1666 and at: "at TYPE('x)" |
|
1667 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" |
|
1668 and dj: "disjoint TYPE('y) TYPE('x)" |
|
1669 shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)" |
|
1670 and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)" |
|
1671 by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool) |
1647 |
1672 |
1648 lemma pt_fresh_bij1: |
1673 lemma pt_fresh_bij1: |
1649 fixes pi :: "'x prm" |
1674 fixes pi :: "'x prm" |
1650 and x :: "'a" |
1675 and x :: "'a" |
1651 and a :: "'x" |
1676 and a :: "'x" |