Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal-General/Nominal2_Base.thy
changeset 2565 6bf332360510
parent 2560 82e37a4595c7
equal deleted inserted replaced
2564:5be8e34c2c0e 2565:6bf332360510 
     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
 
     8 imports Main Infinite_Set
 
     8 imports Main Infinite_Set
 
       
     9         "~~/src/HOL/Quotient_Examples/FSet"
 
     9 uses ("nominal_library.ML")
 
    10 uses ("nominal_library.ML")
 
    10      ("nominal_atoms.ML")
 
    11      ("nominal_atoms.ML")
 
    11 begin
 
    12 begin
 
    12 
    13 
    13 section {* Atoms and Sorts *}
 
    14 section {* Atoms and Sorts *}
 
   502 lemma mem_eqvt:
 
   503 lemma mem_eqvt:
 
   503   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
 
   504   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
 
   504   unfolding mem_def
 
   505   unfolding mem_def
 
   505   by (simp add: permute_fun_app_eq)
 
   506   by (simp add: permute_fun_app_eq)
 
   506 
   507 
       
   508 lemma empty_eqvt:
 
       
   509   shows "p \<bullet> {} = {}"
 
       
   510   unfolding empty_def Collect_def
 
       
   511   by (simp add: permute_fun_def permute_bool_def)
 
       
   512 
   507 lemma insert_eqvt:
 
   513 lemma insert_eqvt:
 
   508   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
 
   514   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
 
   509   unfolding permute_set_eq_image image_insert ..
 
   515   unfolding permute_set_eq_image image_insert ..
 
   510 
   516 
   511 
   517 
   567 instance 
   573 instance 
   568 by (default) (induct_tac [!] x, simp_all)
 
   574 by (default) (induct_tac [!] x, simp_all)
 
   569 
   575 
   570 end
 
   576 end
 
   571 
   577 
       
   578 lemma set_eqvt:
 
       
   579   shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
 
       
   580   by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
 
       
   581 
   572 subsection {* Permutations for options *}
 
   582 subsection {* Permutations for options *}
 
   573 
   583 
   574 instantiation option :: (pt) pt
 
   584 instantiation option :: (pt) pt
 
   575 begin
 
   585 begin
 
   576 
   586 
   582 
   592 
   583 instance 
   593 instance 
   584 by (default) (induct_tac [!] x, simp_all)
 
   594 by (default) (induct_tac [!] x, simp_all)
 
   585 
   595 
   586 end
 
   596 end
 
       
   597 
       
   598 
       
   599 subsection {* Permutations for fsets *}
 
       
   600 
       
   601 lemma permute_fset_rsp[quot_respect]:
 
       
   602   shows "(op = ===> list_eq ===> list_eq) permute permute"
 
       
   603   unfolding fun_rel_def
 
       
   604   by (simp add: set_eqvt[symmetric])
 
       
   605 
       
   606 instantiation fset :: (pt) pt
 
       
   607 begin
 
       
   608 
       
   609 quotient_definition
 
       
   610   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 
       
   611 is
 
       
   612   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
       
   613 
       
   614 instance 
       
   615 proof
 
       
   616   fix x :: "'a fset" and p q :: "perm"
 
       
   617   show "0 \<bullet> x = x" by (descending) (simp)
 
       
   618   show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
 
       
   619 qed
 
       
   620 
       
   621 end
 
       
   622 
       
   623 lemma permute_fset [simp]:
 
       
   624   fixes S::"('a::pt) fset"
 
       
   625   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
 
       
   626   and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
 
       
   627   by (lifting permute_list.simps)
 
       
   628 
       
   629 
   587 
   630 
   588 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
 
   631 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
 
   589 
   632 
   590 instantiation char :: pt
 
   633 instantiation char :: pt
 
   591 begin
 
   634 begin
 
  1017   qed
 
  1060   qed
 
  1018 qed
 
  1061 qed
 
  1019 
  1062 
  1020 section {* Finite Support instances for other types *}
 
  1063 section {* Finite Support instances for other types *}
 
  1021 
  1064 
       
  1065 
  1022 subsection {* Type @{typ "'a \<times> 'b"} is finitely-supported. *}
 
  1066 subsection {* Type @{typ "'a \<times> 'b"} is finitely-supported. *}
 
  1023 
  1067 
  1024 lemma supp_Pair: 
  1068 lemma supp_Pair: 
  1025   shows "supp (x, y) = supp x \<union> supp y"
 
  1069   shows "supp (x, y) = supp x \<union> supp y"
 
  1026   by (simp add: supp_def Collect_imp_eq Collect_neg_eq)
 
  1070   by (simp add: supp_def Collect_imp_eq Collect_neg_eq)
 
  1034   by (simp add: supp_def)
 
  1078   by (simp add: supp_def)
 
  1035 
  1079 
  1036 lemma fresh_Unit:
 
  1080 lemma fresh_Unit:
 
  1037   shows "a \<sharp> ()"
 
  1081   shows "a \<sharp> ()"
 
  1038   by (simp add: fresh_def supp_Unit)
 
  1082   by (simp add: fresh_def supp_Unit)
 
  1039 
       
  1040 
       
  1041 
  1083 
  1042 instance prod :: (fs, fs) fs
 
  1084 instance prod :: (fs, fs) fs
 
  1043 apply default
 
  1085 apply default
 
  1044 apply (induct_tac x)
 
  1086 apply (induct_tac x)
 
  1045 apply (simp add: supp_Pair finite_supp)
 
  1087 apply (simp add: supp_Pair finite_supp)
 
  1046 done
 
  1088 done
 
  1047 
  1089 
       
  1090 
  1048 subsection {* Type @{typ "'a + 'b"} is finitely supported *}
 
  1091 subsection {* Type @{typ "'a + 'b"} is finitely supported *}
 
  1049 
  1092 
  1050 lemma supp_Inl: 
  1093 lemma supp_Inl: 
  1051   shows "supp (Inl x) = supp x"
 
  1094   shows "supp (Inl x) = supp x"
 
  1052   by (simp add: supp_def)
 
  1095   by (simp add: supp_def)
 
  1067 apply default
 
  1110 apply default
 
  1068 apply (induct_tac x)
 
  1111 apply (induct_tac x)
 
  1069 apply (simp_all add: supp_Inl supp_Inr finite_supp)
 
  1112 apply (simp_all add: supp_Inl supp_Inr finite_supp)
 
  1070 done
 
  1113 done
 
  1071 
  1114 
       
  1115 
  1072 subsection {* Type @{typ "'a option"} is finitely supported *}
 
  1116 subsection {* Type @{typ "'a option"} is finitely supported *}
 
  1073 
  1117 
  1074 lemma supp_None: 
  1118 lemma supp_None: 
  1075   shows "supp None = {}"
 
  1119   shows "supp None = {}"
 
  1076 by (simp add: supp_def)
 
  1120 by (simp add: supp_def)
 
  1090 instance option :: (fs) fs
 
  1134 instance option :: (fs) fs
 
  1091 apply default
 
  1135 apply default
 
  1092 apply (induct_tac x)
 
  1136 apply (induct_tac x)
 
  1093 apply (simp_all add: supp_None supp_Some finite_supp)
 
  1137 apply (simp_all add: supp_None supp_Some finite_supp)
 
  1094 done
 
  1138 done
 
       
  1139 
  1095 
  1140 
  1096 subsubsection {* Type @{typ "'a list"} is finitely supported *}
 
  1141 subsubsection {* Type @{typ "'a list"} is finitely supported *}
 
  1097 
  1142 
  1098 lemma supp_Nil: 
  1143 lemma supp_Nil: 
  1099   shows "supp [] = {}"
 
  1144   shows "supp [] = {}"
 
  1188   then show "(\<Union>x \<in> S. supp x) supports S"
 
  1233   then show "(\<Union>x \<in> S. supp x) supports S"
 
  1189     unfolding supports_def 
  1234     unfolding supports_def 
  1190     by (simp add: fresh_def[symmetric] swap_fresh_fresh)
 
  1235     by (simp add: fresh_def[symmetric] swap_fresh_fresh)
 
  1191 qed
 
  1236 qed
 
  1192 
  1237 
  1193 lemma Union_of_fin_supp_sets:
 
  1238 lemma Union_of_finite_supp_sets:
 
  1194   fixes S::"('a::fs set)"
 
  1239   fixes S::"('a::fs set)"
 
  1195   assumes fin: "finite S"   
  1240   assumes fin: "finite S"   
  1196   shows "finite (\<Union>x\<in>S. supp x)"
 
  1241   shows "finite (\<Union>x\<in>S. supp x)"
 
  1197   using fin by (induct) (auto simp add: finite_supp)
 
  1242   using fin by (induct) (auto simp add: finite_supp)
 
  1198 
  1243 
  1201   assumes fin: "finite S"
 
  1246   assumes fin: "finite S"
 
  1202   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 
  1247   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 
  1203 proof -
 
  1248 proof -
 
  1204   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
 
  1249   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
 
  1205     by (rule supp_finite_atom_set[symmetric])
 
  1250     by (rule supp_finite_atom_set[symmetric])
 
  1206        (rule Union_of_fin_supp_sets[OF fin])
 
  1251        (rule Union_of_finite_supp_sets[OF fin])
 
  1207   also have "\<dots> \<subseteq> supp S"
 
  1252   also have "\<dots> \<subseteq> supp S"
 
  1208     by (rule supp_subset_fresh)
 
  1253     by (rule supp_subset_fresh)
 
  1209        (simp add: Union_fresh)
 
  1254        (simp add: Union_fresh)
 
  1210   finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 
  1255   finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 
  1211 qed
 
  1256 qed
 
  1212 
  1257 
  1213 lemma supp_of_fin_sets:
 
  1258 lemma supp_of_finite_sets:
 
  1214   fixes S::"('a::fs set)"
 
  1259   fixes S::"('a::fs set)"
 
  1215   assumes fin: "finite S"
 
  1260   assumes fin: "finite S"
 
  1216   shows "(supp S) = (\<Union>x\<in>S. supp x)"
 
  1261   shows "(supp S) = (\<Union>x\<in>S. supp x)"
 
  1217 apply(rule subset_antisym)
 
  1262 apply(rule subset_antisym)
 
  1218 apply(rule supp_is_subset)
 
  1263 apply(rule supp_is_subset)
 
  1219 apply(rule Union_supports_set)
 
  1264 apply(rule Union_supports_set)
 
  1220 apply(rule Union_of_fin_supp_sets[OF fin])
 
  1265 apply(rule Union_of_finite_supp_sets[OF fin])
 
  1221 apply(rule Union_included_in_supp[OF fin])
 
  1266 apply(rule Union_included_in_supp[OF fin])
 
  1222 done
 
  1267 done
 
  1223 
  1268 
  1224 lemma supp_of_fin_union:
 
  1269 lemma finite_sets_supp:
 
       
  1270   fixes S::"('a::fs set)"
 
       
  1271   assumes "finite S"
 
       
  1272   shows "finite (supp S)"
 
       
  1273 using assms
 
       
  1274 by (simp only: supp_of_finite_sets Union_of_finite_supp_sets)
 
       
  1275 
       
  1276 lemma supp_of_finite_union:
 
  1225   fixes S T::"('a::fs) set"
 
  1277   fixes S T::"('a::fs) set"
 
  1226   assumes fin1: "finite S"
 
  1278   assumes fin1: "finite S"
 
  1227   and     fin2: "finite T"
 
  1279   and     fin2: "finite T"
 
  1228   shows "supp (S \<union> T) = supp S \<union> supp T"
 
  1280   shows "supp (S \<union> T) = supp S \<union> supp T"
 
  1229   using fin1 fin2
 
  1281   using fin1 fin2
 
  1230   by (simp add: supp_of_fin_sets)
 
  1282   by (simp add: supp_of_finite_sets)
 
  1231 
  1283 
  1232 lemma supp_of_fin_insert:
 
  1284 lemma supp_of_finite_insert:
 
  1233   fixes S::"('a::fs) set"
 
  1285   fixes S::"('a::fs) set"
 
  1234   assumes fin:  "finite S"
 
  1286   assumes fin:  "finite S"
 
  1235   shows "supp (insert x S) = supp x \<union> supp S"
 
  1287   shows "supp (insert x S) = supp x \<union> supp S"
 
  1236   using fin
 
  1288   using fin
 
  1237   by (simp add: supp_of_fin_sets)
 
  1289   by (simp add: supp_of_finite_sets)
 
       
  1290 
       
  1291 
       
  1292 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
       
  1293 
       
  1294 lemma fset_eqvt: 
       
  1295   shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
 
       
  1296   by (lifting set_eqvt)
 
       
  1297 
       
  1298 lemma supp_fset [simp]:
 
       
  1299   shows "supp (fset S) = supp S"
 
       
  1300   unfolding supp_def
 
       
  1301   by (simp add: fset_eqvt fset_cong)
 
       
  1302 
       
  1303 lemma supp_empty_fset [simp]:
 
       
  1304   shows "supp {||} = {}"
 
       
  1305   unfolding supp_def
 
       
  1306   by simp
 
       
  1307 
       
  1308 lemma supp_insert_fset [simp]:
 
       
  1309   fixes x::"'a::fs"
 
       
  1310   and   S::"'a fset"
 
       
  1311   shows "supp (insert_fset x S) = supp x \<union> supp S"
 
       
  1312   apply(subst supp_fset[symmetric])
 
       
  1313   apply(simp add: supp_fset supp_of_finite_insert)
 
       
  1314   done
 
       
  1315 
       
  1316 lemma fset_finite_supp:
 
       
  1317   fixes S::"('a::fs) fset"
 
       
  1318   shows "finite (supp S)"
 
       
  1319   by (induct S) (simp_all add: finite_supp)
 
       
  1320 
       
  1321 
       
  1322 instance fset :: (fs) fs
 
       
  1323   apply (default)
 
       
  1324   apply (rule fset_finite_supp)
 
       
  1325   done
 
  1238 
  1326 
  1239 
  1327 
  1240 section {* Fresh-Star *}
 
  1328 section {* Fresh-Star *}
 
  1241 
  1329 
  1242 
  1330 
  1575 qed
 
  1663 qed
 
  1576 
  1664 
  1577 lemma supp_finite_set_at_base:
 
  1665 lemma supp_finite_set_at_base:
 
  1578   assumes a: "finite S"
 
  1666   assumes a: "finite S"
 
  1579   shows "supp S = atom ` S"
 
  1667   shows "supp S = atom ` S"
 
  1580 apply(simp add: supp_of_fin_sets[OF a])
 
  1668 apply(simp add: supp_of_finite_sets[OF a])
 
  1581 apply(simp add: supp_at_base)
 
  1669 apply(simp add: supp_at_base)
 
  1582 apply(auto)
 
  1670 apply(auto)
 
  1583 done
 
  1671 done
 
  1584 
  1672 
  1585 section {* Infrastructure for concrete atom types *}
 
  1673 section {* Infrastructure for concrete atom types *}
nominal2