# HG changeset patch # User kuncar # Date 1380311695 -7200 # Node ID ac0e4ca891f9f03622513f30386191d2029ba71d # Parent 51e81874b6f61b504dbe090e068a66542985357c tuned names diff -r 51e81874b6f6 -r ac0e4ca891f9 src/HOL/Library/FSet.thy --- 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) = (\x. x |\| A \ P x = Q x)" by transfer auto -lemma psubset_ffilter: +lemma pfsubset_ffilter: "(\x. x |\| A \ P x \ Q x) \ (x |\| A & \ P x & Q x) \ ffilter P A |\| 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)