# HG changeset patch # User paulson # Date 1724706859 -3600 # Node ID 94bc8f62c835f06b03c7947c8beb1587695f8fe5 # Parent 3a9e570c916d34f44b16a8581dbea982f24215e7# Parent 623d46973cbe32b60af6c0b78d06e96d1489db36 merged diff -r 623d46973cbe -r 94bc8f62c835 NEWS --- 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] \ 'c" or "\A; B\ \ C" in +Pure, and "\x\A. B x" or "\x\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 diff -r 623d46973cbe -r 94bc8f62c835 src/Doc/Isar_Ref/Inner_Syntax.thy --- 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"} & : & \theory \ theory\ \\ @{command_def "syntax"} & : & \local_theory \ local_theory\ \\ @{command_def "no_syntax"} & : & \local_theory \ local_theory\ \\ + @{command_def "syntax_types"} & : & \theory \ theory\ \\ + @{command_def "syntax_consts"} & : & \theory \ theory\ \\ @{command_def "translations"} & : & \theory \ theory\ \\ @{command_def "no_translations"} & : & \theory \ theory\ \\ @{attribute_def syntax_ast_trace} & : & \attribute\ & default \false\ \\ @@ -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>\ @@ -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 ('==' | '=>' | '<=' | '\' | '\' | '\') transpat +) ; @@ -1106,6 +1111,8 @@ ; mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')') ; + syntaxdeps: (@{syntax name}+) ('==' | '\') (@{syntax name}+) + ; transpat: ('(' @{syntax name} ')')? @{syntax string} \ @@ -1157,6 +1164,14 @@ translations) resulting from \decls\, which are interpreted in the same manner as for @{command "syntax"} above. + \<^descr> @{command "syntax_types"}~\syntax \ types\ and @{command + "syntax_consts"}~\syntax \ consts\ 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"}~\rules\ 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 diff -r 623d46973cbe -r 94bc8f62c835 src/HOL/Data_Structures/Leftist_Heap_List.thy --- 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 \ 5 * length xs" +shows "T_lheap_list xs \ 5 * length xs - 2 * log 2 (length xs)" proof - let ?ts = "map (\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 "\ = 5*(2::real)^k - (2::real)*k - 5" using summation by (simp) - also have "\ \ 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 diff -r 623d46973cbe -r 94bc8f62c835 src/HOL/Data_Structures/Selection.thy --- 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 \Running time analysis\ -fun T_partition3 :: "'a \ 'a list \ 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 diff -r 623d46973cbe -r 94bc8f62c835 src/HOL/GCD.thy --- 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)