equal
deleted
inserted
replaced
1084 done |
1084 done |
1085 |
1085 |
1086 lemma length_eqvt [eqvt]: |
1086 lemma length_eqvt [eqvt]: |
1087 shows "p \<bullet> (length xs) = length (p \<bullet> xs)" |
1087 shows "p \<bullet> (length xs) = length (p \<bullet> xs)" |
1088 by (induct xs) (simp_all add: permute_pure) |
1088 by (induct xs) (simp_all add: permute_pure) |
|
1089 |
|
1090 |
|
1091 subsubsection {* Equivariance for @{typ "'a option"} *} |
|
1092 |
|
1093 lemma option_map_eqvt[eqvt]: |
|
1094 shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" |
|
1095 by (cases x) (simp_all, simp add: permute_fun_app_eq) |
1089 |
1096 |
1090 |
1097 |
1091 subsubsection {* Equivariance for @{typ "'a fset"} *} |
1098 subsubsection {* Equivariance for @{typ "'a fset"} *} |
1092 |
1099 |
1093 lemma in_fset_eqvt [eqvt]: |
1100 lemma in_fset_eqvt [eqvt]: |