# HG changeset patch # User haftmann # Date 1748447362 -7200 # Node ID e9f3b94eb6a0cf49f2b86029e47c4d86d9c79bab # Parent bd951e02d6b9265aee619388f70cda7b1f73f2d3 more modern qualification of auxiliary operations diff -r bd951e02d6b9 -r e9f3b94eb6a0 NEWS --- a/NEWS Sat May 24 09:06:26 2025 +0200 +++ b/NEWS Wed May 28 17:49:22 2025 +0200 @@ -78,6 +78,25 @@ *** HOL *** +* Consolidated auxiliary operations intended for code generation: + + const Set.is_empty + thm is_empty_def ~> Set.is_empty_iff [simp] + + const Set.remove + thm remove_def ~> Set.remove_eq [simp] + + const Set.filter + thm filter_def → Set.filter_eq [simp] + +The _def suffix for characteristic theorems is avoided to emphasize that these +auxiliary operations are candidates for unfolding since they are variants +of existing logical concepts. The [simp] declarations try to move the attention +of the casual user ways from these auxiliary operations; if they pose problems +in existing applications, the can be removed using [simp del] – the regular +theory merge will make sure that this deviant setup will not persist in bigger +developments. INCOMPATIBILITY. + * ML bindings for theorems Ball_def, Bex_def, CollectD, CollectE, CollectI, Collect_conj_eq, Collect_mem_eq, IntD1, IntD2, IntE, IntI, Int_Collect, UNIV_I, UNIV_witness, UnE, UnI1, UnI2, ballE, ballI, bexCI, bexE, bexI, bex_triv, bspec, diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Analysis/Urysohn.thy --- a/src/HOL/Analysis/Urysohn.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Analysis/Urysohn.thy Wed May 28 17:49:22 2025 +0200 @@ -5516,9 +5516,8 @@ moreover have "\\ = topspace X" using ABC UU \_def by auto moreover have "pairwise (separatedin X) \" - using pwU sep ABC unfolding \_def - apply (simp add: separatedin_sym pairwise_def) - by (metis member_remove remove_def separatedin_Un(1)) + using pwU sep ABC separatedin_Un(1) [of X _ A B] + by (simp add: separatedin_sym pairwise_def \_def) (metis DiffD1 DiffD2 singleton_iff) ultimately show ?thesis by blast qed diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Complex_Analysis/Conformal_Mappings.thy --- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Wed May 28 17:49:22 2025 +0200 @@ -723,7 +723,7 @@ then have "(\z. if z = \ then deriv g \ else (g z - g \) / (z - \)) holomorphic_on S" using \ pole_lemma by blast then show ?thesis - using "\
" remove_def by fastforce + using "\
" by (smt (verit, best) DiffD2 singletonI) qed ultimately show "?P = ?Q" and "?P = ?R" by meson+ diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Computational_Algebra/Nth_Powers.thy --- a/src/HOL/Computational_Algebra/Nth_Powers.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Wed May 28 17:49:22 2025 +0200 @@ -70,7 +70,7 @@ have "multiplicity p x = 0" if "p \ prime_factors x" using that and \prime p\ by (simp add: prime_factors_multiplicity) with that and * and assms show ?thesis unfolding prod_power_distrib power_mult [symmetric] - by (subst multiplicity_prod_prime_powers) (auto simp: in_prime_factors_imp_prime elim: dvdE) + by (subst multiplicity_prod_prime_powers) (auto simp: in_prime_factors_imp_prime) qed with assms False have "normalize x = normalize ((\p\prime_factors x. p ^ (multiplicity p x div n)) ^ n)" @@ -253,15 +253,15 @@ lemma first_root_nat' [simp]: "nth_root_nat (Suc 0) n = n" by (intro nth_root_nat_unique) auto - lemma nth_root_nat_code_naive': "nth_root_nat k n = (if k = 0 then 0 else Max (Set.filter (\m. m ^ k \ n) {..n}))" proof (cases "k > 0") case True - hence "{m. m ^ k \ n} \ {..n}" by (rule nth_root_nat_aux1) - hence "Set.filter (\m. m ^ k \ n) {..n} = {m. m ^ k \ n}" - by (auto simp: Set.filter_def) - with True show ?thesis by (simp add: nth_root_nat_def Set.filter_def) + then have "{m. m ^ k \ n} \ {..n}" by (rule nth_root_nat_aux1) + then have "Set.filter (\m. m ^ k \ n) {..n} = {m. m ^ k \ n}" + by (auto simp:) + with True show ?thesis + by (simp add: nth_root_nat_def) qed simp function nth_root_nat_aux :: "nat \ nat \ nat \ nat \ nat" where diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Finite_Set.thy Wed May 28 17:49:22 2025 +0200 @@ -556,7 +556,7 @@ using assms by (simp add: bind_UNION) lemma finite_filter [simp]: "finite S \ finite (Set.filter P S)" -unfolding Set.filter_def by simp + by (simp add:) lemma finite_set_of_finite_funs: assumes "finite A" "finite B" @@ -1341,14 +1341,13 @@ interpret commute_insert: comp_fun_commute "(\x A'. if P x then Set.insert x A' else A')" by (fact comp_fun_commute_filter_fold) from \finite A\ show ?thesis - by induct (auto simp add: Set.filter_def) + by induct (auto simp add: set_eq_iff) qed lemma inter_Set_filter: assumes "finite B" shows "A \ B = Set.filter (\x. x \ A) B" - using assms - by induct (auto simp: Set.filter_def) + using assms by (simp add: set_eq_iff ac_simps) lemma image_fold_insert: assumes "finite A" diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Homology/Invariance_of_Domain.thy --- a/src/HOL/Homology/Invariance_of_Domain.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Homology/Invariance_of_Domain.thy Wed May 28 17:49:22 2025 +0200 @@ -2913,8 +2913,8 @@ using homeomorphism_apply1 [OF gh] SU by (fastforce simp add: image_iff image_subset_iff) show "S - {b} \ h ` g ` (S - {b})" - apply clarify - by (metis SU subsetD homeomorphism_apply1 [OF gh] image_iff member_remove remove_def) + using SU gh homeomorphism_apply1 [of \(rel_frontier U - {b})\ V g h] + by (auto simp add: image_iff) (metis DiffI singletonD subsetD) qed then show ?thesis by (metis image_comp) @@ -2927,8 +2927,8 @@ using homeomorphism_apply1 [OF jk] SU by (fastforce simp add: image_iff image_subset_iff) show "S - {c} \ k ` j ` (S - {c})" - apply clarify - by (metis SU subsetD homeomorphism_apply1 [OF jk] image_iff member_remove remove_def) + using SU jk homeomorphism_apply1 [of \(rel_frontier U - {c})\ V j k] + by (auto simp add: image_iff) (metis DiffI singletonD subsetD) qed then show ?thesis by (metis image_comp) diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Lattices_Big.thy Wed May 28 17:49:22 2025 +0200 @@ -783,7 +783,7 @@ then obtain a where "f a = Max (f ` A)" and "a \ A" by (metis Max_in[of "f ` A"] imageE) then have "P (A - {a})" - using psubset member_remove by blast + using psubset(2) [of \A - {a}\] by auto moreover have "\y. y \ A \ f y \ f a" using \f a = Max (f ` A)\ \finite (f ` A)\ by simp diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Library/Discrete_Functions.thy --- a/src/HOL/Library/Discrete_Functions.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Library/Discrete_Functions.thy Wed May 28 17:49:22 2025 +0200 @@ -200,8 +200,10 @@ lemma floor_sqrt_code[code]: "floor_sqrt n = Max (Set.filter (\m. m\<^sup>2 \ n) {0..n})" proof - - from power2_nat_le_imp_le [of _ n] have "{m. m \ n \ m\<^sup>2 \ n} = {m. m\<^sup>2 \ n}" by auto - then show ?thesis by (simp add: floor_sqrt_def Set.filter_def) + from power2_nat_le_imp_le [of _ n] + have "{m. m \ n \ m\<^sup>2 \ n} = {m. m\<^sup>2 \ n}" by auto + then show ?thesis + by (simp add: floor_sqrt_def) qed lemma floor_sqrt_inverse_power2 [simp]: "floor_sqrt (n\<^sup>2) = n" diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Library/FSet.thy Wed May 28 17:49:22 2025 +0200 @@ -256,7 +256,7 @@ by transfer_prover lift_definition ffilter :: "('a \ bool) \ 'a fset \ 'a fset" is Set.filter - parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp + parametric Lifting_Set.filter_transfer by simp lift_definition fPow :: "'a fset \ 'a fset fset" is Pow parametric Pow_transfer by (simp add: finite_subset) @@ -1015,7 +1015,7 @@ by (rule bind_const[Transfer.transferred]) lemma ffmember_filter[simp]: "(x |\| ffilter P A) = (x |\| A \ P x)" - by (rule member_filter[Transfer.transferred]) + by transfer simp lemma fequalityI: "A |\| B \ B |\| A \ A = B" by (rule equalityI[Transfer.transferred]) @@ -1112,7 +1112,7 @@ lemma fset_of_list_filter[simp]: "fset_of_list (filter P xs) = ffilter P (fset_of_list xs)" - by transfer (auto simp: Set.filter_def) + by transfer auto lemma fset_of_list_subset[intro]: "set xs \ set ys \ fset_of_list xs |\| fset_of_list ys" diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Library/Finite_Map.thy Wed May 28 17:49:22 2025 +0200 @@ -81,12 +81,10 @@ assumes "finite (dom m)" shows "finite (dom (map_filter P m))" proof - - have "dom (map_filter P m) = Set.filter P (dom m)" - unfolding map_filter_def Set.filter_def dom_def - by auto + from assms have \finite (dom (\x. if P x then m x else None))\ + by (rule rev_finite_subset) (auto split: if_splits) then show ?thesis - using assms - by (simp add: Set.filter_def) + by (simp add: map_filter_def) qed definition map_drop :: "'a \ ('a \ 'b) \ ('a \ 'b)" where @@ -269,10 +267,10 @@ by auto lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)" -by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) +by transfer' (auto simp: map_filter_def split: if_splits) lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)" -by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) +by transfer' (auto simp: map_filter_def split: if_splits) lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)" by transfer' (auto simp: map_filter_def) diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Library/RBT.thy Wed May 28 17:49:22 2025 +0200 @@ -169,6 +169,10 @@ "lookup t = Map.empty \ t = empty" by transfer (rule RBT_lookup_empty) +lemma keys_empty_eq [simp]: + \keys empty = []\ + by transfer simp + lemma sorted_keys [iff]: "sorted (keys t)" by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries) diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Library/RBT_Set.thy Wed May 28 17:49:22 2025 +0200 @@ -90,8 +90,8 @@ lemma Set_filter_rbt_filter: "Set.filter P (Set t) = rbt_filter P t" -by (simp add: fold_keys_def Set_filter_fold rbt_filter_def - finite_fold_fold_keys[OF comp_fun_commute_filter_fold]) + by (subst Set_filter_fold) + (simp_all add: fold_keys_def rbt_filter_def finite_fold_fold_keys [OF comp_fun_commute_filter_fold]) subsection \foldi and Ball\ @@ -449,7 +449,7 @@ lemma is_empty_Set [code]: "Set.is_empty (Set t) = RBT.is_empty t" - unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1]) + using non_empty_keys [of t] by (auto simp add: set_keys) lemma compl_code [code]: "- Set xs = Coset xs" @@ -482,7 +482,7 @@ lemma inter_Set [code]: "A \ Set t = rbt_filter (\k. k \ A) t" -by (simp add: inter_Set_filter Set_filter_rbt_filter) + by (auto simp flip: Set_filter_rbt_filter) lemma minus_Set [code]: "A - Set t = fold_keys Set.remove t A" @@ -517,8 +517,8 @@ by (simp add: inter_Set[simplified Int_commute]) lemma filter_Set [code]: - "Set.filter P (Set t) = (rbt_filter P t)" -by (auto simp add: Set_filter_rbt_filter) + "Set.filter P (Set t) = rbt_filter P t" + by (fact Set_filter_rbt_filter) lemma image_Set [code]: "image f (Set t) = fold_keys (\k A. Set.insert (f k) A) t {}" diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Lifting_Set.thy Wed May 28 17:49:22 2025 +0200 @@ -258,7 +258,7 @@ lemma filter_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique A" shows "((A ===> (=)) ===> rel_set A ===> rel_set A) Set.filter Set.filter" - unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast + by (simp add: rel_fun_def rel_set_def) blast lemma finite_transfer [transfer_rule]: "bi_unique A \ (rel_set A ===> (=)) finite finite" diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/List.thy --- a/src/HOL/List.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/List.thy Wed May 28 17:49:22 2025 +0200 @@ -8257,7 +8257,7 @@ lemma is_empty_set [code]: "Set.is_empty (set xs) \ List.null xs" - by (simp add: Set.is_empty_def null_def) + by (simp add: null_def) lemma empty_set [code]: "{} = set []" @@ -8288,7 +8288,7 @@ lemma remove_code [code]: "Set.remove x (set xs) = set (removeAll x xs)" "Set.remove x (List.coset xs) = List.coset (List.insert x xs)" - by (simp_all add: remove_def Compl_insert) + by (simp_all add: set_eq_iff ac_simps) lemma filter_set [code]: "Set.filter P (set xs) = set (filter P xs)" diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Wed May 28 17:49:22 2025 +0200 @@ -454,7 +454,7 @@ (\(ss, w). let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) (ss, w)" - unfolding iter_def Set.is_empty_def some_elem_def .. + by (simp add: iter_def some_elem_def) lemma JVM_sup_unfold [code]: "JVMType.sup S m n = lift2 (Opt.sup diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Nominal/Examples/W.thy --- a/src/HOL/Nominal/Examples/W.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Nominal/Examples/W.thy Wed May 28 17:49:22 2025 +0200 @@ -478,7 +478,8 @@ using freshs_mem [OF _ pi1'] subsetD [OF pi2] ftv_Ctxt fresh_def by fastforce have "\x y. \x \ set (ftv T\<^sub>1 - ftv \); y \ pi \ set (ftv T\<^sub>1 - ftv \)\ \ x \ close \ T\<^sub>1 \ y \ close \ T\<^sub>1" - by (metis DiffE filter_set fresh_def fresh_gen_set freshs_mem ftv_Ctxt ftv_ty gen_supp member_filter pi1') + using pi1' fresh_def fresh_gen_set freshs_mem ftv_Ctxt ftv_ty gen_supp + by (metis (lifting) DiffE mem_Collect_eq set_filter) then have close_fresh': "\(x, y)\set pi. x \ close \ T\<^sub>1 \ y \ close \ T\<^sub>1" using pi2 by auto note x diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Number_Theory/Number_Theory.thy --- a/src/HOL/Number_Theory/Number_Theory.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Number_Theory/Number_Theory.thy Wed May 28 17:49:22 2025 +0200 @@ -15,4 +15,3 @@ begin end - diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Number_Theory/Pocklington.thy --- a/src/HOL/Number_Theory/Pocklington.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Number_Theory/Pocklington.thy Wed May 28 17:49:22 2025 +0200 @@ -516,7 +516,8 @@ hence "Min A \ k" by (intro Min_le) (auto simp: \finite A\) moreover from * have "k \ Min A" unfolding k_def by (intro Least_le) (auto simp: A_def) - ultimately show ?thesis using True by (simp add: ord_def k_def A_def Set.filter_def) + ultimately show ?thesis using True + by (simp add: ord_def k_def A_def) qed auto theorem ord_modulus_mult_coprime: diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Number_Theory/Totient.thy --- a/src/HOL/Number_Theory/Totient.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Number_Theory/Totient.thy Wed May 28 17:49:22 2025 +0200 @@ -20,7 +20,7 @@ by (simp add: totatives_def) lemma totatives_code [code]: "totatives n = Set.filter (\k. coprime k n) {0<..n}" - by (simp add: totatives_def Set.filter_def) + by (simp add: totatives_def) lemma finite_totatives [simp]: "finite (totatives n)" by (simp add: totatives_def) diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/Set.thy --- a/src/HOL/Set.thy Sat May 24 09:06:26 2025 +0200 +++ b/src/HOL/Set.thy Wed May 28 17:49:22 2025 +0200 @@ -1876,33 +1876,32 @@ subsubsection \Operations for execution\ -definition is_empty :: "'a set \ bool" - where [code_abbrev]: "is_empty A \ A = {}" - -hide_const (open) is_empty - -definition remove :: "'a \ 'a set \ 'a set" - where [code_abbrev]: "remove x A = A - {x}" - -hide_const (open) remove - -lemma member_remove [simp]: "x \ Set.remove y A \ x \ A \ x \ y" - by (simp add: remove_def) - -definition filter :: "('a \ bool) \ 'a set \ 'a set" - where [code_abbrev]: "filter P A = {a \ A. P a}" - -hide_const (open) filter - -lemma member_filter [simp]: "x \ Set.filter P A \ x \ A \ P x" - by (simp add: filter_def) +text \ + Use those operations only for generating executable / efficient code. + Otherwise use the RHSs directly. +\ + +context +begin + +qualified definition is_empty :: "'a set \ bool" + where is_empty_iff [code_abbrev, simp]: "is_empty A \ A = {}" + +qualified definition remove :: "'a \ 'a set \ 'a set" + where remove_eq [code_abbrev, simp]: "remove x A = A - {x}" + +qualified definition filter :: "('a \ bool) \ 'a set \ 'a set" + where filter_eq [code_abbrev, simp]: "filter P A = {a \ A. P a}" + +end instantiation set :: (equal) equal begin definition "HOL.equal A B \ A \ B \ B \ A" -instance by standard (auto simp add: equal_set_def) +instance + by standard (auto simp add: equal_set_def) end