equal
deleted
inserted
replaced
1 (* Title: Nominal2_Base |
1 (* Title: Nominal2_Base |
2 Authors: Brian Huffman, Christian Urban |
2 Authors: Christian Urban, Brian Huffman, Cezary Kaliszyk |
3 |
3 |
4 Basic definitions and lemma infrastructure for |
4 Basic definitions and lemma infrastructure for |
5 Nominal Isabelle. |
5 Nominal Isabelle. |
6 *) |
6 *) |
7 theory Nominal2_Base |
7 theory Nominal2_Base |
1108 |
1108 |
1109 lemma union_fset_eqvt [eqvt]: |
1109 lemma union_fset_eqvt [eqvt]: |
1110 shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))" |
1110 shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))" |
1111 by (induct S) (simp_all) |
1111 by (induct S) (simp_all) |
1112 |
1112 |
|
1113 lemma inter_fset_eqvt [eqvt]: |
|
1114 shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))" |
|
1115 apply(descending) |
|
1116 unfolding list_eq_def inter_list_def |
|
1117 apply(perm_simp) |
|
1118 apply(simp) |
|
1119 done |
|
1120 |
|
1121 lemma subset_fset_eqvt [eqvt]: |
|
1122 shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))" |
|
1123 apply(descending) |
|
1124 unfolding sub_list_def |
|
1125 apply(perm_simp) |
|
1126 apply(simp) |
|
1127 done |
|
1128 |
1113 lemma map_fset_eqvt [eqvt]: |
1129 lemma map_fset_eqvt [eqvt]: |
1114 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1130 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1115 by (lifting map_eqvt) |
1131 by (lifting map_eqvt) |
1116 |
1132 |
1117 |
1133 |