Updates for Isabelle 2025

Author: bauereiss

lib/isabelle/Add_Cancel_Distinct.thy

@@ -119,7 +119,12 @@ fun cancel_step ctxt ct = let
     val choose2 = if length choose < Int.min (length lhs_sort, length rhs_sort)
       then choose else List.tl choose
     val _ = List.hd choose2 (* raise Empty if no progress can be made *)
-    val x = Variable.variant_frees ctxt [t] [("x", @{typ unit})]
+    (* TODO: Double-check the following lines, which had to be changed for
+       Isabelle 2025 due to an API change from variant_frees (which called
+       declare_names internally) to variant_names.  The updated code aims
+       to preserve the previous behaviour. *)
+    val ctxt' = Variable.declare_names t ctxt
+    val x = Variable.variant_names ctxt' [("x", @{typ unit})]
         |> the_single |> Free
     val conv = tag_sum_conv ctxt choose2 x then_conv split_by_var_conv ctxt x
     val lhs_split = conv lhs
@@ -293,4 +298,4 @@ have "distinct (rev [12 ..< 80])"
 
 end
 
-end
+end

lib/isabelle/Sail2_monadic_combinators_lemmas.thy

@@ -177,7 +177,7 @@ lemma of_bl_bin_word_of_int:
 lemma get_slice_int_0_bin_to_bl[simp]:
   "len > 0 \<Longrightarrow> get_slice_int len n 0 = of_bl (bin_to_bl (nat len) n)"
   unfolding get_slice_int_def get_slice_int_bv_def subrange_list_def
-  by (auto simp: subrange_list_dec_drop_take len_bin_to_bl_aux)
+  by (auto simp: subrange_list_dec_drop_take size_bin_to_bl_aux)
 
 lemma to_bl_of_bl[simp]:
   fixes bl :: "bool list"

lib/isabelle/Sail2_operators_mwords_lemmas.thy

@@ -111,7 +111,7 @@ lemma of_bl_bin_word_of_int:
 lemma get_slice_int_0_bin_to_bl[simp]:
   "len > 0 \<Longrightarrow> get_slice_int len n 0 = of_bl (bin_to_bl (nat len) n)"
   unfolding get_slice_int_def get_slice_int_bv_def subrange_list_def
-  by (auto simp: subrange_list_dec_drop_take len_bin_to_bl_aux)
+  by (auto simp: subrange_list_dec_drop_take size_bin_to_bl_aux)
 
 lemma to_bl_of_bl[simp]:
   fixes bl :: "bool list"

lib/isabelle/Sail2_values_lemmas.thy

@@ -91,7 +91,7 @@ proof (use assms in \<open>induction xs n arbitrary: i rule: repeat.induct[case_
   show ?case
     using Step.prems Step.IH[of "i - length xs"]
     unfolding repeat.simps[of xs n]
-    by (auto simp: nth_append Divides.mod_geq[symmetric] nat_diff_distrib diff_mult_distrib)
+    by (auto simp: nth_append le_mod_geq[symmetric] nat_diff_distrib diff_mult_distrib)
 qed
 
 termination index_list