6 *) |
6 *) |
7 theory Nominal2_Base |
7 theory Nominal2_Base |
8 imports Main |
8 imports Main |
9 "~~/src/HOL/Library/Infinite_Set" |
9 "~~/src/HOL/Library/Infinite_Set" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
|
11 "~~/src/HOL/Library/FinFun_Syntax" |
11 keywords |
12 keywords |
12 "atom_decl" "equivariance" :: thy_decl |
13 "atom_decl" "equivariance" :: thy_decl |
13 uses ("nominal_basics.ML") |
14 uses ("nominal_basics.ML") |
14 ("nominal_thmdecls.ML") |
15 ("nominal_thmdecls.ML") |
15 ("nominal_permeq.ML") |
16 ("nominal_permeq.ML") |
652 lemma fset_eqvt: |
653 lemma fset_eqvt: |
653 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
654 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
654 by (lifting set_eqvt) |
655 by (lifting set_eqvt) |
655 |
656 |
656 |
657 |
|
658 subsection {* Permutations for @{typ "'a \<Rightarrow>f 'b"} (FinFuns) *} |
|
659 |
|
660 instantiation finfun :: (pt, pt) pt |
|
661 begin |
|
662 |
|
663 definition "p \<bullet> f = Abs_finfun (p \<bullet> (finfun_apply f))" |
|
664 |
|
665 lemma Rep_finfun_permute: |
|
666 shows "p \<bullet> finfun_apply f \<in> finfun" |
|
667 apply(simp add: permute_fun_comp) |
|
668 apply(rule finfun_right_compose) |
|
669 apply(rule finfun_left_compose) |
|
670 apply(rule finfun_apply) |
|
671 apply(simp) |
|
672 done |
|
673 |
|
674 instance |
|
675 apply(default) |
|
676 apply(simp_all add: permute_finfun_def finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse) |
|
677 done |
|
678 |
|
679 end |
|
680 |
|
681 |
657 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} |
682 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} |
658 |
683 |
659 instantiation char :: pt |
684 instantiation char :: pt |
660 begin |
685 begin |
661 |
686 |
1187 done |
1212 done |
1188 |
1213 |
1189 lemma map_fset_eqvt [eqvt]: |
1214 lemma map_fset_eqvt [eqvt]: |
1190 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1215 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1191 by (lifting map_eqvt) |
1216 by (lifting map_eqvt) |
|
1217 |
|
1218 subsubsection {* Equivariance for @{typ "'a \<Rightarrow>f 'b"} *} |
|
1219 |
|
1220 lemma permute_finfun_update[simp, eqvt]: |
|
1221 "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)" |
|
1222 unfolding finfun_update_def |
|
1223 unfolding permute_finfun_def |
|
1224 apply(simp add: Abs_finfun_inverse fun_upd_finfun finfun_apply finfun_apply_inverse Rep_finfun_permute) |
|
1225 apply(simp add: fun_upd_def) |
|
1226 apply(perm_simp exclude: finfun_apply) |
|
1227 apply(rule refl) |
|
1228 done |
|
1229 |
|
1230 lemma permute_finfun_const[simp, eqvt]: |
|
1231 shows "(p \<bullet> (K$ b)) = (K$ (p \<bullet> b))" |
|
1232 unfolding finfun_const_def |
|
1233 unfolding permute_finfun_def |
|
1234 by (simp add: permute_finfun_def const_finfun finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse) |
|
1235 |
1192 |
1236 |
1193 |
1237 |
1194 section {* Supp, Freshness and Supports *} |
1238 section {* Supp, Freshness and Supports *} |
1195 |
1239 |
1196 context pt |
1240 context pt |
2182 by (simp add: supp_union_fset) |
2226 by (simp add: supp_union_fset) |
2183 |
2227 |
2184 instance fset :: (fs) fs |
2228 instance fset :: (fs) fs |
2185 apply (default) |
2229 apply (default) |
2186 apply (rule fset_finite_supp) |
2230 apply (rule fset_finite_supp) |
|
2231 done |
|
2232 |
|
2233 |
|
2234 subsection {* Type @{typ "'a \<Rightarrow>f 'b"} is finitely supported *} |
|
2235 |
|
2236 lemma fresh_finfun_const: |
|
2237 shows "a \<sharp> (K$ b) \<longleftrightarrow> a \<sharp> b" |
|
2238 by (simp add: fresh_def supp_def) |
|
2239 |
|
2240 lemma fresh_finfun_update: |
|
2241 shows "\<lbrakk>a \<sharp> f; a \<sharp> b; a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> f(b $:= x)" |
|
2242 unfolding fresh_conv_MOST |
|
2243 unfolding permute_finfun_update |
|
2244 by (elim MOST_rev_mp) (simp) |
|
2245 |
|
2246 lemma supp_finfun_const: |
|
2247 "supp (K$ b) = supp(b)" |
|
2248 by (simp add: supp_def) |
|
2249 |
|
2250 lemma supp_finfun_update: |
|
2251 "supp (f(a $:= b)) \<subseteq> supp(f, a, b)" |
|
2252 using fresh_finfun_update |
|
2253 by (auto simp add: fresh_def supp_Pair) |
|
2254 |
|
2255 instance finfun :: (fs, fs) fs |
|
2256 apply(default) |
|
2257 apply(induct_tac x rule: finfun_weak_induct) |
|
2258 apply(simp add: supp_finfun_const finite_supp) |
|
2259 apply(rule finite_subset) |
|
2260 apply(rule supp_finfun_update) |
|
2261 apply(simp add: supp_Pair finite_supp) |
2187 done |
2262 done |
2188 |
2263 |
2189 |
2264 |
2190 section {* Freshness and Fresh-Star *} |
2265 section {* Freshness and Fresh-Star *} |
2191 |
2266 |