merged

--- a/.hgtags	Mon Dec 13 22:12:48 2021 +0100
+++ b/.hgtags	Mon Dec 13 22:13:22 2021 +0100
@@ -38,9 +38,4 @@
 83774d669b5181fb28d19d7a0219fbf6c6d38aab Isabelle2019
 abf3e80bd815c2c062b02c78b256f7ba27481380 Isabelle2020
 7e2a9a8c2b85f10d81f3be433878fe51fa13eb6f Isabelle2021
-fedc0b659881c3768f7209f64d9d0213aac0941d Isabelle2021-1-RC0
-81cc8f2ea9e720a68f0ba96e2b8d8e98a5ff3152 Isabelle2021-1-RC1
-b92b5a57521b27cf592b835caa8e8d73e05070d2 Isabelle2021-1-RC2
-2b212c8138a57096487461fa353386f753ff7a11 Isabelle2021-1-RC3
-2336356d4180b948eb9070f3f9f8986cda7e8f76 Isabelle2021-1-RC4
-8baf2e8b16e2218edaeb6dee402b21f97a49a505 Isabelle2021-1-RC5
+c2a2be496f35aa1a6072393aebfdb1b85c9f2e9e Isabelle2021-1

--- a/ANNOUNCE	Mon Dec 13 22:12:48 2021 +0100
+++ b/ANNOUNCE	Mon Dec 13 22:13:22 2021 +0100
@@ -38,8 +38,9 @@
 
 * System: improved document preparation using Isabelle/Scala.
 
-* System: update to current OpenJDK 17 (LTS) and Poly/ML 5.9 (with preliminary
-support for arm64).
+* System: update to current Java 17 LTS.
+
+* System: update to Poly/ML 5.9 with improved support for ARM64 on Linux.
 
 
 You may get Isabelle2021-1 from the following mirror sites:

--- a/Admin/Release/mirror-website	Mon Dec 13 22:12:48 2021 +0100
+++ b/Admin/Release/mirror-website	Mon Dec 13 22:13:22 2021 +0100
@@ -6,7 +6,7 @@
 
 case ${HOST} in
   sunbroy* | atbroy* | macbroy* | lxbroy* | lxcisa*)
-    DEST=/home/html/isabelle/html-data
+    DEST=/p/home/isabelle/html-data/html-data
     ;;
   *.cl.cam.ac.uk)
     USER=paulson

--- a/src/Doc/Implementation/Logic.thy	Mon Dec 13 22:12:48 2021 +0100
+++ b/src/Doc/Implementation/Logic.thy	Mon Dec 13 22:13:22 2021 +0100
@@ -492,7 +492,7 @@
       @{syntax name} (@{syntax embedded_ml}*) (@{syntax for_args})?
     ;
     @{syntax_def term_const_fn}:
-      @{ syntax term_const} @'=>' @{syntax embedded_ml}
+      @{syntax term_const} @'=>' @{syntax embedded_ml}
     ;
     @{syntax_def for_args}: @'for' (@{syntax embedded_ml}+)
   \<close>

--- a/src/Doc/System/Scala.thy	Mon Dec 13 22:12:48 2021 +0100
+++ b/src/Doc/System/Scala.thy	Mon Dec 13 22:13:22 2021 +0100
@@ -321,15 +321,25 @@
 subsection \<open>Defining functions in Isabelle/Scala\<close>
 
 text \<open>
-  A Scala functions of type \<^scala_type>\<open>String => String\<close> may be wrapped as
-  \<^scala_type>\<open>isabelle.Scala.Fun\<close> and collected via an instance of the
-  class \<^scala_type>\<open>isabelle.Scala.Functions\<close>. A system component can then
-  register that class via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>
-  (\secref{sec:scala-build}). An example is the predefined collection of
-  \<^scala_type>\<open>isabelle.Scala.Functions\<close> in \<^file>\<open>$ISABELLE_HOME/etc/build.props\<close>.
+  The service class \<^scala_type>\<open>isabelle.Scala.Functions\<close> collects Scala
+  functions of type \<^scala_type>\<open>isabelle.Scala.Fun\<close>: by registering
+  instances via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>
+  (\secref{sec:scala-build}), it is becomes possible to invoke Isabelle/Scala
+  from Isabelle/ML (see below).
 
-  The overall list of registered functions is accessible in Isabelle/Scala as
+  An example is the predefined collection of
+  \<^scala_type>\<open>isabelle.Scala.Functions\<close> in
+  \<^file>\<open>$ISABELLE_HOME/etc/build.props\<close>. The overall list of registered functions
+  is accessible in Isabelle/Scala as
   \<^scala_object>\<open>isabelle.Scala.functions\<close>.
+
+  The general class \<^scala_type>\<open>isabelle.Scala.Fun\<close> expects a multi-argument
+  / multi-result function
+  \<^scala_type>\<open>List[isabelle.Bytes] => List[isabelle.Bytes]\<close>; more common are
+  instances of \<^scala_type>\<open>isabelle.Scala.Fun_Strings\<close> for type
+  \<^scala_type>\<open>List[String] => List[String]\<close>, or
+  \<^scala_type>\<open>isabelle.Scala.Fun_String\<close> for type
+  \<^scala_type>\<open>String => String\<close>.
 \<close>
 
 
@@ -357,11 +367,12 @@
 
   \<^descr> \<open>@{scala name}\<close> and \<open>@{scala_thread name}\<close> invoke the checked function via
   the PIDE protocol. In Isabelle/ML this appears as a function of type
-  \<^ML_type>\<open>string -> string\<close>, which is subject to interrupts within the ML
-  runtime environment as usual. A \<^scala>\<open>null\<close> result in Scala raises an
-  exception \<^ML>\<open>Scala.Null\<close> in ML. The execution of \<open>@{scala}\<close> works via a
-  Scala future on a bounded thread farm, while \<open>@{scala_thread}\<close> always forks
-  a separate Java thread.
+  \<^ML_type>\<open>string list -> string list\<close> or \<^ML_type>\<open>string -> string\<close>,
+  depending on the definition in Isabelle/Scala. Evaluation is subject to
+  interrupts within the ML runtime environment as usual. A \<^scala>\<open>null\<close>
+  result in Scala raises an exception \<^ML>\<open>Scala.Null\<close> in ML. The execution
+  of \<open>@{scala}\<close> works via a Scala future on a bounded thread farm, while
+  \<open>@{scala_thread}\<close> always forks a separate Java thread.
 
   The standard approach of representing datatypes via strings works via XML in
   YXML transfer syntax. See Isabelle/ML operations and modules @{ML

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Dec 13 22:12:48 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Dec 13 22:13:22 2021 +0100
@@ -458,8 +458,7 @@
 fun make_axiom_tcon_clause (s, name, (cl, args)) =
   let
     val args = args |> map normalize_classes
-    val tvars =
-      1 upto length args |> map (fn j => TVar ((tvar_a_str, j), \<^sort>\<open>type\<close>))
+    val tvars = args |> map_index (fn (j, _) => TVar ((tvar_a_str, j + 1), \<^sort>\<open>type\<close>))
   in (name, args ~~ tvars, (cl, Type (s, tvars))) end
 
 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
@@ -857,12 +856,9 @@
   | do_cheaply_conceal_lambdas _ t = t
 
 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
-fun conceal_bounds Ts t =
-  subst_bounds (map (Free o apfst concealed_bound_name)
-                    (0 upto length Ts - 1 ~~ Ts), t)
+fun conceal_bounds Ts t = subst_bounds (map_index (Free o apfst concealed_bound_name) Ts, t)
 fun reveal_bounds Ts =
-  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
-                    (0 upto length Ts - 1 ~~ Ts))
+  subst_atomic (map_index (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) Ts)
 
 fun do_introduce_combinators ctxt Ts t =
   (t |> conceal_bounds Ts
@@ -917,7 +913,7 @@
       val head_T = fastype_of head
       val n = length args
       val arg_Ts = head_T |> binder_types |> take n |> rev
-      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+      val u = u |> subst_atomic (map_index (swap o apfst Bound) args)
     in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
   | intentionalize_def t = t
 
@@ -1429,11 +1425,9 @@
     val (facts, lambda_ts) =
       facts |> map (snd o snd) |> trans_lams
             |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
-    val lam_facts =
-      map2 (fn t => fn j =>
-               ((lam_fact_prefix ^ Int.toString j,
-                 (Global, Non_Rec_Def)), (Axiom, t)))
-           lambda_ts (1 upto length lambda_ts)
+    val lam_facts = lambda_ts
+      |> map_index (fn (j, t) =>
+         ((lam_fact_prefix ^ Int.toString (j + 1), (Global, Non_Rec_Def)), (Axiom, t)))
   in (facts, lam_facts) end
 
 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate this in Sledgehammer to
@@ -1525,7 +1519,7 @@
       if forall null footprint then
         []
       else
-        0 upto length footprint - 1 ~~ footprint
+        map_index I footprint
         |> sort (rev_order o list_ord Term_Ord.indexname_ord o apply2 snd)
         |> cover []
     end
@@ -2094,7 +2088,7 @@
     val facts = facts |> map (apsnd (pair Axiom))
     val conjs =
       map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
-      |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
+      |> map_index (apfst (rpair (Local, General) o string_of_int))
     val ((conjs, facts), lam_facts) =
       (conjs, facts)
       |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop simp_options ctxt type_enc))))
@@ -2145,8 +2139,7 @@
           val ary = length tms
           val cover = type_arg_cover thy pos s ary
         in
-          exists (fn (j, tm) => tm = var andalso member (op =) cover j)
-                 (0 upto ary - 1 ~~ tms) orelse
+          exists (fn (j, tm) => tm = var andalso member (op =) cover j) (map_index I tms) orelse
           exists is_undercover tms
         end
       | is_undercover _ = true
@@ -2199,7 +2192,7 @@
               val ary = length args
               fun arg_site j = if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary)
             in
-              map2 (fn j => term (arg_site j)) (0 upto ary - 1) args
+              map_index (fn (j, arg) => term (arg_site j) arg) args
               |> mk_aterm type_enc name T_args
             end
           | IVar (name, _) =>
@@ -2313,7 +2306,7 @@
   if is_type_enc_polymorphic type_enc then
     let
       val type_classes = (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
-      fun line j (cl, T) =
+      fun line (j, (cl, T)) =
         if type_classes then
           Class_Memb (class_memb_prefix ^ string_of_int j, [],
             native_atp_type_of_typ type_enc false 0 T, `make_class cl)
@@ -2324,7 +2317,7 @@
         fold (union (op =)) (map #atomic_types facts) []
         |> class_membs_of_types type_enc add_sorts_on_tfree
     in
-      map2 line (0 upto length membs - 1) membs
+      map_index line membs
     end
   else
     []
@@ -2543,14 +2536,13 @@
     val (role, maybe_negate) = honor_conj_sym_role in_conj
     val (arg_Ts, res_T) = chop_fun ary T
     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
-    val bounds =
-      bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
+    val bounds = map2 (fn name => fn T => IConst (name, T, [])) bound_names arg_Ts
     val bound_Ts =
       (case level_of_type_enc type_enc of
         All_Types => if null T_args then replicate ary NONE else map SOME arg_Ts
       | Undercover_Types =>
         let val cover = type_arg_cover thy NONE s ary in
-          map2 (fn j => if member (op =) cover j then SOME else K NONE) (0 upto ary - 1) arg_Ts
+          map_index (fn (j, arg_T) => if member (op =) cover j then SOME arg_T else NONE) arg_Ts
         end
       | _ => replicate ary NONE)
   in
@@ -2594,7 +2586,7 @@
       let
         val cover = type_arg_cover thy NONE s ary
         fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T
-        val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts)
+        val bounds = bounds |> map2 maybe_tag (map_index I arg_Ts)
       in formula (cst bounds) end
     else
       formula (cst bounds)
@@ -2621,15 +2613,14 @@
       val n = length decls
       val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
     in
-      (0 upto length decls - 1, decls)
-      |-> map2 (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)
+      map_index (uncurry (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)) decls
     end
   | Tags (_, level) =>
     if is_type_level_uniform level then
       []
     else
       let val n = length decls in
-        (0 upto n - 1 ~~ decls)
+        map_index I decls
         |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s)
       end)
 
@@ -2883,15 +2874,15 @@
     val freshen = mode <> Exporter andalso mode <> Translator
     val pos = mode <> Exporter
     val rank_of = rank_of_fact_num num_facts
-    val fact_lines =
-      map (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of)
-        (0 upto num_facts - 1 ~~ facts)
+    val fact_lines = facts
+      |> map_index (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc
+         rank_of)
+
     val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs
     val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses
-    val helper_lines =
-      0 upto length helpers - 1 ~~ helpers
-      |> map (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc
-        (K default_rank))
+    val helper_lines = helpers
+      |> map_index (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc
+         (K default_rank))
     val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
     val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
     (* Reordering these might confuse the proof reconstruction code. *)
@@ -2948,7 +2939,7 @@
           fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
                             / Real.fromInt num_facts
       in
-        map weight_of (0 upto num_facts - 1) ~~ facts
+        map_index (apfst weight_of) facts
         |> fold (uncurry add_line_weights)
       end
     val get = these o AList.lookup (op =) problem