merged

--- a/NEWS	Mon Aug 26 21:59:35 2024 +0100
+++ b/NEWS	Mon Aug 26 22:14:19 2024 +0100
@@ -9,6 +9,13 @@
 
 ** General **
 
+* Inner syntax translations now support formal dependencies via commands
+'syntax_types' or 'syntax_consts'. This is essentially an abstract
+specification of the effect of 'translations' (or translation functions
+in ML). Most Isabelle theories have been adapted accordingly, such that
+hyperlinks work properly e.g. for "['a, 'b] \<Rightarrow> 'c" or "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> C" in
+Pure, and "\<forall>x\<in>A. B x" or "\<exists>x\<in>A. B x" in HOL.
+
 * The Simplifier now supports special "congprocs", using keyword
 'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
 antiquotation of the same name). See also

--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Aug 26 21:59:35 2024 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Aug 26 22:14:19 2024 +0100
@@ -1078,6 +1078,8 @@
     @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command_def "syntax_types"} & : & \<open>theory \<rightarrow> theory\<close> \\
+    @{command_def "syntax_consts"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@@ -1089,8 +1091,9 @@
   raw syntax declarations provide full access to the priority grammar of the
   inner syntax, without any sanity checks. This includes additional syntactic
   categories (via @{command nonterminal}) and free-form grammar productions
-  (via @{command syntax}). Additional syntax translations (or macros, via
-  @{command translations}) are required to turn resulting parse trees into
+  (via @{command syntax} with formal dependencies via @{command syntax_types}
+  and @{command syntax_consts}). Additional syntax translations (or macros,
+  via @{command translations}) are required to turn resulting parse trees into
   proper representations of formal entities again.
 
   \<^rail>\<open>
@@ -1098,6 +1101,8 @@
     ;
     (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
     ;
+    (@@{command syntax_types} | @@{command syntax_consts}) (syntaxdeps + @'and')
+    ;
     (@@{command translations} | @@{command no_translations})
       (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +)
     ;
@@ -1106,6 +1111,8 @@
     ;
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
+    syntaxdeps: (@{syntax name}+) ('==' | '\<rightleftharpoons>') (@{syntax name}+)
+    ;
     transpat: ('(' @{syntax name} ')')? @{syntax string}
   \<close>
 
@@ -1157,6 +1164,14 @@
   translations) resulting from \<open>decls\<close>, which are interpreted in the same
   manner as for @{command "syntax"} above.
 
+  \<^descr> @{command "syntax_types"}~\<open>syntax \<rightleftharpoons> types\<close> and @{command
+  "syntax_consts"}~\<open>syntax \<rightleftharpoons> consts\<close> declare dependencies of syntax constants
+  wrt.\ formal entities of the logic: multiple names may be given on both
+  sides. This tells the inner-syntax engine how to markup concrete syntax, to
+  support hyperlinks in the browser or editor. It is essentially an abstract
+  specification of the effect of translation rules (see below) or translation
+  functions (see \secref{sec:tr-funs}).
+
   \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
   (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
   theory context maintains two independent lists translation rules: parse

--- a/src/HOL/Data_Structures/Leftist_Heap_List.thy	Mon Aug 26 21:59:35 2024 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap_List.thy	Mon Aug 26 22:14:19 2024 +0100
@@ -155,7 +155,7 @@
 qed
 
 lemma T_lheap_list: assumes "length xs = 2 ^ k"
-shows "T_lheap_list xs \<le> 5 * length xs"
+shows "T_lheap_list xs \<le> 5 * length xs - 2 * log 2 (length xs)"
 proof -
   let ?ts = "map (\<lambda>x. Node Leaf (x,1) Leaf) xs"
   have "T_lheap_list xs = T_merge_all ?ts" by simp
@@ -172,10 +172,8 @@
     by (simp add:log_nat_power algebra_simps)
   also have "\<dots> = 5*(2::real)^k - (2::real)*k - 5"
     using summation by (simp)
-  also have "\<dots> \<le> 5*(2::real)^k"
-    by linarith
   finally show ?thesis
-    using assms of_nat_le_iff by fastforce
+    using assms of_nat_le_iff by simp
 qed
 
 end
\ No newline at end of file

--- a/src/HOL/Data_Structures/Selection.thy	Mon Aug 26 21:59:35 2024 +0100
+++ b/src/HOL/Data_Structures/Selection.thy	Mon Aug 26 22:14:19 2024 +0100
@@ -633,9 +633,7 @@
 
 subsection \<open>Running time analysis\<close>
 
-fun T_partition3 :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
-  "T_partition3 x [] = 1"
-| "T_partition3 x (y # ys) = T_partition3 x ys + 1"
+time_fun partition3 equations partition3_code
 
 lemma T_partition3_eq: "T_partition3 x xs = length xs + 1"
   by (induction x xs rule: T_partition3.induct) auto

--- a/src/HOL/GCD.thy	Mon Aug 26 21:59:35 2024 +0100
+++ b/src/HOL/GCD.thy	Mon Aug 26 22:14:19 2024 +0100
@@ -2933,7 +2933,7 @@
 
 end
 
-lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char TYPE('a) = 0"
+lemma (in semiring_char_0) CHAR_eq_0 [simp]: "CHAR('a) = 0"
   by (simp add: CHAR_eq0_iff)