# HG changeset patch
# User haftmann
# Date 1749500078 -7200
# Node ID b69e4da2604bfd4cd2289dcde50cb5c47c9784eb
# Parent  cccbfa567117415ab061d2e2ca866606831e2395
more qualified auxiliary operations

diff -r cccbfa567117 -r b69e4da2604b NEWS
--- a/NEWS	Fri Jun 06 18:36:29 2025 +0100
+++ b/NEWS	Mon Jun 09 22:14:38 2025 +0200
@@ -87,11 +87,17 @@
     thm remove_def ~> Set.remove_eq [simp]
 
     const Set.filter
-    thm filter_def → Set.filter_eq [simp]
+    thm filter_def ~> Set.filter_eq [simp]
 
     const [List.]can_select ~> Set.can_select
     thm can_select_def ~> Set.can_select_iff [simp]
 
+    const member ~> List.member
+    thm member_def ~> List.member_iff [simp]
+
+    const null ~> List.null
+    thm null_def ~> List.null_iff [simp]
+
     const List.all_interval_nat List.all_interval_int
     discontinued in favour of a generic List.all_range
 
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -550,7 +550,7 @@
   where [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
 
 lemma is_zero_null [code_abbrev]: "is_zero p \<longleftrightarrow> p = 0"
-  by (simp add: is_zero_def null_def)
+  by (simp add: is_zero_def)
 
 
 text \<open>Reconstructing the polynomial from the list\<close>
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -286,7 +286,7 @@
 
 lemma NULL[import_const NULL : List.null]:
   "List.null ([]::'t18373 list) = True \<and> List.null ((h::'t18373) # t) = False"
-  unfolding null_def by simp
+  by simp
 
 lemma ALL[import_const ALL : list_all]:
   "list_all (P::'t18393 \<Rightarrow> bool) [] = True \<and>
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Library/AList_Mapping.thy
--- a/src/HOL/Library/AList_Mapping.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Library/AList_Mapping.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -22,7 +22,7 @@
   by transfer simp
 
 lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
-  by (cases xs) (simp_all add: is_empty_def null_def)
+  by (cases xs) (simp_all add: is_empty_def)
 
 lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
   by transfer (simp add: update_conv')
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Library/Dlist.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -189,7 +189,7 @@
   next
     case (Cons x xs)
     then have "\<not> Dlist.member (Dlist xs) x" and "P (Dlist xs)"
-      by (simp_all add: Dlist.member_def List.member_def)
+      by (simp_all add: Dlist.member_def)
     with insrt have "P (Dlist.insert x (Dlist xs))" .
     with Cons show ?case by (simp add: Dlist.insert_def distinct_remdups_id)
   qed
@@ -212,7 +212,7 @@
     case (Cons x xs)
     with dxs distinct have "\<not> Dlist.member (Dlist xs) x"
       and "dxs = Dlist.insert x (Dlist xs)"
-      by (simp_all add: Dlist.member_def List.member_def Dlist.insert_def distinct_remdups_id)
+      by (simp_all add: Dlist.member_def Dlist.insert_def distinct_remdups_id)
     with insert show ?thesis .
   qed
 qed
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -4318,7 +4318,7 @@
   by simp
 
 lemma [code]: "Multiset.is_empty (mset xs) \<longleftrightarrow> List.null xs"
-  by (simp add: Multiset.is_empty_def List.null_def)
+  by (simp add: Multiset.is_empty_def)
 
 lemma union_code [code]: "mset xs + mset ys = mset (xs @ ys)"
   by simp
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -220,15 +220,17 @@
 
 subsection \<open>Alternative rules for membership in lists\<close>
 
-declare in_set_member[code_pred_inline]
+lemma in_set_member [code_pred_inline]:
+  "x \<in> set xs \<longleftrightarrow> List.member xs x"
+  by simp
 
 lemma member_intros [code_pred_intro]:
   "List.member (x#xs) x"
   "List.member xs x \<Longrightarrow> List.member (y#xs) x"
-by(simp_all add: List.member_def)
+  by simp_all
 
 code_pred List.member
-  by(auto simp add: List.member_def elim: list.set_cases)
+  by(auto simp add: elim: list.set_cases)
 
 code_identifier constant member_i_i
    \<rightharpoonup> (SML) "List.member_i_i"
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Library/Sublist.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -1462,7 +1462,7 @@
   case (1 P xs ys)
   show ?case
     by (induction ys arbitrary: xs)
-       (auto simp: list_emb_code List.null_def split: list.splits)
+       (auto simp: list_emb_code split: list.splits)
 qed
 
 lemma prefix_transfer [transfer_rule]:
diff -r cccbfa567117 -r b69e4da2604b src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/List.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -7846,20 +7846,23 @@
 
 subsubsection \<open>Counterparts for set-related operations\<close>
 
-definition member :: \<open>'a list \<Rightarrow> 'a \<Rightarrow> bool\<close>
-  where [code_abbrev]: \<open>member xs x \<longleftrightarrow> x \<in> set xs\<close>
+context
+begin
+
+qualified definition member :: \<open>'a list \<Rightarrow> 'a \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
+  where member_iff [code_abbrev, simp]: \<open>member xs x \<longleftrightarrow> x \<in> set xs\<close>
 
 text \<open>
   Use \<open>member\<close> only for generating executable code.  Otherwise use
   \<^prop>\<open>x \<in> set xs\<close> instead --- it is much easier to reason about.
 \<close>
 
-lemma member_rec [code]:
-  \<open>member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y\<close>
+qualified lemma member_code [code, no_atp]:
   \<open>member [] y \<longleftrightarrow> False\<close>
-  by (auto simp add: member_def)
-
-hide_const (open) member
+  \<open>member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y\<close>
+  by auto
+
+end
 
 lemma list_all_iff [code_abbrev]:
   \<open>list_all P xs \<longleftrightarrow> Ball (set xs) P\<close>
@@ -7941,8 +7944,8 @@
 
 text \<open>Executable checks for relations on sets\<close>
 
-definition listrel1p :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close>
-  where \<open>listrel1p r xs ys \<longleftrightarrow> (xs, ys) \<in> listrel1 {(x, y). r x y}\<close>
+definition listrel1p :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
+  where  \<open>listrel1p r xs ys \<longleftrightarrow> (xs, ys) \<in> listrel1 {(x, y). r x y}\<close>
 
 lemma [code_unfold]:
   \<open>(xs, ys) \<in> listrel1 r \<longleftrightarrow> listrel1p (\<lambda>x y. (x, y) \<in> r) xs ys\<close>
@@ -7955,7 +7958,7 @@
      r x y \<and> xs = ys \<or> x = y \<and> listrel1p r xs ys\<close>
   by (simp_all add: listrel1p_def)
 
-definition lexordp :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close>
+definition lexordp :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
   where \<open>lexordp r xs ys \<longleftrightarrow> (xs, ys) \<in> lexord {(x, y). r x y}\<close>
 
 lemma [code_unfold]:
@@ -8145,24 +8148,23 @@
 
 subsubsection \<open>Operations for optimization and efficiency\<close>
 
-definition null :: \<open>'a list \<Rightarrow> bool\<close>
-  where [code_abbrev]: \<open>null xs \<longleftrightarrow> xs = []\<close>
-
-text \<open>
-  Efficient emptyness check is implemented by \<^const>\<open>null\<close>.
-\<close>
-
-lemma null_rec [code]:
+context
+begin
+
+qualified definition null :: \<open>'a list \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
+  where null_iff [code_abbrev, simp]: \<open>null xs \<longleftrightarrow> xs = []\<close>
+
+lemma null_code [code, no_atp]:
+  \<open>null [] \<longleftrightarrow> True\<close>
   \<open>null (x # xs) \<longleftrightarrow> False\<close>
-  \<open>null [] \<longleftrightarrow> True\<close>
-  by (simp_all add: null_def)
-
-lemma equal_Nil_null [code_unfold]:
+  by simp_all
+
+lemma equal_Nil_null [code_unfold, no_atp]:
   \<open>HOL.equal xs [] \<longleftrightarrow> null xs\<close>
   \<open>HOL.equal [] = null\<close>
-  by (auto simp add: equal null_def)
-
-hide_const (open) null
+  by (auto simp add: equal)
+
+end
 
 
 text \<open>optimized code (tail-recursive) for \<^term>\<open>length\<close>\<close>
@@ -8185,7 +8187,6 @@
 definition maps :: \<open>('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list\<close>
   where [code_abbrev]: \<open>maps f xs = concat (map f xs)\<close>
 
-
 text \<open>
   Operation \<^const>\<open>maps\<close> avoids
   intermediate lists on execution -- do not use for proving.
@@ -8203,7 +8204,7 @@
 
 lemma is_empty_set [code]:
   "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
-  by (simp add: null_def)
+  by simp
 
 lemma empty_set [code]:
   "{} = set []"
@@ -8224,7 +8225,7 @@
 lemma [code]:
   "x \<in> set xs \<longleftrightarrow> List.member xs x"
   "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
-  by (simp_all add: member_def)
+  by simp_all
 
 lemma insert_code [code]:
   "insert x (set xs) = set (List.insert x xs)"
@@ -8238,7 +8239,7 @@
 
 lemma filter_set [code]:
   "Set.filter P (set xs) = set (filter P xs)"
-  by auto
+  by simp
 
 lemma image_set [code]:
   "image f (set xs) = set (map f xs)"
@@ -8294,7 +8295,7 @@
 
 lemma [code]:
   "R `` S = List.map_project (\<lambda>(x, y). if x \<in> S then Some y else None) R"
-  unfolding map_project_def by (auto split: prod.split if_split_asm)
+  by (auto simp add: map_project_def split: prod.split if_split_asm)
 
 lemma trancl_set_ntrancl [code]:
   "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
@@ -8302,13 +8303,14 @@
 
 lemma set_relcomp [code]:
   "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
-  by auto (auto simp add: Bex_def image_def)
+  by simp (auto simp add: Bex_def image_def)
 
 lemma wf_set:
   "wf (set xs) = acyclic (set xs)"
   by (simp add: wf_iff_acyclic_if_finite)
 
-lemma wf_code_set[code]: "wf_code (set xs) = acyclic (set xs)"
+lemma wf_code_set [code]:
+  "wf_code (set xs) = acyclic (set xs)"
   unfolding wf_code_def using wf_set .
 
 text \<open>\<open>LEAST\<close> and \<open>GREATEST\<close> operator.\<close>
@@ -8644,7 +8646,7 @@
 
 lemma null_transfer [transfer_rule]:
   "(list_all2 A ===> (=)) List.null List.null"
-  unfolding rel_fun_def List.null_def by auto
+  unfolding rel_fun_def by auto
 
 lemma list_all_transfer [transfer_rule]:
   "((A ===> (=)) ===> list_all2 A ===> (=)) list_all list_all"
@@ -8710,14 +8712,6 @@
   "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs"
   by (induct xs) auto
 
-lemma in_set_member (* FIXME delete candidate *):
-  "x \<in> set xs \<longleftrightarrow> List.member xs x"
-  by (simp add: member_def)
-
-lemma eq_Nil_null: (* FIXME delete candidate *)
-  "xs = [] \<longleftrightarrow> List.null xs"
-  by (simp add: null_def)
-
 lemma concat_map_maps: (* FIXME delete candidate *)
   "concat (map f xs) = List.maps f xs"
   by (simp add: maps_def)
diff -r cccbfa567117 -r b69e4da2604b src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -20,7 +20,7 @@
 lemma [code]:
   "is_target step phi pc' =
     list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]"
-by (force simp: list_ex_iff member_def is_target_def)
+  by (force simp: list_ex_iff is_target_def)
 
 
 locale lbvc = lbv + 
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -57,10 +57,10 @@
 unfolding hotel.simps issuedp_def cardsp_def isinp_def
 by (auto split: event.split)
 
-declare List.member_rec[code_pred_def]
+declare List.member_code [code_pred_def]
 
 lemma [code_pred_def]: "no_Check_in s r = (\<not> (\<exists>g c. List.member s (Check_in g r c)))"
-unfolding no_Check_in_def member_def by auto
+  by (simp add: no_Check_in_def)
 
 lemma [code_pred_def]: "feels_safe s r =
 (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Quotient_Examples/DList.thy
--- a/src/HOL/Quotient_Examples/DList.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Quotient_Examples/DList.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -60,11 +60,12 @@
 
 lemma remdups_eq_member_eq:
   assumes "remdups xa = remdups ya"
-    shows "List.member xa = List.member ya"
-  using assms
-  unfolding fun_eq_iff List.member_def
-  by (induct xa ya rule: list_induct2')
-     (metis remdups_nil_noteq_cons set_remdups)+
+  shows "List.member xa = List.member ya"
+proof -
+  from assms have \<open>set (remdups xa) = set (remdups ya)\<close>
+    by simp
+  then show ?thesis by (simp add: fun_eq_iff)
+qed
 
 text \<open>Setting up the quotient type\<close>
 
@@ -129,11 +130,11 @@
 
 lemma dlist_member_insert:
   "member dl x \<Longrightarrow> insert x dl = dl"
-  by descending (simp add: List.member_def)
+  by descending simp
 
 lemma dlist_member_insert_eq:
   "member (insert y dl) x = (x = y \<or> member dl x)"
-  by descending (simp add: List.member_def)
+  by descending simp
 
 lemma dlist_insert_idem:
   "insert x (insert x dl) = insert x dl"
@@ -145,23 +146,23 @@
 
 lemma not_dlist_member_empty:
   "\<not> member empty x"
-  by descending (simp add: List.member_def)
+  by descending simp
 
 lemma not_dlist_member_remove:
   "\<not> member (remove x dl) x"
-  by descending (simp add: List.member_def)
+  by descending simp
 
 lemma dlist_in_remove:
   "a \<noteq> b \<Longrightarrow> member (remove b dl) a = member dl a"
-  by descending (simp add: List.member_def)
+  by descending simp
 
 lemma dlist_not_memb_remove:
   "\<not> member dl x \<Longrightarrow> remove x dl = dl"
-  by descending (simp add: List.member_def)
+  by descending simp
 
 lemma dlist_no_memb_remove_insert:
   "\<not> member dl x \<Longrightarrow> remove x (insert x dl) = dl"
-  by descending (simp add: List.member_def)
+  by descending simp
 
 lemma dlist_remove_empty:
   "remove x empty = empty"
@@ -182,12 +183,12 @@
 lemma dlist_no_memb_foldr:
   assumes "\<not> member dl x"
   shows "foldr f (insert x dl) e = f x (foldr f dl e)"
-  using assms by descending (simp add: List.member_def)
+  using assms by descending simp
 
 lemma dlist_foldr_insert_not_memb:
   assumes "\<not>member t h"
   shows "foldr f (insert h t) e = f h (foldr f t e)"
-  using assms by descending (simp add: List.member_def)
+  using assms by descending simp
 
 lemma list_of_dlist_empty[simp]:
   "list_of_dlist empty = []"
@@ -197,7 +198,7 @@
   "list_of_dlist (insert x xs) =
     (if member xs x then (remdups (list_of_dlist xs))
     else x # (remdups (list_of_dlist xs)))"
-  by descending (simp add: List.member_def remdups_remdups)
+  by descending (simp add: remdups_remdups)
 
 lemma list_of_dlist_remove[simp]:
   "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
@@ -280,8 +281,10 @@
 
 lemma dlist_cases:
   "dl = empty \<or> (\<exists>h t. dl = insert h t \<and> \<not> member t h)"
-  by descending
-    (metis List.member_def dlist_eq_def hd_Cons_tl list_of_dlist_dlist remdups_hd_notin_tl remdups_list_of_dlist)
+  apply descending
+  apply auto
+  apply (metis neq_Nil_conv remdups_eq_nil_right_iff remdups_hd_notin_tl remdups_repeat)
+  done
 
 lemma dlist_exhaust:
   obtains "y = empty" | a dl where "y = insert a dl"
diff -r cccbfa567117 -r b69e4da2604b src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -54,8 +54,6 @@
   lists.
 \<close>
 
-declare List.member_def [simp]
-
 definition
   sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 where 
@@ -978,7 +976,7 @@
   proof (cases "xs=[]")
     case True
     then show ?thesis
-      using Cons.prems member_rec(2) by fastforce
+      using Cons.prems by auto (metis empty_iff empty_subsetI list.set(1)) 
   next
     case False
     have "\<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" for x ys
@@ -1091,8 +1089,8 @@
     have d: "card_list l = Suc m" by fact
     then have "\<exists>a. List.member l a" by (auto dest: card_eq_SucD)
     then obtain a where e: "List.member l a" by auto
-    then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b 
-      by auto
+    then have e': "List.member r a" using list_eq_def [of l r] b 
+      by simp
     have f: "card_list (removeAll a l) = m" using e d by (simp)
     have g: "removeAll a l \<approx> removeAll a r" using remove_fset.rsp b by simp
     have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
diff -r cccbfa567117 -r b69e4da2604b src/HOL/ex/Execute_Choice.thy
--- a/src/HOL/ex/Execute_Choice.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/ex/Execute_Choice.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -66,7 +66,7 @@
   shows [code]: "valuesum (Mapping []) = 0"
   and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
     the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
-  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
+  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
 
 text \<open>
   As a side effect the precondition disappears (but note this has nothing to do with choice!).