427 end |
427 end |
428 |
428 |
429 lemma Not_eqvt: |
429 lemma Not_eqvt: |
430 shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))" |
430 shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))" |
431 by (simp add: permute_bool_def) |
431 by (simp add: permute_bool_def) |
|
432 |
|
433 lemma conj_eqvt: |
|
434 shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))" |
|
435 by (simp add: permute_bool_def) |
|
436 |
|
437 lemma imp_eqvt: |
|
438 shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))" |
|
439 by (simp add: permute_bool_def) |
|
440 |
|
441 lemma ex_eqvt: |
|
442 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
|
443 unfolding permute_fun_def permute_bool_def |
|
444 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
432 |
445 |
433 lemma permute_boolE: |
446 lemma permute_boolE: |
434 fixes P::"bool" |
447 fixes P::"bool" |
435 shows "p \<bullet> P \<Longrightarrow> P" |
448 shows "p \<bullet> P \<Longrightarrow> P" |
436 by (simp add: permute_bool_def) |
449 by (simp add: permute_bool_def) |
849 instance atom :: fs |
862 instance atom :: fs |
850 by default (simp add: supp_atom) |
863 by default (simp add: supp_atom) |
851 |
864 |
852 section {* Support for finite sets of atoms *} |
865 section {* Support for finite sets of atoms *} |
853 |
866 |
|
867 |
854 lemma supp_finite_atom_set: |
868 lemma supp_finite_atom_set: |
855 fixes S::"atom set" |
869 fixes S::"atom set" |
856 assumes "finite S" |
870 assumes "finite S" |
857 shows "supp S = S" |
871 shows "supp S = S" |
858 apply(rule finite_supp_unique) |
872 apply(rule finite_supp_unique) |
859 apply(simp add: supports_def) |
873 apply(simp add: supports_def) |
860 apply(simp add: swap_set_not_in) |
874 apply(simp add: swap_set_not_in) |
861 apply(rule assms) |
875 apply(rule assms) |
862 apply(simp add: swap_set_in) |
876 apply(simp add: swap_set_in) |
863 done |
877 done |
864 |
|
865 lemma supp_atom_insert: |
|
866 fixes S::"atom set" |
|
867 assumes a: "finite S" |
|
868 shows "supp (insert a S) = supp a \<union> supp S" |
|
869 using a by (simp add: supp_finite_atom_set supp_atom) |
|
870 |
878 |
871 section {* Type @{typ perm} is finitely-supported. *} |
879 section {* Type @{typ perm} is finitely-supported. *} |
872 |
880 |
873 lemma perm_swap_eq: |
881 lemma perm_swap_eq: |
874 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |
882 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |
1063 apply default |
1071 apply default |
1064 apply (induct_tac x) |
1072 apply (induct_tac x) |
1065 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1073 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1066 done |
1074 done |
1067 |
1075 |
|
1076 |
1068 section {* Support and freshness for applications *} |
1077 section {* Support and freshness for applications *} |
1069 |
1078 |
1070 lemma fresh_conv_MOST: |
1079 lemma fresh_conv_MOST: |
1071 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1080 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1072 unfolding fresh_def supp_def |
1081 unfolding fresh_def supp_def |
1108 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1117 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1109 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1118 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1110 unfolding fresh_def |
1119 unfolding fresh_def |
1111 using supp_fun_app by auto |
1120 using supp_fun_app by auto |
1112 qed |
1121 qed |
|
1122 |
|
1123 |
|
1124 section {* Support of Finite Sets of Finitely Supported Elements *} |
|
1125 |
|
1126 lemma Union_fresh: |
|
1127 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
|
1128 unfolding Union_image_eq[symmetric] |
|
1129 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
|
1130 apply(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt) |
|
1131 apply(subst permute_fun_app_eq) |
|
1132 back |
|
1133 apply(simp add: supp_eqvt) |
|
1134 apply(assumption) |
|
1135 done |
|
1136 |
|
1137 lemma Union_supports_set: |
|
1138 shows "(\<Union>x \<in> S. supp x) supports S" |
|
1139 proof - |
|
1140 { fix a b |
|
1141 have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S" |
|
1142 unfolding permute_set_eq by force |
|
1143 } |
|
1144 then show "(\<Union>x \<in> S. supp x) supports S" |
|
1145 unfolding supports_def |
|
1146 by (simp add: fresh_def[symmetric] swap_fresh_fresh) |
|
1147 qed |
|
1148 |
|
1149 lemma Union_of_fin_supp_sets: |
|
1150 fixes S::"('a::fs set)" |
|
1151 assumes fin: "finite S" |
|
1152 shows "finite (\<Union>x\<in>S. supp x)" |
|
1153 using fin by (induct) (auto simp add: finite_supp) |
|
1154 |
|
1155 lemma Union_included_in_supp: |
|
1156 fixes S::"('a::fs set)" |
|
1157 assumes fin: "finite S" |
|
1158 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
|
1159 proof - |
|
1160 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
|
1161 by (rule supp_finite_atom_set[symmetric]) |
|
1162 (rule Union_of_fin_supp_sets[OF fin]) |
|
1163 also have "\<dots> \<subseteq> supp S" |
|
1164 by (rule supp_subset_fresh) |
|
1165 (simp add: Union_fresh) |
|
1166 finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" . |
|
1167 qed |
|
1168 |
|
1169 lemma supp_of_fin_sets: |
|
1170 fixes S::"('a::fs set)" |
|
1171 assumes fin: "finite S" |
|
1172 shows "(supp S) = (\<Union>x\<in>S. supp x)" |
|
1173 apply(rule subset_antisym) |
|
1174 apply(rule supp_is_subset) |
|
1175 apply(rule Union_supports_set) |
|
1176 apply(rule Union_of_fin_supp_sets[OF fin]) |
|
1177 apply(rule Union_included_in_supp[OF fin]) |
|
1178 done |
|
1179 |
|
1180 lemma supp_of_fin_union: |
|
1181 fixes S T::"('a::fs) set" |
|
1182 assumes fin1: "finite S" |
|
1183 and fin2: "finite T" |
|
1184 shows "supp (S \<union> T) = supp S \<union> supp T" |
|
1185 using fin1 fin2 |
|
1186 by (simp add: supp_of_fin_sets) |
|
1187 |
|
1188 lemma supp_of_fin_insert: |
|
1189 fixes S::"('a::fs) set" |
|
1190 assumes fin: "finite S" |
|
1191 shows "supp (insert x S) = supp x \<union> supp S" |
|
1192 using fin |
|
1193 by (simp add: supp_of_fin_sets) |
1113 |
1194 |
1114 |
1195 |
1115 section {* Concrete atoms types *} |
1196 section {* Concrete atoms types *} |
1116 |
1197 |
1117 text {* |
1198 text {* |
1177 then obtain a :: 'a where "atom a \<notin> X" |
1258 then obtain a :: 'a where "atom a \<notin> X" |
1178 by auto |
1259 by auto |
1179 thus ?thesis .. |
1260 thus ?thesis .. |
1180 qed |
1261 qed |
1181 |
1262 |
1182 lemma image_eqvt: |
|
1183 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
|
1184 unfolding permute_set_eq_image |
|
1185 unfolding permute_fun_def [where f=f] |
|
1186 by (simp add: image_image) |
|
1187 |
|
1188 lemma atom_image_cong: |
|
1189 shows "(atom ` X = atom ` Y) = (X = Y)" |
|
1190 apply(rule inj_image_eq_iff) |
|
1191 apply(simp add: inj_on_def) |
|
1192 done |
|
1193 |
|
1194 lemma atom_image_supp: |
|
1195 shows "supp S = supp (atom ` S)" |
|
1196 apply(simp add: supp_def) |
|
1197 apply(simp add: image_eqvt) |
|
1198 apply(subst (2) permute_fun_def) |
|
1199 apply(simp add: atom_eqvt) |
|
1200 apply(simp add: atom_image_cong) |
|
1201 done |
|
1202 |
|
1203 lemma supp_finite_set_at_base: |
1263 lemma supp_finite_set_at_base: |
1204 assumes a: "finite S" |
1264 assumes a: "finite S" |
1205 shows "supp S = atom ` S" |
1265 shows "supp S = atom ` S" |
1206 proof - |
1266 apply(simp add: supp_of_fin_sets[OF a]) |
1207 have fin: "finite (atom ` S)" using a by simp |
1267 apply(simp add: supp_at_base) |
1208 have "supp S = supp (atom ` S)" by (rule atom_image_supp) |
1268 apply(auto) |
1209 also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) |
1269 done |
1210 finally show "supp S = atom ` S" by simp |
1270 |
1211 qed |
|
1212 |
|
1213 lemma supp_at_base_insert: |
|
1214 fixes a::"'a::at_base" |
|
1215 assumes a: "finite S" |
|
1216 shows "supp (insert a S) = supp a \<union> supp S" |
|
1217 using a by (simp add: supp_finite_set_at_base supp_at_base) |
|
1218 |
1271 |
1219 section {* library functions for the nominal infrastructure *} |
1272 section {* library functions for the nominal infrastructure *} |
1220 use "nominal_library.ML" |
1273 use "nominal_library.ML" |
1221 |
1274 |
1222 end |
1275 |
|
1276 |
|
1277 end |