# HG changeset patch
# User wenzelm
# Date 1502224805 -7200
# Node ID 429b55991197102261b3b8bc84850cf24e929a79
# Parent  1b70820dc6ba05e4324dd4a375385d4bc24adbb9# Parent  96ff0eb8294a323f3e9545498f266e7c4d60d881
merged

diff -r 1b70820dc6ba -r 429b55991197 etc/options
--- a/etc/options	Tue Aug 08 13:31:48 2017 +0200
+++ b/etc/options	Tue Aug 08 22:40:05 2017 +0200
@@ -155,6 +155,9 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
+public option editor_consolidate_delay : real = 1.0
+  -- "delay to consolidate status of command evaluation (execution forks)"
+
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 
diff -r 1b70820dc6ba -r 429b55991197 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Tue Aug 08 22:40:05 2017 +0200
@@ -1,6 +1,9 @@
 (*  Title:      HOL/Number_Theory/Cong.thy
-    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
-                Thomas M. Rasmussen, Jeremy Avigad
+    Author:     Christophe Tabacznyj
+    Author:     Lawrence C. Paulson
+    Author:     Amine Chaieb
+    Author:     Thomas M. Rasmussen
+    Author:     Jeremy Avigad
 
 Defines congruence (notation: [x = y] (mod z)) for natural numbers and
 integers.
@@ -26,12 +29,13 @@
 section \<open>Congruence\<close>
 
 theory Cong
-imports "~~/src/HOL/Computational_Algebra/Primes"
+  imports "~~/src/HOL/Computational_Algebra/Primes"
 begin
 
 subsection \<open>Turn off \<open>One_nat_def\<close>\<close>
 
-lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
+lemma power_eq_one_eq_nat [simp]: "x^m = 1 \<longleftrightarrow> m = 0 \<or> x = 1"
+  for x m :: nat
   by (induct m) auto
 
 declare mod_pos_pos_trivial [simp]
@@ -40,7 +44,7 @@
 subsection \<open>Main definitions\<close>
 
 class cong =
-  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))")
+  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ = _] '(()mod _'))")
 begin
 
 abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(()mod _'))")
@@ -48,26 +52,27 @@
 
 end
 
-(* definitions for the natural numbers *)
+
+subsubsection \<open>Definitions for the natural numbers\<close>
 
 instantiation nat :: cong
 begin
 
 definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "cong_nat x y m = ((x mod m) = (y mod m))"
+  where "cong_nat x y m \<longleftrightarrow> x mod m = y mod m"
 
 instance ..
 
 end
 
 
-(* definitions for the integers *)
+subsubsection \<open>Definitions for the integers\<close>
 
 instantiation int :: cong
 begin
 
 definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
-  where "cong_int x y m = ((x mod m) = (y mod m))"
+  where "cong_int x y m \<longleftrightarrow> x mod m = y mod m"
 
 instance ..
 
@@ -78,253 +83,259 @@
 
 
 lemma transfer_nat_int_cong:
-  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
-    ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
+  for x y m :: int
   unfolding cong_int_def cong_nat_def
   by (metis Divides.transfer_int_nat_functions(2) nat_0_le nat_mod_distrib)
 
 
-declare transfer_morphism_nat_int[transfer add return:
-    transfer_nat_int_cong]
+declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
 
-lemma transfer_int_nat_cong:
-  "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
-  apply (auto simp add: cong_int_def cong_nat_def)
-  apply (auto simp add: zmod_int [symmetric])
-  done
+lemma transfer_int_nat_cong: "[int x = int y] (mod (int m)) = [x = y] (mod m)"
+  by (auto simp add: cong_int_def cong_nat_def) (auto simp add: zmod_int [symmetric])
 
-declare transfer_morphism_int_nat[transfer add return:
-    transfer_int_nat_cong]
+declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_cong]
 
 
 subsection \<open>Congruence\<close>
 
 (* was zcong_0, etc. *)
-lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
-  unfolding cong_nat_def by auto
+lemma cong_0_nat [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b"
+  for a b :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
-  unfolding cong_int_def by auto
+lemma cong_0_int [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b"
+  for a b :: int
+  by (auto simp: cong_int_def)
 
-lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
-  unfolding cong_nat_def by auto
+lemma cong_1_nat [simp, presburger]: "[a = b] (mod 1)"
+  for a b :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
-  unfolding cong_nat_def by auto
+lemma cong_Suc_0_nat [simp, presburger]: "[a = b] (mod Suc 0)"
+  for a b :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
-  unfolding cong_int_def by auto
+lemma cong_1_int [simp, presburger]: "[a = b] (mod 1)"
+  for a b :: int
+  by (auto simp: cong_int_def)
 
-lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
-  unfolding cong_nat_def by auto
+lemma cong_refl_nat [simp]: "[k = k] (mod m)"
+  for k :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
-  unfolding cong_int_def by auto
+lemma cong_refl_int [simp]: "[k = k] (mod m)"
+  for k :: int
+  by (auto simp: cong_int_def)
 
-lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
-  unfolding cong_nat_def by auto
+lemma cong_sym_nat: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+  for a b :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
-  unfolding cong_int_def by auto
+lemma cong_sym_int: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+  for a b :: int
+  by (auto simp: cong_int_def)
 
-lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
-  unfolding cong_nat_def by auto
+lemma cong_sym_eq_nat: "[a = b] (mod m) = [b = a] (mod m)"
+  for a b :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
-  unfolding cong_int_def by auto
+lemma cong_sym_eq_int: "[a = b] (mod m) = [b = a] (mod m)"
+  for a b :: int
+  by (auto simp: cong_int_def)
 
-lemma cong_trans_nat [trans]:
-    "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
-  unfolding cong_nat_def by auto
+lemma cong_trans_nat [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
+  for a b c :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_trans_int [trans]:
-    "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
-  unfolding cong_int_def by auto
+lemma cong_trans_int [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
+  for a b c :: int
+  by (auto simp: cong_int_def)
 
-lemma cong_add_nat:
-    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
-  unfolding cong_nat_def  by (metis mod_add_cong)
+lemma cong_add_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
+  for a b c :: nat
+  unfolding cong_nat_def by (metis mod_add_cong)
 
-lemma cong_add_int:
-    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
-  unfolding cong_int_def  by (metis mod_add_cong)
+lemma cong_add_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
+  for a b c :: int
+  unfolding cong_int_def by (metis mod_add_cong)
 
-lemma cong_diff_int:
-    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
-  unfolding cong_int_def  by (metis mod_diff_cong) 
+lemma cong_diff_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
+  for a b c :: int
+  unfolding cong_int_def by (metis mod_diff_cong)
 
 lemma cong_diff_aux_int:
-  "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
-   (a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
+  "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
+    a \<ge> c \<Longrightarrow> b \<ge> d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
+  for a b c d :: int
   by (metis cong_diff_int tsub_eq)
 
 lemma cong_diff_nat:
-  assumes"[a = b] (mod m)" "[c = d] (mod m)" "(a::nat) >= c" "b >= d" 
+  fixes a b c d :: nat
+  assumes "[a = b] (mod m)" "[c = d] (mod m)" "a \<ge> c" "b \<ge> d"
   shows "[a - c = b - d] (mod m)"
   using assms by (rule cong_diff_aux_int [transferred])
 
-lemma cong_mult_nat:
-    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
-  unfolding cong_nat_def  by (metis mod_mult_cong) 
+lemma cong_mult_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
+  for a b c d :: nat
+  unfolding cong_nat_def  by (metis mod_mult_cong)
 
-lemma cong_mult_int:
-    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
-  unfolding cong_int_def  by (metis mod_mult_cong) 
-
-lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
-  by (induct k) (auto simp add: cong_mult_nat)
+lemma cong_mult_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
+  for a b c d :: int
+  unfolding cong_int_def  by (metis mod_mult_cong)
 
-lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
-  by (induct k) (auto simp add: cong_mult_int)
+lemma cong_exp_nat: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+  for x y :: nat
+  by (induct k) (auto simp: cong_mult_nat)
 
-lemma cong_sum_nat [rule_format]:
-    "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
-      [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply (auto intro: cong_add_nat)
-  done
+lemma cong_exp_int: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+  for x y :: int
+  by (induct k) (auto simp: cong_mult_int)
 
-lemma cong_sum_int [rule_format]:
-    "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
-      [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply (auto intro: cong_add_int)
-  done
+lemma cong_sum_nat: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
+  for f g :: "'a \<Rightarrow> nat"
+  by (induct A rule: infinite_finite_induct) (auto intro: cong_add_nat)
+
+lemma cong_sum_int: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
+  for f g :: "'a \<Rightarrow> int"
+  by (induct A rule: infinite_finite_induct) (auto intro: cong_add_int)
 
-lemma cong_prod_nat [rule_format]:
-    "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
-      [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply (auto intro: cong_mult_nat)
-  done
+lemma cong_prod_nat: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
+  for f g :: "'a \<Rightarrow> nat"
+  by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_nat)
 
-lemma cong_prod_int [rule_format]:
-    "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
-      [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply (auto intro: cong_mult_int)
-  done
+lemma cong_prod_int: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
+  for f g :: "'a \<Rightarrow> int"
+  by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_int)
 
-lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+lemma cong_scalar_nat: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+  for a b k :: nat
   by (rule cong_mult_nat) simp_all
 
-lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+lemma cong_scalar_int: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+  for a b k :: int
   by (rule cong_mult_int) simp_all
 
-lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+lemma cong_scalar2_nat: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+  for a b k :: nat
   by (rule cong_mult_nat) simp_all
 
-lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+lemma cong_scalar2_int: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+  for a b k :: int
   by (rule cong_mult_int) simp_all
 
-lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
-  unfolding cong_nat_def by auto
+lemma cong_mult_self_nat: "[a * m = 0] (mod m)"
+  for a m :: nat
+  by (auto simp: cong_nat_def)
 
-lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
-  unfolding cong_int_def by auto
+lemma cong_mult_self_int: "[a * m = 0] (mod m)"
+  for a m :: int
+  by (auto simp: cong_int_def)
 
-lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
+lemma cong_eq_diff_cong_0_int: "[a = b] (mod m) = [a - b = 0] (mod m)"
+  for a b :: int
   by (metis cong_add_int cong_diff_int cong_refl_int diff_add_cancel diff_self)
 
-lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
-    [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
+lemma cong_eq_diff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [a = b] (mod m) = [tsub a b = 0] (mod m)"
+  for a b :: int
   by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
 
 lemma cong_eq_diff_cong_0_nat:
-  assumes "(a::nat) >= b"
+  fixes a b :: nat
+  assumes "a \<ge> b"
   shows "[a = b] (mod m) = [a - b = 0] (mod m)"
   using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
 
 lemma cong_diff_cong_0'_nat:
-  "[(x::nat) = y] (mod n) \<longleftrightarrow>
-    (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
+  "[x = y] (mod n) \<longleftrightarrow> (if x \<le> y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
+  for x y :: nat
   by (metis cong_eq_diff_cong_0_nat cong_sym_nat nat_le_linear)
 
-lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
+lemma cong_altdef_nat: "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+  for a b :: nat
   apply (subst cong_eq_diff_cong_0_nat, assumption)
   apply (unfold cong_nat_def)
   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   done
 
-lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
+lemma cong_altdef_int: "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+  for a b :: int
   by (metis cong_int_def mod_eq_dvd_iff)
 
-lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
+lemma cong_abs_int: "[x = y] (mod abs m) \<longleftrightarrow> [x = y] (mod m)"
+  for x y :: int
   by (simp add: cong_altdef_int)
 
 lemma cong_square_int:
-  fixes a::int
-  shows "\<lbrakk> prime p; 0 < a; [a * a = 1] (mod p) \<rbrakk>
-    \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
+  "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
+  for a :: int
   apply (simp only: cong_altdef_int)
   apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
   apply (auto simp add: field_simps)
   done
 
-lemma cong_mult_rcancel_int:
-    "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+lemma cong_mult_rcancel_int: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+  for a k m :: int
   by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
 
-lemma cong_mult_rcancel_nat:
-    "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+lemma cong_mult_rcancel_nat: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+  for a k m :: nat
   by (metis cong_mult_rcancel_int [transferred])
 
-lemma cong_mult_lcancel_nat:
-    "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
+lemma cong_mult_lcancel_nat: "coprime k m \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
+  for a k m :: nat
   by (simp add: mult.commute cong_mult_rcancel_nat)
 
-lemma cong_mult_lcancel_int:
-    "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
+lemma cong_mult_lcancel_int: "coprime k m \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
+  for a k m :: int
   by (simp add: mult.commute cong_mult_rcancel_int)
 
 (* was zcong_zgcd_zmult_zmod *)
 lemma coprime_cong_mult_int:
-  "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
-    \<Longrightarrow> [a = b] (mod m * n)"
-by (metis divides_mult cong_altdef_int)
+  "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
+  for a b :: int
+  by (metis divides_mult cong_altdef_int)
 
 lemma coprime_cong_mult_nat:
-  assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
-  shows "[a = b] (mod m * n)"
-  by (metis assms coprime_cong_mult_int [transferred])
+  "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
+  for a b :: nat
+  by (metis coprime_cong_mult_int [transferred])
 
-lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
-    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+lemma cong_less_imp_eq_nat: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+  for a b :: nat
   by (auto simp add: cong_nat_def)
 
-lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
-    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+lemma cong_less_imp_eq_int: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+  for a b :: int
   by (auto simp add: cong_int_def)
 
-lemma cong_less_unique_nat:
-    "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+  for a m :: nat
   by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial)
 
-lemma cong_less_unique_int:
-    "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+  for a m :: int
   by (auto simp: cong_int_def)  (metis mod_mod_trivial pos_mod_conj)
 
-lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
+lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
+  for a b :: int
   apply (auto simp add: cong_altdef_int dvd_def)
   apply (rule_tac [!] x = "-k" in exI, auto)
   done
 
-lemma cong_iff_lin_nat: 
-   "([(a::nat) = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" (is "?lhs = ?rhs")
-proof (rule iffI)
-  assume eqm: ?lhs
+lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
+  (is "?lhs = ?rhs")
+  for a b :: nat
+proof
+  assume ?lhs
   show ?rhs
   proof (cases "b \<le> a")
     case True
-    then show ?rhs using eqm
+    with \<open>?lhs\<close> show ?rhs
       by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute)
   next
     case False
-    then show ?rhs using eqm 
+    with \<open>?lhs\<close> show ?rhs
       apply (subst (asm) cong_sym_eq_nat)
       apply (auto simp: cong_altdef_nat)
       apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
@@ -336,26 +347,32 @@
     by (metis cong_nat_def mod_mult_self2 mult.commute)
 qed
 
-lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+  for a b :: int
   by (metis cong_int_def gcd_red_int)
 
-lemma cong_gcd_eq_nat:
-    "[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
+lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+  for a b :: nat
   by (metis cong_gcd_eq_int [transferred])
 
-lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
+lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
+  for a b :: nat
   by (auto simp add: cong_gcd_eq_nat)
 
-lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
+lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
+  for a b :: int
   by (auto simp add: cong_gcd_eq_int)
 
-lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
+lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
+  for a b :: nat
   by (auto simp add: cong_nat_def)
 
-lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
+lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
+  for a b :: int
   by (auto simp add: cong_int_def)
 
-lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
+lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
+  for a b :: int
   by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
 
 (*
@@ -375,115 +392,158 @@
   done
 *)
 
-lemma cong_add_lcancel_nat:
-    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  for a x y :: nat
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_lcancel_int:
-    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  for a x y :: int
   by (simp add: cong_iff_lin_int)
 
-lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  for a x y :: nat
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  for a x y :: int
   by (simp add: cong_iff_lin_int)
 
-lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
-  by (simp add: cong_iff_lin_nat)
-
-lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
-  by (simp add: cong_iff_lin_int)
-
-lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  for a x :: nat
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+lemma cong_add_lcancel_0_int: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  for a x :: int
   by (simp add: cong_iff_lin_int)
 
-lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
-    [x = y] (mod n)"
+lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  for a x :: nat
+  by (simp add: cong_iff_lin_nat)
+
+lemma cong_add_rcancel_0_int: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  for a x :: int
+  by (simp add: cong_iff_lin_int)
+
+lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
+  for x y :: nat
   apply (auto simp add: cong_iff_lin_nat dvd_def)
-  apply (rule_tac x="k1 * k" in exI)
-  apply (rule_tac x="k2 * k" in exI)
+  apply (rule_tac x= "k1 * k" in exI)
+  apply (rule_tac x= "k2 * k" in exI)
   apply (simp add: field_simps)
   done
 
-lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
+lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
+  for x y :: int
   by (auto simp add: cong_altdef_int dvd_def)
 
-lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
-  unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
+lemma cong_dvd_eq_nat: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
+  for x y :: nat
+  by (auto simp: cong_nat_def dvd_eq_mod_eq_0)
 
-lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
-  unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
+lemma cong_dvd_eq_int: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
+  for x y :: int
+  by (auto simp: cong_int_def dvd_eq_mod_eq_0)
 
-lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+lemma cong_mod_nat: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
+  for a n :: nat
   by (simp add: cong_nat_def)
 
-lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+lemma cong_mod_int: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
+  for a n :: int
   by (simp add: cong_int_def)
 
-lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
-    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
+lemma mod_mult_cong_nat: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
+  for a b :: nat
   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
 
-lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
+lemma neg_cong_int: "[a = b] (mod m) \<longleftrightarrow> [- a = - b] (mod m)"
+  for a b :: int
   by (metis cong_int_def minus_minus mod_minus_cong)
 
-lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
+lemma cong_modulus_neg_int: "[a = b] (mod m) \<longleftrightarrow> [a = b] (mod - m)"
+  for a b :: int
   by (auto simp add: cong_altdef_int)
 
-lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
-    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
-  apply (cases "b > 0", simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
-  apply (subst (1 2) cong_modulus_neg_int)
-  apply (unfold cong_int_def)
-  apply (subgoal_tac "a * b = (-a * -b)")
-  apply (erule ssubst)
-  apply (subst zmod_zmult2_eq)
-  apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
-  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+
+lemma mod_mult_cong_int: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
+  for a b :: int
+proof (cases "b > 0")
+  case True
+  then show ?thesis
+    by (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
+next
+  case False
+  then show ?thesis
+    apply (subst (1 2) cong_modulus_neg_int)
+    apply (unfold cong_int_def)
+    apply (subgoal_tac "a * b = (- a * - b)")
+     apply (erule ssubst)
+     apply (subst zmod_zmult2_eq)
+      apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
+     apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+
+    done
+qed
+
+lemma cong_to_1_nat:
+  fixes a :: nat
+  assumes "[a = 1] (mod n)"
+  shows "n dvd (a - 1)"
+proof (cases "a = 0")
+  case True
+  then show ?thesis by force
+next
+  case False
+  with assms show ?thesis by (metis cong_altdef_nat leI less_one)
+qed
+
+lemma cong_0_1_nat': "[0 = Suc 0] (mod n) \<longleftrightarrow> n = Suc 0"
+  by (auto simp: cong_nat_def)
+
+lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1"
+  for n :: nat
+  by (auto simp: cong_nat_def)
+
+lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1"
+  for n :: int
+  by (auto simp: cong_int_def zmult_eq_1_iff)
+
+lemma cong_to_1'_nat: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
+  for a :: nat
+  by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat
+      dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if)
+
+lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
+  for x y :: nat
+  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
+
+lemma cong_solve_nat:
+  fixes a :: nat
+  assumes "a \<noteq> 0"
+  shows "\<exists>x. [a * x = gcd a n] (mod n)"
+proof (cases "n = 0")
+  case True
+  then show ?thesis by force
+next
+  case False
+  then show ?thesis
+    using bezout_nat [of a n, OF \<open>a \<noteq> 0\<close>]
+    by auto (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute)
+qed
+
+lemma cong_solve_int: "a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)"
+  for a :: int
+  apply (cases "n = 0")
+   apply (cases "a \<ge> 0")
+    apply auto
+   apply (rule_tac x = "-1" in exI)
+   apply auto
+  apply (insert bezout_int [of a n], auto)
+  apply (metis cong_iff_lin_int mult.commute)
   done
 
-lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
-  apply (cases "a = 0", force)
-  by (metis cong_altdef_nat leI less_one)
-
-lemma cong_0_1_nat': "[(0::nat) = Suc 0] (mod n) = (n = Suc 0)"
-  unfolding cong_nat_def by auto
-
-lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
-  unfolding cong_nat_def by auto
-
-lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
-  unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
-
-lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
-    a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
-by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if)
-
-lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
-  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
-
-lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
-  apply (cases "n = 0")
-  apply force
-  apply (frule bezout_nat [of a n], auto)
-  by (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute)
-
-lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
-  apply (cases "n = 0")
-  apply (cases "a \<ge> 0")
-  apply auto
-  apply (rule_tac x = "-1" in exI)
-  apply auto
-  apply (insert bezout_int [of a n], auto)
-  by (metis cong_iff_lin_int mult.commute)
-
 lemma cong_solve_dvd_nat:
-  assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
-  shows "EX x. [a * x = d] (mod n)"
+  fixes a :: nat
+  assumes a: "a \<noteq> 0" and b: "gcd a n dvd d"
+  shows "\<exists>x. [a * x = d] (mod n)"
 proof -
   from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
     by auto
@@ -499,7 +559,7 @@
 
 lemma cong_solve_dvd_int:
   assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
-  shows "EX x. [a * x = d] (mod n)"
+  shows "\<exists>x. [a * x = d] (mod n)"
 proof -
   from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
     by auto
@@ -513,54 +573,62 @@
     by auto
 qed
 
-lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
-  apply (cases "a = 0")
-  apply force
-  apply (metis cong_solve_nat)
-  done
+lemma cong_solve_coprime_nat:
+  fixes a :: nat
+  assumes "coprime a n"
+  shows "\<exists>x. [a * x = 1] (mod n)"
+proof (cases "a = 0")
+  case True
+  with assms show ?thesis by force
+next
+  case False
+  with assms show ?thesis by (metis cong_solve_nat)
+qed
 
-lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
+lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
   apply (cases "a = 0")
-  apply auto
-  apply (cases "n \<ge> 0")
-  apply auto
+   apply auto
+   apply (cases "n \<ge> 0")
+    apply auto
   apply (metis cong_solve_int)
   done
 
 lemma coprime_iff_invertible_nat:
-  "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
+  "m > 0 \<Longrightarrow> coprime a m = (\<exists>x. [a * x = Suc 0] (mod m))"
   by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0)
-  
-lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
+
+lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
+  for m :: int
   apply (auto intro: cong_solve_coprime_int)
   apply (metis cong_int_def coprime_mul_eq gcd_1_int gcd.commute gcd_red_int)
   done
 
-lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m =
-    (EX x. 0 \<le> x & x < m & [a * x = Suc 0] (mod m))"
+lemma coprime_iff_invertible'_nat:
+  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
   apply (subst coprime_iff_invertible_nat)
-  apply auto
+   apply auto
   apply (auto simp add: cong_nat_def)
   apply (metis mod_less_divisor mod_mult_right_eq)
   done
 
-lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
-    (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
+lemma coprime_iff_invertible'_int:
+  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))"
+  for m :: int
   apply (subst coprime_iff_invertible_int)
-  apply (auto simp add: cong_int_def)
+   apply (auto simp add: cong_int_def)
   apply (metis mod_mult_right_eq pos_mod_conj)
   done
 
-lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
-    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
+lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
+  for x y :: nat
   apply (cases "y \<le> x")
   apply (metis cong_altdef_nat lcm_least)
   apply (meson cong_altdef_nat cong_sym_nat lcm_least_iff nat_le_linear)
   done
 
-lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
-    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
-  by (auto simp add: cong_altdef_int lcm_least) [1]
+lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
+  for x y :: int
+  by (auto simp add: cong_altdef_int lcm_least)
 
 lemma cong_cong_prod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
     (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
@@ -581,162 +649,168 @@
   done
 
 lemma binary_chinese_remainder_aux_nat:
-  assumes a: "coprime (m1::nat) m2"
-  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
-    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
+  fixes m1 m2 :: nat
+  assumes a: "coprime m1 m2"
+  shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
 proof -
-  from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+  from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
     by auto
   from a have b: "coprime m2 m1"
     by (subst gcd.commute)
-  from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+  from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
-    by (subst mult.commute, rule cong_mult_self_nat)
+    by (subst mult.commute) (rule cong_mult_self_nat)
   moreover have "[m2 * x2 = 0] (mod m2)"
-    by (subst mult.commute, rule cong_mult_self_nat)
-  moreover note one two
-  ultimately show ?thesis by blast
+    by (subst mult.commute) (rule cong_mult_self_nat)
+  ultimately show ?thesis
+    using 1 2 by blast
 qed
 
 lemma binary_chinese_remainder_aux_int:
-  assumes a: "coprime (m1::int) m2"
-  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
-    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
+  fixes m1 m2 :: int
+  assumes a: "coprime m1 m2"
+  shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
 proof -
-  from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+  from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
     by auto
   from a have b: "coprime m2 m1"
     by (subst gcd.commute)
-  from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+  from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
-    by (subst mult.commute, rule cong_mult_self_int)
+    by (subst mult.commute) (rule cong_mult_self_int)
   moreover have "[m2 * x2 = 0] (mod m2)"
-    by (subst mult.commute, rule cong_mult_self_int)
-  moreover note one two
-  ultimately show ?thesis by blast
+    by (subst mult.commute) (rule cong_mult_self_int)
+  ultimately show ?thesis
+    using 1 2 by blast
 qed
 
 lemma binary_chinese_remainder_nat:
-  assumes a: "coprime (m1::nat) m2"
-  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+  fixes m1 m2 :: nat
+  assumes a: "coprime m1 m2"
+  shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
   from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
-      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
-            "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
+    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
+      and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
     by blast
   let ?x = "u1 * b1 + u2 * b2"
   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
     apply (rule cong_add_nat)
-    apply (rule cong_scalar2_nat)
-    apply (rule \<open>[b1 = 1] (mod m1)\<close>)
+     apply (rule cong_scalar2_nat)
+     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
     apply (rule cong_scalar2_nat)
     apply (rule \<open>[b2 = 0] (mod m1)\<close>)
     done
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     apply (rule cong_add_nat)
-    apply (rule cong_scalar2_nat)
-    apply (rule \<open>[b1 = 0] (mod m2)\<close>)
+     apply (rule cong_scalar2_nat)
+     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
     apply (rule cong_scalar2_nat)
     apply (rule \<open>[b2 = 1] (mod m2)\<close>)
     done
-  then have "[?x = u2] (mod m2)" by simp
-  with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
+  then have "[?x = u2] (mod m2)"
+    by simp
+  with \<open>[?x = u1] (mod m1)\<close> show ?thesis
+    by blast
 qed
 
 lemma binary_chinese_remainder_int:
-  assumes a: "coprime (m1::int) m2"
-  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+  fixes m1 m2 :: int
+  assumes a: "coprime m1 m2"
+  shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
   from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
-    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
-          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
+    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
+      and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
     by blast
   let ?x = "u1 * b1 + u2 * b2"
   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
     apply (rule cong_add_int)
-    apply (rule cong_scalar2_int)
-    apply (rule \<open>[b1 = 1] (mod m1)\<close>)
+     apply (rule cong_scalar2_int)
+     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
     apply (rule cong_scalar2_int)
     apply (rule \<open>[b2 = 0] (mod m1)\<close>)
     done
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     apply (rule cong_add_int)
-    apply (rule cong_scalar2_int)
-    apply (rule \<open>[b1 = 0] (mod m2)\<close>)
+     apply (rule cong_scalar2_int)
+     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
     apply (rule cong_scalar2_int)
     apply (rule \<open>[b2 = 1] (mod m2)\<close>)
     done
   then have "[?x = u2] (mod m2)" by simp
-  with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
+  with \<open>[?x = u1] (mod m1)\<close> show ?thesis
+    by blast
 qed
 
-lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
-    [x = y] (mod m)"
+lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
+  for x y :: nat
   apply (cases "y \<le> x")
-  apply (simp add: cong_altdef_nat)
-  apply (erule dvd_mult_left)
+   apply (simp add: cong_altdef_nat)
+   apply (erule dvd_mult_left)
   apply (rule cong_sym_nat)
   apply (subst (asm) cong_sym_eq_nat)
   apply (simp add: cong_altdef_nat)
   apply (erule dvd_mult_left)
   done
 
-lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
-    [x = y] (mod m)"
+lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
+  for x y :: int
   apply (simp add: cong_altdef_int)
   apply (erule dvd_mult_left)
   done
 
-lemma cong_less_modulus_unique_nat:
-    "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
+lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
+  for x y :: nat
   by (simp add: cong_nat_def)
 
 lemma binary_chinese_remainder_unique_nat:
-  assumes a: "coprime (m1::nat) m2"
+  fixes m1 m2 :: nat
+  assumes a: "coprime m1 m2"
     and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
-  from binary_chinese_remainder_nat [OF a] obtain y where
-      "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
+  from binary_chinese_remainder_nat [OF a] obtain y
+    where "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
     by blast
   let ?x = "y mod (m1 * m2)"
   from nz have less: "?x < m1 * m2"
     by auto
-  have one: "[?x = u1] (mod m1)"
+  have 1: "[?x = u1] (mod m1)"
     apply (rule cong_trans_nat)
-    prefer 2
-    apply (rule \<open>[y = u1] (mod m1)\<close>)
+     prefer 2
+     apply (rule \<open>[y = u1] (mod m1)\<close>)
     apply (rule cong_modulus_mult_nat)
     apply (rule cong_mod_nat)
     using nz apply auto
     done
-  have two: "[?x = u2] (mod m2)"
+  have 2: "[?x = u2] (mod m2)"
     apply (rule cong_trans_nat)
-    prefer 2
-    apply (rule \<open>[y = u2] (mod m2)\<close>)
+     prefer 2
+     apply (rule \<open>[y = u2] (mod m2)\<close>)
     apply (subst mult.commute)
     apply (rule cong_modulus_mult_nat)
     apply (rule cong_mod_nat)
     using nz apply auto
     done
-  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
+  have "\<forall>z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
   proof clarify
     fix z
     assume "z < m1 * m2"
     assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
     have "[?x = z] (mod m1)"
       apply (rule cong_trans_nat)
-      apply (rule \<open>[?x = u1] (mod m1)\<close>)
+       apply (rule \<open>[?x = u1] (mod m1)\<close>)
       apply (rule cong_sym_nat)
       apply (rule \<open>[z = u1] (mod m1)\<close>)
       done
     moreover have "[?x = z] (mod m2)"
       apply (rule cong_trans_nat)
-      apply (rule \<open>[?x = u2] (mod m2)\<close>)
+       apply (rule \<open>[?x = u2] (mod m2)\<close>)
       apply (rule cong_sym_nat)
       apply (rule \<open>[z = u2] (mod m2)\<close>)
       done
@@ -744,32 +818,30 @@
       by (auto intro: coprime_cong_mult_nat a)
     with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
       apply (intro cong_less_modulus_unique_nat)
-      apply (auto, erule cong_sym_nat)
+        apply (auto, erule cong_sym_nat)
       done
   qed
-  with less one two show ?thesis by auto
+  with less 1 2 show ?thesis by auto
  qed
 
 lemma chinese_remainder_aux_nat:
   fixes A :: "'a set"
     and m :: "'a \<Rightarrow> nat"
   assumes fin: "finite A"
-    and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
-  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
+    and cop: "\<forall>i \<in> A. (\<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  shows "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
 proof (rule finite_set_choice, rule fin, rule ballI)
   fix i
-  assume "i : A"
+  assume "i \<in> A"
   with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
-    by (intro prod_coprime, auto)
-  then have "EX x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
+    by (intro prod_coprime) auto
+  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
     by (elim cong_solve_coprime_nat)
   then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
     by auto
-  moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0]
-    (mod (\<Prod>j \<in> A - {i}. m j))"
+  moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
     by (subst mult.commute, rule cong_mult_self_nat)
-  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
-      (mod prod m (A - {i}))"
+  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
     by blast
 qed
 
@@ -778,37 +850,35 @@
     and m :: "'a \<Rightarrow> nat"
     and u :: "'a \<Rightarrow> nat"
   assumes fin: "finite A"
-    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
-  shows "EX x. (ALL i:A. [x = u i] (mod m i))"
+    and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)"
+  shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)"
 proof -
-  from chinese_remainder_aux_nat [OF fin cop] obtain b where
-    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
-      [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
+  from chinese_remainder_aux_nat [OF fin cop]
+  obtain b where b: "\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
     by blast
   let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
-  show "?thesis"
+  show ?thesis
   proof (rule exI, clarify)
     fix i
-    assume a: "i : A"
+    assume a: "i \<in> A"
     show "[?x = u i] (mod m i)"
     proof -
-      from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) +
-          (\<Sum>j \<in> A - {i}. u j * b j)"
-        by (subst sum.union_disjoint [symmetric], auto intro: sum.cong)
+      from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) + (\<Sum>j \<in> A - {i}. u j * b j)"
+        by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong)
       then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)"
         by auto
       also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
                   u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
         apply (rule cong_add_nat)
-        apply (rule cong_scalar2_nat)
-        using bprop a apply blast
+         apply (rule cong_scalar2_nat)
+        using b a apply blast
         apply (rule cong_sum_nat)
         apply (rule cong_scalar2_nat)
-        using bprop apply auto
+        using b apply auto
         apply (rule cong_dvd_modulus_nat)
-        apply (drule (1) bspec)
-        apply (erule conjE)
-        apply assumption
+         apply (drule (1) bspec)
+         apply (erule conjE)
+         apply assumption
         apply rule
         using fin a apply auto
         done
@@ -833,36 +903,35 @@
     and u :: "'a \<Rightarrow> nat"
   assumes fin: "finite A"
     and nz: "\<forall>i\<in>A. m i \<noteq> 0"
-    and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+    and cop: "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)"
   shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
 proof -
   from chinese_remainder_nat [OF fin cop]
-  obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
+  obtain y where one: "(\<forall>i\<in>A. [y = u i] (mod m i))"
     by blast
   let ?x = "y mod (\<Prod>i\<in>A. m i)"
   from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0"
     by auto
   then have less: "?x < (\<Prod>i\<in>A. m i)"
     by auto
-  have cong: "ALL i:A. [?x = u i] (mod m i)"
+  have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)"
     apply auto
     apply (rule cong_trans_nat)
-    prefer 2
+     prefer 2
     using one apply auto
     apply (rule cong_dvd_modulus_nat)
-    apply (rule cong_mod_nat)
+     apply (rule cong_mod_nat)
     using prodnz apply auto
     apply rule
-    apply (rule fin)
+     apply (rule fin)
     apply assumption
     done
-  have unique: "ALL z. z < (\<Prod>i\<in>A. m i) \<and>
-      (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
-  proof (clarify)
+  have unique: "\<forall>z. z < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
+  proof clarify
     fix z
     assume zless: "z < (\<Prod>i\<in>A. m i)"
-    assume zcong: "(ALL i:A. [z = u i] (mod m i))"
-    have "ALL i:A. [?x = z] (mod m i)"
+    assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))"
+    have "\<forall>i\<in>A. [?x = z] (mod m i)"
       apply clarify
       apply (rule cong_trans_nat)
       using cong apply (erule bspec)
@@ -871,14 +940,16 @@
       done
     with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
       apply (intro coprime_cong_prod_nat)
-      apply auto
+        apply auto
       done
     with zless less show "z = ?x"
       apply (intro cong_less_modulus_unique_nat)
-      apply (auto, erule cong_sym_nat)
+        apply auto
+      apply (erule cong_sym_nat)
       done
   qed
-  from less cong unique show ?thesis by blast
+  from less cong unique show ?thesis
+    by blast
 qed
 
 end
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -40,7 +40,7 @@
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
-  val group_snapshot: group -> task list
+  val snapshot: group list -> task list
   val shutdown: unit -> unit
 end;
 
@@ -638,11 +638,11 @@
 fun fulfill x res = fulfill_result x (Exn.Res res);
 
 
-(* group snapshot *)
+(* snapshot: current tasks of groups *)
 
-fun group_snapshot group =
-  SYNCHRONIZED "group_snapshot" (fn () =>
-    Task_Queue.group_tasks (! queue) group);
+fun snapshot groups =
+  SYNCHRONIZED "snapshot" (fn () =>
+    Task_Queue.group_tasks (! queue) groups);
 
 
 (* shutdown *)
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -29,7 +29,7 @@
   val waiting: task -> task list -> (unit -> 'a) -> 'a
   type queue
   val empty: queue
-  val group_tasks: queue -> group -> task list
+  val group_tasks: queue -> group list -> task list
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
@@ -222,7 +222,11 @@
 fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent};
 val empty = make_queue Inttab.empty Task_Graph.empty 0;
 
-fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
+fun group_tasks (Queue {groups, ...}) gs =
+  fold (fn g => fn tasks => Tasks.merge (op =) (tasks, get_tasks groups (group_id g)))
+    gs Tasks.empty
+  |> Tasks.keys;
+
 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
 
 
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -12,6 +12,7 @@
   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     blob list * int -> Token.T list -> Toplevel.transition
   type eval
+  val eval_exec_id: eval -> Document_ID.exec
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 08 22:40:05 2017 +0200
@@ -213,6 +213,9 @@
     results: Results = Results.empty,
     markups: Markups = Markups.empty)
   {
+    lazy val consolidated: Boolean =
+      status.exists(markup => markup.name == Markup.CONSOLIDATED)
+
     lazy val protocol_status: Protocol.Status =
     {
       val warnings =
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -24,6 +24,7 @@
   val command_exec: state -> string -> Document_ID.command -> Command.exec option
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
+  val consolidate_execution: state -> unit
   val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
     Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
@@ -59,16 +60,17 @@
   keywords: Keyword.keywords option,  (*outer syntax keywords*)
   perspective: perspective,  (*command perspective*)
   entries: Command.exec option Entries.T,  (*command entries with executions*)
-  result: Command.eval option}  (*result of last execution*)
+  result: Command.eval option,  (*result of last execution*)
+  consolidated: unit lazy}  (*consolidation status of eval forks*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (header, keywords, perspective, entries, result) =
+fun make_node (header, keywords, perspective, entries, result, consolidated) =
   Node {header = header, keywords = keywords, perspective = perspective,
-    entries = entries, result = result};
+    entries = entries, result = result, consolidated = consolidated};
 
-fun map_node f (Node {header, keywords, perspective, entries, result}) =
-  make_node (f (header, keywords, perspective, entries, result));
+fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) =
+  make_node (f (header, keywords, perspective, entries, result, consolidated));
 
 fun make_perspective (required, command_ids, overlays) : perspective =
  {required = required,
@@ -80,7 +82,7 @@
   {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
 val no_perspective = make_perspective (false, [], []);
 
-val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
+val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
 
 fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
@@ -88,12 +90,13 @@
   is_none visible_last andalso
   Inttab.is_empty overlays;
 
-fun is_empty_node (Node {header, keywords, perspective, entries, result}) =
+fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
   header = no_header andalso
   is_none keywords andalso
   is_no_perspective perspective andalso
   Entries.is_empty entries andalso
-  is_none result;
+  is_none result andalso
+  Lazy.is_finished consolidated;
 
 
 (* basic components *)
@@ -104,14 +107,15 @@
   | _ => Path.current);
 
 fun set_header master header errors =
-  map_node (fn (_, keywords, perspective, entries, result) =>
-    ({master = master, header = header, errors = errors}, keywords, perspective, entries, result));
+  map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
+    ({master = master, header = header, errors = errors},
+      keywords, perspective, entries, result, consolidated));
 
 fun get_header (Node {header, ...}) = header;
 
 fun set_keywords keywords =
-  map_node (fn (header, _, perspective, entries, result) =>
-    (header, keywords, perspective, entries, result));
+  map_node (fn (header, _, perspective, entries, result, consolidated) =>
+    (header, keywords, perspective, entries, result, consolidated));
 
 fun get_keywords (Node {keywords, ...}) = keywords;
 
@@ -134,8 +138,8 @@
 fun get_perspective (Node {perspective, ...}) = perspective;
 
 fun set_perspective args =
-  map_node (fn (header, keywords, _, entries, result) =>
-    (header, keywords, make_perspective args, entries, result));
+  map_node (fn (header, keywords, _, entries, result, consolidated) =>
+    (header, keywords, make_perspective args, entries, result, consolidated));
 
 val required_node = #required o get_perspective;
 val visible_command = Inttab.defined o #visible o get_perspective;
@@ -144,8 +148,8 @@
 val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
-  map_node (fn (header, keywords, perspective, entries, result) =>
-    (header, keywords, perspective, f entries, result));
+  map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
+    (header, keywords, perspective, f entries, result, consolidated));
 
 fun get_entries (Node {entries, ...}) = entries;
 
@@ -158,14 +162,8 @@
 fun get_result (Node {result, ...}) = result;
 
 fun set_result result =
-  map_node (fn (header, keywords, perspective, entries, _) =>
-    (header, keywords, perspective, entries, result));
-
-fun changed_result node node' =
-  (case (get_result node, get_result node') of
-    (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
-  | (NONE, NONE) => false
-  | _ => true);
+  map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
+    (header, keywords, perspective, entries, result, consolidated));
 
 fun pending_result node =
   (case get_result node of
@@ -177,6 +175,35 @@
     SOME eval => Command.eval_finished eval
   | NONE => false);
 
+fun finished_result_theory node =
+  finished_result node andalso
+    let val st = Command.eval_result_state (the (get_result node))
+    in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end;
+
+val reset_consolidated =
+  map_node (fn (header, keywords, perspective, entries, result, _) =>
+    (header, keywords, perspective, entries, result, Lazy.lazy I));
+
+fun check_consolidated (node as Node {consolidated, ...}) =
+  Lazy.is_finished consolidated orelse
+  finished_result_theory node andalso
+    let
+      val result_id = Command.eval_exec_id (the (get_result node));
+      val eval_ids =
+        iterate_entries (fn (_, opt_exec) => fn eval_ids =>
+          (case opt_exec of
+            SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
+          | NONE => NONE)) node [];
+    in
+      (case Execution.snapshot eval_ids of
+        [] =>
+         (Lazy.force consolidated;
+          Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
+            (fn () => Output.status (Markup.markup_only Markup.consolidated)) ();
+          true)
+      | _ => false)
+    end;
+
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
@@ -400,10 +427,16 @@
 
 val the_command_name = #1 oo the_command;
 
+
+(* execution *)
+
+fun get_execution (State {execution, ...}) = execution;
+fun get_execution_version state = the_version state (#version_id (get_execution state));
+
 fun command_exec state node_name command_id =
   let
-    val State {execution = {version_id, ...}, ...} = state;
-    val node = get_node (nodes_of (the_version state version_id)) node_name;
+    val version = get_execution_version state;
+    val node = get_node (nodes_of version) node_name;
   in the_entry node command_id end;
 
 end;
@@ -492,6 +525,10 @@
         {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
     in (versions, blobs, commands, execution') end));
 
+fun consolidate_execution state =
+  String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node))
+    (nodes_of (get_execution_version state)) ();
+
 
 
 (** document update **)
@@ -702,11 +739,13 @@
                         val removed = maps (removed_execs node0) assign_update;
                         val _ = List.app Execution.cancel removed;
 
+                        val result_changed =
+                          not (eq_option Command.eval_eq (get_result node0, result));
                         val node' = node
                           |> assign_update_apply assigned_execs
-                          |> set_result result;
+                          |> set_result result
+                          |> result_changed ? reset_consolidated;
                         val assigned_node = SOME (name, node');
-                        val result_changed = changed_result node0 node';
                       in ((removed, assign_update, assigned_node, result_changed), node') end
                     else (([], [], NONE, false), node)
                   end))))
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 08 22:40:05 2017 +0200
@@ -453,6 +453,7 @@
 
     def node_name: Node.Name
     def node: Node
+    def node_consolidated: Boolean
 
     def commands_loading: List[Command]
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
@@ -791,6 +792,11 @@
       } yield tree).toList
     }
 
+    def node_consolidated(version: Version, name: Node.Name): Boolean =
+      !name.is_theory ||
+        version.nodes(name).commands.reverse.iterator.
+          flatMap(command_states(version, _)).exists(_.consolidated)
+
     // persistent user-view
     def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
       : Snapshot =
@@ -835,6 +841,8 @@
         val node_name: Node.Name = name
         val node: Node = version.nodes(name)
 
+        def node_consolidated: Boolean = state.node_consolidated(version, node_name)
+
         val commands_loading: List[Command] =
           if (node_name.is_theory) Nil
           else version.nodes.commands_loading(node_name)
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/execution.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -80,8 +80,7 @@
   | NONE => []);
 
 fun snapshot exec_ids =
-  change_state_result (fn state =>
-    (maps Future.group_snapshot (maps (exec_groups state) exec_ids), state));
+  change_state_result (`(fn state => Future.snapshot (maps (exec_groups state) exec_ids)));
 
 fun join exec_ids =
   (case snapshot exec_ids of
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -159,6 +159,7 @@
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
+  val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
   val statusN: string val status: T
@@ -555,6 +556,7 @@
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
+val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 
 (* messages *)
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Aug 08 22:40:05 2017 +0200
@@ -423,6 +423,7 @@
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
+  val CONSOLIDATED = "consolidated"
 
 
   /* interactive documents */
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -58,6 +58,10 @@
       end);
 
 val _ =
+  Isabelle_Process.protocol_command "Document.consolidate_execution"
+    (fn [] => Document.consolidate_execution (Document.state ()));
+
+val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"
     (fn [] => Execution.discontinue ());
 
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 08 22:40:05 2017 +0200
@@ -352,6 +352,9 @@
 
   /* execution */
 
+  def consolidate_execution(): Unit =
+    protocol_command("Document.consolidate_execution")
+
   def discontinue_execution(): Unit =
     protocol_command("Document.discontinue_execution")
 
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Aug 08 22:40:05 2017 +0200
@@ -130,6 +130,7 @@
   /* dynamic session options */
 
   def output_delay: Time = session_options.seconds("editor_output_delay")
+  def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
   def prune_delay: Time = session_options.seconds("editor_prune_delay")
   def prune_size: Int = session_options.int("editor_prune_size")
   def syslog_limit: Int = session_options.int("editor_syslog_limit")
@@ -191,6 +192,7 @@
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Update_Options(options: Options)
+  private case object Consolidate_Execution
   private case object Prune_History
 
 
@@ -519,6 +521,9 @@
               prover.get.terminate
             }
 
+          case Consolidate_Execution =>
+            if (prover.defined) prover.get.consolidate_execution()
+
           case Prune_History =>
             if (prover.defined) {
               val old_versions = global_state.change_result(_.remove_versions(prune_size))
@@ -564,6 +569,28 @@
     }
   }
 
+  private val consolidator: Thread =
+    Standard_Thread.fork("Session.consolidator", daemon = true) {
+      try {
+        while (true) {
+          Thread.sleep(consolidate_delay.ms)
+
+          val state = global_state.value
+          state.stable_tip_version match {
+            case None =>
+            case Some(version) =>
+              val consolidated =
+                version.nodes.iterator.forall(
+                  { case (name, _) =>
+                      resources.session_base.loaded_theory(name) ||
+                      state.node_consolidated(version, name) })
+              if (!consolidated) manager.send(Consolidate_Execution)
+          }
+        }
+      }
+      catch { case Exn.Interrupt() => }
+    }
+
 
   /* main operations */
 
@@ -602,6 +629,8 @@
 
     change_parser.shutdown()
     change_buffer.shutdown()
+    consolidator.interrupt
+    consolidator.join
     manager.shutdown()
     dispatcher.shutdown()
 
diff -r 1b70820dc6ba -r 429b55991197 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 08 13:31:48 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 08 22:40:05 2017 +0200
@@ -156,8 +156,8 @@
   let
     val _ = Execution.join [exec_id];
     val res = Exn.capture Thm.consolidate_theory theory;
-    val errs = maps Task_Queue.group_status (Execution.peek exec_id);
-  in res :: map Exn.Exn errs end;
+    val exns = maps Task_Queue.group_status (Execution.peek exec_id);
+  in res :: map Exn.Exn exns end;
 
 datatype task =
   Task of Path.T * string list * (theory list -> result) |