# HG changeset patch
# User haftmann
# Date 1750951529 -7200
# Node ID 4ec8e654112fdce0809d01ea206844f5e93005ab
# Parent  59b937edcff8a7c10e00fb290863855b1b915d46
scope pending code equations to theories

diff -r 59b937edcff8 -r 4ec8e654112f NEWS
--- a/NEWS	Thu Jun 26 17:30:33 2025 +0200
+++ b/NEWS	Thu Jun 26 17:25:29 2025 +0200
@@ -136,6 +136,9 @@
 subset_refl, subset_trans, vimageD, vimageE, vimageI, vimageI2, vimage_Collect,
 vimage_Int, vimage_Un. INCOMPATIBILITY, use thm(s) antiquotation instead.
 
+* Clarified semantics for adding code equations: code equations from preceeding
+theories are superseded. Minor INCOMPATIBILITY.
+
 * Normalization by evaluation (method "normalization", command value) could
 yield false positives due to incomplete handling of polymorphism in certain
 situations; this is now corrected.
diff -r 59b937edcff8 -r 4ec8e654112f src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -2383,6 +2383,24 @@
 
   Variant \<open>code equation\<close> declares a conventional equation as code equation.
 
+  Variant \<open>code nbe\<close> accepts also non-left-linear equations for
+  \<^emph>\<open>normalization by evaluation\<close> only.
+
+  Variant \<open>code del\<close> deselects a code equation for code generation.
+
+  Multiple \<open>code equation\<close> / \<open>code nbe\<close> declarations referring to the same
+  constant within the same theory are handled as \<^emph>\<open>one\<close> function declaration
+  for that particular constant: the first code declaration within a theory
+  disregards any previous function declaration and superseedes any equations
+  from preceeding theories.
+
+  Each code equation is prepended to existing code equations declared in
+  the same theory, with syntactically subsumed equations removed.
+
+  Packages usually provide reasonable default code equations; an explicit
+  declaration of a code equation superseedes any preceeding default code
+  equations.
+
   Variants \<open>code abstype\<close> and \<open>code abstract\<close> declare abstract datatype
   certificates or code equations on abstract datatype representations
   respectively.
@@ -2390,19 +2408,11 @@
   Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstract\<close>
   depending on the syntactic shape of the underlying equation.
 
-  Variant \<open>code del\<close> deselects a code equation for code generation.
-
-  Variant \<open>code nbe\<close> accepts also non-left-linear equations for
-  \<^emph>\<open>normalization by evaluation\<close> only.
-
   Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constants as arguments
   and drop all code equations declared for them. In the case of \<open>abort\<close>,
   these constants if needed are implemented by program abort
   (exception).
 
-  Packages declaring code equations usually provide a reasonable default
-  setup.
-
   \<^descr> @{command (HOL) "code_datatype"} specifies a constructor set for a logical
   type.
 
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -112,7 +112,6 @@
 definition f1 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat llist \<Rightarrow> unit" where
   "f1 _ _ _ _ = ()"
 
-declare [[code drop: f1]]
 lemma f1_code1 [code]: 
   "f1 b c d    ns     = Code.abort (STR ''4'') (\<lambda>_. ())" 
   "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())" 
@@ -167,7 +166,6 @@
 
 definition f2 :: "nat llist llist list \<Rightarrow> unit" where "f2 _ = ()"
 
-declare [[code drop: f2]]
 lemma f2_code1 [code]:
   "f2 xs = Code.abort (STR ''a'') (\<lambda>_. ())"
   "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]] = ()"
@@ -182,7 +180,6 @@
 
 definition f3 :: "nat set llist \<Rightarrow> unit" where "f3 _ = ()"
 
-declare [[code drop: f3]]
 lemma f3_code1 [code]:
   "f3 \<^bold>[\<^bold>] = ()"
   "f3 \<^bold>[A\<^bold>] = ()"
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Filter.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -2088,9 +2088,7 @@
 
 hide_const (open) abstract_filter
 
-declare [[code drop: filterlim prod_filter filtermap eventually
-  "inf :: _ filter \<Rightarrow> _" "sup :: _ filter \<Rightarrow> _" "less_eq :: _ filter \<Rightarrow> _"
-  Abs_filter]]
+declare [[code drop: Abs_filter]]
 
 declare filterlim_principal [code]
 declare principal_prod_principal [code]
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -7,9 +7,9 @@
 subsubsection "Pretty printing state sets"
 
 text\<open>Tweak code generation to work with sets of non-equality types:\<close>
-declare insert_code[code del] union_coset_filter[code del]
-lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
-by simp
+lemma insert_code [code]: "insert x (set xs) = set (x#xs)"
+  and union_code [code]: "set xs \<union> A = fold insert xs A"
+  by (simp_all add: union_set_fold)
 
 text\<open>Compensate for the fact that sets may now have duplicates:\<close>
 definition compact :: "'a set \<Rightarrow> 'a set" where
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -43,8 +43,6 @@
 context
 begin
 
-declare [[code drop: "plus :: nat \<Rightarrow> _"]]  
-
 lemma plus_nat_code [code]:
   "nat_of_num k + nat_of_num l = nat_of_num (k + l)"
   "m + 0 = (m::nat)"
@@ -79,24 +77,18 @@
     Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def 
     sub_non_positive nat_add_distrib sub_non_negative)
 
-declare [[code drop: "minus :: nat \<Rightarrow> _"]]
-
 lemma minus_nat_code [code]:
   "nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
   "m - 0 = (m::nat)"
   "0 - n = (0::nat)"
   by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
 
-declare [[code drop: "times :: nat \<Rightarrow> _"]]
-
 lemma times_nat_code [code]:
   "nat_of_num k * nat_of_num l = nat_of_num (k * l)"
   "m * 0 = (0::nat)"
   "0 * n = (0::nat)"
   by (simp_all add: nat_of_num_numeral)
 
-declare [[code drop: "HOL.equal :: nat \<Rightarrow> _"]]
-
 lemma equal_nat_code [code]:
   "HOL.equal 0 (0::nat) \<longleftrightarrow> True"
   "HOL.equal 0 (nat_of_num l) \<longleftrightarrow> False"
@@ -108,24 +100,18 @@
   "HOL.equal (n::nat) n \<longleftrightarrow> True"
   by (rule equal_refl)
 
-declare [[code drop: "less_eq :: nat \<Rightarrow> _"]]
-
 lemma less_eq_nat_code [code]:
   "0 \<le> (n::nat) \<longleftrightarrow> True"
   "nat_of_num k \<le> 0 \<longleftrightarrow> False"
   "nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l"
   by (simp_all add: nat_of_num_numeral)
 
-declare [[code drop: "less :: nat \<Rightarrow> _"]]
-
 lemma less_nat_code [code]:
   "(m::nat) < 0 \<longleftrightarrow> False"
   "0 < nat_of_num l \<longleftrightarrow> True"
   "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
   by (simp_all add: nat_of_num_numeral)
 
-declare [[code drop: Euclidean_Rings.divmod_nat]]
-  
 lemma divmod_nat_code [code]:
   "Euclidean_Rings.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
   "Euclidean_Rings.divmod_nat m 0 = (0, m)"
@@ -137,8 +123,6 @@
 
 subsection \<open>Conversions\<close>
 
-declare [[code drop: of_nat]]
-
 lemma of_nat_code [code]:
   "of_nat 0 = 0"
   "of_nat (nat_of_num k) = numeral k"
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Library/Code_Cardinality.thy
--- a/src/HOL/Library/Code_Cardinality.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Library/Code_Cardinality.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -16,7 +16,7 @@
 begin
 
 qualified definition card_UNIV' :: "'a card_UNIV"
-where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
+where "card_UNIV' = Phantom('a) CARD('a)"
 
 lemma CARD_code [code_unfold]:
   "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)"
@@ -36,7 +36,7 @@
 begin
 
 qualified definition finite' :: "'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "finite' = finite"
+where [simp, code_abbrev]: "finite' = finite"
 
 lemma finite'_code [code]:
   "finite' (set xs) \<longleftrightarrow> True"
@@ -49,7 +49,7 @@
 begin
 
 qualified definition card' :: "'a set \<Rightarrow> nat" 
-where [simp, code del, code_abbrev]: "card' = card"
+where [simp, code_abbrev]: "card' = card"
  
 lemma card'_code [code]:
   "card' (set xs) = length (remdups xs)"
@@ -58,7 +58,7 @@
 
 
 qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)"
+where [simp, code_abbrev]: "subset' = (\<subseteq>)"
 
 lemma subset'_code [code]:
   "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
@@ -68,7 +68,7 @@
   (metis finite_compl finite_set rev_finite_subset)
 
 qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "eq_set = (=)"
+where [simp, code_abbrev]: "eq_set = (=)"
 
 lemma eq_set_code [code]:
   fixes ys
@@ -122,19 +122,22 @@
   Constrain the element type with sort \<^class>\<open>card_UNIV\<close> to change this.
 \<close>
 
-lemma card_coset_error [code]:
-  "card (List.coset xs) = 
+lemma card_code [code]:
+  "card (set xs) = length (remdups xs)"
+  "card (List.coset xs) =
    Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'')
      (\<lambda>_. card (List.coset xs))"
-by(simp)
+  by (simp_all add: length_remdups_card_conv)
 
 lemma coset_subseteq_set_code [code]:
+  "set xs \<subseteq> B = list_all (\<lambda>x. x \<in> B) xs"
+  "A \<subseteq> List.coset ys = list_all (\<lambda>y. y \<notin> A) ys"
   "List.coset xs \<subseteq> set ys \<longleftrightarrow> 
   (if xs = [] \<and> ys = [] then False 
    else Code.abort
      (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
      (\<lambda>_. List.coset xs \<subseteq> set ys))"
-by simp
+  by (auto simp add: list_all_iff)
 
 notepad begin \<comment> \<open>test code setup\<close>
 have "List.coset [True] = set [False] \<and> 
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -10,8 +10,6 @@
 
 code_datatype int_of_integer
 
-declare [[code drop: integer_of_int]]
-
 context
 includes integer.lifting
 begin
@@ -112,8 +110,6 @@
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
 
-declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
-
 lemma gcd_int_of_integer [code]:
   "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
   by transfer rule
@@ -163,10 +159,6 @@
   includes integer.lifting and bit_operations_syntax
 begin
 
-declare [[code drop: \<open>bit :: int \<Rightarrow> _\<close> \<open>not :: int \<Rightarrow> _\<close>
-  \<open>and :: int \<Rightarrow> _\<close> \<open>or :: int \<Rightarrow> _\<close> \<open>xor :: int \<Rightarrow> _\<close>
-  \<open>push_bit :: _ \<Rightarrow> _ \<Rightarrow> int\<close> \<open>drop_bit :: _ \<Rightarrow> _ \<Rightarrow> int\<close> \<open>take_bit :: _ \<Rightarrow> _ \<Rightarrow> int\<close>]]
-
 lemma [code]:
   \<open>bit (int_of_integer k) n \<longleftrightarrow> bit k n\<close>
   by transfer rule
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -194,10 +194,6 @@
   includes integer.lifting and bit_operations_syntax
 begin
 
-declare [[code drop: \<open>bit :: nat \<Rightarrow> _\<close>
-  \<open>and :: nat \<Rightarrow> _\<close> \<open>or :: nat \<Rightarrow> _\<close> \<open>xor :: nat \<Rightarrow> _\<close>
-  \<open>push_bit :: _ \<Rightarrow> _ \<Rightarrow> nat\<close> \<open>drop_bit :: _ \<Rightarrow> _ \<Rightarrow> nat\<close> \<open>take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat\<close>]]
-
 lemma [code]:
   \<open>bit m n \<longleftrightarrow> bit (integer_of_nat m) n\<close>
   by transfer (simp add: bit_simps)
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -25,17 +25,6 @@
   where [simp]: "Coset t = - Set t"
 
 
-section \<open>Deletion of already existing code equations\<close>
-
-declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set
-  Set.member Set.insert Set.remove UNIV Set.filter image
-  Set.subset_eq Ball Bex Set.can_select Set.union minus_set_inst.minus_set Set.inter
-  card the_elem Pow sum prod Product_Type.product Id_on
-  Image trancl relcomp wf_on wf_code Min Inf_fin Max Sup_fin
-  "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"
-  sorted_list_of_set List.map_project List.Least List.Greatest]]
-
-
 section \<open>Lemmas\<close>
 
 subsection \<open>Auxiliary lemmas\<close>
@@ -582,6 +571,15 @@
     by (auto simp add: sum.eq_fold finite_fold_fold_keys o_def)
 qed
 
+lemma prod_Set [code]:
+  "prod f (Set xs) = fold_keys (times \<circ> f) xs 1"
+proof -
+  have "comp_fun_commute (\<lambda>x. (*) (f x))"
+    by standard (auto simp: ac_simps)
+  then show ?thesis 
+    by (auto simp add: prod.eq_fold finite_fold_fold_keys o_def)
+qed
+
 lemma the_elem_set [code]:
   fixes t :: "('a :: linorder, unit) rbt"
   shows "the_elem (Set t) = (case RBT.impl_of t of 
@@ -666,6 +664,8 @@
   "Inf_fin (Set t) = Min (Set t)"
 by (simp add: inf_min Inf_fin_def Min_def)
 
+declare [[code drop: "Inf :: _ \<Rightarrow> 'a set"]]
+
 lemma Inf_Set_fold:
   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
@@ -695,6 +695,8 @@
   "Sup_fin (Set t) = Max (Set t)"
 by (simp add: sup_max Sup_fin_def Max_def)
 
+declare [[code drop: "Sup :: _ \<Rightarrow> 'a set"]]
+
 lemma Sup_Set_fold:
   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
@@ -711,7 +713,21 @@
 context
 begin
 
-declare [[code drop: Gcd_fin Lcm_fin \<open>Gcd :: _ \<Rightarrow> nat\<close> \<open>Gcd :: _ \<Rightarrow> int\<close> \<open>Lcm :: _ \<Rightarrow> nat\<close> \<open>Lcm :: _ \<Rightarrow> int\<close>]]
+qualified definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a"
+  where [code_abbrev]: "Inf' = Inf"
+
+lemma Inf'_Set_fold [code]:
+  "Inf' (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
+  by (simp add: Inf'_def Inf_Set_fold)
+
+qualified definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a"
+  where [code_abbrev]: "Sup' = Sup"
+
+lemma Sup'_Set_fold [code]:
+  "Sup' (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
+  by (simp add: Sup'_def Sup_Set_fold)
+
+end
 
 lemma [code]:
   "Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) = fold_keys gcd t (0::'a::{semiring_gcd, linorder})"
@@ -724,7 +740,7 @@
   then show ?thesis
     by (simp add: Gcd_fin.eq_fold)
 qed
-    
+
 lemma [code]:
   "Gcd (Set t) = (Gcd\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
   by simp
@@ -745,30 +761,14 @@
     by (simp add: Lcm_fin.eq_fold)
 qed
 
-lemma [code drop: "Lcm :: _ \<Rightarrow> nat", code]:
+lemma [code]:
   "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: nat)"
   by simp
 
-lemma [code drop: "Lcm :: _ \<Rightarrow> int", code]:
+lemma [code]:
   "Lcm (Set t) = (Lcm\<^sub>f\<^sub>i\<^sub>n (Set t) :: int)"
   by simp
 
-qualified definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a"
-  where [code_abbrev]: "Inf' = Inf"
-
-lemma Inf'_Set_fold [code]:
-  "Inf' (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
-  by (simp add: Inf'_def Inf_Set_fold)
-
-qualified definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a"
-  where [code_abbrev]: "Sup' = Sup"
-
-lemma Sup'_Set_fold [code]:
-  "Sup' (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
-  by (simp add: Sup'_def Sup_Set_fold)
-
-end
-
 lemma sorted_list_set [code]: "sorted_list_of_set (Set t) = RBT.keys t"
   by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
 
@@ -788,6 +788,9 @@
     apply auto
   done
 
+declare [[code drop: Set.can_select List.map_project Wellfounded.acc pred_of_set
+  \<open>Inf :: _ \<Rightarrow> 'a Predicate.pred\<close> \<open>Sup :: _ \<Rightarrow> 'a Predicate.pred\<close>]]
+
 hide_const (open) RBT_Set.Set RBT_Set.Coset
 
 end
diff -r 59b937edcff8 -r 4ec8e654112f src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -271,8 +271,6 @@
 
 end
 
-declare [[code drop: "partial_term_of :: int itself \<Rightarrow> _"]]
-
 lemma [code]:
   "partial_term_of (ty :: int itself) (Narrowing_variable p t) \<equiv>
     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
@@ -293,8 +291,6 @@
 
 end
 
-declare [[code drop: "partial_term_of :: integer itself \<Rightarrow> _"]]  
-
 lemma [code]:
   "partial_term_of (ty :: integer itself) (Narrowing_variable p t) \<equiv>
     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Code_Numeral.integer'') [])"
diff -r 59b937edcff8 -r 4ec8e654112f src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/Pure/Isar/code.ML	Thu Jun 26 17:25:29 2025 +0200
@@ -456,15 +456,8 @@
    declarations as "pending" and historize them as proper declarations
    at the end of each theory. *)
 
-fun modify_pending_eqns c f specs =
-  let
-    val existing_eqns = case History.lookup (functions_of specs) c of
-        SOME (Eqns (false, eqns)) => eqns
-      | _ => [];
-  in
-    specs
-    |> map_pending_eqns (Symtab.map_default (c, existing_eqns) f)
-  end;
+fun modify_pending_eqns c f =
+  map_pending_eqns (Symtab.map_default (c, []) f);
 
 fun register_fun_spec c spec =
   map_pending_eqns (Symtab.delete_safe c)