--- a/src/HOL/Library/FSet.thy Fri Sep 27 21:54:55 2013 +0200
+++ b/src/HOL/Library/FSet.thy Fri Sep 27 21:54:55 2013 +0200
@@ -214,19 +214,19 @@
lemmas fBex_disj_distrib = bex_disj_distrib[Transfer.transferred]
lemmas fBall_cong = ball_cong[Transfer.transferred]
lemmas fBex_cong = bex_cong[Transfer.transferred]
-lemmas subfsetI[intro!] = subsetI[Transfer.transferred]
-lemmas subfsetD[elim, intro?] = subsetD[Transfer.transferred]
-lemmas rev_subfsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred]
-lemmas subfsetCE[no_atp,elim] = subsetCE[Transfer.transferred]
-lemmas subfset_eq[no_atp] = subset_eq[Transfer.transferred]
-lemmas contra_subfsetD[no_atp] = contra_subsetD[Transfer.transferred]
-lemmas subfset_refl = subset_refl[Transfer.transferred]
-lemmas subfset_trans = subset_trans[Transfer.transferred]
+lemmas fsubsetI[intro!] = subsetI[Transfer.transferred]
+lemmas fsubsetD[elim, intro?] = subsetD[Transfer.transferred]
+lemmas rev_fsubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred]
+lemmas fsubsetCE[no_atp,elim] = subsetCE[Transfer.transferred]
+lemmas fsubset_eq[no_atp] = subset_eq[Transfer.transferred]
+lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred]
+lemmas fsubset_refl = subset_refl[Transfer.transferred]
+lemmas fsubset_trans = subset_trans[Transfer.transferred]
lemmas fset_rev_mp = set_rev_mp[Transfer.transferred]
lemmas fset_mp = set_mp[Transfer.transferred]
-lemmas subfset_not_subfset_eq[code] = subset_not_subset_eq[Transfer.transferred]
+lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred]
-lemmas subfset_antisym[intro!] = subset_antisym[Transfer.transferred]
+lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred]
lemmas fequalityD1 = equalityD1[Transfer.transferred]
lemmas fequalityD2 = equalityD2[Transfer.transferred]
lemmas fequalityE = equalityE[Transfer.transferred]
@@ -234,7 +234,7 @@
lemmas eqfset_imp_iff = eqset_imp_iff[Transfer.transferred]
lemmas eqfelem_imp_iff = eqelem_imp_iff[Transfer.transferred]
lemmas fempty_iff[simp] = empty_iff[Transfer.transferred]
-lemmas fempty_subfsetI[iff] = empty_subsetI[Transfer.transferred]
+lemmas fempty_fsubsetI[iff] = empty_subsetI[Transfer.transferred]
lemmas equalsffemptyI = equals0I[Transfer.transferred]
lemmas equalsffemptyD = equals0D[Transfer.transferred]
lemmas fBall_fempty[simp] = ball_empty[Transfer.transferred]
@@ -265,7 +265,7 @@
lemmas finsertI2 = insertI2[Transfer.transferred]
lemmas finsertE[elim!] = insertE[Transfer.transferred]
lemmas finsertCI[intro!] = insertCI[Transfer.transferred]
-lemmas subfset_finsert_iff = subset_insert_iff[Transfer.transferred]
+lemmas fsubset_finsert_iff = subset_insert_iff[Transfer.transferred]
lemmas finsert_ident = insert_ident[Transfer.transferred]
lemmas fsingletonI[intro!,no_atp] = singletonI[Transfer.transferred]
lemmas fsingletonD[dest!,no_atp] = singletonD[Transfer.transferred]
@@ -273,7 +273,7 @@
lemmas fsingleton_inject[dest!] = singleton_inject[Transfer.transferred]
lemmas fsingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred]
lemmas fsingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred]
-lemmas subfset_fsingletonD = subset_singletonD[Transfer.transferred]
+lemmas fsubset_fsingletonD = subset_singletonD[Transfer.transferred]
lemmas fminus_single_finsert = diff_single_insert[Transfer.transferred]
lemmas fdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred]
lemmas funion_fsingleton_iff = Un_singleton_iff[Transfer.transferred]
@@ -285,43 +285,43 @@
lemmas Compr_fimage_eq = Compr_image_eq[Transfer.transferred]
lemmas fimage_funion = image_Un[Transfer.transferred]
lemmas fimage_iff = image_iff[Transfer.transferred]
-lemmas fimage_subfset_iff[no_atp] = image_subset_iff[Transfer.transferred]
-lemmas fimage_subfsetI = image_subsetI[Transfer.transferred]
+lemmas fimage_fsubset_iff[no_atp] = image_subset_iff[Transfer.transferred]
+lemmas fimage_fsubsetI = image_subsetI[Transfer.transferred]
lemmas fimage_ident[simp] = image_ident[Transfer.transferred]
lemmas split_if_fmem1 = split_if_mem1[Transfer.transferred]
lemmas split_if_fmem2 = split_if_mem2[Transfer.transferred]
-lemmas psubfsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
-lemmas psubfsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
-lemmas psubfset_finsert_iff = psubset_insert_iff[Transfer.transferred]
-lemmas psubfset_eq = psubset_eq[Transfer.transferred]
-lemmas psubfset_imp_subfset = psubset_imp_subset[Transfer.transferred]
-lemmas psubfset_trans = psubset_trans[Transfer.transferred]
-lemmas psubfsetD = psubsetD[Transfer.transferred]
-lemmas psubfset_subfset_trans = psubset_subset_trans[Transfer.transferred]
-lemmas subfset_psubfset_trans = subset_psubset_trans[Transfer.transferred]
-lemmas psubfset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred]
+lemmas pfsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
+lemmas pfsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
+lemmas pfsubset_finsert_iff = psubset_insert_iff[Transfer.transferred]
+lemmas pfsubset_eq = psubset_eq[Transfer.transferred]
+lemmas pfsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred]
+lemmas pfsubset_trans = psubset_trans[Transfer.transferred]
+lemmas pfsubsetD = psubsetD[Transfer.transferred]
+lemmas pfsubset_fsubset_trans = psubset_subset_trans[Transfer.transferred]
+lemmas fsubset_pfsubset_trans = subset_psubset_trans[Transfer.transferred]
+lemmas pfsubset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred]
lemmas fimage_fPow_mono = image_Pow_mono[Transfer.transferred]
lemmas fimage_fPow_surj = image_Pow_surj[Transfer.transferred]
-lemmas subfset_finsertI = subset_insertI[Transfer.transferred]
-lemmas subfset_finsertI2 = subset_insertI2[Transfer.transferred]
-lemmas subfset_finsert = subset_insert[Transfer.transferred]
+lemmas fsubset_finsertI = subset_insertI[Transfer.transferred]
+lemmas fsubset_finsertI2 = subset_insertI2[Transfer.transferred]
+lemmas fsubset_finsert = subset_insert[Transfer.transferred]
lemmas funion_upper1 = Un_upper1[Transfer.transferred]
lemmas funion_upper2 = Un_upper2[Transfer.transferred]
lemmas funion_least = Un_least[Transfer.transferred]
lemmas finter_lower1 = Int_lower1[Transfer.transferred]
lemmas finter_lower2 = Int_lower2[Transfer.transferred]
lemmas finter_greatest = Int_greatest[Transfer.transferred]
-lemmas fminus_subfset = Diff_subset[Transfer.transferred]
-lemmas fminus_subfset_conv = Diff_subset_conv[Transfer.transferred]
-lemmas subfset_fempty[simp] = subset_empty[Transfer.transferred]
-lemmas not_psubfset_fempty[iff] = not_psubset_empty[Transfer.transferred]
+lemmas fminus_fsubset = Diff_subset[Transfer.transferred]
+lemmas fminus_fsubset_conv = Diff_subset_conv[Transfer.transferred]
+lemmas fsubset_fempty[simp] = subset_empty[Transfer.transferred]
+lemmas not_pfsubset_fempty[iff] = not_psubset_empty[Transfer.transferred]
lemmas finsert_is_funion = insert_is_Un[Transfer.transferred]
lemmas finsert_not_fempty[simp] = insert_not_empty[Transfer.transferred]
lemmas fempty_not_finsert = empty_not_insert[Transfer.transferred]
lemmas finsert_absorb = insert_absorb[Transfer.transferred]
lemmas finsert_absorb2[simp] = insert_absorb2[Transfer.transferred]
lemmas finsert_commute = insert_commute[Transfer.transferred]
-lemmas finsert_subfset[simp] = insert_subset[Transfer.transferred]
+lemmas finsert_fsubset[simp] = insert_subset[Transfer.transferred]
lemmas finsert_inter_finsert[simp] = insert_inter_insert[Transfer.transferred]
lemmas finsert_disjoint[simp,no_atp] = insert_disjoint[Transfer.transferred]
lemmas disjoint_finsert[simp,no_atp] = disjoint_insert[Transfer.transferred]
@@ -334,8 +334,8 @@
lemmas fimage_is_fempty[iff] = image_is_empty[Transfer.transferred]
lemmas fempty_is_fimage[iff] = empty_is_image[Transfer.transferred]
lemmas fimage_cong = image_cong[Transfer.transferred]
-lemmas fimage_finter_subfset = image_Int_subset[Transfer.transferred]
-lemmas fimage_fminus_subfset = image_diff_subset[Transfer.transferred]
+lemmas fimage_finter_fsubset = image_Int_subset[Transfer.transferred]
+lemmas fimage_fminus_fsubset = image_diff_subset[Transfer.transferred]
lemmas finter_absorb = Int_absorb[Transfer.transferred]
lemmas finter_left_absorb = Int_left_absorb[Transfer.transferred]
lemmas finter_commute = Int_commute[Transfer.transferred]
@@ -349,7 +349,7 @@
lemmas disjoint_iff_fnot_equal = disjoint_iff_not_equal[Transfer.transferred]
lemmas finter_funion_distrib = Int_Un_distrib[Transfer.transferred]
lemmas finter_funion_distrib2 = Int_Un_distrib2[Transfer.transferred]
-lemmas finter_subfset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred]
+lemmas finter_fsubset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred]
lemmas funion_absorb = Un_absorb[Transfer.transferred]
lemmas funion_left_absorb = Un_left_absorb[Transfer.transferred]
lemmas funion_commute = Un_commute[Transfer.transferred]
@@ -371,9 +371,9 @@
lemmas funion_finter_distrib = Un_Int_distrib[Transfer.transferred]
lemmas funion_finter_distrib2 = Un_Int_distrib2[Transfer.transferred]
lemmas funion_finter_crazy = Un_Int_crazy[Transfer.transferred]
-lemmas subfset_funion_eq = subset_Un_eq[Transfer.transferred]
+lemmas fsubset_funion_eq = subset_Un_eq[Transfer.transferred]
lemmas funion_fempty[iff] = Un_empty[Transfer.transferred]
-lemmas funion_subfset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred]
+lemmas funion_fsubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred]
lemmas funion_fminus_finter = Un_Diff_Int[Transfer.transferred]
lemmas fminus_finter2 = Diff_Int2[Transfer.transferred]
lemmas funion_finter_assoc_eq = Un_Int_assoc_eq[Transfer.transferred]
@@ -407,11 +407,11 @@
lemmas fUNIV_bool[no_atp] = UNIV_bool[Transfer.transferred]
lemmas fPow_fempty[simp] = Pow_empty[Transfer.transferred]
lemmas fPow_finsert = Pow_insert[Transfer.transferred]
-lemmas funion_fPow_subfset = Un_Pow_subset[Transfer.transferred]
+lemmas funion_fPow_fsubset = Un_Pow_subset[Transfer.transferred]
lemmas fPow_finter_eq[simp] = Pow_Int_eq[Transfer.transferred]
-lemmas fset_eq_subfset = set_eq_subset[Transfer.transferred]
-lemmas subfset_iff[no_atp] = subset_iff[Transfer.transferred]
-lemmas subfset_iff_psubfset_eq = subset_iff_psubset_eq[Transfer.transferred]
+lemmas fset_eq_fsubset = set_eq_subset[Transfer.transferred]
+lemmas fsubset_iff[no_atp] = subset_iff[Transfer.transferred]
+lemmas fsubset_iff_pfsubset_eq = subset_iff_psubset_eq[Transfer.transferred]
lemmas all_not_fin_conv[simp] = all_not_in_conv[Transfer.transferred]
lemmas ex_fin_conv = ex_in_conv[Transfer.transferred]
lemmas fimage_mono = image_mono[Transfer.transferred]
@@ -477,7 +477,7 @@
"(ffilter P A = ffilter Q A) = (\<forall>x. x |\<in>| A \<longrightarrow> P x = Q x)"
by transfer auto
-lemma psubset_ffilter:
+lemma pfsubset_ffilter:
"(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A & \<not> P x & Q x) \<Longrightarrow>
ffilter P A |\<subset>| ffilter Q A"
unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
@@ -530,6 +530,8 @@
subsubsection {* fcard *}
+(* FIXME: improve transferred to handle bounded meta quantification *)
+
lemma fcard_fempty:
"fcard {||} = 0"
by transfer (rule card_empty)