# 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 \ - (\