65 primrec

    58 

    59 definition

    68   "fminus_raw ys [] = ys"

    62   "fminus_raw xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"

    69 | "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs"

    63 

    94   by (induct ys arbitrary: xs) (auto)

    88   by (auto simp add: fminus_raw_def)

    95 

   408 section {* Finsert and Membership *}

   401 

   402 section {* Definitions for fsets *}

   403 

   412 is "Cons"

   407   is "Cons"

   435 is

   430   is fcard_raw

   436   fcard_raw

   440 is

   434   is map

   441   map

   453   is "ffold_raw"

   446   is ffold_raw

   457 is

   450   is concat

   458   "concat"

   462 is

   454   is filter

   463   "filter"

   455 

   464 

   456 

   465 text {* Compositional Respectfullness and Preservation *}

   457 subsection {* Compositional Respectfulness and Preservation *}

   548 text {* Raw theorems. Finsert, memb, singleron, sub_list *}

   540 

   549 

   541 

   550 lemma nil_not_cons:

   542 section {* Cases *}

   551   shows "\<not> ([] \<approx> x # xs)"

   552   and   "\<not> (x # xs \<approx> [])"

   553   by auto

   554 

   555 lemma no_memb_nil:

   556   "(\<forall>x. \<not> memb x xs) = (xs = [])"

   557   by (simp add: memb_def)

   558 

   559 lemma memb_consI1:

   560   shows "memb x (x # xs)"

   561   by (simp add: memb_def)

   562 

   563 lemma memb_consI2:

   564   shows "memb x xs \<Longrightarrow> memb x (y # xs)"

   565   by (simp add: memb_def)

   566 

   567 lemma singleton_list_eq:

   568   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"

   569   by (simp)

   570 

   571 lemma sub_list_cons:

   572   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"

   573   by (auto simp add: memb_def sub_list_def)

   574 

   575 lemma fminus_raw_red: 

   576   "fminus_raw (x # xs) ys = (if x \<in> set ys then fminus_raw xs ys else x # (fminus_raw xs ys))"

   577   by (induct ys arbitrary: xs x) (simp_all)

   578 

   579 text {* Cardinality of finite sets *}

   580 

   581 (* used in memb_card_not_0 *)

   582 lemma fcard_raw_0:

   583   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"

   584   unfolding fcard_raw_def

   585   by (induct xs) (auto)

   586 

   587 (* used in list_eq2_equiv *)

   588 lemma memb_card_not_0:

   589   assumes a: "memb a A"

   590   shows "\<not>(fcard_raw A = 0)"

   591 proof -

   592   have "\<not>(\<forall>x. \<not> memb x A)" using a by auto

   593   then have "\<not>A \<approx> []" by (simp add: memb_def)

   594   then show ?thesis using fcard_raw_0[of A] by simp

   595 qed

   596 

   597 

   598 

   599 section {* ? *}

   612   have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)

   555   have c: "xs = [] \<Longrightarrow> thesis" using b unfolding memb_def

   556     by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)

   705       then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto

   631       then have "\<forall>x. \<not> memb x l" unfolding fcard_raw_def memb_def by auto

   706       then have z: "l = []" using no_memb_nil by auto

   632       then have z: "l = []" unfolding memb_def by auto

   721       have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp

   647       have f: "fcard_raw (removeAll a l) = m" using e d by (simp add: fcard_raw_def memb_def)

   734 text {* Lifted theorems *}

   660 

   735 

   661 section {* Lifted theorems *}

   736 lemma not_fin_fnil: "x |\<notin>| {||}"

   662 

   663 

   664 subsection {* fin *}

   665 

   666 lemma not_fin_fnil: 

   667   shows "x |\<notin>| {||}"

   740   "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"

   690   shows "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"

   746   by (lifting memb_consI1 memb_consI2)

   696   by (descending, simp add: memb_def)+

   753   "{||} \<noteq> finsert x S"

   703   shows "{||} \<noteq> finsert x S"

   754   "finsert x S \<noteq> {||}"

   704   and   "finsert x S \<noteq> {||}"

   755   by (lifting nil_not_cons)

   705   by (descending, simp)+

   758   "finsert x (finsert y S) = finsert y (finsert x S)"

   708   shows "finsert x (finsert y S) = finsert y (finsert x S)"

   762   "finsert x (finsert x S) = finsert x S"

   712   shows "finsert x (finsert x S) = finsert x S"

   770 text {* fset *}

   720 (* FIXME: is this in any case a useful lemma *)

   721 lemma fin_mdef:

   722   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"

   723   by (descending) (auto simp add: memb_def fminus_raw_def)

   724 

   725 

   726 subsection {* fset *}

   777 lemma fin_fset:

   733 lemma finite_fset [simp]: 

   778   "x \<in> fset S \<longleftrightarrow> x |\<in>| S"

   734   shows "finite (fset S)"

   779   by (lifting memb_def[symmetric])

   735   by (descending) (simp)

   780 

   736 

   781 lemma none_fin_fempty:

   737 lemma fset_cong:

   782   "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"

   738   shows "fset S = fset T \<longleftrightarrow> S = T"

   739   by (descending) (simp)

   740 

   741 lemma ffilter_set [simp]: 

   742   shows "fset (ffilter P xs) = P \<inter> fset xs"

   743   by (descending) (auto simp add: mem_def)

   744 

   745 lemma fdelete_set [simp]: 

   746   shows "fset (fdelete x xs) = fset xs - {x}"

   747   by (descending) (simp)

   748 

   749 lemma finter_set [simp]: 

   750   shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"

   751   by (lifting set_finter_raw)

   752 

   753 lemma funion_set [simp]: 

   754   shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"

   755   by (lifting set_append)

   756 

   757 lemma fminus_set [simp]: 

   758   shows "fset (xs - ys) = fset xs - fset ys"

   759   by (lifting set_fminus_raw)

   760 

   761 

   762 subsection {* funion *}

   763 

   764 lemmas [simp] =

   765   sup_bot_left[where 'a="'a fset", standard]

   766   sup_bot_right[where 'a="'a fset", standard]

   767 

   768 lemma funion_finsert[simp]:

   769   shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"

   770   by (lifting append.simps(2))

   771 

   772 lemma singleton_funion_left:

   773   shows "{|a|} |\<union>| S = finsert a S"

   774   by simp

   775 

   776 lemma singleton_funion_right:

   777   shows "S |\<union>| {|a|} = finsert a S"

   778   by (subst sup.commute) simp

   779 

   780 lemma fin_funion:

   781   shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"

   785 lemma fset_cong:

   784 

   786   "S = T \<longleftrightarrow> fset S = fset T"

   785 subsection {* fminus *}

   787   by (lifting list_eq.simps)

   786 

   788 

   787 lemma fminus_fin: 

   789 

   788   shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"

   790 section {* fcard *}

   789   by (descending) (simp add: memb_def)

   790 

   791 lemma fminus_red: 

   792   shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"

   793   by (descending) (auto simp add: memb_def)

   794 

   795 lemma fminus_red_fin[simp]: 

   796   shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"

   797   by (simp add: fminus_red)

   798 

   799 lemma fminus_red_fnotin[simp]: 

   800   shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"

   801   by (simp add: fminus_red)

   802 

   803 lemma fin_fminus_fnotin: 

   804   shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"

   805   unfolding fin_set fminus_set

   806   by blast

   807 

   808 lemma fin_fnotin_fminus: 

   809   shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"

   810   unfolding fin_set fminus_set

   811   by blast

   812 

   813 

   814 section {* fdelete *}

   815 

   816 lemma fin_fdelete:

   817   shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"

   818   by (descending) (simp add: memb_def)

   819 

   820 lemma fnotin_fdelete:

   821   shows "x |\<notin>| fdelete x S"

   822   by (descending) (simp add: memb_def)

   823 

   824 lemma fnotin_fdelete_ident:

   825   shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"

   826   by (descending) (simp add: memb_def)

   827 

   828 lemma fset_fdelete_cases:

   829   shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"

   830   by (descending) (auto simp add: memb_def insert_absorb)

   831   

   832 

   833 section {* finter *}

   834 

   835 lemma finter_empty_l:

   836   shows "{||} |\<inter>| S = {||}"

   837   by simp

   838 

   839 lemma finter_empty_r:

   840   shows "S |\<inter>| {||} = {||}"

   841   by simp

   842 

   843 lemma finter_finsert:

   844   shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"

   845   by (descending) (simp add: memb_def)

   846 

   847 lemma fin_finter:

   848   shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"

   849   by (descending) (simp add: memb_def)

   850 

   851 

   852 subsection {* fsubset *}

   853 

   854 lemma fsubseteq_set: 

   855   shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"

   856   by (descending) (simp add: sub_list_def)

   857 

   858 lemma fsubset_set: 

   859   shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"

   860   unfolding less_fset_def 

   861   by (descending) (auto simp add: sub_list_def)

   862 

   863 lemma fsubseteq_finsert:

   864   shows "(finsert x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"

   865   by (descending) (simp add: sub_list_def memb_def)

   866 

   867 lemma fsubset_fin: 

   868   shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"

   869   by (descending) (auto simp add: sub_list_def memb_def)

   870 

   871 (* FIXME: no type ord *)

   872 (*

   873 lemma fsubset_finsert:

   874   shows "(finsert x xs) |\<subset>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subset>| ys"

   875   by (descending) (simp add: sub_list_def memb_def)

   876 *)

   877 

   878 lemma fsubseteq_fempty:

   879   shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"

   880   by (descending) (simp add: sub_list_def)

   881 

   882 (* also problem with ord *)

   883 lemma not_fsubset_fnil: 

   884   shows "\<not> xs |\<subset>| {||}"

   885   by (metis fset_simps(1) fsubset_set not_psubset_empty)

   886 

   887 

   888 section {* fmap *}

   889 

   890 lemma fmap_simps [simp]:

   891    shows "fmap f {||} = {||}"

   892   and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"

   893   by (descending, simp)+

   894 

   895 lemma fmap_set_image [simp]:

   896   shows "fset (fmap f S) = f ` (fset S)"

   897   by (descending) (simp)

   898 

   899 lemma inj_fmap_eq_iff:

   900   shows "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"

   901   by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)

   902 

   903 lemma fmap_funion: 

   904   shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"

   905   by (descending) (simp)

   906 

   907 

   908 subsection {* fcard *}

   909 

   910 lemma fcard_set: 

   911   shows "fcard xs = card (fset xs)"

   912   by (lifting fcard_raw_def)

   819   apply(simp add: fcard_raw_def memb_def)

   941   apply(auto simp add: fcard_raw_def memb_def)

   828   "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"

   950   shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"

   829   by (lifting fcard_raw_delete)

   951   by (descending) (simp add: fcard_raw_def memb_def)

   843 

   965 lemma fcard_mono: 

   844 section {* funion *}

   966   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"

   845 

   967   unfolding fcard_set fsubseteq_set

   846 lemmas [simp] =

   968   by (simp add: card_mono[OF finite_fset])

   847   sup_bot_left[where 'a="'a fset", standard]

   969 

   848   sup_bot_right[where 'a="'a fset", standard]

   970 lemma fcard_fsubset_eq: 

   849 

   971   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"

   850 lemma funion_finsert[simp]:

   972   unfolding fcard_set fsubseteq_set

   851   shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"

   973   by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)

   852   by (lifting append.simps(2))

   974 

   853 

   975 lemma psubset_fcard_mono: 

   854 lemma singleton_union_left:

   976   shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"

   855   shows "{|a|} |\<union>| S = finsert a S"

   977   unfolding fcard_set fsubset_set

   856   by simp

   978   by (rule psubset_card_mono[OF finite_fset])

   857 

   979 

   858 lemma singleton_union_right:

   980 lemma fcard_funion_finter: 

   859   shows "S |\<union>| {|a|} = finsert a S"

   981   shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"

   860   by (subst sup.commute) simp

   982   unfolding fcard_set funion_set finter_set

   983   by (rule card_Un_Int[OF finite_fset finite_fset])

   984 

   985 lemma fcard_funion_disjoint: 

   986   shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"

   987   unfolding fcard_set funion_set 

   988   apply (rule card_Un_disjoint[OF finite_fset finite_fset])

   989   by (metis finter_set fset_simps(1))

   990 

   991 lemma fcard_delete1_less: 

   992   shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"

   993   unfolding fcard_set fin_set fdelete_set 

   994   by (rule card_Diff1_less[OF finite_fset])

   995 

   996 lemma fcard_delete2_less: 

   997   shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"

   998   unfolding fcard_set fdelete_set fin_set

   999   by (rule card_Diff2_less[OF finite_fset])

  1000 

  1001 lemma fcard_delete1_le: 

  1002   shows "fcard (fdelete x xs) \<le> fcard xs"

  1003   unfolding fdelete_set fcard_set

  1004   by (rule card_Diff1_le[OF finite_fset])

  1005 

  1006 lemma fcard_psubset: 

  1007   shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"

  1008   unfolding fcard_set fsubseteq_set fsubset_set

  1009   by (rule card_psubset[OF finite_fset])

  1010 

  1011 lemma fcard_fmap_le: 

  1012   shows "fcard (fmap f xs) \<le> fcard xs"

  1013   unfolding fcard_set fmap_set_image

  1014   by (rule card_image_le[OF finite_fset])

  1015 

  1016 lemma fcard_fminus_finsert[simp]:

  1017   assumes "a |\<in>| A" and "a |\<notin>| B"

  1018   shows "fcard (A - finsert a B) = fcard (A - B) - 1"

  1019   using assms 

  1020   unfolding fin_set fcard_set fminus_set

  1021   by (simp add: card_Diff_insert[OF finite_fset])

  1022 

  1023 lemma fcard_fminus_fsubset:

  1024   assumes "B |\<subseteq>| A"

  1025   shows "fcard (A - B) = fcard A - fcard B"

  1026   using assms 

  1027   unfolding fsubseteq_set fcard_set fminus_set

  1028   by (rule card_Diff_subset[OF finite_fset])

  1029 

  1030 lemma fcard_fminus_subset_finter:

  1031   shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"

  1032   unfolding finter_set fcard_set fminus_set

  1033   by (rule card_Diff_subset_Int) (simp)

  1034 

  1035 

  1036 section {* fconcat *}

  1037 

  1038 lemma fconcat_fempty:

  1039   shows "fconcat {||} = {||}"

  1040   by (lifting concat.simps(1))

  1041 

  1042 lemma fconcat_finsert:

  1043   shows "fconcat (finsert x S) = x |\<union>| fconcat S"

  1044   by (lifting concat.simps(2))

  1045 

  1046 lemma fconcat_finter:

  1047   shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"

  1048   by (lifting concat_append)

  1049 

  1050 

  1051 section {* ffilter *}

  1052 

  1053 lemma subseteq_filter: 

  1054   shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"

  1055   by  (descending) (auto simp add: memb_def sub_list_def)

  1056 

  1057 lemma eq_ffilter: 

  1058   shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"

  1059   by (descending) (auto simp add: memb_def)

  1060 

  1061 lemma subset_ffilter:

  1062   shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"

  1063   unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)

  1064 

  1065 

  1066 subsection {* ffold *}

  1067 

  1068 lemma ffold_nil: 

  1069   shows "ffold f z {||} = z"

  1070   by (descending) (simp)

  1071 

  1072 lemma ffold_finsert: "ffold f z (finsert a A) =

  1073   (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"

  1074   by (descending) (simp add: memb_def)

  1075 

  1076 lemma fin_commute_ffold:

  1077   "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"

  1078   by (descending) (simp add: memb_def memb_commute_ffold_raw)

  1079 

  1080 

  1081 subsection {* Choice in fsets *}

  1082 

  1083 lemma fset_choice: 

  1084   assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"

  1085   shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"

  1086   using a

  1087   apply(descending)

  1088   using finite_set_choice

  1089   by (auto simp add: memb_def Ball_def)

  1090 

  1091 

  1092 (* FIXME: is that in any way useful *)  

  1093 

  1133 lemma finite_fset [simp]: 

  1183 

  1134   shows "finite (fset S)"

  1184 

  1135   by (induct S) auto

  1136 

  1137 lemma fset_choice: 

  1138   shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"

  1139   apply(descending)

  1140   apply(simp add: memb_def)

  1141   apply(rule finite_set_choice[simplified Ball_def])

  1142   apply(simp_all)

  1143   done

  1144 

  1145 lemma fsubseteq_fempty:

  1146   shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"

  1147   by (metis finter_empty_r le_iff_inf)

  1148 

  1149 lemma not_fsubset_fnil: 

  1150   shows "\<not> xs |\<subset>| {||}"

  1151   by (metis fset_simps(1) fsubset_set not_psubset_empty)

  1152   

  1153 lemma fcard_mono: 

  1154   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"

  1155   unfolding fcard_set fsubseteq_set

  1156   by (rule card_mono[OF finite_fset])

  1157 

  1158 lemma fcard_fseteq: 

  1159   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"

  1160   unfolding fcard_set fsubseteq_set

  1161   by (simp add: card_seteq[OF finite_fset] fset_cong)

  1162 

  1163 lemma psubset_fcard_mono: 

  1164   shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"

  1165   unfolding fcard_set fsubset_set

  1166   by (rule psubset_card_mono[OF finite_fset])

  1167 

  1168 lemma fcard_funion_finter: 

  1169   shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"

  1170   unfolding fcard_set funion_set finter_set

  1171   by (rule card_Un_Int[OF finite_fset finite_fset])

  1172 

  1173 lemma fcard_funion_disjoint: 

  1174   shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"

  1175   unfolding fcard_set funion_set 

  1176   apply (rule card_Un_disjoint[OF finite_fset finite_fset])

  1177   by (metis finter_set fset_simps(1))

  1178 

  1179 lemma fcard_delete1_less: 

  1180   shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"

  1181   unfolding fcard_set fin_set fdelete_set 

  1182   by (rule card_Diff1_less[OF finite_fset])

  1183 

  1184 lemma fcard_delete2_less: 

  1185   shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"

  1186   unfolding fcard_set fdelete_set fin_set

  1187   by (rule card_Diff2_less[OF finite_fset])

  1188 

  1189 lemma fcard_delete1_le: 

  1190   shows "fcard (fdelete x xs) \<le> fcard xs"

  1191   unfolding fdelete_set fcard_set

  1192   by (rule card_Diff1_le[OF finite_fset])

  1193 

  1194 lemma fcard_psubset: 

  1195   shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"

  1196   unfolding fcard_set fsubseteq_set fsubset_set

  1197   by (rule card_psubset[OF finite_fset])

  1198 

  1199 lemma fcard_fmap_le: 

  1200   shows "fcard (fmap f xs) \<le> fcard xs"

  1201   unfolding fcard_set  fmap_set_image

  1202   by (rule card_image_le[OF finite_fset])

  1203 

  1204 lemma fin_fminus_fnotin: 

  1205   shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"

  1206   unfolding fin_set fminus_set

  1207   by blast

  1208 

  1209 lemma fin_fnotin_fminus: 

  1210   shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"

  1211   unfolding fin_set fminus_set

  1212   by blast

  1213 

  1214 lemma fin_mdef:

  1215   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"

  1216   unfolding fin_set fset_simps fset_cong fminus_set

  1217   by blast

  1218 

  1219 lemma fcard_fminus_finsert[simp]:

  1220   assumes "a |\<in>| A" and "a |\<notin>| B"

  1221   shows "fcard (A - finsert a B) = fcard (A - B) - 1"

  1222   using assms 

  1223   unfolding fin_set fcard_set fminus_set

  1224   by (simp add: card_Diff_insert[OF finite_fset])

  1225 

  1226 lemma fcard_fminus_fsubset:

  1227   assumes "B |\<subseteq>| A"

  1228   shows "fcard (A - B) = fcard A - fcard B"

  1229   using assms 

  1230   unfolding fsubseteq_set fcard_set fminus_set

  1231   by (rule card_Diff_subset[OF finite_fset])

  1232 

  1233 lemma fcard_fminus_subset_finter:

  1234   shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"

  1235   unfolding finter_set fcard_set fminus_set

  1236   by (rule card_Diff_subset_Int) (simp)