817 unfolding card_fset remove_fset in_fset |
817 unfolding card_fset remove_fset in_fset |
818 by (rule card_Diff2_less[OF finite_fset]) |
818 by (rule card_Diff2_less[OF finite_fset]) |
819 |
819 |
820 lemma card_remove_fset_le1: |
820 lemma card_remove_fset_le1: |
821 shows "card_fset (remove_fset x xs) \<le> card_fset xs" |
821 shows "card_fset (remove_fset x xs) \<le> card_fset xs" |
822 unfolding remove_fset card_fset |
822 by simp |
823 by (rule card_Diff1_le[OF finite_fset]) |
|
824 |
823 |
825 lemma card_psubset_fset: |
824 lemma card_psubset_fset: |
826 shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs" |
825 shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs" |
827 unfolding card_fset psubset_fset subset_fset |
826 unfolding card_fset psubset_fset subset_fset |
828 by (rule card_psubset[OF finite_fset]) |
827 by (rule card_psubset[OF finite_fset]) |
833 by (rule card_image_le[OF finite_fset]) |
832 by (rule card_image_le[OF finite_fset]) |
834 |
833 |
835 lemma card_minus_insert_fset[simp]: |
834 lemma card_minus_insert_fset[simp]: |
836 assumes "a |\<in>| A" and "a |\<notin>| B" |
835 assumes "a |\<in>| A" and "a |\<notin>| B" |
837 shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1" |
836 shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1" |
838 using assms |
837 using assms by (simp add: in_fset card_fset) |
839 unfolding in_fset card_fset minus_fset |
|
840 by (simp add: card_Diff_insert[OF finite_fset]) |
|
841 |
838 |
842 lemma card_minus_subset_fset: |
839 lemma card_minus_subset_fset: |
843 assumes "B |\<subseteq>| A" |
840 assumes "B |\<subseteq>| A" |
844 shows "card_fset (A - B) = card_fset A - card_fset B" |
841 shows "card_fset (A - B) = card_fset A - card_fset B" |
845 using assms |
842 using assms |
846 unfolding subset_fset card_fset minus_fset |
843 by (simp add: subset_fset card_fset card_Diff_subset) |
847 by (rule card_Diff_subset[OF finite_fset]) |
|
848 |
844 |
849 lemma card_minus_fset: |
845 lemma card_minus_fset: |
850 shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)" |
846 shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)" |
851 unfolding inter_fset card_fset minus_fset |
847 by (simp add: card_fset card_Diff_subset_Int) |
852 by (rule card_Diff_subset_Int) (simp) |
|
853 |
848 |
854 |
849 |
855 subsection \<open>concat_fset\<close> |
850 subsection \<open>concat_fset\<close> |
856 |
851 |
857 lemma concat_empty_fset [simp]: |
852 lemma concat_empty_fset [simp]: |