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 "~~/src/HOL/Library/FinFun" |
12 keywords |
12 keywords |
13 "atom_decl" "equivariance" :: thy_decl |
13 "atom_decl" "equivariance" :: thy_decl |
14 uses ("nominal_basics.ML") |
14 uses ("nominal_basics.ML") |
15 ("nominal_thmdecls.ML") |
15 ("nominal_thmdecls.ML") |
16 ("nominal_permeq.ML") |
16 ("nominal_permeq.ML") |
653 lemma fset_eqvt: |
653 lemma fset_eqvt: |
654 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
654 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
655 by (lifting set_eqvt) |
655 by (lifting set_eqvt) |
656 |
656 |
657 |
657 |
658 subsection {* Permutations for @{typ "'a \<Rightarrow>f 'b"} (FinFuns) *} |
658 subsection {* Permutations for @{typ "('a, 'b) finfun"} *} |
659 |
659 |
660 instantiation finfun :: (pt, pt) pt |
660 instantiation finfun :: (pt, pt) pt |
661 begin |
661 begin |
662 |
662 |
663 definition "p \<bullet> f = Abs_finfun (p \<bullet> (finfun_apply f))" |
663 lift_definition |
664 |
664 permute_finfun :: "perm \<Rightarrow> ('a, 'b) finfun \<Rightarrow> ('a, 'b) finfun" |
665 lemma Rep_finfun_permute: |
665 is |
666 shows "p \<bullet> finfun_apply f \<in> finfun" |
666 "permute :: perm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" |
667 apply(simp add: permute_fun_comp) |
667 apply(simp add: permute_fun_comp) |
668 apply(rule finfun_right_compose) |
668 apply(rule finfun_right_compose) |
669 apply(rule finfun_left_compose) |
669 apply(rule finfun_left_compose) |
670 apply(rule finfun_apply) |
670 apply(assumption) |
671 apply(simp) |
671 apply(simp) |
672 done |
672 done |
673 |
673 |
674 instance |
674 instance |
675 apply(default) |
675 apply(default) |
676 apply(simp_all add: permute_finfun_def finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse) |
676 apply(transfer) |
|
677 apply(simp) |
|
678 apply(transfer) |
|
679 apply(simp) |
677 done |
680 done |
678 |
681 |
679 end |
682 end |
680 |
683 |
681 |
684 |
1123 lemma finite_eqvt [eqvt]: |
1126 lemma finite_eqvt [eqvt]: |
1124 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1127 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1125 unfolding finite_def |
1128 unfolding finite_def |
1126 by simp |
1129 by simp |
1127 |
1130 |
|
1131 lemma fun_upd_eqvt[eqvt]: |
|
1132 shows "p \<bullet> (f(x := y)) = (p \<bullet> f)((p \<bullet> x) := (p \<bullet> y))" |
|
1133 unfolding fun_upd_def |
|
1134 by (simp) |
|
1135 |
1128 |
1136 |
1129 subsubsection {* Equivariance for product operations *} |
1137 subsubsection {* Equivariance for product operations *} |
1130 |
1138 |
1131 lemma fst_eqvt [eqvt]: |
1139 lemma fst_eqvt [eqvt]: |
1132 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |
1140 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |
1213 |
1221 |
1214 lemma map_fset_eqvt [eqvt]: |
1222 lemma map_fset_eqvt [eqvt]: |
1215 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1223 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
1216 by (lifting map_eqvt) |
1224 by (lifting map_eqvt) |
1217 |
1225 |
1218 subsubsection {* Equivariance for @{typ "'a \<Rightarrow>f 'b"} *} |
1226 subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *} |
1219 |
1227 |
1220 lemma permute_finfun_update[simp, eqvt]: |
1228 lemma permute_finfun_update[eqvt]: |
1221 "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)" |
1229 shows "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)" |
1222 unfolding finfun_update_def |
1230 by (transfer) (simp) |
1223 unfolding permute_finfun_def |
1231 |
1224 apply(simp add: Abs_finfun_inverse fun_upd_finfun finfun_apply finfun_apply_inverse Rep_finfun_permute) |
1232 lemma permute_finfun_const[eqvt]: |
1225 apply(simp add: fun_upd_def) |
1233 shows "(p \<bullet> (finfun_const b)) = (finfun_const (p \<bullet> b))" |
1226 apply(perm_simp exclude: finfun_apply) |
1234 by (transfer) (simp) |
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 |
|
1236 |
1235 |
1237 |
1236 |
1238 section {* Supp, Freshness and Supports *} |
1237 section {* Supp, Freshness and Supports *} |
1239 |
1238 |
1240 context pt |
1239 context pt |
2229 apply (default) |
2228 apply (default) |
2230 apply (rule fset_finite_supp) |
2229 apply (rule fset_finite_supp) |
2231 done |
2230 done |
2232 |
2231 |
2233 |
2232 |
2234 subsection {* Type @{typ "'a \<Rightarrow>f 'b"} is finitely supported *} |
2233 subsection {* Type @{typ "('a, 'b) finfun"} is finitely supported *} |
2235 |
2234 |
2236 lemma fresh_finfun_const: |
2235 lemma fresh_finfun_const: |
2237 shows "a \<sharp> (K$ b) \<longleftrightarrow> a \<sharp> b" |
2236 shows "a \<sharp> (finfun_const b) \<longleftrightarrow> a \<sharp> b" |
2238 by (simp add: fresh_def supp_def) |
2237 by (simp add: fresh_def supp_def) |
2239 |
2238 |
2240 lemma fresh_finfun_update: |
2239 lemma fresh_finfun_update: |
2241 shows "\<lbrakk>a \<sharp> f; a \<sharp> b; a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> f(b $:= x)" |
2240 shows "\<lbrakk>a \<sharp> f; a \<sharp> x; a \<sharp> y\<rbrakk> \<Longrightarrow> a \<sharp> finfun_update f x y" |
2242 unfolding fresh_conv_MOST |
2241 unfolding fresh_conv_MOST |
2243 unfolding permute_finfun_update |
2242 unfolding permute_finfun_update |
2244 by (elim MOST_rev_mp) (simp) |
2243 by (elim MOST_rev_mp) (simp) |
2245 |
2244 |
2246 lemma supp_finfun_const: |
2245 lemma supp_finfun_const: |
2247 "supp (K$ b) = supp(b)" |
2246 shows "supp (finfun_const b) = supp(b)" |
2248 by (simp add: supp_def) |
2247 by (simp add: supp_def) |
2249 |
2248 |
2250 lemma supp_finfun_update: |
2249 lemma supp_finfun_update: |
2251 "supp (f(a $:= b)) \<subseteq> supp(f, a, b)" |
2250 shows "supp (finfun_update f x y) \<subseteq> supp(f, x, y)" |
2252 using fresh_finfun_update |
2251 using fresh_finfun_update |
2253 by (auto simp add: fresh_def supp_Pair) |
2252 by (auto simp add: fresh_def supp_Pair) |
2254 |
2253 |
2255 instance finfun :: (fs, fs) fs |
2254 instance finfun :: (fs, fs) fs |
2256 apply(default) |
2255 apply(default) |