# HG changeset patch # User haftmann # Date 1750951529 -7200 # Node ID 2865a6618cba80d6f6f125be401287c029f672d3 # Parent 4ec8e654112fdce0809d01ea206844f5e93005ab append (rather than prepend) code equations: the order within a theory is maintained in the resulting code diff -r 4ec8e654112f -r 2865a6618cba NEWS --- 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 diff -r 4ec8e654112f -r 2865a6618cba src/Doc/Codegen/Foundations.thy --- 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') \ (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 \ (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 \ diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Basic_BNFs.thy --- 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 \ 'b set" for s :: "'a + 'b" where "s = Inr x \ x \ setr s" -lemma sum_set_defs[code]: +lemma sum_set_defs [code]: "setl = (\x. case x of Inl z \ {z} | _ \ {})" "setr = (\x. case x of Inr z \ {z} | _ \ {})" 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 \ pred_sum P1 P2 (Inl a)" | "P2 b \ pred_sum P1 P2 (Inr b)" -lemma pred_sum_inject[code, simp]: +lemma pred_sum_inject [code, simp]: "pred_sum P1 P2 (Inl a) \ P1 a" "pred_sum P1 P2 (Inr b) \ P2 b" by (simp add: pred_sum.simps)+ diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Code_Numeral.thy --- 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 @@ \Pos (Num.Bit0 m) XOR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m XOR Pos n)\ \Pos (Num.Bit1 m) XOR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m XOR Pos n)\ \Pos (Num.Bit1 m) XOR Pos (Num.Bit1 n) = dup (Pos m XOR Pos n)\ + \Neg Num.One XOR k = NOT k\ + \k XOR Neg Num.One = NOT k\ \Neg m XOR k = NOT (sub m num.One XOR k)\ \k XOR Neg n = NOT (k XOR (sub n num.One))\ - \Neg Num.One XOR k = NOT k\ - \k XOR Neg Num.One = NOT k\ \0 XOR k = k\ \k XOR 0 = k\ for k :: integer @@ -707,14 +707,6 @@ by (fact flip_bit_def) lemma [code]: - \push_bit n k = k * 2 ^ n\ for k :: integer - by (fact push_bit_eq_mult) - -lemma [code]: - \drop_bit n k = k div 2 ^ n\ for k :: integer - by (fact drop_bit_eq_div) - -lemma [code]: \take_bit n k = k AND mask n\ 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) \ True" + by (rule equal_class.equal_refl) + lemma [code]: "HOL.equal m n \ HOL.equal (integer_of_natural m) (integer_of_natural n)" by transfer (simp add: equal) -lemma [code nbe]: "HOL.equal n (n::natural) \ True" - by (rule equal_class.equal_refl) - lemma [code]: "m \ n \ integer_of_natural m \ integer_of_natural n" by transfer simp diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Codegenerator_Test/Code_Lazy_Test.thy --- 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 \ 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'') (\_. ())" + "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" - "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" - "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())" - "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'') (\_. ())" + "f1 b True d \<^bold>[n\<^bold>] = ()" + "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" - "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" - "f1 b True d \<^bold>[n\<^bold>] = ()" - "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" - 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'') (\_. ())" - "f1 b c True \<^bold>[n, m\<^bold>] = ()" + "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())" - "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" - by(simp_all add: f1_def) + "f1 b c True \<^bold>[n, m\<^bold>] = ()" + "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" + 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'') (\_. ())" + "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())" - "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" - by(simp_all add: f1_def) + "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" + "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 \ unit" where "f2 _ = ()" lemma f2_code1 [code]: - "f2 xs = Code.abort (STR ''a'') (\_. ())" "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'') (\_. ())" + 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>]" diff -r 4ec8e654112f -r 2865a6618cba src/HOL/HOL.thy --- 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 @@ \ +subsubsection \Generic code generator foundation\ + +text \Datatype \<^typ>\bool\\ + +code_datatype True False + +lemma [code]: + "P \ True \ P" + "P \ False \ False" + "True \ P \ P" + "False \ P \ False" + by simp_all + +lemma [code]: + "P \ True \ True" + "P \ False \ P" + "True \ P \ True" + "False \ P \ P" + by simp_all + +lemma [code]: + "(P \ True) \ True" + "(P \ False) \ \ P" + "(True \ P) \ P" + "(False \ P) \ True" + by simp_all + +text \More about \<^typ>\prop\\ + +lemma [code nbe]: + "(P \ R) \ Trueprop (P \ R)" + "(PROP Q \ True) \ Trueprop True" + "(True \ PROP Q) \ PROP Q" + by (auto intro!: equal_intr_rule) + +lemma Trueprop_code [code]: "Trueprop True \ Code_Generator.holds" + by (auto intro!: equal_intr_rule holds) + +declare Trueprop_code [symmetric, code_post] + +text \Cases\ + +lemma Let_case_cert: + assumes "CASE \ (\x. Let x f)" + shows "CASE x \ f x" + using assms by simp_all + +setup \ + Code.declare_case_global @{thm Let_case_cert} #> + Code.declare_undefined_global \<^const_name>\undefined\ +\ + +declare [[code abort: undefined]] + + subsubsection \Equality\ +lemma [code nbe]: + \x = x \ True\ + by iprover + class equal = fixes equal :: "'a \ 'a \ bool" assumes equal_eq: "equal x y \ x = y" begin -lemma equal: "equal = (=)" +lemma eq_equal [code]: "(=) \ 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 \ True" unfolding equal by (rule iffI TrueI refl)+ -lemma eq_equal: "(=) \ 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) = \fn _ => fn _ => fn ct => (case Thm.term_of ct of @@ -1972,51 +2028,6 @@ setup \Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\equal\)\ - -subsubsection \Generic code generator foundation\ - -text \Datatype \<^typ>\bool\\ - -code_datatype True False - -lemma [code]: - shows "False \ P \ False" - and "True \ P \ P" - and "P \ False \ False" - and "P \ True \ P" - by simp_all - -lemma [code]: - shows "False \ P \ P" - and "True \ P \ True" - and "P \ False \ P" - and "P \ True \ True" - by simp_all - -lemma [code]: - shows "(False \ P) \ True" - and "(True \ P) \ P" - and "(P \ False) \ \ P" - and "(P \ True) \ True" - by simp_all - -text \More about \<^typ>\prop\\ - -lemma [code nbe]: - shows "(True \ PROP Q) \ PROP Q" - and "(PROP Q \ True) \ Trueprop True" - and "(P \ R) \ Trueprop (P \ R)" - by (auto intro!: equal_intr_rule) - -lemma Trueprop_code [code]: "Trueprop True \ Code_Generator.holds" - by (auto intro!: equal_intr_rule holds) - -declare Trueprop_code [symmetric, code_post] - -text \Equality\ - -declare simp_thms(6) [code nbe] - instantiation itself :: (type) equal begin @@ -2050,20 +2061,6 @@ setup \Nbe.add_const_alias @{thm equal_alias_cert}\ -text \Cases\ - -lemma Let_case_cert: - assumes "CASE \ (\x. Let x f)" - shows "CASE x \ f x" - using assms by simp_all - -setup \ - Code.declare_case_global @{thm Let_case_cert} #> - Code.declare_undefined_global \<^const_name>\undefined\ -\ - -declare [[code abort: undefined]] - subsubsection \Generic code generator target languages\ diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- 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 \ 'a list Heap" where - [code del]: "traverse l = + "traverse l = (case l of Empty \ return [] | Node x r \ do { tl \ Ref.lookup r; xs \ traverse tl; diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/Code_Binary_Nat.thy --- 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 \Bounded subtraction needs some auxiliary\ @@ -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 \ 0 | Some j \ 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 \ 0 | Some j \ 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 diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/Code_Real_Approx_By_Float.thy --- 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]: \Ratreal r = (case quotient_of r of (p, q) \ real_of_int p / real_of_int q)\ - by (cases r) (simp add: quotient_of_Fract of_rat_rat) - -lemma [code]: \inverse r = 1 / r\ for r :: real - by (fact inverse_eq_divide) - declare [[code drop: \HOL.equal :: real \ real \ bool\ \(\) :: real \ real \ bool\ \(<) :: real \ real \ bool\ @@ -75,6 +69,7 @@ \uminus :: real \ real\ \minus :: real \ real \ real\ \divide :: real \ real \ real\ + \inverse :: real \ real\ sqrt \ln :: real \ real\ pi @@ -82,6 +77,12 @@ arccos arctan]] +lemma [code]: \Ratreal r = (case quotient_of r of (p, q) \ real_of_int p / real_of_int q)\ + by (cases r) (simp add: quotient_of_Fract of_rat_rat) + +lemma [code]: \inverse r = 1 / r\ for r :: real + by (fact inverse_eq_divide) + code_reserved (SML) Real code_printing diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/Comparator.thy --- 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]: + \HOL.equal (cmp :: 'a::enum comparator) cmp \ True\ + by (fact equal_refl) + lemma [code]: \HOL.equal cmp1 cmp2 \ Enum.enum_all (\x. compare cmp1 x = compare cmp2 x)\ by transfer (simp add: enum_UNIV) -lemma [code nbe]: - \HOL.equal (cmp :: 'a::enum comparator) cmp \ True\ - by (fact equal_refl) - instantiation comparator :: ("{linorder, typerep}") full_exhaustive begin diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/DAList_Multiset.thy --- 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 \Delete prexisting code equations\ - -declare [[code drop: "{#}" Multiset.is_empty add_mset - "plus :: 'a multiset \ _" "minus :: 'a multiset \ _" - inter_mset union_mset image_mset filter_mset count - "size :: _ multiset \ nat" sum_mset prod_mset - set_mset sorted_list_of_multiset subset_mset subseteq_mset - equal_multiset_inst.equal_multiset]] - - text \Raw operations on lists\ definition join_raw :: diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/Float.thy --- 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]: diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/Lexord.thy --- 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 \(\) :: _ list \ _ list \ bool\ \(<) :: _ list \ _ list \ bool\ in Haskell - subsection \Non-canonical instance\ @@ -194,10 +192,4 @@ global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict by (fact dvd.preordering) -definition \example = lex_dvd [(4::int), - 7, 8] [- 8, 13, 5]\ - -export_code example in Haskell - -value example - end diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/RBT_Impl.thy --- 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 \ '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) diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/RBT_Set.thy --- 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 \ Set t = rbt_filter (\k. k \ A) t" +by (simp flip: Set_filter_rbt_filter add: inter_Set_filter) + +lemma union_Set_Set [code]: + "Set t1 \ 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 \ 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 \ Set t = rbt_filter (\k. k \ 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 \ Coset t2 = Coset (RBT.union t1 t2)" +by (auto simp add: lookup_union map_add_Some_iff Set_def) + +lemma inter_Coset [code]: + "A \ Coset t = fold_keys Set.remove t A" +by (simp add: Diff_eq [symmetric] minus_Set) + lemma union_Coset [code]: "Coset t \ A = - rbt_filter (\k. k \ A) t" proof - have *: "\A B. (-A \ B) = -(-B \ A)" by blast show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set) qed - -lemma union_Set_Set [code]: - "Set t1 \ Set t2 = Set (RBT.union t1 t2)" -by (auto simp add: lookup_union map_add_Some_iff Set_def) - -lemma inter_Coset [code]: - "A \ Coset t = fold_keys Set.remove t A" -by (simp add: Diff_eq [symmetric] minus_Set) - -lemma inter_Coset_Coset [code]: - "Coset t1 \ 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 (\k. k \ A) t" diff -r 4ec8e654112f -r 2865a6618cba src/HOL/List.thy --- 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 \ P y \ \ (\ y \ 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 \ None | @@ -7508,8 +7508,8 @@ end lemma lexordp_simps [simp, code]: - "lexordp [] ys = (ys \ [])" - "lexordp xs [] = False" + "lexordp [] ys \ ys \ []" + "lexordp xs [] \ False" "lexordp (x # xs) (y # ys) \ x < y \ \ y < x \ lexordp xs ys" by(subst lexordp.simps, fastforce simp add: neq_Nil_conv)+ @@ -7519,9 +7519,8 @@ | Cons_eq: "\ \ x < y; \ y < x; lexordp_eq xs ys \ \ lexordp_eq (x # xs) (y # ys)" lemma lexordp_eq_simps [simp, code]: - "lexordp_eq [] ys = True" + "lexordp_eq [] ys \ True" "lexordp_eq xs [] \ xs = []" - "lexordp_eq (x # xs) [] = False" "lexordp_eq (x # xs) (y # ys) \ x < y \ \ y < x \ lexordp_eq xs ys" by(subst lexordp_eq.simps, fastforce)+ diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Matrix_LP/SparseMatrix.thy --- 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]: + \0 = sparse_row_vector []\ + by simp lemma foldl_distrstart: "\a x y. (f (g x y) a = g x (f y a)) \ (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]: + \sparse_row_matrix A + sparse_row_matrix B = sparse_row_matrix (add_spmat A B)\ + \sparse_row_vector a + sparse_row_vector b = sparse_row_vector (add_spvec a b)\ + 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 \ (ab = a | (brr \ [] & ab = fst (hd brr)))" proof - diff -r 4ec8e654112f -r 2865a6618cba src/HOL/MicroJava/BV/BVExample.thy --- 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 diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Nat.thy --- 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 \ funpow n f" - "funpow 0 f = id" by (simp_all add: funpow_code_def) end diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Number_Theory/Eratosthenes.thy --- 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 *: "\q. Suc n < q \ q \ Suc (n + length bs) \ bs ! (q - Suc (Suc n)) \ \ Suc n dvd q \ q dvd m \ m dvd q" by auto - from 2 have "\ Suc n dvd q" by (auto elim: dvdE) + from 2 have "\ Suc n dvd q" by auto moreover note 3 moreover note \q dvd m\ ultimately show ?thesis by (auto intro: *) diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Option.thy --- 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 \ True" + "is_none (Some x) \ False" by simp_all lemma rel_option_unfold: diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Predicate.thy --- 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 \ P \ Q \ Q \ P" for P Q :: "'a pred" - by auto lemma [code nbe]: "HOL.equal P P \ True" for P :: "'a pred" by (fact equal_refl) lemma [code]: + "HOL.equal P Q \ P \ Q \ Q \ P" for P Q :: "'a pred" + by auto + +lemma [code]: "case_pred f P = f (eval P)" by (fact pred.case_eq_if) diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- 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 diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Product_Type.thy --- 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] \ \prefer plain propositional version\ -lemma [code]: "HOL.equal False P \ \ P" - and [code]: "HOL.equal True P \ P" - and [code]: "HOL.equal P False \ \ P" - and [code]: "HOL.equal P True \ P" - and [code nbe]: "HOL.equal P P \ True" +lemma [code]: + "HOL.equal False P \ \ P" + "HOL.equal True P \ P" + "HOL.equal P False \ \ P" + "HOL.equal P True \ P" + by (simp_all add: equal) + +lemma [code nbe]: + "HOL.equal P P \ True" for P :: bool by (simp_all add: equal) lemma If_case_cert: diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Rat.thy --- 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) \ - Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) \ 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) \ + Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" by (rule partial_term_of_anything)+ instantiation rat :: narrowing diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Transitive_Closure.thy --- 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 diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Unix/Nested_Environment.thy --- 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 \Code generation\ - -lemma equal_env_code [code]: - fixes x y :: "'a::equal" - and f g :: "'c::{equal, finite} \ ('b::equal, 'a, 'c) env option" - shows - "HOL.equal (Env x f) (Env y g) \ - HOL.equal x y \ (\z \ UNIV. - case f z of - None \ (case g z of None \ True | Some _ \ False) - | Some a \ (case g z of None \ False | Some b \ HOL.equal a b))" (is ?env) - and "HOL.equal (Val a) (Val b) \ HOL.equal a b" - and "HOL.equal (Val a) (Env y g) \ False" - and "HOL.equal (Env x f) (Val b) \ False" -proof (unfold equal) - have "f = g \ - (\z. case f z of - None \ (case g z of None \ True | Some _ \ False) - | Some a \ (case g z of None \ False | Some b \ a = b))" (is "?lhs = ?rhs") - proof - assume ?lhs - then show ?rhs by (auto split: option.splits) - next - assume ?rhs (is "\z. ?prop z") - show ?lhs - proof - fix z - from \?rhs\ have "?prop z" .. - then show "f z = g z" by (auto split: option.splits) - qed - qed - then show "Env x f = Env y g \ - x = y \ (\z \ UNIV. - case f z of - None \ (case g z of None \ True | Some _ \ False) - | Some a \ (case g z of None \ False | Some b \ a = b))" by simp -qed simp_all - -lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \ True" - by (fact equal_refl) - end diff -r 4ec8e654112f -r 2865a6618cba src/HOL/ex/Code_Lazy_Demo.thy --- 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 = \" | "mk_tree (Suc n) = (let t = mk_tree n in t \ t)" -declare mk_tree.simps [code] - code_thms mk_tree function subtree :: "bool list \ tree \ tree" where @@ -140,6 +138,8 @@ digging into one subtree spreads to the whole tree.\ 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]: \ \Make the evaluation visible with tracing.\ "mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick''); t = mk_tree n in t \ t)" @@ -149,6 +149,8 @@ \ \The recursive call to \<^const>\mk_tree\ is not guarded by a lazy constructor, so all the suspensions are built up immediately.\ +declare [[code drop: mk_tree]] mk_tree.simps(1) [code] + lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n \ mk_tree n" \ \In this code equation, there is no sharing and the recursive calls are guarded by a constructor.\ 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 \ mk_tree n)" by(simp add: Let_def) diff -r 4ec8e654112f -r 2865a6618cba src/HOL/ex/Normalization_by_Evaluation.thy --- 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 diff -r 4ec8e654112f -r 2865a6618cba src/Pure/Isar/code.ML --- 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>\code_only_single_equation\ (K false); +val prepend_allowed = Attrib.setup_config_bool \<^binding>\code_prepend_allowed\ (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") diff -r 4ec8e654112f -r 2865a6618cba src/Tools/Code_Generator.thy --- 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 \ PROP holds) \ PROP holds" "(PROP holds \ PROP P) \ PROP P" - "(PROP P \ PROP holds) \ PROP holds" proof - show "(PROP holds \ PROP P) \ PROP P" proof