--- 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,
--- 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 "\<Union>\<V> = topspace X"
using ABC UU \<V>_def by auto
moreover have "pairwise (separatedin X) \<V>"
- using pwU sep ABC unfolding \<V>_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 \<V>_def) (metis DiffD1 DiffD2 singleton_iff)
ultimately show ?thesis
by blast
qed
--- 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 "(\<lambda>z. if z = \<xi> then deriv g \<xi> else (g z - g \<xi>) / (z - \<xi>)) holomorphic_on S"
using \<xi> pole_lemma by blast
then show ?thesis
- using "\<section>" remove_def by fastforce
+ using "\<section>" by (smt (verit, best) DiffD2 singletonI)
qed
ultimately show "?P = ?Q" and "?P = ?R"
by meson+
--- 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 \<notin> prime_factors x"
using that and \<open>prime p\<close> 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 ((\<Prod>p\<in>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 (\<lambda>m. m ^ k \<le> n) {..n}))"
proof (cases "k > 0")
case True
- hence "{m. m ^ k \<le> n} \<subseteq> {..n}" by (rule nth_root_nat_aux1)
- hence "Set.filter (\<lambda>m. m ^ k \<le> n) {..n} = {m. m ^ k \<le> 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 \<le> n} \<subseteq> {..n}" by (rule nth_root_nat_aux1)
+ then have "Set.filter (\<lambda>m. m ^ k \<le> n) {..n} = {m. m ^ k \<le> n}"
+ by (auto simp:)
+ with True show ?thesis
+ by (simp add: nth_root_nat_def)
qed simp
function nth_root_nat_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
--- 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 \<Longrightarrow> 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 "(\<lambda>x A'. if P x then Set.insert x A' else A')"
by (fact comp_fun_commute_filter_fold)
from \<open>finite A\<close> 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 \<inter> B = Set.filter (\<lambda>x. x \<in> 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"
--- 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} \<subseteq> 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 \<open>(rel_frontier U - {b})\<close> 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} \<subseteq> 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 \<open>(rel_frontier U - {c})\<close> V j k]
+ by (auto simp add: image_iff) (metis DiffI singletonD subsetD)
qed
then show ?thesis
by (metis image_comp)
--- 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 \<in> A"
by (metis Max_in[of "f ` A"] imageE)
then have "P (A - {a})"
- using psubset member_remove by blast
+ using psubset(2) [of \<open>A - {a}\<close>] by auto
moreover
have "\<And>y. y \<in> A \<Longrightarrow> f y \<le> f a"
using \<open>f a = Max (f ` A)\<close> \<open>finite (f ` A)\<close> by simp
--- 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 (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
proof -
- from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> 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 \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> 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"
--- 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 \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> '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 \<Rightarrow> '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 |\<in>| ffilter P A) = (x |\<in>| A \<and> P x)"
- by (rule member_filter[Transfer.transferred])
+ by transfer simp
lemma fequalityI: "A |\<subseteq>| B \<Longrightarrow> B |\<subseteq>| A \<Longrightarrow> 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 \<subseteq> set ys \<Longrightarrow> fset_of_list xs |\<subseteq>| fset_of_list ys"
--- 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 \<open>finite (dom (\<lambda>x. if P x then m x else None))\<close>
+ 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 \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> '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)
--- 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 \<longleftrightarrow> t = empty"
by transfer (rule RBT_lookup_empty)
+lemma keys_empty_eq [simp]:
+ \<open>keys empty = []\<close>
+ by transfer simp
+
lemma sorted_keys [iff]:
"sorted (keys t)"
by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)
--- 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 \<open>foldi and Ball\<close>
@@ -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 \<inter> Set t = rbt_filter (\<lambda>k. k \<in> 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 (\<lambda>k A. Set.insert (f k) A) t {}"
--- 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 \<Longrightarrow> (rel_set A ===> (=)) finite finite"
--- 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) \<longleftrightarrow> 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)"
--- 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 @@
(\<lambda>(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
--- 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 "\<And>x y. \<lbrakk>x \<in> set (ftv T\<^sub>1 - ftv \<Gamma>); y \<in> pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)\<rbrakk>
\<Longrightarrow> x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> 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': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1"
using pi2 by auto
note x
--- 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
-
--- 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 \<le> k" by (intro Min_le) (auto simp: \<open>finite A\<close>)
moreover from * have "k \<le> 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:
--- 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 (\<lambda>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)
--- 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 \<open>Operations for execution\<close>
-definition is_empty :: "'a set \<Rightarrow> bool"
- where [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
-
-hide_const (open) is_empty
-
-definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
- where [code_abbrev]: "remove x A = A - {x}"
-
-hide_const (open) remove
-
-lemma member_remove [simp]: "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
- by (simp add: remove_def)
-
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
- where [code_abbrev]: "filter P A = {a \<in> A. P a}"
-
-hide_const (open) filter
-
-lemma member_filter [simp]: "x \<in> Set.filter P A \<longleftrightarrow> x \<in> A \<and> P x"
- by (simp add: filter_def)
+text \<open>
+ Use those operations only for generating executable / efficient code.
+ Otherwise use the RHSs directly.
+\<close>
+
+context
+begin
+
+qualified definition is_empty :: "'a set \<Rightarrow> bool"
+ where is_empty_iff [code_abbrev, simp]: "is_empty A \<longleftrightarrow> A = {}"
+
+qualified definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ where remove_eq [code_abbrev, simp]: "remove x A = A - {x}"
+
+qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ where filter_eq [code_abbrev, simp]: "filter P A = {a \<in> A. P a}"
+
+end
instantiation set :: (equal) equal
begin
definition "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
-instance by standard (auto simp add: equal_set_def)
+instance
+ by standard (auto simp add: equal_set_def)
end