merged
authorpaulson
Wed, 22 Jan 2025 22:22:37 +0000
changeset 81900 53bf4095ad3e
parent 81898 a70e471b2582 (diff)
parent 81899 1171ea4a23e4 (current diff)
child 81902 7d711d3f37bf
merged
--- a/NEWS	Wed Jan 22 22:22:27 2025 +0000
+++ b/NEWS	Wed Jan 22 22:22:37 2025 +0000
@@ -361,7 +361,7 @@
 
     isabelle find_facts_index HOL
     isabelle find_facts_server
-    open http://localhost:8080/app#search?q=Hilbert
+    open http://localhost:8080/find_facts#search?q=Hilbert
 
 Persistent data is stored in $ISABELLE_HOME_USER/find_facts/.
 
--- a/src/HOL/Bit_Operations.thy	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/HOL/Bit_Operations.thy	Wed Jan 22 22:22:37 2025 +0000
@@ -132,6 +132,17 @@
   using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
   by simp (metis (full_types) add.left_commute add_left_imp_eq)
 
+lemma half_numeral_Bit1_eq [simp]:
+  \<open>numeral (num.Bit1 m) div 2 = numeral (num.Bit0 m) div 2\<close>
+  using even_half_succ_eq [of \<open>2 * numeral m\<close>]
+  by simp
+
+lemma double_half_numeral_Bit_0_eq [simp]:
+  \<open>2 * (numeral (num.Bit0 m) div 2) = numeral (num.Bit0 m)\<close>
+  \<open>(numeral (num.Bit0 m) div 2) * 2 = numeral (num.Bit0 m)\<close>
+  using mod_mult_div_eq [of \<open>numeral (Num.Bit0 m)\<close> 2]
+  by (simp_all add: mod2_eq_if ac_simps)
+
 named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
 
 definition possible_bit :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
@@ -1195,7 +1206,7 @@
     by (cases n) (auto simp: bit_0 bit_double_iff even_bit_succ_iff)
 qed
 
-lemma set_bit_0 [simp]:
+lemma set_bit_0:
   \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
 
@@ -1204,7 +1215,7 @@
   by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
     elim: possible_bit_less_imp)
 
-lemma unset_bit_0 [simp]:
+lemma unset_bit_0:
   \<open>unset_bit 0 a = 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps simp flip: bit_Suc)
 
@@ -1212,7 +1223,7 @@
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
 
-lemma flip_bit_0 [simp]:
+lemma flip_bit_0:
   \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
 
@@ -1557,7 +1568,7 @@
 
 lemma drop_bit_Suc_bit1 [simp]:
   \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit1_div_2)
+  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
 
 lemma drop_bit_numeral_bit0 [simp]:
   \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
@@ -1565,7 +1576,7 @@
 
 lemma drop_bit_numeral_bit1 [simp]:
   \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
-  by (simp add: drop_bit_rec numeral_Bit1_div_2)
+  by (simp add: drop_bit_rec numeral_Bit0_div_2)
 
 lemma take_bit_Suc_1 [simp]:
   \<open>take_bit (Suc n) 1 = 1\<close>
@@ -1577,7 +1588,7 @@
 
 lemma take_bit_Suc_bit1:
   \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
+  by (simp add: take_bit_Suc numeral_Bit0_div_2 mod_2_eq_odd)
 
 lemma take_bit_numeral_1 [simp]:
   \<open>take_bit (numeral l) 1 = 1\<close>
@@ -1589,7 +1600,7 @@
 
 lemma take_bit_numeral_bit1:
   \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
+  by (simp add: take_bit_rec numeral_Bit0_div_2 mod_2_eq_odd)
 
 lemma bit_of_nat_iff_bit [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
@@ -2600,7 +2611,7 @@
 lemma [code]:
   \<open>unset_bit 0 m = 2 * (m div 2)\<close>
   \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m n :: nat
-  by (simp_all add: unset_bit_Suc)
+  by (simp_all add: unset_bit_0 unset_bit_Suc)
 
 lemma push_bit_of_Suc_0 [simp]:
   \<open>push_bit n (Suc 0) = 2 ^ n\<close>
@@ -2778,7 +2789,7 @@
 
 lemma bit_numeral_Bit1_Suc_iff [simp]:
   \<open>bit (numeral (Num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
-  by (simp add: bit_Suc numeral_Bit1_div_2)
+  by (simp add: bit_Suc numeral_Bit0_div_2)
 
 lemma bit_numeral_rec:
   \<open>bit (numeral (Num.Bit0 w)) n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc m \<Rightarrow> bit (numeral w) m)\<close>
@@ -3278,6 +3289,86 @@
 
 end
 
+context semiring_bit_operations
+begin
+
+lemma push_bit_eq_pow:
+  \<open>push_bit (numeral n) 1 = numeral (Num.pow (Num.Bit0 Num.One) n)\<close>
+  by simp
+
+lemma set_bit_of_0 [simp]:
+  \<open>set_bit n 0 = 2 ^ n\<close>
+  by (simp add: set_bit_eq_or)
+
+lemma unset_bit_of_0 [simp]:
+  \<open>unset_bit n 0 = 0\<close>
+  by (simp add: unset_bit_eq_or_xor)
+
+lemma flip_bit_of_0 [simp]:
+  \<open>flip_bit n 0 = 2 ^ n\<close>
+  by (simp add: flip_bit_eq_xor)
+
+lemma set_bit_0_numeral_eq [simp]:
+  \<open>set_bit 0 (numeral Num.One) = 1\<close>
+  \<open>set_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+  \<open>set_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit1 m)\<close>
+  by (simp_all add: set_bit_0)
+
+lemma set_bit_numeral_eq_or [simp]:
+  \<open>set_bit (numeral n) (numeral m) = numeral m OR push_bit (numeral n) 1\<close>
+  by (fact set_bit_eq_or)
+
+lemma unset_bit_0_numeral_eq_and_not' [simp]:
+  \<open>unset_bit 0 (numeral Num.One) = 0\<close>
+  \<open>unset_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit0 m)\<close>
+  \<open>unset_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+  by (simp_all add: unset_bit_0)
+
+lemma unset_bit_numeral_eq_or [simp]:
+  \<open>unset_bit (numeral n) (numeral m) =
+    (case and_not_num m (Num.pow (Num.Bit0 Num.One) n)
+     of None \<Rightarrow> 0
+      | Some q \<Rightarrow> numeral q)\<close> (is \<open>?lhs = _\<close>)
+proof -
+  have \<open>?lhs = of_nat (unset_bit (numeral n) (numeral m))\<close>
+    by (simp add: of_nat_unset_bit_eq)
+  also have \<open>unset_bit (numeral n) (numeral m) = nat (unset_bit (numeral n) (numeral m))\<close>
+    by (simp flip: int_int_eq add: Bit_Operations.of_nat_unset_bit_eq)
+  finally have *: \<open>?lhs = of_nat (nat (unset_bit (numeral n) (numeral m)))\<close> .
+  show ?thesis
+    by (simp only: * unset_bit_eq_and_not Bit_Operations.push_bit_eq_pow int_numeral_and_not_num)
+      (auto split: option.splits)
+qed
+
+lemma flip_bit_0_numeral_eq_or [simp]:
+  \<open>flip_bit 0 (numeral Num.One) = 0\<close>
+  \<open>flip_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+  \<open>flip_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+  by (simp_all add: flip_bit_0)
+
+lemma flip_bit_numeral_eq_xor [simp]:
+  \<open>flip_bit (numeral n) (numeral m) = numeral m XOR push_bit (numeral n) 1\<close>
+  by (fact flip_bit_eq_xor)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma set_bit_minus_numeral_eq_or [simp]:
+  \<open>set_bit (numeral n) (- numeral m) = - numeral m OR push_bit (numeral n) 1\<close>
+  by (fact set_bit_eq_or)
+
+lemma unset_bit_minus_numeral_eq_and_not [simp]:
+  \<open>unset_bit (numeral n) (- numeral m) = - numeral m AND NOT (push_bit (numeral n) 1)\<close>
+  by (fact unset_bit_eq_and_not)
+
+lemma flip_bit_minus_numeral_eq_xor [simp]:
+  \<open>flip_bit (numeral n) (- numeral m) = - numeral m XOR push_bit (numeral n) 1\<close>
+  by (fact flip_bit_eq_xor)
+
+end
+
 lemma xor_int_code [code]:
   fixes i j :: int shows
   \<open>0 XOR j = j\<close>
--- a/src/HOL/List.thy	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/HOL/List.thy	Wed Jan 22 22:22:37 2025 +0000
@@ -263,6 +263,15 @@
 replicate_0: "replicate 0 x = []" |
 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
 
+overloading pow_list == "compow :: nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+begin
+
+primrec pow_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"pow_list 0 xs = []" |
+"pow_list (Suc n) xs = xs @ pow_list n xs"
+
+end
+
 text \<open>
   Function \<open>size\<close> is overloaded for all datatypes. Users may
   refer to the list version as \<open>length\<close>.\<close>
@@ -1168,7 +1177,7 @@
 by(blast dest:map_injective)
 
 lemma inj_mapI: "inj f \<Longrightarrow> inj (map f)"
-by (iprover dest: map_injective injD intro: inj_onI)
+by (rule list.inj_map)
 
 lemma inj_mapD: "inj (map f) \<Longrightarrow> inj f"
   by (metis (no_types, opaque_lifting) injI list.inject list.simps(9) the_inv_f_f)
@@ -1180,7 +1189,7 @@
   by (blast intro:inj_onI dest:inj_onD map_inj_on)
 
 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
-by (induct xs, auto)
+by (rule list.map_ident_strong)
 
 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
 by (induct xs) auto
@@ -1218,6 +1227,9 @@
 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
 by (induct xs) auto
 
+lemma rev_involution[simp]: "rev \<circ> rev = id"
+by auto
+
 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
 by auto
 
@@ -1284,6 +1296,21 @@
   qed
 qed simp
 
+lemma rev_induct2:
+  "\<lbrakk> P [] [];
+  \<And>x xs. P (xs @ [x]) [];
+  \<And>y ys. P [] (ys @ [y]);
+  \<And>x xs y ys. P xs ys  \<Longrightarrow> P (xs @ [x]) (ys @ [y]) \<rbrakk>
+ \<Longrightarrow> P xs ys"
+proof (induct xs arbitrary: ys rule: rev_induct)
+  case Nil
+  then show ?case using rev_induct[of "P []"] by presburger
+next
+  case (snoc x xs)
+  hence "P xs ys'" for ys' by simp
+  then show ?case by (simp add: rev_induct snoc.prems(2,4))
+qed
+
 lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)"
 by (induct xs rule: rev_induct) auto
 
@@ -4404,6 +4431,10 @@
   "\<lbrakk> inj_on f (set xs); x \<in> set xs \<rbrakk> \<Longrightarrow> count_list (map f xs) (f x) = count_list xs x"
 by (induction xs) (simp, fastforce)
 
+lemma count_list_map_conv:
+assumes "inj f" shows "count_list (map f xs) (f x) = count_list xs x"
+by (induction xs) (simp_all add: inj_eq[OF assms])
+
 lemma count_list_rev[simp]: "count_list (rev xs) x = count_list xs x"
 by (induction xs) auto
 
@@ -4714,6 +4745,9 @@
   "concat (replicate i []) = []"
   by (induct i) (auto simp add: map_replicate_const)
 
+lemma concat_replicate_single[simp]: "concat (replicate m [a]) = replicate m a"
+by(induction m) auto
+
 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
 by (induct n) auto
 
@@ -4812,6 +4846,134 @@
 by (subst foldr_fold [symmetric]) simp_all
 
 
+subsubsection \<open>\<^term>\<open>xs ^^ n\<close>\<close>
+
+context
+begin
+
+interpretation monoid_mult "[]" "append"
+  rewrites "power u n = u ^^ n"
+proof-
+  show "class.monoid_mult [] (@)"
+    by (unfold_locales, simp_all)
+  show "power.power [] (@) u n = u ^^ n"
+    by(induction n) (auto simp add: power.power.simps)
+qed
+
+\<comment> \<open>inherited power properties\<close>
+
+lemmas pow_list_zero = power.power_0 and
+  pow_list_one = power_Suc0_right and
+  pow_list_1 = power_one_right and
+  pow_list_Nil = power_one and
+  pow_list_2 = power2_eq_square and
+  pow_list_Suc = power_Suc and
+  pow_list_Suc2 = power_Suc2 and
+  pow_list_comm = power_commutes and
+  pow_list_add = power_add and
+  pow_list_eq_if = power_eq_if and
+  pow_list_mult = power_mult and
+  pow_list_commuting_commutes = power_commuting_commutes
+
+end
+
+lemma pow_list_alt: "xs^^n = concat (replicate n xs)"
+by (induct n) auto
+
+lemma pow_list_single: "[a] ^^ m = replicate m a"
+by(simp add: pow_list_alt)
+
+lemma length_pow_list_single [simp]: "length([a] ^^ n) = n"
+by (simp add: pow_list_single)
+
+lemma nth_pow_list_single: "i < m \<Longrightarrow> ([a] ^^ m) ! i = a"
+by (simp add: pow_list_single)
+
+lemma pow_list_not_NilD: "xs ^^ m \<noteq> [] \<Longrightarrow> 0 < m"
+by (cases m) auto
+
+lemma length_pow_list:  "length(xs ^^ k) = k * length xs"
+by (induction k) simp+
+
+lemma pow_list_set: "set (w ^^ Suc k) = set w"
+by (induction k)(simp_all)
+
+lemma pow_list_slide: "xs @ (ys @ xs) ^^ n  @ ys = (xs @ ys)^^(Suc n)"
+by (induction n) simp+
+
+lemma hd_pow_list: "0 < n \<Longrightarrow> hd(xs ^^ n) = hd xs"
+by(auto simp: pow_list_alt hd_append gr0_conv_Suc)
+
+lemma rev_pow_list: "rev (xs ^^ m) = (rev xs) ^^ m"
+by (induction m)(auto simp: pow_list_comm)
+
+lemma eq_pow_list_iff_eq_exp[simp]: assumes "xs \<noteq> []" shows "xs ^^ k = xs ^^ m \<longleftrightarrow> k = m"
+proof
+  assume "k = m" thus "xs ^^ k = xs ^^ m" by simp
+next
+  assume "xs ^^ k = xs ^^ m"
+  thus "k = m" using \<open>xs \<noteq> []\<close>[folded length_0_conv]
+    by (metis length_pow_list mult_cancel2)
+qed
+
+lemma pow_list_Nil_iff_0: "xs \<noteq> [] \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow> m = 0"
+by (simp add: pow_list_eq_if)
+
+lemma pow_list_Nil_iff_Nil: "0 < m \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow>  xs = []"
+by (cases xs) (auto simp add: pow_list_Nil pow_list_Nil_iff_0)
+
+lemma pow_eq_eq:
+  assumes "xs ^^ k = ys ^^ k" and "0 < k"
+  shows "(xs::'a list) = ys"
+proof-
+  have "length xs = length ys"
+    using assms(1) length_pow_list by (metis nat_mult_eq_cancel1[OF \<open>0 < k\<close>])
+  thus ?thesis by (metis Suc_pred append_eq_append_conv assms(1,2) pow_list.simps(2))
+qed
+
+lemma map_pow_list[simp]: "map f (xs ^^ k) = (map f xs) ^^ k"
+by (induction k) simp_all
+
+lemma concat_pow_list: "concat (xs ^^ k) = (concat xs) ^^ k"
+by (induction k) simp_all
+
+lemma concat_pow_list_single[simp]: "concat ([a] ^^ k) = a ^^ k"
+by (simp add: pow_list_alt)
+
+lemma pow_list_single_Nil_iff: "[a] ^^ n = [] \<longleftrightarrow> n = 0"
+by (simp add: pow_list_single)
+
+lemma hd_pow_list_single: "k \<noteq> 0 \<Longrightarrow> hd ([a] ^^ k) = a"
+by (cases k) simp+
+
+lemma index_pow_mod: "i < length(xs ^^ k) \<Longrightarrow> (xs ^^ k)!i = xs!(i mod length xs)"
+proof(induction k)
+  have aux:  "length(xs ^^ Suc l) = length(xs ^^ l) + length xs" for l
+    by simp
+  have aux1: "length (xs ^^ l) \<le> i \<Longrightarrow> i < length(xs ^^ l) + length xs \<Longrightarrow>  i mod length xs = i -  length(xs^^l)" for l
+    unfolding length_pow_list[of l xs]
+     using less_diff_conv2[of "l * length xs" i "length xs", unfolded add.commute[of "length xs"  "l * length xs"]]
+       le_add_diff_inverse[of "l*length xs" i]
+    by (simp add: mod_nat_eqI)
+  case (Suc k)
+  show ?case
+    unfolding aux sym[OF pow_list_Suc2[symmetric]] nth_append le_mod_geq
+    using aux1[ OF _ Suc.prems[unfolded aux]]
+      Suc.IH pow_list_Suc2[symmetric] Suc.prems[unfolded aux] leI[of i "length(xs ^^ k)"] by presburger
+qed auto
+
+lemma unique_letter_word: assumes "\<And>c. c \<in> set w \<Longrightarrow> c = a" shows "w = [a] ^^ length w"
+  using assms proof (induction w)
+  case (Cons b w)
+  have "[a] ^^ length w = w" using Cons.IH[OF Cons.prems[OF list.set_intros(2)]]..
+  then show "b # w = [a] ^^ length(b # w)"
+    unfolding Cons.prems[OF list.set_intros(1)] by auto
+qed simp
+
+lemma count_list_pow_list: "count_list (w ^^ k) a = k * (count_list w a)"
+by (induction k) simp+
+
+
 subsubsection \<open>\<^const>\<open>enumerate\<close>\<close>
 
 lemma enumerate_simps [simp, code]:
@@ -6612,8 +6774,7 @@
 lemma Cons_in_lists_iff[simp]: "x#xs \<in> lists A \<longleftrightarrow> x \<in> A \<and> xs \<in> lists A"
 by auto
 
-lemma append_in_listsp_conv [iff]:
-     "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
+lemma append_in_listsp_conv [iff]: "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
 by (induct xs) auto
 
 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
@@ -6634,6 +6795,9 @@
 
 lemmas in_listsI [intro!] = in_listspI [to_set]
 
+lemma mono_lists: "mono lists"
+unfolding mono_def by auto
+
 lemma lists_eq_set: "lists A = {xs. set xs \<le> A}"
 by auto
 
@@ -6650,6 +6814,41 @@
   then show ?thesis by auto
 qed
 
+lemma inj_on_map_lists: assumes "inj_on f A"
+  shows "inj_on (map f) (lists A)"
+proof
+  fix xs ys
+  assume "xs \<in> lists A" and "ys \<in> lists A" and "map f xs = map f ys"
+  have "x = y" if "x \<in> set xs" and "y \<in> set ys" and  "f x =  f y"  for x y
+    using in_listsD[OF \<open>xs \<in> lists A\<close>, rule_format, OF \<open>x \<in> set xs\<close>]
+          in_listsD[OF \<open>ys \<in> lists A\<close>, rule_format, OF \<open>y \<in> set ys\<close>]
+         \<open>inj_on f A\<close>[unfolded inj_on_def, rule_format, OF _ _ \<open>f x =  f y\<close>] by blast
+  from list.inj_map_strong[OF this  \<open>map f xs = map f ys\<close>]
+  show "xs = ys".
+qed
+
+lemma bij_lists: "bij_betw f X Y \<Longrightarrow> bij_betw (map f) (lists X) (lists Y)"
+unfolding bij_betw_def using inj_on_map_lists lists_image by metis
+
+lemma replicate_in_lists: "a \<in> A \<Longrightarrow> replicate k a \<in> lists A"
+by (induction k) auto
+
+lemma sing_pow_lists: "a \<in> A \<Longrightarrow> [a] ^^ n \<in> lists A"
+by (induction n) auto
+
+lemma one_generated_list_power: "u \<in> lists {x} \<Longrightarrow> \<exists>k. concat u = x ^^ k"
+proof(induction u rule: lists.induct)
+  case Nil
+  then show ?case by (metis concat.simps(1) pow_list.simps(1))
+next
+  case Cons
+  then show ?case by (metis concat.simps(2) pow_list_Suc singletonD)
+qed
+
+lemma pow_list_in_lists: "0 < k \<Longrightarrow> u ^^ k \<in> lists B \<Longrightarrow> u \<in> lists B"
+by (metis Suc_pred in_lists_conv_set pow_list_set)
+
+
 subsubsection \<open>Inductive definition for membership\<close>
 
 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
--- a/src/HOL/ROOT	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/HOL/ROOT	Wed Jan 22 22:22:37 2025 +0000
@@ -694,6 +694,7 @@
     BigO
     BinEx
     Birthday_Paradox
+    Bit_Operation_Calculations
     Bubblesort
     CTL
     Cartouche_Examples
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Bit_Operation_Calculations.thy	Wed Jan 22 22:22:37 2025 +0000
@@ -0,0 +1,145 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Tests for simplifying bit operations on ground terms\<close>
+
+theory Bit_Operation_Calculations
+  imports
+    "HOL.Bit_Operations"
+    "HOL-Library.Word"
+begin
+
+unbundle bit_operations_syntax
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale unsigned_computations =
+  fixes type :: \<open>'a::semiring_bit_operations itself\<close>
+begin
+
+definition computations where
+  \<open>computations = (
+    [bit (473514 :: 'a) 5],
+    [473514 AND 767063 :: 'a],
+    [473514 OR 767063 :: 'a],
+    [473514 XOR 767063 :: 'a],
+    mask 11 :: 'a,
+    [set_bit 15 473514 :: 'a],
+    [unset_bit 13 473514 :: 'a],
+    [flip_bit 15 473514 :: 'a],
+    [push_bit 12 473514 :: 'a],
+    [drop_bit 12 65344 :: 'a],
+    [take_bit 12 473514 :: 'a]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True],
+    [208898 :: 'a::semiring_bit_operations],
+    [1031679 :: 'a],
+    [822781 :: 'a],
+    2047 :: 'a,
+    [506282 :: 'a],
+    [465322 :: 'a],
+    [506282 :: 'a],
+    [1939513344 :: 'a],
+    [15 :: 'a],
+    [2474 :: 'a]
+  )\<close>
+
+lemmas evaluation_simps = computations_def results_def mask_numeral
+   \<comment> \<open>Expressions like \<term>\<open>mask 42\<close> are deliberately not simplified by default\<close>
+
+end
+
+global_interpretation unsigned_computations_nat: unsigned_computations \<open>TYPE(nat)\<close>
+  defines unsigned_computations_nat = unsigned_computations_nat.computations
+    and unsigned_results_nat = unsigned_computations_nat.results .
+
+lemma \<open>unsigned_computations_nat.computations = unsigned_computations_nat.results\<close>
+  by (simp add: unsigned_computations_nat.evaluation_simps)
+
+global_interpretation unsigned_computations_int: unsigned_computations \<open>TYPE(int)\<close>
+  defines unsigned_computations_int = unsigned_computations_int.computations
+    and unsigned_results_int = unsigned_computations_int.results .
+
+lemma \<open>unsigned_computations_int.computations = unsigned_computations_int.results\<close>
+  by (simp add: unsigned_computations_int.evaluation_simps)
+
+global_interpretation unsigned_computations_word16: unsigned_computations \<open>TYPE(16 word)\<close>
+  defines unsigned_computations_word16 = unsigned_computations_word16.computations
+    and unsigned_results_word16 = unsigned_computations_word16.results .
+
+lemma \<open>unsigned_computations_word16 = unsigned_results_word16\<close>
+  by (simp add: unsigned_computations_word16.evaluation_simps)
+
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale signed_computations =
+  fixes type :: \<open>'a::ring_bit_operations itself\<close>
+begin
+
+definition computations where
+  \<open>computations = (
+    [bit (- 805167 :: 'a) 7],
+    [- 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: 'a],
+    [- 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: 'a],
+    [- 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: 'a],
+    [NOT 473513, NOT (- 805167) :: 'a],
+    [set_bit 11 (- 805167) :: 'a],
+    [unset_bit 12 (- 805167) :: 'a],
+    [flip_bit 12 (- 805167) :: 'a],
+    [push_bit 12 (- 805167) :: 'a],
+    [take_bit 12 (- 805167) :: 'a],
+    [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: 'a]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True],
+    [242769, 209184, - 839103 :: 'a],
+    [- 280873, - 50197, - 280591 :: 'a],
+    [- 523642, - 259381, 558512 :: 'a],
+    [- 473514, 805166 :: 'a],
+    [- 803119 :: 'a],
+    [- 809263 :: 'a],
+    [- 809263 :: 'a],
+    [- 3297964032 :: 'a],
+    [1745 :: 'a],
+    [- 1622, - 2351 :: 'a]
+  )\<close>
+
+lemmas evaluation_simps = computations_def results_def
+
+end
+
+global_interpretation signed_computations_int: signed_computations \<open>TYPE(int)\<close>
+  defines signed_computations_int = signed_computations_int.computations
+    and signed_results_int = signed_computations_int.results .
+
+lemma \<open>signed_computations_int.computations = signed_computations_int.results\<close>
+  by (simp add: signed_computations_int.evaluation_simps)
+
+global_interpretation signed_computations_word16: signed_computations \<open>TYPE(16 word)\<close>
+  defines signed_computations_word16 = signed_computations_word16.computations
+    and signed_results_word16 = signed_computations_word16.results .
+
+lemma \<open>signed_computations_word16 = signed_results_word16\<close>
+  by (simp add: signed_computations_word16.evaluation_simps)
+
+
+subsection \<open>Special cases on particular type instances\<close>
+
+lemma
+  \<open>drop_bit 12 (- 17405 :: int) = - 5\<close>
+  by simp
+
+lemma
+  \<open>signed_drop_bit 12 (- 17405 :: 16 word) = - 5\<close>
+  by simp
+
+lemma
+  \<open>drop_bit 12 (- 17405 :: 16 word) = 11\<close>
+  by simp
+
+end
--- a/src/Pure/Build/build_ci.scala	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Pure/Build/build_ci.scala	Wed Jan 22 22:22:37 2025 +0000
@@ -70,16 +70,14 @@
   case object On_Commit extends Trigger
 
   object Timed {
-    def nightly(start_time: Time = Time.zero): Timed =
-      Timed { (before, now) =>
-        val start0 = before.midnight + start_time
-        val start1 = now.midnight + start_time
-        (before.time < start0.time && start0.time <= now.time) ||
-          (before.time < start1.time && start1.time <= now.time)
-      }
+    def nightly(start: Time = Time.hms(0, 17, 0)): Timed = Timed(Date.Daily(start))
+    def weekly(day: Date.Day = Date.Day.sun, start: Time = Time.hms(0, 17, 0)): Timed =
+      Timed(Date.Weekly(day, Date.Daily(start)))
   }
 
-  case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger
+  case class Timed(cycle: Date.Cycle) extends Trigger {
+    def next(previous: Date, now: Date): Boolean = cycle.next(previous).time < cycle.next(now).time
+  }
 
 
   /* build hooks */
--- a/src/Pure/Build/build_manager.scala	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Pure/Build/build_manager.scala	Wed Jan 22 22:22:37 2025 +0000
@@ -1135,7 +1135,7 @@
     private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") {
       for (ci_job <- ci_jobs)
         ci_job.trigger match {
-          case Build_CI.Timed(in_interval) if in_interval(previous, next) =>
+          case timer: Build_CI.Timed if timer.next(previous, next) =>
             val task = CI_Build.task(ci_job)
             echo("Triggered task " + task.kind)
             _state = _state.add_pending(task)
@@ -1411,7 +1411,7 @@
         def render_diff(data: Report.Data, components: List[Component]): XML.Body =
           par(List(page_link(Page.BUILD, "back to build", Markup.Name(build.name)))) ::
           (for (component <- components if !component.is_local) yield {
-            val infos = 
+            val infos =
               data.component_logs.toMap.get(component.name).toList.flatMap(colored) :::
               data.component_diffs.toMap.get(component.name).toList.flatMap(colored)
 
@@ -1508,7 +1508,7 @@
           Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
           HTML.style_file("https://hawkz.github.io/gdcss/gd.css"),
           HTML.style("""
-:root { 
+:root {
   --color-secondary: var(--color-tertiary);
   --color-secondary-hover: var(--color-tertiary-hover);
 }
@@ -1894,7 +1894,7 @@
     progress.interrupt_handler {
       using(store.open_ssh()) { ssh =>
         val user = ssh.execute("whoami").check.out
-        
+
         val build_config = User_Build(user, afp_rev, prefs, requirements, all_sessions,
           base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions,
           build_heap, clean_build, export_files, fresh_build, presentation, verbose)
--- a/src/Pure/General/date.scala	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Pure/General/date.scala	Wed Jan 22 22:22:37 2025 +0000
@@ -10,7 +10,7 @@
 import java.util.Locale
 import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
-import java.time.temporal.TemporalAccessor
+import java.time.temporal.{ChronoUnit, TemporalAccessor}
 
 import scala.annotation.tailrec
 
@@ -99,9 +99,67 @@
 
   def apply(t: Time, timezone: ZoneId = Date.timezone()): Date =
     instant(t.instant, timezone)
+
+
+  /* varying-length calendar cycles */
+
+  enum Day { case mon, tue, wed, thu, fri, sat, sun }
+  enum Month { case jan, feb, mar, apr, may, jun, jul, aug, sep, okt, nov, dec }
+
+  sealed trait Cycle {
+    def zero(date: Date): Date
+    def next(date: Date): Date
+  }
+
+  case class Daily(at: Time = Time.zero) extends Cycle {
+    require(at >= Time.zero && at < Time.hms(24, 0, 0))
+
+    def zero(date: Date): Date = date.midnight
+    def next(date: Date): Date = {
+      val start = zero(date) + at
+      if (date.time < start.time) start else start.shift(1)
+    }
+
+    override def toString: String = "Daily(" + Format.time(Date(at, timezone_utc)) + ")"
+  }
+
+  case class Weekly(on: Day = Day.mon, step: Daily = Daily()) extends Cycle {
+    def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfWeek.getValue).midnight
+    def next(date: Date): Date = {
+      val next = step.next(zero(date).shift(on.ordinal) - Time.ms(1))
+      if (date.time < next.time) next else Date(next.rep.plus(1, ChronoUnit.WEEKS))
+    }
+  }
+
+  case class Monthly(nth: Int = 1, step: Daily = Daily()) extends Cycle {
+    require(nth > 0 && nth <= 31)
+
+    def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfMonth).midnight
+    def next(date: Date): Date = {
+      @tailrec def find_next(zero: Date): Date = {
+        val next = step.next(zero.shift(nth - 1) - Time.ms(1))
+        if (next.rep.getDayOfMonth == nth && date.time < next.time) next
+        else find_next(Date(zero.rep.plus(1, ChronoUnit.MONTHS)))
+      }
+      find_next(zero(date))
+    }
+  }
+
+  case class Yearly(in: Month = Month.jan, step: Monthly = Monthly()) extends Cycle {
+    def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfYear).midnight
+    def next(date: Date): Date = {
+      @tailrec def find_next(zero: Date): Date = {
+        val next = step.next(Date(zero.rep.plus(in.ordinal, ChronoUnit.MONTHS)) - Time.ms(1))
+        if (next.rep.getMonthValue - 1 == in.ordinal && date.time < next.time) next
+        else find_next(Date(zero.rep.plus(1, ChronoUnit.YEARS)))
+      }
+      find_next(zero(date))
+    }
+  }
 }
 
 sealed case class Date(rep: ZonedDateTime) {
+  def shift(days: Int): Date = Date(rep.plus(days, ChronoUnit.DAYS))
   def midnight: Date =
     new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
 
--- a/src/Tools/Code/code_target.ML	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Code/code_target.ML	Wed Jan 22 22:22:37 2025 +0000
@@ -384,16 +384,27 @@
     val serializer = (#serializer o #language) target;
   in { serializer = serializer, data = data, modify = modify } end;
 
-fun project_program_for_syms ctxt syms_hidden syms1 program1 =
+fun report_unimplemented ctxt program requested unimplemented =
   let
-    val syms2 = subtract (op =) syms_hidden syms1;
+    val deps = flat (map_product (fn req => fn unimpl =>
+      Code_Symbol.Graph.irreducible_paths program (req, Constant unimpl)) requested unimplemented)
+    val pretty_dep = space_implode " -> " o map (Code_Symbol.quote ctxt)
+  in
+    error ("No code equations for "
+      ^ commas (map (Proof_Context.markup_const ctxt) unimplemented)
+      ^ ",\nrequested by dependencies\n"
+      ^ space_implode "\n" (map pretty_dep deps))
+  end;
+
+fun project_program_for_syms ctxt syms_hidden requested1 program1 =
+  let
+    val requested2 = subtract (op =) syms_hidden requested1;
     val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1;
     val unimplemented = Code_Thingol.unimplemented program2;
     val _ =
       if null unimplemented then ()
-      else error ("No code equations for " ^
-        commas (map (Proof_Context.markup_const ctxt) unimplemented));
-    val syms3 = Code_Symbol.Graph.all_succs program2 syms2;
+      else report_unimplemented ctxt program2 requested2 unimplemented;
+    val syms3 = Code_Symbol.Graph.all_succs program2 requested2;
     val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2;
   in program3 end;
 
--- a/src/Tools/Find_Facts/etc/settings	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Find_Facts/etc/settings	Wed Jan 22 22:22:37 2025 +0000
@@ -1,9 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
 FIND_FACTS_HOME="$COMPONENT"
-FIND_FACTS_WEB="$ISABELLE_HOME_USER/find_facts/web"
-
-SOLR_DATA="$ISABELLE_HOME_USER/find_facts/solr"
-SOLR_COMPONENTS=""
+FIND_FACTS_HOME_USER="$ISABELLE_HOME_USER/find_facts"
+FIND_FACTS_INDEXES=""
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
--- a/src/Tools/Find_Facts/src/find_facts.scala	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Wed Jan 22 22:22:37 2025 +0000
@@ -112,6 +112,8 @@
 
   /** Solr data model **/
 
+  val solr_data_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/solr")
+
   object private_data extends Solr.Data("find_facts") {
     /* types */
 
@@ -577,29 +579,52 @@
       } yield block)
   }
 
+  def find_facts_index_command(
+    sessions: List[String],
+    ssh: SSH.System = SSH.Local,
+    isabelle_home: Path = Path.current,
+    options: List[Options.Spec] = Nil,
+    dirs: List[Path] = Nil,
+    clean: Boolean = false,
+    no_build: Boolean = false,
+    verbose: Boolean = false,
+  ): String = {
+    ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " find_facts_index" +
+      dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
+      if_proper(clean, " -c") +
+      if_proper(no_build, " -n") +
+      if_proper(verbose, " -v") +
+      Options.Spec.bash_strings(options, bg = true) +
+      sessions.map(session => " " + session).mkString
+  }
+
   def find_facts_index(
     options: Options,
     sessions: List[String],
+    afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
     clean: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     val store = Store(options)
+    val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
     val session = Session(options, Resources.bootstrap)
 
     val selection = Sessions.Selection(sessions = sessions)
-    val session_structure = Sessions.load_structure(options, dirs = dirs).selection(selection)
+    val session_structure =
+      Sessions.load_structure(options, dirs = AFP.main_dirs(afp_root) ::: dirs).selection(selection)
     val deps = Sessions.Deps.load(session_structure)
     val browser_info_context = Browser_Info.context(session_structure)
 
     if (sessions.isEmpty) progress.echo("Nothing to index")
     else {
+      val start_date = Date.now()
       val stats =
-        using(Solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
+        using(solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
           using(Export.open_database_context(store)) { database_context =>
             val document_info = Document_Info.read(database_context, deps, sessions)
-            
+
             def index_session(session_name: String): Unit = {
               using(database_context.open_session0(session_name)) { session_context =>
                 val info = session_structure(session_name)
@@ -611,7 +636,7 @@
                   Build.read_theory(theory_context) match {
                     case None => progress.echo_warning("No snapshot for theory " + name.theory)
                     case Some(snapshot) =>
-                      progress.echo("Theory " + name.theory + " ...")
+                      progress.echo("Indexing theory " + quote(name.theory), verbose = true)
                       val blocks =
                         make_thy_blocks(options, session, browser_info_context, document_info,
                           theory_context, snapshot, info.chapter)
@@ -628,8 +653,9 @@
           Find_Facts.query_stats(db, query)
         }
 
-      progress.echo("Indexed " + stats.results + " blocks with " +
-        stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
+      val timing = Date.now() - start_date
+      progress.echo("Indexed " + stats.results + " blocks with " + stats.consts + " consts, " +
+        stats.typs + " typs, " + stats.thms + " thms in " + timing.message)
     }
   }
 
@@ -638,6 +664,7 @@
 
   def main_tool1(args: Array[String]): Unit = {
     Command_Line.tool {
+      var afp_root: Option[Path] = None
       var clean = false
       val dirs_buffer = new mutable.ListBuffer[Path]
       var no_build = false
@@ -648,6 +675,7 @@
   Usage: isabelle find_facts_index [OPTIONS] [SESSIONS ...]
 
     Options are:
+      -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
       -c           clean previous index
       -d DIR       include session directory
       -n           no build -- take existing session build databases
@@ -656,6 +684,7 @@
 
     Build and index sessions for Find_Facts.
   """,
+        "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "c" -> (_ => clean = true),
         "d:" -> (arg => dirs_buffer += Path.explode(arg)),
         "n" -> (_ => no_build = true),
@@ -673,7 +702,7 @@
       if (!no_build) {
         def build(test: Boolean = false): Build.Results =
           Build.build(options, selection = Sessions.Selection(sessions = sessions), dirs = dirs,
-            no_build = test, progress = if (test) new Progress else progress)
+            afp_root = afp_root, no_build = test, progress = if (test) new Progress else progress)
 
         progress.interrupt_handler {
           if (!build(test = true).ok) {
@@ -690,56 +719,66 @@
 
       /* index */
 
-      find_facts_index(options, sessions, dirs = dirs, clean = clean, progress = progress)
+      find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root, clean = clean,
+        progress = progress)
     }
   }
 
 
-
   /** index components **/
 
-  def find_facts_index_component(
-    options: Options,
+  def resolve_indexes(solr: Solr.System): Unit =
+    for {
+      path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES"))
+      database = Library.perhaps_unprefix("find_facts-", path.file_name)
+      database_dir = solr.database_dir(database)
+      if !database_dir.is_dir
+    } Isabelle_System.copy_dir(path, database_dir, direct = true)
+
+  def find_facts_index_build(
+    database: String,
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
-    val database = options.string("find_facts_database_name")
+    val solr = Solr.init(solr_data_dir)
 
-    val component = "find_facts_index-" + database
+    val component = "find_facts-" + database
     val component_dir =
       Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
-    Isabelle_System.copy_dir(Solr.database_dir(database), component_dir.path)
-    component_dir.write_settings("SOLR_COMPONENTS=\"$SOLR_COMPONENTS:$COMPONENT/" + database + "\"")
+    Isabelle_System.copy_dir(solr.database_dir(database), component_dir.path)
+    component_dir.write_settings(
+      "FIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
   }
 
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool2 = Isabelle_Tool("find_facts_index_component",
+  val isabelle_tool2 = Isabelle_Tool("find_facts_index_build",
     "build Isabelle component from Find_Facts index", Scala_Project.here,
     { args =>
-      var options = Options.init()
       var target_dir = Path.current
 
       val getopts = Getopts("""
-  Usage: isabelle find_facts_index_component
+  Usage: isabelle find_facts_index_build DATABASE
 
     Options are:
-      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
       -D DIR       target directory (default ".")
 
-    Build Isabelle component from finalized Find_Facts index with given name.
+    Build Isabelle component from finalized Find_Facts index with given database name.
   """,
-        "o:" -> (arg => options = options + arg),
         "D:" -> (arg => target_dir = Path.explode(arg)))
 
       val more_args = getopts(args)
-      if (more_args.nonEmpty) getopts.usage()
+      val database =
+        more_args match {
+          case database :: Nil => database
+          case _ => getopts.usage()
+        }
 
       val progress = new Console_Progress()
 
-      find_facts_index_component(options, target_dir = target_dir, progress = progress)
+      find_facts_index_build(database, target_dir = target_dir, progress = progress)
     })
 
 
@@ -846,19 +885,18 @@
 
   /* find facts */
 
-  val template_web_dir: Path = Path.explode("$FIND_FACTS_HOME/web")
-  val default_web_dir: Path = Path.explode("$FIND_FACTS_WEB")
+  val web_sources: Path = Path.explode("$FIND_FACTS_HOME/web")
+  val web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web")
 
   val default_port = 8080
 
-  def find_facts(
+  def find_facts_server(
     options: Options,
     port: Int = default_port,
     devel: Boolean = false,
-    web_dir: Path = default_web_dir,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.copy_dir(template_web_dir, web_dir, direct = true)
+    Isabelle_System.copy_dir(web_sources, web_dir, direct = true)
 
     val database = options.string("find_facts_database_name")
     val encode = new Encode(options)
@@ -878,7 +916,10 @@
 
     val frontend = project.build_html(progress = progress)
 
-    using(Solr.open_database(database)) { db =>
+    val solr = Solr.init(solr_data_dir)
+    resolve_indexes(solr)
+
+    using(solr.open_database(database)) { db =>
       val stats = Find_Facts.query_stats(db, Query(Nil))
       progress.echo("Started Find_Facts with " + stats.results + " blocks, " +
         stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
@@ -890,7 +931,7 @@
             def apply(request: HTTP.Request): Option[HTTP.Response] =
               Some(HTTP.Response(Bytes(isabelle_style), "text/css"))
           },
-          new HTTP.Service("app") {
+          new HTTP.Service("find_facts") {
             def apply(request: HTTP.Request): Option[HTTP.Response] =
               Some(HTTP.Response.html(
                 if (devel) project.build_html(progress = progress) else frontend))
@@ -917,7 +958,7 @@
           }))
 
       server.start()
-      progress.echo("Server started " + server.toString + "/app")
+      progress.echo("Server started " + server.toString + "/find_facts")
 
       @tailrec
       def loop(): Unit = {
@@ -938,7 +979,6 @@
       var options = Options.init()
       var port = default_port
       var verbose = false
-      var web_dir = default_web_dir
 
       val getopts = Getopts("""
 Usage: isabelle find_facts_server [OPTIONS]
@@ -948,22 +988,20 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p PORT      explicit web server port (default: """ + default_port + """)
     -v           verbose server
-    -w DIR       web directory (default: """ + default_web_dir + """)
 
   Run server for Find_Facts.
 """,
         "d" -> (_ => devel = true),
         "o:" -> (arg => options = options + arg),
         "p:" -> (arg => port = Value.Int.parse(arg)),
-        "v" -> (_ => verbose = true),
-        "w:" -> (arg => web_dir = Path.explode(arg)))
+        "v" -> (_ => verbose = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress(verbose = verbose)
 
-      find_facts(options, port = port, devel = devel, web_dir = web_dir, progress = progress)
+      find_facts_server(options, port = port, devel = devel, progress = progress)
     }
   }
 }
--- a/src/Tools/Find_Facts/src/solr.scala	Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Find_Facts/src/solr.scala	Wed Jan 22 22:22:37 2025 +0000
@@ -23,20 +23,12 @@
 
 
 object Solr {
-  def init(solr_data: Path): Path = {
+  def init(solr_data: Path): System = {
     File.write(Isabelle_System.make_directory(solr_data) + Path.basic("solr.xml"), "<solr/>")
-
-    // non-portable: only for Linux or macOS
-    for (path <- Path.split(Isabelle_System.getenv("SOLR_COMPONENTS"))) {
-      Isabelle_System.symlink(path.absolute, solr_data, force = true)
-    }
-
     java.util.logging.LogManager.getLogManager.reset()
-    solr_data
+    new System(solr_data)
   }
 
-  lazy val solr_data: Path = init(Path.explode("$SOLR_DATA"))
-
 
   /** query language */
 
@@ -347,32 +339,36 @@
 
   /* database */
 
-  def database_dir(database: String): Path = solr_data + Path.basic(database)
+  class System private[Solr](val solr_data: Path) {
+    def database_dir(database: String): Path = solr_data + Path.basic(database)
 
-  def init_database(database: String, data: Data, clean: Boolean = false): Database = {
-    val db_dir = database_dir(database)
+    def init_database(database: String, data: Data, clean: Boolean = false): Database = {
+      val db_dir = database_dir(database)
 
-    if (clean) Isabelle_System.rm_tree(db_dir)
+      if (clean) Isabelle_System.rm_tree(db_dir)
 
-    val conf_dir = db_dir + Path.basic("conf")
-    if (!conf_dir.is_dir) {
-      Isabelle_System.make_directory(conf_dir)
-      File.write(conf_dir + Path.basic("schema.xml"), XML.string_of_body(data.schema))
-      File.write(conf_dir + Path.basic("solrconfig.xml"), XML.string_of_body(data.solr_config))
-      data.more_config.foreach((path, content) => File.write(conf_dir + path, content))
+      val conf_dir = db_dir + Path.basic("conf")
+      if (!conf_dir.is_dir) {
+        Isabelle_System.make_directory(conf_dir)
+        File.write(conf_dir + Path.basic("schema.xml"), XML.string_of_body(data.schema))
+        File.write(conf_dir + Path.basic("solrconfig.xml"), XML.string_of_body(data.solr_config))
+        data.more_config.foreach((path, content) => File.write(conf_dir + path, content))
+      }
+
+      open_database(database)
     }
 
-    open_database(database)
-  }
-
-  def open_database(database: String): Database = {
-    val server = new EmbeddedSolrServer(solr_data.java_path, database)
-
-    val cores = server.getCoreContainer.getAllCoreNames.asScala
-    if (cores.contains(database)) server.getCoreContainer.reload(database)
-    else server.getCoreContainer.create(database, Map.empty.asJava)
-
-    new Database(server)
+    def open_database(database: String): Database =
+      if (!database_dir(database).is_dir) error("Missing Solr database: " + quote(database))
+      else {
+        val server = new EmbeddedSolrServer(solr_data.java_path, database)
+  
+        val cores = server.getCoreContainer.getAllCoreNames.asScala
+        if (cores.contains(database)) server.getCoreContainer.reload(database)
+        else server.getCoreContainer.create(database, Map.empty.asJava)
+  
+        new Database(server)
+      }
   }
 
   class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {