merged;
authorLukas Stevens <mail@lukas-stevens.de>
Fri, 03 Sep 2021 17:54:12 +0200
changeset 74558 59ec97f1665c
parent 74554 fc41b8c3267e (current diff)
parent 74497 8798edfc61ef (diff)
merged;
src/HOL/Library/Mapping.thy
--- a/NEWS	Tue Aug 17 17:09:20 2021 +0200
+++ b/NEWS	Fri Sep 03 17:54:12 2021 +0200
@@ -9,6 +9,17 @@
 
 *** General ***
 
+* Configuration option "show_results" controls output of final results
+in commands like 'definition' or 'theorem'. Output is normally enabled
+in interactive mode, but it could occasionally cause unnecessary
+slowdown. It can be disabled like this:
+
+  context notes [[show_results = true]]
+  begin
+    definition "test = True"
+    theorem test by (simp add: test_def)
+  end
+
 * Timeouts for Isabelle/ML tools are subject to system option
 "timeout_scale" --- this already used for the overall session build
 process before, and allows to adapt to slow machines. The underlying
@@ -195,6 +206,10 @@
 in classes (semi)ring_bit_operations, class semiring_bit_shifts is
 gone.
 
+* Expressions of the form "NOT (numeral _)" are not simplified by
+default any longer.  INCOMPATIBILITY, use not_one_eq and not_numeral_eq
+as simp rule explicitly if needed.
+
 * Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
 as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
 "setBit", "clearBit". See there further the changelog in theory Guide.
--- a/src/Doc/Implementation/Logic.thy	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy	Fri Sep 03 17:54:12 2021 +0200
@@ -585,7 +585,7 @@
   @{define_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   @{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   @{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\
-  @{define_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
+  @{define_ML Thm.generalize: "Symtab.set * Symtab.set -> int -> thm -> thm"} \\
   @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   -> thm -> thm"} \\
   @{define_ML Thm.add_axiom: "Proof.context ->
@@ -646,8 +646,8 @@
 
   \<^descr> \<^ML>\<open>Thm.generalize\<close>~\<open>(\<^vec>\<alpha>, \<^vec>x)\<close> corresponds to the
   \<open>generalize\<close> rules of \figref{fig:subst-rules}. Here collections of type and
-  term variables are generalized simultaneously, specified by the given basic
-  names.
+  term variables are generalized simultaneously, specified by the given sets of
+  basic names.
 
   \<^descr> \<^ML>\<open>Thm.instantiate\<close>~\<open>(\<^vec>\<alpha>\<^sub>s, \<^vec>x\<^sub>\<tau>)\<close> corresponds to the
   \<open>instantiate\<close> rules of \figref{fig:subst-rules}. Type variables are
--- a/src/HOL/Bit_Operations.thy	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Bit_Operations.thy	Fri Sep 03 17:54:12 2021 +0200
@@ -758,6 +758,10 @@
   \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
   using one_xor_eq [of a] by (simp add: ac_simps)
 
+lemma xor_self_eq [simp]:
+  \<open>a XOR a = 0\<close>
+  by (rule bit_eqI) (simp add: bit_simps)
+
 lemma bit_iff_odd_drop_bit:
   \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
   by (simp add: bit_iff_odd drop_bit_eq_div)
@@ -1319,7 +1323,7 @@
   \<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
   by (simp add: bit_minus_iff bit_1_iff)
 
-lemma not_one [simp]:
+lemma not_one_eq:
   \<open>NOT 1 = - 2\<close>
   by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
 
@@ -1464,7 +1468,7 @@
   \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
   by (cases k) (simp_all add: not_int_def divide_int_def nat_add_distrib)
 
-lemma bit_not_int_iff [bit_simps]:
+lemma bit_not_int_iff:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
   for k :: int
   by (simp add: bit_not_int_iff' not_int_def)
@@ -2057,6 +2061,11 @@
     else \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> for k l :: int
   by (auto simp add: xor_int_rec [of k l] not_int_def elim!: oddE)
 
+lemma bit_minus_int_iff:
+  \<open>bit (- k) n \<longleftrightarrow> bit (NOT (k - 1)) n\<close>
+  for k :: int
+  by (simp add: bit_simps)
+
 
 subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
@@ -2215,7 +2224,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>
+  \<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)
   
 
@@ -2308,10 +2317,6 @@
   \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
   by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div)
 
-lemma bit_push_bit_iff_of_nat_iff [bit_simps]:
-  \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
-  by (auto simp add: bit_push_bit_iff)
-
 lemma take_bit_sum:
   "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))"
   for n :: nat
@@ -2338,6 +2343,293 @@
 instance int :: unique_euclidean_semiring_with_bit_operations ..
 
 
+subsection \<open>Symbolic computations on numeral expressions\<close>
+
+context unique_euclidean_semiring_with_bit_operations
+begin
+
+lemma bit_numeral_iff:
+  \<open>bit (numeral m) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
+  using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
+
+lemma bit_numeral_Bit0_Suc_iff [simp]:
+  \<open>bit (numeral (Num.Bit0 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
+  by (simp add: bit_Suc numeral_Bit0_div_2)
+
+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)
+
+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>
+  \<open>bit (numeral (Num.Bit1 w)) n \<longleftrightarrow> (case n of 0 \<Rightarrow> True | Suc m \<Rightarrow> bit (numeral w) m)\<close>
+  by (cases n; simp)+
+
+lemma bit_numeral_simps [simp]:
+  \<open>\<not> bit 1 (numeral n)\<close>
+  \<open>bit (numeral (Num.Bit0 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
+  \<open>bit (numeral (Num.Bit1 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
+  by (simp_all add: bit_1_iff numeral_eq_Suc)
+
+lemma and_numerals [simp]:
+  \<open>1 AND numeral (Num.Bit0 y) = 0\<close>
+  \<open>1 AND numeral (Num.Bit1 y) = 1\<close>
+  \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = 2 * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = 2 * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) AND 1 = 0\<close>
+  \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = 2 * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + 2 * (numeral x AND numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) AND 1 = 1\<close>
+  by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+fun and_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+  \<open>and_num num.One num.One = Some num.One\<close>
+| \<open>and_num num.One (num.Bit0 n) = None\<close>
+| \<open>and_num num.One (num.Bit1 n) = Some num.One\<close>
+| \<open>and_num (num.Bit0 m) num.One = None\<close>
+| \<open>and_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit1 m) num.One = Some num.One\<close>
+| \<open>and_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
+| \<open>and_num (num.Bit1 m) (num.Bit1 n) = (case and_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
+
+lemma numeral_and_num:
+  \<open>numeral m AND numeral n = (case and_num m n of None \<Rightarrow> 0 | Some n' \<Rightarrow> numeral n')\<close>
+  by (induction m n rule: and_num.induct) (simp_all add: split: option.split)
+
+lemma and_num_eq_None_iff:
+  \<open>and_num m n = None \<longleftrightarrow> numeral m AND numeral n = 0\<close>
+  by (simp add: numeral_and_num split: option.split)
+
+lemma and_num_eq_Some_iff:
+  \<open>and_num m n = Some q \<longleftrightarrow> numeral m AND numeral n = numeral q\<close>
+  by (simp add: numeral_and_num split: option.split)
+
+lemma or_numerals [simp]:
+  \<open>1 OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
+  \<open>1 OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\<close>
+  \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = 2 * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + 2 * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) OR 1 = numeral (Num.Bit1 x)\<close>
+  \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + 2 * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + 2 * (numeral x OR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) OR 1 = numeral (Num.Bit1 x)\<close>
+  by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+fun or_num :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+  \<open>or_num num.One num.One = num.One\<close>
+| \<open>or_num num.One (num.Bit0 n) = num.Bit1 n\<close>
+| \<open>or_num num.One (num.Bit1 n) = num.Bit1 n\<close>
+| \<open>or_num (num.Bit0 m) num.One = num.Bit1 m\<close>
+| \<open>or_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (or_num m n)\<close>
+| \<open>or_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
+| \<open>or_num (num.Bit1 m) num.One = num.Bit1 m\<close>
+| \<open>or_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (or_num m n)\<close>
+| \<open>or_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
+
+lemma numeral_or_num:
+  \<open>numeral m OR numeral n = numeral (or_num m n)\<close>
+  by (induction m n rule: or_num.induct) simp_all
+
+lemma numeral_or_num_eq:
+  \<open>numeral (or_num m n) = numeral m OR numeral n\<close>
+  by (simp add: numeral_or_num)
+
+lemma xor_numerals [simp]:
+  \<open>1 XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
+  \<open>1 XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\<close>
+  \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = 2 * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + 2 * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit0 x) XOR 1 = numeral (Num.Bit1 x)\<close>
+  \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + 2 * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = 2 * (numeral x XOR numeral y)\<close>
+  \<open>numeral (Num.Bit1 x) XOR 1 = numeral (Num.Bit0 x)\<close>
+  by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+fun xor_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+  \<open>xor_num num.One num.One = None\<close>
+| \<open>xor_num num.One (num.Bit0 n) = Some (num.Bit1 n)\<close>
+| \<open>xor_num num.One (num.Bit1 n) = Some (num.Bit0 n)\<close>
+| \<open>xor_num (num.Bit0 m) num.One = Some (num.Bit1 m)\<close>
+| \<open>xor_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (xor_num m n)\<close>
+| \<open>xor_num (num.Bit0 m) (num.Bit1 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
+| \<open>xor_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>xor_num (num.Bit1 m) (num.Bit0 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
+| \<open>xor_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (xor_num m n)\<close>
+
+lemma numeral_xor_num:
+  \<open>numeral m XOR numeral n = (case xor_num m n of None \<Rightarrow> 0 | Some n' \<Rightarrow> numeral n')\<close>
+  by (induction m n rule: xor_num.induct) (simp_all split: option.split)
+
+lemma xor_num_eq_None_iff:
+  \<open>xor_num m n = None \<longleftrightarrow> numeral m XOR numeral n = 0\<close>
+  by (simp add: numeral_xor_num split: option.split)
+
+lemma xor_num_eq_Some_iff:
+  \<open>xor_num m n = Some q \<longleftrightarrow> numeral m XOR numeral n = numeral q\<close>
+  by (simp add: numeral_xor_num split: option.split)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma minus_numeral_inc_eq:
+  \<open>- numeral (Num.inc n) = NOT (numeral n)\<close>
+  by (simp add: not_eq_complement sub_inc_One_eq add_One)
+
+lemma sub_one_eq_not_neg:
+  \<open>Num.sub n num.One = NOT (- numeral n)\<close>
+  by (simp add: not_eq_complement)
+
+lemma minus_numeral_eq_not_sub_one:
+  \<open>- numeral n = NOT (Num.sub n num.One)\<close>
+  by (simp add: not_eq_complement)
+
+lemma not_numeral_eq:
+  \<open>NOT (numeral n) = - numeral (Num.inc n)\<close>
+  by (simp add: minus_numeral_inc_eq)
+
+lemma not_minus_numeral_eq [simp]:
+  \<open>NOT (- numeral n) = Num.sub n num.One\<close>
+  by (simp add: sub_one_eq_not_neg)
+
+lemma minus_not_numeral_eq [simp]:
+  \<open>- (NOT (numeral n)) = numeral (Num.inc n)\<close>
+  by (simp add: not_numeral_eq)
+
+end
+
+lemma bit_minus_numeral_int [simp]:
+  \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
+  by (simp_all add: bit_minus_iff bit_not_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq)
+
+lemma and_not_numerals [simp]:
+  \<open>1 AND NOT 1 = (0 :: int)\<close>
+  \<open>1 AND NOT (numeral (Num.Bit0 n)) = (1 :: int)\<close>
+  \<open>1 AND NOT (numeral (Num.Bit1 n)) = (0 :: int)\<close>
+  \<open>numeral (Num.Bit0 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
+  \<open>numeral (Num.Bit0 m) AND NOT (numeral (Num.Bit0 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+  \<open>numeral (Num.Bit0 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+  \<open>numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
+  \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+  \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
+  by (simp_all add: bit_eq_iff) (auto simp add: bit_simps bit_Suc bit_numeral_rec BitM_inc_eq split: nat.splits)
+
+lemma and_not_not_numerals [simp]:
+  \<open>NOT 1 AND NOT 1 = NOT (1 :: int)\<close>
+  \<open>NOT 1 AND NOT (numeral n) = NOT (1 OR numeral n :: int)\<close>
+  \<open>NOT (numeral m) AND NOT 1 = NOT (numeral m OR 1 :: int)\<close>
+  \<open>NOT (numeral m) AND NOT (numeral n) = NOT (numeral m OR numeral n :: int)\<close>
+  by simp_all
+
+lemma and_minus_numerals [simp]:
+  \<open>- 1 AND k = k\<close>
+  \<open>k AND - 1 = k\<close>
+  \<open>- numeral n AND k = NOT (neg_numeral_class.sub n num.One) AND k\<close>
+  \<open>k AND - numeral n = k AND NOT (neg_numeral_class.sub n num.One)\<close> for k :: int
+  by (simp_all add: minus_numeral_eq_not_sub_one)
+
+fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+  \<open>and_not_num num.One num.One = None\<close>
+| \<open>and_not_num num.One (num.Bit0 n) = Some num.One\<close>
+| \<open>and_not_num num.One (num.Bit1 n) = None\<close>
+| \<open>and_not_num (num.Bit0 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>and_not_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_not_num m n)\<close>
+| \<open>and_not_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
+| \<open>and_not_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
+| \<open>and_not_num (num.Bit1 m) (num.Bit0 n) = (case and_not_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
+| \<open>and_not_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
+
+lemma int_numeral_and_not_num:
+  \<open>numeral m AND NOT (numeral n) = (case and_not_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+  by (induction m n rule: and_not_num.induct) (simp_all split: option.split)
+
+lemma int_numeral_not_and_num:
+  \<open>NOT (numeral m) AND numeral n = (case and_not_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
+  using int_numeral_and_not_num [of n m] by (simp add: ac_simps)
+
+lemma and_not_num_eq_None_iff:
+  \<open>and_not_num m n = None \<longleftrightarrow> numeral m AND NOT (numeral n) = (0 :: int)\<close>
+  by (simp add: int_numeral_and_not_num split: option.split)
+
+lemma and_not_num_eq_Some_iff:
+  \<open>and_not_num m n = Some q \<longleftrightarrow> numeral m AND NOT (numeral n) = (numeral q :: int)\<close>
+  by (simp add: int_numeral_and_not_num split: option.split)
+
+lemma or_not_numerals [simp]:
+  \<open>1 OR NOT 1 = NOT (0 :: int)\<close>
+  \<open>1 OR NOT (numeral (Num.Bit0 n)) = NOT (numeral (Num.Bit0 n) :: int)\<close>
+  \<open>1 OR NOT (numeral (Num.Bit1 n)) = NOT (numeral (Num.Bit0 n) :: int)\<close>
+  \<open>numeral (Num.Bit0 m) OR NOT (1 :: int) = NOT (1 :: int)\<close>
+  \<open>numeral (Num.Bit0 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+  \<open>numeral (Num.Bit0 m) OR NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+  \<open>numeral (Num.Bit1 m) OR NOT (1 :: int) = NOT (0 :: int)\<close>
+  \<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+  \<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit1 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
+  by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits)
+
+lemma or_and_numerals [simp]:
+  \<open>NOT 1 OR 1 = NOT (0 :: int)\<close>
+  \<open>NOT 1 OR numeral n = numeral n OR NOT (1 :: int)\<close>
+  \<open>NOT (numeral m) OR 1 = 1 OR NOT (numeral m :: int)\<close>
+  \<open>NOT (numeral m) OR (numeral n) = numeral n OR NOT (numeral m :: int)\<close>
+  by (simp_all add: ac_simps)
+
+lemma or_not_not_numerals [simp]:
+  \<open>NOT 1 OR NOT 1 = NOT (1 :: int)\<close>
+  \<open>NOT 1 OR NOT (numeral n) = NOT (1 AND numeral n :: int)\<close>
+  \<open>NOT (numeral m) OR NOT 1 = NOT (numeral m AND 1 :: int)\<close>
+  \<open>NOT (numeral m) OR NOT (numeral n) = NOT (numeral m AND numeral n :: int)\<close>
+  by simp_all
+
+lemma or_minus_numerals [simp]:
+  \<open>- 1 OR k = - 1\<close>
+  \<open>k OR - 1 = - 1\<close>
+  \<open>- numeral n OR k = NOT (neg_numeral_class.sub n num.One) OR k\<close>
+  \<open>k OR - numeral n = k OR NOT (neg_numeral_class.sub n num.One)\<close> for k :: int
+  by (simp_all add: minus_numeral_eq_not_sub_one)
+
+fun or_not_num_neg :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
+where
+  \<open>or_not_num_neg num.One num.One = num.One\<close>
+| \<open>or_not_num_neg num.One (num.Bit0 m) = num.Bit1 m\<close>
+| \<open>or_not_num_neg num.One (num.Bit1 m) = num.Bit1 m\<close>
+| \<open>or_not_num_neg (num.Bit0 n) num.One = num.Bit0 num.One\<close>
+| \<open>or_not_num_neg (num.Bit0 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit0 n) (num.Bit1 m) = num.Bit0 (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit1 n) num.One = num.One\<close>
+| \<open>or_not_num_neg (num.Bit1 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
+| \<open>or_not_num_neg (num.Bit1 n) (num.Bit1 m) = Num.BitM (or_not_num_neg n m)\<close>
+
+lemma int_numeral_or_not_num_neg:
+  \<open>numeral m OR NOT (numeral n :: int) = - numeral (or_not_num_neg m n)\<close>
+  apply (induction m n rule: or_not_num_neg.induct)
+  apply simp_all
+    apply (simp_all add: not_one_eq not_numeral_eq)
+  done
+
+lemma int_numeral_not_or_num_neg:
+  \<open>NOT (numeral m) OR (numeral n :: int) = - numeral (or_not_num_neg n m)\<close>
+  using int_numeral_or_not_num_neg [of n m] by (simp add: ac_simps)
+
+lemma numeral_or_not_num_eq:
+  \<open>numeral (or_not_num_neg m n) = - (numeral m OR NOT (numeral n :: int))\<close>
+  using int_numeral_or_not_num_neg [of m n] by simp
+
+lemma xor_minus_numerals [simp]:
+  \<open>- 1 XOR k = NOT k\<close>
+  \<open>k XOR - 1 = NOT k\<close>
+  \<open>- numeral n XOR k = NOT (neg_numeral_class.sub n num.One XOR k)\<close>
+  \<open>k XOR - numeral n = NOT (k XOR (neg_numeral_class.sub n num.One))\<close> for k :: int
+  by (simp_all add: minus_numeral_eq_not_sub_one)
+
+
 subsection \<open>More properties\<close>
 
 lemma take_bit_eq_mask_iff:
@@ -2425,6 +2717,10 @@
   \<open>of_int (NOT k) = NOT (of_int k)\<close>
   by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff)
 
+lemma of_int_not_numeral:
+  \<open>of_int (NOT (numeral k)) = NOT (numeral k)\<close>
+  by (simp add: local.of_int_not_eq)
+
 lemma of_int_and_eq:
   \<open>of_int (k AND l) = of_int k AND of_int l\<close>
   by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff)
@@ -2547,157 +2843,6 @@
   by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
     dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
 
-lemma minus_numeral_inc_eq:
-  \<open>- numeral (Num.inc n) = NOT (numeral n :: int)\<close>
-  by (simp add: not_int_def sub_inc_One_eq add_One)
-
-lemma sub_one_eq_not_neg:
-  \<open>Num.sub n num.One = NOT (- numeral n :: int)\<close>
-  by (simp add: not_int_def)
-
-lemma bit_numeral_int_iff [bit_simps]:
-  \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
-  using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
-
-lemma bit_minus_int_iff [bit_simps]:
-  \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
-  for k :: int
-  using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
-
-lemma bit_numeral_int_simps [simp]:
-  \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
-  by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
-
-lemma bit_numeral_Bit0_Suc_iff [simp]:
-  \<open>bit (numeral (Num.Bit0 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
-  by (simp add: bit_Suc)
-
-lemma bit_numeral_Bit1_Suc_iff [simp]:
-  \<open>bit (numeral (Num.Bit1 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
-  by (simp add: bit_Suc)
-
-lemma int_not_numerals [simp]:
-  \<open>NOT (numeral (Num.Bit0 n) :: int) = - numeral (Num.Bit1 n)\<close>
-  \<open>NOT (numeral (Num.Bit1 n) :: int) = - numeral (Num.inc (num.Bit1 n))\<close>
-  \<open>NOT (numeral (Num.BitM n) :: int) = - numeral (num.Bit0 n)\<close>
-  \<open>NOT (- numeral (Num.Bit0 n) :: int) = numeral (Num.BitM n)\<close>
-  \<open>NOT (- numeral (Num.Bit1 n) :: int) = numeral (Num.Bit0 n)\<close>
-  by (simp_all add: not_int_def add_One inc_BitM_eq) 
-
-text \<open>FIXME: The rule sets below are very large (24 rules for each
-  operator). Is there a simpler way to do this?\<close>
-
-context
-begin
-
-private lemma eqI:
-  \<open>k = l\<close>
-  if num: \<open>\<And>n. bit k (numeral n) \<longleftrightarrow> bit l (numeral n)\<close>
-    and even: \<open>even k \<longleftrightarrow> even l\<close>
-  for k l :: int
-proof (rule bit_eqI)
-  fix n
-  show \<open>bit k n \<longleftrightarrow> bit l n\<close>
-  proof (cases n)
-    case 0
-    with even show ?thesis
-      by simp
-  next
-    case (Suc n)
-    with num [of \<open>num_of_nat (Suc n)\<close>] show ?thesis
-      by (simp only: numeral_num_of_nat)
-  qed
-qed
-
-lemma int_and_numerals [simp]:
-  \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))\<close>
-  \<open>numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))\<close>
-  \<open>- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))\<close>
-  \<open>- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))\<close>
-  \<open>(1::int) AND numeral (Num.Bit0 y) = 0\<close>
-  \<open>(1::int) AND numeral (Num.Bit1 y) = 1\<close>
-  \<open>(1::int) AND - numeral (Num.Bit0 y) = 0\<close>
-  \<open>(1::int) AND - numeral (Num.Bit1 y) = 1\<close>
-  \<open>numeral (Num.Bit0 x) AND (1::int) = 0\<close>
-  \<open>numeral (Num.Bit1 x) AND (1::int) = 1\<close>
-  \<open>- numeral (Num.Bit0 x) AND (1::int) = 0\<close>
-  \<open>- numeral (Num.Bit1 x) AND (1::int) = 1\<close>
-  by (auto simp add: bit_and_iff bit_minus_iff even_and_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq intro: eqI)
-
-lemma int_or_numerals [simp]:
-  \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\<close>
-  \<open>numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\<close>
-  \<open>- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))\<close>
-  \<open>- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))\<close>
-  \<open>(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
-  \<open>(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\<close>
-  \<open>(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\<close>
-  \<open>(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)\<close>
-  \<open>numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)\<close>
-  \<open>numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)\<close>
-  \<open>- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)\<close>
-  \<open>- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)\<close>
-  by (auto simp add: bit_or_iff bit_minus_iff even_or_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
-
-lemma int_xor_numerals [simp]:
-  \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)\<close>
-  \<open>numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))\<close>
-  \<open>numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)\<close>
-  \<open>numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))\<close>
-  \<open>- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)\<close>
-  \<open>- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))\<close>
-  \<open>- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)\<close>
-  \<open>- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))\<close>
-  \<open>(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\<close>
-  \<open>(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\<close>
-  \<open>(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\<close>
-  \<open>(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))\<close>
-  \<open>numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)\<close>
-  \<open>numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)\<close>
-  \<open>- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)\<close>
-  \<open>- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))\<close>
-  by (auto simp add: bit_xor_iff bit_minus_iff even_xor_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)
-
-end
-
 context semiring_bit_operations
 begin
 
@@ -3368,129 +3513,6 @@
 qed
 
 
-subsection \<open>Symbolic computations on numeral expressions\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
-
-fun and_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
-where
-  \<open>and_num num.One num.One = Some num.One\<close>
-| \<open>and_num num.One (num.Bit0 n) = None\<close>
-| \<open>and_num num.One (num.Bit1 n) = Some num.One\<close>
-| \<open>and_num (num.Bit0 m) num.One = None\<close>
-| \<open>and_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
-| \<open>and_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_num m n)\<close>
-| \<open>and_num (num.Bit1 m) num.One = Some num.One\<close>
-| \<open>and_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\<close>
-| \<open>and_num (num.Bit1 m) (num.Bit1 n) = (case and_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
-
-fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
-where
-  \<open>and_not_num num.One num.One = None\<close>
-| \<open>and_not_num num.One (num.Bit0 n) = Some num.One\<close>
-| \<open>and_not_num num.One (num.Bit1 n) = None\<close>
-| \<open>and_not_num (num.Bit0 m) num.One = Some (num.Bit0 m)\<close>
-| \<open>and_not_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_not_num m n)\<close>
-| \<open>and_not_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
-| \<open>and_not_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
-| \<open>and_not_num (num.Bit1 m) (num.Bit0 n) = (case and_not_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))\<close>
-| \<open>and_not_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\<close>
-
-fun or_num :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close>
-where
-  \<open>or_num num.One num.One = num.One\<close>
-| \<open>or_num num.One (num.Bit0 n) = num.Bit1 n\<close>
-| \<open>or_num num.One (num.Bit1 n) = num.Bit1 n\<close>
-| \<open>or_num (num.Bit0 m) num.One = num.Bit1 m\<close>
-| \<open>or_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (or_num m n)\<close>
-| \<open>or_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
-| \<open>or_num (num.Bit1 m) num.One = num.Bit1 m\<close>
-| \<open>or_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (or_num m n)\<close>
-| \<open>or_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (or_num m n)\<close>
-
-fun or_not_num_neg :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close>
-where
-  \<open>or_not_num_neg num.One num.One = num.One\<close>
-| \<open>or_not_num_neg num.One (num.Bit0 m) = num.Bit1 m\<close>
-| \<open>or_not_num_neg num.One (num.Bit1 m) = num.Bit1 m\<close>
-| \<open>or_not_num_neg (num.Bit0 n) num.One = num.Bit0 num.One\<close>
-| \<open>or_not_num_neg (num.Bit0 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
-| \<open>or_not_num_neg (num.Bit0 n) (num.Bit1 m) = num.Bit0 (or_not_num_neg n m)\<close>
-| \<open>or_not_num_neg (num.Bit1 n) num.One = num.One\<close>
-| \<open>or_not_num_neg (num.Bit1 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\<close>
-| \<open>or_not_num_neg (num.Bit1 n) (num.Bit1 m) = Num.BitM (or_not_num_neg n m)\<close>
-
-fun xor_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close>
-where
-  \<open>xor_num num.One num.One = None\<close>
-| \<open>xor_num num.One (num.Bit0 n) = Some (num.Bit1 n)\<close>
-| \<open>xor_num num.One (num.Bit1 n) = Some (num.Bit0 n)\<close>
-| \<open>xor_num (num.Bit0 m) num.One = Some (num.Bit1 m)\<close>
-| \<open>xor_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (xor_num m n)\<close>
-| \<open>xor_num (num.Bit0 m) (num.Bit1 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
-| \<open>xor_num (num.Bit1 m) num.One = Some (num.Bit0 m)\<close>
-| \<open>xor_num (num.Bit1 m) (num.Bit0 n) = Some (case xor_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')\<close>
-| \<open>xor_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (xor_num m n)\<close>
-
-lemma int_numeral_and_num:
-  \<open>numeral m AND numeral n = (case and_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
-  by (induction m n rule: and_num.induct) (simp_all split: option.split)
-
-lemma and_num_eq_None_iff:
-  \<open>and_num m n = None \<longleftrightarrow> numeral m AND numeral n = (0::int)\<close>
-  by (simp add: int_numeral_and_num split: option.split)
-
-lemma and_num_eq_Some_iff:
-  \<open>and_num m n = Some q \<longleftrightarrow> numeral m AND numeral n = (numeral q :: int)\<close>
-  by (simp add: int_numeral_and_num split: option.split)
-
-lemma int_numeral_and_not_num:
-  \<open>numeral m AND NOT (numeral n) = (case and_not_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
-  by (induction m n rule: and_not_num.induct) (simp_all add: add_One BitM_inc_eq not_int_def split: option.split)
-
-lemma int_numeral_not_and_num:
-  \<open>NOT (numeral m) AND numeral n = (case and_not_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
-  using int_numeral_and_not_num [of n m] by (simp add: ac_simps)
-
-lemma and_not_num_eq_None_iff:
-  \<open>and_not_num m n = None \<longleftrightarrow> numeral m AND NOT (numeral n) = (0::int)\<close>
-  by (simp add: int_numeral_and_not_num split: option.split)
-
-lemma and_not_num_eq_Some_iff:
-  \<open>and_not_num m n = Some q \<longleftrightarrow> numeral m AND NOT (numeral n) = (numeral q :: int)\<close>
-  by (simp add: int_numeral_and_not_num split: option.split)
-
-lemma int_numeral_or_num:
-  \<open>numeral m OR numeral n = (numeral (or_num m n) :: int)\<close>
-  by (induction m n rule: or_num.induct) simp_all
-
-lemma numeral_or_num_eq:
-  \<open>numeral (or_num m n) = (numeral m OR numeral n :: int)\<close>
-  by (simp add: int_numeral_or_num)
-
-lemma int_numeral_or_not_num_neg:
-  \<open>numeral m OR NOT (numeral n :: int) = - numeral (or_not_num_neg m n)\<close>
-  by (induction m n rule: or_not_num_neg.induct) (simp_all add: add_One BitM_inc_eq not_int_def)
-
-lemma int_numeral_not_or_num_neg:
-  \<open>NOT (numeral m) OR (numeral n :: int) = - numeral (or_not_num_neg n m)\<close>
-  using int_numeral_or_not_num_neg [of n m] by (simp add: ac_simps)
-
-lemma numeral_or_not_num_eq:
-  \<open>numeral (or_not_num_neg m n) = - (numeral m OR NOT (numeral n :: int))\<close>
-  using int_numeral_or_not_num_neg [of m n] by simp
-
-lemma int_numeral_xor_num:
-  \<open>numeral m XOR numeral n = (case xor_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')\<close>
-  by (induction m n rule: xor_num.induct) (simp_all split: option.split)
-
-lemma xor_num_eq_None_iff:
-  \<open>xor_num m n = None \<longleftrightarrow> numeral m XOR numeral n = (0::int)\<close>
-  by (simp add: int_numeral_xor_num split: option.split)
-
-lemma xor_num_eq_Some_iff:
-  \<open>xor_num m n = Some q \<longleftrightarrow> numeral m XOR numeral n = (numeral q :: int)\<close>
-  by (simp add: int_numeral_xor_num split: option.split)
-
-
 subsection \<open>Key ideas of bit operations\<close>
 
 text \<open>
--- a/src/HOL/Eisbach/match_method.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -173,7 +173,7 @@
 
                   val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
                     |> Conjunction.intr_balanced
-                    |> Drule.generalize ([], map fst abs_nms)
+                    |> Drule.generalize (Symtab.empty, Symtab.make_set (map fst abs_nms))
                     |> Thm.tag_free_dummy;
 
                   val atts = map (Attrib.attribute ctxt') att;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Functions.thy	Fri Sep 03 17:54:12 2021 +0200
@@ -0,0 +1,519 @@
+(*  Title:      HOL/ex/Functions.thy
+    Author:     Alexander Krauss, TU Muenchen
+*)
+
+section \<open>Examples of function definitions\<close>
+
+theory Functions
+imports Main "HOL-Library.Monad_Syntax"
+begin
+
+subsection \<open>Very basic\<close>
+
+fun fib :: "nat \<Rightarrow> nat"
+where
+  "fib 0 = 1"
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
+text \<open>Partial simp and induction rules:\<close>
+thm fib.psimps
+thm fib.pinduct
+
+text \<open>There is also a cases rule to distinguish cases along the definition:\<close>
+thm fib.cases
+
+
+text \<open>Total simp and induction rules:\<close>
+thm fib.simps
+thm fib.induct
+
+text \<open>Elimination rules:\<close>
+thm fib.elims
+
+
+subsection \<open>Currying\<close>
+
+fun add
+where
+  "add 0 y = y"
+| "add (Suc x) y = Suc (add x y)"
+
+thm add.simps
+thm add.induct  \<comment> \<open>Note the curried induction predicate\<close>
+
+
+subsection \<open>Nested recursion\<close>
+
+function nz
+where
+  "nz 0 = 0"
+| "nz (Suc x) = nz (nz x)"
+by pat_completeness auto
+
+lemma nz_is_zero:  \<comment> \<open>A lemma we need to prove termination\<close>
+  assumes trm: "nz_dom x"
+  shows "nz x = 0"
+using trm
+by induct (auto simp: nz.psimps)
+
+termination nz
+  by (relation "less_than") (auto simp:nz_is_zero)
+
+thm nz.simps
+thm nz.induct
+
+
+subsubsection \<open>Here comes McCarthy's 91-function\<close>
+
+function f91 :: "nat \<Rightarrow> nat"
+where
+  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
+by pat_completeness auto
+
+text \<open>Prove a lemma before attempting a termination proof:\<close>
+lemma f91_estimate:
+  assumes trm: "f91_dom n"
+  shows "n < f91 n + 11"
+using trm by induct (auto simp: f91.psimps)
+
+termination
+proof
+  let ?R = "measure (\<lambda>x. 101 - x)"
+  show "wf ?R" ..
+
+  fix n :: nat
+  assume "\<not> 100 < n"  \<comment> \<open>Inner call\<close>
+  then show "(n + 11, n) \<in> ?R" by simp
+
+  assume inner_trm: "f91_dom (n + 11)"  \<comment> \<open>Outer call\<close>
+  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
+  with \<open>\<not> 100 < n\<close> show "(f91 (n + 11), n) \<in> ?R" by simp
+qed
+
+text \<open>Now trivial (even though it does not belong here):\<close>
+lemma "f91 n = (if 100 < n then n - 10 else 91)"
+  by (induct n rule: f91.induct) auto
+
+
+subsubsection \<open>Here comes Takeuchi's function\<close>
+
+definition tak_m1 where "tak_m1 = (\<lambda>(x,y,z). if x \<le> y then 0 else 1)"
+definition tak_m2 where "tak_m2 = (\<lambda>(x,y,z). nat (Max {x, y, z} - Min {x, y, z}))"
+definition tak_m3 where "tak_m3 = (\<lambda>(x,y,z). nat (x - Min {x, y, z}))"
+
+function tak :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
+  "tak x y z = (if x \<le> y then y else tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y))"
+  by auto
+
+lemma tak_pcorrect:
+  "tak_dom (x, y, z) \<Longrightarrow> tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
+  by (induction x y z rule: tak.pinduct) (auto simp: tak.psimps)
+
+termination
+  by (relation "tak_m1 <*mlex*> tak_m2 <*mlex*> tak_m3 <*mlex*> {}")
+     (auto simp: mlex_iff wf_mlex tak_pcorrect tak_m1_def tak_m2_def tak_m3_def min_def max_def)
+
+theorem tak_correct: "tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
+  by (induction x y z rule: tak.induct) auto
+
+
+subsection \<open>More general patterns\<close>
+
+subsubsection \<open>Overlapping patterns\<close>
+
+text \<open>
+  Currently, patterns must always be compatible with each other, since
+  no automatic splitting takes place. But the following definition of
+  GCD is OK, although patterns overlap:
+\<close>
+
+fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "gcd2 x 0 = x"
+| "gcd2 0 y = y"
+| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
+                                    else gcd2 (x - y) (Suc y))"
+
+thm gcd2.simps
+thm gcd2.induct
+
+
+subsubsection \<open>Guards\<close>
+
+text \<open>We can reformulate the above example using guarded patterns:\<close>
+
+function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "gcd3 x 0 = x"
+| "gcd3 0 y = y"
+| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
+| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y"
+  apply (case_tac x, case_tac a, auto)
+  apply (case_tac ba, auto)
+  done
+termination by lexicographic_order
+
+thm gcd3.simps
+thm gcd3.induct
+
+
+text \<open>General patterns allow even strange definitions:\<close>
+
+function ev :: "nat \<Rightarrow> bool"
+where
+  "ev (2 * n) = True"
+| "ev (2 * n + 1) = False"
+proof -  \<comment> \<open>completeness is more difficult here \dots\<close>
+  fix P :: bool
+  fix x :: nat
+  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
+    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
+  have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
+  show P
+  proof (cases "x mod 2 = 0")
+    case True
+    with divmod have "x = 2 * (x div 2)" by simp
+    with c1 show "P" .
+  next
+    case False
+    then have "x mod 2 = 1" by simp
+    with divmod have "x = 2 * (x div 2) + 1" by simp
+    with c2 show "P" .
+  qed
+qed presburger+  \<comment> \<open>solve compatibility with presburger\<close>
+termination by lexicographic_order
+
+thm ev.simps
+thm ev.induct
+thm ev.cases
+
+
+subsection \<open>Mutual Recursion\<close>
+
+fun evn od :: "nat \<Rightarrow> bool"
+where
+  "evn 0 = True"
+| "od 0 = False"
+| "evn (Suc n) = od n"
+| "od (Suc n) = evn n"
+
+thm evn.simps
+thm od.simps
+
+thm evn_od.induct
+thm evn_od.termination
+
+thm evn.elims
+thm od.elims
+
+
+subsection \<open>Definitions in local contexts\<close>
+
+locale my_monoid =
+  fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    and un :: "'a"
+  assumes assoc: "opr (opr x y) z = opr x (opr y z)"
+    and lunit: "opr un x = x"
+    and runit: "opr x un = x"
+begin
+
+fun foldR :: "'a list \<Rightarrow> 'a"
+where
+  "foldR [] = un"
+| "foldR (x # xs) = opr x (foldR xs)"
+
+fun foldL :: "'a list \<Rightarrow> 'a"
+where
+  "foldL [] = un"
+| "foldL [x] = x"
+| "foldL (x # y # ys) = foldL (opr x y # ys)"
+
+thm foldL.simps
+
+lemma foldR_foldL: "foldR xs = foldL xs"
+  by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
+
+thm foldR_foldL
+
+end
+
+thm my_monoid.foldL.simps
+thm my_monoid.foldR_foldL
+
+
+subsection \<open>\<open>fun_cases\<close>\<close>
+
+subsubsection \<open>Predecessor\<close>
+
+fun pred :: "nat \<Rightarrow> nat"
+where
+  "pred 0 = 0"
+| "pred (Suc n) = n"
+
+thm pred.elims
+
+lemma
+  assumes "pred x = y"
+  obtains "x = 0" "y = 0" | "n" where "x = Suc n" "y = n"
+  by (fact pred.elims[OF assms])
+
+
+text \<open>If the predecessor of a number is 0, that number must be 0 or 1.\<close>
+
+fun_cases pred0E[elim]: "pred n = 0"
+
+lemma "pred n = 0 \<Longrightarrow> n = 0 \<or> n = Suc 0"
+  by (erule pred0E) metis+
+
+text \<open>
+  Other expressions on the right-hand side also work, but whether the
+  generated rule is useful depends on how well the simplifier can
+  simplify it. This example works well:
+\<close>
+
+fun_cases pred42E[elim]: "pred n = 42"
+
+lemma "pred n = 42 \<Longrightarrow> n = 43"
+  by (erule pred42E)
+
+
+subsubsection \<open>List to option\<close>
+
+fun list_to_option :: "'a list \<Rightarrow> 'a option"
+where
+  "list_to_option [x] = Some x"
+| "list_to_option _ = None"
+
+fun_cases list_to_option_NoneE: "list_to_option xs = None"
+  and list_to_option_SomeE: "list_to_option xs = Some x"
+
+lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
+  by (erule list_to_option_SomeE)
+
+
+subsubsection \<open>Boolean Functions\<close>
+
+fun xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+where
+  "xor False False = False"
+| "xor True True = False"
+| "xor _ _ = True"
+
+thm xor.elims
+
+text \<open>
+  \<open>fun_cases\<close> does not only recognise function equations, but also works with
+  functions that return a boolean, e.g.:
+\<close>
+
+fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\<not>xor a b"
+print_theorems
+
+
+subsubsection \<open>Many parameters\<close>
+
+fun sum4 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "sum4 a b c d = a + b + c + d"
+
+fun_cases sum40E: "sum4 a b c d = 0"
+
+lemma "sum4 a b c d = 0 \<Longrightarrow> a = 0"
+  by (erule sum40E)
+
+
+subsection \<open>Partial Function Definitions\<close>
+
+text \<open>Partial functions in the option monad:\<close>
+
+partial_function (option)
+  collatz :: "nat \<Rightarrow> nat list option"
+where
+  "collatz n =
+    (if n \<le> 1 then Some [n]
+     else if even n
+       then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
+       else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
+
+declare collatz.simps[code]
+value "collatz 23"
+
+
+text \<open>Tail-recursive functions:\<close>
+
+partial_function (tailrec) fixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+  "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
+
+
+subsection \<open>Regression tests\<close>
+
+text \<open>
+  The following examples mainly serve as tests for the
+  function package.
+\<close>
+
+fun listlen :: "'a list \<Rightarrow> nat"
+where
+  "listlen [] = 0"
+| "listlen (x#xs) = Suc (listlen xs)"
+
+
+subsubsection \<open>Context recursion\<close>
+
+fun f :: "nat \<Rightarrow> nat"
+where
+  zero: "f 0 = 0"
+| succ: "f (Suc n) = (if f n = 0 then 0 else f n)"
+
+
+subsubsection \<open>A combination of context and nested recursion\<close>
+
+function h :: "nat \<Rightarrow> nat"
+where
+  "h 0 = 0"
+| "h (Suc n) = (if h n = 0 then h (h n) else h n)"
+by pat_completeness auto
+
+
+subsubsection \<open>Context, but no recursive call\<close>
+
+fun i :: "nat \<Rightarrow> nat"
+where
+  "i 0 = 0"
+| "i (Suc n) = (if n = 0 then 0 else i n)"
+
+
+subsubsection \<open>Tupled nested recursion\<close>
+
+fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "fa 0 y = 0"
+| "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)"
+
+
+subsubsection \<open>Let\<close>
+
+fun j :: "nat \<Rightarrow> nat"
+where
+  "j 0 = 0"
+| "j (Suc n) = (let u = n in Suc (j u))"
+
+
+text \<open>There were some problems with fresh names \dots\<close>
+function  k :: "nat \<Rightarrow> nat"
+where
+  "k x = (let a = x; b = x in k x)"
+  by pat_completeness auto
+
+
+function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "f2 p = (let (x,y) = p in f2 (y,x))"
+  by pat_completeness auto
+
+
+subsubsection \<open>Abbreviations\<close>
+
+fun f3 :: "'a set \<Rightarrow> bool"
+where
+  "f3 x = finite x"
+
+
+subsubsection \<open>Simple Higher-Order Recursion\<close>
+
+datatype 'a tree = Leaf 'a | Branch "'a tree list"
+
+fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+where
+  "treemap fn (Leaf n) = (Leaf (fn n))"
+| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
+
+fun tinc :: "nat tree \<Rightarrow> nat tree"
+where
+  "tinc (Leaf n) = Leaf (Suc n)"
+| "tinc (Branch l) = Branch (map tinc l)"
+
+fun testcase :: "'a tree \<Rightarrow> 'a list"
+where
+  "testcase (Leaf a) = [a]"
+| "testcase (Branch x) =
+    (let xs = concat (map testcase x);
+         ys = concat (map testcase x) in
+     xs @ ys)"
+
+
+subsubsection \<open>Pattern matching on records\<close>
+
+record point =
+  Xcoord :: int
+  Ycoord :: int
+
+function swp :: "point \<Rightarrow> point"
+where
+  "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
+proof -
+  fix P x
+  assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
+  then show P by (cases x)
+qed auto
+termination by rule auto
+
+
+subsubsection \<open>The diagonal function\<close>
+
+fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat"
+where
+  "diag x True False = 1"
+| "diag False y True = 2"
+| "diag True False z = 3"
+| "diag True True True = 4"
+| "diag False False False = 5"
+
+
+subsubsection \<open>Many equations (quadratic blowup)\<close>
+
+datatype DT =
+  A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
+| Q | R | S | T | U | V
+
+fun big :: "DT \<Rightarrow> nat"
+where
+  "big A = 0"
+| "big B = 0"
+| "big C = 0"
+| "big D = 0"
+| "big E = 0"
+| "big F = 0"
+| "big G = 0"
+| "big H = 0"
+| "big I = 0"
+| "big J = 0"
+| "big K = 0"
+| "big L = 0"
+| "big M = 0"
+| "big N = 0"
+| "big P = 0"
+| "big Q = 0"
+| "big R = 0"
+| "big S = 0"
+| "big T = 0"
+| "big U = 0"
+| "big V = 0"
+
+
+subsubsection \<open>Automatic pattern splitting\<close>
+
+fun f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+  "f4 0 0 = True"
+| "f4 _ _ = False"
+
+
+subsubsection \<open>Polymorphic partial-function\<close>
+
+partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
+where
+  "f5 x = f5 x"
+
+end
--- a/src/HOL/Library/Word.thy	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Library/Word.thy	Fri Sep 03 17:54:12 2021 +0200
@@ -3394,7 +3394,11 @@
   "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
-  by (transfer, simp)+
+              apply (simp_all add: word_uint_eq_iff unsigned_not_eq unsigned_and_eq unsigned_or_eq unsigned_xor_eq not_one_eq of_nat_take_bit ac_simps)
+       apply (simp_all add: minus_numeral_eq_not_sub_one)
+   apply (simp_all only: sub_one_eq_not_neg bit.xor_compl_right take_bit_xor bit.double_compl)
+   apply simp_all
+  done
 
 text \<open>Special cases for when one of the arguments equals -1.\<close>
 
@@ -3408,6 +3412,10 @@
   "x XOR (-1::'a::len word) = NOT x"
   by (transfer, simp)+
 
+lemma word_of_int_not_numeral_eq [simp]:
+  \<open>(word_of_int (NOT (numeral bin)) :: 'a::len word) = - numeral bin - 1\<close>
+  by transfer (simp add: not_eq_complement)
+
 lemma uint_and:
   \<open>uint (x AND y) = uint x AND uint y\<close>
   by transfer simp
--- a/src/HOL/Library/cconv.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Library/cconv.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -146,7 +146,8 @@
              val rule = abstract_rule_thm x
              val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
            in
-             (Drule.instantiate_normalize inst rule OF [Drule.generalize ([], [u]) eq])
+             (Drule.instantiate_normalize inst rule OF
+               [Drule.generalize (Symtab.empty, Symtab.make_set [u]) eq])
              |> Drule.zero_var_indexes
            end
 
--- a/src/HOL/Library/code_lazy.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -122,7 +122,7 @@
         |> Conjunction.intr_balanced
         |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
         |> Thm.implies_intr assum
-        |> Thm.generalize ([], params) 0
+        |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
         |> Axclass.unoverload ctxt
         |> Thm.varifyT_global
       end
@@ -494,7 +494,9 @@
     val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
       |> Drule.infer_instantiate' lthy10
          [SOME (Thm.cterm_of lthy10 (Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, HOLogic.unitT --> lazy_type)))]
-      |> Thm.generalize (map (fst o dest_TFree) type_args, []) (Variable.maxidx_of lthy10 + 1);
+      |> Thm.generalize
+         (Symtab.make_set (map (fst o dest_TFree) type_args), Symtab.empty)
+         (Variable.maxidx_of lthy10 + 1);
 
     val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms
     val ctr_thms_abs = map (fn thm => Drule.abs_def (thm RS @{thm eq_reflection})) ctrs_lazy_thms
--- a/src/HOL/ROOT	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/ROOT	Fri Sep 03 17:54:12 2021 +0200
@@ -28,6 +28,7 @@
     Coherent
     Commands
     Drinker
+    Functions
     Groebner_Examples
     Iff_Oracle
     Induction_Schema
@@ -665,7 +666,6 @@
     Eval_Examples
     Executable_Relation
     Execute_Choice
-    Functions
     Function_Growth
     Gauge_Integration
     Guess
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -82,7 +82,7 @@
 fun symbol (x : string, _ : Position.T) = x;
 
 fun explode_pos s pos = fst (fold_map (fn x => fn pos =>
-  ((x, pos), Position.advance x pos)) (raw_explode s) pos);
+  ((x, pos), Position.symbol x pos)) (raw_explode s) pos);
 
 
 (** scanners **)
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -101,6 +101,7 @@
   val tptp_empty_list : string
   val tptp_unary_builtins : string list
   val tptp_binary_builtins : string list
+  val tptp_ternary_builtins : string list
   val dfg_individual_type : string
   val isabelle_info_prefix : string
   val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
@@ -266,6 +267,7 @@
 val tptp_unary_builtins = [tptp_not]
 val tptp_binary_builtins =
   [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
+val tptp_ternary_builtins = [tptp_ite]
 
 val dfg_individual_type = "iii" (* cannot clash *)
 
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -567,34 +567,48 @@
 
 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort
    infomation. *)
-fun iterm_of_term thy type_enc bs (P $ Q) =
-    let
-      val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P
-      val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q
-    in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
-  | iterm_of_term thy type_enc _ (Const (c, T)) =
-    (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)),
-     atomic_types_of T)
-  | iterm_of_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T)
-  | iterm_of_term _ type_enc _ (Var (v as (s, _), T)) =
-    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
-       let
-         val Ts = T |> strip_type |> swap |> op ::
-         val s' = new_skolem_const_name s (length Ts)
-       in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
-     else
-       IVar ((make_schematic_var v, s), T), atomic_types_of T)
-  | iterm_of_term _ _ bs (Bound j) =
-    nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
-  | iterm_of_term thy type_enc bs (Abs (s, T, t)) =
-    let
-      fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
-      val s = vary s
-      val name = `make_bound_var s
-      val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t
-    in
-      (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T))
-    end
+fun iterm_of_term thy type_enc =
+  let
+    fun iot true bs ((t0 as Const (\<^const_name>\<open>Let\<close>, _)) $ t1 $ (t2 as Abs (s, T, t'))) =
+        let
+          val (t0', t0_atomics_Ts) = iot true bs t0
+          val (t1', t1_atomics_Ts) = iot true bs t1
+          val (t2', t2_atomics_Ts) = iot true bs t2
+        in
+          (IApp (IApp (t0', t1'), t2'),
+           fold (union (op =)) [t0_atomics_Ts, t1_atomics_Ts, t2_atomics_Ts] [])
+        end
+      | iot true bs ((t0 as Const (\<^const_name>\<open>Let\<close>, _)) $ t1 $ t2) =
+        iot true bs (t0 $ t1 $ eta_expand (map (snd o snd) bs) t2 1)
+      | iot fool bs (P $ Q) =
+        let
+          val (P', P_atomics_Ts) = iot fool bs P
+          val (Q', Q_atomics_Ts) = iot fool bs Q
+        in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
+      | iot _ _ (Const (c, T)) =
+        (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)),
+         atomic_types_of T)
+      | iot _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T)
+      | iot _ _ (Var (v as (s, _), T)) =
+        (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
+           let
+             val Ts = T |> strip_type |> swap |> op ::
+             val s' = new_skolem_const_name s (length Ts)
+           in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
+         else
+           IVar ((make_schematic_var v, s), T), atomic_types_of T)
+      | iot _ bs (Bound j) =
+        nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
+      | iot fool bs (Abs (s, T, t)) =
+        let
+          fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
+          val s = vary s
+          val name = `make_bound_var s
+          val (tm, atomic_Ts) = iot fool ((s, (name, T)) :: bs) t
+        in
+          (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T))
+        end
+  in iot (is_type_enc_fool type_enc)  end
 
 (* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
 val queries = ["?", "_query"]
@@ -745,8 +759,8 @@
     is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
   | _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
 
-fun simple_translate_lambdas do_lambdas ctxt type_enc t =
-  if is_first_order_lambda_free t then
+fun simple_translate_lambdas eta_matters do_lambdas ctxt type_enc t =
+  if not eta_matters andalso is_first_order_lambda_free t then
     t
   else
     let
@@ -791,9 +805,11 @@
         | Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts
         | _ => t)
 
-      val trans = if is_type_enc_fool type_enc then trans_fool else trans_first_order
-      val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt
-    in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
+      val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
+    in
+      t' |> (if is_type_enc_fool type_enc then trans_fool else trans_first_order) []
+         |> singleton (Variable.export_terms ctxt' ctxt)
+    end
 
 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
     do_cheaply_conceal_lambdas Ts t1
@@ -819,7 +835,8 @@
      |> reveal_bounds Ts)
   (* A type variable of sort "{}" will make abstraction fail. *)
   handle THM _ => t |> do_cheaply_conceal_lambdas Ts
-val introduce_combinators = simple_translate_lambdas do_introduce_combinators
+
+val introduce_combinators = simple_translate_lambdas false do_introduce_combinators
 
 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
   | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
@@ -827,28 +844,32 @@
     (if String.isPrefix lam_lifted_prefix s then Const else Free) x
   | constify_lifted t = t
 
+fun is_binder true (Const (\<^const_name>\<open>Let\<close>, _) $ _) = true
+  | is_binder _ t = Lambda_Lifting.is_quantifier t
+
 fun lift_lams_part_1 ctxt type_enc =
   map hol_close_form #> rpair ctxt
-  #-> Lambda_Lifting.lift_lambdas
-          (SOME ((if is_type_enc_polymorphic type_enc then
-                    lam_lifted_poly_prefix
-                  else
-                    lam_lifted_mono_prefix) ^ "_a"))
-          Lambda_Lifting.is_quantifier
+  #-> Lambda_Lifting.lift_lambdas (SOME
+    ((if is_type_enc_polymorphic type_enc then lam_lifted_poly_prefix
+      else lam_lifted_mono_prefix) ^ "_a"))
+    (is_binder (is_type_enc_fool type_enc))
   #> fst
 
 fun lift_lams_part_2 ctxt type_enc (facts, lifted) =
   (facts, lifted)
-  (* Lambda-lifting sometimes leaves some lambdas around; we need some way to
-     get rid of them *)
+  (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid of them *)
   |> apply2 (map (introduce_combinators ctxt type_enc))
   |> apply2 (map constify_lifted)
-  (* Requires bound variables not to clash with any schematic variables (as
-     should be the case right after lambda-lifting). *)
+  (* Requires bound variables not to clash with any schematic variables (as should be the case right
+     after lambda-lifting). *)
   |>> map (hol_open_form (unprefix hol_close_form_prefix))
   ||> map (hol_open_form I)
 
-fun lift_lams ctxt type_enc = lift_lams_part_2 ctxt type_enc o lift_lams_part_1 ctxt type_enc
+fun lift_lams ctxt type_enc =
+  (is_type_enc_fool type_enc ?
+   map (simple_translate_lambdas true (fn _ => fn _ => fn t => t) ctxt type_enc))
+  #> lift_lams_part_1 ctxt type_enc
+  #> lift_lams_part_2 ctxt type_enc
 
 fun intentionalize_def (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) =
     intentionalize_def t
@@ -1186,12 +1207,7 @@
           val tm2' = intro false [] tm2
           val tm2'' =
             (case tm1' of
-              IApp (IConst ((s, _), _, _), _) =>
-              if s = tptp_let then
-                eta_expand_quantifier_body tm2'
-              else
-                tm2'
-            | IConst ((s, _), _, _) =>
+              IConst ((s, _), _, _) =>
               if s = tptp_ho_forall orelse s = tptp_ho_exists then
                 eta_expand_quantifier_body tm2'
               else
@@ -1379,9 +1395,10 @@
 
 fun presimp_prop simp_options ctxt type_enc t =
   let
-    val t = t |> Envir.beta_eta_contract
-              |> transform_elim_prop
-              |> Object_Logic.atomize_term ctxt
+    val t =
+      t |> Envir.beta_eta_contract
+        |> transform_elim_prop
+        |> Object_Logic.atomize_term ctxt
     val need_trueprop = (fastype_of t = \<^typ>\<open>bool\<close>)
     val is_ho = is_type_enc_full_higher_order type_enc
   in
@@ -1528,7 +1545,8 @@
     (make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
     (map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @
     (map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @
-    (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins))
+    (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins)) @
+    (map (rpair (mk_sym_info true 3)) tptp_ternary_builtins)
     |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
       ? cons (prefixed_predicator_name, mk_sym_info true 1)
   end
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -157,32 +157,31 @@
 fun from_lemmas [] = ""
   | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
 
-fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable"
-  | string_of_atp_failure Unprovable = "The generated problem is unprovable"
-  | string_of_atp_failure GaveUp = "The prover gave up"
+fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable"
+  | string_of_atp_failure Unprovable = "Unprovable problem"
+  | string_of_atp_failure GaveUp = "Gave up"
   | string_of_atp_failure ProofMissing =
-    "The prover claims the conjecture is a theorem but did not provide a proof"
+    "Claims the conjecture is a theorem but did not provide a proof"
   | string_of_atp_failure ProofIncomplete =
-    "The prover claims the conjecture is a theorem but provided an incomplete proof"
+    "Claims the conjecture is a theorem but provided an incomplete proof"
   | string_of_atp_failure ProofUnparsable =
-    "The prover claims the conjecture is a theorem but provided an unparsable proof"
+    "Claims the conjecture is a theorem but provided an unparsable proof"
   | string_of_atp_failure (UnsoundProof (false, ss)) =
-    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
-    "; specify a sound type encoding or omit the \"type_enc\" option"
+    "Derived the lemma \"False\"" ^ from_lemmas ss ^
+    ", probably due to the use of an unsound type encoding"
   | string_of_atp_failure (UnsoundProof (true, ss)) =
-    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
+    "Derived the lemma \"False\"" ^ from_lemmas ss ^
     ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
   | string_of_atp_failure TimedOut = "Timed out"
-  | string_of_atp_failure Inappropriate =
-    "The generated problem lies outside the prover's scope"
-  | string_of_atp_failure OutOfResources = "The prover ran out of resources"
-  | string_of_atp_failure MalformedInput = "The generated problem is malformed"
-  | string_of_atp_failure MalformedOutput = "The prover output is malformed"
-  | string_of_atp_failure Interrupted = "The prover was interrupted"
-  | string_of_atp_failure Crashed = "The prover crashed"
-  | string_of_atp_failure InternalError = "An internal prover error occurred"
+  | string_of_atp_failure Inappropriate = "Problem outside the prover's scope"
+  | string_of_atp_failure OutOfResources = "Ran out of resources"
+  | string_of_atp_failure MalformedInput = "Malformed problem"
+  | string_of_atp_failure MalformedOutput = "Malformed output"
+  | string_of_atp_failure Interrupted = "Interrupted"
+  | string_of_atp_failure Crashed = "Crashed"
+  | string_of_atp_failure InternalError = "Internal prover error"
   | string_of_atp_failure (UnknownError s) =
-    "A prover error occurred" ^
+    "Prover error" ^
     (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s)
 
 fun extract_delimited (begin_delim, end_delim) output =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -852,7 +852,7 @@
                 |> unfold_thms lthy [dtor_ctor];
             in
               (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
-              |> Drule.generalize ([], [y_s])
+              |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s])
             end;
 
         val map_thms =
@@ -931,7 +931,7 @@
               |> infer_instantiate' lthy (replicate live NONE @
                 [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
               |> unfold_thms lthy [dtor_ctor]
-              |> Drule.generalize ([], [y_s, z_s])
+              |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s, z_s])
             end;
 
         val rel_inject_thms =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -160,7 +160,7 @@
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
     in
       Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
-      |> Drule.generalize ([], [s])
+      |> Drule.generalize (Symtab.empty, Symtab.make_set [s])
     end
   | _ => split);
 
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -42,7 +42,7 @@
     |> Conjunction.intr_balanced
     |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
     |> Thm.implies_intr assum
-    |> Thm.generalize ([], params) 0
+    |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
     |> Axclass.unoverload ctxt
     |> Thm.varifyT_global
   end;
--- a/src/HOL/Tools/Function/induction_schema.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -381,7 +381,7 @@
 
     val res = Conjunction.intr_balanced (map_index project branches)
       |> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps)
-      |> Drule.generalize ([], [Rn])
+      |> Drule.generalize (Symtab.empty, Symtab.make_set [Rn])
 
     val nbranches = length branches
     val npres = length pres
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -171,7 +171,7 @@
 fun by_tac ctxt thms ns ts t tac =
   Goal.prove ctxt [] (map as_prop ts) (as_prop t)
     (fn {context, prems} => HEADGOAL (tac context prems))
-  |> Drule.generalize ([], ns)
+  |> Drule.generalize (Symtab.empty, Symtab.make_set ns)
   |> discharge 1 thms
 
 fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -550,20 +550,22 @@
 
 val zipperposition_config : atp_config =
   let
-    val format = THF (With_FOOL, Polymorphic, THF_Without_Choice)
+    val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
        ["--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
         |> extra_options <> "" ? prefix (extra_options ^ " ")],
      proof_delims = tstp_proof_delims,
-     known_failures = known_szs_status_failures,
+     known_failures =
+       [(TimedOut, "SZS status ResourceOut")] @   (* odd way of timing out *)
+       known_szs_status_failures,
      prem_role = Hypothesis,
      best_slices = fn _ =>
        (* FUDGE *)
-       [(0.333, (((128, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_blsimp)),
-        (0.333, (((32, "meshN"), format, "poly_native_higher_fool", keep_lamsN, false), zipperposition_s6)),
-        (0.334, (((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_cdots))],
+       [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
+        (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
+        (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
      best_max_mono_iters = default_max_mono_iters,
      best_max_new_mono_instances = default_max_new_mono_instances}
   end
--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -575,7 +575,7 @@
       ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   in
     thm
-    |> Thm.generalize (tfrees, rnames @ frees) idx
+    |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
     |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
@@ -596,7 +596,7 @@
       ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   in
     thm
-    |> Thm.generalize (tfrees, rnames @ frees) idx
+    |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
     |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
@@ -718,7 +718,8 @@
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
-    |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, [])
+    |> Drule.generalize
+        (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
     |> Drule.zero_var_indexes
   end
 (*
@@ -753,7 +754,8 @@
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
-    |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, [])
+    |> Drule.generalize
+        (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
     |> Drule.zero_var_indexes
   end
 
--- a/src/HOL/ex/Functions.thy	Tue Aug 17 17:09:20 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,519 +0,0 @@
-(*  Title:      HOL/ex/Functions.thy
-    Author:     Alexander Krauss, TU Muenchen
-*)
-
-section \<open>Examples of function definitions\<close>
-
-theory Functions
-imports Main "HOL-Library.Monad_Syntax"
-begin
-
-subsection \<open>Very basic\<close>
-
-fun fib :: "nat \<Rightarrow> nat"
-where
-  "fib 0 = 1"
-| "fib (Suc 0) = 1"
-| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-
-text \<open>Partial simp and induction rules:\<close>
-thm fib.psimps
-thm fib.pinduct
-
-text \<open>There is also a cases rule to distinguish cases along the definition:\<close>
-thm fib.cases
-
-
-text \<open>Total simp and induction rules:\<close>
-thm fib.simps
-thm fib.induct
-
-text \<open>Elimination rules:\<close>
-thm fib.elims
-
-
-subsection \<open>Currying\<close>
-
-fun add
-where
-  "add 0 y = y"
-| "add (Suc x) y = Suc (add x y)"
-
-thm add.simps
-thm add.induct  \<comment> \<open>Note the curried induction predicate\<close>
-
-
-subsection \<open>Nested recursion\<close>
-
-function nz
-where
-  "nz 0 = 0"
-| "nz (Suc x) = nz (nz x)"
-by pat_completeness auto
-
-lemma nz_is_zero:  \<comment> \<open>A lemma we need to prove termination\<close>
-  assumes trm: "nz_dom x"
-  shows "nz x = 0"
-using trm
-by induct (auto simp: nz.psimps)
-
-termination nz
-  by (relation "less_than") (auto simp:nz_is_zero)
-
-thm nz.simps
-thm nz.induct
-
-
-subsubsection \<open>Here comes McCarthy's 91-function\<close>
-
-function f91 :: "nat \<Rightarrow> nat"
-where
-  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
-by pat_completeness auto
-
-text \<open>Prove a lemma before attempting a termination proof:\<close>
-lemma f91_estimate:
-  assumes trm: "f91_dom n"
-  shows "n < f91 n + 11"
-using trm by induct (auto simp: f91.psimps)
-
-termination
-proof
-  let ?R = "measure (\<lambda>x. 101 - x)"
-  show "wf ?R" ..
-
-  fix n :: nat
-  assume "\<not> 100 < n"  \<comment> \<open>Inner call\<close>
-  then show "(n + 11, n) \<in> ?R" by simp
-
-  assume inner_trm: "f91_dom (n + 11)"  \<comment> \<open>Outer call\<close>
-  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
-  with \<open>\<not> 100 < n\<close> show "(f91 (n + 11), n) \<in> ?R" by simp
-qed
-
-text \<open>Now trivial (even though it does not belong here):\<close>
-lemma "f91 n = (if 100 < n then n - 10 else 91)"
-  by (induct n rule: f91.induct) auto
-
-
-subsubsection \<open>Here comes Takeuchi's function\<close>
-
-definition tak_m1 where "tak_m1 = (\<lambda>(x,y,z). if x \<le> y then 0 else 1)"
-definition tak_m2 where "tak_m2 = (\<lambda>(x,y,z). nat (Max {x, y, z} - Min {x, y, z}))"
-definition tak_m3 where "tak_m3 = (\<lambda>(x,y,z). nat (x - Min {x, y, z}))"
-
-function tak :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
-  "tak x y z = (if x \<le> y then y else tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y))"
-  by auto
-
-lemma tak_pcorrect:
-  "tak_dom (x, y, z) \<Longrightarrow> tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
-  by (induction x y z rule: tak.pinduct) (auto simp: tak.psimps)
-
-termination
-  by (relation "tak_m1 <*mlex*> tak_m2 <*mlex*> tak_m3 <*mlex*> {}")
-     (auto simp: mlex_iff wf_mlex tak_pcorrect tak_m1_def tak_m2_def tak_m3_def min_def max_def)
-
-theorem tak_correct: "tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
-  by (induction x y z rule: tak.induct) auto
-
-
-subsection \<open>More general patterns\<close>
-
-subsubsection \<open>Overlapping patterns\<close>
-
-text \<open>
-  Currently, patterns must always be compatible with each other, since
-  no automatic splitting takes place. But the following definition of
-  GCD is OK, although patterns overlap:
-\<close>
-
-fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
-  "gcd2 x 0 = x"
-| "gcd2 0 y = y"
-| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
-                                    else gcd2 (x - y) (Suc y))"
-
-thm gcd2.simps
-thm gcd2.induct
-
-
-subsubsection \<open>Guards\<close>
-
-text \<open>We can reformulate the above example using guarded patterns:\<close>
-
-function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
-  "gcd3 x 0 = x"
-| "gcd3 0 y = y"
-| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
-| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y"
-  apply (case_tac x, case_tac a, auto)
-  apply (case_tac ba, auto)
-  done
-termination by lexicographic_order
-
-thm gcd3.simps
-thm gcd3.induct
-
-
-text \<open>General patterns allow even strange definitions:\<close>
-
-function ev :: "nat \<Rightarrow> bool"
-where
-  "ev (2 * n) = True"
-| "ev (2 * n + 1) = False"
-proof -  \<comment> \<open>completeness is more difficult here \dots\<close>
-  fix P :: bool
-  fix x :: nat
-  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
-    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
-  have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
-  show P
-  proof (cases "x mod 2 = 0")
-    case True
-    with divmod have "x = 2 * (x div 2)" by simp
-    with c1 show "P" .
-  next
-    case False
-    then have "x mod 2 = 1" by simp
-    with divmod have "x = 2 * (x div 2) + 1" by simp
-    with c2 show "P" .
-  qed
-qed presburger+  \<comment> \<open>solve compatibility with presburger\<close>
-termination by lexicographic_order
-
-thm ev.simps
-thm ev.induct
-thm ev.cases
-
-
-subsection \<open>Mutual Recursion\<close>
-
-fun evn od :: "nat \<Rightarrow> bool"
-where
-  "evn 0 = True"
-| "od 0 = False"
-| "evn (Suc n) = od n"
-| "od (Suc n) = evn n"
-
-thm evn.simps
-thm od.simps
-
-thm evn_od.induct
-thm evn_od.termination
-
-thm evn.elims
-thm od.elims
-
-
-subsection \<open>Definitions in local contexts\<close>
-
-locale my_monoid =
-  fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-    and un :: "'a"
-  assumes assoc: "opr (opr x y) z = opr x (opr y z)"
-    and lunit: "opr un x = x"
-    and runit: "opr x un = x"
-begin
-
-fun foldR :: "'a list \<Rightarrow> 'a"
-where
-  "foldR [] = un"
-| "foldR (x # xs) = opr x (foldR xs)"
-
-fun foldL :: "'a list \<Rightarrow> 'a"
-where
-  "foldL [] = un"
-| "foldL [x] = x"
-| "foldL (x # y # ys) = foldL (opr x y # ys)"
-
-thm foldL.simps
-
-lemma foldR_foldL: "foldR xs = foldL xs"
-  by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
-
-thm foldR_foldL
-
-end
-
-thm my_monoid.foldL.simps
-thm my_monoid.foldR_foldL
-
-
-subsection \<open>\<open>fun_cases\<close>\<close>
-
-subsubsection \<open>Predecessor\<close>
-
-fun pred :: "nat \<Rightarrow> nat"
-where
-  "pred 0 = 0"
-| "pred (Suc n) = n"
-
-thm pred.elims
-
-lemma
-  assumes "pred x = y"
-  obtains "x = 0" "y = 0" | "n" where "x = Suc n" "y = n"
-  by (fact pred.elims[OF assms])
-
-
-text \<open>If the predecessor of a number is 0, that number must be 0 or 1.\<close>
-
-fun_cases pred0E[elim]: "pred n = 0"
-
-lemma "pred n = 0 \<Longrightarrow> n = 0 \<or> n = Suc 0"
-  by (erule pred0E) metis+
-
-text \<open>
-  Other expressions on the right-hand side also work, but whether the
-  generated rule is useful depends on how well the simplifier can
-  simplify it. This example works well:
-\<close>
-
-fun_cases pred42E[elim]: "pred n = 42"
-
-lemma "pred n = 42 \<Longrightarrow> n = 43"
-  by (erule pred42E)
-
-
-subsubsection \<open>List to option\<close>
-
-fun list_to_option :: "'a list \<Rightarrow> 'a option"
-where
-  "list_to_option [x] = Some x"
-| "list_to_option _ = None"
-
-fun_cases list_to_option_NoneE: "list_to_option xs = None"
-  and list_to_option_SomeE: "list_to_option xs = Some x"
-
-lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
-  by (erule list_to_option_SomeE)
-
-
-subsubsection \<open>Boolean Functions\<close>
-
-fun xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
-where
-  "xor False False = False"
-| "xor True True = False"
-| "xor _ _ = True"
-
-thm xor.elims
-
-text \<open>
-  \<open>fun_cases\<close> does not only recognise function equations, but also works with
-  functions that return a boolean, e.g.:
-\<close>
-
-fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\<not>xor a b"
-print_theorems
-
-
-subsubsection \<open>Many parameters\<close>
-
-fun sum4 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  where "sum4 a b c d = a + b + c + d"
-
-fun_cases sum40E: "sum4 a b c d = 0"
-
-lemma "sum4 a b c d = 0 \<Longrightarrow> a = 0"
-  by (erule sum40E)
-
-
-subsection \<open>Partial Function Definitions\<close>
-
-text \<open>Partial functions in the option monad:\<close>
-
-partial_function (option)
-  collatz :: "nat \<Rightarrow> nat list option"
-where
-  "collatz n =
-    (if n \<le> 1 then Some [n]
-     else if even n
-       then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
-       else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
-
-declare collatz.simps[code]
-value "collatz 23"
-
-
-text \<open>Tail-recursive functions:\<close>
-
-partial_function (tailrec) fixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
-where
-  "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
-
-
-subsection \<open>Regression tests\<close>
-
-text \<open>
-  The following examples mainly serve as tests for the
-  function package.
-\<close>
-
-fun listlen :: "'a list \<Rightarrow> nat"
-where
-  "listlen [] = 0"
-| "listlen (x#xs) = Suc (listlen xs)"
-
-
-subsubsection \<open>Context recursion\<close>
-
-fun f :: "nat \<Rightarrow> nat"
-where
-  zero: "f 0 = 0"
-| succ: "f (Suc n) = (if f n = 0 then 0 else f n)"
-
-
-subsubsection \<open>A combination of context and nested recursion\<close>
-
-function h :: "nat \<Rightarrow> nat"
-where
-  "h 0 = 0"
-| "h (Suc n) = (if h n = 0 then h (h n) else h n)"
-by pat_completeness auto
-
-
-subsubsection \<open>Context, but no recursive call\<close>
-
-fun i :: "nat \<Rightarrow> nat"
-where
-  "i 0 = 0"
-| "i (Suc n) = (if n = 0 then 0 else i n)"
-
-
-subsubsection \<open>Tupled nested recursion\<close>
-
-fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
-  "fa 0 y = 0"
-| "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)"
-
-
-subsubsection \<open>Let\<close>
-
-fun j :: "nat \<Rightarrow> nat"
-where
-  "j 0 = 0"
-| "j (Suc n) = (let u = n in Suc (j u))"
-
-
-text \<open>There were some problems with fresh names \dots\<close>
-function  k :: "nat \<Rightarrow> nat"
-where
-  "k x = (let a = x; b = x in k x)"
-  by pat_completeness auto
-
-
-function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "f2 p = (let (x,y) = p in f2 (y,x))"
-  by pat_completeness auto
-
-
-subsubsection \<open>Abbreviations\<close>
-
-fun f3 :: "'a set \<Rightarrow> bool"
-where
-  "f3 x = finite x"
-
-
-subsubsection \<open>Simple Higher-Order Recursion\<close>
-
-datatype 'a tree = Leaf 'a | Branch "'a tree list"
-
-fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
-where
-  "treemap fn (Leaf n) = (Leaf (fn n))"
-| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
-
-fun tinc :: "nat tree \<Rightarrow> nat tree"
-where
-  "tinc (Leaf n) = Leaf (Suc n)"
-| "tinc (Branch l) = Branch (map tinc l)"
-
-fun testcase :: "'a tree \<Rightarrow> 'a list"
-where
-  "testcase (Leaf a) = [a]"
-| "testcase (Branch x) =
-    (let xs = concat (map testcase x);
-         ys = concat (map testcase x) in
-     xs @ ys)"
-
-
-subsubsection \<open>Pattern matching on records\<close>
-
-record point =
-  Xcoord :: int
-  Ycoord :: int
-
-function swp :: "point \<Rightarrow> point"
-where
-  "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
-proof -
-  fix P x
-  assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
-  then show P by (cases x)
-qed auto
-termination by rule auto
-
-
-subsubsection \<open>The diagonal function\<close>
-
-fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat"
-where
-  "diag x True False = 1"
-| "diag False y True = 2"
-| "diag True False z = 3"
-| "diag True True True = 4"
-| "diag False False False = 5"
-
-
-subsubsection \<open>Many equations (quadratic blowup)\<close>
-
-datatype DT =
-  A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
-| Q | R | S | T | U | V
-
-fun big :: "DT \<Rightarrow> nat"
-where
-  "big A = 0"
-| "big B = 0"
-| "big C = 0"
-| "big D = 0"
-| "big E = 0"
-| "big F = 0"
-| "big G = 0"
-| "big H = 0"
-| "big I = 0"
-| "big J = 0"
-| "big K = 0"
-| "big L = 0"
-| "big M = 0"
-| "big N = 0"
-| "big P = 0"
-| "big Q = 0"
-| "big R = 0"
-| "big S = 0"
-| "big T = 0"
-| "big U = 0"
-| "big V = 0"
-
-
-subsubsection \<open>Automatic pattern splitting\<close>
-
-fun f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool"
-where
-  "f4 0 0 = True"
-| "f4 _ _ = False"
-
-
-subsubsection \<open>Polymorphic partial-function\<close>
-
-partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
-where
-  "f5 x = f5 x"
-
-end
--- a/src/Pure/Concurrent/future.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Concurrent/future.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -407,7 +407,7 @@
 
 fun error_message pos ((serial, msg), exec_id) =
   Position.setmp_thread_data pos (fn () =>
-    let val id = Position.get_id pos in
+    let val id = Position.id_of pos in
       if is_none id orelse is_none exec_id orelse id = exec_id
       then Output.error_message' (serial, msg) else ()
     end) ();
@@ -415,7 +415,7 @@
 fun identify_result pos res =
   res |> Exn.map_exn (fn exn =>
     let val exec_id =
-      (case Position.get_id pos of
+      (case Position.id_of pos of
         NONE => []
       | SOME id => [(Markup.exec_idN, id)])
     in Par_Exn.identify exec_id exn end);
--- a/src/Pure/General/name_space.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/General/name_space.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -112,7 +112,7 @@
   serial: serial};
 
 fun entry_markup def kind (name, {pos, serial, ...}: entry) =
-  Markup.properties (Position.entity_properties_of def serial pos) (Markup.entity kind name);
+  Position.make_entity_markup def serial kind (name, pos);
 
 fun print_entry_ref kind (name, entry) =
   quote (Markup.markup (entry_markup false kind (name, entry)) name);
--- a/src/Pure/General/position.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/General/position.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -1,7 +1,9 @@
 (*  Title:      Pure/General/position.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Source positions: counting Isabelle symbols, starting from 1.
+Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
+symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
+right-open interval offset .. end_offset (exclusive).
 *)
 
 signature POSITION =
@@ -14,8 +16,9 @@
   val offset_of: T -> int option
   val end_offset_of: T -> int option
   val file_of: T -> string option
-  val advance: Symbol.symbol -> T -> T
-  val advance_offsets: int -> T -> T
+  val id_of: T -> string option
+  val symbol: Symbol.symbol -> T -> T
+  val symbol_explode: string -> T -> T
   val distance_of: T * T -> int option
   val none: T
   val start: T
@@ -28,18 +31,18 @@
   val get_props: T -> Properties.T
   val id: string -> T
   val id_only: string -> T
-  val get_id: T -> string option
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
   val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
+  val advance_offsets: int -> T -> T
   val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
-  val entity_properties_of: bool -> serial -> T -> Properties.T
+  val make_entity_markup: bool -> serial -> string -> string * T -> Markup.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
@@ -73,7 +76,8 @@
 
 (* datatype position *)
 
-datatype T = Pos of (int * int * int) * Properties.T;
+type count = int * int * int;
+datatype T = Pos of count * Properties.T;
 
 fun dest2 f = apply2 (fn Pos p => f p);
 
@@ -92,37 +96,34 @@
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
 
 fun valid (i: int) = i > 0;
+val invalid = not o valid;
+fun maybe_valid i = if valid i then SOME i else NONE;
 fun if_valid i i' = if valid i then i' else i;
 
 
 (* fields *)
 
-fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
-fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
-fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
+fun line_of (Pos ((i, _, _), _)) = maybe_valid i;
+fun offset_of (Pos ((_, j, _), _)) = maybe_valid j;
+fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k;
 
 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
+fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
 
 
-(* advance *)
+(* count position *)
 
-fun advance_count "\n" (i: int, j: int, k: int) =
+fun count_symbol "\n" ((i, j, k): count) =
       (if_valid i (i + 1), if_valid j (j + 1), k)
-  | advance_count s (i, j, k) =
-      if Symbol.not_eof s then (i, if_valid j (j + 1), k)
-      else (i, j, k);
+  | count_symbol s (i, j, k) =
+      if Symbol.not_eof s then (i, if_valid j (j + 1), k) else (i, j, k);
 
-fun invalid_count (i, j, _: int) =
-  not (valid i orelse valid j);
-
-fun advance sym (pos as (Pos (count, props))) =
-  if invalid_count count then pos else Pos (advance_count sym count, props);
+fun count_invalid ((i, j, _): count) = invalid i andalso invalid j;
 
-fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
-  if offset = 0 orelse invalid_count count then pos
-  else if offset < 0 then raise Fail "Illegal offset"
-  else if valid i then raise Fail "Illegal line position"
-  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
+fun symbol sym (pos as (Pos (count, props))) =
+  if count_invalid count then pos else Pos (count_symbol sym count, props);
+
+val symbol_explode = fold symbol o Symbol.explode;
 
 
 (* distance of adjacent positions *)
@@ -152,17 +153,25 @@
 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 
-fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
-fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
+fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
-fun parse_id pos = Option.map Value.parse_int (get_id pos);
+fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
 fun id_properties_of pos =
-  (case get_id pos of
+  (case id_of pos of
     SOME id => [(Markup.idN, id)]
   | NONE => []);
 
+
+(* adjust offsets *)
+
+fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
+  if offset = 0 orelse count_invalid count then pos
+  else if offset < 0 then raise Fail "Illegal offset"
+  else if valid i then raise Fail "Illegal line position"
+  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
+
 fun adjust_offsets adjust (pos as Pos (_, props)) =
   if is_none (file_of pos) then
     (case parse_id pos of
@@ -178,40 +187,47 @@
 
 (* markup properties *)
 
-fun get props name =
+fun get_int props name =
   (case Properties.get props name of
     NONE => 0
   | SOME s => Value.parse_int s);
 
 fun of_properties props =
-  make {line = get props Markup.lineN,
-    offset = get props Markup.offsetN,
-    end_offset = get props Markup.end_offsetN,
+  make {
+    line = get_int props Markup.lineN,
+    offset = get_int props Markup.offsetN,
+    end_offset = get_int props Markup.end_offsetN,
     props = props};
 
-fun value k i = if valid i then [(k, Value.print_int i)] else [];
+fun int_entry k i = if invalid i then [] else [(k, Value.print_int i)];
 
 fun properties_of (Pos ((i, j, k), props)) =
-  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
+  int_entry Markup.lineN i @
+  int_entry Markup.offsetN j @
+  int_entry Markup.end_offsetN k @ props;
 
 fun offset_properties_of (Pos ((_, j, k), _)) =
-  value Markup.offsetN j @ value Markup.end_offsetN k;
+  int_entry Markup.offsetN j @
+  int_entry Markup.end_offsetN k;
 
-val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
+val def_properties_of = properties_of #> map (apfst Markup.def_name);
 
 fun entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos);
 
-fun entity_properties_of def serial pos =
-  if def then (Markup.defN, Value.print_int serial) :: properties_of pos
-  else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
+fun make_entity_markup def serial kind (name, pos) =
+  let
+    val props =
+      if def then (Markup.defN, Value.print_int serial) :: properties_of pos
+      else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
+  in Markup.entity kind name |> Markup.properties props end;
 
 val markup = Markup.properties o properties_of;
 
 
 (* reports *)
 
-fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
+fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos);
 fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
 
 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
@@ -271,14 +287,14 @@
   let
     val pos = of_properties props;
     val pos' =
-      make {line = get props Markup.end_lineN,
-        offset = get props Markup.end_offsetN,
+      make {line = get_int props Markup.end_lineN,
+        offset = get_int props Markup.end_offsetN,
         end_offset = 0,
         props = props};
   in (pos, pos') end;
 
 fun properties_of_range (pos, pos') =
-  properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
+  properties_of pos @ int_entry Markup.end_lineN (the_default 0 (line_of pos'));
 
 
 (* thread data *)
--- a/src/Pure/General/symbol_explode.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/General/symbol_explode.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -18,13 +18,12 @@
 fun explode string =
   let
     fun char i = String.sub (string, i);
-    fun string_range i j = String.substring (string, i, j - i);
+    fun substring i j = String.substring (string, i, j - i);
 
     val n = size string;
     fun test pred i = i < n andalso pred (char i);
     fun many pred i = if test pred i then many pred (i + 1) else i;
-    fun maybe pred i = if test pred i then i + 1 else i;
-    fun maybe_char c = maybe (fn c' => c = c');
+    fun maybe_char c i = if test (fn c' => c = c') i then i + 1 else i;
     fun maybe_ascii_id i = if test is_ascii_letter i then many is_ascii_letdig (i + 1) else i;
 
     fun scan i =
@@ -39,11 +38,11 @@
           (*utf8*)
           else if is_utf8 ch then
             let val j = many is_utf8_trailer (i + 1)
-            in string_range i j :: scan j end
+            in substring i j :: scan j end
           (*named symbol*)
           else if ch = #"\\" andalso test (fn c => c = #"<") (i + 1) then
             let val j = (i + 2) |> maybe_char #"^" |> maybe_ascii_id |> maybe_char #">"
-            in string_range i j :: scan j end
+            in substring i j :: scan j end
           (*single character*)
           else String.str ch :: scan (i + 1)
         end
--- a/src/Pure/General/symbol_pos.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/General/symbol_pos.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -40,7 +40,7 @@
   type text = string
   val implode: T list -> text
   val implode_range: Position.range -> T list -> text * Position.range
-  val explode_delete: text * Position.T -> T list * Position.T list
+  val explode_deleted: string * Position.T -> Position.T list
   val explode: text * Position.T -> T list
   val explode0: string -> T list
   val scan_ident: T list scanner
@@ -62,7 +62,7 @@
 val content = implode o map symbol;
 
 fun range (syms as (_, pos) :: _) =
-      let val pos' = List.last syms |-> Position.advance
+      let val pos' = List.last syms |-> Position.symbol
       in Position.range (pos, pos') end
   | range [] = Position.no_range;
 
@@ -75,7 +75,7 @@
 val is_eof = Symbol.is_eof o symbol;
 
 val stopper =
-  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance)) is_eof;
+  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.symbol)) is_eof;
 
 
 (* basic scanners *)
@@ -233,7 +233,7 @@
 
 fun source pos =
   Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos =>
-    Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos))))));
+    Scan.one Symbol.not_eof >> (fn s => (Position.symbol s pos, (s, pos))))));
 
 
 (* compact representation -- with Symbol.DEL padding *)
@@ -244,7 +244,7 @@
   | pad [(s, _)] = [s]
   | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
       let
-        val end_pos1 = Position.advance s1 pos1;
+        val end_pos1 = Position.symbol s1 pos1;
         val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
       in s1 :: replicate d Symbol.DEL @ pad rest end;
 
@@ -254,19 +254,25 @@
   let val syms' = (("", pos1) :: syms @ [("", pos2)])
   in (implode syms', range syms') end;
 
-fun explode_delete (str, pos) =
-  let
-    val (res, _) =
-      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
-        (Symbol.explode str) ([], Position.no_range_position pos);
-  in
-    fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p)))
-      res ([], [])
-  end;
+local
+
+fun rev_explode (str, pos) =
+  fold (fn s => fn (res, p) => ((s, p) :: res, Position.symbol s p))
+    (Symbol.explode str) ([], Position.no_range_position pos)
+  |> #1;
+
+in
 
-val explode = explode_delete #> #1;
+fun explode_deleted arg =
+  fold (fn (s, p) => s = Symbol.DEL ? cons p) (rev_explode arg) [];
+
+fun explode arg =
+  fold (fn (s, p) => s <> Symbol.DEL ? cons (s, p)) (rev_explode arg) [];
+
 fun explode0 str = explode (str, Position.none);
 
+end;
+
 
 (* identifiers *)
 
--- a/src/Pure/General/time.scala	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/General/time.scala	Fri Sep 03 17:54:12 2021 +0200
@@ -14,8 +14,8 @@
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
-  def minutes(s: Double): Time = new Time((s * 60000.0).round)
-  def ms(m: Long): Time = new Time(m)
+  def minutes(m: Double): Time = new Time((m * 60000.0).round)
+  def ms(ms: Long): Time = new Time(ms)
   def hms(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h)
 
   def now(): Time = ms(System.currentTimeMillis())
--- a/src/Pure/General/timing.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/General/timing.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/timing.ML
     Author:     Makarius
 
-Basic support for time measurement.
+Support for time measurement.
 *)
 
 signature BASIC_TIMING =
--- a/src/Pure/Isar/attrib.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -602,6 +602,7 @@
   register_config_bool Thm.show_consts #>
   register_config_bool Thm.show_hyps #>
   register_config_bool Thm.show_tags #>
+  register_config_bool Proof_Display.show_results #>
   register_config_bool Pattern.unify_trace_failure #>
   register_config_int Unify.trace_bound #>
   register_config_int Unify.search_bound #>
--- a/src/Pure/Isar/calculation.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -68,8 +68,7 @@
     fun report def serial pos =
       Context_Position.report (Proof.context_of state)
         (Position.thread_data ())
-          (Markup.entity calculationN ""
-            |> Markup.properties (Position.entity_properties_of def serial pos));
+        (Position.make_entity_markup def serial calculationN ("", pos));
     val calculation =
       (case calc of
         NONE => NONE
--- a/src/Pure/Isar/keyword.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Isar/keyword.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -216,8 +216,7 @@
 fun command_markup keywords name =
   lookup_command keywords name
   |> Option.map (fn {pos, id, ...} =>
-      Markup.properties (Position.entity_properties_of false id pos)
-        (Markup.entity Markup.command_keywordN name));
+      Position.make_entity_markup false id Markup.command_keywordN (name, pos));
 
 fun command_kind keywords = Option.map #kind o lookup_command keywords;
 
--- a/src/Pure/Isar/local_defs.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Isar/local_defs.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -89,7 +89,8 @@
 *)
 fun expand defs =
   Drule.implies_intr_list defs
-  #> Drule.generalize ([], map (#1 o head_of_def o Thm.term_of) defs)
+  #> Drule.generalize
+      (Symtab.empty, fold (Symtab.insert_set o #1 o head_of_def o Thm.term_of) defs Symtab.empty)
   #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
 val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
--- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -65,8 +65,7 @@
 fun command_pos (Command {pos, ...}) = pos;
 
 fun command_markup def (name, Command {pos, id, ...}) =
-  Markup.properties (Position.entity_properties_of def id pos)
-    (Markup.entity Markup.commandN name);
+  Position.make_entity_markup def id Markup.commandN (name, pos);
 
 fun pretty_command (cmd as (name, Command {comment, ...})) =
   Pretty.block
--- a/src/Pure/Isar/proof_display.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -22,6 +22,7 @@
   val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
+  val show_results: bool Config.T
   val print_results: bool -> Position.T -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Position.T -> Proof.context ->
@@ -263,6 +264,14 @@
 
 fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
 
+val interactive =
+  Config.declare_bool ("interactive", \<^here>) (K false);
+
+val show_results =
+  Config.declare_bool ("show_results", \<^here>) (fn context => Config.get_generic context interactive);
+
+fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);
+
 local
 
 fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
@@ -276,8 +285,8 @@
 
 in
 
-fun print_results do_print pos ctxt ((kind, name), facts) =
-  if not do_print orelse kind = "" then ()
+fun print_results int pos ctxt ((kind, name), facts) =
+  if kind = "" orelse no_print int ctxt then ()
   else if name = "" then
     (Output.state o Pretty.string_of)
       (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
@@ -315,8 +324,8 @@
 
 in
 
-fun print_consts do_print pos ctxt pred cs =
-  if not do_print orelse null cs then ()
+fun print_consts int pos ctxt pred cs =
+  if null cs orelse no_print int ctxt then ()
   else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
 
 end;
--- a/src/Pure/Isar/token.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Isar/token.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -338,8 +338,8 @@
     let
       val pos = pos_of tok;
       val (m, text) = token_kind_markup (kind_of tok);
-      val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos));
-    in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end;
+      val deleted = Symbol_Pos.explode_deleted (source_of tok, pos);
+    in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) deleted end;
 
 fun markups keywords = map (#2 o #1) o reports keywords;
 
@@ -381,7 +381,7 @@
 fun file_source (file: file) =
   let
     val text = cat_lines (#lines file);
-    val end_pos = fold Position.advance (Symbol.explode text) (#pos file);
+    val end_pos = Position.symbol_explode text (#pos file);
   in Input.source true text (Position.range (#pos file, end_pos)) end;
 
 fun get_files (Token (_, _, Value (SOME (Files files)))) = files
--- a/src/Pure/ML/ml_antiquotations2.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations2.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -9,12 +9,11 @@
 
 val _ = Theory.setup
  (ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
-      ML_Syntax.print_string (Method.check_name ctxt (name, pos)))) #>
+    (Args.context -- Scan.lift Args.embedded_position >>
+      (ML_Syntax.print_string o uncurry Method.check_name)) #>
 
   ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
-   (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
-      Locale.check (Proof_Context.theory_of ctxt) (name, pos)
-      |> ML_Syntax.print_string)));
+   (Args.theory -- Scan.lift Args.embedded_position >>
+      (ML_Syntax.print_string o uncurry Locale.check)));
 
 end;
--- a/src/Pure/ML/ml_lex.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -333,8 +333,8 @@
       if null syms then []
       else
         let
-          val pos1 = List.last syms |-> Position.advance;
-          val pos2 = Position.advance Symbol.space pos1;
+          val pos1 = List.last syms |-> Position.symbol;
+          val pos2 = Position.symbol Symbol.space pos1;
         in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
 
     fun check (Antiquote.Text tok) =
--- a/src/Pure/PIDE/command.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -95,7 +95,7 @@
   let
     val file_pos =
       Position.file file_node |>
-      (case Position.get_id (Position.thread_data ()) of
+      (case Position.id_of (Position.thread_data ()) of
         NONE => I
       | SOME exec_id => Position.put_id exec_id);
   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
--- a/src/Pure/PIDE/document.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -132,7 +132,7 @@
       if null errors then ()
       else
         cat_lines errors |>
-        (case Position.get_id (Position.thread_data ()) of
+        (case Position.id_of (Position.thread_data ()) of
           NONE => I
         | SOME id => Protocol_Message.command_positions_yxml id)
         |> error;
--- a/src/Pure/PIDE/markup.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -60,9 +60,10 @@
   val end_offsetN: string
   val fileN: string
   val idN: string
+  val positionN: string val position: T
   val position_properties: string list
   val position_property: Properties.entry -> bool
-  val positionN: string val position: T
+  val def_name: string -> string
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
@@ -394,10 +395,22 @@
 val fileN = "file";
 val idN = "id";
 
+val (positionN, position) = markup_elem "position";
+
 val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
-val (positionN, position) = markup_elem "position";
+
+(* position "def" names *)
+
+fun make_def a = "def_" ^ a;
+
+val def_names = Symtab.make (map (fn a => (a, make_def a)) position_properties);
+
+fun def_name a =
+  (case Symtab.lookup def_names a of
+    SOME b => b
+  | NONE => make_def a);
 
 
 (* expression *)
--- a/src/Pure/PIDE/markup.scala	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Sep 03 17:54:12 2021 +0200
@@ -159,10 +159,19 @@
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
+  val POSITION = "position"
+
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
-  val POSITION = "position"
+
+  /* position "def" name */
+
+  private val def_names: Map[String, String] =
+    Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET,
+      FILE -> DEF_FILE, ID -> DEF_ID)
+
+  def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
 
 
   /* expression */
--- a/src/Pure/PIDE/resources.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -168,8 +168,7 @@
 fun check_session ctxt arg =
   Completion.check_item "session"
     (fn (name, {pos, serial}) =>
-      Markup.entity Markup.sessionN name
-      |> Markup.properties (Position.entity_properties_of false serial pos))
+      Position.make_entity_markup false serial Markup.sessionN (name, pos))
     (get_session_base1 #session_positions) ctxt arg;
 
 fun session_chapter name =
--- a/src/Pure/Pure.thy	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Pure.thy	Fri Sep 03 17:54:12 2021 +0200
@@ -134,7 +134,7 @@
             val _ =
               (lines, pos0) |-> fold (fn line => fn pos1 =>
                 let
-                  val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
+                  val pos2 = Position.symbol_explode line pos1;
                   val range = Position.range (pos1, pos2);
                   val source = Input.source true line range;
                   val _ =
@@ -144,7 +144,7 @@
                     else
                       (ignore (Resources.check_session_dir ctxt (SOME dir) source)
                         handle ERROR msg => Output.error_message msg);
-                in pos2 |> Position.advance "\n" end);
+                in pos2 |> Position.symbol "\n" end);
           in thy' end)));
 
   val _ =
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -60,10 +60,7 @@
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 
 fun markup_bound def ps (name, id) =
-  let val entity = Markup.entity Markup.boundN name in
-    Markup.bound ::
-      map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
-  end;
+  Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity ctxt c =
   (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
@@ -84,7 +81,7 @@
   | reports_of_scope (def_pos :: ps) =
       let
         val id = serial ();
-        fun entity def = (Markup.entityN, Position.entity_properties_of def id def_pos);
+        fun entity def = Position.make_entity_markup def id "" ("", def_pos);
       in
         map (rpair Markup.bound) (def_pos :: ps) @
         ((def_pos, entity true) :: map (rpair (entity false)) ps)
--- a/src/Pure/System/bash.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/System/bash.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/System/bash.ML
     Author:     Makarius
 
-Syntax for GNU bash.
+Support for GNU bash.
 *)
 
 signature BASH =
@@ -19,6 +19,12 @@
   val redirect: params -> params
   val timeout: Time.time -> params -> params
   val description: string -> params -> params
+  val server_run: string
+  val server_kill: string
+  val server_uuid: string
+  val server_interrupt: string
+  val server_failure: string
+  val server_result: string
 end;
 
 structure Bash: BASH =
@@ -91,4 +97,15 @@
 
 end;
 
+
+(* server messages *)
+
+val server_run = "run";
+val server_kill = "kill";
+
+val server_uuid = "uuid";
+val server_interrupt = "interrupt";
+val server_failure = "failure";
+val server_result = "result";
+
 end;
--- a/src/Pure/System/bash.scala	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/System/bash.scala	Fri Sep 03 17:54:12 2021 +0200
@@ -1,7 +1,8 @@
 /*  Title:      Pure/System/bash.scala
     Author:     Makarius
 
-GNU bash processes, with propagation of interrupts.
+Support for GNU bash: portable external processes with propagation of
+interrupts.
 */
 
 package isabelle
@@ -45,22 +46,29 @@
 
   /* process and result */
 
+  private def make_description(description: String): String =
+    proper_string(description) getOrElse "bash_process"
+
   type Watchdog = (Time, Process => Boolean)
 
   def process(script: String,
+      description: String = "",
       cwd: JFile = null,
       env: JMap[String, String] = Isabelle_System.settings(),
       redirect: Boolean = false,
       cleanup: () => Unit = () => ()): Process =
-    new Process(script, cwd, env, redirect, cleanup)
+    new Process(script, description, cwd, env, redirect, cleanup)
 
   class Process private[Bash](
       script: String,
+      description: String,
       cwd: JFile,
       env: JMap[String, String],
       redirect: Boolean,
       cleanup: () => Unit)
   {
+    override def toString: String = make_description(description)
+
     private val timing_file = Isabelle_System.tmp_file("bash_timing")
     private val timing = Synchronized[Option[Timing]](None)
     def get_timing: Timing = timing.value getOrElse Timing.zero
@@ -302,7 +310,7 @@
             Value.Boolean(redirect), Value.Seconds(timeout), description)) =>
           val uuid = UUID.random()
 
-          val descr = proper_string(description) getOrElse "bash_process"
+          val descr = make_description(description)
           if (debugging) {
             Output.writeln(
               "start " + quote(descr) + " (uuid=" + uuid + ", timeout=" + timeout.seconds + ")")
@@ -310,6 +318,7 @@
 
           Exn.capture {
             Bash.process(script,
+              description = description,
               cwd =
                 XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match {
                   case None => null
--- a/src/Pure/System/isabelle_system.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -40,10 +40,10 @@
 
 fun bash_process params =
   let
-    val {script, input, cwd, putenv, redirect, timeout, description: string} =
+    val {script, input, cwd, putenv, redirect, timeout, description} =
       Bash.dest_params params;
     val run =
-      ["run", script, input,
+      [Bash.server_run, script, input,
         let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
         let open XML.Encode in YXML.string_of_body o list (pair string string) end
           (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
@@ -57,31 +57,39 @@
     val _ = address = "" andalso raise Fail "Bad bash_process server address";
     fun with_streams f = Socket_IO.with_streams' f address password;
 
-    fun kill (SOME uuid) = with_streams (fn s => Byte_Message.write_message (#2 s) ["kill", uuid])
+    fun kill (SOME uuid) =
+          with_streams (fn s => Byte_Message.write_message (#2 s) [Bash.server_kill, uuid])
       | kill NONE = ();
   in
     Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
       let
-        fun loop maybe_uuid streams =
-          (case restore_attributes Byte_Message.read_message (#1 streams) of
-            SOME ["uuid", uuid] => loop (SOME uuid) streams
-          | SOME ["interrupt"] => raise Exn.Interrupt
-          | SOME ["failure", msg] => raise Fail msg
-          | SOME ("result" :: a :: b :: c :: d :: lines) =>
-              let
-                val rc = Value.parse_int a;
-                val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
-                val (out_lines, err_lines) = chop (Value.parse_int d) lines;
-              in
-                if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed
-                else
-                  Process_Result.make
-                   {rc = rc,
-                    out_lines = out_lines,
-                    err_lines = err_lines,
-                    timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
-             end
-          | _ => raise Fail "Malformed bash_process server result")
+        fun err () = raise Fail "Malformed result from bash_process server";
+        fun loop maybe_uuid s =
+          (case restore_attributes Byte_Message.read_message (#1 s) of
+            SOME (head :: args) =>
+              if head = Bash.server_uuid andalso length args = 1 then
+                loop (SOME (hd args)) s
+              else if head = Bash.server_interrupt andalso null args then
+                raise Exn.Interrupt
+              else if head = Bash.server_failure andalso length args = 1 then
+                raise Fail (hd args)
+              else if head = Bash.server_result andalso length args >= 4 then
+                let
+                  val a :: b :: c :: d :: lines = args;
+                  val rc = Value.parse_int a;
+                  val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
+                  val (out_lines, err_lines) = chop (Value.parse_int d) lines;
+                in
+                  if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed
+                  else
+                    Process_Result.make
+                     {rc = rc,
+                      out_lines = out_lines,
+                      err_lines = err_lines,
+                      timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
+                 end
+               else err ()
+          | _ => err ())
           handle exn => (kill maybe_uuid; Exn.reraise exn);
       in with_streams (fn s => (Byte_Message.write_message (#2 s) run; loop NONE s)) end) ()
   end;
--- a/src/Pure/System/isabelle_system.scala	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Sep 03 17:54:12 2021 +0200
@@ -387,6 +387,7 @@
   /* GNU bash */
 
   def bash(script: String,
+    description: String = "",
     cwd: JFile = null,
     env: JMap[String, String] = settings(),
     redirect: Boolean = false,
@@ -397,7 +398,8 @@
     strict: Boolean = true,
     cleanup: () => Unit = () => ()): Process_Result =
   {
-    Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
+    Bash.process(script,
+      description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
       result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr,
         watchdog = watchdog, strict = strict)
   }
--- a/src/Pure/System/options.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/System/options.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -26,7 +26,8 @@
   val put_string: string -> string -> T -> T
   val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T
   val update: string -> string -> T -> T
-  val decode: XML.body -> T
+  val encode: T XML.Encode.T
+  val decode: T XML.Decode.T
   val default: unit -> T
   val default_typ: string -> string
   val default_bool: string -> bool
@@ -150,15 +151,24 @@
   in options' end;
 
 
-(* decode *)
+(* XML data *)
 
-fun decode_opt body =
-  let open XML.Decode
-  in list (pair properties (pair string (pair string string))) end body
-  |> map (fn (props, (name, (typ, value))) =>
-      {pos = Position.of_properties props, name = name, typ = typ, value = value});
+fun encode (Options tab) =
+  let
+    val opts =
+      (tab, []) |-> Symtab.fold (fn (name, {pos, typ, value}) =>
+        cons (Position.properties_of pos, (name, (typ, value))));
+    open XML.Encode;
+  in list (pair properties (pair string (pair string string))) opts end;
 
-fun decode body = fold declare (decode_opt body) empty;
+fun decode body =
+  let
+    open XML.Decode;
+    val decode_options =
+      list (pair properties (pair string (pair string string)))
+      #> map (fn (props, (name, (typ, value))) =>
+          {pos = Position.of_properties props, name = name, typ = typ, value = value});
+  in fold declare (decode_options body) empty end;
 
 
 
--- a/src/Pure/Thy/export.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Thy/export.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -36,7 +36,7 @@
 fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
  (report_export thy binding;
   (Output.try_protocol_message o Markup.export)
-   {id = Position.get_id (Position.thread_data ()),
+   {id = Position.id_of (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = Path.implode_binding (tap Path.proper_binding binding),
--- a/src/Pure/Thy/export.scala	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/Thy/export.scala	Fri Sep 03 17:54:12 2021 +0200
@@ -376,7 +376,8 @@
 
             progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
             Isabelle_System.make_directory(path.dir)
-            Bytes.write(path, entry.uncompressed)
+            val bytes = entry.uncompressed
+            if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
             File.set_executable(path, entry.executable)
           }
         }
--- a/src/Pure/drule.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/drule.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -52,7 +52,7 @@
 sig
   include BASIC_DRULE
   val outer_params: term -> (string * typ) list
-  val generalize: string list * string list -> thm -> thm
+  val generalize: Symtab.set * Symtab.set -> thm -> thm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
   val beta_conv: cterm -> cterm -> cterm
--- a/src/Pure/goal.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/goal.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -120,6 +120,7 @@
     val fixes = map (Thm.cterm_of ctxt) xs;
 
     val tfrees = fold Term.add_tfrees (prop :: As) [];
+    val tfrees_set = fold (Symtab.insert_set o #1) tfrees Symtab.empty;
     val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees;
 
     val global_prop =
@@ -131,7 +132,7 @@
         Drule.implies_intr_list assms #>
         Drule.forall_intr_list fixes #>
         Thm.adjust_maxidx_thm ~1 #>
-        Thm.generalize (map #1 tfrees, []) 0 #>
+        Thm.generalize (tfrees_set, Symtab.empty) 0 #>
         Thm.strip_shyps #>
         Thm.solve_constraints);
     val local_result =
--- a/src/Pure/more_thm.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/more_thm.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -408,16 +408,17 @@
         val idx = Thm.maxidx_of th + 1;
         fun index ((a, A), b) = (((a, idx), A), b);
         val insts = (map index instT, map index inst);
-        val frees = (map (#1 o #1) instT, map (#1 o #1) inst);
+        val tfrees = fold (Symtab.insert_set o #1 o #1) instT Symtab.empty;
+        val frees = fold (Symtab.insert_set o #1 o #1) inst Symtab.empty;
 
         val hyps = Thm.chyps_of th;
         val inst_cterm =
-          Thm.generalize_cterm frees idx #>
+          Thm.generalize_cterm (tfrees, frees) idx #>
           Thm.instantiate_cterm insts;
       in
         th
         |> fold_rev Thm.implies_intr hyps
-        |> Thm.generalize frees idx
+        |> Thm.generalize (tfrees, frees) idx
         |> Thm.instantiate insts
         |> fold (elim_implies o Thm.assume o inst_cterm) hyps
       end;
--- a/src/Pure/proofterm.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/proofterm.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -113,7 +113,7 @@
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
-  val generalize_proof: string list * string list -> int -> term -> proof -> proof
+  val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> proof -> proof
   val lift_proof: term -> int -> term -> proof -> proof
@@ -949,14 +949,14 @@
 fun generalize_proof (tfrees, frees) idx prop prf =
   let
     val gen =
-      if null frees then []
+      if Symtab.is_empty frees then []
       else
-        fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T) | _ => I)
-          (Term_Subst.generalize (tfrees, []) idx prop) [];
+        fold_aterms (fn Free (x, T) => Symtab.defined frees x ? insert (op =) (x, T) | _ => I)
+          (Term_Subst.generalize (tfrees, Symtab.empty) idx prop) [];
   in
     prf
     |> Same.commit (map_proof_terms_same
-        (Term_Subst.generalize_same (tfrees, []) idx)
+        (Term_Subst.generalize_same (tfrees, Symtab.empty) idx)
         (Term_Subst.generalizeT_same tfrees idx))
     |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
     |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen
--- a/src/Pure/term_subst.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/term_subst.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -9,10 +9,10 @@
   val map_atypsT_same: typ Same.operation -> typ Same.operation
   val map_types_same: typ Same.operation -> term Same.operation
   val map_aterms_same: term Same.operation -> term Same.operation
-  val generalizeT_same: string list -> int -> typ Same.operation
-  val generalize_same: string list * string list -> int -> term Same.operation
-  val generalizeT: string list -> int -> typ -> typ
-  val generalize: string list * string list -> int -> term -> term
+  val generalizeT_same: Symtab.set -> int -> typ Same.operation
+  val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation
+  val generalizeT: Symtab.set -> int -> typ -> typ
+  val generalize: Symtab.set * Symtab.set -> int -> term -> term
   val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int
   val instantiate_maxidx:
     ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
@@ -68,32 +68,34 @@
 
 (* generalization of fixed variables *)
 
-fun generalizeT_same [] _ _ = raise Same.SAME
-  | generalizeT_same tfrees idx ty =
-      let
-        fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
-          | gen (TFree (a, S)) =
-              if member (op =) tfrees a then TVar ((a, idx), S)
-              else raise Same.SAME
-          | gen _ = raise Same.SAME;
-      in gen ty end;
+fun generalizeT_same tfrees idx ty =
+  if Symtab.is_empty tfrees then raise Same.SAME
+  else
+    let
+      fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
+        | gen (TFree (a, S)) =
+            if Symtab.defined tfrees a then TVar ((a, idx), S)
+            else raise Same.SAME
+        | gen _ = raise Same.SAME;
+    in gen ty end;
 
-fun generalize_same ([], []) _ _ = raise Same.SAME
-  | generalize_same (tfrees, frees) idx tm =
-      let
-        val genT = generalizeT_same tfrees idx;
-        fun gen (Free (x, T)) =
-              if member (op =) frees x then
-                Var (Name.clean_index (x, idx), Same.commit genT T)
-              else Free (x, genT T)
-          | gen (Var (xi, T)) = Var (xi, genT T)
-          | gen (Const (c, T)) = Const (c, genT T)
-          | gen (Bound _) = raise Same.SAME
-          | gen (Abs (x, T, t)) =
-              (Abs (x, genT T, Same.commit gen t)
-                handle Same.SAME => Abs (x, T, gen t))
-          | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
-      in gen tm end;
+fun generalize_same (tfrees, frees) idx tm =
+  if Symtab.is_empty tfrees andalso Symtab.is_empty frees then raise Same.SAME
+  else
+    let
+      val genT = generalizeT_same tfrees idx;
+      fun gen (Free (x, T)) =
+            if Symtab.defined frees x then
+              Var (Name.clean_index (x, idx), Same.commit genT T)
+            else Free (x, genT T)
+        | gen (Var (xi, T)) = Var (xi, genT T)
+        | gen (Const (c, T)) = Const (c, genT T)
+        | gen (Bound _) = raise Same.SAME
+        | gen (Abs (x, T, t)) =
+            (Abs (x, genT T, Same.commit gen t)
+              handle Same.SAME => Abs (x, T, gen t))
+        | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
+    in gen tm end;
 
 fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty;
 fun generalize names i tm = Same.commit (generalize_same names i) tm;
--- a/src/Pure/theory.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/theory.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -120,9 +120,7 @@
 
 fun theory_markup def name id pos =
   if id = 0 then Markup.empty
-  else
-    Markup.properties (Position.entity_properties_of def id pos)
-      (Markup.entity Markup.theoryN name);
+  else Position.make_entity_markup def id Markup.theoryN (name, pos);
 
 fun init_markup (name, pos) thy =
   let
--- a/src/Pure/thm.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/thm.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -151,9 +151,9 @@
   val equal_elim: thm -> thm -> thm
   val solve_constraints: thm -> thm
   val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
-  val generalize: string list * string list -> int -> thm -> thm
-  val generalize_cterm: string list * string list -> int -> cterm -> cterm
-  val generalize_ctyp: string list -> int -> ctyp -> ctyp
+  val generalize: Symtab.set * Symtab.set -> int -> thm -> thm
+  val generalize_cterm: Symtab.set * Symtab.set -> int -> cterm -> cterm
+  val generalize_ctyp: Symtab.set -> int -> ctyp -> ctyp
   val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     thm -> thm
   val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
@@ -1542,56 +1542,57 @@
   A[?'a/'a, ?x/x, ...]
 *)
 
-fun generalize ([], []) _ th = th
-  | generalize (tfrees, frees) idx th =
-      let
-        val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
-        val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
+fun generalize (tfrees, frees) idx th =
+  if Symtab.is_empty tfrees andalso Symtab.is_empty frees then th
+  else
+    let
+      val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
+      val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
 
-        val bad_type =
-          if null tfrees then K false
-          else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false);
-        fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x
-          | bad_term (Var (_, T)) = bad_type T
-          | bad_term (Const (_, T)) = bad_type T
-          | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t
-          | bad_term (t $ u) = bad_term t orelse bad_term u
-          | bad_term (Bound _) = false;
-        val _ = exists bad_term hyps andalso
-          raise THM ("generalize: variable free in assumptions", 0, [th]);
+      val bad_type =
+        if Symtab.is_empty tfrees then K false
+        else Term.exists_subtype (fn TFree (a, _) => Symtab.defined tfrees a | _ => false);
+      fun bad_term (Free (x, T)) = bad_type T orelse Symtab.defined frees x
+        | bad_term (Var (_, T)) = bad_type T
+        | bad_term (Const (_, T)) = bad_type T
+        | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t
+        | bad_term (t $ u) = bad_term t orelse bad_term u
+        | bad_term (Bound _) = false;
+      val _ = exists bad_term hyps andalso
+        raise THM ("generalize: variable free in assumptions", 0, [th]);
 
-        val generalize = Term_Subst.generalize (tfrees, frees) idx;
-        val prop' = generalize prop;
-        val tpairs' = map (apply2 generalize) tpairs;
-        val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
-      in
-        Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der,
-         {cert = cert,
-          tags = [],
-          maxidx = maxidx',
-          constraints = constraints,
-          shyps = shyps,
-          hyps = hyps,
-          tpairs = tpairs',
-          prop = prop'})
-      end;
+      val generalize = Term_Subst.generalize (tfrees, frees) idx;
+      val prop' = generalize prop;
+      val tpairs' = map (apply2 generalize) tpairs;
+      val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
+    in
+      Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der,
+       {cert = cert,
+        tags = [],
+        maxidx = maxidx',
+        constraints = constraints,
+        shyps = shyps,
+        hyps = hyps,
+        tpairs = tpairs',
+        prop = prop'})
+    end;
 
-fun generalize_cterm ([], []) _ ct = ct
-  | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
-      if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
-      else
-        Cterm {cert = cert, sorts = sorts,
-          T = Term_Subst.generalizeT tfrees idx T,
-          t = Term_Subst.generalize (tfrees, frees) idx t,
-          maxidx = Int.max (maxidx, idx)};
+fun generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
+  if Symtab.is_empty tfrees andalso Symtab.is_empty frees then ct
+  else if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
+  else
+    Cterm {cert = cert, sorts = sorts,
+      T = Term_Subst.generalizeT tfrees idx T,
+      t = Term_Subst.generalize (tfrees, frees) idx t,
+      maxidx = Int.max (maxidx, idx)};
 
-fun generalize_ctyp [] _ cT = cT
-  | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) =
-      if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
-      else
-        Ctyp {cert = cert, sorts = sorts,
-          T = Term_Subst.generalizeT tfrees idx T,
-          maxidx = Int.max (maxidx, idx)};
+fun generalize_ctyp tfrees idx (cT as Ctyp {cert, T, maxidx, sorts}) =
+  if Symtab.is_empty tfrees then cT
+  else if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
+  else
+    Ctyp {cert = cert, sorts = sorts,
+      T = Term_Subst.generalizeT tfrees idx T,
+      maxidx = Int.max (maxidx, idx)};
 
 
 (*Instantiation of schematic variables
--- a/src/Pure/variable.ML	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Pure/variable.ML	Fri Sep 03 17:54:12 2021 +0200
@@ -516,14 +516,14 @@
     val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
-      Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y)
-        (fixes_of inner) [];
+      Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Symtab.insert_set y)
+        (fixes_of inner) Symtab.empty;
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
       Symtab.fold (fn (a, xs) =>
         if declared_outer a orelse exists still_fixed xs
-        then I else cons a) (fold decl_type_occs ts type_occs_inner) [];
+        then I else Symtab.insert_set a) (fold decl_type_occs ts type_occs_inner) Symtab.empty;
   in (gen_fixesT, gen_fixes) end;
 
 fun exportT_inst inner outer = #1 (export_inst inner outer);
@@ -534,7 +534,7 @@
     val maxidx = maxidx_of outer;
   in
     fn ts => ts |> map
-      (Term_Subst.generalize (mk_tfrees ts, [])
+      (Term_Subst.generalize (mk_tfrees ts, Symtab.empty)
         (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1))
   end;
 
@@ -565,7 +565,7 @@
     val idx = fold Thm.maxidx_thm ths maxidx + 1;
   in map (Thm.generalize (tfrees, frees) idx) ths end;
 
-fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer);
+fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer);
 fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer);
 
 fun export_morphism inner outer =
@@ -728,13 +728,15 @@
     val ctxt' = fold declare_term ts ctxt;
     val occs = type_occs_of ctxt;
     val occs' = type_occs_of ctxt';
-    val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' [];
+    val types =
+      Symtab.fold (fn (a, _) =>
+        if Symtab.defined occs a then I else Symtab.insert_set a) occs' Symtab.empty;
     val idx = maxidx_of ctxt' + 1;
     val Ts' = (fold o fold_types o fold_atyps)
       (fn T as TFree _ =>
           (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
         | _ => I) ts [];
-    val ts' = map (Term_Subst.generalize (types, []) idx) ts;
+    val ts' = map (Term_Subst.generalize (types, Symtab.empty) idx) ts;
   in (rev Ts', ts') end;
 
 fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
--- a/src/Tools/Haskell/Haskell.thy	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Fri Sep 03 17:54:12 2021 +0200
@@ -25,7 +25,7 @@
   Bytes,
   make, unmake, pack, unpack,
   empty, null, length, index, all, any,
-  head, last, take, drop, isPrefixOf, isSuffixOf,
+  head, last, take, drop, isPrefixOf, isSuffixOf, try_unprefix, try_unsuffix,
   concat, space, spaces, char, all_char, any_char, byte, singleton
 )
 where
@@ -80,10 +80,16 @@
 last bytes = index bytes (length bytes - 1)
 
 take :: Int -> Bytes -> Bytes
-take n = pack . List.take n . unpack
+take n bs
+  | n == 0 = empty
+  | n >= length bs = bs
+  | otherwise = pack (List.take n (unpack bs))
 
 drop :: Int -> Bytes -> Bytes
-drop n = pack . List.drop n . unpack
+drop n bs
+  | n == 0 = bs
+  | n >= length bs = empty
+  | otherwise = pack (List.drop n (unpack bs))
 
 isPrefixOf :: Bytes -> Bytes -> Bool
 isPrefixOf bs1 bs2 =
@@ -95,6 +101,16 @@
   n1 <= n2 && List.all (\i -> index bs1 i == index bs2 (i + k)) [0 .. n1 - 1]
   where n1 = length bs1; n2 = length bs2; k = n2 - n1
 
+try_unprefix :: Bytes -> Bytes -> Maybe Bytes
+try_unprefix bs1 bs2 =
+  if isPrefixOf bs1 bs2 then Just (drop (length bs1) bs2)
+  else Nothing
+
+try_unsuffix :: Bytes -> Bytes -> Maybe Bytes
+try_unsuffix bs1 bs2 =
+  if isSuffixOf bs1 bs2 then Just (take (length bs2 - length bs1) bs2)
+  else Nothing
+
 concat :: [Bytes] -> Bytes
 concat = mconcat
 
@@ -210,7 +226,8 @@
 
 Basic library of Isabelle idioms.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>, \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -221,17 +238,19 @@
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
-  the, the_default,
-
-  fold, fold_rev, single, map_index, get_index, separate,
+  fold, fold_rev, single, the_single, singletonM, map_index, get_index, separate,
 
   StringLike, STRING (..), TEXT (..), BYTES (..),
   show_bytes, show_text,
 
-  proper_string, quote, space_implode, commas, commas_quote, cat_lines,
-  space_explode, split_lines, trim_line)
+  proper_string, enclose, quote, space_implode, commas, commas_quote, cat_lines,
+  space_explode, split_lines, trim_line, trim_split_lines,
+
+  getenv, getenv_strict)
 where
 
+import System.Environment (lookupEnv)
+import Data.Maybe (fromMaybe)
 import qualified Data.Text as Text
 import Data.Text (Text)
 import qualified Data.Text.Lazy as Lazy
@@ -258,17 +277,6 @@
 (f #-> g) x  = x |> f |-> g
 
 
-{- options -}
-
-the :: Maybe a -> a
-the (Just x) = x
-the Nothing = error "the Nothing"
-
-the_default :: a -> Maybe a -> a
-the_default x Nothing = x
-the_default _ (Just y) = y
-
-
 {- lists -}
 
 fold :: (a -> b -> b) -> [a] -> b -> b
@@ -282,6 +290,13 @@
 single :: a -> [a]
 single x = [x]
 
+the_single :: [a] -> a
+the_single [x] = x
+the_single _ = undefined
+
+singletonM :: Monad m => ([a] -> m [b]) -> a -> m b
+singletonM f x = the_single <$> f [x]
+
 map_index :: ((Int, a) -> b) -> [a] -> [b]
 map_index f = map_aux 0
   where
@@ -383,8 +398,11 @@
 proper_string :: StringLike a => a -> Maybe a
 proper_string s = if s == "" then Nothing else Just s
 
+enclose :: StringLike a => a -> a -> a -> a
+enclose lpar rpar str = lpar <> str <> rpar
+
 quote :: StringLike a => a -> a
-quote s = "\"" <> s <> "\""
+quote = enclose "\"" "\""
 
 space_implode :: StringLike a => a -> [a] -> a
 space_implode s = mconcat . separate s
@@ -398,6 +416,24 @@
 
 cat_lines :: StringLike a => [a] -> a
 cat_lines = space_implode "\n"
+
+trim_split_lines :: StringLike a => a -> [a]
+trim_split_lines = trim_line #> split_lines #> map trim_line
+
+
+{- getenv -}
+
+getenv :: Bytes -> IO Bytes
+getenv x = do
+  y <- lookupEnv (make_string x)
+  return $ make_bytes $ fromMaybe "" y
+
+getenv_strict :: Bytes -> IO Bytes
+getenv_strict x = do
+  y <- getenv x
+  if Bytes.null y then
+    errorWithoutStackTrace $ make_string ("Undefined Isabelle environment variable: " <> quote x)
+  else return y
 \<close>
 
 
@@ -407,9 +443,40 @@
     LICENSE:    BSD 3-clause (Isabelle)
 
 Isabelle text symbols.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/symbol.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/General/symbol_explode.ML\<close>.
 -}
 
-module Isabelle.Symbol where
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Symbol (
+  Symbol, eof, is_eof, not_eof,
+
+  is_ascii_letter, is_ascii_digit, is_ascii_hex, is_ascii_quasi,
+  is_ascii_blank, is_ascii_line_terminator, is_ascii_letdig,
+  is_ascii_identifier,
+
+  explode
+)
+where
+
+import Data.Word (Word8)
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+
+
+{- type -}
+
+type Symbol = Bytes
+
+eof :: Symbol
+eof = ""
+
+is_eof, not_eof :: Symbol -> Bool
+is_eof = Bytes.null
+not_eof = not . is_eof
+
 
 {- ASCII characters -}
 
@@ -426,7 +493,7 @@
 is_ascii_quasi c = c == '_' || c == '\''
 
 is_ascii_blank :: Char -> Bool
-is_ascii_blank c = c `elem` " \t\n\11\f\r"
+is_ascii_blank c = c `elem` (" \t\n\11\f\r" :: String)
 
 is_ascii_line_terminator :: Char -> Bool
 is_ascii_line_terminator c = c == '\r' || c == '\n'
@@ -437,6 +504,62 @@
 is_ascii_identifier :: String -> Bool
 is_ascii_identifier s =
   not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
+
+
+{- explode symbols: ASCII, UTF8, named -}
+
+is_utf8 :: Word8 -> Bool
+is_utf8 b = b >= 128
+
+is_utf8_trailer :: Word8 -> Bool
+is_utf8_trailer b = 128 <= b && b < 192
+
+is_utf8_control :: Word8 -> Bool
+is_utf8_control b = 128 <= b && b < 160
+
+(|>) :: a -> (a -> b) -> b
+x |> f = f x
+
+explode :: Bytes -> [Symbol]
+explode string = scan 0
+  where
+    byte = Bytes.index string
+    substring i j =
+      if i == j - 1 then Bytes.singleton (byte i)
+      else Bytes.pack (map byte [i .. j - 1])
+
+    n = Bytes.length string
+    test pred i = i < n && pred (byte i)
+    test_char pred i = i < n && pred (Bytes.char (byte i))
+    many pred i = if test pred i then many pred (i + 1) else i
+    maybe_char c i = if test_char (== c) i then i + 1 else i
+    maybe_ascii_id i =
+      if test_char is_ascii_letter i
+      then many (is_ascii_letdig . Bytes.char) (i + 1)
+      else i
+
+    scan i =
+      if i < n then
+        let
+          b = byte i
+          c = Bytes.char b
+        in
+          {-encoded newline-}
+          if c == '\r' then "\n" : scan (maybe_char '\n' (i + 1))
+          {-pseudo utf8: encoded ascii control-}
+          else if b == 192 && test is_utf8_control (i + 1) && not (test is_utf8 (i + 2))
+          then Bytes.singleton (byte (i + 1) - 128) : scan (i + 2)
+          {-utf8-}
+          else if is_utf8 b then
+            let j = many is_utf8_trailer (i + 1)
+            in substring i j : scan j
+          {-named symbol-}
+          else if c == '\\' && test_char (== '<') (i + 1) then
+            let j = (i + 2) |> maybe_char '^' |> maybe_ascii_id |> maybe_char '>'
+            in substring i j : scan j
+          {-single character-}
+          else Bytes.singleton b : scan (i + 1)
+      else []
 \<close>
 
 generate_file "Isabelle/Buffer.hs" = \<open>
@@ -446,7 +569,7 @@
 
 Efficient buffer of byte strings.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
 -}
 
 module Isabelle.Buffer (T, empty, add, content)
@@ -475,7 +598,7 @@
 
 Plain values, represented as string.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -540,7 +663,7 @@
 
 Property lists.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
 -}
 
 module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
@@ -581,7 +704,7 @@
 
 Quasi-abstract markup elements.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -597,6 +720,7 @@
   completionN, completion, no_completionN, no_completion,
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
+  position_properties, def_name,
 
   expressionN, expression,
 
@@ -636,6 +760,8 @@
 where
 
 import Prelude hiding (words, error, break)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
 
 import Isabelle.Library
 import qualified Isabelle.Properties as Properties
@@ -738,6 +864,24 @@
 position :: T
 position = markup_elem positionN
 
+position_properties :: [Bytes]
+position_properties = [lineN, offsetN, end_offsetN, fileN, idN]
+
+
+{- position "def" names -}
+
+make_def :: Bytes -> Bytes
+make_def a = "def_" <> a
+
+def_names :: Map Bytes Bytes
+def_names = Map.fromList $ map (\a -> (a, make_def a)) position_properties
+
+def_name :: Bytes -> Bytes
+def_name a =
+  case Map.lookup a def_names of
+    Just b -> b
+    Nothing -> make_def a
+
 
 {- expression -}
 
@@ -1090,6 +1234,238 @@
 no_output = ("", "")
 \<close>
 
+generate_file "Isabelle/Position.hs" = \<open>
+{-  Title:      Isabelle/Position.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
+symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
+right-open interval offset .. end_offset (exclusive).
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/position.ML\<close>.
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Position (
+  T, line_of, column_of, offset_of, end_offset_of, file_of, id_of,
+  start, none, put_file, file, file_only, put_id, id, id_only,
+  symbol, symbol_explode, symbol_explode_string, shift_offsets,
+  of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup,
+  Report, Report_Text, is_reported, is_reported_range, here,
+  Range, no_range, no_range_position, range_position, range
+)
+where
+
+import Prelude hiding (id)
+import Data.Maybe (isJust, fromMaybe)
+import Data.Bifunctor (first)
+import qualified Isabelle.Properties as Properties
+import qualified Isabelle.Bytes as Bytes
+import qualified Isabelle.Value as Value
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Markup as Markup
+import qualified Isabelle.YXML as YXML
+import Isabelle.Library
+import qualified Isabelle.Symbol as Symbol
+import Isabelle.Symbol (Symbol)
+
+
+{- position -}
+
+data T =
+  Position {
+    _line :: Int,
+    _column :: Int,
+    _offset :: Int,
+    _end_offset :: Int,
+    _file :: Bytes,
+    _id :: Bytes }
+  deriving (Eq, Ord)
+
+valid, invalid :: Int -> Bool
+valid i = i > 0
+invalid = not . valid
+
+maybe_valid :: Int -> Maybe Int
+maybe_valid i = if valid i then Just i else Nothing
+
+if_valid :: Int -> Int -> Int
+if_valid i i' = if valid i then i' else i
+
+
+{- fields -}
+
+line_of, column_of, offset_of, end_offset_of :: T -> Maybe Int
+line_of = maybe_valid . _line
+column_of = maybe_valid . _column
+offset_of = maybe_valid . _offset
+end_offset_of = maybe_valid . _end_offset
+
+file_of :: T -> Maybe Bytes
+file_of = proper_string . _file
+
+id_of :: T -> Maybe Bytes
+id_of = proper_string . _id
+
+
+{- make position -}
+
+start :: T
+start = Position 1 1 1 0 Bytes.empty Bytes.empty
+
+none :: T
+none = Position 0 0 0 0 Bytes.empty Bytes.empty
+
+put_file :: Bytes -> T -> T
+put_file file pos = pos { _file = file }
+
+file :: Bytes -> T
+file file = put_file file start
+
+file_only :: Bytes -> T
+file_only file = put_file file none
+
+put_id :: Bytes -> T -> T
+put_id id pos = pos { _id = id }
+
+id :: Bytes -> T
+id id = put_id id start
+
+id_only :: Bytes -> T
+id_only id = put_id id none
+
+
+{- count position -}
+
+count_line :: Symbol -> Int -> Int
+count_line "\n" line = if_valid line (line + 1)
+count_line _ line = line
+
+count_column :: Symbol -> Int -> Int
+count_column "\n" column = if_valid column 1
+count_column s column = if Symbol.not_eof s then if_valid column (column + 1) else column
+
+count_offset :: Symbol -> Int -> Int
+count_offset s offset = if Symbol.not_eof s then if_valid offset (offset + 1) else offset
+
+symbol :: Symbol -> T -> T
+symbol s pos =
+  pos {
+    _line = count_line s (_line pos),
+    _column = count_column s (_column pos),
+    _offset = count_offset s (_offset pos) }
+
+symbol_explode :: BYTES a => a -> T -> T
+symbol_explode = fold symbol . Symbol.explode . make_bytes
+
+symbol_explode_string :: String -> T -> T
+symbol_explode_string = symbol_explode
+
+
+{- shift offsets -}
+
+shift_offsets :: Int -> T -> T
+shift_offsets shift pos = pos { _offset = offset', _end_offset = end_offset' }
+  where
+    offset = _offset pos
+    end_offset = _end_offset pos
+    offset' = if invalid offset || invalid shift then offset else offset + shift
+    end_offset' = if invalid end_offset || invalid shift then end_offset else end_offset + shift
+
+
+{- markup properties -}
+
+get_string :: Properties.T -> Bytes -> Bytes
+get_string props name = fromMaybe "" (Properties.get_value Just props name)
+
+get_int :: Properties.T -> Bytes -> Int
+get_int props name = fromMaybe 0 (Properties.get_value Value.parse_int props name)
+
+of_properties :: Properties.T -> T
+of_properties props =
+  none {
+    _line = get_int props Markup.lineN,
+    _offset = get_int props Markup.offsetN,
+    _end_offset = get_int props Markup.end_offsetN,
+    _file = get_string props Markup.fileN,
+    _id = get_string props Markup.idN }
+
+string_entry :: Bytes -> Bytes -> Properties.T
+string_entry k s = if Bytes.null s then [] else [(k, s)]
+
+int_entry :: Bytes -> Int -> Properties.T
+int_entry k i = if invalid i then [] else [(k, Value.print_int i)]
+
+properties_of :: T -> Properties.T
+properties_of pos =
+  int_entry Markup.lineN (_line pos) ++
+  int_entry Markup.offsetN (_offset pos) ++
+  int_entry Markup.end_offsetN (_end_offset pos) ++
+  string_entry Markup.fileN (_file pos) ++
+  string_entry Markup.idN (_id pos)
+
+def_properties_of :: T -> Properties.T
+def_properties_of = properties_of #> map (first Markup.def_name)
+
+entity_markup :: Bytes -> (Bytes, T) -> Markup.T
+entity_markup kind (name, pos) =
+  Markup.entity kind name |> Markup.properties (def_properties_of pos)
+
+make_entity_markup :: Bool -> Int -> Bytes -> (Bytes, T) -> Markup.T
+make_entity_markup def serial kind (name, pos) =
+  let
+    props =
+      if def then (Markup.defN, Value.print_int serial) : properties_of pos
+      else (Markup.refN, Value.print_int serial) : def_properties_of pos
+  in Markup.entity kind name |> Markup.properties props
+
+
+{- reports -}
+
+type Report = (T, Markup.T)
+type Report_Text = (Report, Bytes)
+
+is_reported :: T -> Bool
+is_reported pos = isJust (offset_of pos) && isJust (id_of pos)
+
+is_reported_range :: T -> Bool
+is_reported_range pos = is_reported pos && isJust (end_offset_of pos)
+
+
+{- here: user output -}
+
+here :: T -> Bytes
+here pos = if Bytes.null s2 then "" else s1 <> m1 <> s2 <> m2
+  where
+    props = properties_of pos
+    (m1, m2) = YXML.output_markup (Markup.properties props Markup.position)
+    (s1, s2) =
+      case (line_of pos, file_of pos) of
+        (Just i, Nothing) -> (" ", "(line " <> Value.print_int i <> ")")
+        (Just i, Just name) -> (" ", "(line " <> Value.print_int i <> " of " <> quote name <> ")")
+        (Nothing, Just name) -> (" ", "(file " <> quote name <> ")")
+        _ -> if is_reported pos then ("", "\092<^here>") else ("", "")
+
+
+{- range -}
+
+type Range = (T, T)
+
+no_range :: Range
+no_range = (none, none)
+
+no_range_position :: T -> T
+no_range_position pos = pos { _end_offset = 0 }
+
+range_position :: Range -> T
+range_position (pos, pos') = pos { _end_offset = _offset pos' }
+
+range :: Range -> Range
+range (pos, pos') = (range_position (pos, pos'), no_range_position pos')
+\<close>
+
 generate_file "Isabelle/XML.hs" = \<open>
 {-  Title:      Isabelle/XML.hs
     Author:     Makarius
@@ -1097,7 +1473,7 @@
 
 Untyped XML trees and representation of ML values.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -1185,7 +1561,7 @@
 
 XML as data representation language.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -1200,6 +1576,8 @@
 )
 where
 
+import Data.Maybe (fromJust)
+
 import Isabelle.Library
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.Value as Value
@@ -1270,7 +1648,7 @@
 option f (Just x) = [node (f x)]
 
 variant :: [V a] -> T a
-variant fs x = [tagged (the (get_index (\f -> f x) fs))]
+variant fs x = [tagged (fromJust (get_index (\f -> f x) fs))]
 \<close>
 
 generate_file "Isabelle/XML/Decode.hs" = \<open>
@@ -1280,7 +1658,7 @@
 
 XML as data representation language.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -1395,7 +1773,7 @@
 Efficient text representation of XML trees.  Suitable for direct
 inlining into plain text.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -1534,7 +1912,7 @@
 
 Completion of names.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -1591,7 +1969,7 @@
 
 File-system operations.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
 -}
 
 module Isabelle.File (read, write, append) where
@@ -1619,7 +1997,7 @@
 
 Generic pretty printing module.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -1637,7 +2015,7 @@
 
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
-import Isabelle.Library hiding (quote, separate, commas)
+import Isabelle.Library hiding (enclose, quote, separate, commas)
 import qualified Isabelle.Buffer as Buffer
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.XML as XML
@@ -1775,13 +2153,15 @@
 
 Names of basic logical entities (variables etc.).
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Name (
-  Name, clean_index, clean,
+  Name,
+  uu, uu_, aT,
+  clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
   Context, declare, is_declared, context, make_context, variant
 )
 where
@@ -1798,11 +2178,31 @@
 type Name = Bytes
 
 
-{- suffix for internal names -}
+{- common defaults -}
+
+uu, uu_, aT :: Name
+uu = "uu"
+uu_ = "uu_"
+aT = "'a"
+
+
+{- internal names -- NB: internal subsumes skolem -}
 
 underscore :: Word8
 underscore = Bytes.byte '_'
 
+internal, skolem :: Name -> Name
+internal x = x <> "_"
+skolem x = x <> "__"
+
+is_internal, is_skolem :: Name -> Bool
+is_internal = Bytes.isSuffixOf "_"
+is_skolem = Bytes.isSuffixOf "__"
+
+dest_internal, dest_skolem :: Name -> Maybe Name
+dest_internal = Bytes.try_unsuffix "_"
+dest_skolem = Bytes.try_unsuffix "__"
+
 clean_index :: Name -> (Name, Int)
 clean_index x =
   if Bytes.null x || Bytes.last x /= underscore then (x, 0)
@@ -1819,7 +2219,7 @@
 
 {- context for used names -}
 
-data Context = Context (Set Name)
+newtype Context = Context (Set Name)
 
 declare :: Name -> Context -> Context
 declare x (Context names) = Context (Set.insert x names)
@@ -1870,15 +2270,15 @@
 
 Lambda terms, types, sorts.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Term (
   Indexname, Sort, Typ(..), Term(..),
-  Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
-  type_op0, type_op1, op0, op1, op2, typed_op2, binder,
+  Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_lambda, strip_lambda,
+  type_op0, type_op1, op0, op1, op2, typed_op0, typed_op1, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
   aconv, list_comb, strip_comb, head_of
 )
@@ -1951,19 +2351,19 @@
     subst lev (App (t, u)) = App (subst lev t, subst lev u)
     subst _ t = t
 
-dest_abs :: Name.Context -> Term -> Maybe (Free, Term)
-dest_abs names (Abs (x, ty, b)) =
+dest_lambda :: Name.Context -> Term -> Maybe (Free, Term)
+dest_lambda names (Abs (x, ty, b)) =
   let
     (x', _) = Name.variant x (declare_frees b names)
     v = (x', ty)
   in Just (v, subst_bound (Free v) b)
-dest_abs _ _ = Nothing
-
-strip_abs :: Name.Context -> Term -> ([Free], Term)
-strip_abs names tm =
-  case dest_abs names tm of
+dest_lambda _ _ = Nothing
+
+strip_lambda :: Name.Context -> Term -> ([Free], Term)
+strip_lambda names tm =
+  case dest_lambda names tm of
     Just (v, t) ->
-      let (vs, t') = strip_abs names t'
+      let (vs, t') = strip_lambda names t'
       in (v : vs, t')
     Nothing -> ([], tm)
 
@@ -1974,21 +2374,21 @@
 type_op0 name = (mk, is)
   where
     mk = Type (name, [])
-    is (Type (name, _)) = True
+    is (Type (c, _)) = c == name
     is _ = False
 
 type_op1 :: Name -> (Typ -> Typ, Typ -> Maybe Typ)
 type_op1 name = (mk, dest)
   where
     mk ty = Type (name, [ty])
-    dest (Type (name, [ty])) = Just ty
+    dest (Type (c, [ty])) | c == name = Just ty
     dest _ = Nothing
 
 type_op2 :: Name -> (Typ -> Typ -> Typ, Typ -> Maybe (Typ, Typ))
 type_op2 name = (mk, dest)
   where
     mk ty1 ty2 = Type (name, [ty1, ty2])
-    dest (Type (name, [ty1, ty2])) = Just (ty1, ty2)
+    dest (Type (c, [ty1, ty2])) | c == name = Just (ty1, ty2)
     dest _ = Nothing
 
 op0 :: Name -> (Term, Term -> Bool)
@@ -2012,6 +2412,20 @@
     dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
     dest _ = Nothing
 
+typed_op0 :: Name -> (Typ -> Term, Term -> Maybe Typ)
+typed_op0 name = (mk, dest)
+  where
+    mk ty = Const (name, [ty])
+    dest (Const (c, [ty])) | c == name = Just ty
+    dest _ = Nothing
+
+typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term))
+typed_op1 name = (mk, dest)
+  where
+    mk ty t = App (Const (name, [ty]), t)
+    dest (App (Const (c, [ty]), t)) | c == name = Just (ty, t)
+    dest _ = Nothing
+
 typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term))
 typed_op2 name = (mk, dest)
   where
@@ -2023,7 +2437,7 @@
 binder name = (mk, dest)
   where
     mk (a, ty) b = App (Const (name, [ty]), lambda (a, ty) b)
-    dest names (App (Const (c, _), t)) | c == name = dest_abs names t
+    dest names (App (Const (c, _), t)) | c == name = dest_lambda names t
     dest _ _ = Nothing
 
 
@@ -2075,19 +2489,23 @@
 
 Support for Isabelle/Pure logic.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/logic.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/logic.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Pure (
-  mk_forall, dest_forall, mk_equals, dest_equals, mk_implies, dest_implies
+  mk_forall_op, dest_forall_op, mk_forall, dest_forall,
+  mk_equals, dest_equals, mk_implies, dest_implies
 )
 where
 
 import qualified Isabelle.Name as Name
 import Isabelle.Term
 
+mk_forall_op :: Typ -> Term -> Term; dest_forall_op :: Term -> Maybe (Typ, Term)
+(mk_forall_op, dest_forall_op) = typed_op1 \<open>\<^const_name>\<open>Pure.all\<close>\<close>
+
 mk_forall :: Free -> Term -> Term; dest_forall :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_forall, dest_forall) = binder \<open>\<^const_name>\<open>Pure.all\<close>\<close>
 
@@ -2105,7 +2523,7 @@
 
 Support for Isabelle/HOL logic.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/HOL/Tools/hologic.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/HOL/Tools/hologic.ML\<close>.
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
@@ -2116,7 +2534,9 @@
   mk_eq, dest_eq, true, is_true, false, is_false,
   mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
   mk_imp, dest_imp, mk_iff, dest_iff,
-  mk_all, dest_all, mk_ex, dest_ex
+  mk_all_op, dest_all_op, mk_ex_op, dest_ex_op,
+  mk_all, dest_all, mk_ex, dest_ex,
+  mk_undefined, dest_undefined
 )
 where
 
@@ -2166,11 +2586,20 @@
     Just (ty, t, u) | ty == boolT -> Just (t, u)
     _ -> Nothing
 
+mk_all_op :: Typ -> Term -> Term; dest_all_op :: Term -> Maybe (Typ, Term)
+(mk_all_op, dest_all_op) = typed_op1 \<open>\<^const_name>\<open>All\<close>\<close>
+
+mk_ex_op :: Typ -> Term -> Term; dest_ex_op :: Term -> Maybe (Typ, Term)
+(mk_ex_op, dest_ex_op) = typed_op1 \<open>\<^const_name>\<open>Ex\<close>\<close>
+
 mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_all, dest_all) = binder \<open>\<^const_name>\<open>All\<close>\<close>
 
 mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_ex, dest_ex) = binder \<open>\<^const_name>\<open>Ex\<close>\<close>
+
+mk_undefined :: Typ -> Term; dest_undefined :: Term -> Maybe Typ
+(mk_undefined, dest_undefined) = typed_op0 \<open>\<^const_name>\<open>undefined\<close>\<close>
 \<close>
 
 generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
@@ -2180,7 +2609,7 @@
 
 XML data representation of lambda terms.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
 -}
 
 {-# LANGUAGE LambdaCase #-}
@@ -2226,7 +2655,7 @@
 
 XML data representation of lambda terms.
 
-See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
 -}
 
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
@@ -2405,6 +2834,7 @@
     write, write_line,
     read, read_block, read_line,
     make_message, write_message, read_message,
+    exchange_message, exchange_message0,
     make_line_message, write_line_message, read_line_message,
     read_yxml, write_yxml
   )
@@ -2507,6 +2937,16 @@
     Just line -> Just <$> mapM (read_chunk socket) (parse_header line)
     Nothing -> return Nothing
 
+exchange_message :: Socket -> [Bytes] -> IO (Maybe [Bytes])
+exchange_message socket msg = do
+  write_message socket msg
+  read_message socket
+
+exchange_message0 :: Socket -> [Bytes] -> IO ()
+exchange_message0 socket msg = do
+  _ <- exchange_message socket msg
+  return ()
+
 
 -- hybrid messages: line or length+block (with content restriction)
 
@@ -2732,7 +3172,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Server (
-  localhost_name, localhost, publish_text, publish_stdout,
+  localhost_name, localhost_prefix, localhost, publish_text, publish_stdout,
   server, connection
 )
 where
@@ -2757,6 +3197,9 @@
 localhost_name :: Bytes
 localhost_name = "127.0.0.1"
 
+localhost_prefix :: Bytes
+localhost_prefix = localhost_name <> ":"
+
 localhost :: Socket.HostAddress
 localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
 
@@ -2817,7 +3260,7 @@
             Socket.defaultHints {
               Socket.addrFlags = [Socket.AI_NUMERICHOST, Socket.AI_NUMERICSERV],
               Socket.addrSocketType = Socket.Stream }
-      head <$> Socket.getAddrInfo (Just hints) (Just "127.0.0.1") (Just port)
+      head <$> Socket.getAddrInfo (Just hints) (Just $ make_string localhost_name) (Just port)
 
     open addr = do
       socket <- Socket.socket (Socket.addrFamily addr) (Socket.addrSocketType addr)
@@ -2830,6 +3273,539 @@
       client socket
 \<close>
 
+generate_file "Isabelle/Time.hs" = \<open>
+{-  Title:      Isabelle/Time.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Time based on milliseconds.
+
+See \<^file>\<open>~~/src/Pure/General/time.scala\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Time (
+  Time, seconds, minutes, ms, zero, is_zero, is_relevant,
+  get_seconds, get_minutes, get_ms, message, now
+)
+where
+
+import Text.Printf (printf)
+import Data.Time.Clock.POSIX (getPOSIXTime)
+import Isabelle.Bytes (Bytes)
+import Isabelle.Library
+
+
+newtype Time = Time Int
+
+instance Eq Time where Time ms1 == Time ms2 = ms1 == ms2
+instance Ord Time where compare (Time ms1) (Time ms2) = compare ms1 ms2
+
+seconds :: Double -> Time
+seconds s = Time (round (s * 1000.0))
+
+minutes :: Double -> Time
+minutes m = Time (round (m * 60000.0))
+
+ms :: Int -> Time
+ms = Time
+
+zero :: Time
+zero = ms 0
+
+is_zero :: Time -> Bool
+is_zero (Time ms) = ms == 0
+
+is_relevant :: Time -> Bool
+is_relevant (Time ms) = ms >= 1
+
+get_seconds :: Time -> Double
+get_seconds (Time ms) = fromIntegral ms / 1000.0
+
+get_minutes :: Time -> Double
+get_minutes (Time ms) = fromIntegral ms / 60000.0
+
+get_ms :: Time -> Int
+get_ms (Time ms) = ms
+
+instance Show Time where
+  show t = printf "%.3f" (get_seconds t)
+
+message :: Time -> Bytes
+message t = make_bytes (show t) <> "s"
+
+now :: IO Time
+now = do
+  t <- getPOSIXTime
+  return $ Time (round (realToFrac t * 1000.0 :: Double))
+\<close>
+
+generate_file "Isabelle/Timing.hs" = \<open>
+{-  Title:      Isabelle/Timing.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Support for time measurement.
+
+See \<^file>\<open>~~/src/Pure/General/timing.ML\<close>
+and \<^file>\<open>~~/src/Pure/General/timing.scala\<close>
+-}
+
+module Isabelle.Timing (
+  Timing (..), zero, is_zero, is_relevant
+)
+where
+
+import qualified Isabelle.Time as Time
+import Isabelle.Time (Time)
+
+data Timing = Timing {elapsed :: Time, cpu :: Time, gc :: Time}
+  deriving (Show, Eq)
+
+zero :: Timing
+zero = Timing Time.zero Time.zero Time.zero
+
+is_zero :: Timing -> Bool
+is_zero t = Time.is_zero (elapsed t) && Time.is_zero (cpu t) && Time.is_zero (gc t)
+
+is_relevant :: Timing -> Bool
+is_relevant t = Time.is_relevant (elapsed t) || Time.is_relevant (cpu t) || Time.is_relevant (gc t)
+\<close>
+
+generate_file "Isabelle/Bash.hs" = \<open>
+{-  Title:      Isabelle/Bash.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Support for GNU bash.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/System/bash.ML\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Bash (
+  string, strings,
+
+  Params,
+  get_script, get_input, get_cwd, get_putenv, get_redirect,
+  get_timeout, get_description,
+  script, input, cwd, putenv, redirect, timeout, description,
+  server_run, server_kill,
+  server_uuid, server_interrupt, server_failure, server_result
+)
+where
+
+import Text.Printf (printf)
+import qualified Isabelle.Symbol as Symbol
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Time as Time
+import Isabelle.Time (Time)
+import Isabelle.Library
+
+
+{- concrete syntax -}
+
+string :: Bytes -> Bytes
+string str =
+  if Bytes.null str then "\"\""
+  else str |> Bytes.unpack |> map trans |> Bytes.concat
+    where
+      trans b =
+        case Bytes.char b of
+          '\t' -> "$'\\t'"
+          '\n' -> "$'\\n'"
+          '\f' -> "$'\\f'"
+          '\r' -> "$'\\r'"
+          c ->
+            if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c `elem` ("+,-./:_" :: String)
+            then Bytes.singleton b
+            else if b < 32 || b >= 127 then make_bytes (printf "$'\\x%02x'" b :: String)
+            else "\\" <> Bytes.singleton b
+
+strings :: [Bytes] -> Bytes
+strings = space_implode " " . map string
+
+
+{- server parameters -}
+
+data Params = Params {
+    _script :: Bytes,
+    _input :: Bytes,
+    _cwd :: Maybe Bytes,
+    _putenv :: [(Bytes, Bytes)],
+    _redirect :: Bool,
+    _timeout :: Time,
+    _description :: Bytes}
+  deriving (Show, Eq)
+
+get_script :: Params -> Bytes
+get_script = _script
+
+get_input :: Params -> Bytes
+get_input = _input
+
+get_cwd :: Params -> Maybe Bytes
+get_cwd = _cwd
+
+get_putenv :: Params -> [(Bytes, Bytes)]
+get_putenv = _putenv
+
+get_redirect :: Params -> Bool
+get_redirect = _redirect
+
+get_timeout :: Params -> Time
+get_timeout = _timeout
+
+get_description :: Params -> Bytes
+get_description = _description
+
+script :: Bytes -> Params
+script script = Params script "" Nothing [] False Time.zero ""
+
+input :: Bytes -> Params -> Params
+input input params = params { _input = input }
+
+cwd :: Bytes -> Params -> Params
+cwd cwd params = params { _cwd = Just cwd }
+
+putenv :: [(Bytes, Bytes)] -> Params -> Params
+putenv putenv params = params { _putenv = putenv }
+
+redirect :: Params -> Params
+redirect params = params { _redirect = True }
+
+timeout :: Time -> Params -> Params
+timeout timeout params = params { _timeout = timeout }
+
+description :: Bytes -> Params -> Params
+description description params = params { _description = description }
+
+
+{- server messages -}
+
+server_run, server_kill :: Bytes
+server_run = \<open>Bash.server_run\<close>;
+server_kill = \<open>Bash.server_kill\<close>;
+
+server_uuid, server_interrupt, server_failure, server_result :: Bytes
+server_uuid = \<open>Bash.server_uuid\<close>;
+server_interrupt = \<open>Bash.server_interrupt\<close>;
+server_failure = \<open>Bash.server_failure\<close>;
+server_result = \<open>Bash.server_result\<close>;
+\<close>
+
+generate_file "Isabelle/Process_Result.hs" = \<open>
+{-  Title:      Isabelle/Process_Result.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Result of system process.
+
+See \<^file>\<open>~~/src/Pure/System/process_result.ML\<close>
+and \<^file>\<open>~~/src/Pure/System/process_result.scala\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Process_Result (
+  interrupt_rc, timeout_rc,
+
+  T, make, rc, out_lines, err_lines, timing, timing_elapsed, out, err, ok, check
+)
+where
+
+import Isabelle.Time (Time)
+import qualified Isabelle.Timing as Timing
+import Isabelle.Timing (Timing)
+import Isabelle.Bytes (Bytes)
+import Isabelle.Library
+
+
+interrupt_rc :: Int
+interrupt_rc = 130
+
+timeout_rc :: Int
+timeout_rc = 142
+
+data T =
+  Process_Result {
+    _rc :: Int,
+    _out_lines :: [Bytes],
+    _err_lines :: [Bytes],
+    _timing :: Timing}
+  deriving (Show, Eq)
+
+make :: Int -> [Bytes] -> [Bytes] -> Timing -> T
+make = Process_Result
+
+rc :: T -> Int
+rc = _rc
+
+out_lines :: T -> [Bytes]
+out_lines = _out_lines
+
+err_lines :: T -> [Bytes]
+err_lines = _err_lines
+
+timing :: T -> Timing
+timing = _timing
+
+timing_elapsed :: T -> Time
+timing_elapsed = Timing.elapsed . timing
+
+out :: T -> Bytes
+out = trim_line . cat_lines . out_lines
+
+err :: T -> Bytes
+err = trim_line . cat_lines . err_lines
+
+ok :: T -> Bool
+ok result = rc result == 0
+
+check :: T -> T
+check result = if ok result then result else error (make_string $ err result)
+\<close>
+
+generate_file "Isabelle/Options.hs" = \<open>
+{-  Title:      Isabelle/Options.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+System options with external string representation.
+
+See \<^file>\<open>~~/src/Pure/System/options.ML\<close>
+and \<^file>\<open>~~/src/Pure/System/options.scala\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE InstanceSigs #-}
+
+module Isabelle.Options (
+  boolT, intT, realT, stringT, unknownT,
+
+  T, typ, bool, int, real, seconds, string,
+  decode
+)
+where
+
+import qualified Data.Map.Strict as Map
+import Data.Map.Strict (Map)
+import qualified Isabelle.Properties as Properties
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Value as Value
+import qualified Isabelle.Time as Time
+import Isabelle.Time (Time)
+import Isabelle.Library
+import qualified Isabelle.XML.Decode as Decode
+import Isabelle.XML.Classes (Decode (..))
+
+
+{- representation -}
+
+boolT :: Bytes
+boolT = "bool"
+
+intT :: Bytes
+intT = "int"
+
+realT :: Bytes
+realT = "real"
+
+stringT :: Bytes
+stringT = "string"
+
+unknownT :: Bytes
+unknownT = "unknown"
+
+data Opt = Opt {
+  _pos :: Properties.T,
+  _name :: Bytes,
+  _typ :: Bytes,
+  _value :: Bytes }
+
+data T = Options (Map Bytes Opt)
+
+
+{- check -}
+
+check_name :: T -> Bytes -> Opt
+check_name (Options map) name =
+  case Map.lookup name map of
+    Just opt | _typ opt /= unknownT -> opt
+    _ -> error (make_string ("Unknown system option " <> quote name))
+
+check_type :: T -> Bytes -> Bytes -> Opt
+check_type options name typ =
+  let
+    opt = check_name options name
+    t = _typ opt
+  in
+    if t == typ then opt
+    else error (make_string ("Ill-typed system option " <> quote name <> " : " <> t <> " vs. " <> typ))
+
+
+{- get typ -}
+
+typ :: T -> Bytes -> Bytes
+typ options name = _typ (check_name options name)
+
+
+{- get value -}
+
+get :: Bytes -> (Bytes -> Maybe a) -> T -> Bytes -> a
+get typ parse options name =
+  let opt = check_type options name typ in
+    case parse (_value opt) of
+      Just x -> x
+      Nothing ->
+        error (make_string ("Malformed value for system option " <> quote name <>
+          " : " <> typ <> " =\n" <> quote (_value opt)))
+
+bool :: T -> Bytes -> Bool
+bool = get boolT Value.parse_bool
+
+int :: T -> Bytes -> Int
+int = get intT Value.parse_int
+
+real :: T -> Bytes -> Double
+real = get realT Value.parse_real
+
+seconds :: T -> Bytes -> Time
+seconds options = Time.seconds . real options
+
+string :: T -> Bytes -> Bytes
+string = get stringT Just
+
+
+{- decode -}
+
+instance Decode T where
+  decode :: Decode.T T
+  decode =
+    let
+      decode_entry :: Decode.T (Bytes, Opt)
+      decode_entry body =
+        let
+          (pos, (name, (typ, value))) =
+            Decode.pair Decode.properties (Decode.pair Decode.string (Decode.pair Decode.string Decode.string)) body
+        in (name, Opt { _pos = pos, _name = name, _typ = typ, _value = value })
+    in Options . Map.fromList . Decode.list decode_entry
+\<close>
+
+generate_file "Isabelle/Isabelle_System.hs" = \<open>
+{-  Title:      Isabelle/Isabelle_System.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Isabelle system support.
+
+See \<^file>\<open>~~/src/Pure/System/isabelle_system.ML\<close>
+and \<^file>\<open>~~/src/Pure/System/isabelle_system.scala\<close>
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Isabelle_System (
+  bash_process, bash_process0
+)
+where
+
+import Data.Maybe (fromMaybe)
+import Control.Exception (throw, AsyncException (UserInterrupt))
+import Network.Socket (Socket)
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Byte_Message as Byte_Message
+import qualified Isabelle.Time as Time
+import Isabelle.Timing (Timing (..))
+import qualified Isabelle.Options as Options
+import qualified Isabelle.Bash as Bash
+import qualified Isabelle.Process_Result as Process_Result
+import qualified Isabelle.XML.Encode as Encode
+import qualified Isabelle.YXML as YXML
+import qualified Isabelle.Value as Value
+import qualified Isabelle.Server as Server
+import qualified Isabelle.Isabelle_Thread as Isabelle_Thread
+import Isabelle.Library
+
+
+{- bash_process -}
+
+absolute_path :: Bytes -> Bytes  -- FIXME dummy
+absolute_path = id
+
+bash_process :: Options.T -> Bash.Params -> IO Process_Result.T
+bash_process options = bash_process0 address password
+  where
+    address = Options.string options "bash_process_address"
+    password = Options.string options "bash_process_password"
+
+bash_process0 :: Bytes -> Bytes -> Bash.Params -> IO Process_Result.T
+bash_process0 address password params = do
+  Server.connection port password
+    (\socket -> do
+        isabelle_tmp <- getenv "ISABELLE_TMP"
+        Byte_Message.write_message socket (run isabelle_tmp)
+        loop Nothing socket)
+  where
+    port =
+      case Bytes.try_unprefix Server.localhost_prefix address of
+        Just port -> make_string port
+        Nothing -> errorWithoutStackTrace "Bad bash_process server address"
+
+    script = Bash.get_script params
+    input = Bash.get_input params
+    cwd = Bash.get_cwd params
+    putenv = Bash.get_putenv params
+    redirect = Bash.get_redirect params
+    timeout = Bash.get_timeout params
+    description = Bash.get_description params
+
+    run :: Bytes -> [Bytes]
+    run isabelle_tmp =
+     [Bash.server_run, script, input,
+      YXML.string_of_body (Encode.option (Encode.string . absolute_path) cwd),
+      YXML.string_of_body
+      (Encode.list (Encode.pair Encode.string Encode.string)
+        (("ISABELLE_TMP", isabelle_tmp) : putenv)),
+      Value.print_bool redirect,
+      Value.print_real (Time.get_seconds timeout),
+      description]
+
+    kill :: Maybe Bytes -> IO ()
+    kill maybe_uuid = do
+      case maybe_uuid of
+        Just uuid ->
+          Server.connection port password (\socket ->
+            Byte_Message.write_message socket [Bash.server_kill, uuid])
+        Nothing -> return ()
+
+    err = errorWithoutStackTrace "Malformed result from bash_process server"
+    the = fromMaybe err
+
+    loop :: Maybe Bytes -> Socket -> IO Process_Result.T
+    loop maybe_uuid socket = do
+      result <- Isabelle_Thread.bracket_resource (kill maybe_uuid) (Byte_Message.read_message socket)
+      case result of
+        Just [head, uuid] | head == Bash.server_uuid -> loop (Just uuid) socket
+        Just [head] | head == Bash.server_interrupt -> throw UserInterrupt
+        Just [head, msg] | head == Bash.server_failure -> errorWithoutStackTrace $ make_string msg
+        Just (head : a : b : c : d : lines) | head == Bash.server_result ->
+          let
+            rc = the $ Value.parse_int a
+            elapsed = Time.ms $ the $ Value.parse_int b
+            cpu = Time.ms $ the $ Value.parse_int c
+            timing = Timing elapsed cpu Time.zero
+            n = the $ Value.parse_int d
+            out_lines = take n lines
+            err_lines = drop n lines
+          in return $ Process_Result.make rc out_lines err_lines timing
+        _ -> err
+\<close>
+
 export_generated_files _
 
 end
--- a/src/Tools/Haskell/Test.thy	Tue Aug 17 17:09:20 2021 +0200
+++ b/src/Tools/Haskell/Test.thy	Fri Sep 03 17:54:12 2021 +0200
@@ -18,7 +18,7 @@
         GHC.new_project dir
           {name = "isabelle",
            depends =
-            ["array", "bytestring", "containers", "network", "split", "text", "threads", "uuid"],
+            ["array", "bytestring", "containers", "network", "split", "text", "time", "threads", "uuid"],
            modules = modules};
     in
       writeln (Generated_Files.execute dir \<open>Build\<close> "mv Isabelle src && isabelle ghc_stack build")