# HG changeset patch # User wenzelm # Date 1743798030 -7200 # Node ID 8f6dc8483b1a78e679549dbe798b1faa419887b5 # Parent 13a185b64ffff8bd49fe8e811244008ae7f978b9# Parent 8b5dd705dfef4981380edfde154a79f0916b7e4e merged diff -r 8b5dd705dfef -r 8f6dc8483b1a NEWS --- a/NEWS Fri Apr 04 22:20:23 2025 +0200 +++ b/NEWS Fri Apr 04 22:20:30 2025 +0200 @@ -44,8 +44,15 @@ - Added lemmas. antimonotone_on_inf_fun antimonotone_on_sup_fun + mono_on_invE + mono_on_strict_invE monotone_on_inf_fun monotone_on_sup_fun + strict_mono_on_eq + strict_mono_on_less + strict_mono_on_less_eq + - Removed lemmas. Minor INCOMPATIBILITY. + mono_on_greaterD (use mono_invE instead) * Theory "HOL.Relation": - Changed definition of predicate refl_on to not constrain the domain diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Apr 04 22:20:30 2025 +0200 @@ -2291,26 +2291,29 @@ ; symbol_module: @'code_module' name ; - syntax: @{syntax string} | (@'infix' | @'infixl' | @'infixr') - @{syntax nat} @{syntax string} + target_syntax: @{syntax embedded} + ; + rich_syntax: target_syntax | (@'infix' | @'infixl' | @'infixr') + @{syntax nat} target_syntax ; printing_const: symbol_const ('\' | '=>') \ - ('(' target ')' syntax ? + @'and') + ('(' target ')' rich_syntax ? + @'and') ; printing_type_constructor: symbol_type_constructor ('\' | '=>') \ - ('(' target ')' syntax ? + @'and') + ('(' target ')' rich_syntax ? + @'and') ; printing_class: symbol_class ('\' | '=>') \ - ('(' target ')' @{syntax string} ? + @'and') + ('(' target ')' target_syntax ? + @'and') ; printing_class_relation: symbol_class_relation ('\' | '=>') \ - ('(' target ')' @{syntax string} ? + @'and') + ('(' target ')' target_syntax ? + @'and') ; printing_class_instance: symbol_class_instance ('\'| '=>') \ ('(' target ')' '-' ? + @'and') ; printing_module: symbol_module ('\' | '=>') \ - ('(' target ')' (@{syntax string} for_symbol?)? + @'and') + ('(' target ')' \ + ((target_syntax | @'file' path) for_symbol?)? + @'and') ; for_symbol: @'for' diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Analysis/FPS_Convergence.thy --- a/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 04 22:20:30 2025 +0200 @@ -10,7 +10,9 @@ theory FPS_Convergence imports Generalised_Binomial_Theorem - "HOL-Computational_Algebra.Formal_Power_Series" + "HOL-Computational_Algebra.Formal_Power_Series" + "HOL-Computational_Algebra.Polynomial_FPS" + begin text \ @@ -593,6 +595,52 @@ that is available. \ +subsection \FPS of a polynomial\ + +lemma fps_conv_radius_fps_of_poly [simp]: + fixes p :: "'a :: {banach, real_normed_div_algebra} poly" + shows "fps_conv_radius (fps_of_poly p) = \" +proof - + have "conv_radius (poly.coeff p) = conv_radius (\_. 0 :: 'a)" + using MOST_coeff_eq_0 unfolding cofinite_eq_sequentially by (rule conv_radius_cong') + also have "\ = \" + by simp + finally show ?thesis + by (simp add: fps_conv_radius_def) +qed + +lemma eval_fps_power: + fixes F :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" + assumes z: "norm z < fps_conv_radius F" + shows "eval_fps (F ^ n) z = eval_fps F z ^ n" +proof (induction n) + case 0 + thus ?case + by (auto simp: eval_fps_mult) +next + case (Suc n) + have "eval_fps (F ^ Suc n) z = eval_fps (F * F ^ n) z" + by simp + also from z have "\ = eval_fps F z * eval_fps (F ^ n) z" + by (subst eval_fps_mult) (auto intro!: less_le_trans[OF _ fps_conv_radius_power]) + finally show ?case + using Suc.IH by simp +qed + +lemma eval_fps_of_poly [simp]: "eval_fps (fps_of_poly p) z = poly p z" +proof - + have "(\n. poly.coeff p n * z ^ n) sums poly p z" + unfolding poly_altdef by (rule sums_finite) (auto simp: coeff_eq_0) + moreover have "(\n. poly.coeff p n * z ^ n) sums eval_fps (fps_of_poly p) z" + using sums_eval_fps[of z "fps_of_poly p"] by simp + ultimately show ?thesis + using sums_unique2 by blast +qed + +lemma poly_holomorphic_on [holomorphic_intros]: + assumes [holomorphic_intros]: "f holomorphic_on A" + shows "(\z. poly p (f z)) holomorphic_on A" + unfolding poly_altdef by (intro holomorphic_intros) subsection \Power series expansions of analytic functions\ diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Analysis/Infinite_Products.thy --- a/src/HOL/Analysis/Infinite_Products.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Analysis/Infinite_Products.thy Fri Apr 04 22:20:30 2025 +0200 @@ -211,6 +211,74 @@ by (metis \a = 0\ \f i = 0\ has_prod_0_iff norm_zero) qed +lemma raw_has_prod_imp_nonzero: + assumes "raw_has_prod f N P" "n \ N" + shows "f n \ 0" +proof + assume "f n = 0" + from assms(1) have lim: "(\m. (\k\m. f (k + N))) \ P" and "P \ 0" + unfolding raw_has_prod_def by blast+ + have "eventually (\m. m \ n - N) at_top" + by (rule eventually_ge_at_top) + hence "eventually (\m. (\k\m. f (k + N)) = 0) at_top" + proof eventually_elim + case (elim m) + have "f ((n - N) + N) = 0" "n - N \ {..m}" "finite {..m}" + using \n \ N\ \f n = 0\ elim by auto + thus "(\k\m. f (k + N)) = 0" + using prod_zero[of "{..m}" "\k. f (k + N)"] by blast + qed + with lim have "P = 0" + by (simp add: LIMSEQ_const_iff tendsto_cong) + thus False + using \P \ 0\ by contradiction +qed + +lemma has_prod_imp_tendsto: + fixes f :: "nat \ 'a :: {semidom, t2_space}" + assumes "f has_prod P" + shows "(\n. \k\n. f k) \ P" +proof (cases "P = 0") + case False + with assms show ?thesis + by (auto simp: has_prod_def raw_has_prod_def) +next + case True + with assms obtain N P' where "f N = 0" "raw_has_prod f (Suc N) P'" + by (auto simp: has_prod_def) + thus ?thesis + using LIMSEQ_prod_0 True \f N = 0\ by blast +qed + +lemma has_prod_imp_tendsto': + fixes f :: "nat \ 'a :: {semidom, t2_space}" + assumes "f has_prod P" + shows "(\n. \k P" + using has_prod_imp_tendsto[OF assms] LIMSEQ_lessThan_iff_atMost by blast + +lemma has_prod_nonneg: + assumes "f has_prod P" "\n. f n \ (0::real)" + shows "P \ 0" +proof (rule tendsto_le) + show "((\n. \i\n. f i)) \ P" + using assms(1) by (rule has_prod_imp_tendsto) + show "(\n. 0::real) \ 0" + by auto +qed (use assms in \auto intro!: always_eventually prod_nonneg\) + +lemma has_prod_pos: + assumes "f has_prod P" "\n. f n > (0::real)" + shows "P > 0" +proof - + have "P \ 0" + by (rule has_prod_nonneg[OF assms(1)]) (auto intro!: less_imp_le assms(2)) + moreover have "f n \ 0" for n + using assms(2)[of n] by auto + hence "P \ 0" + using has_prod_0_iff[of f] assms by auto + ultimately show ?thesis + by linarith +qed subsection\Absolutely convergent products\ @@ -986,6 +1054,11 @@ shows "prodinf f = (\n\N. f n)" using has_prod_finite[OF assms, THEN has_prod_unique] by simp +lemma convergent_prod_tendsto_imp_has_prod: + assumes "convergent_prod f" "(\n. (\i\n. f i)) \ P" + shows "f has_prod P" + using assms by (metis convergent_prod_imp_has_prod has_prod_imp_tendsto limI) + end subsection\<^marker>\tag unimportant\ \Infinite products on ordered topological monoids\ @@ -1520,6 +1593,61 @@ end +lemma prod_ge_prodinf: + fixes f :: "nat \ 'a::{linordered_idom,linorder_topology}" + assumes "f has_prod a" "\i. 0 \ f i" "\i. i \ n \ f i \ 1" + shows "prod f {.. prodinf f" +proof (rule has_prod_le; (intro conjI)?) + show "f has_prod prodinf f" + using assms(1) has_prod_unique by blast + show "(\r. if r \ {.. 0" + by (rule assms) + show "f i \ (if i \ {..n. 0 < f n" and le: "\n. f n \ g n" + shows "F < G" +proof - + define F' G' where "F' = (\nn 0" "g n \ 0" for n + using pos[of n] le[of n] by auto + have [simp]: "F' \ 0" "G' \ 0" + by (auto simp: F'_def G'_def) + have f': "(\n. f (n + Suc m)) has_prod (F / F')" + unfolding F'_def using f + by (intro has_prod_split_initial_segment) auto + have g': "(\n. g (n + Suc m)) has_prod (G / G')" + unfolding G'_def using g + by (intro has_prod_split_initial_segment) auto + have "F' * (F / F') < G' * (F / F')" + proof (rule mult_strict_right_mono) + show "F' < G'" + unfolding F'_def G'_def + by (rule prod_mono_strict[of m]) + (auto intro: le less_imp_le[OF pos] less_le_trans[OF pos le] less) + show "F / F' > 0" + using f' by (rule has_prod_pos) (use pos in auto) + qed + also have "\ \ G' * (G / G')" + proof (rule mult_left_mono) + show "F / F' \ G / G'" + using f' g' by (rule has_prod_le) (auto intro: less_imp_le[OF pos] le) + show "G' \ 0" + unfolding G'_def by (intro prod_nonneg order.trans[OF less_imp_le[OF pos] le]) + qed + finally show ?thesis + by simp +qed + subsection\Exponentials and logarithms\ @@ -1905,4 +2033,364 @@ by (fastforce simp: prod_defs simp flip: of_real_prod) qed +subsection \Convergence criteria: especially uniform convergence of infinite products\ + +text \ + Cauchy's criterion for the convergence of infinite products, adapted to proving + uniform convergence: let $f_k(x)$ be a sequence of functions such that + + \<^enum> $f_k(x)$ has uniformly bounded partial products, i.e.\ there exists a constant \C\ + such that $\prod_{k=0}^m f_k(x) \leq C$ for all $m$ and $x\in A$. + + \<^enum> For any $\varepsilon > 0$ there exists a number $M \in \mathbb{N}$ such that, for any + $m, n \geq M$ and all $x\in A$ we have $|(\prod_{k=m}^n f_k(x)) - 1| < \varepsilon$ + + Then $\prod_{k=0}^n f_k(x)$ converges to $\prod_{k=0}^\infty f_k(x)$ uniformly for all + $x \in A$. +\ +lemma uniformly_convergent_prod_Cauchy: + fixes f :: "nat \ 'a :: topological_space \ 'b :: {real_normed_div_algebra, comm_ring_1, banach}" + assumes C: "\x m. x \ A \ norm (\k C" + assumes "\e. e > 0 \ \M. \x\A. \m\M. \n\m. dist (\k=m..n. f k x) 1 < e" + shows "uniformly_convergent_on A (\N x. \n :: real assume \: "\ > 0" + define C' where "C' = max C 1" + have C': "C' > 0" + by (auto simp: C'_def) + define \ where "\ = Min {2 / 3 * \ / C', 1 / 2}" + from \ have "\ > 0" + using \C' > 0\ by (auto simp: \_def) + obtain M where M: "\x m n. x \ A \ m \ M \ n \ m \ dist (\k=m..n. f k x) 1 < \" + using \\ > 0\ assms by fast + + show "\M. \x\A. \m\M. \n>m. dist (\kk" + proof (rule exI, intro ballI allI impI) + fix x m n + assume x: "x \ A" and mn: "M + 1 \ m" "m < n" + show "dist (\kk" + proof (cases "\kkk by simp + next + case False + have *: "{.. {m..n-1}" + using mn by auto + have "dist (\kkkk=m..n-1. f k x) - 1))" + unfolding * by (subst prod.union_disjoint) + (use mn in \auto simp: dist_norm algebra_simps norm_minus_commute\) + also have "\ = (\kk=m..n-1. f k x) 1" + by (simp add: norm_mult dist_norm prod_norm) + also have "\ < (\k / C')" + proof (rule mult_strict_left_mono) + show "dist (\k = m..n - 1. f k x) 1 < 2 / 3 * \ / C'" + using M[of x m "n-1"] x mn unfolding \_def by fastforce + qed (use False in \auto intro!: prod_pos\) + also have "(\kkk=M.. {M..k=M.. 3 / 2" + proof - + have "dist (\k=M..m-1. f k x) 1 < \" + using M[of x M "m-1"] x mn \\ > 0\ by auto + also have "\ \ 1 / 2" + by (simp add: \_def) + also have "{M..m-1} = {M..k=M.. norm (1 :: 'b) + 1 / 2" + by norm + thus ?thesis + by simp + qed + hence "(\kk = M.. / C') \ + (\k / C')" + using \ C' by (intro mult_left_mono mult_right_mono prod_nonneg) auto + also have "\ \ C' * (3 / 2) * (2 / 3 * \ / C')" + proof (intro mult_right_mono) + have "(\k C" + using C[of x M] x by (simp add: prod_norm) + also have "\ \ C'" + by (simp add: C'_def) + finally show "(\k C'" . + qed (use \ C' in auto) + finally show "dist (\kk" + using \C' > 0\ by (simp add: field_simps) + qed + qed +qed + +text \ + By instantiating the set $A$ in this result with a singleton set, we obtain the ``normal'' + Cauchy criterion for infinite products: +\ +lemma convergent_prod_Cauchy_sufficient: + fixes f :: "nat \ 'b :: {real_normed_div_algebra, comm_ring_1, banach}" + assumes "\e. e > 0 \ \M. \m n. M \ m \ m \ n \ dist (\k=m..n. f k) 1 < e" + shows "convergent_prod f" +proof - + obtain M where M: "\m n. m \ M \ n \ m \ dist (prod f {m..n}) 1 < 1 / 2" + using assms(1)[of "1 / 2"] by auto + have nz: "f m \ 0" if "m \ M" for m + using M[of m m] that by auto + + have M': "dist (prod (\k. f (k + M)) {m..k. f (k + M)) {m..k. k + M" "\k. k - M"]) (use True in auto) + finally show ?thesis . + qed auto + + have "uniformly_convergent_on {0::'b} (\N x. \nk=0..k 3 / 2" + by (simp add: atLeast0LessThan) + next + fix e :: real assume e: "e > 0" + obtain M' where M': "\m n. M' \ m \ m \ n \ dist (\k=m..n. f k) 1 < e" + using assms e by blast + show "\M'. \x\{0}. \m\M'. \n\m. dist (\k=m..n. f (k + M)) 1 < e" + proof (rule exI[of _ M'], intro ballI impI allI) + fix m n :: nat assume "M' \ m" "m \ n" + thus "dist (\k=m..n. f (k + M)) 1 < e" + using M' by (metis add.commute add_left_mono prod.shift_bounds_cl_nat_ivl trans_le_add1) + qed + qed + hence "convergent (\N. \nN. \n L" + unfolding convergent_def by blast + + show ?thesis + unfolding convergent_prod_altdef + proof (rule exI[of _ M], rule exI[of _ L], intro conjI) + show "\n\M. f n \ 0" + using nz by auto + next + show "(\n. \i\n. f (i + M)) \ L" + using LIMSEQ_Suc[OF L] by (subst (asm) lessThan_Suc_atMost) + next + have "norm L \ 1 / 2" + proof (rule tendsto_lowerbound) + show "(\n. norm (\i norm L" + by (intro tendsto_intros L) + show "\\<^sub>F n in sequentially. 1 / 2 \ norm (\ik=0.. norm (1 :: 'b) - 1 / 2" + using M'[of 0 m] by norm + thus "norm (\k 1 / 2" + by (simp add: atLeast0LessThan) + qed + qed auto + thus "L \ 0" + by auto + qed +qed + + +text \ + We now prove that the Cauchy criterion for pointwise convergence is both necessary + and sufficient. +\ +lemma convergent_prod_Cauchy_necessary: + fixes f :: "nat \ 'b :: {real_normed_field, banach}" + assumes "convergent_prod f" "e > 0" + shows "\M. \m n. M \ m \ m \ n \ dist (\k=m..n. f k) 1 < e" +proof - + have *: "\M. \m n. M \ m \ m \ n \ dist (\k=m..n. f k) 1 < e" + if f: "convergent_prod f" "0 \ range f" and e: "e > 0" + for f :: "nat \ 'b" and e :: real + proof - + have *: "(\n. norm (\k norm (\k. f k)" + using has_prod_imp_tendsto' f(1) by (intro tendsto_norm) blast + from f(1,2) have [simp]: "(\k. f k) \ 0" + using prodinf_nonzero by fastforce + obtain M' where M': "norm (\k norm (\k. f k) / 2" if "m \ M'" for m + using order_tendstoD(1)[OF *, of "norm (\k. f k) / 2"] + by (auto simp: eventually_at_top_linorder) + define M where "M = Min (insert (norm (\k. f k) / 2) ((\m. norm (\k 0" + unfolding M_def using f(2) by (subst Min_gr_iff) auto + have norm_ge: "norm (\k M" for m + proof (cases "m \ M'") + case True + have "M \ norm (\k. f k) / 2" + unfolding M_def by (intro Min.coboundedI) auto + also from True have "norm (\k norm (\k. f k) / 2" + by (intro M') + finally show ?thesis by linarith + next + case False + thus ?thesis + unfolding M_def + by (intro Min.coboundedI) auto + qed + + have "convergent (\n. \kn. \k 0" + using e \M > 0\ by auto + ultimately obtain N where N: "dist (\kk N" "n \ N" for m n + unfolding Cauchy_def by fast + + show "\M. \m n. M \ m \ m \ n \ dist (prod f {m..n}) 1 < e" + proof (rule exI[of _ N], intro allI impI, goal_cases) + case (1 m n) + have "dist (\kkkkkkkk\{..{m..n}. f k)" + using 1 by (intro prod.cong) auto + also have "\ = (\k\{..k\{m..n}. f k)" + by (subst prod.union_disjoint) auto + also have "\ - (\kkk\{m..n}. f k) - 1)" + by (simp add: algebra_simps) + finally have "norm (prod f {m..n} - 1) < e * M / norm (prod f {.. \ e * M / M" + using e \M > 0\ f(2) by (intro divide_left_mono norm_ge mult_pos_pos) auto + also have "\ = e" + using \M > 0\ by simp + finally show ?case + by (simp add: dist_norm) + qed + qed + + obtain M where M: "f m \ 0" if "m \ M" for m + using convergent_prod_imp_ev_nonzero[OF assms(1)] + by (auto simp: eventually_at_top_linorder) + + have "\M'. \m n. M' \ m \ m \ n \ dist (\k=m..n. f (k + M)) 1 < e" + by (rule *) (use assms M in auto) + then obtain M' where M': "dist (\k=m..n. f (k + M)) 1 < e" if "M' \ m" "m \ n" for m n + by blast + + show "\M. \m n. M \ m \ m \ n \ dist (prod f {m..n}) 1 < e" + proof (rule exI[of _ "M + M'"], safe, goal_cases) + case (1 m n) + have "dist (\k=m-M..n-M. f (k + M)) 1 < e" + by (rule M') (use 1 in auto) + also have "(\k=m-M..n-M. f (k + M)) = (\k=m..n. f k)" + using 1 by (intro prod.reindex_bij_witness[of _ "\k. k - M" "\k. k + M"]) auto + finally show ?case . + qed +qed + +lemma convergent_prod_Cauchy_iff: + fixes f :: "nat \ 'b :: {real_normed_field, banach}" + shows "convergent_prod f \ (\e>0. \M. \m n. M \ m \ m \ n \ dist (\k=m..n. f k) 1 < e)" + using convergent_prod_Cauchy_necessary[of f] convergent_prod_Cauchy_sufficient[of f] + by blast + +lemma uniformly_convergent_on_prod: + fixes f :: "nat \ 'a :: topological_space \ 'b :: {real_normed_div_algebra, comm_ring_1, banach}" + assumes cont: "\n. continuous_on A (f n)" + assumes A: "compact A" + assumes conv_sum: "uniformly_convergent_on A (\N x. \nN x. \nn x. \kx. \k. norm (f k x)) sequentially" + by (rule uniform_limit_suminf) fact + have cont': "\\<^sub>F n in sequentially. continuous_on A (\x. \kx. \k. norm (f k x))" + by (rule uniform_limit_theorem[OF cont' lim]) auto + hence "compact ((\x. \k. norm (f k x)) ` A)" + by (intro compact_continuous_image A) + hence "bounded ((\x. \k. norm (f k x)) ` A)" + by (rule compact_imp_bounded) + then obtain C where C: "norm (\k. norm (f k x)) \ C" if "x \ A" for x + unfolding bounded_iff by blast + show ?thesis + proof (rule uniformly_convergent_prod_Cauchy) + fix x :: 'a and m :: nat + assume x: "x \ A" + have "norm (\kk \ (\k = (\k \ exp (\kk (\k. norm (f k x))" + proof (rule sum_le_suminf) + have "(\n. \k (\k. norm (f k x))" + by (rule tendsto_uniform_limitI[OF lim]) fact + thus "summable (\k. norm (f k x))" + using sums_def sums_iff by blast + qed auto + also have "exp (\k. norm (f k x)) \ exp (norm (\k. norm (f k x)))" + by simp + also have "norm (\k. norm (f k x)) \ C" + by (rule C) fact + finally show "norm (\k exp C" + by - simp_all + next + fix \ :: real assume \: "\ > 0" + have "uniformly_Cauchy_on A (\N x. \n) > 0" + using \ by simp + ultimately obtain M where M: "\m n x. x \ A \ M \ m \ M \ n \ + dist (\kk)" + using \ unfolding uniformly_Cauchy_on_def by metis + + show "\M. \x\A. \m\M. \n\m. dist (\k = m..n. 1 + f k x) 1 < \" + proof (rule exI, intro ballI allI impI) + fix x m n + assume x: "x \ A" and mn: "M \ m" "m \ n" + have "dist (\kk)" + by (rule M) (use x mn in auto) + also have "dist (\kk\k\{.." + using mn by (subst sum_diff) (auto simp: dist_norm) + also have "{..\k=m..n. norm (f k x)\ = (\k=m..n. norm (f k x))" + by (intro abs_of_nonneg sum_nonneg) auto + finally have *: "(\k=m..n. norm (f k x)) < ln (1 + \)" . + + have "dist (\k=m..n. 1 + f k x) 1 = norm ((\k=m..n. 1 + f k x) - 1)" + by (simp add: dist_norm) + also have "norm ((\k=m..n. 1 + f k x) - 1) \ (\n=m..n. 1 + norm (f n x)) - 1" + by (rule norm_prod_minus1_le_prod_minus1) + also have "(\n=m..n. 1 + norm (f n x)) \ exp (\k=m..n. norm (f k x))" + by (rule prod_le_exp_sum) auto + also note * + finally show "dist (\k = m..n. 1 + f k x) 1 < \" + using \ by - simp_all + qed + qed +qed + +lemma uniformly_convergent_on_prod': + fixes f :: "nat \ 'a :: topological_space \ 'b :: {real_normed_div_algebra, comm_ring_1, banach}" + assumes cont: "\n. continuous_on A (f n)" + assumes A: "compact A" + assumes conv_sum: "uniformly_convergent_on A (\N x. \nN x. \nN x. \nauto intro!: continuous_intros\) + thus ?thesis + by simp +qed + end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Analysis/Infinite_Sum.thy --- a/src/HOL/Analysis/Infinite_Sum.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Analysis/Infinite_Sum.thy Fri Apr 04 22:20:30 2025 +0200 @@ -106,9 +106,18 @@ shows \infsum f A = 0\ by (simp add: assms infsum_def) +lemma has_sum_unique: + fixes f :: "_ \ 'a :: {topological_comm_monoid_add, t2_space}" + assumes "(f has_sum x) A" "(f has_sum y) A" + shows "x = y" + using assms infsumI by blast + lemma summable_iff_has_sum_infsum: "f summable_on A \ (f has_sum (infsum f A)) A" using infsumI summable_on_def by blast +lemma has_sum_iff: "(f has_sum S) A \ f summable_on A \ infsum f A = S" + using infsumI summable_iff_has_sum_infsum by blast + lemma has_sum_infsum[simp]: assumes \f summable_on S\ shows \(f has_sum (infsum f S)) S\ @@ -388,6 +397,41 @@ shows "infsum f F = sum f F" by (simp add: assms infsumI) +lemma has_sum_finiteI: "finite A \ S = sum f A \ (f has_sum S) A" + by simp + +lemma has_sum_strict_mono_neutral: + fixes f :: "'a \ 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}" + assumes \(f has_sum a) A\ and "(g has_sum b) B" + assumes \\x. x \ A\B \ f x \ g x\ + assumes \\x. x \ A-B \ f x \ 0\ + assumes \\x. x \ B-A \ g x \ 0\ + assumes \x \ B\ \if x \ A then f x < g x else 0 < g x\ + shows "a < b" +proof - + define y where "y = (if x \ A then f x else 0)" + have "a - y \ b - g x" + proof (rule has_sum_mono_neutral) + show "(f has_sum (a - y)) (A - (if x \ A then {x} else {}))" + by (intro has_sum_Diff assms has_sum_finiteI) (auto simp: y_def) + show "(g has_sum (b - g x)) (B - {x})" + by (intro has_sum_Diff assms has_sum_finiteI) (use assms in auto) + qed (use assms in \auto split: if_splits\) + moreover have "y < g x" + using assms(3,4,5)[of x] assms(6-) by (auto simp: y_def split: if_splits) + ultimately show ?thesis + by (metis diff_strict_left_mono diff_strict_mono leD neqE) +qed + +lemma has_sum_strict_mono: + fixes f :: "'a \ 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}" + assumes \(f has_sum a) A\ and "(g has_sum b) A" + assumes \\x. x \ A \ f x \ g x\ + assumes \x \ A\ \f x < g x\ + shows "a < b" + by (rule has_sum_strict_mono_neutral[OF assms(1,2), where x = x]) + (use assms(3-) in auto) + lemma has_sum_finite_approximation: fixes f :: "'a \ 'b::{comm_monoid_add,metric_space}" assumes "(f has_sum x) A" and "\ > 0" @@ -708,6 +752,39 @@ using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel) +lemma sums_nonneg_imp_has_sum_strong: + assumes "f sums (S::real)" "eventually (\n. f n \ 0) sequentially" + shows "(f has_sum S) UNIV" +proof - + from assms(2) obtain N where N: "\n. n \ N \ f n \ 0" + by (auto simp: eventually_at_top_linorder) + from assms(1) have "summable f" + by (simp add: sums_iff) + hence "summable (\n. f (n + N))" + by (rule summable_ignore_initial_segment) + hence "summable (\n. norm (f (n + N)))" + using N by simp + hence "summable (\n. norm (f n))" + using summable_iff_shift by blast + with assms(1) show ?thesis + using norm_summable_imp_has_sum by blast +qed + +lemma sums_nonneg_imp_has_sum: + assumes "f sums (S::real)" and "\n. f n \ 0" + shows "(f has_sum S) UNIV" + by (rule sums_nonneg_imp_has_sum_strong) (use assms in auto) + +lemma summable_nonneg_imp_summable_on_strong: + assumes "summable f" "eventually (\n. f n \ (0::real)) sequentially" + shows "f summable_on UNIV" + using assms has_sum_iff sums_nonneg_imp_has_sum_strong by blast + +lemma summable_nonneg_imp_summable_on: + assumes "summable f" "\n. f n \ (0::real)" + shows "f summable_on UNIV" + by (rule summable_nonneg_imp_summable_on_strong) (use assms in auto) + text \The following lemma indeed needs a complete space (as formalized by the premise \<^term>\complete UNIV\). The following two counterexamples show this: \begin{itemize} @@ -2759,6 +2836,15 @@ shows "(g has_sum s) S = (h has_sum s') T" by (smt (verit, del_insts) assms bij_betwI' has_sum_cong has_sum_reindex_bij_betw) +lemma summable_on_reindex_bij_witness: + assumes "\a. a \ S \ i (j a) = a" + assumes "\a. a \ S \ j a \ T" + assumes "\b. b \ T \ j (i b) = b" + assumes "\b. b \ T \ i b \ S" + assumes "\a. a \ S \ h (j a) = g a" + shows "g summable_on S \ h summable_on T" + using has_sum_reindex_bij_witness[of S i j T h g, OF assms] + by (simp add: summable_on_def) lemma has_sum_homomorphism: assumes "(f has_sum S) A" "h 0 = 0" "\a b. h (a + b) = h a + h b" "continuous_on UNIV h" @@ -2835,6 +2921,19 @@ shows "infsum (\x. mult c (f x)) A = mult c (infsum f A)" by (metis assms infsum_0 infsum_bounded_linear_strong) +lemma has_sum_scaleR: + fixes f :: "'a \ 'b :: real_normed_vector" + assumes "(f has_sum S) A" + shows "((\x. c *\<^sub>R f x) has_sum (c *\<^sub>R S)) A" + using has_sum_bounded_linear[OF bounded_linear_scaleR_right[of c], of f A S] assms by simp + +lemma has_sum_scaleR_iff: + fixes f :: "'a \ 'b :: real_normed_vector" + assumes "c \ 0" + shows "((\x. c *\<^sub>R f x) has_sum S) A \ (f has_sum (S /\<^sub>R c)) A" + using has_sum_scaleR[of f A "S /\<^sub>R c" c] has_sum_scaleR[of "\x. c *\<^sub>R f x" A S "inverse c"] assms + by auto + lemma has_sum_of_nat: "(f has_sum S) A \ ((\x. of_nat (f x)) has_sum of_nat S) A" by (erule has_sum_homomorphism) (auto intro!: continuous_intros) @@ -2847,6 +2946,31 @@ lemma summable_on_of_int: "f summable_on A \ (\x. of_int (f x)) summable_on A" by (erule summable_on_homomorphism) (auto intro!: continuous_intros) +lemma summable_on_of_real: + "f summable_on A \ (\x. of_real (f x) :: 'a :: real_normed_algebra_1) summable_on A" + using summable_on_bounded_linear[of "of_real :: real \ 'a", OF bounded_linear_of_real, of f A] + by simp + +lemma has_sum_of_real_iff: + "((\x. of_real (f x) :: 'a :: real_normed_div_algebra) has_sum (of_real c)) A \ + (f has_sum c) A" +proof - + have "((\x. of_real (f x) :: 'a) has_sum (of_real c)) A \ + (sum (\x. of_real (f x) :: 'a) \ of_real c) (finite_subsets_at_top A)" + by (simp add: has_sum_def) + also have "sum (\x. of_real (f x) :: 'a) = (\X. of_real (sum f X))" + by simp + also have "((\X. of_real (sum f X) :: 'a) \ of_real c) (finite_subsets_at_top A) \ + (f has_sum c) A" + unfolding has_sum_def tendsto_of_real_iff .. + finally show ?thesis . +qed + +lemma has_sum_of_real: + "(f has_sum S) A \ ((\x. of_real (f x) :: 'a :: real_normed_algebra_1) has_sum of_real S) A" + using has_sum_bounded_linear[of "of_real :: real \ 'a", OF bounded_linear_of_real, of f A S] + by simp + lemma summable_on_discrete_iff: fixes f :: "'a \ 'b :: {discrete_topology, topological_comm_monoid_add, cancel_comm_monoid_add}" shows "f summable_on A \ finite {x\A. f x \ 0}" @@ -3027,9 +3151,6 @@ shows "f summable_on insert x A \ f summable_on A" using summable_on_union[of f A "{x}"] by (auto intro: summable_on_subset) -lemma has_sum_finiteI: "finite A \ S = sum f A \ (f has_sum S) A" - by simp - lemma has_sum_insert: fixes f :: "'a \ 'b :: topological_comm_monoid_add" assumes "x \ A" and "(f has_sum S) A" @@ -3131,11 +3252,32 @@ qed (insert Y(1,2), auto simp: Y1_def) qed -lemma has_sum_unique: - fixes f :: "_ \ 'a :: {topological_comm_monoid_add, t2_space}" - assumes "(f has_sum x) A" "(f has_sum y) A" - shows "x = y" - using assms unfolding has_sum_def using tendsto_unique finite_subsets_at_top_neq_bot by blast +lemma has_sum_finite_iff: + fixes S :: "'a :: {topological_comm_monoid_add,t2_space}" + assumes "finite A" + shows "(f has_sum S) A \ S = (\x\A. f x)" +proof + assume "S = (\x\A. f x)" + thus "(f has_sum S) A" + by (intro has_sum_finiteI assms) +next + assume "(f has_sum S) A" + moreover have "(f has_sum (\x\A. f x)) A" + by (intro has_sum_finiteI assms) auto + ultimately show "S = (\x\A. f x)" + using has_sum_unique by blast +qed + +lemma has_sum_finite_neutralI: + assumes "finite B" "B \ A" "\x. x \ A - B \ f x = 0" "c = (\x\B. f x)" + shows "(f has_sum c) A" +proof - + have "(f has_sum c) B" + by (rule has_sum_finiteI) (use assms in auto) + also have "?this \ (f has_sum c) A" + by (intro has_sum_cong_neutral) (use assms in auto) + finally show ?thesis . +qed lemma has_sum_SigmaI: fixes f :: "_ \ 'a :: {topological_comm_monoid_add, t3_space}" diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Analysis/Path_Connected.thy Fri Apr 04 22:20:30 2025 +0200 @@ -1266,6 +1266,46 @@ lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0" by (simp add: linepath_def) +lemma + assumes "x \ closed_segment y z" + shows in_closed_segment_imp_Re_in_closed_segment: "Re x \ closed_segment (Re y) (Re z)" (is ?th1) + and in_closed_segment_imp_Im_in_closed_segment: "Im x \ closed_segment (Im y) (Im z)" (is ?th2) +proof - + from assms obtain t where t: "t \ {0..1}" "x = linepath y z t" + by (metis imageE linepath_image_01) + have "Re x = linepath (Re y) (Re z) t" "Im x = linepath (Im y) (Im z) t" + by (simp_all add: t Re_linepath' Im_linepath') + with t(1) show ?th1 ?th2 + using linepath_in_path[of t "Re y" "Re z"] linepath_in_path[of t "Im y" "Im z"] by simp_all +qed + +lemma linepath_in_open_segment: "t \ {0<..<1} \ x \ y \ linepath x y t \ open_segment x y" + unfolding greaterThanLessThan_iff by (metis in_segment(2) linepath_def) + +lemma in_open_segment_imp_Re_in_open_segment: + assumes "x \ open_segment y z" "Re y \ Re z" + shows "Re x \ open_segment (Re y) (Re z)" +proof - + from assms obtain t where t: "t \ {0<..<1}" "x = linepath y z t" + by (metis greaterThanLessThan_iff in_segment(2) linepath_def) + have "Re x = linepath (Re y) (Re z) t" + by (simp_all add: t Re_linepath') + with t(1) show ?thesis + using linepath_in_open_segment[of t "Re y" "Re z"] assms by auto +qed + +lemma in_open_segment_imp_Im_in_open_segment: + assumes "x \ open_segment y z" "Im y \ Im z" + shows "Im x \ open_segment (Im y) (Im z)" +proof - + from assms obtain t where t: "t \ {0<..<1}" "x = linepath y z t" + by (metis greaterThanLessThan_iff in_segment(2) linepath_def) + have "Im x = linepath (Im y) (Im z) t" + by (simp_all add: t Im_linepath') + with t(1) show ?thesis + using linepath_in_open_segment[of t "Im y" "Im z"] assms by auto +qed + lemma bounded_linear_linepath: assumes "bounded_linear f" shows "f (linepath a b x) = linepath (f a) (f b) x" diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Analysis/Uniform_Limit.thy --- a/src/HOL/Analysis/Uniform_Limit.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Analysis/Uniform_Limit.thy Fri Apr 04 22:20:30 2025 +0200 @@ -41,6 +41,22 @@ "(\e. e > 0 \ \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e) \ uniform_limit S f l F" by (simp add: uniform_limit_iff) +lemma uniform_limit_on_subset: + "uniform_limit J f g F \ I \ J \ uniform_limit I f g F" + by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono) + +lemma uniformly_convergent_on_subset: + assumes "uniformly_convergent_on A f" "B \ A" + shows "uniformly_convergent_on B f" + using assms by (meson uniform_limit_on_subset uniformly_convergent_on_def) + +lemma uniform_limit_singleton [simp]: "uniform_limit {x} f g F \ ((\n. f n x) \ g x) F" + by (simp add: uniform_limit_iff tendsto_iff) + +lemma uniformly_convergent_on_singleton: + "uniformly_convergent_on {x} f \ convergent (\n. f n x)" + by (auto simp: uniformly_convergent_on_def convergent_def) + lemma uniform_limit_sequentially_iff: "uniform_limit S f l sequentially \ (\e>0. \N. \n\N. \x \ S. dist (f n x) (l x) < e)" unfolding uniform_limit_iff eventually_sequentially .. @@ -71,6 +87,19 @@ by eventually_elim (use \ l in blast) qed +lemma uniform_limit_compose': + assumes "uniform_limit A f g F" and "h \ B \ A" + shows "uniform_limit B (\n x. f n (h x)) (\x. g (h x)) F" + unfolding uniform_limit_iff +proof (intro strip) + fix e :: real + assume e: "e > 0" + with assms(1) have "\\<^sub>F n in F. \x\A. dist (f n x) (g x) < e" + by (auto simp: uniform_limit_iff) + thus "\\<^sub>F n in F. \x\B. dist (f n (h x)) (g (h x)) < e" + by eventually_elim (use assms(2) in blast) +qed + lemma metric_uniform_limit_imp_uniform_limit: assumes f: "uniform_limit S f a F" assumes le: "eventually (\x. \y\S. dist (g x y) (b y) \ dist (f x y) (a y)) F" @@ -83,15 +112,14 @@ by eventually_elim force qed - subsection \Exchange limits\ - -proposition swap_uniform_limit: - assumes f: "\\<^sub>F n in F. (f n \ g n) (at x within S)" +proposition swap_uniform_limit': + assumes f: "\\<^sub>F n in F. (f n \ g n) G" assumes g: "(g \ l) F" assumes uc: "uniform_limit S f h F" + assumes ev: "\\<^sub>F x in G. x \ S" assumes "\trivial_limit F" - shows "(h \ l) (at x within S)" + shows "(h \ l) G" proof (rule tendstoI) fix e :: real define e' where "e' = e/3" @@ -102,21 +130,19 @@ by (simp add: dist_commute) moreover from f - have "\\<^sub>F n in F. \\<^sub>F x in at x within S. dist (g n) (f n x) < e'" + have "\\<^sub>F n in F. \\<^sub>F x in G. dist (g n) (f n x) < e'" by eventually_elim (auto dest!: tendstoD[OF _ \0 < e'\] simp: dist_commute) moreover from tendstoD[OF g \0 < e'\] have "\\<^sub>F x in F. dist l (g x) < e'" by (simp add: dist_commute) ultimately - have "\\<^sub>F _ in F. \\<^sub>F x in at x within S. dist (h x) l < e" + have "\\<^sub>F _ in F. \\<^sub>F x in G. dist (h x) l < e" proof eventually_elim case (elim n) note fh = elim(1) note gl = elim(3) - have "\\<^sub>F x in at x within S. x \ S" - by (auto simp: eventually_at_filter) - with elim(2) show ?case + using elim(2) ev proof eventually_elim case (elim x) from fh[rule_format, OF \x \ S\] elim(1) @@ -126,10 +152,17 @@ show ?case by (simp add: e'_def) qed qed - thus "\\<^sub>F x in at x within S. dist (h x) l < e" + thus "\\<^sub>F x in G. dist (h x) l < e" using eventually_happens by (metis \\trivial_limit F\) qed +corollary swap_uniform_limit: + assumes "\\<^sub>F n in F. (f n \ g n) (at x within S)" + assumes "(g \ l) F" "uniform_limit S f h F" "\trivial_limit F" + shows "(h \ l) (at x within S)" + using swap_uniform_limit' eventually_at_topological assms + by blast + subsection \Uniform limit theorem\ @@ -378,7 +411,7 @@ qed (metis uniformly_convergent_on_sum_E) lemma uniform_limit_suminf: - fixes f:: "nat \ 'a::{metric_space, comm_monoid_add} \ 'a" + fixes f:: "nat \ 'a :: topological_space \ 'b::{metric_space, comm_monoid_add}" assumes "uniformly_convergent_on X (\n x. \kn x. \kx. \k. f k x) sequentially" proof - @@ -631,6 +664,22 @@ qed qed +lemma Weierstrass_m_test_general': + fixes f :: "'a \ 'b \ 'c :: banach" + fixes M :: "'a \ real" + assumes norm_le: "\x y. x \ X \ y \ Y \ norm (f x y) \ M x" + assumes has_sum: "\y. y \ Y \ ((\x. f x y) has_sum S y) X" + assumes summable: "M summable_on X" + shows "uniform_limit Y (\X y. \x\X. f x y) S (finite_subsets_at_top X)" +proof - + have "uniform_limit Y (\X y. \x\X. f x y) (\y. \\<^sub>\x\X. f x y) (finite_subsets_at_top X)" + using norm_le summable by (rule Weierstrass_m_test_general) + also have "?this \ ?thesis" + by (intro uniform_limit_cong refl always_eventually allI ballI) + (use has_sum in \auto simp: has_sum_iff\) + finally show ?thesis . +qed + subsection\<^marker>\tag unimportant\ \Structural introduction rules\ @@ -897,10 +946,6 @@ shows "uniform_limit (Union I) f g F" by (metis SUP_identity_eq assms uniform_limit_on_UNION) -lemma uniform_limit_on_subset: - "uniform_limit J f g F \ I \ J \ uniform_limit I f g F" - by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono) - lemma uniform_limit_bounded: fixes f::"'i \ 'a::topological_space \ 'b::metric_space" assumes l: "uniform_limit S f l F" @@ -957,27 +1002,98 @@ fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}" assumes "r < conv_radius a" shows "uniform_limit (cball \ r) (\n x. \i) ^ i) (\x. suminf (\i. a i * (x - \) ^ i)) sequentially" -using powser_uniformly_convergent [OF assms] -by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim) + using powser_uniformly_convergent [OF assms] + by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim) lemma powser_continuous_suminf: fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}" assumes "r < conv_radius a" shows "continuous_on (cball \ r) (\x. suminf (\i. a i * (x - \) ^ i))" -apply (rule uniform_limit_theorem [OF _ powser_uniform_limit]) -apply (rule eventuallyI continuous_intros assms)+ -apply (simp add:) -done + apply (rule uniform_limit_theorem [OF _ powser_uniform_limit]) + apply (rule eventuallyI continuous_intros assms)+ + apply auto + done lemma powser_continuous_sums: fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}" assumes r: "r < conv_radius a" - and sm: "\x. x \ cball \ r \ (\n. a n * (x - \) ^ n) sums (f x)" + and sm: "\x. x \ cball \ r \ (\n. a n * (x - \) ^ n) sums (f x)" shows "continuous_on (cball \ r) f" -apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]]) -using sm sums_unique by fastforce + apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]]) + using sm sums_unique by fastforce lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union] +subsection \Tannery's Theorem\ + +text \ + Tannery's Theorem proves that, under certain boundedness conditions: + \[ \lim_{x\to\bar x} \sum_{k=0}^\infty f(k,n) = \sum_{k=0}^\infty \lim_{x\to\bar x} f(k,n) \] +\ +lemma tannerys_theorem: + fixes a :: "nat \ _ \ 'a :: {real_normed_algebra, banach}" + assumes limit: "\k. ((\n. a k n) \ b k) F" + assumes bound: "eventually (\(k,n). norm (a k n) \ M k) (at_top \\<^sub>F F)" + assumes "summable M" + assumes [simp]: "F \ bot" + shows "eventually (\n. summable (\k. norm (a k n))) F \ + summable (\n. norm (b n)) \ + ((\n. suminf (\k. a k n)) \ suminf b) F" +proof (intro conjI allI) + show "eventually (\n. summable (\k. norm (a k n))) F" + proof - + have "eventually (\n. eventually (\k. norm (a k n) \ M k) at_top) F" + using eventually_eventually_prod_filter2[OF bound] by simp + thus ?thesis + proof eventually_elim + case (elim n) + show "summable (\k. norm (a k n))" + proof (rule summable_comparison_test_ev) + show "eventually (\k. norm (norm (a k n)) \ M k) at_top" + using elim by auto + qed fact + qed + qed + + have bound': "eventually (\k. norm (b k) \ M k) at_top" + proof - + have "eventually (\k. eventually (\n. norm (a k n) \ M k) F) at_top" + using eventually_eventually_prod_filter1[OF bound] by simp + thus ?thesis + proof eventually_elim + case (elim k) + show "norm (b k) \ M k" + proof (rule tendsto_upperbound) + show "((\n. norm (a k n)) \ norm (b k)) F" + by (intro tendsto_intros limit) + qed (use elim in auto) + qed + qed + show "summable (\n. norm (b n))" + by (rule summable_comparison_test_ev[OF _ \summable M\]) (use bound' in auto) + + from bound obtain Pf Pg where + *: "eventually Pf at_top" "eventually Pg F" "\k n. Pf k \ Pg n \ norm (a k n) \ M k" + unfolding eventually_prod_filter by auto + + show "((\n. \k. a k n) \ (\k. b k)) F" + proof (rule swap_uniform_limit') + show "(\K. (\k (\k. b k)" + using \summable (\n. norm (b n))\ + by (intro summable_LIMSEQ) (auto dest: summable_norm_cancel) + show "\\<^sub>F K in sequentially. ((\n. \k (\k\<^sub>F x in F. x \ {n. Pg n}" + using *(2) by simp + show "uniform_limit {n. Pg n} (\K n. \kn. \k. a k n) sequentially" + proof (rule Weierstrass_m_test_ev) + show "\\<^sub>F k in at_top. \n\{n. Pg n}. norm (a k n) \ M k" + using *(1) by eventually_elim (use *(3) in auto) + show "summable M" + by fact + qed + qed auto +qed + end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Complex.thy --- a/src/HOL/Complex.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Complex.thy Fri Apr 04 22:20:30 2025 +0200 @@ -878,6 +878,12 @@ lemma cis_divide: "cis a / cis b = cis (a - b)" by (simp add: divide_complex_def cis_mult) +lemma cis_power_int: "cis x powi n = cis (of_int n * x)" + by (auto simp: power_int_def DeMoivre) + +lemma complex_cnj_power_int [simp]: "cnj (x powi n) = cnj x powi n" + by (auto simp: power_int_def) + lemma divide_conv_cnj: "norm z = 1 \ x / z = x * cnj z" by (metis complex_div_cnj div_by_1 mult_1 of_real_1 power2_eq_square) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Fri Apr 04 22:20:30 2025 +0200 @@ -620,7 +620,7 @@ have **: "\f' x' f x::complex. f'*x' - f*x = f' * (x' - x) + x * (f' - f)" by (simp add: algebra_simps) have "norm (pathint (shrink u) (shrink v) - pathint u v) - \ (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))" + \ (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * measure lborel (cbox 0 (1::real))" apply (rule has_integral_bound [of _ "\x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)" _ 0 1]) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Complex_Analysis/Contour_Integration.thy --- a/src/HOL/Complex_Analysis/Contour_Integration.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Fri Apr 04 22:20:30 2025 +0200 @@ -808,7 +808,7 @@ "0 \ B" and B: "\x. x \ closed_segment a b \ norm(f x) \ B" shows "norm i \ B * norm(b - a)" proof - - have "norm i \ (B * norm (b - a)) * content (cbox 0 (1::real))" + have "norm i \ (B * norm (b - a)) * measure lborel (cbox 0 (1::real))" proof (rule has_integral_bound [of _ "\x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"]) show "cmod (f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Complex_Analysis/Great_Picard.thy --- a/src/HOL/Complex_Analysis/Great_Picard.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Complex_Analysis/Great_Picard.thy Fri Apr 04 22:20:30 2025 +0200 @@ -1178,8 +1178,7 @@ have "(\z. g z - g z1) holomorphic_on S" by (intro holomorphic_intros holg) then obtain r where "0 < r" "ball z2 r \ S" "\z. dist z2 z < r \ z \ z2 \ g z \ g z1" - apply (rule isolated_zeros [of "\z. g z - g z1" S z2 z0]) - using S \z0 \ S\ z0 z12 by auto + using isolated_zeros [of "\z. g z - g z1" S z2 z0] S \z0 \ S\ z0 z12 by auto have "g z2 - g z1 \ 0" proof (rule Hurwitz_no_zeros [of "S - {z1}" "\n z. \ n z - \ n z1" "\z. g z - g z1"]) show "open (S - {z1})" @@ -1200,13 +1199,13 @@ then have K: "\\<^sub>F n in sequentially. \x \ K. dist (\ n x) (g x) < e/2" using \0 < e\ by (force simp: intro!: uniform_limitD) have "uniform_limit {z1} \ g sequentially" - by (simp add: ul_g z12) + by (intro ul_g) (auto simp: z12) then have "\\<^sub>F n in sequentially. \x \ {z1}. dist (\ n x) (g x) < e/2" using \0 < e\ by (force simp: intro!: uniform_limitD) then have z1: "\\<^sub>F n in sequentially. dist (\ n z1) (g z1) < e/2" by simp show "\\<^sub>F n in sequentially. \x\K. dist (\ n x - \ n z1) (g x - g z1) < e" - apply (rule eventually_mono [OF eventually_conj [OF K z1]]) + apply (intro eventually_mono [OF eventually_conj [OF K z1]]) by (metis (no_types, opaque_lifting) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half) qed show "\ (\z. g z - g z1) constant_on S - {z1}" diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Computational_Algebra/Formal_Laurent_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Fri Apr 04 22:20:30 2025 +0200 @@ -912,6 +912,9 @@ instance fls :: (comm_monoid_add) comm_monoid_add by (standard, transfer, auto simp: add.commute) +lemma fls_nth_sum: "fls_nth (\x\A. f x) n = (\x\A. fls_nth (f x) n)" + by (induction A rule: infinite_finite_induct) auto + subsubsection \Subtraction and negatives\ @@ -2923,6 +2926,20 @@ by simp_all qed +lemma one_plus_fls_X_powi_eq: + "(1 + fls_X) powi n = fps_to_fls (fps_binomial (of_int n :: 'a :: field_char_0))" +proof (cases "n \ 0") + case True + thus ?thesis + using fps_binomial_of_nat[of "nat n", where ?'a = 'a] + by (simp add: power_int_def fps_to_fls_power) +next + case False + thus ?thesis + using fps_binomial_minus_of_nat[of "nat (-n)", where ?'a = 'a] + by (simp add: power_int_def fps_to_fls_power fps_inverse_power flip: fls_inverse_fps_to_fls) +qed + instance fls :: (field) field by (standard, simp_all add: field_simps) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Deriv.thy Fri Apr 04 22:20:30 2025 +0200 @@ -1130,18 +1130,19 @@ using DERIV_power [OF DERIV_ident] by simp lemma DERIV_power_int [derivative_intros]: - assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)" and [simp]: "f x \ 0" + assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)" + and "n \ 0 \ f x \ 0" shows "((\x. power_int (f x) n) has_field_derivative (of_int n * power_int (f x) (n - 1) * d)) (at x within s)" proof (cases n rule: int_cases4) case (nonneg n) thus ?thesis - by (cases "n = 0") - (auto intro!: derivative_eq_intros simp: field_simps power_int_diff - simp flip: power_Suc power_Suc2 power_add) + by (cases "n = 0"; cases "f x = 0") + (auto intro!: derivative_eq_intros simp: field_simps power_int_diff + power_diff power_int_0_left_if) next case (neg n) - thus ?thesis + thus ?thesis using assms(2) by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus simp flip: power_Suc power_Suc2 power_add) qed diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Filter.thy --- a/src/HOL/Filter.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Filter.thy Fri Apr 04 22:20:30 2025 +0200 @@ -1132,6 +1132,38 @@ by (intro exI[of _ P] exI[of _ "\x. True"]) auto qed +lemma eventually_eventually_prod_filter1: + assumes "eventually P (F \\<^sub>F G)" + shows "eventually (\x. eventually (\y. P (x, y)) G) F" +proof - + from assms obtain Pf Pg where + *: "eventually Pf F" "eventually Pg G" "\x y. Pf x \ Pg y \ P (x, y)" + unfolding eventually_prod_filter by auto + show ?thesis + using *(1) + proof eventually_elim + case x: (elim x) + show ?case + using *(2) by eventually_elim (use x *(3) in auto) + qed +qed + +lemma eventually_eventually_prod_filter2: + assumes "eventually P (F \\<^sub>F G)" + shows "eventually (\y. eventually (\x. P (x, y)) F) G" +proof - + from assms obtain Pf Pg where + *: "eventually Pf F" "eventually Pg G" "\x y. Pf x \ Pg y \ P (x, y)" + unfolding eventually_prod_filter by auto + show ?thesis + using *(2) + proof eventually_elim + case y: (elim y) + show ?case + using *(1) by eventually_elim (use y *(3) in auto) + qed +qed + lemma INF_filter_bot_base: fixes F :: "'a \ 'b filter" assumes *: "\i j. i \ I \ j \ I \ \k\I. F k \ F i \ F j" diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Fun.thy --- a/src/HOL/Fun.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Fun.thy Fri Apr 04 22:20:30 2025 +0200 @@ -368,6 +368,15 @@ lemma bij_betw_singletonI [intro]: "f x = y \ bij_betw f {x} {y}" by auto +lemma bij_betw_imp_empty_iff: "bij_betw f A B \ A = {} \ B = {}" + unfolding bij_betw_def by blast + +lemma bij_betw_imp_Ex_iff: "bij_betw f {x. P x} {x. Q x} \ (\x. P x) \ (\x. Q x)" + unfolding bij_betw_def by blast + +lemma bij_betw_imp_Bex_iff: "bij_betw f {x\A. P x} {x\B. Q x} \ (\x\A. P x) \ (\x\B. Q x)" + unfolding bij_betw_def by blast + lemma bij_betw_apply: "\bij_betw f A B; a \ A\ \ f a \ B" unfolding bij_betw_def by auto @@ -1041,10 +1050,10 @@ where "strict_mono_on A \ monotone_on A (<) (<)" abbreviation antimono_on :: "'a set \ ('a \ 'b :: ord) \ bool" - where "antimono_on A \ monotone_on A (\) (\)" + where "antimono_on A \ monotone_on A (\) (\x y. y \ x)" abbreviation strict_antimono_on :: "'a set \ ('a \ 'b :: ord) \ bool" - where "strict_antimono_on A \ monotone_on A (<) (>)" + where "strict_antimono_on A \ monotone_on A (<) (\x y. y < x)" lemma mono_on_def[no_atp]: "mono_on A f \ (\r s. r \ A \ s \ A \ r \ s \ f r \ f s)" by (auto simp add: monotone_on_def) @@ -1075,17 +1084,6 @@ end -lemma mono_on_greaterD: - fixes g :: "'a::linorder \ 'b::linorder" - assumes "mono_on A g" "x \ A" "y \ A" "g x > g y" - shows "x > y" -proof (rule ccontr) - assume "\x > y" - hence "x \ y" by (simp add: not_less) - from assms(1-3) and this have "g x \ g y" by (rule mono_onD) - with assms(4) show False by simp -qed - context order begin abbreviation mono :: "('a \ 'b::order) \ bool" @@ -1144,62 +1142,54 @@ from assms show "f x \ f y" by (simp add: antimono_def) qed +end + lemma mono_imp_mono_on: "mono f \ mono_on A f" by (rule monotone_on_subset[OF _ subset_UNIV]) -lemma strict_mono_mono [dest?]: - assumes "strict_mono f" - shows "mono f" -proof (rule monoI) - fix x y - assume "x \ y" - show "f x \ f y" - proof (cases "x = y") - case True then show ?thesis by simp - next - case False with \x \ y\ have "x < y" by simp - with assms strict_monoD have "f x < f y" by auto - then show ?thesis by simp - - qed +lemma strict_mono_on_imp_mono_on: "strict_mono_on A f \ mono_on A f" + for f :: "'a::order \ 'b::preorder" +proof (intro mono_onI) + fix r s :: 'a assume asm: "r \ s" "strict_mono_on A f" "r \ A" "s \ A" + from this(1) consider "r < s" | "r = s" by fastforce + then show "f r \ f s" + proof(cases) + case 1 + from strict_mono_onD[OF asm(2-4) this] show ?thesis by (fact order.strict_implies_order) + qed simp qed +lemma strict_mono_mono [dest?]: + "strict_mono f \ mono f" + by (fact strict_mono_on_imp_mono_on) + lemma mono_on_ident: "mono_on S (\x. x)" - by (simp add: monotone_on_def) + by (intro monotone_onI) + +lemma mono_on_id: "mono_on S id" + unfolding id_def by (fact mono_on_ident) lemma strict_mono_on_ident: "strict_mono_on S (\x. x)" - by (simp add: monotone_on_def) + by (intro monotone_onI) + +lemma strict_mono_on_id: "strict_mono_on S id" + unfolding id_def by (fact strict_mono_on_ident) lemma mono_on_const: - fixes a :: "'b::order" shows "mono_on S (\x. a)" - by (simp add: mono_on_def) + fixes a :: "'b::preorder" shows "mono_on S (\x. a)" + by (intro monotone_onI order.refl) lemma antimono_on_const: - fixes a :: "'b::order" shows "antimono_on S (\x. a)" - by (simp add: monotone_on_def) + fixes a :: "'b::preorder" shows "antimono_on S (\x. a)" + by (intro monotone_onI order.refl) -end context linorder begin -lemma mono_invE: - fixes f :: "'a \ 'b::order" - assumes "mono f" - assumes "f x < f y" - obtains "x \ y" -proof - show "x \ y" - proof (rule ccontr) - assume "\ x \ y" - then have "y \ x" by simp - with \mono f\ obtain "f y \ f x" by (rule monoE) - with \f x < f y\ show False by simp - qed -qed - -lemma mono_strict_invE: - fixes f :: "'a \ 'b::order" - assumes "mono f" +lemma mono_on_strict_invE: + fixes f :: "'a \ 'b::preorder" + assumes "mono_on S f" + assumes "x \ S" "y \ S" assumes "f x < f y" obtains "x < y" proof @@ -1207,47 +1197,68 @@ proof (rule ccontr) assume "\ x < y" then have "y \ x" by simp - with \mono f\ obtain "f y \ f x" by (rule monoE) - with \f x < f y\ show False by simp + with \mono_on S f\ \x \ S\ \y \ S\ have "f y \ f x" by (simp only: monotone_onD) + with \f x < f y\ show False by (simp add: preorder_class.less_le_not_le) qed qed -lemma strict_mono_eq: - assumes "strict_mono f" +corollary mono_on_invE: + fixes f :: "'a \ 'b::preorder" + assumes "mono_on S f" + assumes "x \ S" "y \ S" + assumes "f x < f y" + obtains "x \ y" + using assms mono_on_strict_invE[of S f x y thesis] by simp + +lemma strict_mono_on_eq: + assumes "strict_mono_on S (f::'a \ 'b::preorder)" + assumes "x \ S" "y \ S" shows "f x = f y \ x = y" proof assume "f x = f y" show "x = y" proof (cases x y rule: linorder_cases) - case less with assms strict_monoD have "f x < f y" by auto + case less with assms have "f x < f y" by (simp add: monotone_onD) with \f x = f y\ show ?thesis by simp next case equal then show ?thesis . next - case greater with assms strict_monoD have "f y < f x" by auto + case greater with assms have "f y < f x" by (simp add: monotone_onD) with \f x = f y\ show ?thesis by simp qed qed simp -lemma strict_mono_less_eq: - assumes "strict_mono f" +lemma strict_mono_on_less_eq: + assumes "strict_mono_on S (f::'a \ 'b::preorder)" + assumes "x \ S" "y \ S" shows "f x \ f y \ x \ y" proof assume "x \ y" - with assms strict_mono_mono monoD show "f x \ f y" by auto + then show "f x \ f y" + using nless_le[of x y] monotone_onD[OF assms] order_less_imp_le[of "f x" "f y"] + by blast next assume "f x \ f y" - show "x \ y" proof (rule ccontr) - assume "\ x \ y" then have "y < x" by simp - with assms strict_monoD have "f y < f x" by auto - with \f x \ f y\ show False by simp + show "x \ y" + proof (rule ccontr) + assume "\ x \ y" + then have "y < x" by simp + with assms have "f y < f x" by (simp add: monotone_onD) + with \f x \ f y\ show False by (simp add: preorder_class.less_le_not_le) qed qed -lemma strict_mono_less: - assumes "strict_mono f" +lemma strict_mono_on_less: + assumes "strict_mono_on S (f::'a \ _::preorder)" + assumes "x \ S" "y \ S" shows "f x < f y \ x < y" - using assms - by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq) + using assms strict_mono_on_eq[of S f x y] + by (auto simp add: strict_mono_on_less_eq preorder_class.less_le_not_le) + +lemmas mono_invE = mono_on_invE[OF _ UNIV_I UNIV_I] +lemmas mono_strict_invE = mono_on_strict_invE[OF _ UNIV_I UNIV_I] +lemmas strict_mono_eq = strict_mono_on_eq[OF _ UNIV_I UNIV_I] +lemmas strict_mono_less_eq = strict_mono_on_less_eq[OF _ UNIV_I UNIV_I] +lemmas strict_mono_less = strict_mono_on_less[OF _ UNIV_I UNIV_I] end @@ -1274,7 +1285,7 @@ qed lemma strict_mono_on_leD: - fixes f :: "'a::linorder \ 'b::preorder" + fixes f :: "'a::order \ 'b::preorder" assumes "strict_mono_on A f" "x \ A" "y \ A" "x \ y" shows "f x \ f y" proof (cases "x = y") @@ -1293,10 +1304,6 @@ shows "y = x" using assms by (cases rule: linorder_cases) (auto dest: strict_mono_onD) -lemma strict_mono_on_imp_mono_on: "strict_mono_on A f \ mono_on A f" - for f :: "'a::linorder \ 'b::preorder" - by (rule mono_onI, rule strict_mono_on_leD) - lemma mono_imp_strict_mono: fixes f :: "'a::order \ 'b::order" shows "\mono_on S f; inj_on f S\ \ strict_mono_on S f" diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Groups_Big.thy Fri Apr 04 22:20:30 2025 +0200 @@ -1580,6 +1580,16 @@ qed qed +lemma prod_uminus: "(\x\A. -f x :: 'a :: comm_ring_1) = (-1) ^ card A * (\x\A. f x)" + by (induction A rule: infinite_finite_induct) (auto simp: algebra_simps) + +lemma prod_diff: + fixes f :: "'a \ 'b :: field" + assumes "finite A" "B \ A" "\x. x \ B \ f x \ 0" + shows "prod f (A - B) = prod f A / prod f B" + by (metis assms finite_subset nonzero_eq_divide_eq prod.subset_diff + prod_zero_iff) + lemma sum_zero_power [simp]: "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)" for c :: "nat \ 'a::division_ring" by (induct A rule: infinite_finite_induct) auto @@ -1712,10 +1722,22 @@ for y :: "'a::comm_monoid_mult" by (induct A rule: infinite_finite_induct) simp_all +lemma prod_diff_swap: + fixes f :: "'a \ 'b :: comm_ring_1" + shows "prod (\x. f x - g x) A = (-1) ^ card A * prod (\x. g x - f x) A" + using prod.distrib[of "\_. -1" "\x. f x - g x" A] + by simp + lemma prod_power_distrib: "prod f A ^ n = prod (\x. (f x) ^ n) A" for f :: "'a \ 'b::comm_semiring_1" by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib) +lemma power_inject_exp': + assumes "a \ 1" "a > (0 :: 'a :: linordered_semidom)" + shows "a ^ m = a ^ n \ m = n" + by (metis assms not_less_iff_gr_or_eq order_le_less power_decreasing_iff + power_inject_exp) + lemma power_sum: "c ^ (\a\A. f a) = (\a\A. c ^ f a)" by (induct A rule: infinite_finite_induct) (simp_all add: power_add) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/HOL.thy Fri Apr 04 22:20:30 2025 +0200 @@ -5,7 +5,7 @@ section \The basis of Higher-Order Logic\ theory HOL -imports Pure Tools.Code_Generator +imports Pure Try0 Tools.Code_Generator keywords "try" "solve_direct" "quickcheck" "print_coercions" "print_claset" "print_induct_rules" :: diag and @@ -34,6 +34,12 @@ ML_file \~~/src/Tools/subtyping.ML\ ML_file \~~/src/Tools/case_product.ML\ +ML \ +val _ = + Try.tool_setup + {name = "try0", weight = 30, auto_option = \<^system_option>\auto_methods\, + body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE Try0.empty_facts} +\ ML \Plugin_Name.declare_setup \<^binding>\extraction\\ diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Int.thy --- a/src/HOL/Int.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Int.thy Fri Apr 04 22:20:30 2025 +0200 @@ -1881,6 +1881,15 @@ lemma power_int_mult: "power_int (x :: 'a) (m * n) = power_int (power_int x m) n" by (auto simp: power_int_def zero_le_mult_iff simp flip: power_mult power_inverse nat_mult_distrib) +lemma power_int_power: "(a ^ b :: 'a :: division_ring) powi c = a powi (int b * c)" + by (subst power_int_mult) simp + +lemma power_int_power': "(a powi b :: 'a :: division_ring) ^ c = a powi (b * int c)" + by (simp add: power_int_mult) + +lemma power_int_nonneg_exp: "n \ 0 \ x powi n = x ^ nat n" + by (simp add: power_int_def) + end context diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Code_Lazy.thy --- a/src/HOL/Library/Code_Lazy.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Library/Code_Lazy.thy Fri Apr 04 22:20:30 2025 +0200 @@ -67,50 +67,8 @@ has been evaluated to or not. \ -code_printing code_module Lazy \ (SML) -\signature LAZY = -sig - type 'a lazy; - val lazy : (unit -> 'a) -> 'a lazy; - val force : 'a lazy -> 'a; - val peek : 'a lazy -> 'a option - val termify_lazy : - (string -> 'typerep -> 'term) -> - ('term -> 'term -> 'term) -> - (string -> 'typerep -> 'term -> 'term) -> - 'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) -> - ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term; -end; - -structure Lazy : LAZY = -struct - -datatype 'a content = - Delay of unit -> 'a - | Value of 'a - | Exn of exn; - -datatype 'a lazy = Lazy of 'a content ref; - -fun lazy f = Lazy (ref (Delay f)); - -fun force (Lazy x) = case !x of - Delay f => ( - let val res = f (); val _ = x := Value res; in res end - handle exn => (x := Exn exn; raise exn)) - | Value x => x - | Exn exn => raise exn; - -fun peek (Lazy x) = case !x of - Value x => SOME x - | _ => NONE; - -fun termify_lazy const app abs unitT funT lazyT term_of T x _ = - app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T))) - (case peek x of SOME y => abs "_" unitT (term_of y) - | _ => const "Pure.dummy_pattern" (funT unitT T)); - -end;\ for type_constructor lazy constant delay force termify_lazy +code_printing code_module Lazy \ (SML) file "~~/src/HOL/Library/Tools/lazy.ML" + for type_constructor lazy constant delay force termify_lazy | type_constructor lazy \ (SML) "_ Lazy.lazy" | constant delay \ (SML) "Lazy.lazy" | constant force \ (SML) "Lazy.force" @@ -124,17 +82,8 @@ | type_constructor lazy \ (Eval) "_ Lazy.lazy" | constant delay \ (Eval) "Lazy.lazy" | constant force \ (Eval) "Lazy.force" -| code_module Termify_Lazy \ (Eval) -\structure Termify_Lazy = struct -fun termify_lazy - (_: string -> typ -> term) (_: term -> term -> term) (_: string -> typ -> term -> term) - (_: typ) (_: typ -> typ -> typ) (_: typ -> typ) - (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) = - Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $ - (case Lazy.peek x of - SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x) - | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T)); -end;\ for constant termify_lazy +| code_module Termify_Lazy \ (Eval) file "~~/src/HOL/Library/Tools/termify_lazy.ML" + for constant termify_lazy | constant termify_lazy \ (Eval) "Termify'_Lazy.termify'_lazy" code_reserved (Eval) Termify_Lazy @@ -143,34 +92,15 @@ type_constructor lazy \ (OCaml) "_ Lazy.t" | constant delay \ (OCaml) "Lazy.from'_fun" | constant force \ (OCaml) "Lazy.force" -| code_module Termify_Lazy \ (OCaml) -\module Termify_Lazy : sig - val termify_lazy : - (string -> 'typerep -> 'term) -> - ('term -> 'term -> 'term) -> - (string -> 'typerep -> 'term -> 'term) -> - 'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) -> - ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term -end = struct - -let termify_lazy const app abs unitT funT lazyT term_of ty x _ = - app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty))) - (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x)) - else const "Pure.dummy_pattern" (funT unitT ty));; - -end;;\ for constant termify_lazy +| code_module Termify_Lazy \ (OCaml) file "~~/src/HOL/Library/Tools/termify_lazy.ocaml" + for constant termify_lazy | constant termify_lazy \ (OCaml) "Termify'_Lazy.termify'_lazy" code_reserved (OCaml) Lazy Termify_Lazy - code_printing - code_module Lazy \ (Haskell) \ -module Lazy(Lazy, delay, force) where - -newtype Lazy a = Lazy a -delay f = Lazy (f ()) -force (Lazy x) = x\ for type_constructor lazy constant delay force + code_module Lazy \ (Haskell) file "~~/src/HOL/Library/Tools/lazy.hs" + for type_constructor lazy constant delay force | type_constructor lazy \ (Haskell) "Lazy.Lazy _" | constant delay \ (Haskell) "Lazy.delay" | constant force \ (Haskell) "Lazy.force" @@ -178,43 +108,8 @@ code_reserved (Haskell) Lazy code_printing - code_module Lazy \ (Scala) -\object Lazy { - final class Lazy[A] (f: Unit => A) { - var evaluated = false; - lazy val x: A = f(()) - - def get() : A = { - evaluated = true; - return x - } - } - - def force[A] (x: Lazy[A]) : A = { - return x.get() - } - - def delay[A] (f: Unit => A) : Lazy[A] = { - return new Lazy[A] (f) - } - - def termify_lazy[Typerep, Term, A] ( - const: String => Typerep => Term, - app: Term => Term => Term, - abs: String => Typerep => Term => Term, - unitT: Typerep, - funT: Typerep => Typerep => Typerep, - lazyT: Typerep => Typerep, - term_of: A => Term, - ty: Typerep, - x: Lazy[A], - dummy: Term) : Term = { - x.evaluated match { - case true => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get()))) - case false => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty))) - } - } -}\ for type_constructor lazy constant delay force termify_lazy + code_module Lazy \ (Scala) file "~~/src/HOL/Library/Tools/lazy.scala" + for type_constructor lazy constant delay force termify_lazy | type_constructor lazy \ (Scala) "Lazy.Lazy[_]" | constant delay \ (Scala) "Lazy.delay" | constant force \ (Scala) "Lazy.force" diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Comparator.thy --- a/src/HOL/Library/Comparator.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Library/Comparator.thy Fri Apr 04 22:20:30 2025 +0200 @@ -13,146 +13,146 @@ datatype comp = Less | Equiv | Greater locale comparator = - fixes cmp :: "'a \ 'a \ comp" - assumes refl [simp]: "\a. cmp a a = Equiv" - and trans_equiv: "\a b c. cmp a b = Equiv \ cmp b c = Equiv \ cmp a c = Equiv" - assumes trans_less: "cmp a b = Less \ cmp b c = Less \ cmp a c = Less" - and greater_iff_sym_less: "\b a. cmp b a = Greater \ cmp a b = Less" + fixes cmp :: \'a \ 'a \ comp\ + assumes refl [simp]: \\a. cmp a a = Equiv\ + and trans_equiv: \\a b c. cmp a b = Equiv \ cmp b c = Equiv \ cmp a c = Equiv\ + assumes trans_less: \cmp a b = Less \ cmp b c = Less \ cmp a c = Less\ + and greater_iff_sym_less: \\b a. cmp b a = Greater \ cmp a b = Less\ begin text \Dual properties\ lemma trans_greater: - "cmp a c = Greater" if "cmp a b = Greater" "cmp b c = Greater" + \cmp a c = Greater\ if \cmp a b = Greater\ \cmp b c = Greater\ using that greater_iff_sym_less trans_less by blast lemma less_iff_sym_greater: - "cmp b a = Less \ cmp a b = Greater" + \cmp b a = Less \ cmp a b = Greater\ by (simp add: greater_iff_sym_less) text \The equivalence part\ lemma sym: - "cmp b a = Equiv \ cmp a b = Equiv" + \cmp b a = Equiv \ cmp a b = Equiv\ by (metis (full_types) comp.exhaust greater_iff_sym_less) lemma reflp: - "reflp (\a b. cmp a b = Equiv)" + \reflp (\a b. cmp a b = Equiv)\ by (rule reflpI) simp lemma symp: - "symp (\a b. cmp a b = Equiv)" + \symp (\a b. cmp a b = Equiv)\ by (rule sympI) (simp add: sym) lemma transp: - "transp (\a b. cmp a b = Equiv)" + \transp (\a b. cmp a b = Equiv)\ by (rule transpI) (fact trans_equiv) lemma equivp: - "equivp (\a b. cmp a b = Equiv)" + \equivp (\a b. cmp a b = Equiv)\ using reflp symp transp by (rule equivpI) text \The strict part\ lemma irreflp_less: - "irreflp (\a b. cmp a b = Less)" + \irreflp (\a b. cmp a b = Less)\ by (rule irreflpI) simp lemma irreflp_greater: - "irreflp (\a b. cmp a b = Greater)" + \irreflp (\a b. cmp a b = Greater)\ by (rule irreflpI) simp lemma asym_less: - "cmp b a \ Less" if "cmp a b = Less" + \cmp b a \ Less\ if \cmp a b = Less\ using that greater_iff_sym_less by force lemma asym_greater: - "cmp b a \ Greater" if "cmp a b = Greater" + \cmp b a \ Greater\ if \cmp a b = Greater\ using that greater_iff_sym_less by force lemma asymp_less: - "asymp (\a b. cmp a b = Less)" - using irreflp_less by (auto intro: asympI dest: asym_less) + \asymp (\a b. cmp a b = Less)\ + using irreflp_less by (auto dest: asym_less) lemma asymp_greater: - "asymp (\a b. cmp a b = Greater)" - using irreflp_greater by (auto intro!: asympI dest: asym_greater) + \asymp (\a b. cmp a b = Greater)\ + using irreflp_greater by (auto dest: asym_greater) lemma trans_equiv_less: - "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less" + \cmp a c = Less\ if \cmp a b = Equiv\ and \cmp b c = Less\ using that by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less) lemma trans_less_equiv: - "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv" + \cmp a c = Less\ if \cmp a b = Less\ and \cmp b c = Equiv\ using that by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less) lemma trans_equiv_greater: - "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater" + \cmp a c = Greater\ if \cmp a b = Equiv\ and \cmp b c = Greater\ using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv) lemma trans_greater_equiv: - "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv" + \cmp a c = Greater\ if \cmp a b = Greater\ and \cmp b c = Equiv\ using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less) lemma transp_less: - "transp (\a b. cmp a b = Less)" + \transp (\a b. cmp a b = Less)\ by (rule transpI) (fact trans_less) lemma transp_greater: - "transp (\a b. cmp a b = Greater)" + \transp (\a b. cmp a b = Greater)\ by (rule transpI) (fact trans_greater) text \The reflexive part\ lemma reflp_not_less: - "reflp (\a b. cmp a b \ Less)" + \reflp (\a b. cmp a b \ Less)\ by (rule reflpI) simp lemma reflp_not_greater: - "reflp (\a b. cmp a b \ Greater)" + \reflp (\a b. cmp a b \ Greater)\ by (rule reflpI) simp lemma quasisym_not_less: - "cmp a b = Equiv" if "cmp a b \ Less" and "cmp b a \ Less" + \cmp a b = Equiv\ if \cmp a b \ Less\ and \cmp b a \ Less\ using that comp.exhaust greater_iff_sym_less by auto lemma quasisym_not_greater: - "cmp a b = Equiv" if "cmp a b \ Greater" and "cmp b a \ Greater" + \cmp a b = Equiv\ if \cmp a b \ Greater\ and \cmp b a \ Greater\ using that comp.exhaust greater_iff_sym_less by auto lemma trans_not_less: - "cmp a c \ Less" if "cmp a b \ Less" "cmp b c \ Less" + \cmp a c \ Less\ if \cmp a b \ Less\ \cmp b c \ Less\ using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less) lemma trans_not_greater: - "cmp a c \ Greater" if "cmp a b \ Greater" "cmp b c \ Greater" + \cmp a c \ Greater\ if \cmp a b \ Greater\ \cmp b c \ Greater\ using that greater_iff_sym_less trans_not_less by blast lemma transp_not_less: - "transp (\a b. cmp a b \ Less)" + \transp (\a b. cmp a b \ Less)\ by (rule transpI) (fact trans_not_less) lemma transp_not_greater: - "transp (\a b. cmp a b \ Greater)" + \transp (\a b. cmp a b \ Greater)\ by (rule transpI) (fact trans_not_greater) text \Substitution under equivalences\ lemma equiv_subst_left: - "cmp z y = comp \ cmp x y = comp" if "cmp z x = Equiv" for comp + \cmp z y = comp \ cmp x y = comp\ if \cmp z x = Equiv\ for comp proof - - from that have "cmp x z = Equiv" + from that have \cmp x z = Equiv\ by (simp add: sym) with that show ?thesis by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater) qed lemma equiv_subst_right: - "cmp x z = comp \ cmp x y = comp" if "cmp z y = Equiv" for comp + \cmp x z = comp \ cmp x y = comp\ if \cmp z y = Equiv\ for comp proof - - from that have "cmp y z = Equiv" + from that have \cmp y z = Equiv\ by (simp add: sym) with that show ?thesis by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv) @@ -160,10 +160,10 @@ end -typedef 'a comparator = "{cmp :: 'a \ 'a \ comp. comparator cmp}" +typedef 'a comparator = \{cmp :: 'a \ 'a \ comp. comparator cmp}\ morphisms compare Abs_comparator proof - - have "comparator (\_ _. Equiv)" + have \comparator (\_ _. Equiv)\ by standard simp_all then show ?thesis by auto @@ -171,30 +171,42 @@ setup_lifting type_definition_comparator -global_interpretation compare: comparator "compare cmp" +global_interpretation compare: comparator \compare cmp\ using compare [of cmp] by simp -lift_definition flat :: "'a comparator" - is "\_ _. Equiv" by standard simp_all +lift_definition flat :: \'a comparator\ + is \\_ _. Equiv\ by standard simp_all instantiation comparator :: (linorder) default begin -lift_definition default_comparator :: "'a comparator" - is "\x y. if x < y then Less else if x > y then Greater else Equiv" +lift_definition default_comparator :: \'a comparator\ + is \\x y. if x < y then Less else if x > y then Greater else Equiv\ by standard (auto split: if_splits) instance .. end +lemma compare_default_eq_Less_iff [simp]: + \compare default x y = Less \ x < y\ + by transfer simp + +lemma compare_default_eq_Equiv_iff [simp]: + \compare default x y = Equiv \ x = y\ + by transfer auto + +lemma compare_default_eq_Greater_iff [simp]: + \compare default x y = Greater \ x > y\ + by transfer auto + text \A rudimentary quickcheck setup\ instantiation comparator :: (enum) equal begin -lift_definition equal_comparator :: "'a comparator \ 'a comparator \ bool" - is "\f g. \x \ set Enum.enum. f x = g x" . +lift_definition equal_comparator :: \'a comparator \ 'a comparator \ bool\ + is \\f g. \x \ set Enum.enum. f x = g x\ . instance by (standard; transfer) (auto simp add: enum_UNIV) @@ -202,23 +214,23 @@ end lemma [code]: - "HOL.equal cmp1 cmp2 \ Enum.enum_all (\x. compare cmp1 x = compare cmp2 x)" + \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" + \HOL.equal (cmp :: 'a::enum comparator) cmp \ True\ by (fact equal_refl) instantiation comparator :: ("{linorder, typerep}") full_exhaustive begin definition full_exhaustive_comparator :: - "('a comparator \ (unit \ term) \ (bool \ term list) option) - \ natural \ (bool \ term list) option" - where "full_exhaustive_comparator f s = + \('a comparator \ (unit \ term) \ (bool \ term list) option) + \ natural \ (bool \ term list) option\ + where \full_exhaustive_comparator f s = Quickcheck_Exhaustive.orelse (f (flat, (\u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator)))) - (f (default, (\u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))" + (f (default, (\u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))\ instance .. @@ -227,67 +239,108 @@ subsection \Fundamental comparator combinators\ -lift_definition reversed :: "'a comparator \ 'a comparator" - is "\cmp a b. cmp b a" +lift_definition reversed :: \'a comparator \ 'a comparator\ + is \\cmp a b. cmp b a\ proof - - fix cmp :: "'a \ 'a \ comp" - assume "comparator cmp" + fix cmp :: \'a \ 'a \ comp\ + assume \comparator cmp\ then interpret comparator cmp . - show "comparator (\a b. cmp b a)" + show \comparator (\a b. cmp b a)\ + by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less) +qed + +lemma compare_reversed_apply [simp]: + \compare (reversed cmp) x y = compare cmp y x\ + by transfer simp + +lift_definition key :: \('b \ 'a) \ 'a comparator \ 'b comparator\ + is \\f cmp a b. cmp (f a) (f b)\ +proof - + fix cmp :: \'a \ 'a \ comp\ and f :: \'b \ 'a\ + assume \comparator cmp\ + then interpret comparator cmp . + show \comparator (\a b. cmp (f a) (f b))\ by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less) qed -lift_definition key :: "('b \ 'a) \ 'a comparator \ 'b comparator" - is "\f cmp a b. cmp (f a) (f b)" +lemma compare_key_apply [simp]: + \compare (key f cmp) x y = compare cmp (f x) (f y)\ + by transfer simp + +lift_definition prod_lex :: \'a comparator \ 'b comparator \ ('a \ 'b) comparator\ + is \\f g (a, c) (b, d). case f a b of Less \ Less | Equiv \ g c d | Greater \ Greater\ proof - - fix cmp :: "'a \ 'a \ comp" and f :: "'b \ 'a" - assume "comparator cmp" - then interpret comparator cmp . - show "comparator (\a b. cmp (f a) (f b))" - by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less) + fix f :: \'a \ 'a \ comp\ and g :: \'b \ 'b \ comp\ + assume \comparator f\ + then interpret f: comparator f . + assume \comparator g\ + then interpret g: comparator g . + define h where \h = (\(a, c) (b, d). case f a b of Less \ Less | Equiv \ g c d | Greater \ Greater)\ + then have h_apply [simp]: \h (a, c) (b, d) = (case f a b of Less \ Less | Equiv \ g c d | Greater \ Greater)\ for a b c d + by simp + have h_equiv: \h p q = Equiv \ f (fst p) (fst q) = Equiv \ g (snd p) (snd q) = Equiv\ for p q + by (cases p; cases q) (simp split: comp.split) + have h_less: \h p q = Less \ f (fst p) (fst q) = Less \ f (fst p) (fst q) = Equiv \ g (snd p) (snd q) = Less\ for p q + by (cases p; cases q) (simp split: comp.split) + have h_greater: \h p q = Greater \ f (fst p) (fst q) = Greater \ f (fst p) (fst q) = Equiv \ g (snd p) (snd q) = Greater\ for p q + by (cases p; cases q) (simp split: comp.split) + have \comparator h\ + apply standard + apply (simp_all add: h_equiv h_less h_greater f.greater_iff_sym_less g.greater_iff_sym_less f.sym g.sym) + apply (auto intro: f.trans_equiv g.trans_equiv f.trans_less g.trans_less f.trans_less_equiv f.trans_equiv_less) + done + then show \comparator (\(a, c) (b, d). case f a b of Less \ Less + | Equiv \ g c d + | Greater \ Greater)\ + by (simp add: h_def) qed +lemma compare_prod_lex_apply: + \compare (prod_lex cmp1 cmp2) p q = + (case compare (key fst cmp1) p q of Less \ Less | Equiv \ compare (key snd cmp2) p q | Greater \ Greater)\ + by transfer (simp add: split_def) + subsection \Direct implementations for linear orders on selected types\ -definition comparator_bool :: "bool comparator" - where [simp, code_abbrev]: "comparator_bool = default" +definition comparator_bool :: \bool comparator\ + where [simp, code_abbrev]: \comparator_bool = default\ lemma compare_comparator_bool [code abstract]: - "compare comparator_bool = (\p q. + \compare comparator_bool = (\p q. if p then if q then Equiv else Greater - else if q then Less else Equiv)" - by (auto simp add: fun_eq_iff) (transfer; simp)+ + else if q then Less else Equiv)\ + by (auto simp add: fun_eq_iff) -definition raw_comparator_nat :: "nat \ nat \ comp" - where [simp]: "raw_comparator_nat = compare default" +definition raw_comparator_nat :: \nat \ nat \ comp\ + where [simp]: \raw_comparator_nat = compare default\ lemma default_comparator_nat [simp, code]: - "raw_comparator_nat (0::nat) 0 = Equiv" - "raw_comparator_nat (Suc m) 0 = Greater" - "raw_comparator_nat 0 (Suc n) = Less" - "raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n" + \raw_comparator_nat (0::nat) 0 = Equiv\ + \raw_comparator_nat (Suc m) 0 = Greater\ + \raw_comparator_nat 0 (Suc n) = Less\ + \raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n\ by (transfer; simp)+ -definition comparator_nat :: "nat comparator" - where [simp, code_abbrev]: "comparator_nat = default" +definition comparator_nat :: \nat comparator\ + where [simp, code_abbrev]: \comparator_nat = default\ lemma compare_comparator_nat [code abstract]: - "compare comparator_nat = raw_comparator_nat" + \compare comparator_nat = raw_comparator_nat\ by simp -definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator" - where [simp, code_abbrev]: "comparator_linordered_group = default" +definition comparator_linordered_group :: \'a::linordered_ab_group_add comparator\ + where [simp, code_abbrev]: \comparator_linordered_group = default\ lemma comparator_linordered_group [code abstract]: - "compare comparator_linordered_group = (\a b. + \compare comparator_linordered_group = (\a b. let c = a - b in if c < 0 then Less - else if c = 0 then Equiv else Greater)" + else if c = 0 then Equiv else Greater)\ proof (rule ext)+ fix a b :: 'a - show "compare comparator_linordered_group a b = + show \compare comparator_linordered_group a b = (let c = a - b in if c < 0 then Less - else if c = 0 then Equiv else Greater)" + else if c = 0 then Equiv else Greater)\ by (simp add: Let_def not_less) (transfer; auto) qed diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Infinite_Typeclass.thy --- a/src/HOL/Library/Infinite_Typeclass.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Library/Infinite_Typeclass.thy Fri Apr 04 22:20:30 2025 +0200 @@ -27,6 +27,9 @@ by auto qed +lemma arb_inj_on_finite_infinite: "finite(A :: 'b set) \ \f :: 'b \ 'a. inj_on f A" +by (meson arb_finite_subset card_le_inj infinite_imp_nonempty) + lemma arb_countable_map: "finite Y \ \f :: (nat \ 'a). inj f \ range f \ UNIV - Y" using infinite_UNIV by (auto simp: infinite_countable_subset) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Sorting_Algorithms.thy --- a/src/HOL/Library/Sorting_Algorithms.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Library/Sorting_Algorithms.thy Fri Apr 04 22:20:30 2025 +0200 @@ -8,43 +8,43 @@ section \Stably sorted lists\ -abbreviation (input) stable_segment :: "'a comparator \ 'a \ 'a list \ 'a list" - where "stable_segment cmp x \ filter (\y. compare cmp x y = Equiv)" +abbreviation (input) stable_segment :: \'a comparator \ 'a \ 'a list \ 'a list\ + where \stable_segment cmp x \ filter (\y. compare cmp x y = Equiv)\ -fun sorted :: "'a comparator \ 'a list \ bool" - where sorted_Nil: "sorted cmp [] \ True" - | sorted_single: "sorted cmp [x] \ True" - | sorted_rec: "sorted cmp (y # x # xs) \ compare cmp y x \ Greater \ sorted cmp (x # xs)" +fun sorted :: \'a comparator \ 'a list \ bool\ + where sorted_Nil: \sorted cmp [] \ True\ + | sorted_single: \sorted cmp [x] \ True\ + | sorted_rec: \sorted cmp (y # x # xs) \ compare cmp y x \ Greater \ sorted cmp (x # xs)\ lemma sorted_ConsI: - "sorted cmp (x # xs)" if "sorted cmp xs" - and "\y ys. xs = y # ys \ compare cmp x y \ Greater" + \sorted cmp (x # xs)\ if \sorted cmp xs\ + and \\y ys. xs = y # ys \ compare cmp x y \ Greater\ using that by (cases xs) simp_all lemma sorted_Cons_imp_sorted: - "sorted cmp xs" if "sorted cmp (x # xs)" + \sorted cmp xs\ if \sorted cmp (x # xs)\ using that by (cases xs) simp_all lemma sorted_Cons_imp_not_less: - "compare cmp y x \ Greater" if "sorted cmp (y # xs)" - and "x \ set xs" + \compare cmp y x \ Greater\ if \sorted cmp (y # xs)\ + and \x \ set xs\ using that by (induction xs arbitrary: y) (auto dest: compare.trans_not_greater) lemma sorted_induct [consumes 1, case_names Nil Cons, induct pred: sorted]: - "P xs" if "sorted cmp xs" and "P []" - and *: "\x xs. sorted cmp xs \ P xs - \ (\y. y \ set xs \ compare cmp x y \ Greater) \ P (x # xs)" + \P xs\ if \sorted cmp xs\ and \P []\ + and *: \\x xs. sorted cmp xs \ P xs + \ (\y. y \ set xs \ compare cmp x y \ Greater) \ P (x # xs)\ using \sorted cmp xs\ proof (induction xs) case Nil show ?case by (rule \P []\) next case (Cons x xs) - from \sorted cmp (x # xs)\ have "sorted cmp xs" + from \sorted cmp (x # xs)\ have \sorted cmp xs\ by (cases xs) simp_all - moreover have "P xs" using \sorted cmp xs\ + moreover have \P xs\ using \sorted cmp xs\ by (rule Cons.IH) - moreover have "compare cmp x y \ Greater" if "y \ set xs" for y + moreover have \compare cmp x y \ Greater\ if \y \ set xs\ for y using that \sorted cmp (x # xs)\ proof (induction xs) case Nil then show ?case @@ -58,9 +58,9 @@ by simp next case (Cons w ws) - with Cons.prems have "compare cmp z w \ Greater" "compare cmp x z \ Greater" + with Cons.prems have \compare cmp z w \ Greater\ \compare cmp x z \ Greater\ by auto - then have "compare cmp x w \ Greater" + then have \compare cmp x w \ Greater\ by (auto dest: compare.trans_not_greater) with Cons show ?thesis using Cons.prems Cons.IH by auto @@ -71,28 +71,28 @@ qed lemma sorted_induct_remove1 [consumes 1, case_names Nil minimum]: - "P xs" if "sorted cmp xs" and "P []" - and *: "\x xs. sorted cmp xs \ P (remove1 x xs) + \P xs\ if \sorted cmp xs\ and \P []\ + and *: \\x xs. sorted cmp xs \ P (remove1 x xs) \ x \ set xs \ hd (stable_segment cmp x xs) = x \ (\y. y \ set xs \ compare cmp x y \ Greater) - \ P xs" + \ P xs\ using \sorted cmp xs\ proof (induction xs) case Nil show ?case by (rule \P []\) next case (Cons x xs) - then have "sorted cmp (x # xs)" + then have \sorted cmp (x # xs)\ by (simp add: sorted_ConsI) moreover note Cons.IH - moreover have "\y. compare cmp x y = Greater \ y \ set xs \ False" + moreover have \\y. compare cmp x y = Greater \ y \ set xs \ False\ using Cons.hyps by simp ultimately show ?case - by (auto intro!: * [of "x # xs" x]) blast + by (auto intro!: * [of \x # xs\ x]) blast qed lemma sorted_remove1: - "sorted cmp (remove1 x xs)" if "sorted cmp xs" -proof (cases "x \ set xs") + \sorted cmp (remove1 x xs)\ if \sorted cmp xs\ +proof (cases \x \ set xs\) case False with that show ?thesis by (simp add: remove1_idem) @@ -104,21 +104,21 @@ by simp next case (Cons y ys) - show ?case proof (cases "x = y") + show ?case proof (cases \x = y\) case True with Cons.hyps show ?thesis by simp next case False - then have "sorted cmp (remove1 x ys)" + then have \sorted cmp (remove1 x ys)\ using Cons.IH Cons.prems by auto - then have "sorted cmp (y # remove1 x ys)" + then have \sorted cmp (y # remove1 x ys)\ proof (rule sorted_ConsI) fix z zs - assume "remove1 x ys = z # zs" - with \x \ y\ have "z \ set ys" + assume \remove1 x ys = z # zs\ + with \x \ y\ have \z \ set ys\ using notin_set_remove1 [of z ys x] by auto - then show "compare cmp y z \ Greater" + then show \compare cmp y z \ Greater\ by (rule Cons.hyps(2)) qed with False show ?thesis @@ -128,7 +128,7 @@ qed lemma sorted_stable_segment: - "sorted cmp (stable_segment cmp x xs)" + \sorted cmp (stable_segment cmp x xs)\ proof (induction xs) case Nil show ?case @@ -141,22 +141,22 @@ qed -primrec insort :: "'a comparator \ 'a \ 'a list \ 'a list" - where "insort cmp y [] = [y]" - | "insort cmp y (x # xs) = (if compare cmp y x \ Greater +primrec insort :: \'a comparator \ 'a \ 'a list \ 'a list\ + where \insort cmp y [] = [y]\ + | \insort cmp y (x # xs) = (if compare cmp y x \ Greater then y # x # xs - else x # insort cmp y xs)" + else x # insort cmp y xs)\ lemma mset_insort [simp]: - "mset (insort cmp x xs) = add_mset x (mset xs)" + \mset (insort cmp x xs) = add_mset x (mset xs)\ by (induction xs) simp_all lemma length_insort [simp]: - "length (insort cmp x xs) = Suc (length xs)" + \length (insort cmp x xs) = Suc (length xs)\ by (induction xs) simp_all lemma sorted_insort: - "sorted cmp (insort cmp x xs)" if "sorted cmp xs" + \sorted cmp (insort cmp x xs)\ if \sorted cmp xs\ using that proof (induction xs) case Nil then show ?case @@ -168,37 +168,37 @@ qed lemma stable_insort_equiv: - "stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs" - if "compare cmp y x = Equiv" + \stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs\ + if \compare cmp y x = Equiv\ proof (induction xs) case Nil from that show ?case by simp next case (Cons z xs) - moreover from that have "compare cmp y z = Equiv \ compare cmp z x = Equiv" + moreover from that have \compare cmp y z = Equiv \ compare cmp z x = Equiv\ by (auto intro: compare.trans_equiv simp add: compare.sym) ultimately show ?case using that by (auto simp add: compare.greater_iff_sym_less) qed lemma stable_insort_not_equiv: - "stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs" - if "compare cmp y x \ Equiv" + \stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs\ + if \compare cmp y x \ Equiv\ using that by (induction xs) simp_all lemma remove1_insort_same_eq [simp]: - "remove1 x (insort cmp x xs) = xs" + \remove1 x (insort cmp x xs) = xs\ by (induction xs) simp_all lemma insort_eq_ConsI: - "insort cmp x xs = x # xs" - if "sorted cmp xs" "\y. y \ set xs \ compare cmp x y \ Greater" + \insort cmp x xs = x # xs\ + if \sorted cmp xs\ \\y. y \ set xs \ compare cmp x y \ Greater\ using that by (induction xs) (simp_all add: compare.greater_iff_sym_less) lemma remove1_insort_not_same_eq [simp]: - "remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)" - if "sorted cmp xs" "x \ y" + \remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)\ + if \sorted cmp xs\ \x \ y\ using that proof (induction xs) case Nil then show ?case @@ -206,13 +206,13 @@ next case (Cons z zs) show ?case - proof (cases "compare cmp x z = Greater") + proof (cases \compare cmp x z = Greater\) case True with Cons show ?thesis by simp next case False - then have "compare cmp x y \ Greater" if "y \ set zs" for y + then have \compare cmp x y \ Greater\ if \y \ set zs\ for y using that Cons.hyps by (auto dest: compare.trans_not_greater) with Cons show ?thesis @@ -221,25 +221,25 @@ qed lemma insort_remove1_same_eq: - "insort cmp x (remove1 x xs) = xs" - if "sorted cmp xs" and "x \ set xs" and "hd (stable_segment cmp x xs) = x" + \insort cmp x (remove1 x xs) = xs\ + if \sorted cmp xs\ and \x \ set xs\ and \hd (stable_segment cmp x xs) = x\ using that proof (induction xs) case Nil then show ?case by simp next case (Cons y ys) - then have "compare cmp x y \ Less" + then have \compare cmp x y \ Less\ by (auto simp add: compare.greater_iff_sym_less) - then consider "compare cmp x y = Greater" | "compare cmp x y = Equiv" - by (cases "compare cmp x y") auto + then consider \compare cmp x y = Greater\ | \compare cmp x y = Equiv\ + by (cases \compare cmp x y\) auto then show ?case proof cases case 1 with Cons.prems Cons.IH show ?thesis by auto next case 2 - with Cons.prems have "x = y" + with Cons.prems have \x = y\ by simp with Cons.hyps show ?thesis by (simp add: insort_eq_ConsI) @@ -247,8 +247,8 @@ qed lemma sorted_append_iff: - "sorted cmp (xs @ ys) \ sorted cmp xs \ sorted cmp ys - \ (\x \ set xs. \y \ set ys. compare cmp x y \ Greater)" (is "?P \ ?R \ ?S \ ?Q") + \sorted cmp (xs @ ys) \ sorted cmp xs \ sorted cmp ys + \ (\x \ set xs. \y \ set ys. compare cmp x y \ Greater)\ (is \?P \ ?R \ ?S \ ?Q\) proof assume ?P have ?R @@ -260,10 +260,10 @@ moreover have ?Q using \?P\ by (induction xs) (auto simp add: sorted_Cons_imp_not_less, simp add: sorted_Cons_imp_sorted) - ultimately show "?R \ ?S \ ?Q" + ultimately show \?R \ ?S \ ?Q\ by simp next - assume "?R \ ?S \ ?Q" + assume \?R \ ?S \ ?Q\ then have ?R ?S ?Q by simp_all then show ?P @@ -271,65 +271,65 @@ (auto simp add: append_eq_Cons_conv intro!: sorted_ConsI) qed -definition sort :: "'a comparator \ 'a list \ 'a list" - where "sort cmp xs = foldr (insort cmp) xs []" +definition sort :: \'a comparator \ 'a list \ 'a list\ + where \sort cmp xs = foldr (insort cmp) xs []\ lemma sort_simps [simp]: - "sort cmp [] = []" - "sort cmp (x # xs) = insort cmp x (sort cmp xs)" + \sort cmp [] = []\ + \sort cmp (x # xs) = insort cmp x (sort cmp xs)\ by (simp_all add: sort_def) lemma mset_sort [simp]: - "mset (sort cmp xs) = mset xs" + \mset (sort cmp xs) = mset xs\ by (induction xs) simp_all lemma length_sort [simp]: - "length (sort cmp xs) = length xs" + \length (sort cmp xs) = length xs\ by (induction xs) simp_all lemma sorted_sort [simp]: - "sorted cmp (sort cmp xs)" + \sorted cmp (sort cmp xs)\ by (induction xs) (simp_all add: sorted_insort) lemma stable_sort: - "stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs" + \stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs\ by (induction xs) (simp_all add: stable_insort_equiv stable_insort_not_equiv) lemma sort_remove1_eq [simp]: - "sort cmp (remove1 x xs) = remove1 x (sort cmp xs)" + \sort cmp (remove1 x xs) = remove1 x (sort cmp xs)\ by (induction xs) simp_all lemma set_insort [simp]: - "set (insort cmp x xs) = insert x (set xs)" + \set (insort cmp x xs) = insert x (set xs)\ by (induction xs) auto lemma set_sort [simp]: - "set (sort cmp xs) = set xs" + \set (sort cmp xs) = set xs\ by (induction xs) auto lemma sort_eqI: - "sort cmp ys = xs" - if permutation: "mset ys = mset xs" - and sorted: "sorted cmp xs" - and stable: "\y. y \ set ys \ - stable_segment cmp y ys = stable_segment cmp y xs" + \sort cmp ys = xs\ + if permutation: \mset ys = mset xs\ + and sorted: \sorted cmp xs\ + and stable: \\y. y \ set ys \ + stable_segment cmp y ys = stable_segment cmp y xs\ proof - - have stable': "stable_segment cmp y ys = - stable_segment cmp y xs" for y - proof (cases "\x\set ys. compare cmp y x = Equiv") + have stable': \stable_segment cmp y ys = + stable_segment cmp y xs\ for y + proof (cases \\x\set ys. compare cmp y x = Equiv\) case True - then obtain z where "z \ set ys" and "compare cmp y z = Equiv" + then obtain z where \z \ set ys\ and \compare cmp y z = Equiv\ by auto - then have "compare cmp y x = Equiv \ compare cmp z x = Equiv" for x + then have \compare cmp y x = Equiv \ compare cmp z x = Equiv\ for x by (meson compare.sym compare.trans_equiv) - moreover have "stable_segment cmp z ys = - stable_segment cmp z xs" + moreover have \stable_segment cmp z ys = + stable_segment cmp z xs\ using \z \ set ys\ by (rule stable) ultimately show ?thesis by simp next case False - moreover from permutation have "set ys = set xs" + moreover from permutation have \set ys = set xs\ by (rule mset_eq_setD) ultimately show ?thesis by simp @@ -341,40 +341,40 @@ by simp next case (minimum x xs) - from \mset ys = mset xs\ have ys: "set ys = set xs" + from \mset ys = mset xs\ have ys: \set ys = set xs\ by (rule mset_eq_setD) - then have "compare cmp x y \ Greater" if "y \ set ys" for y + then have \compare cmp x y \ Greater\ if \y \ set ys\ for y using that minimum.hyps by simp - from minimum.prems have stable: "stable_segment cmp x ys = stable_segment cmp x xs" + from minimum.prems have stable: \stable_segment cmp x ys = stable_segment cmp x xs\ by simp - have "sort cmp (remove1 x ys) = remove1 x xs" + have \sort cmp (remove1 x ys) = remove1 x xs\ by (rule minimum.IH) (simp_all add: minimum.prems filter_remove1) - then have "remove1 x (sort cmp ys) = remove1 x xs" + then have \remove1 x (sort cmp ys) = remove1 x xs\ by simp - then have "insort cmp x (remove1 x (sort cmp ys)) = - insort cmp x (remove1 x xs)" + then have \insort cmp x (remove1 x (sort cmp ys)) = + insort cmp x (remove1 x xs)\ by simp - also from minimum.hyps ys stable have "insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys" + also from minimum.hyps ys stable have \insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys\ by (simp add: stable_sort insort_remove1_same_eq) - also from minimum.hyps have "insort cmp x (remove1 x xs) = xs" + also from minimum.hyps have \insort cmp x (remove1 x xs) = xs\ by (simp add: insort_remove1_same_eq) finally show ?case . qed qed lemma filter_insort: - "filter P (insort cmp x xs) = insort cmp x (filter P xs)" - if "sorted cmp xs" and "P x" + \filter P (insort cmp x xs) = insort cmp x (filter P xs)\ + if \sorted cmp xs\ and \P x\ using that by (induction xs) (auto simp add: compare.trans_not_greater insort_eq_ConsI) lemma filter_insort_triv: - "filter P (insort cmp x xs) = filter P xs" - if "\ P x" + \filter P (insort cmp x xs) = filter P xs\ + if \\ P x\ using that by (induction xs) simp_all lemma filter_sort: - "filter P (sort cmp xs) = sort cmp (filter P xs)" + \filter P (sort cmp xs) = sort cmp (filter P xs)\ by (induction xs) (auto simp add: filter_insort filter_insort_triv) @@ -382,80 +382,80 @@ subsection \Quicksort\ -definition quicksort :: "'a comparator \ 'a list \ 'a list" - where quicksort_is_sort [simp]: "quicksort = sort" +definition quicksort :: \'a comparator \ 'a list \ 'a list\ + where quicksort_is_sort [simp]: \quicksort = sort\ lemma sort_by_quicksort: - "sort = quicksort" + \sort = quicksort\ by simp lemma sort_by_quicksort_rec: - "sort cmp xs = sort cmp [x\xs. compare cmp x (xs ! (length xs div 2)) = Less] + \sort cmp xs = sort cmp [x\xs. compare cmp x (xs ! (length xs div 2)) = Less] @ stable_segment cmp (xs ! (length xs div 2)) xs - @ sort cmp [x\xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "_ = ?rhs") + @ sort cmp [x\xs. compare cmp x (xs ! (length xs div 2)) = Greater]\ (is \_ = ?rhs\) proof (rule sort_eqI) - show "mset xs = mset ?rhs" + show \mset xs = mset ?rhs\ by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust) next - show "sorted cmp ?rhs" + show \sorted cmp ?rhs\ by (auto simp add: sorted_append_iff sorted_stable_segment compare.equiv_subst_right dest: compare.trans_greater) next - let ?pivot = "xs ! (length xs div 2)" + let ?pivot = \xs ! (length xs div 2)\ fix l - have "compare cmp x ?pivot = comp \ compare cmp l x = Equiv - \ compare cmp l ?pivot = comp \ compare cmp l x = Equiv" for x comp + have \compare cmp x ?pivot = comp \ compare cmp l x = Equiv + \ compare cmp l ?pivot = comp \ compare cmp l x = Equiv\ for x comp proof - - have "compare cmp x ?pivot = comp \ compare cmp l ?pivot = comp" - if "compare cmp l x = Equiv" + have \compare cmp x ?pivot = comp \ compare cmp l ?pivot = comp\ + if \compare cmp l x = Equiv\ using that by (simp add: compare.equiv_subst_left compare.sym) then show ?thesis by blast qed - then show "stable_segment cmp l xs = stable_segment cmp l ?rhs" + then show \stable_segment cmp l xs = stable_segment cmp l ?rhs\ by (simp add: stable_sort compare.sym [of _ ?pivot]) - (cases "compare cmp l ?pivot", simp_all) + (cases \compare cmp l ?pivot\, simp_all) qed context begin -qualified definition partition :: "'a comparator \ 'a \ 'a list \ 'a list \ 'a list \ 'a list" - where "partition cmp pivot xs = - ([x \ xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \ xs. compare cmp x pivot = Greater])" +qualified definition partition :: \'a comparator \ 'a \ 'a list \ 'a list \ 'a list \ 'a list\ + where \partition cmp pivot xs = + ([x \ xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \ xs. compare cmp x pivot = Greater])\ qualified lemma partition_code [code]: - "partition cmp pivot [] = ([], [], [])" - "partition cmp pivot (x # xs) = + \partition cmp pivot [] = ([], [], [])\ + \partition cmp pivot (x # xs) = (let (lts, eqs, gts) = partition cmp pivot xs in case compare cmp x pivot of Less \ (x # lts, eqs, gts) | Equiv \ (lts, x # eqs, gts) - | Greater \ (lts, eqs, x # gts))" + | Greater \ (lts, eqs, x # gts))\ using comp.exhaust by (auto simp add: partition_def Let_def compare.sym [of _ pivot]) lemma quicksort_code [code]: - "quicksort cmp xs = + \quicksort cmp xs = (case xs of [] \ [] | [x] \ xs | [x, y] \ (if compare cmp x y \ Greater then xs else [y, x]) | _ \ let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs - in quicksort cmp lts @ eqs @ quicksort cmp gts)" -proof (cases "length xs \ 3") + in quicksort cmp lts @ eqs @ quicksort cmp gts)\ +proof (cases \length xs \ 3\) case False - then have "length xs \ {0, 1, 2}" + then have \length xs \ {0, 1, 2}\ by (auto simp add: not_le le_less less_antisym) - then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]" + then consider \xs = []\ | x where \xs = [x]\ | x y where \xs = [x, y]\ by (auto simp add: length_Suc_conv numeral_2_eq_2) then show ?thesis by cases simp_all next case True - then obtain x y z zs where "xs = x # y # z # zs" + then obtain x y z zs where \xs = x # y # z # zs\ by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3) - moreover have "quicksort cmp xs = + moreover have \quicksort cmp xs = (let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs - in quicksort cmp lts @ eqs @ quicksort cmp gts)" + in quicksort cmp lts @ eqs @ quicksort cmp gts)\ using sort_by_quicksort_rec [of cmp xs] by (simp add: partition_def) ultimately show ?thesis by simp @@ -466,38 +466,38 @@ subsection \Mergesort\ -definition mergesort :: "'a comparator \ 'a list \ 'a list" - where mergesort_is_sort [simp]: "mergesort = sort" +definition mergesort :: \'a comparator \ 'a list \ 'a list\ + where mergesort_is_sort [simp]: \mergesort = sort\ lemma sort_by_mergesort: - "sort = mergesort" + \sort = mergesort\ by simp context - fixes cmp :: "'a comparator" + fixes cmp :: \'a comparator\ begin -qualified function merge :: "'a list \ 'a list \ 'a list" - where "merge [] ys = ys" - | "merge xs [] = xs" - | "merge (x # xs) (y # ys) = (if compare cmp x y = Greater - then y # merge (x # xs) ys else x # merge xs (y # ys))" +qualified function merge :: \'a list \ 'a list \ 'a list\ + where \merge [] ys = ys\ + | \merge xs [] = xs\ + | \merge (x # xs) (y # ys) = (if compare cmp x y = Greater + then y # merge (x # xs) ys else x # merge xs (y # ys))\ by pat_completeness auto qualified termination by lexicographic_order lemma mset_merge: - "mset (merge xs ys) = mset xs + mset ys" + \mset (merge xs ys) = mset xs + mset ys\ by (induction xs ys rule: merge.induct) simp_all lemma merge_eq_Cons_imp: - "xs \ [] \ z = hd xs \ ys \ [] \ z = hd ys" - if "merge xs ys = z # zs" + \xs \ [] \ z = hd xs \ ys \ [] \ z = hd ys\ + if \merge xs ys = z # zs\ using that by (induction xs ys rule: merge.induct) (auto split: if_splits) lemma filter_merge: - "filter P (merge xs ys) = merge (filter P xs) (filter P ys)" - if "sorted cmp xs" and "sorted cmp ys" + \filter P (merge xs ys) = merge (filter P xs) (filter P ys)\ + if \sorted cmp xs\ and \sorted cmp ys\ using that proof (induction xs ys rule: merge.induct) case (1 ys) then show ?case @@ -509,47 +509,47 @@ next case (3 x xs y ys) show ?case - proof (cases "compare cmp x y = Greater") + proof (cases \compare cmp x y = Greater\) case True - with 3 have hyp: "filter P (merge (x # xs) ys) = - merge (filter P (x # xs)) (filter P ys)" + with 3 have hyp: \filter P (merge (x # xs) ys) = + merge (filter P (x # xs)) (filter P ys)\ by (simp add: sorted_Cons_imp_sorted) show ?thesis - proof (cases "\ P x \ P y") + proof (cases \\ P x \ P y\) case False with \compare cmp x y = Greater\ show ?thesis by (auto simp add: hyp) next case True from \compare cmp x y = Greater\ "3.prems" - have *: "compare cmp z y = Greater" if "z \ set (filter P xs)" for z + have *: \compare cmp z y = Greater\ if \z \ set (filter P xs)\ for z using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less) from \compare cmp x y = Greater\ show ?thesis - by (cases "filter P xs") (simp_all add: hyp *) + by (cases \filter P xs\) (simp_all add: hyp *) qed next case False - with 3 have hyp: "filter P (merge xs (y # ys)) = - merge (filter P xs) (filter P (y # ys))" + with 3 have hyp: \filter P (merge xs (y # ys)) = + merge (filter P xs) (filter P (y # ys))\ by (simp add: sorted_Cons_imp_sorted) show ?thesis - proof (cases "P x \ \ P y") + proof (cases \P x \ \ P y\) case False with \compare cmp x y \ Greater\ show ?thesis by (auto simp add: hyp) next case True from \compare cmp x y \ Greater\ "3.prems" - have *: "compare cmp x z \ Greater" if "z \ set (filter P ys)" for z + have *: \compare cmp x z \ Greater\ if \z \ set (filter P ys)\ for z using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less) from \compare cmp x y \ Greater\ show ?thesis - by (cases "filter P ys") (simp_all add: hyp *) + by (cases \filter P ys\) (simp_all add: hyp *) qed qed qed lemma sorted_merge: - "sorted cmp (merge xs ys)" if "sorted cmp xs" and "sorted cmp ys" + \sorted cmp (merge xs ys)\ if \sorted cmp xs\ and \sorted cmp ys\ using that proof (induction xs ys rule: merge.induct) case (1 ys) then show ?case @@ -561,15 +561,15 @@ next case (3 x xs y ys) show ?case - proof (cases "compare cmp x y = Greater") + proof (cases \compare cmp x y = Greater\) case True - with 3 have "sorted cmp (merge (x # xs) ys)" + with 3 have \sorted cmp (merge (x # xs) ys)\ by (simp add: sorted_Cons_imp_sorted) - then have "sorted cmp (y # merge (x # xs) ys)" + then have \sorted cmp (y # merge (x # xs) ys)\ proof (rule sorted_ConsI) fix z zs - assume "merge (x # xs) ys = z # zs" - with 3(4) True show "compare cmp y z \ Greater" + assume \merge (x # xs) ys = z # zs\ + with 3(4) True show \compare cmp y z \ Greater\ by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp) (auto simp add: compare.asym_greater sorted_Cons_imp_not_less) qed @@ -577,13 +577,13 @@ by simp next case False - with 3 have "sorted cmp (merge xs (y # ys))" + with 3 have \sorted cmp (merge xs (y # ys))\ by (simp add: sorted_Cons_imp_sorted) - then have "sorted cmp (x # merge xs (y # ys))" + then have \sorted cmp (x # merge xs (y # ys))\ proof (rule sorted_ConsI) fix z zs - assume "merge xs (y # ys) = z # zs" - with 3(3) False show "compare cmp x z \ Greater" + assume \merge xs (y # ys) = z # zs\ + with 3(3) False show \compare cmp x z \ Greater\ by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp) (auto simp add: compare.asym_greater sorted_Cons_imp_not_less) qed @@ -593,45 +593,45 @@ qed lemma merge_eq_appendI: - "merge xs ys = xs @ ys" - if "\x y. x \ set xs \ y \ set ys \ compare cmp x y \ Greater" + \merge xs ys = xs @ ys\ + if \\x y. x \ set xs \ y \ set ys \ compare cmp x y \ Greater\ using that by (induction xs ys rule: merge.induct) simp_all lemma merge_stable_segments: - "merge (stable_segment cmp l xs) (stable_segment cmp l ys) = - stable_segment cmp l xs @ stable_segment cmp l ys" + \merge (stable_segment cmp l xs) (stable_segment cmp l ys) = + stable_segment cmp l xs @ stable_segment cmp l ys\ by (rule merge_eq_appendI) (auto dest: compare.trans_equiv_greater) lemma sort_by_mergesort_rec: - "sort cmp xs = + \sort cmp xs = merge (sort cmp (take (length xs div 2) xs)) - (sort cmp (drop (length xs div 2) xs))" (is "_ = ?rhs") + (sort cmp (drop (length xs div 2) xs))\ (is \_ = ?rhs\) proof (rule sort_eqI) - have "mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) = - mset (take (length xs div 2) xs @ drop (length xs div 2) xs)" + have \mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) = + mset (take (length xs div 2) xs @ drop (length xs div 2) xs)\ by (simp only: mset_append) - then show "mset xs = mset ?rhs" + then show \mset xs = mset ?rhs\ by (simp add: mset_merge) next - show "sorted cmp ?rhs" + show \sorted cmp ?rhs\ by (simp add: sorted_merge) next fix l - have "stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs) - = stable_segment cmp l xs" + have \stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs) + = stable_segment cmp l xs\ by (simp only: filter_append [symmetric] append_take_drop_id) - have "merge (stable_segment cmp l (take (length xs div 2) xs)) + have \merge (stable_segment cmp l (take (length xs div 2) xs)) (stable_segment cmp l (drop (length xs div 2) xs)) = - stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)" + stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)\ by (rule merge_eq_appendI) (auto simp add: compare.trans_equiv_greater) - also have "\ = stable_segment cmp l xs" + also have \\ = stable_segment cmp l xs\ by (simp only: filter_append [symmetric] append_take_drop_id) - finally show "stable_segment cmp l xs = stable_segment cmp l ?rhs" + finally show \stable_segment cmp l xs = stable_segment cmp l ?rhs\ by (simp add: stable_sort filter_merge) qed lemma mergesort_code [code]: - "mergesort cmp xs = + \mergesort cmp xs = (case xs of [] \ [] | [x] \ xs @@ -641,25 +641,25 @@ half = length xs div 2; ys = take half xs; zs = drop half xs - in merge (mergesort cmp ys) (mergesort cmp zs))" -proof (cases "length xs \ 3") + in merge (mergesort cmp ys) (mergesort cmp zs))\ +proof (cases \length xs \ 3\) case False - then have "length xs \ {0, 1, 2}" + then have \length xs \ {0, 1, 2}\ by (auto simp add: not_le le_less less_antisym) - then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]" + then consider \xs = []\ | x where \xs = [x]\ | x y where \xs = [x, y]\ by (auto simp add: length_Suc_conv numeral_2_eq_2) then show ?thesis by cases simp_all next case True - then obtain x y z zs where "xs = x # y # z # zs" + then obtain x y z zs where \xs = x # y # z # zs\ by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3) - moreover have "mergesort cmp xs = + moreover have \mergesort cmp xs = (let half = length xs div 2; ys = take half xs; zs = drop half xs - in merge (mergesort cmp ys) (mergesort cmp zs))" + in merge (mergesort cmp ys) (mergesort cmp zs))\ using sort_by_mergesort_rec [of xs] by (simp add: Let_def) ultimately show ?thesis by simp @@ -667,4 +667,89 @@ end + +subsection \Lexicographic products\ + +lemma sorted_prod_lex_imp_sorted_fst: + \sorted (key fst cmp1) ps\ if \sorted (prod_lex cmp1 cmp2) ps\ +using that proof (induction rule: sorted_induct) + case Nil + then show ?case + by simp +next + case (Cons p ps) + have \compare (key fst cmp1) p q \ Greater\ if \ps = q # qs\ for q qs + using that Cons.hyps(2) [of q] by (simp add: compare_prod_lex_apply split: comp.splits) + with Cons.IH show ?case + by (rule sorted_ConsI) simp +qed + +lemma sorted_prod_lex_imp_sorted_snd: + \sorted (key snd cmp2) ps\ if \sorted (prod_lex cmp1 cmp2) ps\ \\a' b'. (a', b') \ set ps \ compare cmp1 a a' = Equiv\ +using that proof (induction rule: sorted_induct) + case Nil + then show ?case + by simp +next + case (Cons p ps) + then show ?case + apply (cases p) + apply (rule sorted_ConsI) + apply (simp_all add: compare_prod_lex_apply) + apply (auto cong del: comp.case_cong_weak) + apply (metis comp.simps(8) compare.equiv_subst_left) + done +qed + +lemma sort_comp_fst_snd_eq_sort_prod_lex: + \sort (key fst cmp1) \ sort (key snd cmp2) = sort (prod_lex cmp1 cmp2)\ (is \sort ?cmp1 \ sort ?cmp2 = sort ?cmp\) +proof + fix ps :: \('a \ 'b) list\ + have \sort ?cmp1 (sort ?cmp2 ps) = sort ?cmp ps\ + proof (rule sort_eqI) + show \mset (sort ?cmp2 ps) = mset (sort ?cmp ps)\ + by simp + show \sorted ?cmp1 (sort ?cmp ps)\ + by (rule sorted_prod_lex_imp_sorted_fst [of _ cmp2]) simp + next + fix p :: \'a \ 'b\ + define a b where ab: \a = fst p\ \b = snd p\ + moreover assume \p \ set (sort ?cmp2 ps)\ + ultimately have \(a, b) \ set (sort ?cmp2 ps)\ + by simp + let ?qs = \filter (\(a', _). compare cmp1 a a' = Equiv) ps\ + have \sort ?cmp2 ?qs = sort ?cmp ?qs\ + proof (rule sort_eqI) + show \mset ?qs = mset (sort ?cmp ?qs)\ + by simp + show \sorted ?cmp2 (sort ?cmp ?qs)\ + by (rule sorted_prod_lex_imp_sorted_snd) auto + next + fix q :: \'a \ 'b\ + define c d where \c = fst q\ \d = snd q\ + moreover assume \q \ set ?qs\ + ultimately have \(c, d) \ set ?qs\ + by simp + from sorted_stable_segment [of ?cmp \(a, d)\ ps] + have \sorted ?cmp (filter (\(c, b). compare (prod_lex cmp1 cmp2) (a, d) (c, b) = Equiv) ps)\ + by (simp only: case_prod_unfold prod.collapse) + also have \(\(c, b). compare (prod_lex cmp1 cmp2) (a, d) (c, b) = Equiv) = + (\(c, b). compare cmp1 a c = Equiv \ compare cmp2 d b = Equiv)\ + by (simp add: fun_eq_iff compare_prod_lex_apply split: comp.split) + finally have *: \sorted ?cmp (filter (\(c, b). compare cmp1 a c = Equiv \ compare cmp2 d b = Equiv) ps)\ . + let ?rs = \filter (\(_, d'). compare cmp2 d d' = Equiv) ?qs\ + have \sort ?cmp ?rs = ?rs\ + by (rule sort_eqI) (use * in \simp_all add: case_prod_unfold\) + then show \filter (\r. compare ?cmp2 q r = Equiv) ?qs = + filter (\r. compare ?cmp2 q r = Equiv) (sort ?cmp ?qs)\ + by (simp add: filter_sort case_prod_unfold flip: \d = snd q\) + qed + then show \filter (\q. compare ?cmp1 p q = Equiv) (sort ?cmp2 ps) = + filter (\q. compare ?cmp1 p q = Equiv) (sort ?cmp ps)\ + by (simp add: filter_sort case_prod_unfold flip: ab) + qed + then show \(sort (key fst cmp1) \ sort (key snd cmp2)) ps = sort (prod_lex cmp1 cmp2) ps\ + by simp +qed + end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Tools/lazy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Tools/lazy.ML Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,46 @@ +(* Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset *) + +signature LAZY = +sig + type 'a lazy; + val lazy : (unit -> 'a) -> 'a lazy; + val force : 'a lazy -> 'a; + val peek : 'a lazy -> 'a option + val termify_lazy : + (string -> 'typerep -> 'term) -> + ('term -> 'term -> 'term) -> + (string -> 'typerep -> 'term -> 'term) -> + 'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) -> + ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term; +end; + +structure Lazy : LAZY = +struct + +datatype 'a content = + Delay of unit -> 'a + | Value of 'a + | Exn of exn; + +datatype 'a lazy = Lazy of 'a content ref; + +fun lazy f = Lazy (ref (Delay f)); + +fun force (Lazy x) = case !x of + Delay f => ( + let val res = f (); val _ = x := Value res; in res end + handle exn => (x := Exn exn; raise exn)) + | Value x => x + | Exn exn => raise exn; + +fun peek (Lazy x) = case !x of + Value x => SOME x + | _ => NONE; + +fun termify_lazy const app abs unitT funT lazyT term_of T x _ = + app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T))) + (case peek x of SOME y => abs "_" unitT (term_of y) + | _ => const "Pure.dummy_pattern" (funT unitT T)); + +end; diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Tools/lazy.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Tools/lazy.hs Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,8 @@ +{- Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset -} + +module Lazy(Lazy, delay, force) where + +newtype Lazy a = Lazy a +delay f = Lazy (f ()) +force (Lazy x) = x diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Tools/lazy.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Tools/lazy.scala Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,39 @@ +/* Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset */ + +object Lazy { + final class Lazy[A] (f: Unit => A) { + var evaluated = false; + lazy val x: A = f(()) + + def get() : A = { + evaluated = true; + return x + } + } + + def force[A] (x: Lazy[A]) : A = { + return x.get() + } + + def delay[A] (f: Unit => A) : Lazy[A] = { + return new Lazy[A] (f) + } + + def termify_lazy[Typerep, Term, A] ( + const: String => Typerep => Term, + app: Term => Term => Term, + abs: String => Typerep => Term => Term, + unitT: Typerep, + funT: Typerep => Typerep => Typerep, + lazyT: Typerep => Typerep, + term_of: A => Term, + ty: Typerep, + x: Lazy[A], + dummy: Term) : Term = { + x.evaluated match { + case true => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get()))) + case false => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty))) + } + } +} diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Tools/termify_lazy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Tools/termify_lazy.ML Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,16 @@ +(* Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset *) + +structure Termify_Lazy = +struct + +fun termify_lazy + (_: string -> typ -> term) (_: term -> term -> term) (_: string -> typ -> term -> term) + (_: typ) (_: typ -> typ -> typ) (_: typ -> typ) + (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) = + Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $ + (case Lazy.peek x of + SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x) + | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T)); + +end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Tools/termify_lazy.ocaml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Tools/termify_lazy.ocaml Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,18 @@ +(* Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset *) + +module Termify_Lazy : sig + val termify_lazy : + (string -> 'typerep -> 'term) -> + ('term -> 'term -> 'term) -> + (string -> 'typerep -> 'term -> 'term) -> + 'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) -> + ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term +end = struct + +let termify_lazy const app abs unitT funT lazyT term_of ty x _ = + app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty))) + (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x)) + else const "Pure.dummy_pattern" (funT unitT ty));; + +end;; diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Tools/word_lib.ML --- a/src/HOL/Library/Tools/word_lib.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Library/Tools/word_lib.ML Fri Apr 04 22:20:30 2025 +0200 @@ -35,7 +35,7 @@ then Type (\<^type_name>\Numeral_Type.bit0\, [T]) else Type (\<^type_name>\Numeral_Type.bit1\, [T]) -fun mk_binT size = +fun mk_binT size = if size = 0 then \<^typ>\Numeral_Type.num0\ else if size = 1 then \<^typ>\Numeral_Type.num1\ else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Library/Word.thy Fri Apr 04 22:20:30 2025 +0200 @@ -475,9 +475,10 @@ by (rule; transfer) simp lemma [code]: - \Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\ + \Word.the_signed_int w = (let k = Word.the_int w + in if bit k (LENGTH('a) - Suc 0) then k + push_bit LENGTH('a) (- 1) else k)\ for w :: \'a::len word\ - by transfer (simp add: signed_take_bit_take_bit) + by transfer (simp add: bit_simps signed_take_bit_eq_take_bit_add) lemma [code_abbrev, simp]: \Word.the_signed_int = sint\ @@ -1629,6 +1630,67 @@ subsection \Ordering\ +instance word :: (len) wellorder +proof + fix P :: "'a word \ bool" and a + assume *: "(\b. (\a. a < b \ P a) \ P b)" + have "wf (measure unat)" .. + moreover have "{(a, b :: ('a::len) word). a < b} \ measure unat" + by (auto simp add: word_less_iff_unsigned [where ?'a = nat]) + ultimately have "wf {(a, b :: ('a::len) word). a < b}" + by (rule wf_subset) + then show "P a" using * + by induction blast +qed + +lemma word_m1_ge [simp]: (* FIXME: delete *) + "word_pred 0 \ y" + by transfer (simp add: mask_eq_exp_minus_1) + +lemma word_less_alt: + "a < b \ uint a < uint b" + by (fact word_less_def) + +lemma word_zero_le [simp]: + "0 \ y" for y :: "'a::len word" + by (fact word_coorder.extremum) + +lemma word_n1_ge [simp]: + "y \ - 1" for y :: "'a::len word" + by (fact word_order.extremum) + +lemmas word_not_simps [simp] = + word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] + +lemma word_gt_0: + "0 < y \ 0 \ y" + for y :: "'a::len word" + by (simp add: less_le) + +lemma word_gt_0_no [simp]: + \(0 :: 'a::len word) < numeral y \ (0 :: 'a::len word) \ numeral y\ + by (fact word_gt_0) + +lemma word_le_nat_alt: + "a \ b \ unat a \ unat b" + by transfer (simp add: nat_le_eq_zle) + +lemma word_less_nat_alt: + "a < b \ unat a < unat b" + by transfer (auto simp: less_le [of 0]) + +lemmas unat_mono = word_less_nat_alt [THEN iffD1] + +lemma wi_less: + "(word_of_int n < (word_of_int m :: 'a::len word)) = + (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" + by (simp add: uint_word_of_int word_less_def) + +lemma wi_le: + "(word_of_int n \ (word_of_int m :: 'a::len word)) = + (n mod 2 ^ LENGTH('a) \ m mod 2 ^ LENGTH('a))" + by (simp add: uint_word_of_int word_le_def) + lift_definition word_sle :: \'a::len word \ 'a word \ bool\ is \\k l. signed_take_bit (LENGTH('a) - Suc 0) k \ signed_take_bit (LENGTH('a) - Suc 0) l\ by (simp flip: signed_take_bit_decr_length_iff) @@ -1650,13 +1712,12 @@ \a <=s b \ sint a \ sint b\ by transfer simp -lemma [code]: - \a sint a < sint b\ +lemma word_sless_alt [code]: + "a sint a < sint b" by transfer simp lemma signed_ordering: \ordering word_sle word_sless\ - apply (standard; transfer) - using signed_take_bit_decr_length_iff by force+ + by (standard; transfer) (auto simp flip: signed_take_bit_decr_length_iff) lemma signed_linorder: \class.linorder word_sle word_sless\ by (standard; transfer) (auto simp: signed_take_bit_decr_length_iff) @@ -1668,63 +1729,6 @@ \x x <=s y \ x \ y\ by (fact signed.less_le) -lemma word_less_alt: "a < b \ uint a < uint b" - by (fact word_less_def) - -lemma word_zero_le [simp]: "0 \ y" - for y :: "'a::len word" - by (fact word_coorder.extremum) - -lemma word_m1_ge [simp] : "word_pred 0 \ y" (* FIXME: delete *) - by transfer (simp add: mask_eq_exp_minus_1) - -lemma word_n1_ge [simp]: "y \ -1" - for y :: "'a::len word" - by (fact word_order.extremum) - -lemmas word_not_simps [simp] = - word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] - -lemma word_gt_0: "0 < y \ 0 \ y" - for y :: "'a::len word" - by (simp add: less_le) - -lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y - -lemma word_sless_alt: "a sint a < sint b" - by transfer simp - -lemma word_le_nat_alt: "a \ b \ unat a \ unat b" - by transfer (simp add: nat_le_eq_zle) - -lemma word_less_nat_alt: "a < b \ unat a < unat b" - by transfer (auto simp: less_le [of 0]) - -lemmas unat_mono = word_less_nat_alt [THEN iffD1] - -instance word :: (len) wellorder -proof - fix P :: "'a word \ bool" and a - assume *: "(\b. (\a. a < b \ P a) \ P b)" - have "wf (measure unat)" .. - moreover have "{(a, b :: ('a::len) word). a < b} \ measure unat" - by (auto simp: word_less_nat_alt) - ultimately have "wf {(a, b :: ('a::len) word). a < b}" - by (rule wf_subset) - then show "P a" using * - by induction blast -qed - -lemma wi_less: - "(word_of_int n < (word_of_int m :: 'a::len word)) = - (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" - by (simp add: uint_word_of_int word_less_def) - -lemma wi_le: - "(word_of_int n \ (word_of_int m :: 'a::len word)) = - (n mod 2 ^ LENGTH('a) \ m mod 2 ^ LENGTH('a))" - by (simp add: uint_word_of_int word_le_def) - subsection \Bit-wise operations\ diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/List.thy --- a/src/HOL/List.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/List.thy Fri Apr 04 22:20:30 2025 +0200 @@ -8156,7 +8156,7 @@ fun print_list (target_fxy, target_cons) pr fxy t1 t2 = Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy ( pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1, - Code_Printer.str target_cons, + Pretty.str target_cons, pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2 ); diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Apr 04 22:20:30 2025 +0200 @@ -148,7 +148,7 @@ let val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) in - case Try0.try0 (SOME (seconds 5.0)) [] state of + case Try0.try0 (SOME (seconds 5.0)) Try0.empty_facts state of [] => (Unsolved, []) | _ => (Solved, []) end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Nat.thy Fri Apr 04 22:20:30 2025 +0200 @@ -1986,7 +1986,7 @@ ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") = \K (try o Nat_Arith.cancel_diff_conv)\ -context order +context preorder begin lemma lift_Suc_mono_le: @@ -1996,7 +1996,7 @@ proof (cases "n < n'") case True then show ?thesis - by (induct n n' rule: less_Suc_induct) (auto intro: mono) + by (induct n n' rule: less_Suc_induct) (auto intro: mono order.trans) next case False with \n \ n'\ show ?thesis by auto @@ -2009,7 +2009,7 @@ proof (cases "n < n'") case True then show ?thesis - by (induct n n' rule: less_Suc_induct) (auto intro: mono) + by (induct n n' rule: less_Suc_induct) (auto intro: mono order.trans) next case False with \n \ n'\ show ?thesis by auto @@ -2019,7 +2019,7 @@ assumes mono: "\n. f n < f (Suc n)" and "n < n'" shows "f n < f n'" - using \n < n'\ by (induct n n' rule: less_Suc_induct) (auto intro: mono) + using \n < n'\ by (induct n n' rule: less_Suc_induct) (auto intro: mono order.strict_trans) lemma lift_Suc_mono_less_iff: "(\n. f n < f (Suc n)) \ f n < f m \ n < m" by (blast intro: less_asym' lift_Suc_mono_less [of f] diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/NthRoot.thy Fri Apr 04 22:20:30 2025 +0200 @@ -548,16 +548,14 @@ lemma not_real_square_gt_zero [simp]: "\ 0 < x * x \ x = 0" for x :: real - apply auto - using linorder_less_linear [where x = x and y = 0] - apply (simp add: zero_less_mult_iff) - done + by (metis linorder_neq_iff zero_less_mult_iff) lemma real_sqrt_abs2 [simp]: "sqrt (x * x) = \x\" - apply (subst power2_eq_square [symmetric]) - apply (rule real_sqrt_abs) - done + by (simp add: real_sqrt_mult) +lemma real_sqrt_abs': "sqrt \x\ = \sqrt x\" + by (metis real_sqrt_abs2 real_sqrt_mult) + lemma real_inv_sqrt_pow2: "0 < x \ (inverse (sqrt x))\<^sup>2 = inverse x" by (simp add: power_inverse) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Presburger.thy Fri Apr 04 22:20:30 2025 +0200 @@ -6,7 +6,6 @@ theory Presburger imports Groebner_Basis Set_Interval -keywords "try0" :: diag begin ML_file \Tools/Qelim/qelim.ML\ @@ -558,9 +557,4 @@ "n mod 4 = Suc 0 \ even ((n - Suc 0) div 2)" by presburger - -subsection \Try0\ - -ML_file \Tools/try0.ML\ - end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Sledgehammer.thy Fri Apr 04 22:20:30 2025 +0200 @@ -7,7 +7,15 @@ section \Sledgehammer: Isabelle--ATP Linkup\ theory Sledgehammer -imports Presburger SMT + imports + \ \FIXME: \<^theory>\HOL.Try0_HOL\ has to be imported first so that @{attribute try0_schedule} gets + the value assigned value there. Otherwise, the value is the one assigned in \<^theory>\HOL.Try0\, + which is imported transitively by both \<^theory>\HOL.Presburger\ and \<^theory>\HOL.SMT\. It seems + that, when merging the attributes from two theories, the value assigned int the leftmost theory + has precedence.\ + Try0_HOL + Presburger + SMT keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Apr 04 22:20:30 2025 +0200 @@ -1935,8 +1935,7 @@ map_filter (try (specialize_helper t)) types else [t]) - |> tag_list 1 - |> map (fn (k, t) => ((dub needs_sound j k, (Global, status)), t)) + |> map_index (fn (k, t) => ((dub needs_sound j (k + 1), (Global, status)), t)) fun make_facts type_enc = map_filter (make_fact ctxt format type_enc false) val sound = is_type_enc_sound type_enc val could_specialize = could_specialize_helpers type_enc diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Apr 04 22:20:30 2025 +0200 @@ -216,7 +216,7 @@ end -val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) [] +val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) Try0.empty_facts fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) = let diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri Apr 04 22:20:30 2025 +0200 @@ -12,9 +12,10 @@ fun make_action ({timeout, ...} : Mirabelle.action_context) = let val generous_timeout = Time.scale 10.0 timeout + val try0 = Try0.try0 (SOME timeout) Try0.empty_facts fun run ({pre, ...} : Mirabelle.command) = - if Timeout.apply generous_timeout (not o null o Try0.try0 (SOME timeout) []) pre then + if Timeout.apply generous_timeout (not o null o try0) pre then "succeeded" else "" diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Nunchaku/nunchaku_commands.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Apr 04 22:20:30 2025 +0200 @@ -246,7 +246,7 @@ fun run_chaku override_params mode i state0 = let - val state = Proof.map_contexts (Try0.silence_methods false) state0; + val state = Proof.map_contexts Try0_HOL.silence_methods state0; val thy = Proof.theory_of state; val ctxt = Proof.context_of state; val _ = List.app check_raw_param override_params; diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/SMT/verit_isar.ML --- a/src/HOL/Tools/SMT/verit_isar.ML Fri Apr 04 22:20:23 2025 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -(* Title: HOL/Tools/SMT/verit_isar.ML - Author: Mathias Fleury, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - -VeriT proofs as generic ATP proofs for Isar proof reconstruction. -*) - -signature VERIT_ISAR = -sig - type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term -> - (string * term) list -> int list -> int -> (int * string) list -> Verit_Proof.veriT_step list -> - (term, string) ATP_Proof.atp_step list -end; - -structure VeriT_Isar: VERIT_ISAR = -struct - -open ATP_Util -open ATP_Problem -open ATP_Proof -open ATP_Proof_Reconstruct -open SMTLIB_Interface -open SMTLIB_Isar -open Verit_Proof - -fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids - conjecture_id fact_helper_ids = - let - fun steps_of (Verit_Proof.VeriT_Step {id, rule, prems, concl, ...}) = - let - val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl - fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems) - in - if rule = input_rule then - let - val id_num = snd (SMTLIB_Interface.role_and_index_of_assert_name id) - val ss = the_list (AList.lookup (op =) fact_helper_ids id_num) - in - (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids - fact_helper_ts hyp_ts concl_t of - NONE => [] - | SOME (role0, concl00) => - let - val name0 = (id ^ "a", ss) - val concl0 = unskolemize_names ctxt concl00 - in - [(name0, role0, concl0, rule, []), - ((id, []), Plain, concl', rewrite_rule, - name0 :: normalizing_prems ctxt concl0)] - end) - end - else - [standard_step (if null prems then Lemma else Plain)] - end - in - maps steps_of - end - -end; diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/SMT/verit_proof_parse.ML --- a/src/HOL/Tools/SMT/verit_proof_parse.ML Fri Apr 04 22:20:23 2025 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -(* Title: HOL/Tools/SMT/verit_proof_parse.ML - Author: Mathias Fleury, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - -VeriT proof parsing. -*) - -signature VERIT_PROOF_PARSE = -sig - type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - val parse_proof: SMT_Translate.replay_data -> - ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> - SMT_Solver.parsed_proof -end; - -structure VeriT_Proof_Parse: VERIT_PROOF_PARSE = -struct - -open ATP_Util -open ATP_Problem -open ATP_Proof -open ATP_Proof_Reconstruct -open VeriT_Isar -open Verit_Proof - -fun add_used_asserts_in_step (Verit_Proof.VeriT_Step {prems, ...}) = - union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems) - -fun parse_proof - ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) - xfacts prems concl output = - let - val num_ll_defs = length ll_defs - - val id_of_index = Integer.add num_ll_defs - val index_of_id = Integer.add (~ num_ll_defs) - - fun step_of_assume j ((_, role), th) = - Verit_Proof.VeriT_Step - {id = SMTLIB_Interface.assert_name_of_role_and_index role (id_of_index j), - rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []} - - val (actual_steps, _) = Verit_Proof.parse typs terms output ctxt - val used_assert_ids = fold add_used_asserts_in_step actual_steps [] - val used_assm_js = - map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end) - used_assert_ids - val used_assms = map (nth assms) used_assm_js - val assm_steps = map2 step_of_assume used_assm_js used_assms - val steps = assm_steps @ actual_steps - - val conjecture_i = 0 - val prems_i = conjecture_i + 1 - val num_prems = length prems - val facts_i = prems_i + num_prems - val num_facts = length xfacts - val helpers_i = facts_i + num_facts - - val conjecture_id = id_of_index conjecture_i - val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1) - val fact_ids' = - map_filter (fn j => - let val ((i, _), _) = nth assms j in - try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) - end) used_assm_js - val helper_ids' = - map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms - - val fact_helper_ts = - map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @ - map (fn (_, ((s, _), th)) => (s, Thm.prop_of th)) fact_ids' - val fact_helper_ids' = - map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids' - in - {outcome = NONE, fact_ids = SOME fact_ids', - atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl - fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps} - end - -end; diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Apr 04 22:20:30 2025 +0200 @@ -175,8 +175,8 @@ () fun print_used_facts used_facts used_from = - tag_list 1 used_from - |> map (fn (j, fact) => fact |> apsnd (K j)) + used_from + |> map_index (fn (j, fact) => fact |> apsnd (K (j + 1))) |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas @@ -188,8 +188,8 @@ val num_used_facts = length used_facts fun find_indices facts = - tag_list 1 facts - |> map (fn (j, fact) => fact |> apsnd (K j)) + facts + |> map_index (fn (j, fact) => fact |> apsnd (K (j + 1))) |> filter_used_facts false used_facts |> distinct (eq_fst (op =)) |> map (prefix "@" o string_of_int o snd) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Apr 04 22:20:30 2025 +0200 @@ -202,26 +202,7 @@ good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = max_new_mono_insts} -val old_e_config : atp_config = make_e_config default_max_new_mono_instances (let - val (format, type_enc, lam_trans, extra_options) = - if getenv "E_VERSION" >= "3.0" then - (* '$ite' support appears to be unsound. *) - (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true") - else if getenv "E_VERSION" >= "2.6" then - (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule") - else - (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule") - in - (* FUDGE *) - [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)), - ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)), - ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)), - ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)), - ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)), - ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))] - end) - -val new_e_config : atp_config = +val e_config : atp_config = (* FUDGE: this solved 950/1500 (63.33 %) using MePo when testing *) let val extra_options = "--auto-schedule" @@ -252,11 +233,7 @@ in -val e = (eN, fn () => - if string_ord (getenv "E_VERSION", "3.0") <> LESS then - new_e_config - else - old_e_config) +val e = (eN, fn () => e_config) end @@ -407,13 +384,6 @@ local -val old_vampire_basic_options = - ["--proof tptp", - "--output_axiom_names on"] @ - (if ML_System.platform_is_windows - then [] (*time slicing is not support in the Windows version of Vampire*) - else ["--mode casc"]) - val new_vampire_basic_options = ["--input_syntax tptp", "--proof tptp", @@ -451,19 +421,7 @@ good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = good_max_new_mono_instances} -val old_vampire_config : atp_config = - (* FUDGE *) - make_vampire_config old_vampire_basic_options (2 * default_max_new_mono_instances) - [((2, false, false, 512, meshN), (TX1, "mono_native", combsN, false, sosN)), - ((2, false, false, 1024, meshN), (TX1, "mono_native", liftingN, false, sosN)), - ((2, false, false, 256, mashN), (TX1, "mono_native", liftingN, false, no_sosN)), - ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), - ((2, false, false, 16, meshN), (TX1, "mono_native", liftingN, false, no_sosN)), - ((2, false, false, 32, meshN), (TX1, "mono_native", combsN, false, no_sosN)), - ((2, false, false, 64, meshN), (TX1, "mono_native", combs_or_liftingN, false, no_sosN)), - ((2, false, false, 128, meshN), (TX1, "mono_native", liftingN, false, no_sosN))] - -val new_vampire_config : atp_config = +val vampire_config : atp_config = (* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *) make_vampire_config new_vampire_basic_options 256 [(((2, false, false, 512, meshN), (TX0, "mono_native_fool", liftingN, false, ""))), @@ -488,11 +446,7 @@ in -val vampire = (vampireN, fn () => - if string_ord (getenv "VAMPIRE_VERSION", "4.8") <> LESS then - new_vampire_config - else - old_vampire_config) +val vampire = (vampireN, fn () => vampire_config) end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Apr 04 22:20:30 2025 +0200 @@ -292,7 +292,7 @@ fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = - Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) + Proof.map_contexts (Try0_HOL.silence_methods #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Apr 04 22:20:30 2025 +0200 @@ -370,10 +370,10 @@ end fun fact_distinct eq facts = - fold (fn (i, fact as (_, th)) => + fold_index (fn (i, fact as (_, th)) => Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd o snd)) (normalize_eq (Thm.prop_of th), (i, fact))) - (tag_list 0 facts) Net.empty + facts Net.empty |> Net.entries |> sort (int_ord o apply2 fst) |> map snd @@ -452,6 +452,13 @@ not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th))) end +local + +type lazy_facts = + {singletons : lazy_fact list , dotteds : lazy_fact list, collections : lazy_fact list} + +in + fun all_facts ctxt generous keywords add_ths chained css = let val thy = Proof_Context.theory_of ctxt @@ -470,7 +477,7 @@ val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) - fun add_facts global foldx facts = + fun add_facts global foldx facts : 'a -> lazy_facts -> lazy_facts = foldx (fn (name0, ths) => fn accum => if name0 <> "" andalso (Long_Name.is_hidden (Facts.intern facts name0) orelse @@ -489,7 +496,7 @@ NONE => false | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')) in - snd (fold_rev (fn th0 => fn (j, accum) => + snd (fold_rev (fn th0 => fn (j, accum as {singletons, dotteds, collections} : lazy_facts) => let val th = transfer th0 in (j - 1, if not (member Thm.eq_thm_prop add_ths th) andalso @@ -517,21 +524,27 @@ val stature = stature_of_thm global assms chained css name0 th val new = ((get_name, stature), th) in - (if collection then apsnd o apsnd - else if dotted_name then apsnd o apfst - else apfst) (cons new) accum + if collection then + {singletons = singletons, dotteds = dotteds, collections = new :: collections} + else if dotted_name then + {singletons = singletons, dotteds = new :: dotteds, collections = collections} + else + {singletons = new :: singletons, dotteds = dotteds, collections = collections} end) end) ths (n, accum)) end) + val {singletons, dotteds, collections} = + {singletons = [], dotteds = [], collections = []} + |> add_facts false fold local_facts (unnamed_locals @ named_locals) + |> add_facts true Facts.fold_static global_facts global_facts in (* Names like "xxx" are preferred to "xxx.yyy", which are preferred to "xxx(666)" and the like. "Preferred" means "put to the front of the list". *) - ([], ([], [])) - |> add_facts false fold local_facts (unnamed_locals @ named_locals) - |> add_facts true Facts.fold_static global_facts global_facts - ||> op @ |> op @ + singletons @ dotteds @ collections end +end + fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t = if only andalso null add then [] diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Apr 04 22:20:30 2025 +0200 @@ -220,7 +220,7 @@ | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n (* FIXME *) -fun proof_method_command meth i n used_chaineds extras = +fun proof_method_command meth i n extras = let val (indirect_facts, direct_facts) = if is_proof_method_direct meth then ([], extras) else (extras, []) @@ -247,9 +247,9 @@ Markup.markup (Markup.break {width = 1, indent = 2}) " ") fun one_line_proof_text ((used_facts, (meth, play)), banner, subgoal, subgoal_count) = - let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in + let val extra = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts in map fst extra - |> proof_method_command meth subgoal subgoal_count (map fst chained) + |> proof_method_command meth subgoal subgoal_count |> (if play = Play_Failed then failed_command_line else try_command_line banner play) end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Fri Apr 04 22:20:30 2025 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen Isabelle tactics as Sledgehammer provers. *) @@ -11,21 +12,6 @@ type prover = Sledgehammer_Prover.prover type base_slice = Sledgehammer_ATP_Systems.base_slice - val algebraN : string - val argoN : string - val autoN : string - val blastN : string - val fastforceN : string - val forceN : string - val linarithN : string - val mesonN : string - val metisN : string - val orderN : string - val presburgerN : string - val satxN : string - val simpN : string - - val tactic_provers : string list val is_tactic_prover : string -> bool val good_slices_of_tactic_prover : string -> base_slice list val run_tactic_prover : mode -> string -> prover @@ -34,31 +20,11 @@ structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC = struct -open ATP_Problem_Generate open ATP_Proof -open Sledgehammer_ATP_Systems open Sledgehammer_Proof_Methods open Sledgehammer_Prover -val algebraN = "algebra" -val argoN = "argo" -val autoN = "auto" -val blastN = "blast" -val fastforceN = "fastforce" -val forceN = "force" -val linarithN = "linarith" -val mesonN = "meson" -val metisN = "metis" -val orderN = "order" -val presburgerN = "presburger" -val satxN = "satx" -val simpN = "simp" - -val tactic_provers = - [algebraN, argoN, autoN, blastN, fastforceN, forceN, linarithN, mesonN, - metisN, orderN, presburgerN, satxN, simpN] - -val is_tactic_prover = member (op =) tactic_provers +val is_tactic_prover : string -> bool = is_some o Try0.get_proof_method val meshN = "mesh" @@ -69,62 +35,61 @@ (1, false, false, 8, meshN), (1, false, false, 32, meshN)] -fun meth_of name = - if name = algebraN then Algebra_Method - else if name = argoN then Argo_Method - else if name = autoN then Auto_Method - else if name = blastN then Blast_Method - else if name = fastforceN then Fastforce_Method - else if name = forceN then Force_Method - else if name = linarithN then Linarith_Method - else if name = mesonN then Meson_Method - else if name = metisN then Metis_Method (NONE, NONE, []) - else if name = orderN then Order_Method - else if name = presburgerN then Presburger_Method - else if name = satxN then SATx_Method - else if name = simpN then Simp_Method - else error ("Unknown tactic: " ^ quote name) - -fun tac_of ctxt name (local_facts, global_facts) = - Sledgehammer_Proof_Methods.tac_of_proof_method ctxt (local_facts, global_facts) (meth_of name) +fun meth_of "algebra" = Algebra_Method + | meth_of "argo" = Argo_Method + | meth_of "auto" = Auto_Method + | meth_of "blast" = Blast_Method + | meth_of "fastforce" = Fastforce_Method + | meth_of "force" = Force_Method + | meth_of "linarith" = Linarith_Method + | meth_of "meson" = Meson_Method + | meth_of "metis" = Metis_Method (NONE, NONE, []) + | meth_of "order" = Order_Method + | meth_of "presburger" = Presburger_Method + | meth_of "satx" = SATx_Method + | meth_of "simp" = Simp_Method + | meth_of _ = Metis_Method (NONE, NONE, []) fun run_tactic_prover mode name ({slices, timeout, ...} : params) - ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice = + ({state, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice = let val (basic_slice as (slice_size, _, _, _, _), No_Slice) = slice val facts = facts_of_basic_slice basic_slice factss - val {facts = chained, ...} = Proof.goal state val ctxt = Proof.context_of state - val (local_facts, global_facts) = - ([], []) - |> fold (fn ((_, (scope, _)), thm) => - if scope = Global then apsnd (cons thm) - else if scope = Chained then I - else apfst (cons thm)) facts - |> apfst (append chained) - - val run_timeout = slice_timeout slice_size slices timeout + fun run_try0 () : Try0.result option = + let + val run_timeout = slice_timeout slice_size slices timeout + fun is_cartouche str = String.isPrefix "\" str andalso String.isSuffix "\" str + fun xref_of_fact (((name, _), thm) : Sledgehammer_Fact.fact) = + let + val xref = + if is_cartouche name then + Facts.Fact (Pretty.pure_string_of (Thm.pretty_thm ctxt thm)) + else + Facts.named name + in + (xref, []) + end + val xrefs = map xref_of_fact facts + val facts : Try0.facts = {usings = xrefs, simps = [], intros = [], elims = [], dests = []} + in + Try0.get_proof_method_or_noop name (SOME run_timeout) facts state + end val timer = Timer.startRealTimer () - val out = - (Timeout.apply run_timeout - (Goal.prove ctxt [] [] (Logic.get_goal (Thm.prop_of goal) subgoal)) - (fn {context = ctxt, ...} => - HEADGOAL (tac_of ctxt name (local_facts, global_facts))); - NONE) + (case run_try0 () of + NONE => SOME GaveUp + | SOME _ => NONE) handle ERROR _ => SOME GaveUp | Exn.Interrupt_Breakdown => SOME GaveUp | Timeout.TIMEOUT _ => SOME TimedOut - val run_time = Timer.checkRealTimer timer val (outcome, used_facts) = (case out of - NONE => - (found_something name; - (NONE, map fst facts)) + NONE => (found_something name; (NONE, map fst facts)) | some_failure => (some_failure, [])) val message = fn _ => diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/literal.ML --- a/src/HOL/Tools/literal.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/literal.ML Fri Apr 04 22:20:30 2025 +0200 @@ -103,7 +103,7 @@ let fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] = case implode_literal b0 b1 b2 b3 b4 b5 b6 t of - SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s + SOME s => (Pretty.str o Code_Printer.literal_string literals) s | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression"; in thy diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/numeral.ML Fri Apr 04 22:20:30 2025 +0200 @@ -104,7 +104,7 @@ let fun pretty literals _ thm _ _ [(t, _)] = case dest_num_code t of - SOME n => (Code_Printer.str o print literals o preproc) n + SOME n => (Pretty.str o print literals o preproc) n | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"; in thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of, diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Tools/try0.ML Fri Apr 04 22:20:30 2025 +0200 @@ -1,180 +1,132 @@ -(* Title: HOL/Tools/try0.ML - Author: Jasmin Blanchette, TU Muenchen +(* Title: HOL/Tools/try0.ML + Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen + Author: Fabian Huch, TU Muenchen Try a combination of proof methods. *) signature TRY0 = sig - val silence_methods : bool -> Proof.context -> Proof.context - datatype modifier = Use | Simp | Intro | Elim | Dest - type xthm = Facts.ref * Token.src list - type tagged_xthm = xthm * modifier list + val serial_commas : string -> string list -> string list + + type xref = Facts.ref * Token.src list + + type facts = + {usings: xref list, + simps : xref list, + intros : xref list, + elims : xref list, + dests : xref list} + val empty_facts : facts + type result = {name: string, command: string, time: Time.time, state: Proof.state} - val apply_proof_method : string -> Time.time option -> (xthm * modifier list) list -> - Proof.state -> result option - val try0 : Time.time option -> tagged_xthm list -> Proof.state -> result list + type proof_method = Time.time option -> facts -> Proof.state -> result option + type proof_method_options = {run_if_auto_try: bool} + + val register_proof_method : string -> proof_method_options -> proof_method -> unit + val get_proof_method : string -> proof_method option + val get_proof_method_or_noop : string -> proof_method + val get_all_proof_method_names : unit -> string list + + val schedule : string Config.T + + datatype mode = Auto_Try | Try | Normal + val generic_try0 : mode -> Time.time option -> facts -> Proof.state -> + (bool * (string * string list)) * result list + val try0 : Time.time option -> facts -> Proof.state -> result list end structure Try0 : TRY0 = struct +fun serial_commas _ [] = ["??"] + | serial_commas _ [s] = [s] + | serial_commas conj [s1, s2] = [s1, conj, s2] + | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] + | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss; + val noneN = "none" datatype mode = Auto_Try | Try | Normal val default_timeout = seconds 5.0 -fun run_tac timeout_opt tac st = - let val with_timeout = - (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) - in with_timeout (Seq.pull o tac) st |> Option.map fst end - -val num_goals = Thm.nprems_of o #goal o Proof.goal -fun apply_recursive recurse elapsed0 timeout_opt apply st = - (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of - ({elapsed, ...}, SOME st') => - if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then - let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) - in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end - else (elapsed0 + elapsed, st') - |_ => (elapsed0, st)) +datatype modifier = Use | Simp | Intro | Elim | Dest +type xref = Facts.ref * Token.src list +type tagged_xref = xref * modifier list +type facts = + {usings: xref list, + simps : xref list, + intros : xref list, + elims : xref list, + dests : xref list} -fun parse_method ctxt s = - enclose "(" ")" s - |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start - |> filter Token.is_proper - |> Scan.read Token.stopper Method.parse - |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") - -datatype modifier = Use | Simp | Intro | Elim | Dest -type xthm = Facts.ref * Token.src list -type tagged_xthm = xthm * modifier list - -fun string_of_xthm ((xref, args) : xthm) = - (case xref of - Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche - | _ => - Facts.string_of_ref xref) ^ implode - (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args) - -fun add_attr_text (tagged : tagged_xthm list) (tag, src) s = - let - val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xthm o fst) - in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end - -fun attrs_text tags (tagged : tagged_xthm list) = - "" |> fold (add_attr_text tagged) tags +val empty_facts: facts = {usings = [], simps = [], intros = [], elims = [], dests = []} +fun union_facts (left : facts) (right : facts) : facts = + {usings = #usings left @ #usings right, + simps = #simps left @ #simps right, + intros = #intros left @ #intros right, + elims = #elims left @ #elims right, + dests = #dests left @ #dests right} type result = {name: string, command: string, time: Time.time, state: Proof.state} +type proof_method = Time.time option -> facts -> Proof.state -> result option +type proof_method_options = {run_if_auto_try: bool} + +val noop_proof_method : proof_method = fn _ => fn _ => fn _ => NONE local - -val full_attrs = [(Simp, "simp"), (Intro, "intro"), (Elim, "elim"), (Dest, "dest")] -val clas_attrs = [(Intro, "intro"), (Elim, "elim"), (Dest, "dest")] -val simp_attrs = [(Simp, "add")] -val metis_attrs = [(Simp, ""), (Intro, ""), (Elim, ""), (Dest, "")] -val no_attrs = [] - -(* name * ((all_goals, run_if_auto_try), tags *) -val raw_named_methods = - [("simp", ((false, true), simp_attrs)), - ("auto", ((true, true), full_attrs)), - ("blast", ((false, true), clas_attrs)), - ("metis", ((false, true), metis_attrs)), - ("argo", ((false, true), no_attrs)), - ("linarith", ((false, true), no_attrs)), - ("presburger", ((false, true), no_attrs)), - ("algebra", ((false, true), no_attrs)), - ("fast", ((false, false), clas_attrs)), - ("fastforce", ((false, false), full_attrs)), - ("force", ((false, false), full_attrs)), - ("meson", ((false, false), metis_attrs)), - ("satx", ((false, false), no_attrs)), - ("order", ((false, true), no_attrs))] - -fun apply_raw_named_method (name, ((all_goals, _), attrs)) timeout_opt tagged st : - result option = - let - val unused = - tagged - |> filter - (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst))) - |> map fst - - val attrs = attrs_text attrs tagged - - val ctxt = Proof.context_of st - - val text = - name ^ attrs - |> parse_method ctxt - |> Method.method_cmd ctxt - |> Method.Basic - |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) - - val apply = - Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)] - #> Proof.refine text #> Seq.filter_results - val num_before = num_goals st - val multiple_goals = all_goals andalso num_before > 1 - val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st - val num_after = num_goals st' - val select = "[" ^ string_of_int (num_before - num_after) ^ "]" - val unused = implode_space (unused |> map string_of_xthm) - val command = - (if unused <> "" then "using " ^ unused ^ " " else "") ^ - (if num_after = 0 then "by " else "apply ") ^ - (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ - (if multiple_goals andalso num_after > 0 then select else "") - in - if num_before > num_after then - SOME {name = name, command = command, time = time, state = st'} - else NONE - end - + val proof_methods = + Synchronized.var "Try0.proof_methods" (Symtab.empty : proof_method Symtab.table); + val auto_try_proof_methods_names = + Synchronized.var "Try0.auto_try_proof_methods" (Symset.empty : Symset.T); in -val named_methods = map fst raw_named_methods - -fun apply_proof_method name timeout_opt tagged st : - result option = - (case AList.lookup (op =) raw_named_methods name of - NONE => NONE - | SOME raw_method => apply_raw_named_method (name, raw_method) timeout_opt tagged st) +fun register_proof_method name ({run_if_auto_try} : proof_method_options) proof_method = + let + val () = if name = "" then error "Registering unnamed proof method" else () + val () = Synchronized.change proof_methods (Symtab.update (name, proof_method)) + val () = + if run_if_auto_try then + Synchronized.change auto_try_proof_methods_names (Symset.insert name) + else + () + in () end -fun maybe_apply_proof_method name mode timeout_opt tagged st : - result option = - (case AList.lookup (op =) raw_named_methods name of - NONE => NONE - | SOME (raw_method as ((_, run_if_auto_try), _)) => - if mode <> Auto_Try orelse run_if_auto_try then - apply_raw_named_method (name, raw_method) timeout_opt tagged st - else - NONE) +fun get_proof_method (name : string) : proof_method option = + Symtab.lookup (Synchronized.value proof_methods) name; + +fun get_all_proof_method_names () : string list = + Symtab.fold (fn (name, _) => fn names => name :: names) (Synchronized.value proof_methods) [] + +fun should_auto_try_proof_method (name : string) : bool = + Symset.member (Synchronized.value auto_try_proof_methods_names) name end -val maybe_apply_methods = map maybe_apply_proof_method named_methods +fun get_proof_method_or_noop name = + (case get_proof_method name of + NONE => (warning ("Proof method \"" ^ name ^ "\" is undefined"); noop_proof_method) + | SOME proof_method => proof_method) + +fun maybe_apply_proof_method name mode : proof_method = + if mode <> Auto_Try orelse should_auto_try_proof_method name then + get_proof_method_or_noop name + else + noop_proof_method + +val schedule = Attrib.setup_config_string \<^binding>\try0_schedule\ (K "") + +local fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms" fun tool_time_string (s, time) = s ^ ": " ^ time_string time -(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification - bound exceeded" warnings and the like. *) -fun silence_methods debug = - Config.put Metis_Tactic.verbose debug - #> not debug ? (fn ctxt => - ctxt - |> Simplifier_Trace.disable - |> Context_Position.set_visible false - |> Config.put Unify.unify_trace false - |> Config.put Argo_Tactic.trace "none") - -fun generic_try0 mode timeout_opt (tagged : tagged_xthm list) st = +fun generic_try0_step mode (timeout_opt : Time.time option) (facts : facts) (st : Proof.state) + (proof_methods : string list) = let - val st = Proof.map_contexts (silence_methods false) st - fun try_method method = method mode timeout_opt tagged st + fun try_method (method : mode -> proof_method) = method mode timeout_opt facts st fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command command ^ " (" ^ time_string time ^ ")" val print_step = Option.map (tap (writeln o get_message)) @@ -188,11 +140,12 @@ methods |> Par_List.get_some try_method |> the_list + val maybe_apply_methods = map maybe_apply_proof_method proof_methods in if mode = Normal then - "Trying " ^ implode_space (Try.serial_commas "and" (map quote named_methods)) ^ - "..." - |> writeln + let val names = map quote proof_methods in + writeln ("Trying " ^ implode_space (serial_commas "and" names) ^ "...") + end else (); (case get_results maybe_apply_methods of @@ -218,31 +171,54 @@ end) end +in + +fun generic_try0 mode (timeout_opt : Time.time option) (facts : facts) (st : Proof.state) = + let + fun some_nonempty_string sub = + if Substring.isEmpty sub then + NONE + else + SOME (Substring.string sub) + val schedule = + Config.get (Proof.context_of st) schedule + |> Substring.full + |> Substring.tokens (fn c => c = #"|") + |> map (map_filter some_nonempty_string o Substring.tokens Char.isSpace) + fun iterate [] = ((false, (noneN, [])), []) + | iterate (proof_methods :: proof_methodss) = + (case generic_try0_step mode timeout_opt facts st proof_methods of + (_, []) => iterate proof_methodss + | result as (_, _ :: _) => result) + in + iterate (if null schedule then [get_all_proof_method_names ()] else schedule) + end; + +end + fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt -fun try0_trans tagged = - Toplevel.keep_proof - (ignore o generic_try0 Normal (SOME default_timeout) tagged o Toplevel.proof_of) +fun try0_trans (facts : facts) = + Toplevel.keep_proof (ignore o try0 (SOME default_timeout) facts o Toplevel.proof_of) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_attr = - Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Simp])) - || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Intro])) - || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Elim])) - || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Dest])) + Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = xrefs, intros = [], elims = [], dests = []}) + || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = [], intros = xrefs, elims = [], dests = []}) + || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = [], intros = [], elims = xrefs, dests = []}) + || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = [], intros = [], elims = [], dests = xrefs}) fun parse_attrs x = (Args.parens parse_attrs - || Scan.repeat parse_attr >> (fn tagged => fold (curry (op @)) tagged [])) x + || Scan.repeat parse_attr >> (fn factss => fold union_facts factss empty_facts)) x val _ = Outer_Syntax.command \<^command_keyword>\try0\ "try a combination of proof methods" - (Scan.optional parse_attrs [] #>> try0_trans) - -val _ = - Try.tool_setup - {name = "try0", weight = 30, auto_option = \<^system_option>\auto_methods\, - body = fn auto => fst o generic_try0 (if auto then Auto_Try else Try) NONE []} + (Scan.optional parse_attrs empty_facts #>> try0_trans) end diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Tools/try0_util.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/try0_util.ML Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,153 @@ +(* Title: HOL/Tools/try0_hol.ML + Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen + Author: Fabian Huch, TU Muenchen + +General-purpose functions used by Try0. +*) + +signature TRY0_UTIL = +sig + val string_of_xref : Try0.xref -> string + + type facts_prefixes = + {simps : string option, + intros : string option, + elims : string option, + dests : string option} + val full_attrs : facts_prefixes + val clas_attrs : facts_prefixes + val simp_attrs : facts_prefixes + val metis_attrs : facts_prefixes + val no_attrs : facts_prefixes + val apply_raw_named_method : string -> bool -> facts_prefixes -> + (Proof.context -> Proof.context) -> Time.time option -> Try0.facts -> Proof.state -> + Try0.result option +end + +structure Try0_Util : TRY0_UTIL = struct + +fun string_of_xref ((xref, args) : Try0.xref) = + (case xref of + Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche + | _ => + Facts.string_of_ref xref) ^ implode + (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args) + + +type facts_prefixes = + {simps : string option, + intros : string option, + elims : string option, + dests : string option} + +val no_attrs : facts_prefixes = + {simps = NONE, intros = NONE, elims = NONE, dests = NONE} +val full_attrs : facts_prefixes = + {simps = SOME "simp: ", intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "} +val clas_attrs : facts_prefixes = + {simps = NONE, intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "} +val simp_attrs : facts_prefixes = + {simps = SOME "add: ", intros = NONE, elims = NONE, dests = NONE} +val metis_attrs : facts_prefixes = + {simps = SOME "", intros = SOME "", elims = SOME "", dests = SOME ""} + +local + +fun parse_method ctxt s = + enclose "(" ")" s + |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start + |> filter Token.is_proper + |> Scan.read Token.stopper Method.parse + |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") + +fun run_tac timeout_opt tac st = + let val with_timeout = + (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) + in with_timeout (Seq.pull o tac) st |> Option.map fst end + +val num_goals = Thm.nprems_of o #goal o Proof.goal + +fun apply_recursive recurse elapsed0 timeout_opt apply st = + (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of + ({elapsed, ...}, SOME st') => + if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then + let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) + in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end + else (elapsed0 + elapsed, st') + |_ => (elapsed0, st)) + +in + +fun apply_raw_named_method (name : string) all_goals (prefixes: facts_prefixes) + (silence_methods : Proof.context -> Proof.context) timeout_opt (facts : Try0.facts) + (st : Proof.state) : Try0.result option = + let + val st = Proof.map_contexts silence_methods st + val ctxt = Proof.context_of st + + val (unused_simps, simps_attrs) = + if null (#simps facts) then + ([], "") + else + (case #simps prefixes of + NONE => (#simps facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#simps facts)))) + + val (unused_intros, intros_attrs) = + if null (#intros facts) then + ([], "") + else + (case #intros prefixes of + NONE => (#intros facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#intros facts)))) + + val (unused_elims, elims_attrs) = + if null (#elims facts) then + ([], "") + else + (case #elims prefixes of + NONE => (#elims facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#elims facts)))) + + val (unused_dests, dests_attrs) = + if null (#dests facts) then + ([], "") + else + (case #dests prefixes of + NONE => (#dests facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#dests facts)))) + + val unused = #usings facts @ unused_simps @ unused_intros @ unused_elims @ unused_dests + + val attrs = simps_attrs ^ intros_attrs ^ elims_attrs ^ dests_attrs + val text = + name ^ attrs + |> parse_method ctxt + |> Method.method_cmd ctxt + |> Method.Basic + |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) + + val apply = + Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)] + #> Proof.refine text #> Seq.filter_results + val num_before = num_goals st + val multiple_goals = all_goals andalso num_before > 1 + val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st + val num_after = num_goals st' + val select = "[" ^ string_of_int (num_before - num_after) ^ "]" + val unused = implode_space (unused |> map string_of_xref) + val command = + (if unused <> "" then "using " ^ unused ^ " " else "") ^ + (if num_after = 0 then "by " else "apply ") ^ + (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ + (if multiple_goals andalso num_after > 0 then select else "") + in + if num_before > num_after then + SOME {name = name, command = command, time = time, state = st'} + else NONE + end + +end + +end \ No newline at end of file diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Fri Apr 04 22:20:23 2025 +0200 +++ b/src/HOL/Transcendental.thy Fri Apr 04 22:20:30 2025 +0200 @@ -3978,12 +3978,24 @@ lemma sin_npi2_numeral [simp]: "sin (pi * Num.numeral n) = 0" by (metis of_nat_numeral sin_npi2) +lemma sin_npi_complex' [simp]: "sin (of_nat n * of_real pi) = 0" + by (metis of_real_0 of_real_mult of_real_of_nat_eq sin_npi sin_of_real) + lemma cos_npi_numeral [simp]: "cos (Num.numeral n * pi) = (- 1) ^ Num.numeral n" by (metis cos_npi of_nat_numeral) lemma cos_npi2_numeral [simp]: "cos (pi * Num.numeral n) = (- 1) ^ Num.numeral n" by (metis cos_npi2 of_nat_numeral) +lemma cos_npi_complex' [simp]: "cos (of_nat n * of_real pi) = (-1) ^ n" for n +proof - + have "cos (of_nat n * of_real pi :: 'a) = of_real (cos (real n * pi))" + by (subst cos_of_real [symmetric]) simp + also have "cos (real n * pi) = (-1) ^ n" + by simp + finally show ?thesis by simp +qed + lemma cos_two_pi [simp]: "cos (2 * pi) = 1" by (simp add: cos_double) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Try0.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Try0.thy Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,22 @@ +(* Title: HOL/Try0.thy + Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen + Author: Fabian Huch, TU Muenchen +*) + +theory Try0 + imports Pure + keywords "try0" :: diag +begin + +ML_file \Tools/try0.ML\ +ML_file \Tools/try0_util.ML\ + +ML \ +val () = + Try0.register_proof_method "simp" {run_if_auto_try = true} + (Try0_Util.apply_raw_named_method "simp" false Try0_Util.simp_attrs Simplifier_Trace.disable) + handle Symtab.DUP _ => () +\ + +end \ No newline at end of file diff -r 8b5dd705dfef -r 8f6dc8483b1a src/HOL/Try0_HOL.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Try0_HOL.thy Fri Apr 04 22:20:30 2025 +0200 @@ -0,0 +1,72 @@ +(* Title: HOL/Try0_HOL.thy + Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen + Author: Fabian Huch, TU Muenchen +*) +theory Try0_HOL + imports Try0 Presburger +begin + +ML \ +signature TRY0_HOL = +sig + val silence_methods : Proof.context -> Proof.context +end + +structure Try0_HOL : TRY0_HOL = struct + +(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification + bound exceeded" warnings and the like. *) +fun silence_methods ctxt = + ctxt + |> Config.put Metis_Tactic.verbose false + |> Simplifier_Trace.disable + |> Context_Position.set_visible false + |> Config.put Unify.unify_trace false + |> Config.put Argo_Tactic.trace "none" + +local + +open Try0_Util + +(* name * (run_if_auto_try * (all_goals * tags)) *) +val raw_named_methods = + [("auto", (true, (true, full_attrs))), + ("blast", (true, (false, clas_attrs))), + ("metis", (true, (false, metis_attrs))), + ("argo", (true, (false, no_attrs))), + ("linarith", (true, (false, no_attrs))), + ("presburger", (true, (false, no_attrs))), + ("algebra", (true, (false, no_attrs))), + ("fast", (false, (false, clas_attrs))), + ("fastforce", (false, (false, full_attrs))), + ("force", (false, (false, full_attrs))), + ("meson", (false, (false, metis_attrs))), + ("satx", (false, (false, no_attrs))), + ("iprover", (false, (false, no_attrs))), + ("order", (true, (false, no_attrs)))] + +in + +val () = raw_named_methods + |> List.app (fn (name, (run_if_auto_try, (all_goals, tags))) => + let + val meth : Try0.proof_method = + Try0_Util.apply_raw_named_method name all_goals tags silence_methods + in + Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth + handle Symtab.DUP _ => () + end) + +end + +end +\ + +declare [[try0_schedule = " + satx iprover metis | + order presburger linarith algebra argo | + simp auto blast fast fastforce force meson +"]] + +end \ No newline at end of file diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Pure/Build/build_manager.scala Fri Apr 04 22:20:30 2025 +0200 @@ -871,7 +871,10 @@ val rsync_context = Rsync.Context() private def sync(repository: Mercurial.Repository, rev: String, target: Path): String = { - repository.pull() + val pull_result = Exn.capture(repository.pull()) + if (Exn.is_exn(pull_result)) { + echo_error_message("Could not read from repository: " + Exn.the_exn(pull_result).getMessage) + } if (rev.nonEmpty) repository.sync(rsync_context, target, rev = rev) diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/Code/code_haskell.ML Fri Apr 04 22:20:30 2025 +0200 @@ -51,20 +51,20 @@ | SOME class => class; fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs of [] => [] - | constraints => enum "," "(" ")" ( + | constraints => Pretty.enum "," "(" ")" ( map (fn (v, class) => - str (class_name class ^ " " ^ lookup_var tyvars v)) constraints) - @@ str " => "; + Pretty.str (class_name class ^ " " ^ lookup_var tyvars v)) constraints) + @@ Pretty.str " => "; fun print_typforall tyvars vs = case map fst vs of [] => [] - | vnames => str "forall " :: Pretty.breaks - (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; + | vnames => Pretty.str "forall " :: Pretty.breaks + (map (Pretty.str o lookup_var tyvars) vnames) @ Pretty.str "." @@ Pretty.brk 1; fun print_tyco_expr tyvars fxy (tyco, tys) = - brackify fxy (str tyco :: map (print_typ tyvars BR) tys) + brackify fxy (Pretty.str tyco :: map (print_typ tyvars BR) tys) and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys) | SOME (_, print) => print (print_typ tyvars) fxy tys) - | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; + | print_typ tyvars fxy (ITyVar v) = (Pretty.str o lookup_var tyvars) v; fun print_typdecl tyvars (tyco, vs) = print_tyco_expr tyvars NOBR (tyco, map ITyVar vs); fun print_typscheme tyvars (vs, ty) = @@ -80,14 +80,14 @@ print_term tyvars some_thm vars BR t2 ]) | print_term tyvars some_thm vars fxy (IVar NONE) = - str "_" + Pretty.str "_" | print_term tyvars some_thm vars fxy (IVar (SOME v)) = - (str o lookup_var vars) v + (Pretty.str o lookup_var vars) v | print_term tyvars some_thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars; - in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end + in brackets (Pretty.str "\\" :: ps @ Pretty.str "->" @@ print_term tyvars some_thm vars' NOBR t') end | print_term tyvars some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) of SOME (app as ({ sym = Constant const, ... }, _)) => @@ -99,42 +99,42 @@ let val printed_const = case annotation of - SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty] - | NONE => (str o deresolve) sym + SOME ty => brackets [(Pretty.str o deresolve) sym, Pretty.str "::", print_typ tyvars NOBR ty] + | NONE => (Pretty.str o deresolve) sym in printed_const :: map (print_term tyvars some_thm vars BR) ts end and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p and print_case tyvars some_thm vars fxy { clauses = [], ... } = - (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""] + (brackify fxy o Pretty.breaks o map Pretty.str) ["error", "\"empty case\""] | print_case tyvars some_thm vars fxy (case_expr as { clauses = [(IVar _, _)], ... }) = let val (vs, body) = Code_Thingol.unfold_let_no_pat (ICase case_expr); fun print_assignment ((some_v, _), t) vars = vars |> print_bind tyvars some_thm BR (IVar some_v) - |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) + |>> (fn p => semicolon [p, Pretty.str "=", print_term tyvars some_thm vars NOBR t]) val (ps, vars') = fold_map print_assignment vs vars; - in brackify_block fxy (str "let {") + in brackify_block fxy (Pretty.str "let {") ps - (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body]) + (concat [Pretty.str "}", Pretty.str "in", print_term tyvars some_thm vars' NOBR body]) end | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } = let fun print_select (pat, body) = let val (p, vars') = print_bind tyvars some_thm NOBR pat vars; - in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end; + in semicolon [p, Pretty.str "->", print_term tyvars some_thm vars' NOBR body] end; in Pretty.block_enclose - (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})") + (concat [Pretty.str "(case", print_term tyvars some_thm vars NOBR t, Pretty.str "of", Pretty.str "{"], Pretty.str "})") (map print_select clauses) end; fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) = let val tyvars = intro_vars (map fst vs) reserved; fun print_err n = - (semicolon o map str) ( + (semicolon o map Pretty.str) ( deresolve_const const :: replicate n "_" @ "=" @@ -149,16 +149,16 @@ |> intro_vars (build (fold Code_Thingol.add_varnames ts)); in semicolon ( - (str o deresolve_const) const + (Pretty.str o deresolve_const) const :: map (print_term tyvars some_thm vars BR) ts - @ str "=" + @ Pretty.str "=" @@ print_term tyvars some_thm vars NOBR t ) end; in Pretty.chunks ( semicolon [ - (str o suffix " ::" o deresolve_const) const, + (Pretty.str o suffix " ::" o deresolve_const) const, print_typscheme tyvars (vs, ty) ] :: (case filter (snd o snd) raw_eqs @@ -171,7 +171,7 @@ val tyvars = intro_vars vs reserved; in semicolon [ - str "data", + Pretty.str "data", print_typdecl tyvars (deresolve_tyco tyco, vs) ] end @@ -180,12 +180,12 @@ val tyvars = intro_vars vs reserved; in semicolon ( - str "newtype" + Pretty.str "newtype" :: print_typdecl tyvars (deresolve_tyco tyco, vs) - :: str "=" - :: (str o deresolve_const) co + :: Pretty.str "=" + :: (Pretty.str o deresolve_const) co :: print_typ tyvars BR ty - :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else []) + :: (if deriving_show tyco then [Pretty.str "deriving (Prelude.Read, Prelude.Show)"] else []) ) end | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) = @@ -193,17 +193,17 @@ val tyvars = intro_vars vs reserved; fun print_co ((co, _), tys) = concat ( - (str o deresolve_const) co + (Pretty.str o deresolve_const) co :: map (print_typ tyvars BR) tys ) in semicolon ( - str "data" + Pretty.str "data" :: print_typdecl tyvars (deresolve_tyco tyco, vs) - :: str "=" + :: Pretty.str "=" :: print_co co - :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos - @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else []) + :: map ((fn p => Pretty.block [Pretty.str "| ", p]) o print_co) cos + @ (if deriving_show tyco then [Pretty.str "deriving (Prelude.Read, Prelude.Show)"] else []) ) end | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) = @@ -211,19 +211,19 @@ val tyvars = intro_vars [v] reserved; fun print_classparam (classparam, ty) = semicolon [ - (str o deresolve_const) classparam, - str "::", + (Pretty.str o deresolve_const) classparam, + Pretty.str "::", print_typ tyvars NOBR ty ] in Pretty.block_enclose ( Pretty.block [ - str "class ", + Pretty.str "class ", Pretty.block (print_typcontext tyvars [(v, map snd classrels)]), - str (deresolve_class class ^ " " ^ lookup_var tyvars v), - str " where {" + Pretty.str (deresolve_class class ^ " " ^ lookup_var tyvars v), + Pretty.str " where {" ], - str "};" + Pretty.str "};" ) (map print_classparam classparams) end | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) = @@ -232,13 +232,13 @@ fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = case const_syntax classparam of NONE => semicolon [ - (str o Long_Name.base_name o deresolve_const) classparam, - str "=", + (Pretty.str o Long_Name.base_name o deresolve_const) classparam, + Pretty.str "=", print_app tyvars (SOME thm) reserved NOBR (const, []) ] | SOME (_, Code_Printer.Plain_printer s) => semicolon [ - (str o Long_Name.base_name) s, - str "=", + (Pretty.str o Long_Name.base_name) s, + Pretty.str "=", print_app tyvars (SOME thm) reserved NOBR (const, []) ] | SOME (wanted, Code_Printer.Complex_printer _) => @@ -258,20 +258,20 @@ in semicolon [ print_term tyvars (SOME thm) vars NOBR lhs, - str "=", + Pretty.str "=", print_term tyvars (SOME thm) vars NOBR rhs ] end; in Pretty.block_enclose ( Pretty.block [ - str "instance ", + Pretty.str "instance ", Pretty.block (print_typcontext tyvars vs), - str (class_name class ^ " "), + Pretty.str (class_name class ^ " "), print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs), - str " where {" + Pretty.str " where {" ], - str "};" + Pretty.str "};" ) (map print_classparam_instance inst_params) end; in print_stmt end; @@ -368,31 +368,31 @@ fun print_module_frame module_name header exports ps = (module_names module_name, Pretty.chunks2 ( header - @ concat [str "module", + @ concat [Pretty.str "module", case exports of - SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)] - | NONE => str module_name, - str "where {" + SOME ps => Pretty.block [Pretty.str module_name, Pretty.enclose "(" ")" (Pretty.commas ps)] + | NONE => Pretty.str module_name, + Pretty.str "where {" ] :: ps - @| str "}" + @| Pretty.str "}" )); fun print_qualified_import module_name = - semicolon [str "import qualified", str module_name]; + semicolon [Pretty.str "import qualified", Pretty.str module_name]; val import_common_ps = - enclose "import Prelude (" ");" (commas (map str - (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified) - @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr)) - :: enclose "import Data.Bits (" ");" (commas - (map (str o Library.enclose "(" ")") data_bits_import_operators)) + Pretty.enclose "import Prelude (" ");" (Pretty.commas (map Pretty.str + (map (enclose "(" ")") prelude_import_operators @ prelude_import_unqualified) + @ map (fn (tyco, constrs) => (Pretty.enclose (tyco ^ "(") ")" o Pretty.commas o map Pretty.str) constrs) prelude_import_unqualified_constr)) + :: Pretty.enclose "import Data.Bits (" ");" (Pretty.commas + (map (Pretty.str o enclose "(" ")") data_bits_import_operators)) :: print_qualified_import "Prelude" :: print_qualified_import "Data.Bits" :: map (print_qualified_import o fst) includes; fun print_module module_name (gr, imports) = let val deresolve = deresolver module_name; - val deresolve_import = SOME o str o deresolve; - val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve; + val deresolve_import = SOME o Pretty.str o deresolve; + val deresolve_import_attached = SOME o Pretty.str o suffix "(..)" o deresolve; fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym | print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym @@ -409,7 +409,7 @@ |> split_list |> apfst (map_filter I); in - print_module_frame module_name [str language_pragma] (SOME export_ps) + print_module_frame module_name [Pretty.str language_pragma] (SOME export_ps) ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps) end; @@ -430,7 +430,7 @@ val literals = Literals { literal_string = print_haskell_string, literal_numeral = print_numeral "Integer", - literal_list = enum "," "[" "]", + literal_list = Pretty.enum "," "[" "]", infix_cons = (5, ":") }; @@ -455,22 +455,22 @@ (semicolon [print_term vars NOBR t], vars) | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars |> print_bind NOBR bind - |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t]) + |>> (fn p => semicolon [p, Pretty.str "<-", print_term vars NOBR t]) | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars |> print_bind NOBR bind - |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]); + |>> (fn p => semicolon [Pretty.str "let", Pretty.str "{", p, Pretty.str "=", print_term vars NOBR t, Pretty.str "}"]); fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 of SOME (bind, t') => let val (binds, t'') = implode_monad t' val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) (bind :: binds) vars; in - brackify_block fxy (str "do { ") + brackify_block fxy (Pretty.str "do { ") (ps @| print_term vars' NOBR t'') - (str " }") + (Pretty.str " }") end | NONE => brackify_infix (1, L) fxy - (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2) + (print_term vars (INFX (1, L)) t1, Pretty.str ">>=", print_term vars (INFX (1, X)) t2) in (2, pretty) end; fun add_monad target' raw_c_bind thy = @@ -499,7 +499,7 @@ [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => brackify_infix (1, R) fxy ( print_typ (INFX (1, X)) ty1, - str "->", + Pretty.str "->", print_typ (INFX (1, R)) ty2 )))])) #> fold (Code_Target.add_reserved target) [ diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/Code/code_ml.ML Fri Apr 04 22:20:30 2025 +0200 @@ -42,11 +42,11 @@ fun print_product _ [] = NONE | print_product print [x] = SOME (print x) - | print_product print xs = (SOME o enum " *" "" "") (map print xs); + | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs); fun tuplify _ _ [] = NONE | tuplify print fxy [x] = SOME (print fxy x) - | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); + | tuplify print _ xs = SOME (Pretty.enum "," "(" ")" (map (print NOBR) xs)); (** SML serializer **) @@ -65,33 +65,33 @@ val deresolve_const = deresolve o Constant; val deresolve_classrel = deresolve o Class_Relation; val deresolve_inst = deresolve o Class_Instance; - fun print_tyco_expr (sym, []) = (str o deresolve) sym + fun print_tyco_expr (sym, []) = (Pretty.str o deresolve) sym | print_tyco_expr (sym, [ty]) = - concat [print_typ BR ty, (str o deresolve) sym] + concat [print_typ BR ty, (Pretty.str o deresolve) sym] | print_tyco_expr (sym, tys) = - concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] + concat [Pretty.enum "," "(" ")" (map (print_typ BR) tys), (Pretty.str o deresolve) sym] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr (Type_Constructor tyco, tys) | SOME (_, print) => print print_typ fxy tys) - | print_typ fxy (ITyVar v) = str ("'" ^ v); + | print_typ fxy (ITyVar v) = Pretty.str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]); - fun print_typscheme_prefix (vs, p) = enum " ->" "" "" + fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); fun print_classrels fxy [] ps = brackify fxy ps - | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps] + | print_classrels fxy [classrel] ps = brackify fxy [(Pretty.str o deresolve_classrel) classrel, brackify BR ps] | print_classrels fxy classrels ps = - brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps] + brackify fxy [Pretty.enum " o" "(" ")" (map (Pretty.str o deresolve_classrel) classrels), brackify BR ps] fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x) and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = - ((str o deresolve_inst) inst :: - (if is_pseudo_fun (Class_Instance inst) then [str "()"] + ((Pretty.str o deresolve_inst) inst :: + (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"] else map_filter (print_dicts is_pseudo_fun BR o snd) dss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = - [str (if length = 1 then Name.enforce_case true var ^ "_" + [Pretty.str (if length = 1 then Name.enforce_case true var ^ "_" else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")] and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR @@ -100,9 +100,9 @@ fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = - str "_" + Pretty.str "_" | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) = - str (lookup_var vars v) + Pretty.str (lookup_var vars v) | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME app => print_app is_pseudo_fun some_thm vars fxy app @@ -113,7 +113,7 @@ val (binds, t') = Code_Thingol.unfold_pat_abs t; fun print_abs (pat, ty) = print_bind is_pseudo_fun some_thm NOBR pat - #>> (fn p => concat [str "fn", p, str "=>"]); + #>> (fn p => concat [Pretty.str "fn", p, Pretty.str "=>"]); val (ps, vars') = fold_map print_abs binds vars; in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) = @@ -127,33 +127,33 @@ if is_constr sym then let val wanted = length dom in if wanted < 2 orelse length ts = wanted - then (str o deresolve) sym + then (Pretty.str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)] end else if is_pseudo_fun sym - then (str o deresolve) sym @@ str "()" - else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts + then (Pretty.str o deresolve) sym @@ Pretty.str "()" + else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } = - (concat o map str) ["raise", "Fail", "\"empty case\""] + (concat o map Pretty.str) ["raise", "Fail", "\"empty case\""] | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) = let val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); fun print_match ((pat, _), t) vars = vars |> print_bind is_pseudo_fun some_thm NOBR pat - |>> (fn p => semicolon [str "val", p, str "=", + |>> (fn p => semicolon [Pretty.str "val", p, Pretty.str "=", print_term is_pseudo_fun some_thm vars NOBR t]) val (ps, vars') = fold_map print_match binds vars; in Pretty.chunks [ - Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], - Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body], - str "end" + Pretty.block [Pretty.str "let", Pretty.fbrk, Pretty.chunks ps], + Pretty.block [Pretty.str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body], + Pretty.str "end" ] end | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = @@ -162,29 +162,29 @@ let val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; in - concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body] + concat [Pretty.str delim, p, Pretty.str "=>", print_term is_pseudo_fun some_thm vars' NOBR body] end; in brackets ( - str "case" + Pretty.str "case" :: print_term is_pseudo_fun some_thm vars NOBR t :: print_select "of" clause :: map (print_select "|") clauses ) end; fun print_val_decl print_typscheme (sym, typscheme) = concat - [str "val", str (deresolve sym), str ":", print_typscheme typscheme]; + [Pretty.str "val", Pretty.str (deresolve sym), Pretty.str ":", print_typscheme typscheme]; fun print_datatype_decl definer (tyco, (vs, cos)) = let - fun print_co ((co, _), []) = str (deresolve_const co) - | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", - enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + fun print_co ((co, _), []) = Pretty.str (deresolve_const co) + | print_co ((co, _), tys) = concat [Pretty.str (deresolve_const co), Pretty.str "of", + Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( - str definer + Pretty.str definer :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) - :: str "=" - :: separate (str "|") (map print_co cos) + :: Pretty.str "=" + :: separate (Pretty.str "|") (map print_co cos) ) end; fun print_def is_pseudo_fun needs_typ definer @@ -197,15 +197,15 @@ deresolve (t :: ts) |> intro_vars (build (fold Code_Thingol.add_varnames ts)); val prolog = if needs_typ then - concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] - else (concat o map str) [definer, deresolve_const const]; + concat [Pretty.str definer, (Pretty.str o deresolve_const) const, Pretty.str ":", print_typ NOBR ty] + else (concat o map Pretty.str) [definer, deresolve_const const]; in concat ( prolog - :: (if is_pseudo_fun (Constant const) then [str "()"] + :: (if is_pseudo_fun (Constant const) then [Pretty.str "()"] else print_dict_args vs @ map (print_term is_pseudo_fun some_thm vars BR) ts) - @ str "=" + @ Pretty.str "=" @@ print_term is_pseudo_fun some_thm vars NOBR t ) end @@ -223,35 +223,35 @@ let fun print_super_instance (super_class, x) = concat [ - (str o Long_Name.base_name o deresolve_classrel) (class, super_class), - str "=", + (Pretty.str o Long_Name.base_name o deresolve_classrel) (class, super_class), + Pretty.str "=", print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x))) ]; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ - (str o Long_Name.base_name o deresolve_const) classparam, - str "=", + (Pretty.str o Long_Name.base_name o deresolve_const) classparam, + Pretty.str "=", print_app (K false) (SOME thm) reserved NOBR (const, []) ]; in pair (print_val_decl print_dicttypscheme (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) (concat ( - str definer - :: (str o deresolve_inst) inst - :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] + Pretty.str definer + :: (Pretty.str o deresolve_inst) inst + :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"] else print_dict_args vs) - @ str "=" - :: enum "," "{" "}" + @ Pretty.str "=" + :: Pretty.enum "," "{" "}" (map print_super_instance superinsts @ map print_classparam_instance inst_params) - :: str ":" + :: Pretty.str ":" @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) )) end; fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair [print_val_decl print_typscheme (Constant const, vs_ty)] - ((semicolon o map str) ( + ((semicolon o map Pretty.str) ( (if n = 0 then "val" else "fun") :: deresolve_const const :: replicate n "_" @@ -271,11 +271,11 @@ let val print_def' = print_def (member (op =) pseudo_funs) false; fun print_pseudo_fun sym = concat [ - str "val", - (str o deresolve) sym, - str "=", - (str o deresolve) sym, - str "();" + Pretty.str "val", + (Pretty.str o deresolve) sym, + Pretty.str "=", + (Pretty.str o deresolve) sym, + Pretty.str "();" ]; val (sig_ps, (ps, p)) = (apsnd split_last o split_list) (print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings); @@ -290,8 +290,8 @@ val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); in pair - [concat [str "type", ty_p]] - (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"]) + [concat [Pretty.str "type", ty_p]] + (semicolon [Pretty.str "datatype", ty_p, Pretty.str "=", Pretty.str "EMPTY__"]) end | print_stmt export (ML_Datas (data :: datas)) = let @@ -302,15 +302,15 @@ (if Code_Namespace.is_public export then decl_ps else map (fn (tyco, (vs, _)) => - concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) + concat [Pretty.str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) (data :: datas)) (Pretty.chunks (ps @| semicolon [p])) end | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) = let - fun print_field s p = concat [str s, str ":", p]; + fun print_field s p = concat [Pretty.str s, Pretty.str ":", p]; fun print_proj s p = semicolon - (map str ["val", s, "=", "#" ^ s, ":"] @| p); + (map Pretty.str ["val", s, "=", "#" ^ s, ":"] @| p); fun print_super_class_decl (classrel as (_, super_class)) = print_val_decl print_dicttypscheme (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v))); @@ -328,17 +328,17 @@ print_proj (deresolve_const classparam) (print_typscheme ([(v, [class])], ty)); in pair - (concat [str "type", print_dicttyp (class, ITyVar v)] + (concat [Pretty.str "type", print_dicttyp (class, ITyVar v)] :: (if Code_Namespace.is_public export then map print_super_class_decl classrels @ map print_classparam_decl classparams else [])) (Pretty.chunks ( concat [ - str "type", + Pretty.str "type", print_dicttyp (class, ITyVar v), - str "=", - enum "," "{" "};" ( + Pretty.str "=", + Pretty.enum "," "{" "};" ( map print_super_class_field classrels @ map print_classparam_field classparams ) @@ -352,18 +352,18 @@ fun print_sml_module name decls body = Pretty.chunks2 ( Pretty.chunks [ - str ("structure " ^ name ^ " : sig"), - (indent 2 o Pretty.chunks) decls, - str "end = struct" + Pretty.str ("structure " ^ name ^ " : sig"), + (Pretty.indent 2 o Pretty.chunks) decls, + Pretty.str "end = struct" ] :: body - @| str ("end; (*struct " ^ name ^ "*)") + @| Pretty.str ("end; (*struct " ^ name ^ "*)") ); val literals_sml = Literals { literal_string = print_sml_string, literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)", - literal_list = enum "," "[" "]", + literal_list = Pretty.enum "," "[" "]", infix_cons = (7, "::") }; @@ -392,32 +392,32 @@ val deresolve_const = deresolve o Constant; val deresolve_classrel = deresolve o Class_Relation; val deresolve_inst = deresolve o Class_Instance; - fun print_tyco_expr (sym, []) = (str o deresolve) sym + fun print_tyco_expr (sym, []) = (Pretty.str o deresolve) sym | print_tyco_expr (sym, [ty]) = - concat [print_typ BR ty, (str o deresolve) sym] + concat [print_typ BR ty, (Pretty.str o deresolve) sym] | print_tyco_expr (sym, tys) = - concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] + concat [Pretty.enum "," "(" ")" (map (print_typ BR) tys), (Pretty.str o deresolve) sym] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr (Type_Constructor tyco, tys) | SOME (_, print) => print print_typ fxy tys) - | print_typ fxy (ITyVar v) = str ("'" ^ v); + | print_typ fxy (ITyVar v) = Pretty.str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]); - fun print_typscheme_prefix (vs, p) = enum " ->" "" "" + fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); val print_classrels = - fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel]) + fold_rev (fn classrel => fn p => Pretty.block [p, Pretty.str ".", (Pretty.str o deresolve_classrel) classrel]) fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_plain_dict is_pseudo_fun fxy x |> print_classrels classrels and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = - brackify BR ((str o deresolve_inst) inst :: - (if is_pseudo_fun (Class_Instance inst) then [str "()"] + brackify BR ((Pretty.str o deresolve_inst) inst :: + (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"] else map_filter (print_dicts is_pseudo_fun BR o snd) dss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = - str (if length = 1 then "_" ^ Name.enforce_case true var + Pretty.str (if length = 1 then "_" ^ Name.enforce_case true var else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1)) and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR @@ -426,9 +426,9 @@ fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = - str "_" + Pretty.str "_" | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) = - str (lookup_var vars v) + Pretty.str (lookup_var vars v) | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME app => print_app is_pseudo_fun some_thm vars fxy app @@ -438,7 +438,7 @@ let val (binds, t') = Code_Thingol.unfold_pat_abs t; val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars; - in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end + in brackets (Pretty.str "fun" :: ps @ Pretty.str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) of SOME (app as ({ sym = Constant const, ... }, _)) => @@ -450,19 +450,19 @@ if is_constr sym then let val wanted = length dom in if length ts = wanted - then (str o deresolve) sym + then (Pretty.str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)] end else if is_pseudo_fun sym - then (str o deresolve) sym @@ str "()" - else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts + then (Pretty.str o deresolve) sym @@ Pretty.str "()" + else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } = - (concat o map str) ["failwith", "\"empty case\""] + (concat o map Pretty.str) ["failwith", "\"empty case\""] | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) = let val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); @@ -470,7 +470,7 @@ vars |> print_bind is_pseudo_fun some_thm NOBR pat |>> (fn p => concat - [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"]) + [Pretty.str "let", p, Pretty.str "=", print_term is_pseudo_fun some_thm vars NOBR t, Pretty.str "in"]) val (ps, vars') = fold_map print_let binds vars; in brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body] @@ -480,28 +480,28 @@ fun print_select delim (pat, body) = let val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; - in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end; + in concat [Pretty.str delim, p, Pretty.str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end; in brackets ( - str "match" + Pretty.str "match" :: print_term is_pseudo_fun some_thm vars NOBR t :: print_select "with" clause :: map (print_select "|") clauses ) end; fun print_val_decl print_typscheme (sym, typscheme) = concat - [str "val", str (deresolve sym), str ":", print_typscheme typscheme]; + [Pretty.str "val", Pretty.str (deresolve sym), Pretty.str ":", print_typscheme typscheme]; fun print_datatype_decl definer (tyco, (vs, cos)) = let - fun print_co ((co, _), []) = str (deresolve_const co) - | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", - enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + fun print_co ((co, _), []) = Pretty.str (deresolve_const co) + | print_co ((co, _), tys) = concat [Pretty.str (deresolve_const co), Pretty.str "of", + Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( - str definer + Pretty.str definer :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) - :: str "=" - :: separate (str "|") (map print_co cos) + :: Pretty.str "=" + :: separate (Pretty.str "|") (map print_co cos) ) end; fun print_def is_pseudo_fun needs_typ definer @@ -514,9 +514,9 @@ deresolve (t :: ts) |> intro_vars (build (fold Code_Thingol.add_varnames ts)); in concat [ - (Pretty.block o commas) + (Pretty.block o Pretty.commas) (map (print_term is_pseudo_fun some_thm vars NOBR) ts), - str "->", + Pretty.str "->", print_term is_pseudo_fun some_thm vars NOBR t ] end; fun print_eqns is_pseudo [((ts, t), (some_thm, _))] = @@ -527,20 +527,20 @@ |> intro_vars (build (fold Code_Thingol.add_varnames ts)); in concat ( - (if is_pseudo then [str "()"] + (if is_pseudo then [Pretty.str "()"] else map (print_term is_pseudo_fun some_thm vars BR) ts) - @ str "=" + @ Pretty.str "=" @@ print_term is_pseudo_fun some_thm vars NOBR t ) end | print_eqns _ ((eq as (([_], _), _)) :: eqs) = Pretty.block ( - str "=" + Pretty.str "=" :: Pretty.brk 1 - :: str "function" + :: Pretty.str "function" :: Pretty.brk 1 :: print_eqn eq - :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] + :: maps (append [Pretty.fbrk, Pretty.str "|", Pretty.brk 1] o single o print_eqn) eqs ) | print_eqns _ (eqs as eq :: eqs') = @@ -548,27 +548,27 @@ val vars = reserved |> intro_base_names_for (is_none o const_syntax) deresolve (map (snd o fst) eqs) - val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs; + val dummy_parms = (map Pretty.str o aux_params vars o map (fst o fst)) eqs; in Pretty.block ( Pretty.breaks dummy_parms @ Pretty.brk 1 - :: str "=" + :: Pretty.str "=" :: Pretty.brk 1 - :: str "match" + :: Pretty.str "match" :: Pretty.brk 1 - :: (Pretty.block o commas) dummy_parms + :: (Pretty.block o Pretty.commas) dummy_parms :: Pretty.brk 1 - :: str "with" + :: Pretty.str "with" :: Pretty.brk 1 :: print_eqn eq - :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] + :: maps (append [Pretty.fbrk, Pretty.str "|", Pretty.brk 1] o single o print_eqn) eqs' ) end; val prolog = if needs_typ then - concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] - else (concat o map str) [definer, deresolve_const const]; + concat [Pretty.str definer, (Pretty.str o deresolve_const) const, Pretty.str ":", print_typ NOBR ty] + else (concat o map Pretty.str) [definer, deresolve_const const]; in pair (print_val_decl print_typscheme (Constant const, vs_ty)) (concat ( @@ -582,36 +582,36 @@ let fun print_super_instance (super_class, dss) = concat [ - (str o deresolve_classrel) (class, super_class), - str "=", + (Pretty.str o deresolve_classrel) (class, super_class), + Pretty.str "=", print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dss))) ]; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ - (str o deresolve_const) classparam, - str "=", + (Pretty.str o deresolve_const) classparam, + Pretty.str "=", print_app (K false) (SOME thm) reserved NOBR (const, []) ]; in pair (print_val_decl print_dicttypscheme (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) (concat ( - str definer - :: (str o deresolve_inst) inst - :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] + Pretty.str definer + :: (Pretty.str o deresolve_inst) inst + :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"] else print_dict_args vs) - @ str "=" + @ Pretty.str "=" @@ brackets [ enum_default "()" ";" "{" "}" (map print_super_instance superinsts @ map print_classparam_instance inst_params), - str ":", + Pretty.str ":", print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) ] )) end; fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair [print_val_decl print_typscheme (Constant const, vs_ty)] - ((doublesemicolon o map str) ( + ((doublesemicolon o map Pretty.str) ( "let" :: deresolve_const const :: replicate n "_" @@ -630,11 +630,11 @@ let val print_def' = print_def (member (op =) pseudo_funs) false; fun print_pseudo_fun sym = concat [ - str "let", - (str o deresolve) sym, - str "=", - (str o deresolve) sym, - str "();;" + Pretty.str "let", + (Pretty.str o deresolve) sym, + Pretty.str "=", + (Pretty.str o deresolve) sym, + Pretty.str "();;" ]; val (sig_ps, (ps, p)) = (apsnd split_last o split_list) (print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings); @@ -649,8 +649,8 @@ val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); in pair - [concat [str "type", ty_p]] - (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"]) + [concat [Pretty.str "type", ty_p]] + (doublesemicolon [Pretty.str "type", ty_p, Pretty.str "=", Pretty.str "EMPTY__"]) end | print_stmt export (ML_Datas (data :: datas)) = let @@ -661,13 +661,13 @@ (if Code_Namespace.is_public export then decl_ps else map (fn (tyco, (vs, _)) => - concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) + concat [Pretty.str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) (data :: datas)) (Pretty.chunks (ps @| doublesemicolon [p])) end | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) = let - fun print_field s p = concat [str s, str ":", p]; + fun print_field s p = concat [Pretty.str s, Pretty.str ":", p]; fun print_super_class_field (classrel as (_, super_class)) = print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); fun print_classparam_decl (classparam, ty) = @@ -677,12 +677,12 @@ print_field (deresolve_const classparam) (print_typ NOBR ty); val w = "_" ^ Name.enforce_case true v; fun print_classparam_proj (classparam, _) = - (concat o map str) ["let", deresolve_const classparam, w, "=", + (concat o map Pretty.str) ["let", deresolve_const classparam, w, "=", w ^ "." ^ deresolve_const classparam ^ ";;"]; val type_decl_p = concat [ - str "type", + Pretty.str "type", print_dicttyp (class, ITyVar v), - str "=", + Pretty.str "=", enum_default "unit" ";" "{" "}" ( map print_super_class_field classrels @ map print_classparam_field classparams @@ -693,7 +693,7 @@ then type_decl_p :: map print_classparam_decl classparams else if null classrels andalso null classparams then [type_decl_p] (*work around weakness in export calculation*) - else [concat [str "type", print_dicttyp (class, ITyVar v)]]) + else [concat [Pretty.str "type", print_dicttyp (class, ITyVar v)]]) (Pretty.chunks ( doublesemicolon [type_decl_p] :: map print_classparam_proj classparams @@ -704,12 +704,12 @@ fun print_ocaml_module name decls body = Pretty.chunks2 ( Pretty.chunks [ - str ("module " ^ name ^ " : sig"), - (indent 2 o Pretty.chunks) decls, - str "end = struct" + Pretty.str ("module " ^ name ^ " : sig"), + (Pretty.indent 2 o Pretty.chunks) decls, + Pretty.str "end = struct" ] :: body - @| str ("end;; (*struct " ^ name ^ "*)") + @| Pretty.str ("end;; (*struct " ^ name ^ "*)") ); val literals_ocaml = let @@ -721,7 +721,7 @@ in Literals { literal_string = print_ocaml_string, literal_numeral = numeral_ocaml, - literal_list = enum ";" "[" "]", + literal_list = Pretty.enum ";" "[" "]", infix_cons = (6, "::") } end; @@ -868,7 +868,7 @@ fun fun_syntax print_typ fxy [ty1, ty2] = brackify_infix (1, R) fxy ( print_typ (INFX (1, X)) ty1, - str "->", + Pretty.str "->", print_typ (INFX (1, R)) ty2 ); diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/Code/code_printer.ML Fri Apr 04 22:20:30 2025 +0200 @@ -9,22 +9,16 @@ type itype = Code_Thingol.itype type iterm = Code_Thingol.iterm type const = Code_Thingol.const - type dict = Code_Thingol.dict val eqn_error: theory -> thm option -> string -> 'a val @@ : 'a * 'a -> 'a list val @| : 'a list * 'a -> 'a list - val str: string -> Pretty.T val concat: Pretty.T list -> Pretty.T val brackets: Pretty.T list -> Pretty.T - val enclose: string -> string -> Pretty.T list -> Pretty.T - val commas: Pretty.T list -> Pretty.T list - val enum: string -> string -> string -> Pretty.T list -> Pretty.T val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T val semicolon: Pretty.T list -> Pretty.T val doublesemicolon: Pretty.T list -> Pretty.T - val indent: int -> Pretty.T -> Pretty.T val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T val format: Code_Symbol.T list -> int -> Pretty.T -> Bytes.T @@ -64,6 +58,7 @@ val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option + val parse_target_source: string parser type raw_const_syntax val plain_const_syntax: string -> raw_const_syntax type simple_const_syntax @@ -120,17 +115,13 @@ infixr 5 @|; fun x @@ y = [x, y]; fun xs @| y = xs @ [y]; -val str = Pretty.str; val concat = Pretty.block o Pretty.breaks; val commas = Pretty.commas; -val enclose = Pretty.enclose; -val brackets = enclose "(" ")" o Pretty.breaks; -val enum = Pretty.enum; -fun enum_default default sep l r [] = str default - | enum_default default sep l r xs = enum sep l r xs; -fun semicolon ps = Pretty.block [concat ps, str ";"]; -fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; -val indent = Pretty.indent; +val brackets = Pretty.enclose "(" ")" o Pretty.breaks; +fun enum_default default sep l r [] = Pretty.str default + | enum_default default sep l r xs = Pretty.enum sep l r xs; +fun semicolon ps = Pretty.block [concat ps, Pretty.str ";"]; +fun doublesemicolon ps = Pretty.block [concat ps, Pretty.str ";;"]; fun markup_stmt sym = Pretty.mark (Markup.code_presentationN, [(Markup.stmt_nameN, Code_Symbol.marker sym)]); @@ -250,38 +241,58 @@ | fixity _ _ = true; fun gen_brackify _ [p] = p - | gen_brackify true (ps as _::_) = enclose "(" ")" ps + | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps | gen_brackify false (ps as _::_) = Pretty.block ps; fun brackify fxy_ctxt = gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks; fun brackify_infix infx fxy_ctxt (l, m, r) = - gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r]; + gen_brackify (fixity (INFX infx) fxy_ctxt) [l, Pretty.str " ", m, Pretty.brk 1, r]; fun brackify_block fxy_ctxt p1 ps p2 = let val p = Pretty.block_enclose (p1, p2) ps in if fixity BR fxy_ctxt - then enclose "(" ")" [p] + then Pretty.enclose "(" ")" [p] else p end; fun gen_applify strict opn cls f fxy_ctxt p [] = if strict - then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)] + then gen_brackify (fixity BR fxy_ctxt) [p, Pretty.str (opn ^ cls)] else p | gen_applify strict opn cls f fxy_ctxt p ps = - gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps)); + gen_brackify (fixity BR fxy_ctxt) (p @@ Pretty.enum "," opn cls (map f ps)); fun applify opn = gen_applify false opn; fun tuplify _ _ [] = NONE | tuplify print fxy [x] = SOME (print fxy x) - | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); + | tuplify print _ xs = SOME (Pretty.enum "," "(" ")" (map (print NOBR) xs)); (* generic syntax *) +local + +val target = Markup.language' + {name = "code target language", symbols = false, antiquotes = false}; + +fun markup_target source = + let + val pos = Input.pos_of source; + val _ = + if Position.is_reported_range pos + then Position.report pos (target (Input.is_delimited source)) + else (); + in Input.string_of source end; + +in + +val parse_target_source = Parse.input Parse.embedded >> markup_target; + +end + type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T) -> fixity -> (iterm * itype) list -> Pretty.T); @@ -316,7 +327,7 @@ Constant name => (case const_syntax name of NONE => brackify fxy (print_app_expr some_thm vars app) | SOME (_, Plain_printer s) => - brackify fxy (str s :: map (print_term some_thm vars BR) ts) + brackify fxy (Pretty.str s :: map (print_term some_thm vars BR) ts) | SOME (wanted, Complex_printer print) => let val ((vs_tys, (ts1, rty)), ts2) = @@ -361,7 +372,7 @@ | fillin print (Arg fxy :: mfx) (a :: args) = (print fxy o prep_arg) a :: fillin print mfx args | fillin print (String s :: mfx) args = - str s :: fillin print mfx args + Pretty.str s :: fillin print mfx args | fillin print (Break :: mfx) args = Pretty.brk 1 :: fillin print mfx args; in @@ -400,8 +411,8 @@ (\<^keyword>\infix\ >> K X) || (\<^keyword>\infixl\ >> K L) || (\<^keyword>\infixr\ >> K R) fun parse_mixfix x = - (Parse.string >> read_mixfix - || parse_fixity -- Parse.nat -- Parse.string + (parse_target_source >> read_mixfix + || parse_fixity -- Parse.nat -- parse_target_source >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x; fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s @@ -409,7 +420,7 @@ of_printer (printer_of_mixfix prep_arg (fixity, mfx)); fun parse_tyco_syntax x = - (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x; + (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o Pretty.str) s)) I I) x; val parse_const_syntax = parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst; diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/Code/code_runtime.ML Fri Apr 04 22:20:30 2025 +0200 @@ -55,7 +55,7 @@ val _ = Theory.setup (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)]) #> Code_Target.set_printings (Type_Constructor (\<^type_name>\prop\, - [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))])) + [(target, SOME (0, (K o K o K) (Pretty.str truthN)))])) #> Code_Target.set_printings (Constant (\<^const_name>\Code_Generator.holds\, [(target, SOME (Code_Printer.plain_const_syntax HoldsN))])) #> Code_Target.add_reserved target thisN @@ -685,7 +685,7 @@ | pr pr' _ [ty] = Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] | pr pr' _ tys = - Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] + Code_Printer.concat [Pretty.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] in thy |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))])) @@ -709,9 +709,9 @@ thy |> Code_Target.add_reserved target module_name |> Context.theory_map (compile_ML true code) - |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map - |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map - |> fold (add_eval_const o apsnd Code_Printer.str) const_map + |> fold (add_eval_tyco o apsnd Pretty.str) tyco_map + |> fold (add_eval_constr o apsnd Pretty.str) constr_map + |> fold (add_eval_const o apsnd Pretty.str) const_map | process_reflection (code, _) _ (SOME binding) thy = let val code_binding = Path.map_binding Code_Target.code_path binding; @@ -856,7 +856,7 @@ |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] [] |-> (fn ([Const (const, _)], _) => Code_Target.set_printings (Constant (const, - [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) + [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Pretty.str) ml_name)))])) #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE [])); fun process_file filepath (definienda, thy) = diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/Code/code_scala.ML Fri Apr 04 22:20:30 2025 +0200 @@ -57,29 +57,29 @@ fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true; fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs); fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]" - (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys + (print_typ tyvars NOBR) fxy ((Pretty.str o deresolve) sym) tys and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys) | SOME (_, print) => print (print_typ tyvars) fxy tys) - | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v; + | print_typ tyvars fxy (ITyVar v) = (Pretty.str o lookup_tyvar tyvars) v; fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]); fun print_tupled_typ tyvars ([], ty) = print_typ tyvars NOBR ty | print_tupled_typ tyvars ([ty1], ty2) = - concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2] + concat [print_typ tyvars BR ty1, Pretty.str "=>", print_typ tyvars NOBR ty2] | print_tupled_typ tyvars (tys, ty) = - concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys), - str "=>", print_typ tyvars NOBR ty]; - fun constraint p1 p2 = Pretty.block [p1, str " : ", p2]; - fun print_var vars NONE = str "_" - | print_var vars (SOME v) = (str o lookup_var vars) v; + concat [Pretty.enum "," "(" ")" (map (print_typ tyvars NOBR) tys), + Pretty.str "=>", print_typ tyvars NOBR ty]; + fun constraint p1 p2 = Pretty.block [p1, Pretty.str " : ", p2]; + fun print_var vars NONE = Pretty.str "_" + | print_var vars (SOME v) = (Pretty.str o lookup_var vars) v; fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d and applify_plain_dict tyvars (Dict_Const (inst, dss)) = - applify_dictss tyvars ((str o deresolve o Class_Instance) inst) (map snd dss) + applify_dictss tyvars ((Pretty.str o deresolve o Class_Instance) inst) (map snd dss) | applify_plain_dict tyvars (Dict_Var { var, class, ... }) = - Pretty.block [str "implicitly", - enclose "[" "]" [Pretty.block [(str o deresolve_class) class, - enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]] + Pretty.block [Pretty.str "implicitly", + Pretty.enclose "[" "]" [Pretty.block [(Pretty.str o deresolve_class) class, + Pretty.enclose "[" "]" [(Pretty.str o lookup_tyvar tyvars) var]]]] and applify_dictss tyvars p dss = applify "(" ")" (applify_dict tyvars) NOBR p (flat dss) fun print_term tyvars is_pat some_thm vars fxy (IConst const) = @@ -110,8 +110,8 @@ val vars' = intro_vars (the_list some_v) vars; in (concat [ - enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)], - str "=>" + Pretty.enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)], + Pretty.str "=>" ], vars') end and print_app tyvars is_pat some_thm vars fxy @@ -131,12 +131,12 @@ (gen_applify (is_constr sym) "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) - NOBR ((str o deresolve) sym) typargs') ts) dicts) + NOBR ((Pretty.str o deresolve) sym) typargs') ts) dicts) | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts (applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) - NOBR (str s) typargs') ts) dicts) + NOBR (Pretty.str s) typargs') ts) dicts) | SOME (k, Complex_printer print) => (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take k dom)) @@ -148,21 +148,21 @@ print' fxy ts else Pretty.block (print' BR ts1 :: map (fn t => Pretty.block - [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts2) + [Pretty.str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, Pretty.str ")"]) ts2) else print_term tyvars is_pat some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty)) end and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p and print_case tyvars some_thm vars fxy { clauses = [], ... } = - (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"] + (brackify fxy o Pretty.breaks o map Pretty.str) ["sys.error(\"empty case\")"] | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) = let val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr); fun print_match_val ((pat, ty), t) vars = vars |> print_bind tyvars some_thm BR pat - |>> (fn p => (false, concat [str "val", p, str "=", + |>> (fn p => (false, concat [Pretty.str "val", p, Pretty.str "=", constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars BR ty)])); fun print_match_seq t vars = ((true, print_term tyvars false some_thm vars NOBR t), vars); @@ -177,30 +177,30 @@ val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)]; fun insert_seps [(_, p)] = [p] | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) = - (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps - in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end + (if sep then Pretty.block [p, Pretty.str ";"] else p) :: insert_seps seps_ps + in brackify_block fxy (Pretty.str "{") (insert_seps all_seps_ps) (Pretty.str "}") end | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } = let fun print_select (pat, body) = let val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars; val p_body = print_term tyvars false some_thm vars' NOBR body - in concat [str "case", p_pat, str "=>", p_body] end; + in concat [Pretty.str "case", p_pat, Pretty.str "=>", p_body] end; in map print_select clauses - |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match {"], str "}") + |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, Pretty.str "match {"], Pretty.str "}") |> single - |> enclose "(" ")" + |> Pretty.enclose "(" ")" end; fun print_context tyvars vs s = applify "[" "]" - (fn (v, sort) => (Pretty.block o map str) + (fn (v, sort) => (Pretty.block o map Pretty.str) (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) - NOBR (str s) vs; + NOBR (Pretty.str s) vs; fun print_defhead tyvars vars const vs params tys ty = - concat [str "def", constraint (applify "(" ")" (fn (param, ty) => - constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) + concat [Pretty.str "def", constraint (applify "(" ")" (fn (param, ty) => + constraint ((Pretty.str o lookup_var vars) param) (print_typ tyvars NOBR ty)) NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty), - str "="]; + Pretty.str "="]; fun print_def const (vs, ty) [] = let val (tys, ty') = Code_Thingol.unfold_fun ty; @@ -209,7 +209,7 @@ val vars = intro_vars params reserved; in concat [print_defhead tyvars vars const vs params tys ty', - str ("sys.error(" ^ print_scala_string const ^ ")")] + Pretty.str ("sys.error(" ^ print_scala_string const ^ ")")] end | print_def const (vs, ty) eqs = let @@ -231,7 +231,7 @@ val vars2 = intro_vars params vars1; val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty; fun tuplify [p] = p - | tuplify ps = enum "," "(" ")" ps; + | tuplify ps = Pretty.enum "," "(" ")" ps; fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t; fun print_clause (eq as ((ts, _), (some_thm, _))) = @@ -239,20 +239,20 @@ val vars' = intro_vars (build (fold Code_Thingol.add_varnames ts)) vars1; in - concat [str "case", + concat [Pretty.str "case", tuplify (map (print_term tyvars true some_thm vars' NOBR) ts), - str "=>", print_rhs vars' eq] + Pretty.str "=>", print_rhs vars' eq] end; val head = print_defhead tyvars vars2 const vs params tys' ty'; in if simple then concat [head, print_rhs vars2 (hd eqs)] else Pretty.block_enclose - (concat [head, tuplify (map (str o lookup_var vars2) params), - str "match {"], str "}") + (concat [head, tuplify (map (Pretty.str o lookup_var vars2) params), + Pretty.str "match {"], Pretty.str "}") (map print_clause eqs) end; - val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant; + val print_method = Pretty.str o enclose "`" "`" o deresolve_full o Constant; fun print_inst class (tyco, { vs, inst_params, superinst_params }) = let val tyvars = intro_tyvars vs reserved; @@ -264,22 +264,22 @@ val vars = intro_vars auxs reserved; val (aux_dom1, aux_dom2) = chop dom_length aux_dom; fun abstract_using [] = [] - | abstract_using aux_dom = [enum "," "(" ")" - (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux) - (print_typ tyvars NOBR ty)) aux_dom), str "=>"]; + | abstract_using aux_dom = [Pretty.enum "," "(" ")" + (map (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux) + (print_typ tyvars NOBR ty)) aux_dom), Pretty.str "=>"]; val aux_abstr1 = abstract_using aux_dom1; val aux_abstr2 = abstract_using aux_dom2; in - concat ([str "val", print_method classparam, str "="] + concat ([Pretty.str "val", print_method classparam, Pretty.str "="] @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)) end; in - Pretty.block_enclose (concat [str "implicit def", + Pretty.block_enclose (concat [Pretty.str "implicit def", constraint (print_context tyvars vs ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class))) (print_dicttyp tyvars classtyp), - str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") + Pretty.str "=", Pretty.str "new", print_dicttyp tyvars classtyp, Pretty.str "{"], Pretty.str "}") (map print_classparam_instance (inst_params @ superinst_params)) end; fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) = @@ -288,29 +288,29 @@ let val tyvars = intro_tyvars (map (rpair []) vs) reserved; fun print_co ((co, vs_args), tys) = - concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR - (str ("final case class " ^ deresolve_const co)) vs_args) - @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) + concat [Pretty.block ((applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR + (Pretty.str ("final case class " ^ deresolve_const co)) vs_args) + @@ Pretty.enum "," "(" ")" (map (fn (v, arg) => constraint (Pretty.str v) (print_typ tyvars NOBR arg)) (Name.invent_names (snd reserved) "a" tys))), - str "extends", - applify "[" "]" (str o lookup_tyvar tyvars) NOBR - ((str o deresolve_tyco) tyco) vs + Pretty.str "extends", + applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR + ((Pretty.str o deresolve_tyco) tyco) vs ]; in - Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars) - NOBR (str ("abstract sealed class " ^ deresolve_tyco tyco)) vs + Pretty.chunks (applify "[" "]" (Pretty.str o lookup_tyvar tyvars) + NOBR (Pretty.str ("abstract sealed class " ^ deresolve_tyco tyco)) vs :: map print_co cos) end | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) = let val tyvars = intro_tyvars [(v, [class])] reserved; fun add_typarg s = Pretty.block - [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"]; + [Pretty.str s, Pretty.str "[", (Pretty.str o lookup_tyvar tyvars) v, Pretty.str "]"]; fun print_super_classes [] = NONE - | print_super_classes classrels = SOME (concat (str "extends" - :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels))); + | print_super_classes classrels = SOME (concat (Pretty.str "extends" + :: separate (Pretty.str "with") (map (add_typarg o deresolve_class o snd) classrels))); fun print_classparam_val (classparam, ty) = - concat [str "val", constraint (print_method classparam) + concat [Pretty.str "val", constraint (print_method classparam) ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)]; fun print_classparam_def (classparam, ty) = let @@ -320,23 +320,23 @@ val auxs = Name.invent (snd proto_vars) "a" (length tys); val vars = intro_vars auxs proto_vars; in - concat [str "def", constraint (Pretty.block [applify "(" ")" - (fn (aux, ty) => constraint ((str o lookup_var vars) aux) + concat [Pretty.str "def", constraint (Pretty.block [applify "(" ")" + (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux) (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam)) - (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ", - add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=", - applify "(" ")" (str o lookup_var vars) NOBR - (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs] + (auxs ~~ tys), Pretty.str "(implicit ", Pretty.str implicit_name, Pretty.str ": ", + add_typarg (deresolve_class class), Pretty.str ")"]) (print_typ tyvars NOBR ty), Pretty.str "=", + applify "(" ")" (Pretty.str o lookup_var vars) NOBR + (Pretty.block [Pretty.str implicit_name, Pretty.str ".", print_method classparam]) auxs] end; in Pretty.chunks ( (Pretty.block_enclose - (concat ([str "trait", (add_typarg o deresolve_class) class] - @ the_list (print_super_classes classrels) @ [str "{"]), str "}") + (concat ([Pretty.str "trait", (add_typarg o deresolve_class) class] + @ the_list (print_super_classes classrels) @ [Pretty.str "{"]), Pretty.str "}") (map print_classparam_val classparams)) :: map print_classparam_def classparams @| Pretty.block_enclose - (str ("object " ^ deresolve_class class ^ " {"), str "}") + (Pretty.str ("object " ^ deresolve_class class ^ " {"), Pretty.str "}") (map (print_inst class) insts) ) end; @@ -432,8 +432,8 @@ (* print modules *) fun print_module _ base _ ps = Pretty.chunks2 - (str ("object " ^ base ^ " {") - :: ps @| str ("} /* object " ^ base ^ " */")); + (Pretty.str ("object " ^ base ^ " {") + :: ps @| Pretty.str ("} /* object " ^ base ^ " */")); (* serialization *) val p = Pretty.chunks2 (map snd includes @@ -456,7 +456,7 @@ in Literals { literal_string = print_scala_string, literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")", - literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps], + literal_list = fn [] => Pretty.str "Nil" | ps => Pretty.block [Pretty.str "List", Pretty.enum "," "(" ")" ps], infix_cons = (6, "::") } end; @@ -475,7 +475,7 @@ [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => brackify_infix (1, R) fxy ( print_typ BR ty1 (*product type vs. tupled arguments!*), - str "=>", + Pretty.str "=>", print_typ (INFX (1, R)) ty2 )))])) #> fold (Code_Target.add_reserved target) [ diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/Code/code_target.ML Fri Apr 04 22:20:30 2025 +0200 @@ -9,9 +9,6 @@ val cert_tyco: Proof.context -> string -> string val read_tyco: Proof.context -> string -> string - datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; - val next_export: theory -> string * theory - val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory @@ -47,16 +44,18 @@ -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm -> ((string list * Bytes.T) list * string) * (Code_Symbol.T -> string option) + datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; type serializer - type literals = Code_Printer.literals type language type ancestry val assert_target: theory -> string -> string val add_language: string * language -> theory -> theory val add_derived_target: string * ancestry -> theory -> theory - val the_literals: Proof.context -> string -> literals + val the_literals: Proof.context -> string -> Code_Printer.literals + val parse_args: 'a parser -> Token.T list -> 'a val default_code_width: int Config.T + val next_export: theory -> string * theory type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl @@ -72,7 +71,6 @@ open Basic_Code_Symbol; open Basic_Code_Thingol; -type literals = Code_Printer.literals; type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl = (string * (string * 'a option) list, string * (string * 'b option) list, class * (string * 'c option) list, (class * class) * (string * 'd option) list, @@ -172,7 +170,7 @@ -> Code_Symbol.T list -> pretty_modules * (Code_Symbol.T -> string option); -type language = {serializer: serializer, literals: literals, +type language = {serializer: serializer, literals: Code_Printer.literals, check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string}, evaluation_args: Token.T list}; @@ -652,7 +650,16 @@ (* custom printings *) -fun arrange_printings prep_syms ctxt = +datatype target_source = Literal of string | File of Path.T + +local + +val format_source = Pretty.block0 o Pretty.fbreaks o map Pretty.str o split_lines; + +fun eval_source (Literal s) = s + | eval_source (File p) = File.read p; + +fun arrange_printings prep_syms prep_source ctxt = let val thy = Proof_Context.theory_of ctxt; fun arrange check (sym, target_syns) = @@ -662,23 +669,26 @@ Code_Symbol.maps_attr' (arrange check_const_syntax) (arrange check_tyco_syntax) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) - (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_syms) => - (Pretty.block0 (Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))), - map (prep_syms ctxt) raw_syms))) + (arrange (fn ctxt => fn _ => fn _ => fn (source, raw_syms) => + (format_source (prep_source source), map (prep_syms ctxt) raw_syms))) end; -fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms ctxt; +fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms I ctxt; -fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms ctxt; +fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms eval_source ctxt; fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn); fun gen_set_printings prep_print_decl raw_print_decls thy = fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy; +in + val set_printings = gen_set_printings cert_printings; val set_printings_cmd = gen_set_printings read_printings; +end; + (* concrete syntax *) @@ -731,6 +741,9 @@ Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma") (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module)); +val parse_target_source = Code_Printer.parse_target_source >> Literal + || \<^keyword>\file\ |-- Parse.path >> (File o Path.explode); + val code_expr_argsP = Scan.optional (\<^keyword>\(\ |-- Parse.args --| \<^keyword>\)\) []; fun code_expr_inP (all_public, raw_cs) = @@ -762,8 +775,8 @@ val _ = Outer_Syntax.command \<^command_keyword>\code_printing\ "declare dedicated printing for code symbols" (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax) - Parse.string (Parse.minus >> K ()) (Parse.minus >> K ()) - (Parse.embedded -- Scan.optional (\<^keyword>\for\ |-- parse_simple_symbols) []) + Code_Printer.parse_target_source (Parse.minus >> K ()) (Parse.minus >> K ()) + (parse_target_source -- Scan.optional (\<^keyword>\for\ |-- parse_simple_symbols) []) >> (Toplevel.theory o fold set_printings_cmd)); val _ = diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/Code/code_thingol.ML Fri Apr 04 22:20:30 2025 +0200 @@ -187,13 +187,13 @@ | _ => NONE); val unfold_abs = unfoldr - (fn (v `|=> (t, _)) => SOME (v, t) + (fn (v_ty `|=> (t, _)) => SOME (v_ty, t) | _ => NONE); -fun unfold_abs_typed (v_ty `|=> body) = +fun unfold_abs_typed (v_ty `|=> t_ty) = unfoldr - (fn (v_ty `|=> body, _) => SOME (v_ty, body) - | _ => NONE) body + (fn (v_ty `|=> t_ty, _) => SOME (v_ty, t_ty) + | _ => NONE) t_ty |> apfst (cons v_ty) |> SOME | unfold_abs_typed _ = NONE diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/nbe.ML Fri Apr 04 22:20:30 2025 +0200 @@ -153,7 +153,7 @@ (** the semantic universe **) (* - Functions are given by their semantical function value. To avoid + Functions are given by their semantic function value. To avoid trouble with the ML-type system, these functions have the most generic type, that is "Univ list -> Univ". The calling convention is that the arguments come as a list, the last argument first. In @@ -255,9 +255,6 @@ val univs_cookie = (get_result, put_result, name_put); -fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value" - | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym) - ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i; fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n; fun nbe_bound v = "v_" ^ v; fun nbe_bound_optional NONE = "_" @@ -267,13 +264,8 @@ (*note: these three are the "turning spots" where proper argument order is established!*) fun nbe_apps t [] = t | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; -fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts); -fun nbe_apps_constr ctxt idx_of c ts = - let - val c' = if Config.get ctxt trace - then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)" - else string_of_int (idx_of c); - in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end; +fun nbe_apps_local c ts = c `$` ml_list (rev ts); +fun nbe_apps_constr c ts = name_const `$` ("(" ^ c ^ ", " ^ ml_list (rev ts) ^ ")"); fun nbe_abss 0 f = f `$` ml_list [] | nbe_abss n f = name_abss `$$` [string_of_int n, f]; @@ -288,107 +280,122 @@ (* code generation *) -fun assemble_eqnss ctxt idx_of deps eqnss = +fun subst_nonlin_vars args = let - fun prep_eqns (c, (vs, eqns)) = + val vs = (fold o Code_Thingol.fold_varnames) + (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args []; + val names = Name.make_context (map fst vs); + val (vs_renames, _) = fold_map (fn (v, k) => if k > 1 + then Name.invent' v (k - 1) #>> (fn vs => (v, vs)) + else pair (v, [])) vs names; + val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames; + fun subst_vars (t as IConst _) samepairs = (t, samepairs) + | subst_vars (t as IVar NONE) samepairs = (t, samepairs) + | subst_vars (t as IVar (SOME v)) samepairs = (case AList.lookup (op =) samepairs v + of SOME v' => (IVar (SOME v'), AList.delete (op =) v samepairs) + | NONE => (t, samepairs)) + | subst_vars (t1 `$ t2) samepairs = samepairs + |> subst_vars t1 + ||>> subst_vars t2 + |>> (op `$) + | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs; + val (args', _) = fold_map subst_vars args samepairs; + in (samepairs, args') end; + +fun preprocess_eqns (sym, (vs, eqns)) = + let + val dict_params = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; + val num_args = length dict_params + ((length o fst o hd) eqns); + val default_params = map nbe_default (Name.invent_global "a" (num_args - length dict_params)); + in (sym, (num_args, (dict_params, (map o apfst) subst_nonlin_vars eqns, default_params))) end; + +fun assemble_preprocessed_eqnss ctxt idx_of_const deps eqnss = + let + fun fun_ident 0 (Code_Symbol.Constant "") = "nbe_value" + | fun_ident i sym = "c_" ^ string_of_int (idx_of_const sym) + ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i; + fun constr_fun_ident c = + if Config.get ctxt trace + then string_of_int (idx_of_const c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)" + else string_of_int (idx_of_const c); + + fun apply_local i sym = nbe_apps_local (fun_ident i sym); + fun apply_constr sym = nbe_apps_constr (constr_fun_ident sym); + + fun assemble_constapp sym dicts ts = let - val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; - val num_args = length dicts + ((length o fst o hd) eqns); - in (c, (num_args, (dicts, eqns))) end; - val eqnss' = map prep_eqns eqnss; - - fun assemble_constapp sym dss ts = - let - val ts' = (maps o map) assemble_dict dss @ ts; - in case AList.lookup (op =) eqnss' sym + val ts' = (maps o map) assemble_dict dicts @ ts; + in case AList.lookup (op =) eqnss sym of SOME (num_args, _) => if num_args <= length ts' then let val (ts1, ts2) = chop num_args ts' - in nbe_apps (nbe_apps_local idx_of 0 sym ts1) ts2 - end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts' + in nbe_apps (apply_local 0 sym ts1) ts2 + end else nbe_apps (nbe_abss num_args (fun_ident 0 sym)) ts' | NONE => if member (op =) deps sym - then nbe_apps (nbe_fun idx_of 0 sym) ts' - else nbe_apps_constr ctxt idx_of sym ts' + then nbe_apps (fun_ident 0 sym) ts' + else apply_constr sym ts' end and assemble_classrels classrels = fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels and assemble_dict (Dict (classrels, x)) = assemble_classrels classrels (assemble_plain_dict x) - and assemble_plain_dict (Dict_Const (inst, dss)) = - assemble_constapp (Class_Instance inst) (map snd dss) [] + and assemble_plain_dict (Dict_Const (inst, dicts)) = + assemble_constapp (Class_Instance inst) (map snd dicts) [] | assemble_plain_dict (Dict_Var { var, index, ... }) = nbe_dict var index + fun assemble_constmatch sym dicts ts = + apply_constr sym ((maps o map) (K "_") dicts @ ts); + fun assemble_iterm constapp = let - fun of_iterm match_cont t = + fun of_iterm match_continuation t = let val (t', ts) = Code_Thingol.unfold_app t - in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end - and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts - | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts - | of_iapp match_cont ((v, _) `|=> (t, _)) ts = + in of_iapp match_continuation t' (fold_rev (cons o of_iterm NONE) ts []) end + and of_iapp match_continuation (IConst { sym, dicts, ... }) ts = constapp sym dicts ts + | of_iapp match_continuation (IVar v) ts = nbe_apps (nbe_bound_optional v) ts + | of_iapp match_continuation ((v, _) `|=> (t, _)) ts = nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts - | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts = + | of_iapp match_continuation (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts = nbe_apps (ml_cases (of_iterm NONE t) - (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses - @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts + (map (fn (p, t) => (of_iterm NONE p, of_iterm match_continuation t)) clauses + @ [("_", case match_continuation of SOME s => s | NONE => of_iterm NONE t0)])) ts in of_iterm end; - fun subst_nonlin_vars args = - let - val vs = (fold o Code_Thingol.fold_varnames) - (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args []; - val names = Name.make_context (map fst vs); - val (vs_renames, _) = fold_map (fn (v, k) => if k > 1 - then Name.invent' v (k - 1) #>> (fn vs => (v, vs)) - else pair (v, [])) vs names; - val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames; - fun subst_vars (t as IConst _) samepairs = (t, samepairs) - | subst_vars (t as IVar NONE) samepairs = (t, samepairs) - | subst_vars (t as IVar (SOME v)) samepairs = (case AList.lookup (op =) samepairs v - of SOME v' => (IVar (SOME v'), AList.delete (op =) v samepairs) - | NONE => (t, samepairs)) - | subst_vars (t1 `$ t2) samepairs = samepairs - |> subst_vars t1 - ||>> subst_vars t2 - |>> (op `$) - | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs; - val (args', _) = fold_map subst_vars args samepairs; - in (samepairs, args') end; + val assemble_args = map (assemble_iterm assemble_constmatch NONE); + val assemble_rhs = assemble_iterm assemble_constapp; - fun assemble_eqn sym dicts default_args (i, (args, rhs)) = + fun assemble_eqn sym dict_params default_params (i, ((samepairs, args), rhs)) = let - val match_cont = if Code_Symbol.is_value sym then NONE - else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args)); - val assemble_arg = assemble_iterm - (fn sym' => fn dss => fn ts => nbe_apps_constr ctxt idx_of sym' ((maps o map) (K "_") - dss @ ts)) NONE; - val assemble_rhs = assemble_iterm assemble_constapp match_cont; - val (samepairs, args') = subst_nonlin_vars args; - val s_args = map assemble_arg args'; - val s_rhs = if null samepairs then assemble_rhs rhs + val default_rhs = apply_local (i + 1) sym (dict_params @ default_params); + val s_args = assemble_args args; + val s_rhs = if null samepairs then assemble_rhs (SOME default_rhs) rhs else ml_if (ml_and (map nbe_same samepairs)) - (assemble_rhs rhs) (the match_cont); - val eqns = case match_cont - of NONE => [([ml_list (rev (dicts @ s_args))], s_rhs)] - | SOME default_rhs => - [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs), - ([ml_list (rev (dicts @ default_args))], default_rhs)] - in (nbe_fun idx_of i sym, eqns) end; + (assemble_rhs (SOME default_rhs) rhs) default_rhs; + val eqns = [([ml_list (rev (dict_params @ map2 ml_as default_params s_args))], s_rhs), + ([ml_list (rev (dict_params @ default_params))], default_rhs)] + in (fun_ident i sym, eqns) end; + + fun assemble_default_eqn sym dict_params default_params i = + (fun_ident i sym, + [([ml_list (rev (dict_params @ default_params))], apply_constr sym (dict_params @ default_params))]); + + fun assemble_value_equation sym dict_params (([], args), rhs) = + (fun_ident 0 sym, [([ml_list (rev (dict_params @ assemble_args args))], assemble_rhs NONE rhs)]); - fun assemble_eqns (sym, (num_args, (dicts, eqns))) = - let - val default_args = map nbe_default (Name.invent_global "a" (num_args - length dicts)); - val eqns' = map_index (assemble_eqn sym dicts default_args) eqns - @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym, - [([ml_list (rev (dicts @ default_args))], - nbe_apps_constr ctxt idx_of sym (dicts @ default_args))])]); - in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end; + fun assemble_eqns (sym, (num_args, (dict_params, eqns, default_params))) = + (if Code_Symbol.is_value sym then [assemble_value_equation sym dict_params (the_single eqns)] + else map_index (assemble_eqn sym dict_params default_params) eqns + @ [assemble_default_eqn sym dict_params default_params (length eqns)], + nbe_abss num_args (fun_ident 0 sym)); - val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; - val deps_vars = ml_list (map (nbe_fun idx_of 0) deps); + val (fun_vars, fun_vals) = map_split assemble_eqns eqnss; + val deps_vars = ml_list (map (fun_ident 0) deps); in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end; +fun assemble_eqnss ctxt idx_of_const deps eqnss = + assemble_preprocessed_eqnss ctxt idx_of_const deps (map preprocess_eqns eqnss); + (* compilation of equations *) @@ -397,26 +404,26 @@ let val (deps, deps_vals) = split_list (map_filter (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps); - val idx_of = raw_deps + val idx_of_const = raw_deps |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep))) |> AList.lookup (op =) |> (fn f => the o f); - val s = assemble_eqnss ctxt idx_of deps eqnss; - val cs = map fst eqnss; + val s = assemble_eqnss ctxt idx_of_const deps eqnss; + val syms = map fst eqnss; in s |> traced ctxt (fn s => "\n--- code to be evaluated:\n" ^ s) |> pair "" |> Code_Runtime.value ctxt univs_cookie |> (fn f => f deps_vals) - |> (fn univs => cs ~~ univs) + |> (fn univs => syms ~~ univs) end; (* extraction of equations from statements *) -fun dummy_const sym dss = - IConst { sym = sym, typargs = [], dicts = dss, +fun dummy_const sym dicts = + IConst { sym = sym, typargs = [], dicts = dicts, dom = [], annotation = NONE, range = ITyVar "" }; fun eqns_of_stmt (_, Code_Thingol.NoStmt) = @@ -444,17 +451,17 @@ [] | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) = [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] `$$ - map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) (map snd dss)) superinsts + map (fn (class, dicts) => dummy_const (Class_Instance (tyco, class)) (map snd dicts)) superinsts @ map (IConst o fst o snd o fst) inst_params)]))]; (* compilation of whole programs *) -fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) = +fun ensure_const_idx name (nbe_program, (maxidx, const_tab)) = if can (Code_Symbol.Graph.get_node nbe_program) name - then (nbe_program, (maxidx, idx_tab)) + then (nbe_program, (maxidx, const_tab)) else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program, - (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab)); + (maxidx + 1, Inttab.update_new (maxidx, name) const_tab)); fun compile_stmts ctxt stmts_deps = let @@ -472,16 +479,17 @@ fold ensure_const_idx refl_deps #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps #> compile - #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ)))) + #-> fold (fn (sym, univ) => (Code_Symbol.Graph.map_node sym o apfst) (K (SOME univ)))) end; fun compile_program { ctxt, program } = let - fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names - then (nbe_program, (maxidx, idx_tab)) - else (nbe_program, (maxidx, idx_tab)) - |> compile_stmts ctxt (map (fn name => ((name, Code_Symbol.Graph.get_node program name), - Code_Symbol.Graph.immediate_succs program name)) names); + fun add_stmts names (nbe_program, (maxidx, const_tab)) = + if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names + then (nbe_program, (maxidx, const_tab)) + else (nbe_program, (maxidx, const_tab)) + |> compile_stmts ctxt (map (fn sym => ((sym, Code_Symbol.Graph.get_node program sym), + Code_Symbol.Graph.immediate_succs program sym)) names); in fold_rev add_stmts (Code_Symbol.Graph.strong_conn program) end; @@ -501,25 +509,25 @@ |> (fn t => apps t (rev dict_frees)) end; -fun reconstruct_term ctxt (idx_tab : Code_Symbol.T Inttab.table) t = +fun reconstruct_term ctxt (const_tab : Code_Symbol.T Inttab.table) t = let fun take_until f [] = [] | take_until f (x :: xs) = if f x then [] else x :: take_until f xs; fun is_dict (Const (idx, _)) = - (case Inttab.lookup idx_tab idx of + (case Inttab.lookup const_tab idx of SOME (Constant _) => false | _ => true) | is_dict (DFree _) = true | is_dict _ = false; fun const_of_idx idx = - case Inttab.lookup idx_tab idx of SOME (Constant const) => const; + case Inttab.lookup const_tab idx of SOME (Constant const) => const; fun of_apps bounds (t, ts) = fold_map (of_univ bounds) ts #>> (fn ts' => list_comb (t, rev ts')) and of_univ bounds (Const (idx, ts)) typidx = let + val const = const_of_idx idx; val ts' = take_until is_dict ts; - val const = const_of_idx idx; val T = map_type_tvar (fn ((v, i), _) => Type_Infer.param typidx (v ^ string_of_int i, [])) (Sign.the_const_type (Proof_Context.theory_of ctxt) const); @@ -533,12 +541,12 @@ |-> (fn t' => pair (Term.Abs ("u", dummyT, t'))) in of_univ 0 t 0 |> fst end; -fun compile_and_reconstruct_term { ctxt, nbe_program, idx_tab, deps, term } = +fun compile_and_reconstruct_term { ctxt, nbe_program, const_tab, deps, term } = compile_term { ctxt = ctxt, nbe_program = nbe_program, deps = deps, term = term } - |> reconstruct_term ctxt idx_tab; + |> reconstruct_term ctxt const_tab; -fun normalize_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps = +fun normalize_term (nbe_program, const_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps = let val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt); val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); @@ -553,7 +561,7 @@ else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t'); in Code_Preproc.timed "computing NBE expression" #ctxt compile_and_reconstruct_term - { ctxt = ctxt, nbe_program = nbe_program, idx_tab = idx_tab, deps = deps, term = (vs, t) } + { ctxt = ctxt, nbe_program = nbe_program, const_tab = const_tab, deps = deps, term = (vs, t) } |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t) |> type_infer |> traced ctxt (fn t => "Types inferred:\n" ^ string_of_term t) @@ -572,11 +580,11 @@ fun compile ignore_cache ctxt program = let - val (nbe_program, (_, idx_tab)) = + val (nbe_program, (_, const_tab)) = Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) (Code_Preproc.timed "compiling NBE program" #ctxt compile_program { ctxt = ctxt, program = program }); - in (nbe_program, idx_tab) end; + in (nbe_program, const_tab) end; (* evaluation oracle *) @@ -590,11 +598,11 @@ val (_, raw_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\normalization_by_evaluation\, - fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) => - mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))); + fn (nbe_program_const_tab, ctxt, vs_ty_t, deps, ct) => + mk_equals ctxt ct (normalize_term nbe_program_const_tab ctxt (Thm.term_of ct) vs_ty_t deps))); -fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct = - raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct); +fun oracle nbe_program_const_tab ctxt vs_ty_t deps ct = + raw_oracle (nbe_program_const_tab, ctxt, vs_ty_t, deps, ct); fun dynamic_conv ctxt = lift_triv_classes_conv ctxt (fn ctxt' => Code_Thingol.dynamic_conv ctxt' (fn program => diff -r 8b5dd705dfef -r 8f6dc8483b1a src/Tools/try.ML --- a/src/Tools/try.ML Fri Apr 04 22:20:23 2025 +0200 +++ b/src/Tools/try.ML Fri Apr 04 22:20:30 2025 +0200 @@ -20,11 +20,7 @@ (* helpers *) -fun serial_commas _ [] = ["??"] - | serial_commas _ [s] = [s] - | serial_commas conj [s1, s2] = [s1, conj, s2] - | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] - | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss; +val serial_commas = Try0.serial_commas (* configuration *)