--- 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.
--- 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.
--- 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>] = ()"
--- 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]
--- 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
--- 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"
--- 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>
--- 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
--- 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)
--- 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
--- 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'') [])"
--- 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)