--- 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
--- 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>
--- 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>
--- 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')
--- 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
--- 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
--- 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"
--- 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]:
--- 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)
--- 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 +
--- 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'.
--- 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"
--- 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])
--- 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!).