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/FSet.thy
changeset 2528 9bde8a508594
parent 2525 c848f93807b9
child 2529 775d0bfd99fd
equal deleted inserted replaced
2527:40187684fc16 2528:9bde8a508594 
     4 
     4 
     5 A reasoning infrastructure for the type of finite sets.
 
     5 A reasoning infrastructure for the type of finite sets.
 
     6 *)
 
     6 *)
 
     7 
     7 
     8 theory FSet
 
     8 theory FSet
 
     9 imports Quotient_List Quotient_Product
 
     9 imports Quotient_List
 
    10 begin
 
    10 begin
 
    11 
    11 
    12 text {* Definiton of List relation and the quotient type *}
 
    12 text {* Definiton of List relation and the quotient type *}
 
    13 
    13 
    14 fun
 
    14 fun
 
    24 
    24 
    25 quotient_type
 
    25 quotient_type
 
    26   'a fset = "'a list" / "list_eq"
 
    26   'a fset = "'a list" / "list_eq"
 
    27   by (rule list_eq_equivp)
 
    27   by (rule list_eq_equivp)
 
    28 
    28 
    29 text {* Raw definitions of membership, sublist, cardinality, 
    29 text {* Raw definitions of membership, sublist, cardinality,
 
    30   intersection
 
    30   intersection
 
    31 *}
 
    31 *}
 
    32 
    32 
    33 definition
 
    33 definition
 
    34   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 
    34   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 
   377   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
 
   377   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
 
   378   apply (induct x)
 
   378   apply (induct x)
 
   379   apply (auto)
 
   379   apply (auto)
 
   380   done
 
   380   done
 
   381 
   381 
   382 instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
 
   382 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 
   383 begin
 
   383 begin
 
   384 
   384 
   385 quotient_definition
 
   385 quotient_definition
 
   386   "bot :: 'a fset" is "[] :: 'a list"
 
   386   "bot :: 'a fset" is "[] :: 'a list"
 
   387 
   387 
   436   "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
   436   "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
   437 
   437 
   438 instance
 
   438 instance
 
   439 proof
 
   439 proof
 
   440   fix x y z :: "'a fset"
 
   440   fix x y z :: "'a fset"
 
   441   show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
 
   441   show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
 
   442     unfolding less_fset_def by (lifting sub_list_not_eq)
 
   442     unfolding less_fset_def by (lifting sub_list_not_eq)
 
   443   show "x |\<subseteq>| x" by (lifting sub_list_refl)
 
   443   show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
 
   444   show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
 
   444   show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
 
   445   show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
 
   445   show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
 
   446   show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
 
   446   show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
 
   447   show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
 
   447   show "x |\<inter>| y |\<subseteq>| x"
 
   448   show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
 
   448     by (descending) (simp add: sub_list_def memb_def[symmetric])
 
   449   show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
 
   449   show "x |\<inter>| y |\<subseteq>| y" 
       
   450     by (descending) (simp add: sub_list_def memb_def[symmetric])
 
       
   451   show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
       
   452     by (descending) (rule append_inter_distrib)
 
   450 next
 
   453 next
 
   451   fix x y z :: "'a fset"
 
   454   fix x y z :: "'a fset"
 
   452   assume a: "x |\<subseteq>| y"
 
   455   assume a: "x |\<subseteq>| y"
 
   453   assume b: "y |\<subseteq>| z"
 
   456   assume b: "y |\<subseteq>| z"
 
   454   show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
 
   457   show "x |\<subseteq>| z" using a b 
       
   458     by (descending) (simp add: sub_list_def)
 
   455 next
 
   459 next
 
   456   fix x y :: "'a fset"
 
   460   fix x y :: "'a fset"
 
   457   assume a: "x |\<subseteq>| y"
 
   461   assume a: "x |\<subseteq>| y"
 
   458   assume b: "y |\<subseteq>| x"
 
   462   assume b: "y |\<subseteq>| x"
 
   459   show "x = y" using a b by (lifting sub_list_list_eq)
 
   463   show "x = y" using a b 
       
   464     by (descending) (unfold sub_list_def list_eq.simps, blast)
 
   460 next
 
   465 next
 
   461   fix x y z :: "'a fset"
 
   466   fix x y z :: "'a fset"
 
   462   assume a: "y |\<subseteq>| x"
 
   467   assume a: "y |\<subseteq>| x"
 
   463   assume b: "z |\<subseteq>| x"
 
   468   assume b: "z |\<subseteq>| x"
 
   464   show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
 
   469   show "y |\<union>| z |\<subseteq>| x" using a b 
       
   470     by (descending) (simp add: sub_list_def)
 
   465 next
 
   471 next
 
   466   fix x y z :: "'a fset"
 
   472   fix x y z :: "'a fset"
 
   467   assume a: "x |\<subseteq>| y"
 
   473   assume a: "x |\<subseteq>| y"
 
   468   assume b: "x |\<subseteq>| z"
 
   474   assume b: "x |\<subseteq>| z"
 
   469   show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
 
   475   show "x |\<subseteq>| y |\<inter>| z" using a b 
       
   476     by (descending) (simp add: sub_list_def memb_def[symmetric])
 
   470 qed
 
   477 qed
 
   471 
   478 
   472 end
 
   479 end
 
   473 
   480 
   474 section {* Finsert and Membership *}
 
   481 section {* Finsert and Membership *}
 
   540   apply (rule_tac b="x # b" in pred_compI)
 
   547   apply (rule_tac b="x # b" in pred_compI)
 
   541   apply auto
 
   548   apply auto
 
   542   apply (rule_tac b="x # ba" in pred_compI)
 
   549   apply (rule_tac b="x # ba" in pred_compI)
 
   543   apply auto
 
   550   apply auto
 
   544   done
 
   551   done
 
   545 
       
   546 lemma insert_preserve2:
 
       
   547   shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
 
       
   548          (id ---> rep_fset ---> abs_fset) op #"
 
       
   549   by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
 
       
   550 
   552 
   551 lemma [quot_preserve]:
 
   553 lemma [quot_preserve]:
 
   552   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
 
   554   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
 
   553   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
 
   555   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
 
   554       abs_o_rep[OF Quotient_fset] map_id finsert_def)
 
   556       abs_o_rep[OF Quotient_fset] map_id finsert_def)
 
   826 
   828 
   827 lemma not_fin_fnil: "x |\<notin>| {||}"
 
   829 lemma not_fin_fnil: "x |\<notin>| {||}"
 
   828   by (lifting not_memb_nil)
 
   830   by (lifting not_memb_nil)
 
   829 
   831 
   830 lemma fin_finsert_iff[simp]:
 
   832 lemma fin_finsert_iff[simp]:
 
   831   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
 
   833   "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
 
   832   by (lifting memb_cons_iff)
 
   834   by (descending) (simp add: memb_def)
 
   833 
   835 
   834 lemma
 
   836 lemma
 
   835   shows finsertI1: "x |\<in>| finsert x S"
 
   837   shows finsertI1: "x |\<in>| finsert x S"
 
   836   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
 
   838   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
 
   837   by (lifting memb_consI1, lifting memb_consI2)
 
   839   by (lifting memb_consI1 memb_consI2)
 
   838 
   840 
   839 lemma finsert_absorb[simp]:
 
   841 lemma finsert_absorb[simp]:
 
   840   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
 
   842   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
 
   841   by (lifting memb_absorb)
 
   843   by (descending) (auto simp add: memb_def)
 
   842 
   844 
   843 lemma fempty_not_finsert[simp]:
 
   845 lemma fempty_not_finsert[simp]:
 
   844   "{||} \<noteq> finsert x S"
 
   846   "{||} \<noteq> finsert x S"
 
   845   "finsert x S \<noteq> {||}"
 
   847   "finsert x S \<noteq> {||}"
 
   846   by (lifting nil_not_cons)
 
   848   by (lifting nil_not_cons)
 
   847 
   849 
   848 lemma finsert_left_comm:
 
   850 lemma finsert_left_comm:
 
   849   "finsert x (finsert y S) = finsert y (finsert x S)"
 
   851   "finsert x (finsert y S) = finsert y (finsert x S)"
 
   850   by (lifting cons_left_comm)
 
   852   by (descending) (auto)
 
   851 
   853 
   852 lemma finsert_left_idem:
 
   854 lemma finsert_left_idem:
 
   853   "finsert x (finsert x S) = finsert x S"
 
   855   "finsert x (finsert x S) = finsert x S"
 
   854   by (lifting cons_left_idem)
 
   856   by (descending) (auto)
 
   855 
   857 
   856 lemma fsingleton_eq[simp]:
 
   858 lemma fsingleton_eq[simp]:
 
   857   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
 
   859   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
 
   858   by (lifting singleton_list_eq)
 
   860   by (descending) (auto)
 
   859 
   861 
   860 
   862 
   861 text {* fset *}
 
   863 text {* fset *}
 
   862 
   864 
   863 lemma fset_simps[simp]:
 
   865 lemma fset_simps[simp]:
 
  1011 
  1013 
  1012 
  1014 
  1013 section {* fmap *}
 
  1015 section {* fmap *}
 
  1014 
  1016 
  1015 lemma fmap_simps[simp]:
 
  1017 lemma fmap_simps[simp]:
 
  1016   "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
 
  1018   fixes f::"'a \<Rightarrow> 'b"
 
  1017   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
 
  1019   shows "fmap f {||} = {||}"
 
       
  1020   and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
 
  1018   by (lifting map.simps)
 
  1021   by (lifting map.simps)
 
  1019 
  1022 
  1020 lemma fmap_set_image:
 
  1023 lemma fmap_set_image:
 
  1021   "fset (fmap f S) = f ` (fset S)"
 
  1024   "fset (fmap f S) = f ` (fset S)"
 
  1022   by (induct S) simp_all
 
  1025   by (induct S) simp_all
 
  1023 
  1026 
  1024 lemma inj_fmap_eq_iff:
 
  1027 lemma inj_fmap_eq_iff:
 
  1025   "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
 
  1028   "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
 
  1026   by (lifting inj_map_eq_iff)
 
  1029   by (lifting inj_map_eq_iff)
 
  1027 
  1030 
  1028 lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
 
  1031 lemma fmap_funion: 
       
  1032   shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
 
  1029   by (lifting map_append)
 
  1033   by (lifting map_append)
 
  1030 
  1034 
  1031 lemma fin_funion:
 
  1035 lemma fin_funion:
 
  1032   "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
 
  1036   shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
 
  1033   by (lifting memb_append)
 
  1037   by (lifting memb_append)
 
  1034 
  1038 
  1035 
  1039 
  1036 section {* fset *}
 
  1040 section {* fset *}
 
  1037 
  1041 
  1156 lemma fminus_red_fnotin[simp]: 
  1160 lemma fminus_red_fnotin[simp]: 
  1157   shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
 
  1161   shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
 
  1158   by (simp add: fminus_red)
 
  1162   by (simp add: fminus_red)
 
  1159 
  1163 
  1160 lemma fset_eq_iff:
 
  1164 lemma fset_eq_iff:
 
  1161   "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
 
  1165   shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
 
  1162   by (descending) (auto simp add: memb_def)
 
  1166   by (descending) (auto simp add: memb_def)
 
  1163 
  1167 
  1164 (* We cannot write it as "assumes .. shows" since Isabelle changes
 
  1168 (* We cannot write it as "assumes .. shows" since Isabelle changes
 
  1165    the quantifiers to schematic variables and reintroduces them in
 
  1169    the quantifiers to schematic variables and reintroduces them in
 
  1166    a different order *)
 
  1170    a different order *)
 
  1195 
  1199 
  1196 lemma fconcat_insert:
 
  1200 lemma fconcat_insert:
 
  1197   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 
  1201   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 
  1198   by (lifting concat.simps(2))
 
  1202   by (lifting concat.simps(2))
 
  1199 
  1203 
       
  1204 lemma 
       
  1205   shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
 
       
  1206   by (lifting concat_append)
 
       
  1207 
  1200 
  1208 
  1201 section {* ffilter *}
 
  1209 section {* ffilter *}
 
  1202 
  1210 
  1203 lemma subseteq_filter: 
  1211 lemma subseteq_filter: 
  1204   shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
 
  1212   shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
 
  1316   unfolding fsubseteq_set fcard_set fminus_set
 
  1324   unfolding fsubseteq_set fcard_set fminus_set
 
  1317   by (rule card_Diff_subset[OF finite_fset])
 
  1325   by (rule card_Diff_subset[OF finite_fset])
 
  1318 
  1326 
  1319 lemma fcard_fminus_subset_finter:
 
  1327 lemma fcard_fminus_subset_finter:
 
  1320   shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
 
  1328   shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
 
  1321   using assms 
       
  1322   unfolding finter_set fcard_set fminus_set
 
  1329   unfolding finter_set fcard_set fminus_set
 
  1323   by (rule card_Diff_subset_Int) (simp)
 
  1330   by (rule card_Diff_subset_Int) (simp)
 
  1324 
  1331 
  1325 
  1332 
  1326 lemma list_all2_refl:
 
  1333 lemma list_all2_refl:
 
  1392     then show "(list_all2 R OOO op \<approx>) r s"
 
  1399     then show "(list_all2 R OOO op \<approx>) r s"
 
  1393       using a c pred_compI by simp
 
  1400       using a c pred_compI by simp
 
  1394   qed
 
  1401   qed
 
  1395 qed
 
  1402 qed
 
  1396 
  1403 
       
  1404 
       
  1405 ML {*
 
       
  1406 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
 
       
  1407   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
       
  1408 *}
 
       
  1409 
  1397 no_notation
 
  1410 no_notation
 
  1398   list_eq (infix "\<approx>" 50)
 
  1411   list_eq (infix "\<approx>" 50)
 
  1399 
  1412 
  1400 
  1413 
  1401 end
 
  1414 end
nominal2