Theory Regular_Tree_Relations.FSet_Utils
theory FSet_Utils
imports "HOL-Library.FSet"
"HOL-Library.List_Lexorder"
Ground_Terms
begin
context
includes fset.lifting
begin
lift_definition fCollect :: "('a ⇒ bool) ⇒ 'a fset" is "λ P. if finite (Collect P) then Collect P else {}"
by auto
lift_definition fSigma :: "'a fset ⇒ ('a ⇒ 'b fset) ⇒ ('a × 'b) fset" is Sigma
by auto
lift_definition is_fempty :: "'a fset ⇒ bool" is Set.is_empty .
lift_definition fremove :: "'a ⇒ 'a fset ⇒ 'a fset" is Set.remove
by (simp add: remove_def)
lift_definition finj_on :: "('a ⇒ 'b) ⇒ 'a fset ⇒ bool" is inj_on .
lift_definition the_finv_into :: "'a fset ⇒ ('a ⇒ 'b) ⇒ 'b ⇒ 'a" is the_inv_into .
lemma fCollect_memberI [intro!]:
"finite (Collect P) ⟹ P x ⟹ x |∈| fCollect P"
by transfer auto
lemma fCollect_member [iff]:
"x |∈| fCollect P ⟷ finite (Collect P) ∧ P x"
by transfer (auto split: if_splits)
lemma fCollect_cong: "(⋀x. P x = Q x) ⟹ fCollect P = fCollect Q"
by presburger
end
syntax
"_fColl" :: "pttrn ⇒ bool ⇒ 'a set" (‹(1{|_./ _|})›)
syntax_consts
"_fColl" ⇌ fCollect
translations
"{|x. P|}" ⇌ "CONST fCollect (λx. P)"
syntax (ASCII)
"_fCollect" :: "pttrn ⇒ 'a set ⇒ bool ⇒ 'a set" (‹(1{(_/|:| _)./ _})›)
syntax
"_fCollect" :: "pttrn ⇒ 'a set ⇒ bool ⇒ 'a set" (‹(1{(_/ |∈| _)./ _})›)
syntax_consts
"_fCollect" ⇌ fCollect
translations
"{p|:|A. P}" ⇀ "CONST fCollect (λp. p |∈| A ∧ P)"
syntax
"_fSetcompr" :: "'a ⇒ idts ⇒ bool ⇒ 'a fset" (‹(1{|_ |/_./ _|})›)
syntax_consts
"_fSetcompr" ⇌ fCollect
parse_translation ‹
let
val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", \<^const_syntax>‹Ex›));
fun nvars (Const (\<^syntax_const>‹_idts›, _) $ _ $ idts) = nvars idts + 1
| nvars _ = 1;
fun setcompr_tr ctxt [e, idts, b] =
let
val eq = Syntax.const \<^const_syntax>‹HOL.eq› $ Bound (nvars idts) $ e;
val P = Syntax.const \<^const_syntax>‹HOL.conj› $ eq $ b;
val exP = ex_tr ctxt [idts, P];
in Syntax.const \<^const_syntax>‹fCollect› $ absdummy dummyT exP end;
in [(\<^syntax_const>‹_fSetcompr›, setcompr_tr)] end
›
print_translation ‹
let
val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (\<^const_syntax>‹Ex›, "DUMMY"));
fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
let
fun check (Const (\<^const_syntax>‹Ex›, _) $ Abs (_, _, P), n) = check (P, n + 1)
| check (Const (\<^const_syntax>‹HOL.conj›, _) $
(Const (\<^const_syntax>‹HOL.eq›, _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (=) (0 upto (n - 1), add_loose_bnos (e, 0, []))
| check _ = false;
fun tr' (_ $ abs) =
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' ctxt [abs]
in Syntax.const \<^syntax_const>‹_fSetcompr› $ e $ idts $ Q end;
in
if check (P, 0) then tr' P
else
let
val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
val M = Syntax.const \<^syntax_const>‹_fColl› $ x $ t;
in
case t of
Const (\<^const_syntax>‹HOL.conj›, _) $
(Const (\<^const_syntax>‹fmember›, _) $
(Const (\<^syntax_const>‹_bound›, _) $ Free (yN, _)) $ A) $ P =>
if xN = yN then Syntax.const \<^syntax_const>‹_fCollect› $ x $ A $ P else M
| _ => M
end
end;
in [(\<^const_syntax>‹fCollect›, setcompr_tr')] end
›
syntax
"_fSigma" :: "pttrn ⇒ 'a fset ⇒ 'b fset ⇒ ('a × 'b) set" (‹(3fSIGMA _|:|_./ _)› [0, 0, 10] 10)
syntax_consts
"_fSigma" ⇌ fSigma
translations
"fSIGMA x|:|A. B" ⇌ "CONST fSigma A (λx. B)"
notation
ffUnion (‹|⋃|›)
context
includes fset.lifting
begin
lemma right_total_cr_fset [transfer_rule]:
"right_total cr_fset"
by (auto simp: cr_fset_def right_total_def)
lemma bi_unique_cr_fset [transfer_rule]:
"bi_unique cr_fset"
by (auto simp: bi_unique_def cr_fset_def fset_inject)
lemma right_total_pcr_fset_eq [transfer_rule]:
"right_total (pcr_fset (=))"
by (simp add: right_total_cr_fset fset.pcr_cr_eq)
lemma bi_unique_pcr_fset [transfer_rule]:
"bi_unique (pcr_fset (=))"
by (simp add: fset.pcr_cr_eq bi_unique_cr_fset)
lemma set_fset_of_list_transfer [transfer_rule]:
"rel_fun (list_all2 A) (pcr_fset A) set fset_of_list"
unfolding pcr_fset_def rel_set_def rel_fun_def
by (force simp: list_all2_conv_all_nth in_set_conv_nth cr_fset_def fset_of_list.rep_eq relcompp_apply)
lemma fCollectD: "a |∈| {|x . P x|} ⟹ P a"
by transfer (auto split: if_splits)
lemma fCollectI: "P a ⟹ finite (Collect P) ⟹ a |∈| {| x. P x|}"
by (auto intro: fCollect_memberI)
lemma fCollect_fempty_eq [simp]: "fCollect P = {||} ⟷ (∀x. ¬ P x) ∨ infinite (Collect P)"
by auto
lemma fempty_fCollect_eq [simp]: "{||} = fCollect P ⟷ (∀x. ¬ P x) ∨ infinite (Collect P)"
by auto
lemma fset_image_conv:
"{f x | x. x |∈| T} = fset (f |`| T)"
by transfer auto
lemma fimage_def:
"f |`| A = {| y. ∃x|∈|A. y = f x |}"
by transfer auto
lemma ffilter_simp: "ffilter P A = {a |∈| A. P a}"
by transfer auto
lemmas fset_list_fsubset_eq_nth_conv = set_list_subset_eq_nth_conv[Transfer.transferred]
lemmas mem_idx_fset_sound = mem_idx_sound[Transfer.transferred]
abbreviation fTimes :: "'a fset ⇒ 'b fset ⇒ ('a × 'b) fset" (infixr ‹|×|› 80)
where "A |×| B ≡ fSigma A (λ_. B)"
lemma fSigma_repeq:
"fset (A |×| B) = fset A × fset B"
by (transfer) auto
lemmas fSigmaI [intro!] = SigmaI[Transfer.transferred]
lemmas fSigmaE [elim!] = SigmaE[Transfer.transferred]
lemmas fSigmaD1 = SigmaD1[Transfer.transferred]
lemmas fSigmaD2 = SigmaD2[Transfer.transferred]
lemmas fSigmaE2 = SigmaE2[Transfer.transferred]
lemmas fSigma_cong = Sigma_cong[Transfer.transferred]
lemmas fSigma_mono = Sigma_mono[Transfer.transferred]
lemmas fSigma_empty1 [simp] = Sigma_empty1[Transfer.transferred]
lemmas fSigma_empty2 [simp] = Sigma_empty2[Transfer.transferred]
lemmas fmem_Sigma_iff [iff] = mem_Sigma_iff[Transfer.transferred]
lemmas fmem_Times_iff = mem_Times_iff[Transfer.transferred]
lemmas fSigma_empty_iff = Sigma_empty_iff[Transfer.transferred]
lemmas fTimes_subset_cancel2 = Times_subset_cancel2[Transfer.transferred]
lemmas fTimes_eq_cancel2 = Times_eq_cancel2[Transfer.transferred]
lemmas fUN_Times_distrib = UN_Times_distrib[Transfer.transferred]
lemmas fsplit_paired_Ball_Sigma [simp, no_atp] = split_paired_Ball_Sigma[Transfer.transferred]
lemmas fsplit_paired_Bex_Sigma [simp, no_atp] = split_paired_Bex_Sigma[Transfer.transferred]
lemmas fSigma_Un_distrib1 = Sigma_Un_distrib1[Transfer.transferred]
lemmas fSigma_Un_distrib2 = Sigma_Un_distrib2[Transfer.transferred]
lemmas fSigma_Int_distrib1 = Sigma_Int_distrib1[Transfer.transferred]
lemmas fSigma_Int_distrib2 = Sigma_Int_distrib2[Transfer.transferred]
lemmas fSigma_Diff_distrib1 = Sigma_Diff_distrib1[Transfer.transferred]
lemmas fSigma_Diff_distrib2 = Sigma_Diff_distrib2[Transfer.transferred]
lemmas fSigma_Union = Sigma_Union[Transfer.transferred]
lemmas fTimes_Un_distrib1 = Times_Un_distrib1[Transfer.transferred]
lemmas fTimes_Int_distrib1 = Times_Int_distrib1[Transfer.transferred]
lemmas fTimes_Diff_distrib1 = Times_Diff_distrib1[Transfer.transferred]
lemmas fTimes_empty [simp] = Times_empty[Transfer.transferred]
lemmas ftimes_subset_iff = times_subset_iff[Transfer.transferred]
lemmas ftimes_eq_iff = times_eq_iff[Transfer.transferred]
lemmas ffst_image_times [simp] = fst_image_times[Transfer.transferred]
lemmas fsnd_image_times [simp] = snd_image_times[Transfer.transferred]
lemmas fsnd_image_Sigma = snd_image_Sigma[Transfer.transferred]
lemmas finsert_Times_insert = insert_Times_insert[Transfer.transferred]
lemmas fTimes_Int_Times = Times_Int_Times[Transfer.transferred]
lemmas fimage_paired_Times = image_paired_Times[Transfer.transferred]
lemmas fproduct_swap = product_swap[Transfer.transferred]
lemmas fswap_product = swap_product[Transfer.transferred]
lemmas fsubset_fst_snd = subset_fst_snd[Transfer.transferred]
lemmas map_prod_ftimes = map_prod_times[Transfer.transferred]
lemma fCollect_case_prod [simp]:
"{|(a, b). P a ∧ Q b|} = fCollect P |×| fCollect Q"
by transfer (auto dest: finite_cartesian_productD1 finite_cartesian_productD2)
lemma fCollect_case_prodD:
"x |∈| {|(x, y). A x y|} ⟹ A (fst x) (snd x)"
by auto
lemmas fCollect_case_prod_Sigma = Collect_case_prod_Sigma[Transfer.transferred]
lemmas ffst_image_Sigma = fst_image_Sigma[Transfer.transferred]
lemmas fimage_split_eq_Sigma = image_split_eq_Sigma[Transfer.transferred]
lift_definition ftrancl :: "('a × 'a) fset ⇒ ('a × 'a) fset" (‹(_|⇧+|)› [1000] 999) is trancl
by auto
lemmas fr_into_trancl [intro, Pure.intro] = r_into_trancl[Transfer.transferred]
lemmas ftrancl_into_trancl [Pure.intro] = trancl_into_trancl[Transfer.transferred]
lemmas ftrancl_induct[consumes 1, case_names Base Step] = trancl.induct[Transfer.transferred]
lemmas ftrancl_mono = trancl_mono[Transfer.transferred]
lemmas ftrancl_trans[trans] = trancl_trans[Transfer.transferred]
lemmas ftrancl_empty [simp] = trancl_empty [Transfer.transferred]
lemmas ftranclE[cases set: ftrancl] = tranclE[Transfer.transferred]
lemmas converse_ftrancl_induct[consumes 1, case_names Base Step] = converse_trancl_induct[Transfer.transferred]
lemmas converse_ftranclE = converse_tranclE[Transfer.transferred]
lemma in_ftrancl_UnI:
"x |∈| R|⇧+| ∨ x |∈| S|⇧+| ⟹ x |∈| (R |∪| S)|⇧+|"
by transfer (auto simp add: trancl_mono)
lemma ftranclD:
"(x, y) |∈| R|⇧+| ⟹ ∃z. (x, z) |∈| R ∧ (z = y ∨ (z, y) |∈| R|⇧+|)"
by (induct rule: ftrancl_induct) (auto, meson ftrancl_into_trancl)
lemma ftranclD2:
"(x, y) |∈| R|⇧+| ⟹ ∃z. (x = z ∨ (x, z) |∈| R|⇧+|) ∧ (z, y) |∈| R"
by (induct rule: ftrancl_induct) auto
lemma not_ftrancl_into:
"(x, z) |∉| r|⇧+| ⟹ (y, z) |∈| r ⟹ (x, y) |∉| r|⇧+|"
by transfer (auto simp add: trancl.trancl_into_trancl)
lemmas ftrancl_map_both_fRestr = trancl_map_both_Restr[Transfer.transferred]
lemma ftrancl_map_both_fsubset:
"finj_on f X ⟹ R |⊆| X |×| X ⟹ (map_both f |`| R)|⇧+| = map_both f |`| R|⇧+|"
using ftrancl_map_both_fRestr[of f X R]
by (simp add: inf_absorb1)
lemmas ftrancl_map_prod_mono = trancl_map_prod_mono[Transfer.transferred]
lemmas ftrancl_map = trancl_map[Transfer.transferred]
lemmas ffUnion_iff [simp] = Union_iff[Transfer.transferred]
lemmas ffUnionI [intro] = UnionI[Transfer.transferred]
lemmas fUn_simps [simp] = UN_simps[Transfer.transferred]
lemmas fINT_simps [simp] = INT_simps[Transfer.transferred]
lemmas fUN_ball_bex_simps [simp] = UN_ball_bex_simps[Transfer.transferred]
lemmas in_fset_conv_nth = in_set_conv_nth[Transfer.transferred]
lemmas fnth_mem [simp] = nth_mem[Transfer.transferred]
lemmas distinct_sorted_list_of_fset = distinct_sorted_list_of_set [Transfer.transferred]
lemmas fcard_fset = card_set[Transfer.transferred]
lemma upt_fset:
"fset_of_list [i..<j] = fCollect (λ n. i ≤ n ∧ n < j)"
by (induct j arbitrary: i) auto
abbreviation fRestr :: "('a × 'a) fset ⇒ 'a fset ⇒ ('a × 'a) fset" where
"fRestr r A ≡ r |∩| (A |×| A)"
lift_definition fId_on :: "'a fset ⇒ ('a × 'a) fset" is Id_on
using Id_on_subset_Times finite_subset by fastforce
lemmas fId_on_empty [simp] = Id_on_empty [Transfer.transferred]
lemmas fId_on_eqI = Id_on_eqI [Transfer.transferred]
lemmas fId_onI [intro!] = Id_onI [Transfer.transferred]
lemmas fId_onE [elim!] = Id_onE [Transfer.transferred]
lemmas fId_on_iff = Id_on_iff [Transfer.transferred]
lemmas fId_on_fsubset_fTimes = Id_on_subset_Times [Transfer.transferred]
lift_definition fconverse :: "('a × 'b) fset ⇒ ('b × 'a) fset" (‹(_|¯|)› [1000] 999) is converse by auto
lemmas fconverseI [sym] = converseI [Transfer.transferred]
lemmas fconverseD [sym] = converseD [Transfer.transferred]
lemmas fconverseE [elim!] = converseE [Transfer.transferred]
lemmas fconverse_iff [iff] = converse_iff[Transfer.transferred]
lemmas fconverse_fconverse [simp] = converse_converse[Transfer.transferred]
lemmas fconverse_empty[simp] = converse_empty[Transfer.transferred]
lemmas finj_on_def' = inj_on_def[Transfer.transferred]
lemmas fsubset_finj_on = subset_inj_on[Transfer.transferred]
lemmas the_finv_into_f_f = the_inv_into_f_f[Transfer.transferred]
lemmas f_the_finv_into_f = f_the_inv_into_f[Transfer.transferred]
lemmas the_finv_into_into = the_inv_into_into[Transfer.transferred]
lemmas the_finv_into_onto [simp] = the_inv_into_onto[Transfer.transferred]
lemmas the_finv_into_f_eq = the_inv_into_f_eq[Transfer.transferred]
lemmas the_finv_into_comp = the_inv_into_comp[Transfer.transferred]
lemmas finj_on_the_finv_into = inj_on_the_inv_into [Transfer.transferred]
lemmas finj_on_fUn = inj_on_Un[Transfer.transferred]
lemma finj_Inl_Inr:
"finj_on Inl A" "finj_on Inr A"
by (transfer, auto)+
lemma finj_CInl_CInr:
"finj_on CInl A" "finj_on CInr A"
using finj_Inl_Inr by force+
lemma finj_Some:
"finj_on Some A"
by (transfer, auto)
lift_definition fImage :: "('a × 'b) fset ⇒ 'a fset ⇒ 'b fset" (infixr ‹|``|› 90) is Image
using finite_Image by force
lemmas fImage_iff = Image_iff[Transfer.transferred]
lemmas fImage_singleton_iff [iff] = Image_singleton_iff[Transfer.transferred]
lemmas fImageI [intro] = ImageI[Transfer.transferred]
lemmas ImageE [elim!] = ImageE[Transfer.transferred]
lemmas frev_ImageI = rev_ImageI[Transfer.transferred]
lemmas fImage_empty1 [simp] = Image_empty1[Transfer.transferred]
lemmas fImage_empty2 [simp] = Image_empty2[Transfer.transferred]
lemmas fImage_fInt_fsubset = Image_Int_subset[Transfer.transferred]
lemmas fImage_fUn = Image_Un[Transfer.transferred]
lemmas fUn_fImage = Un_Image[Transfer.transferred]
lemmas fImage_fsubset = Image_subset[Transfer.transferred]
lemmas fImage_eq_fUN = Image_eq_UN[Transfer.transferred]
lemmas fImage_mono = Image_mono[Transfer.transferred]
lemmas fImage_fUN = Image_UN[Transfer.transferred]
lemmas fUN_fImage = UN_Image[Transfer.transferred]
lemmas fSigma_fImage = Sigma_Image[Transfer.transferred]
lemmas fImage_singleton = Image_singleton[Transfer.transferred]
lemmas fImage_Id_on [simp] = Image_Id_on[Transfer.transferred]
lemmas fImage_Id [simp] = Image_Id[Transfer.transferred]
lemmas fImage_fInt_eq = Image_Int_eq[Transfer.transferred]
lemmas fImage_fsubset_eq = Image_subset_eq[Transfer.transferred]
lemmas fImage_fCollect_case_prod [simp] = Image_Collect_case_prod[Transfer.transferred]
lemmas fImage_fINT_fsubset = Image_INT_subset[Transfer.transferred]
lemmas term_fset_induct = term.induct[Transfer.transferred]
lemmas fmap_prod_fimageI = map_prod_imageI[Transfer.transferred]
lemmas finj_on_eq_iff = inj_on_eq_iff[Transfer.transferred]
lemmas prod_fun_fimageE = prod_fun_imageE[Transfer.transferred]
lemma rel_set_cr_fset:
"rel_set cr_fset = (λ A B. A = fset ` B)"
proof -
have "rel_set cr_fset A B ⟷ A = fset ` B" for A B
by (auto simp: image_def rel_set_def cr_fset_def )
then show ?thesis by blast
qed
lemma pcr_fset_cr_fset:
"pcr_fset cr_fset = (λ x y. x = fset (fset |`| y))"
unfolding pcr_fset_def rel_set_cr_fset
unfolding cr_fset_def
by (auto simp: image_def relcompp_apply)
lemma sorted_list_of_fset_id:
"sorted_list_of_fset x = sorted_list_of_fset y ⟹ x = y"
by (metis sorted_list_of_fset_simps(2))
lemmas fBall_def = Ball_def[Transfer.transferred]
lemmas fBex_def = Bex_def[Transfer.transferred]
lemmas fCollectE = fCollectD [elim_format]
lemma fCollect_conj_eq:
"finite (Collect P) ⟹ finite (Collect Q) ⟹ {|x. P x ∧ Q x|} = fCollect P |∩| fCollect Q"
by auto
lemma finite_ntrancl:
"finite R ⟹ finite (ntrancl n R)"
by (induct n) auto
lift_definition nftrancl :: "nat ⇒ ('a × 'a) fset ⇒ ('a × 'a) fset" is ntrancl
by (intro finite_ntrancl) simp
lift_definition frelcomp :: "('a × 'b) fset ⇒ ('b × 'c) fset ⇒ ('a × 'c) fset" (infixr ‹|O|› 75) is relcomp
by (intro finite_relcomp) simp
lemmas frelcompE[elim!] = relcompE[Transfer.transferred]
lemmas frelcompI[intro] = relcompI[Transfer.transferred]
lemma fId_on_frelcomp_id:
"fst |`| R |⊆| S ⟹ fId_on S |O| R = R"
by (auto intro!: frelcompI)
lemma fId_on_frelcomp_id2:
"snd |`| R |⊆| S ⟹ R |O| fId_on S = R"
by (auto intro!: frelcompI)
lemmas fimage_fset = image_set[Transfer.transferred]
lemmas ftrancl_Un2_separatorE = trancl_Un2_separatorE[Transfer.transferred]
lemma finite_funs_term: "finite (funs_term t)" by (induct t) auto
lemma finite_funas_term: "finite (funas_term t)" by (induct t) auto
lemma finite_vars_ctxt: "finite (vars_ctxt C)" by (induct C) auto
lift_definition ffuns_term :: "('f, 'v) term ⇒ 'f fset" is funs_term using finite_funs_term
by blast
lift_definition fvars_term :: "('f, 'v) term ⇒ 'v fset" is vars_term by simp
lift_definition fvars_ctxt :: "('f, 'v) ctxt ⇒ 'v fset" is vars_ctxt by (simp add: finite_vars_ctxt)
lemmas fvars_term_ctxt_apply [simp] = vars_term_ctxt_apply[Transfer.transferred]
lemmas fvars_term_of_gterm [simp] = vars_term_of_gterm[Transfer.transferred]
lemmas ground_fvars_term_empty [simp] = ground_vars_term_empty[Transfer.transferred]
lemma ffuns_term_Var [simp]: "ffuns_term (Var x) = {||}"
by transfer auto
lemma fffuns_term_Fun [simp]: "ffuns_term (Fun f ts) = |⋃| (ffuns_term |`| fset_of_list ts) |∪| {|f|}"
by transfer auto
lemma fvars_term_Var [simp]: "fvars_term (Var x) = {|x|}"
by transfer auto
lemma fvars_term_Fun [simp]: "fvars_term (Fun f ts) = |⋃| (fvars_term |`| fset_of_list ts)"
by transfer auto
lift_definition ffunas_term :: "('f, 'v) term ⇒ ('f × nat) fset" is funas_term
by (simp add: finite_funas_term)
lift_definition ffunas_gterm :: "'f gterm ⇒ ('f × nat) fset" is funas_gterm
by (simp add: finite_funas_gterm)
lemmas ffunas_term_simps [simp] = funas_term.simps[Transfer.transferred]
lemmas ffunas_gterm_simps [simp] = funas_gterm.simps[Transfer.transferred]
lemmas ffunas_term_of_gterm_conv = funas_term_of_gterm_conv[Transfer.transferred]
lemmas ffunas_gterm_gterm_of_term = funas_gterm_gterm_of_term[Transfer.transferred]
lemma sorted_list_of_fset_fimage_dist:
"sorted_list_of_fset (f |`| A) = sort (remdups (map f (sorted_list_of_fset A)))"
by (auto simp: sorted_list_of_fset.rep_eq simp flip: sorted_list_of_set_sort_remdups)
end
lemma finite_snd [intro]:
"finite S ⟹ finite {x. (y, x) ∈ S}"
by (induct S rule: finite.induct) auto
lemma finite_Collect_less_eq:
"Q ≤ P ⟹ finite (Collect P) ⟹ finite (Collect Q)"
by (metis (full_types) Ball_Collect infinite_iff_countable_subset rev_predicate1D)