append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
--- a/NEWS Thu Jun 26 17:25:29 2025 +0200
+++ b/NEWS Thu Jun 26 17:25:29 2025 +0200
@@ -136,8 +136,11 @@
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.
+* Clarified semantics for adding code equations
+ * Code equations from preceeding theories are superseded.
+ * Code equations declared in the course of a theory are appended, not
+ prepended.
+INCOMPATIBILITY.
* Normalization by evaluation (method "normalization", command value) could
yield false positives due to incomplete handling of polymorphism in certain
--- a/src/Doc/Codegen/Foundations.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/Doc/Codegen/Foundations.thy Thu Jun 26 17:25:29 2025 +0200
@@ -273,9 +273,9 @@
of (Some x, q') \<Rightarrow> (x, q'))"
lemma %quote strict_dequeue_AQueue [code]:
- "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
"strict_dequeue (AQueue xs []) =
(case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
+ "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
text \<open>
--- a/src/HOL/Basic_BNFs.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Basic_BNFs.thy Thu Jun 26 17:25:29 2025 +0200
@@ -19,12 +19,12 @@
inductive_set setr :: "'a + 'b \<Rightarrow> 'b set" for s :: "'a + 'b" where
"s = Inr x \<Longrightarrow> x \<in> setr s"
-lemma sum_set_defs[code]:
+lemma sum_set_defs [code]:
"setl = (\<lambda>x. case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {})"
"setr = (\<lambda>x. case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {})"
by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits)
-lemma rel_sum_simps[code, simp]:
+lemma rel_sum_simps [code, simp]:
"rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
"rel_sum R1 R2 (Inl a1) (Inr b2) = False"
"rel_sum R1 R2 (Inr a2) (Inl b1) = False"
@@ -37,7 +37,7 @@
"P1 a \<Longrightarrow> pred_sum P1 P2 (Inl a)"
| "P2 b \<Longrightarrow> pred_sum P1 P2 (Inr b)"
-lemma pred_sum_inject[code, simp]:
+lemma pred_sum_inject [code, simp]:
"pred_sum P1 P2 (Inl a) \<longleftrightarrow> P1 a"
"pred_sum P1 P2 (Inr b) \<longleftrightarrow> P2 b"
by (simp add: pred_sum.simps)+
--- a/src/HOL/Code_Numeral.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Code_Numeral.thy Thu Jun 26 17:25:29 2025 +0200
@@ -673,10 +673,10 @@
\<open>Pos (Num.Bit0 m) XOR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m XOR Pos n)\<close>
\<open>Pos (Num.Bit1 m) XOR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m XOR Pos n)\<close>
\<open>Pos (Num.Bit1 m) XOR Pos (Num.Bit1 n) = dup (Pos m XOR Pos n)\<close>
+ \<open>Neg Num.One XOR k = NOT k\<close>
+ \<open>k XOR Neg Num.One = NOT k\<close>
\<open>Neg m XOR k = NOT (sub m num.One XOR k)\<close>
\<open>k XOR Neg n = NOT (k XOR (sub n num.One))\<close>
- \<open>Neg Num.One XOR k = NOT k\<close>
- \<open>k XOR Neg Num.One = NOT k\<close>
\<open>0 XOR k = k\<close>
\<open>k XOR 0 = k\<close>
for k :: integer
@@ -707,14 +707,6 @@
by (fact flip_bit_def)
lemma [code]:
- \<open>push_bit n k = k * 2 ^ n\<close> for k :: integer
- by (fact push_bit_eq_mult)
-
-lemma [code]:
- \<open>drop_bit n k = k div 2 ^ n\<close> for k :: integer
- by (fact drop_bit_eq_div)
-
-lemma [code]:
\<open>take_bit n k = k AND mask n\<close> for k :: integer
by (fact take_bit_eq_mask)
@@ -828,6 +820,12 @@
minus_mod_eq_mult_div [symmetric] *)
qed
+lemma int_of_integer_code_nbe [code nbe]:
+ "int_of_integer 0 = 0"
+ "int_of_integer (Pos n) = Int.Pos n"
+ "int_of_integer (Neg n) = Int.Neg n"
+ by simp_all
+
lemma int_of_integer_code [code]:
"int_of_integer k = (if k < 0 then - (int_of_integer (- k))
else if k = 0 then 0
@@ -837,10 +835,10 @@
in if j = 0 then l' else l' + 1)"
by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
-lemma int_of_integer_code_nbe [code nbe]:
- "int_of_integer 0 = 0"
- "int_of_integer (Pos n) = Int.Pos n"
- "int_of_integer (Neg n) = Int.Neg n"
+lemma integer_of_int_code_nbe [code nbe]:
+ "integer_of_int 0 = 0"
+ "integer_of_int (Int.Pos n) = Pos n"
+ "integer_of_int (Int.Neg n) = Neg n"
by simp_all
lemma integer_of_int_code [code]:
@@ -852,12 +850,6 @@
in if j = 0 then l else l + 1)"
by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
-lemma integer_of_int_code_nbe [code nbe]:
- "integer_of_int 0 = 0"
- "integer_of_int (Int.Pos n) = Pos n"
- "integer_of_int (Int.Neg n) = Neg n"
- by simp_all
-
hide_const (open) Pos Neg sub dup divmod_abs
context
@@ -1550,13 +1542,13 @@
"integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
by transfer (simp add: zmod_int)
+lemma [code nbe]: "HOL.equal n (n::natural) \<longleftrightarrow> True"
+ by (rule equal_class.equal_refl)
+
lemma [code]:
"HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
by transfer (simp add: equal)
-lemma [code nbe]: "HOL.equal n (n::natural) \<longleftrightarrow> True"
- by (rule equal_class.equal_refl)
-
lemma [code]: "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
by transfer simp
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Thu Jun 26 17:25:29 2025 +0200
@@ -93,9 +93,6 @@
value [code] "mk_tree 10"
value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
-lemma mk_tree_Suc: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
- by(simp add: Let_def)
-lemmas [code] = mk_tree_0 mk_tree_Suc
value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
value [code] "let t = mk_tree 4; _ = subtree [True, True, False, False] t in t"
@@ -113,51 +110,51 @@
"f1 _ _ _ _ = ()"
lemma f1_code1 [code]:
+ "f1 True c d \<^bold>[\<^bold>] = ()"
+ "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\<lambda>_. ())"
+ "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
"f1 b c d ns = Code.abort (STR ''4'') (\<lambda>_. ())"
- "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
- "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\<lambda>_. ())"
- "f1 True c d \<^bold>[\<^bold>] = ()"
- by(simp_all add: f1_def)
+ by (simp_all add: f1_def)
value [code] "f1 True False False \<^bold>[\<^bold>]"
deactivate_lazy_type llist
value [code] "f1 True False False \<^bold>[\<^bold>]"
-declare f1_code1(1) [code del]
+declare f1_code1(4) [code del]
value [code] "f1 True False False \<^bold>[\<^bold>]"
activate_lazy_type llist
value [code] "f1 True False False \<^bold>[\<^bold>]"
declare [[code drop: f1]]
-lemma f1_code2 [code]:
+lemma f1_code2 [code]:
+ "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\<lambda>_. ())"
+ "f1 b True d \<^bold>[n\<^bold>] = ()"
+ "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
"f1 b c d ns = Code.abort (STR ''4'') (\<lambda>_. ())"
- "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
- "f1 b True d \<^bold>[n\<^bold>] = ()"
- "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\<lambda>_. ())"
- by(simp_all add: f1_def)
+ by (simp_all add: f1_def)
value [code] "f1 True True True \<^bold>[0\<^bold>]"
-declare f1_code2(1)[code del]
+declare f1_code2(4)[code del]
value [code] "f1 True True True \<^bold>[0\<^bold>]"
declare [[code drop: f1]]
lemma f1_code3 [code]:
- "f1 b c d ns = Code.abort (STR ''4'') (\<lambda>_. ())"
- "f1 b c True \<^bold>[n, m\<^bold>] = ()"
+ "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\<lambda>_. ())"
"f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\<lambda>_. ())"
- "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\<lambda>_. ())"
- by(simp_all add: f1_def)
+ "f1 b c True \<^bold>[n, m\<^bold>] = ()"
+ "f1 b c d ns = Code.abort (STR ''4'') (\<lambda>_. ())"
+ by (simp_all add: f1_def)
value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"
-declare f1_code3(1)[code del]
+declare f1_code3(4)[code del]
value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"
declare [[code drop: f1]]
lemma f1_code4 [code]:
- "f1 b c d ns = ()"
- "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
+ "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\<lambda>_. ())"
"f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\<lambda>_. ())"
- "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\<lambda>_. ())"
- by(simp_all add: f1_def)
+ "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
+ "f1 b c d ns = ()"
+ by (simp_all add: f1_def)
value [code] "f1 True True True \<^bold>[0, 1, 2\<^bold>]"
value [code] "f1 True True False \<^bold>[0, 1\<^bold>]"
@@ -167,11 +164,11 @@
definition f2 :: "nat llist llist list \<Rightarrow> unit" where "f2 _ = ()"
lemma f2_code1 [code]:
- "f2 xs = Code.abort (STR ''a'') (\<lambda>_. ())"
"f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]] = ()"
"f2 [\<^bold>[\<^bold>[Suc n\<^bold>]\<^bold>]] = ()"
"f2 [\<^bold>[\<^bold>[0, Suc n\<^bold>]\<^bold>]] = ()"
- by(simp_all add: f2_def)
+ "f2 xs = Code.abort (STR ''a'') (\<lambda>_. ())"
+ by (simp_all add: f2_def)
value [code] "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]]"
value [code] "f2 [\<^bold>[\<^bold>[4\<^bold>]\<^bold>]]"
@@ -183,7 +180,7 @@
lemma f3_code1 [code]:
"f3 \<^bold>[\<^bold>] = ()"
"f3 \<^bold>[A\<^bold>] = ()"
- by(simp_all add: f3_def)
+ by (simp_all add: f3_def)
value [code] "f3 \<^bold>[\<^bold>]"
value [code] "f3 \<^bold>[{}\<^bold>]"
--- a/src/HOL/HOL.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/HOL.thy Thu Jun 26 17:25:29 2025 +0200
@@ -1943,27 +1943,83 @@
\<close>
+subsubsection \<open>Generic code generator foundation\<close>
+
+text \<open>Datatype \<^typ>\<open>bool\<close>\<close>
+
+code_datatype True False
+
+lemma [code]:
+ "P \<and> True \<longleftrightarrow> P"
+ "P \<and> False \<longleftrightarrow> False"
+ "True \<and> P \<longleftrightarrow> P"
+ "False \<and> P \<longleftrightarrow> False"
+ by simp_all
+
+lemma [code]:
+ "P \<or> True \<longleftrightarrow> True"
+ "P \<or> False \<longleftrightarrow> P"
+ "True \<or> P \<longleftrightarrow> True"
+ "False \<or> P \<longleftrightarrow> P"
+ by simp_all
+
+lemma [code]:
+ "(P \<longrightarrow> True) \<longleftrightarrow> True"
+ "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+ "(True \<longrightarrow> P) \<longleftrightarrow> P"
+ "(False \<longrightarrow> P) \<longleftrightarrow> True"
+ by simp_all
+
+text \<open>More about \<^typ>\<open>prop\<close>\<close>
+
+lemma [code nbe]:
+ "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
+ "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
+ "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
+ by (auto intro!: equal_intr_rule)
+
+lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
+ by (auto intro!: equal_intr_rule holds)
+
+declare Trueprop_code [symmetric, code_post]
+
+text \<open>Cases\<close>
+
+lemma Let_case_cert:
+ assumes "CASE \<equiv> (\<lambda>x. Let x f)"
+ shows "CASE x \<equiv> f x"
+ using assms by simp_all
+
+setup \<open>
+ Code.declare_case_global @{thm Let_case_cert} #>
+ Code.declare_undefined_global \<^const_name>\<open>undefined\<close>
+\<close>
+
+declare [[code abort: undefined]]
+
+
subsubsection \<open>Equality\<close>
+lemma [code nbe]:
+ \<open>x = x \<longleftrightarrow> True\<close>
+ by iprover
+
class equal =
fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
begin
-lemma equal: "equal = (=)"
+lemma eq_equal [code]: "(=) \<equiv> equal"
+ by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
+
+lemma equal [code_post]: "equal = (=)"
by (rule ext equal_eq)+
lemma equal_refl: "equal x x \<longleftrightarrow> True"
unfolding equal by (rule iffI TrueI refl)+
-lemma eq_equal: "(=) \<equiv> equal"
- by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
-
end
-declare eq_equal [symmetric, code_post]
-declare eq_equal [code]
-
simproc_setup passive equal (HOL.eq) =
\<open>fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
@@ -1972,51 +2028,6 @@
setup \<open>Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\<open>equal\<close>)\<close>
-
-subsubsection \<open>Generic code generator foundation\<close>
-
-text \<open>Datatype \<^typ>\<open>bool\<close>\<close>
-
-code_datatype True False
-
-lemma [code]:
- shows "False \<and> P \<longleftrightarrow> False"
- and "True \<and> P \<longleftrightarrow> P"
- and "P \<and> False \<longleftrightarrow> False"
- and "P \<and> True \<longleftrightarrow> P"
- by simp_all
-
-lemma [code]:
- shows "False \<or> P \<longleftrightarrow> P"
- and "True \<or> P \<longleftrightarrow> True"
- and "P \<or> False \<longleftrightarrow> P"
- and "P \<or> True \<longleftrightarrow> True"
- by simp_all
-
-lemma [code]:
- shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
- and "(True \<longrightarrow> P) \<longleftrightarrow> P"
- and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
- and "(P \<longrightarrow> True) \<longleftrightarrow> True"
- by simp_all
-
-text \<open>More about \<^typ>\<open>prop\<close>\<close>
-
-lemma [code nbe]:
- shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
- and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
- and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
- by (auto intro!: equal_intr_rule)
-
-lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
- by (auto intro!: equal_intr_rule holds)
-
-declare Trueprop_code [symmetric, code_post]
-
-text \<open>Equality\<close>
-
-declare simp_thms(6) [code nbe]
-
instantiation itself :: (type) equal
begin
@@ -2050,20 +2061,6 @@
setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close>
-text \<open>Cases\<close>
-
-lemma Let_case_cert:
- assumes "CASE \<equiv> (\<lambda>x. Let x f)"
- shows "CASE x \<equiv> f x"
- using assms by simp_all
-
-setup \<open>
- Code.declare_case_global @{thm Let_case_cert} #>
- Code.declare_undefined_global \<^const_name>\<open>undefined\<close>
-\<close>
-
-declare [[code abort: undefined]]
-
subsubsection \<open>Generic code generator target languages\<close>
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jun 26 17:25:29 2025 +0200
@@ -39,7 +39,7 @@
partial_function (heap) traverse :: "'a::heap node \<Rightarrow> 'a list Heap"
where
- [code del]: "traverse l =
+ "traverse l =
(case l of Empty \<Rightarrow> return []
| Node x r \<Rightarrow> do { tl \<leftarrow> Ref.lookup r;
xs \<leftarrow> traverse tl;
--- a/src/HOL/Library/Code_Binary_Nat.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy Thu Jun 26 17:25:29 2025 +0200
@@ -44,9 +44,9 @@
begin
lemma plus_nat_code [code]:
- "nat_of_num k + nat_of_num l = nat_of_num (k + l)"
+ "0 + n = (n::nat)"
"m + 0 = (m::nat)"
- "0 + n = (n::nat)"
+ "nat_of_num k + nat_of_num l = nat_of_num (k + l)"
by (simp_all add: nat_of_num_numeral)
text \<open>Bounded subtraction needs some auxiliary\<close>
@@ -78,15 +78,15 @@
sub_non_positive nat_add_distrib sub_non_negative)
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)"
+ "0 - n = (0::nat)"
"m - 0 = (m::nat)"
- "0 - n = (0::nat)"
+ "nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
lemma times_nat_code [code]:
- "nat_of_num k * nat_of_num l = nat_of_num (k * l)"
+ "0 * n = (0::nat)"
"m * 0 = (0::nat)"
- "0 * n = (0::nat)"
+ "nat_of_num k * nat_of_num l = nat_of_num (k * l)"
by (simp_all add: nat_of_num_numeral)
lemma equal_nat_code [code]:
@@ -113,9 +113,9 @@
by (simp_all add: nat_of_num_numeral)
lemma divmod_nat_code [code]:
- "Euclidean_Rings.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
+ "Euclidean_Rings.divmod_nat 0 n = (0, 0)"
"Euclidean_Rings.divmod_nat m 0 = (0, m)"
- "Euclidean_Rings.divmod_nat 0 n = (0, 0)"
+ "Euclidean_Rings.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
by (simp_all add: Euclidean_Rings.divmod_nat_def nat_of_num_numeral)
end
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Jun 26 17:25:29 2025 +0200
@@ -61,12 +61,6 @@
end
-lemma [code]: \<open>Ratreal r = (case quotient_of r of (p, q) \<Rightarrow> real_of_int p / real_of_int q)\<close>
- by (cases r) (simp add: quotient_of_Fract of_rat_rat)
-
-lemma [code]: \<open>inverse r = 1 / r\<close> for r :: real
- by (fact inverse_eq_divide)
-
declare [[code drop: \<open>HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool\<close>
\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
@@ -75,6 +69,7 @@
\<open>uminus :: real \<Rightarrow> real\<close>
\<open>minus :: real \<Rightarrow> real \<Rightarrow> real\<close>
\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close>
+ \<open>inverse :: real \<Rightarrow> real\<close>
sqrt
\<open>ln :: real \<Rightarrow> real\<close>
pi
@@ -82,6 +77,12 @@
arccos
arctan]]
+lemma [code]: \<open>Ratreal r = (case quotient_of r of (p, q) \<Rightarrow> real_of_int p / real_of_int q)\<close>
+ by (cases r) (simp add: quotient_of_Fract of_rat_rat)
+
+lemma [code]: \<open>inverse r = 1 / r\<close> for r :: real
+ by (fact inverse_eq_divide)
+
code_reserved (SML) Real
code_printing
--- a/src/HOL/Library/Comparator.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/Comparator.thy Thu Jun 26 17:25:29 2025 +0200
@@ -213,14 +213,14 @@
end
+lemma [code nbe]:
+ \<open>HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True\<close>
+ by (fact equal_refl)
+
lemma [code]:
\<open>HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)\<close>
by transfer (simp add: enum_UNIV)
-lemma [code nbe]:
- \<open>HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True\<close>
- by (fact equal_refl)
-
instantiation comparator :: ("{linorder, typerep}") full_exhaustive
begin
--- a/src/HOL/Library/DAList_Multiset.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Thu Jun 26 17:25:29 2025 +0200
@@ -8,16 +8,6 @@
imports Multiset DAList
begin
-text \<open>Delete prexisting code equations\<close>
-
-declare [[code drop: "{#}" Multiset.is_empty add_mset
- "plus :: 'a multiset \<Rightarrow> _" "minus :: 'a multiset \<Rightarrow> _"
- inter_mset union_mset image_mset filter_mset count
- "size :: _ multiset \<Rightarrow> nat" sum_mset prod_mset
- set_mset sorted_list_of_multiset subset_mset subseteq_mset
- equal_multiset_inst.equal_multiset]]
-
-
text \<open>Raw operations on lists\<close>
definition join_raw ::
--- a/src/HOL/Library/Float.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/Float.thy Thu Jun 26 17:25:29 2025 +0200
@@ -1774,7 +1774,7 @@
by transfer (simp add: plus_down_def ac_simps Let_def)
qed
-lemma compute_float_plus_down_naive[code]: "float_plus_down p x y = float_round_down p (x + y)"
+lemma compute_float_plus_down_naive: "float_plus_down p x y = float_round_down p (x + y)"
by transfer (auto simp: plus_down_def)
qualified lemma compute_float_plus_down[code]:
--- a/src/HOL/Library/Lexord.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/Lexord.thy Thu Jun 26 17:25:29 2025 +0200
@@ -173,8 +173,6 @@
instance list :: (order) order
by (rule order.intro_of_class, rule ordering_orderI, fact lex.ordering)
-export_code \<open>(\<le>) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> \<open>(<) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> in Haskell
-
subsection \<open>Non-canonical instance\<close>
@@ -194,10 +192,4 @@
global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict
by (fact dvd.preordering)
-definition \<open>example = lex_dvd [(4::int), - 7, 8] [- 8, 13, 5]\<close>
-
-export_code example in Haskell
-
-value example
-
end
--- a/src/HOL/Library/RBT_Impl.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Thu Jun 26 17:25:29 2025 +0200
@@ -45,7 +45,7 @@
definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where
"keys t = map fst (entries t)"
-lemma keys_simps [simp, code]:
+lemma keys_simps [simp]:
"keys Empty = []"
"keys (Branch c l k v r) = keys l @ k # keys r"
by (simp_all add: keys_def)
--- a/src/HOL/Library/RBT_Set.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/RBT_Set.thy Thu Jun 26 17:25:29 2025 +0200
@@ -460,6 +460,14 @@
"Set.remove x (Coset t) = Coset (RBT.insert x () t)"
by (auto simp: Set_def)
+lemma inter_Set [code]:
+ "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
+by (simp flip: Set_filter_rbt_filter add: inter_Set_filter)
+
+lemma union_Set_Set [code]:
+ "Set t1 \<union> Set t2 = Set (RBT.union t1 t2)"
+by (auto simp add: lookup_union map_add_Some_iff Set_def)
+
lemma union_Set [code]:
"Set t \<union> A = fold_keys Set.insert t A"
proof -
@@ -469,10 +477,6 @@
show ?thesis by (auto simp add: union_fold_insert)
qed
-lemma inter_Set [code]:
- "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
- by (auto simp flip: Set_filter_rbt_filter)
-
lemma minus_Set [code]:
"A - Set t = fold_keys Set.remove t A"
proof -
@@ -482,24 +486,20 @@
show ?thesis by (auto simp add: minus_fold_remove)
qed
+lemma inter_Coset_Coset [code]:
+ "Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)"
+by (auto simp add: lookup_union map_add_Some_iff Set_def)
+
+lemma inter_Coset [code]:
+ "A \<inter> Coset t = fold_keys Set.remove t A"
+by (simp add: Diff_eq [symmetric] minus_Set)
+
lemma union_Coset [code]:
"Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
proof -
have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
qed
-
-lemma union_Set_Set [code]:
- "Set t1 \<union> Set t2 = Set (RBT.union t1 t2)"
-by (auto simp add: lookup_union map_add_Some_iff Set_def)
-
-lemma inter_Coset [code]:
- "A \<inter> Coset t = fold_keys Set.remove t A"
-by (simp add: Diff_eq [symmetric] minus_Set)
-
-lemma inter_Coset_Coset [code]:
- "Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)"
-by (auto simp add: lookup_union map_add_Some_iff Set_def)
lemma minus_Coset [code]:
"A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
--- a/src/HOL/List.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/List.thy Thu Jun 26 17:25:29 2025 +0200
@@ -4587,10 +4587,10 @@
xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)"
by(auto simp: extract_def dropWhile_eq_Cons_conv dest: set_takeWhileD split: list.splits)
-lemma extract_Nil_code[code]: "List.extract P [] = None"
+lemma extract_Nil_code [code]: "List.extract P [] = None"
by(simp add: extract_def)
-lemma extract_Cons_code[code]:
+lemma extract_Cons_code [code]:
"List.extract P (x # xs) = (if P x then Some ([], x, xs) else
(case List.extract P xs of
None \<Rightarrow> None |
@@ -7508,8 +7508,8 @@
end
lemma lexordp_simps [simp, code]:
- "lexordp [] ys = (ys \<noteq> [])"
- "lexordp xs [] = False"
+ "lexordp [] ys \<longleftrightarrow> ys \<noteq> []"
+ "lexordp xs [] \<longleftrightarrow> False"
"lexordp (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp xs ys"
by(subst lexordp.simps, fastforce simp add: neq_Nil_conv)+
@@ -7519,9 +7519,8 @@
| Cons_eq: "\<lbrakk> \<not> x < y; \<not> y < x; lexordp_eq xs ys \<rbrakk> \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
lemma lexordp_eq_simps [simp, code]:
- "lexordp_eq [] ys = True"
+ "lexordp_eq [] ys \<longleftrightarrow> True"
"lexordp_eq xs [] \<longleftrightarrow> xs = []"
- "lexordp_eq (x # xs) [] = False"
"lexordp_eq (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp_eq xs ys"
by(subst lexordp_eq.simps, fastforce)+
--- a/src/HOL/Matrix_LP/SparseMatrix.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy Thu Jun 26 17:25:29 2025 +0200
@@ -23,7 +23,9 @@
lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
by (simp add: sparse_row_matrix_def)
-lemmas [code] = sparse_row_vector_empty [symmetric]
+lemma [code]:
+ \<open>0 = sparse_row_vector []\<close>
+ by simp
lemma foldl_distrstart: "\<forall>a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> (foldl f (g x y) l = g x (foldl f y l))"
by (induct l arbitrary: x y, auto)
@@ -373,8 +375,10 @@
lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat A B) = (sparse_row_matrix A) + (sparse_row_matrix B)"
by (induct A B rule: add_spmat.induct) (auto simp: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
-lemmas [code] = sparse_row_add_spmat [symmetric]
-lemmas [code] = sparse_row_vector_add [symmetric]
+lemma [code]:
+ \<open>sparse_row_matrix A + sparse_row_matrix B = sparse_row_matrix (add_spmat A B)\<close>
+ \<open>sparse_row_vector a + sparse_row_vector b = sparse_row_vector (add_spvec a b)\<close>
+ by (simp_all add: sparse_row_add_spmat sparse_row_vector_add)
lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr) brr = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
proof -
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Jun 26 17:25:29 2025 +0200
@@ -465,11 +465,11 @@
Listn.sl_def upto_esl_def JType.esl_def Err.esl_def)
by simp
-lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
-lemmas [code] = lesub_def plussub_def
-
lemmas [code] =
JType.sup_def [unfolded exec_lub_def]
+ JVM_le_unfold
+ lesub_def
+ plussub_def
wf_class_code
widen.equation
match_exception_entry_def
--- a/src/HOL/Nat.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Nat.thy Thu Jun 26 17:25:29 2025 +0200
@@ -215,7 +215,7 @@
primrec plus_nat
where
- add_0: "0 + n = (n::nat)"
+ add_0 [code]: "0 + n = (n::nat)"
| add_Suc: "Suc m + n = Suc (m + n)"
lemma add_0_right [simp]: "m + 0 = m"
@@ -225,8 +225,6 @@
lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
by (induct m) simp_all
-declare add_0 [code]
-
lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
by simp
@@ -1501,8 +1499,8 @@
where funpow_code_def [code_abbrev]: "funpow = compow"
lemma [code]:
+ "funpow 0 f = id"
"funpow (Suc n) f = f \<circ> funpow n f"
- "funpow 0 f = id"
by (simp_all add: funpow_code_def)
end
--- a/src/HOL/Number_Theory/Eratosthenes.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Thu Jun 26 17:25:29 2025 +0200
@@ -223,7 +223,7 @@
from 1 have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs) \<Longrightarrow>
bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q"
by auto
- from 2 have "\<not> Suc n dvd q" by (auto elim: dvdE)
+ from 2 have "\<not> Suc n dvd q" by auto
moreover note 3
moreover note \<open>q dvd m\<close>
ultimately show ?thesis by (auto intro: *)
--- a/src/HOL/Option.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Option.thy Thu Jun 26 17:25:29 2025 +0200
@@ -188,8 +188,8 @@
by (simp_all add: is_none_def)
lemma is_none_code [code]:
- "is_none None = True"
- "is_none (Some x) = False"
+ "is_none None \<longleftrightarrow> True"
+ "is_none (Some x) \<longleftrightarrow> False"
by simp_all
lemma rel_option_unfold:
--- a/src/HOL/Predicate.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Predicate.thy Thu Jun 26 17:25:29 2025 +0200
@@ -533,16 +533,16 @@
instance by standard simp
end
-
-lemma [code]:
- "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" for P Q :: "'a pred"
- by auto
lemma [code nbe]:
"HOL.equal P P \<longleftrightarrow> True" for P :: "'a pred"
by (fact equal_refl)
lemma [code]:
+ "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" for P Q :: "'a pred"
+ by auto
+
+lemma [code]:
"case_pred f P = f (eval P)"
by (fact pred.case_eq_if)
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Jun 26 17:25:29 2025 +0200
@@ -86,6 +86,6 @@
lemma issued_nil: "issued [] = {Key0}"
by (auto simp add: initk_def)
-lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
+lemmas issued_simps [code, code_pred_def] = issued_nil issued.simps(2)
end
--- a/src/HOL/Product_Type.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Product_Type.thy Thu Jun 26 17:25:29 2025 +0200
@@ -37,11 +37,15 @@
declare case_split [cases type: bool]
\<comment> \<open>prefer plain propositional version\<close>
-lemma [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
- and [code]: "HOL.equal True P \<longleftrightarrow> P"
- and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
- and [code]: "HOL.equal P True \<longleftrightarrow> P"
- and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
+lemma [code]:
+ "HOL.equal False P \<longleftrightarrow> \<not> P"
+ "HOL.equal True P \<longleftrightarrow> P"
+ "HOL.equal P False \<longleftrightarrow> \<not> P"
+ "HOL.equal P True \<longleftrightarrow> P"
+ by (simp_all add: equal)
+
+lemma [code nbe]:
+ "HOL.equal P P \<longleftrightarrow> True" for P :: bool
by (simp_all add: equal)
lemma If_case_cert:
--- a/src/HOL/Rat.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Rat.thy Thu Jun 26 17:25:29 2025 +0200
@@ -1100,8 +1100,6 @@
instance rat :: partial_term_of ..
lemma [code]:
- "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) \<equiv>
- Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) \<equiv>
Code_Evaluation.App
(Code_Evaluation.Const (STR ''Rat.Frct'')
@@ -1119,6 +1117,8 @@
Typerep.Typerep (STR ''Product_Type.prod'')
[Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]]))
(partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))"
+ "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) \<equiv>
+ Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
by (rule partial_term_of_anything)+
instantiation rat :: narrowing
--- a/src/HOL/Transitive_Closure.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Jun 26 17:25:29 2025 +0200
@@ -951,13 +951,13 @@
where relpowp_code_def [code_abbrev]: "relpowp = compow"
lemma [code]:
- "relpow (Suc n) R = (relpow n R) O R"
"relpow 0 R = Id"
+ "relpow (Suc n) R = relpow n R O R"
by (simp_all add: relpow_code_def)
lemma [code]:
- "relpowp (Suc n) R = (R ^^ n) OO R"
"relpowp 0 R = HOL.eq"
+ "relpowp (Suc n) R = relpowp n R OO R"
by (simp_all add: relpowp_code_def)
hide_const (open) relpow
--- a/src/HOL/Unix/Nested_Environment.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy Thu Jun 26 17:25:29 2025 +0200
@@ -516,46 +516,4 @@
qed
qed
-
-subsection \<open>Code generation\<close>
-
-lemma equal_env_code [code]:
- fixes x y :: "'a::equal"
- and f g :: "'c::{equal, finite} \<Rightarrow> ('b::equal, 'a, 'c) env option"
- shows
- "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
- HOL.equal x y \<and> (\<forall>z \<in> UNIV.
- case f z of
- None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
- and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
- and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
- and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
-proof (unfold equal)
- have "f = g \<longleftrightarrow>
- (\<forall>z. case f z of
- None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
- proof
- assume ?lhs
- then show ?rhs by (auto split: option.splits)
- next
- assume ?rhs (is "\<forall>z. ?prop z")
- show ?lhs
- proof
- fix z
- from \<open>?rhs\<close> have "?prop z" ..
- then show "f z = g z" by (auto split: option.splits)
- qed
- qed
- then show "Env x f = Env y g \<longleftrightarrow>
- x = y \<and> (\<forall>z \<in> UNIV.
- case f z of
- None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
-qed simp_all
-
-lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
- by (fact equal_refl)
-
end
--- a/src/HOL/ex/Code_Lazy_Demo.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Thu Jun 26 17:25:29 2025 +0200
@@ -122,8 +122,6 @@
"mk_tree 0 = \<spadesuit>"
| "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
-declare mk_tree.simps [code]
-
code_thms mk_tree
function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
@@ -140,6 +138,8 @@
digging into one subtree spreads to the whole tree.\<close>
value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
+declare mk_tree.simps(1) [code]
+
lemma mk_tree_Suc_debug [code]: \<comment> \<open>Make the evaluation visible with tracing.\<close>
"mk_tree (Suc n) =
(let _ = Debug.flush (STR ''tick''); t = mk_tree n in t \<triangle> t)"
@@ -149,6 +149,8 @@
\<comment> \<open>The recursive call to \<^const>\<open>mk_tree\<close> is not guarded by a lazy constructor,
so all the suspensions are built up immediately.\<close>
+declare [[code drop: mk_tree]] mk_tree.simps(1) [code]
+
lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
\<comment> \<open>In this code equation, there is no sharing and the recursive calls are guarded by a constructor.\<close>
by(simp add: Let_def)
@@ -156,6 +158,8 @@
value [code] "mk_tree 10"
value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
+declare [[code drop: mk_tree]] mk_tree.simps(1) [code]
+
lemma mk_tree_Suc_debug' [code]:
"mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick'') in mk_tree n \<triangle> mk_tree n)"
by(simp add: Let_def)
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Thu Jun 26 17:25:29 2025 +0200
@@ -26,12 +26,13 @@
| "add2 (S m) n = S(add2 m n)"
declare add2.simps [code]
+lemma [code]: "add2 n Z = n"
+ by(induct n) auto
+lemma [code]: "add2 n (S m) = S (add2 n m)"
+ by(induct n) auto
lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
by (induct n) auto
-lemma [code]: "add2 n (S m) = S (add2 n m)"
- by(induct n) auto
-lemma [code]: "add2 n Z = n"
- by(induct n) auto
+
lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
--- a/src/Pure/Isar/code.ML Thu Jun 26 17:25:29 2025 +0200
+++ b/src/Pure/Isar/code.ML Thu Jun 26 17:25:29 2025 +0200
@@ -62,6 +62,10 @@
val get_case_cong: theory -> string -> thm option
val is_undefined: theory -> string -> bool
val print_codesetup: theory -> unit
+
+ (*transitional*)
+ val only_single_equation: bool Config.T
+ val prepend_allowed: bool Config.T
end;
signature CODE_DATA_ARGS =
@@ -105,6 +109,16 @@
end;
+(* transitional *)
+
+val only_single_equation = Attrib.setup_config_bool \<^binding>\<open>code_only_single_equation\<close> (K false);
+val prepend_allowed = Attrib.setup_config_bool \<^binding>\<open>code_prepend_allowed\<close> (K false);
+
+val _ = Theory.setup (Theory.at_end ((fn thy => if Config.get_global thy prepend_allowed
+ then thy |> Config.put_global prepend_allowed false |> SOME
+ else NONE)));
+
+
(* constants *)
fun const_typ thy = Term.strip_sortsT o Sign.the_const_type thy;
@@ -456,8 +470,12 @@
declarations as "pending" and historize them as proper declarations
at the end of each theory. *)
-fun modify_pending_eqns c f =
- map_pending_eqns (Symtab.map_default (c, []) f);
+fun modify_pending_eqns thy { check_singleton } c f =
+ map_pending_eqns (Symtab.map_default (c, []) (fn eqns =>
+ if null eqns orelse not check_singleton orelse not (Config.get_global thy only_single_equation)
+ then f eqns
+ else error ("Only a single code equation is allowed for " ^ string_of_const thy c)
+ ));
fun register_fun_spec c spec =
map_pending_eqns (Symtab.delete_safe c)
@@ -497,7 +515,7 @@
|> SOME
end;
-val _ = Theory.setup (Theory.at_end historize_pending_fun_specs);
+val _ = Theory.setup (Theory.at_end (historize_pending_fun_specs));
(** foundation **)
@@ -1374,7 +1392,29 @@
local
-fun subsumptive_add thy verbose (thm, proper) eqns =
+fun subsumptive_append thy { verbose } (thm, proper) eqns =
+ let
+ val args_of = drop_prefix is_Var o rev o snd o strip_comb
+ o Term.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of
+ o Thm.transfer thy;
+ val args = args_of thm;
+ val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
+ fun matches_args args' =
+ let
+ val k = length args - length args'
+ in k >= 0 andalso Pattern.matchess thy (map incr_idx args', drop k args) end;
+ fun matches (thm', proper') =
+ (not proper orelse proper') andalso matches_args (args_of thm');
+ in
+ if exists matches eqns then
+ (if verbose then warning ("Code generator: ignoring syntactically subsumed code equation\n" ^
+ Thm.string_of_thm_global thy thm) else ();
+ eqns)
+ else
+ eqns @ [(thm |> Thm.close_derivation \<^here> |> Thm.trim_context, proper)]
+ end;
+
+fun subsumptive_prepend thy { verbose } (thm, proper) eqns =
let
val args_of = drop_prefix is_Var o rev o snd o strip_comb
o Term.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of
@@ -1387,21 +1427,30 @@
in k >= 0 andalso Pattern.matchess thy (args, (map incr_idx o drop k) args') end;
fun drop (thm', proper') = if (proper orelse not proper')
andalso matches_args (args_of thm') then
- (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
- Thm.string_of_thm_global thy thm') else (); true)
+ (if verbose then warning ("Code generator: dropping syntactically subsumed code equation\n" ^
+ Thm.string_of_thm_global thy thm') else (); true)
else false;
in (thm |> Thm.close_derivation \<^here> |> Thm.trim_context, proper) :: filter_out drop eqns end;
-fun add_eqn_for (c, eqn) thy =
- thy |> modify_specs (modify_pending_eqns c (subsumptive_add thy true eqn));
+fun subsumptive_add thy { verbose, prepend } =
+ if prepend then
+ if Config.get_global thy prepend_allowed
+ then subsumptive_prepend thy { verbose = verbose }
+ else error "Not allowed to prepend code equation"
+ else
+ subsumptive_append thy { verbose = verbose };
-fun add_eqns_for default (c, proto_eqns) thy =
+fun add_eqn_for { check_singleton, prepend } (c, eqn) thy =
+ thy |> (modify_specs o modify_pending_eqns thy { check_singleton = check_singleton } c)
+ (subsumptive_add thy { verbose = true, prepend = prepend } eqn);
+
+fun add_eqns_for { default } (c, proto_eqns) thy =
thy |> modify_specs (fn specs =>
if is_default (lookup_fun_spec specs c) orelse not default
then
let
val eqns = []
- |> fold_rev (subsumptive_add thy (not default)) proto_eqns;
+ |> fold (subsumptive_append thy { verbose = not default }) proto_eqns;
in specs |> register_fun_spec c (Eqns (default, eqns)) end
else specs);
@@ -1411,35 +1460,38 @@
in
-fun generic_declare_eqns default strictness raw_eqns thy =
- fold (add_eqns_for default) (prep_eqns strictness thy raw_eqns) thy;
+fun generic_declare_eqns { default } strictness raw_eqns thy =
+ fold (add_eqns_for { default = default }) (prep_eqns strictness thy raw_eqns) thy;
-fun generic_add_eqn strictness raw_eqn thy =
- fold add_eqn_for (the_list (prep_eqn strictness thy raw_eqn)) thy;
+fun generic_add_eqn { strictness, prepend } raw_eqn thy =
+ fold (add_eqn_for { check_singleton = false, prepend = prepend }) (the_list (prep_eqn strictness thy raw_eqn)) thy;
fun generic_declare_abstract_eqn strictness raw_abs_eqn thy =
fold add_abstract_for (the_list (prep_abs_eqn strictness thy raw_abs_eqn)) thy;
fun add_maybe_abs_eqn_liberal thm thy =
case prep_maybe_abs_eqn thy thm
- of SOME (c, (eqn, NONE)) => add_eqn_for (c, eqn) thy
+ of SOME (c, (eqn, NONE)) => add_eqn_for { check_singleton = true, prepend = false } (c, eqn) thy
| SOME (c, ((thm, _), SOME tyco)) => add_abstract_for (c, (thm, tyco)) thy
| NONE => thy;
end;
-val declare_default_eqns_global = generic_declare_eqns true Silent;
-val declare_default_eqns = code_declaration Silent (map o apfst o Morphism.thm) (generic_declare_eqns true);
+val declare_default_eqns_global = generic_declare_eqns { default = true } Silent;
+val declare_default_eqns = code_declaration Silent (map o apfst o Morphism.thm)
+ (generic_declare_eqns { default = true });
-val declare_eqns_global = generic_declare_eqns false Strict;
-val declare_eqns = code_declaration Liberal (map o apfst o Morphism.thm) (generic_declare_eqns false);
+val declare_eqns_global = generic_declare_eqns { default = false } Strict;
+val declare_eqns = code_declaration Liberal (map o apfst o Morphism.thm)
+ (generic_declare_eqns { default = false });
-val add_eqn_global = generic_add_eqn Strict;
+val add_eqn_global = generic_add_eqn { strictness = Strict, prepend = false };
fun del_eqn_global thm thy =
case prep_eqn Liberal thy (thm, false) of
SOME (c, (thm, _)) =>
- modify_specs (modify_pending_eqns c (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')))) thy
+ (modify_specs o modify_pending_eqns thy { check_singleton = false } c)
+ (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm'))) thy
| NONE => thy;
val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict;
@@ -1514,9 +1566,11 @@
(let
val code_attribute_parser =
code_thm_attribute (Args.$$$ "equation")
- (fn thm => generic_add_eqn Liberal (thm, true))
+ (fn thm => generic_add_eqn { strictness = Liberal, prepend = false } (thm, true))
+ || code_thm_attribute (Args.$$$ "prepend")
+ (fn thm => generic_add_eqn { strictness = Liberal, prepend = true } (thm, true))
|| code_thm_attribute (Args.$$$ "nbe")
- (fn thm => generic_add_eqn Liberal (thm, false))
+ (fn thm => generic_add_eqn { strictness = Liberal, prepend = false } (thm, false))
|| code_thm_attribute (Args.$$$ "abstract")
(generic_declare_abstract_eqn Liberal)
|| code_thm_attribute (Args.$$$ "abstype")
--- a/src/Tools/Code_Generator.thy Thu Jun 26 17:25:29 2025 +0200
+++ b/src/Tools/Code_Generator.thy Thu Jun 26 17:25:29 2025 +0200
@@ -39,8 +39,8 @@
code_datatype holds
lemma implies_code [code]:
+ "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
"(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
- "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
proof -
show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
proof