# HG changeset patch # User blanchet # Date 1348101769 -7200 # Node ID de07eecb26649196ae838afc04d8828cc4d73406 # Parent 4dd451a075ce41aca0d8af4b429952f7478f39f3 adapting "More_BNFs" to new relators/predicators diff -r 4dd451a075ce -r de07eecb2664 src/HOL/Codatatype/Examples/Misc_Data.thy --- a/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:49 2012 +0200 @@ -12,27 +12,12 @@ imports (* "../Codatatype" *) "../BNF_LFP" begin -declare [[bnf_note_all = false]] - -local_setup {* fn lthy => -snd (snd (BNF_Comp.bnf_of_typ BNF_Def.Dont_Inline (Binding.qualify true "xxx") - BNF_Comp.default_comp_sort - @{typ "('a \ 'a) + ('a + 'b) + 'c"} (BNF_Comp.empty_unfold, lthy))) -*} - -print_theorems - -data 'a lst = Nl | Cns 'a "'a lst" - -thm pre_lst.rel_unfold - pre_lst.pred_unfold - lst.rel_unfold - lst.pred_unfold +bnf_def ID2: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" ["id :: 'a \ 'a"] + "id :: ('a \ 'b) set \ ('a \ 'b) set" +sorry data simple = X1 | X2 | X3 | X4 -thm simple.rel_unfold - data simple' = X1' unit | X2' unit | X3' unit | X4' unit data 'a mylist = MyNil | MyCons 'a "'a mylist" diff -r 4dd451a075ce -r de07eecb2664 src/HOL/Codatatype/More_BNFs.thy --- a/src/HOL/Codatatype/More_BNFs.thy Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/More_BNFs.thy Thu Sep 20 02:42:49 2012 +0200 @@ -22,7 +22,10 @@ lemma option_rec_conv_option_case: "option_rec = option_case" by (simp add: fun_eq_iff split: option.split) -bnf_def Option.map [Option.set] "\_::'a option. natLeq" ["None"] +definition option_rel :: "('a \ 'b) set \ ('a option \ 'b option) set" where +"option_rel R = {x. case x of (None, None) \ True | (Some a, Some b) \ (a, b) \ R | _ \ False}" + +bnf_def Option.map [Option.set] "\_::'a option. natLeq" ["None"] option_rel proof - show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split) next @@ -81,17 +84,15 @@ fix z assume "z \ Option.set None" thus False by simp +next + fix R + show "option_rel R = + (Gr {x. Option.set x \ R} (Option.map fst))\ O Gr {x. Option.set x \ R} (Option.map snd)" + unfolding option_rel_def Gr_def relcomp_unfold converse_unfold + by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some] + split: option.splits) blast qed -lemma option_pred[simp]: "option_pred R x_opt y_opt = - (case (x_opt, y_opt) of - (None, None) \ True - | (Some x, Some y) \ R x y - | _ \ False)" -unfolding option_pred_def option_rel_def Gr_def relcomp_unfold converse_unfold -by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some] - split: option.splits) - lemma card_of_list_in: "|{xs. set xs \ A}| \o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \o |?RHS|") proof - @@ -240,7 +241,7 @@ thus "\as bs. as \ ?B1 \ bs \ ?B2 \ map f1 as = map f2 bs \ (\zs \ ?A. map p1 zs = as \ map p2 zs = bs)" by blast qed -qed auto +qed simp+ (* Finite sets *) abbreviation afset where "afset \ abs_fset" @@ -355,7 +356,35 @@ lemma fset_to_fset: "finite A \ fset (the_inv fset A) = A" by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset) -bnf_def map_fset [fset] "\_::'a fset. natLeq" ["{||}"] +lemma fset_pred: +"(a, b) \ (Gr {a. fset a \ {(a, b). R a b}} (map_fset fst))\ O + Gr {a. fset a \ {(a, b). R a b}} (map_fset snd) \ + ((\t \ fset a. \u \ fset b. R t u) \ (\u \ fset b. \t \ fset a. R t u))" (is "?L = ?R") +proof + assume ?L thus ?R unfolding Gr_def relcomp_unfold converse_unfold + apply (simp add: subset_eq Ball_def) + apply (rule conjI) + apply (clarsimp, metis snd_conv) + by (clarsimp, metis fst_conv) +next + assume ?R + def R' \ "the_inv fset (Collect (split R) \ (fset a \ fset b))" (is "the_inv fset ?R'") + have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto + hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset) + show ?L unfolding Gr_def relcomp_unfold converse_unfold + proof (intro CollectI prod_caseI exI conjI) + from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`] + by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) + from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`] + by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) + qed (auto simp add: *) +qed + +definition fset_rel :: "('a \ 'b) set \ ('a fset \ 'b fset) set" where +"fset_rel R = {(a, b) | a b. (\t \ fset a. \u \ fset b. (t, u) \ R) \ + (\u \ fset b. \t \ fset a. (t, u) \ R)}" + +bnf_def map_fset [fset] "\_::'a fset. natLeq" ["{||}"] fset_rel proof - show "map_fset id = id" unfolding map_fset_def2 map_id o_id afset_rfset_id .. @@ -429,32 +458,15 @@ unfolding X'eq map_fset_def2_raw fset_def2_raw set_map[symmetric] afset_set[symmetric] afset_rfset by simp qed +next + fix R + let ?pred = "\Q x y. (x, y) \ (Gr {x. fset x \ {(x, y). Q x y}} (map_fset fst))\ O Gr {x. fset x \ {(x, y). Q x y}} (map_fset snd)" + have rel_as_pred: "fset_rel R = {(a, b) | a b. ?pred (\t u. (t, u) \ R) a b}" + unfolding fset_rel_def fset_pred by (rule refl) + show "fset_rel R = (Gr {x. fset x \ R} (map_fset fst))\ O Gr {x. fset x \ R} (map_fset snd)" + unfolding rel_as_pred by simp qed auto -lemma fset_pred[simp]: "fset_pred R a b \ - ((\t \ fset a. \u \ fset b. R t u) \ - (\t \ fset b. \u \ fset a. R u t))" (is "?L = ?R") -proof - assume ?L thus ?R unfolding fset_rel_def fset_pred_def - Gr_def relcomp_unfold converse_unfold - apply (simp add: subset_eq Ball_def) - apply (rule conjI) - apply (clarsimp, metis snd_conv) - by (clarsimp, metis fst_conv) -next - assume ?R - def R' \ "the_inv fset (Collect (split R) \ (fset a \ fset b))" (is "the_inv fset ?R'") - have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto - hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset) - show ?L unfolding fset_rel_def fset_pred_def Gr_def relcomp_unfold converse_unfold - proof (intro CollectI prod_caseI exI conjI) - from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`] - by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) - from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`] - by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) - qed (auto simp add: *) -qed - (* Countable sets *) lemma card_of_countable_sets_range: @@ -511,7 +523,52 @@ finally show ?thesis . qed -bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] +lemma rcset_to_rcset: "countable A \ rcset (the_inv rcset A) = A" +apply (rule f_the_inv_into_f) +unfolding inj_on_def rcset_inj using rcset_surj by auto + +lemma Collect_Int_Times: +"{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" +by auto + +lemma rcset_natural': "rcset (cIm f x) = f ` rcset x" +unfolding cIm_def[abs_def] by simp + +lemma cset_pred: +"(a, b) \ (Gr {x. rcset x \ {(a, b). R a b}} (cIm fst))\ O + Gr {x. rcset x \ {(a, b). R a b}} (cIm snd) \ + ((\t \ rcset a. \u \ rcset b. R t u) \ (\t \ rcset b. \u \ rcset a. R u t))" (is "?L = ?R") +proof + assume ?L thus ?R unfolding Gr_def relcomp_unfold converse_unfold + apply (simp add: subset_eq Ball_def) + apply (rule conjI) + apply (clarsimp, metis (lifting, no_types) rcset_natural' image_iff surjective_pairing) + apply (clarsimp) + by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range) +next + assume ?R + def R' \ "the_inv rcset (Collect (split R) \ (rcset a \ rcset b))" + (is "the_inv rcset ?R'") + have "countable ?R'" by auto + hence *: "rcset R' = ?R'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset) + show ?L unfolding Gr_def relcomp_unfold converse_unfold + proof (intro CollectI prod_caseI exI conjI) + have "rcset a = fst ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?A") + using conjunct1[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times) + hence "a = acset ?A" by (metis acset_rcset) + thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto + have "rcset b = snd ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?B") + using conjunct2[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times) + hence "b = acset ?B" by (metis acset_rcset) + thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto + qed (auto simp add: *) +qed + +definition cset_rel :: "('a \ 'b) set \ ('a cset \ 'b cset) set" where +"cset_rel R = {(a, b) | a b. (\t \ rcset a. \u \ rcset b. (t, u) \ R) \ + (\u \ rcset b. \t \ rcset a. (t, u) \ R)}" + +bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] cset_rel proof - show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto next @@ -573,52 +630,21 @@ show "\x\{x. rcset x \ A}. cIm p1 x = y1 \ cIm p2 x = y2" apply(intro bexI[of _ "x"]) using X' Y1 Y2 unfolding X'eq cIm_def by auto qed +next + fix R + let ?pred = "\Q x y. (x, y) \ (Gr {x. rcset x \ {(x, y). Q x y}} (cIm fst))\ O Gr {x. rcset x \ {(x, y). Q x y}} (cIm snd)" + have rel_as_pred: "cset_rel R = {(a, b) | a b. ?pred (\t u. (t, u) \ R) a b}" + unfolding cset_rel_def cset_pred by (rule refl) + show "cset_rel R = (Gr {x. rcset x \ R} (cIm fst))\ O Gr {x. rcset x \ R} (cIm snd)" + unfolding rel_as_pred by simp qed (unfold cEmp_def, auto) -lemma rcset_to_rcset: "countable A \ rcset (the_inv rcset A) = A" -apply (rule f_the_inv_into_f) -unfolding inj_on_def rcset_inj using rcset_surj by auto - -lemma Collect_Int_Times: -"{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" -by auto - -lemma cset_pred[simp]: "cset_pred R a b \ - ((\t \ rcset a. \u \ rcset b. R t u) \ - (\t \ rcset b. \u \ rcset a. R u t))" (is "?L = ?R") -proof - assume ?L thus ?R unfolding cset_rel_def cset_pred_def - Gr_def relcomp_unfold converse_unfold - apply (simp add: subset_eq Ball_def) - apply (rule conjI) - apply (clarsimp, metis (lifting, no_types) cset.set_natural' image_iff surjective_pairing) - apply (clarsimp) - by (metis Domain.intros Range.simps cset.set_natural' fst_eq_Domain snd_eq_Range) -next - assume ?R - def R' \ "the_inv rcset (Collect (split R) \ (rcset a \ rcset b))" - (is "the_inv rcset ?R'") - have "countable ?R'" by auto - hence *: "rcset R' = ?R'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset) - show ?L unfolding cset_rel_def cset_pred_def Gr_def relcomp_unfold converse_unfold - proof (intro CollectI prod_caseI exI conjI) - have "rcset a = fst ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?A") - using conjunct1[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times) - hence "a = acset ?A" by (metis acset_rcset) - thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto - have "rcset b = snd ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?B") - using conjunct2[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times) - hence "b = acset ?B" by (metis acset_rcset) - thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto - qed (auto simp add: *) -qed - (* Multisets *) -(* The cardinal of a mutiset: this, and the following basic lemmas about it, +(* The cardinal of a mutiset: this, and the following basic lemmas about it, should eventually go into Multiset.thy *) -definition "mcard M \ setsum (count M) {a. count M a > 0}" +definition "mcard M \ setsum (count M) {a. count M a > 0}" lemma mcard_emp[simp]: "mcard {#} = 0" unfolding mcard_def by auto @@ -636,7 +662,7 @@ have "setsum (count M) {a. 0 < count M a + count N a} = setsum (count M) {a. a \# M}" apply(rule setsum_mono_zero_cong_right) by auto - moreover + moreover have "setsum (count N) {a. 0 < count M a + count N a} = setsum (count N) {a. a \# N}" apply(rule setsum_mono_zero_cong_right) by auto @@ -1268,7 +1294,7 @@ lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp lemma multiset_pred_Zero: "multiset_pred R {#} {#}" -unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto +unfolding multiset_pred_def Gr_def relcomp_unfold by auto declare multiset.count[simp] declare mmap[simp] @@ -1321,7 +1347,7 @@ } thus ?thesis using assms - unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by force + unfolding multiset_pred_def Gr_def relcomp_unfold by force qed lemma multiset_pred'_imp_multiset_pred: @@ -1363,7 +1389,7 @@ lemma multiset_pred_mcard: assumes "multiset_pred R M N" shows "mcard M = mcard N" -using assms unfolding multiset_pred_def multiset_rel_def relcomp_unfold Gr_def by auto +using assms unfolding multiset_pred_def relcomp_unfold Gr_def by auto lemma multiset_induct2[case_names empty addL addR]: assumes empty: "P {#} {#}" @@ -1424,14 +1450,14 @@ obtain K where KM: "multiset_map fst K = M + {#a#}" and KN: "multiset_map snd K = N" and sK: "set_of K \ {(a, b). R a b}" using assms - unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto + unfolding multiset_pred_def Gr_def relcomp_unfold by auto obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a" and K1M: "multiset_map fst K1 = M" using msed_map_invR[OF KM] by auto obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "multiset_map snd K1 = N1" using msed_map_invL[OF KN[unfolded K]] by auto have Rab: "R a (snd ab)" using sK a unfolding K by auto have "multiset_pred R M N1" using sK K1M K1N1 - unfolding K multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto + unfolding K multiset_pred_def Gr_def relcomp_unfold by auto thus ?thesis using N Rab by auto qed @@ -1442,14 +1468,14 @@ obtain K where KN: "multiset_map snd K = N + {#b#}" and KM: "multiset_map fst K = M" and sK: "set_of K \ {(a, b). R a b}" using assms - unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto + unfolding multiset_pred_def Gr_def relcomp_unfold by auto obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b" and K1N: "multiset_map snd K1 = N" using msed_map_invR[OF KN] by auto obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "multiset_map fst K1 = M1" using msed_map_invL[OF KM[unfolded K]] by auto have Rab: "R (fst ab) b" using sK b unfolding K by auto have "multiset_pred R M1 N" using sK K1N K1M1 - unfolding K multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto + unfolding K multiset_pred_def Gr_def relcomp_unfold by auto thus ?thesis using M Rab by auto qed diff -r 4dd451a075ce -r de07eecb2664 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:49 2012 +0200 @@ -263,7 +263,7 @@ (maps wit_thms_of_bnf inners); val (bnf', lthy') = - bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) + bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) (((((b, mapx), sets), bd), wits), SOME rel) lthy; val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') @@ -361,7 +361,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) + bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') @@ -449,7 +449,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') @@ -527,7 +527,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf') diff -r 4dd451a075ce -r de07eecb2664 src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:49 2012 +0200 @@ -82,7 +82,7 @@ datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline datatype fact_policy = - Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms + Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms val bnf_note_all: bool Config.T val user_policy: fact_policy -> Proof.context -> fact_policy @@ -507,7 +507,7 @@ datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline; datatype fact_policy = - Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms; + Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms; val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false); @@ -553,9 +553,10 @@ | T => err T) else (b, Local_Theory.full_name no_defs_lthy b); - fun maybe_define (b, rhs) lthy = + fun maybe_define needed_for_extra_facts (b, rhs) lthy = let val inline = + (not needed_for_extra_facts orelse fact_policy = Derive_Few_Facts) andalso (case const_policy of Dont_Inline => false | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs @@ -592,10 +593,10 @@ (bnf_bd_term, raw_bd_def)), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = no_defs_lthy - |> maybe_define map_bind_def - ||>> apfst split_list o fold_map maybe_define set_binds_defs - ||>> maybe_define bd_bind_def - ||>> apfst split_list o fold_map maybe_define wit_binds_defs + |> maybe_define false map_bind_def + ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs + ||>> maybe_define false bd_bind_def + ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs ||> `(maybe_restore no_defs_lthy); val phi = Proof_Context.export_morphism lthy_old lthy; @@ -723,7 +724,7 @@ val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) = lthy - |> maybe_define rel_bind_def + |> maybe_define false rel_bind_def ||> `(maybe_restore lthy); val phi = Proof_Context.export_morphism lthy_old lthy; @@ -742,7 +743,7 @@ val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) = lthy - |> maybe_define pred_bind_def + |> maybe_define true pred_bind_def ||> `(maybe_restore lthy); val phi = Proof_Context.export_morphism lthy_old lthy; @@ -885,7 +886,7 @@ val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order]; val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero}; - fun mk_lazy f = if fact_policy <> Derive_Some_Facts then Lazy.value (f ()) else Lazy.lazy f; + fun mk_lazy f = if fact_policy <> Derive_Few_Facts then Lazy.value (f ()) else Lazy.lazy f; fun mk_collect_set_natural () = let