diff --git a/src/Doc/Classes/Setup.thy b/src/Doc/Classes/Setup.thy
--- a/src/Doc/Classes/Setup.thy
+++ b/src/Doc/Classes/Setup.thy
@@ -1,36 +1,36 @@
 theory Setup
 imports Main
 begin
 
 ML_file \<open>../antiquote_setup.ML\<close>
 ML_file \<open>../more_antiquote.ML\<close>
 
 declare [[default_code_width = 74]]
 
 syntax
   "_alpha" :: "type"  ("\<alpha>")
-  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()::_" [0] 1000)
+  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>' ::_" [0] 1000)
   "_beta" :: "type"  ("\<beta>")
-  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()::_" [0] 1000)
+  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>' ::_" [0] 1000)
 
 parse_ast_translation \<open>
   let
     fun alpha_ast_tr [] = Ast.Variable "'a"
       | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
     fun alpha_ofsort_ast_tr [ast] =
           Ast.Appl [Ast.Constant \<^syntax_const>\<open>_ofsort\<close>, Ast.Variable "'a", ast]
       | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
     fun beta_ast_tr [] = Ast.Variable "'b"
       | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
     fun beta_ofsort_ast_tr [ast] =
           Ast.Appl [Ast.Constant \<^syntax_const>\<open>_ofsort\<close>, Ast.Variable "'b", ast]
       | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
   in
    [(\<^syntax_const>\<open>_alpha\<close>, K alpha_ast_tr),
     (\<^syntax_const>\<open>_alpha_ofsort\<close>, K alpha_ofsort_ast_tr),
     (\<^syntax_const>\<open>_beta\<close>, K beta_ast_tr),
     (\<^syntax_const>\<open>_beta_ofsort\<close>, K beta_ofsort_ast_tr)]
   end
 \<close>
 
 end
diff --git a/src/HOL/Number_Theory/Cong.thy b/src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy
+++ b/src/HOL/Number_Theory/Cong.thy
@@ -1,770 +1,770 @@
 (*  Title:      HOL/Number_Theory/Cong.thy
     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.
 
 This file combines and revises a number of prior developments.
 
 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
 gcd, lcm, and prime for the natural numbers.
 
 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
 extended gcd, lcm, primes to the integers. Amine Chaieb provided
 another extension of the notions to the integers, and added a number
 of results to "Primes" and "GCD".
 
 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
 developed the congruence relations on the integers. The notion was
 extended to the natural numbers by Chaieb. Jeremy Avigad combined
 these, revised and tidied them, made the development uniform for the
 natural numbers and the integers, and added a number of new theorems.
 *)
 
 section \<open>Congruence\<close>
 
 theory Cong
   imports "HOL-Computational_Algebra.Primes"
 begin
 
 subsection \<open>Generic congruences\<close>
  
 context unique_euclidean_semiring
 begin
 
-definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ = _] '(()mod _'))\<close>)
+definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ = _] '(' mod _'))\<close>)
   where "cong b c a \<longleftrightarrow> b mod a = c mod a"
   
-abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ \<noteq> _] '(()mod _'))\<close>)
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  (\<open>(1[_ \<noteq> _] '(' mod _'))\<close>)
   where "notcong b c a \<equiv> \<not> cong b c a"
 
 lemma cong_refl [simp]:
   "[b = b] (mod a)"
   by (simp add: cong_def)
 
 lemma cong_sym: 
   "[b = c] (mod a) \<Longrightarrow> [c = b] (mod a)"
   by (simp add: cong_def)
 
 lemma cong_sym_eq:
   "[b = c] (mod a) \<longleftrightarrow> [c = b] (mod a)"
   by (auto simp add: cong_def)
 
 lemma cong_trans [trans]:
   "[b = c] (mod a) \<Longrightarrow> [c = d] (mod a) \<Longrightarrow> [b = d] (mod a)"
   by (simp add: cong_def)
 
 lemma cong_mult_self_right:
   "[b * a = 0] (mod a)"
   by (simp add: cong_def)
 
 lemma cong_mult_self_left:
   "[a * b = 0] (mod a)"
   by (simp add: cong_def)
 
 lemma cong_mod_left [simp]:
   "[b mod a = c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
   by (simp add: cong_def)  
 
 lemma cong_mod_right [simp]:
   "[b = c mod a] (mod a) \<longleftrightarrow> [b = c] (mod a)"
   by (simp add: cong_def)  
 
 lemma cong_0 [simp, presburger]:
   "[b = c] (mod 0) \<longleftrightarrow> b = c"
   by (simp add: cong_def)
 
 lemma cong_1 [simp, presburger]:
   "[b = c] (mod 1)"
   by (simp add: cong_def)
 
 lemma cong_dvd_iff:
   "a dvd b \<longleftrightarrow> a dvd c" if "[b = c] (mod a)"
   using that by (auto simp: cong_def dvd_eq_mod_eq_0)
 
 lemma cong_0_iff: "[b = 0] (mod a) \<longleftrightarrow> a dvd b"
   by (simp add: cong_def dvd_eq_mod_eq_0)
 
 lemma cong_add:
   "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b + d = c + e] (mod a)"
   by (auto simp add: cong_def intro: mod_add_cong)
 
 lemma cong_mult:
   "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b * d = c * e] (mod a)"
   by (auto simp add: cong_def intro: mod_mult_cong)
 
 lemma cong_scalar_right:
   "[b = c] (mod a) \<Longrightarrow> [b * d = c * d] (mod a)"
   by (simp add: cong_mult)
 
 lemma cong_scalar_left:
   "[b = c] (mod a) \<Longrightarrow> [d * b = d * c] (mod a)"
   by (simp add: cong_mult)
 
 lemma cong_pow:
   "[b = c] (mod a) \<Longrightarrow> [b ^ n = c ^ n] (mod a)"
   by (simp add: cong_def power_mod [symmetric, of b n a] power_mod [symmetric, of c n a])
 
 lemma cong_sum:
   "[sum f A = sum g A] (mod a)" if "\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a)"
   using that by (induct A rule: infinite_finite_induct) (auto intro: cong_add)
 
 lemma cong_prod:
   "[prod f A = prod g A] (mod a)" if "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a))"
   using that by (induct A rule: infinite_finite_induct) (auto intro: cong_mult)
 
 lemma mod_mult_cong_right:
   "[c mod (a * b) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)"
   by (simp add: cong_def mod_mod_cancel mod_add_left_eq)
 
 lemma mod_mult_cong_left:
   "[c mod (b * a) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)"
   using mod_mult_cong_right [of c a b d] by (simp add: ac_simps)
 
 end
 
 context unique_euclidean_ring
 begin
 
 lemma cong_diff:
   "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b - d = c - e] (mod a)"
   by (auto simp add: cong_def intro: mod_diff_cong)
 
 lemma cong_diff_iff_cong_0:
   "[b - c = 0] (mod a) \<longleftrightarrow> [b = c] (mod a)" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   then have "[b - c + c = 0 + c] (mod a)"
     by (rule cong_add) simp
   then show ?Q
     by simp
 next
   assume ?Q
   with cong_diff [of b c a c c] show ?P
     by simp
 qed
 
 lemma cong_minus_minus_iff:
   "[- b = - c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
   using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]
   by (simp add: cong_0_iff dvd_diff_commute)
 
 lemma cong_modulus_minus_iff [iff]:
   "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
   using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"]
   by (simp add: cong_0_iff)
 
 lemma cong_iff_dvd_diff:
   "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
 
 lemma cong_iff_lin:
   "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" (is "?P \<longleftrightarrow> ?Q")
 proof -
   have "?P \<longleftrightarrow> m dvd b - a"
     by (simp add: cong_iff_dvd_diff dvd_diff_commute)
   also have "\<dots> \<longleftrightarrow> ?Q"
     by (auto simp add: algebra_simps elim!: dvdE)
   finally show ?thesis
     by simp
 qed
 
 lemma cong_add_lcancel:
   "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   by (simp add: cong_iff_lin algebra_simps)
 
 lemma cong_add_rcancel:
   "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   by (simp add: cong_iff_lin algebra_simps)
 
 lemma cong_add_lcancel_0:
   "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   using cong_add_lcancel [of a x 0 n] by simp
 
 lemma cong_add_rcancel_0:
   "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   using cong_add_rcancel [of x a 0 n] by simp
 
 lemma cong_dvd_modulus:
   "[x = y] (mod n)" if "[x = y] (mod m)" and "n dvd m"
   using that by (auto intro: dvd_trans simp add: cong_iff_dvd_diff)
 
 lemma cong_modulus_mult:
   "[x = y] (mod m)" if "[x = y] (mod m * n)"
   using that by (simp add: cong_iff_dvd_diff) (rule dvd_mult_left)
 
 end
 
 lemma cong_abs [simp]:
   "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
   for x y :: "'a :: {unique_euclidean_ring, linordered_idom}"
   by (simp add: cong_iff_dvd_diff)
 
 lemma cong_square:
   "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}"
   by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest: prime_dvd_multD)
 
 lemma cong_mult_rcancel:
   "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
   using that by (auto simp add: cong_iff_dvd_diff left_diff_distrib [symmetric] ac_simps coprime_dvd_mult_right_iff)
 
 lemma cong_mult_lcancel:
   "[k * a = k * b] (mod m) = [a = b] (mod m)"
   if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
   using that cong_mult_rcancel [of k m a b] by (simp add: ac_simps)
 
 lemma coprime_cong_mult:
   "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   for a b :: "'a :: {unique_euclidean_ring, semiring_gcd}"
   by (simp add: cong_iff_dvd_diff divides_mult)
 
 lemma cong_gcd_eq:
   "gcd a m = gcd b m" if "[a = b] (mod m)"
   for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
 proof (cases "m = 0")
   case True
   with that show ?thesis
     by simp
 next
   case False
   moreover have "gcd (a mod m) m = gcd (b mod m) m"
     using that by (simp add: cong_def)
   ultimately show ?thesis
     by simp
 qed 
 
 lemma cong_imp_coprime:
   "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
   by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq)
 
 lemma cong_cong_prod_coprime:
   "[x = y] (mod (\<Prod>i\<in>A. m i))" if
     "(\<forall>i\<in>A. [x = y] (mod m i))"
     "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   for x y :: "'a :: {unique_euclidean_ring, semiring_gcd}"
   using that by (induct A rule: infinite_finite_induct)
     (auto intro!: coprime_cong_mult prod_coprime_right)
 
 
 subsection \<open>Congruences on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close>
 
 lemma cong_int_iff:
   "[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)"
   by (simp add: cong_def of_nat_mod [symmetric])
 
 lemma cong_Suc_0 [simp, presburger]:
   "[m = n] (mod Suc 0)"
   using cong_1 [of m n] by simp
 
 lemma cong_diff_nat:
   "[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)"
     and "a \<ge> c" "b \<ge> d" for a b c d m :: nat
 proof -
   have "[c + (a - c) = d + (b - d)] (mod m)"
     using that by simp
   with \<open>[c = d] (mod m)\<close> have "[c + (a - c) = c + (b - d)] (mod m)"
     using mod_add_cong by (auto simp add: cong_def) fastforce
   then show ?thesis
     by (simp add: cong_def nat_mod_eq_iff)
 qed
 
 lemma cong_diff_iff_cong_0_nat:
   "[a - b = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" if "a \<ge> b" for a b :: nat
   using that by (auto simp add: cong_def le_imp_diff_is_add dest: nat_mod_eq_lemma)
 
 lemma cong_diff_iff_cong_0_nat':
   "[nat \<bar>int a - int b\<bar> = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)"
 proof (cases "b \<le> a")
   case True
   then show ?thesis
     by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m])
 next
   case False
   then have "a \<le> b"
     by simp
   then show ?thesis
     by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m])
       (auto simp add: cong_def)
 qed
 
 lemma cong_altdef_nat:
   "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   for a b :: nat
   by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat)
 
 lemma cong_altdef_nat':
   "[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
   using cong_diff_iff_cong_0_nat' [of a b m]
   by (simp only: cong_0_iff [symmetric])
 
 lemma cong_mult_rcancel_nat:
   "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   if "coprime k m" for a k m :: nat
 proof -
   have "[a * k = b * k] (mod m) \<longleftrightarrow> m dvd nat \<bar>int (a * k) - int (b * k)\<bar>"
     by (simp add: cong_altdef_nat')
   also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>(int a - int b) * int k\<bar>"
     by (simp add: algebra_simps)
   also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
     by (simp add: abs_mult nat_times_as_int)
   also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
     by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
   also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
     by (simp add: cong_altdef_nat')
   finally show ?thesis .
 qed
 
 lemma cong_mult_lcancel_nat:
   "[k * a = k * b] (mod m) = [a = b] (mod m)"
   if "coprime k m" for a k m :: nat
   using that by (simp add: cong_mult_rcancel_nat ac_simps)
 
 lemma coprime_cong_mult_nat:
   "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   for a b :: nat
   by (simp add: cong_altdef_nat' divides_mult)
 
 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_def)
 
 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_def)
 
 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_def) (metis mod_less_divisor mod_mod_trivial)
 
 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_def)  (metis mod_mod_trivial pos_mod_conj)
 
 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
     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
     with \<open>?lhs\<close> show ?rhs
       by (metis cong_def mult.commute nat_le_linear nat_mod_eq_lemma)
   qed
 next
   assume ?rhs
   then show ?lhs
     by (metis cong_def mult.commute nat_mod_eq_iff) 
 qed
 
 lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   for a b :: nat
   by simp
 
 lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   for a b :: int
   by simp
 
 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_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_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   for a x :: nat
   using cong_add_lcancel_nat [of a x 0 n] by simp
 
 lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   for a x :: nat
   using cong_add_rcancel_nat [of x a 0 n] by simp
 
 lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
   for x y :: nat
   unfolding cong_iff_lin_nat dvd_def
   by (metis mult.commute mult.left_commute)
 
 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_def)
 
 lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1"
   for n :: nat
   by (auto simp: cong_def)
 
 lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1"
   for n :: int
   by (auto simp: cong_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 (auto simp add: cong_altdef_nat le_imp_diff_is_add elim!: dvdE)
 
 
 lemma cong_solve_nat:
   fixes a :: nat
   shows "\<exists>x. [a * x = gcd a n] (mod n)"
 proof (cases "a = 0 \<or> n = 0")
   case True
   then show ?thesis
     by (force simp add: cong_0_iff cong_sym)
 next
   case False
   then show ?thesis
     using bezout_nat [of a n]
     by auto (metis cong_add_rcancel_0_nat cong_mult_self_left)
 qed
 
 lemma cong_solve_int:
   fixes a :: int
   shows "\<exists>x. [a * x = gcd a n] (mod n)"
     by (metis bezout_int cong_iff_lin mult.commute)
 
 lemma cong_solve_dvd_nat:
   fixes a :: nat
   assumes "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
   then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
     using cong_scalar_left by blast
   also from assms have "(d div gcd a n) * gcd a n = d"
     by (rule dvd_div_mult_self)
   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
     by auto
   finally show ?thesis
     by auto
 qed
 
 lemma cong_solve_dvd_int:
   fixes a::int
   assumes b: "gcd a n dvd d"
   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
   then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
     using cong_scalar_left by blast
   also from b have "(d div gcd a n) * gcd a n = d"
     by (rule dvd_div_mult_self)
   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
     by auto
   finally show ?thesis
     by auto
 qed
 
 lemma cong_solve_coprime_nat:
   "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n"
   using that cong_solve_nat [of a n] by auto
 
 lemma cong_solve_coprime_int:
   "\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int
   using that cong_solve_int [of a n] by (auto simp add: zabs_def split: if_splits)
 
 lemma coprime_iff_invertible_nat:
   "coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P then show ?Q
     by (auto dest!: cong_solve_coprime_nat)
 next
   assume ?Q
   then obtain b where "[a * b = Suc 0] (mod m)"
     by blast
   with coprime_mod_left_iff [of m "a * b"] show ?P
     by (cases "m = 0 \<or> m = 1")
       (unfold cong_def, auto simp add: cong_def)
 qed
 
 lemma coprime_iff_invertible_int:
   "coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))" (is "?P \<longleftrightarrow> ?Q") for m :: int
 proof
   assume ?P then show ?Q
     by (auto dest: cong_solve_coprime_int)
 next
   assume ?Q
   then obtain b where "[a * b = 1] (mod m)"
     by blast
   with coprime_mod_left_iff [of m "a * b"] show ?P
     by (cases "m = 0 \<or> m = 1")
       (unfold cong_def, auto simp add: zmult_eq_1_iff)
 qed
 
 lemma coprime_iff_invertible'_nat:
   assumes "m > 0"
   shows "coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
 proof -
   have "\<And>b. \<lbrakk>0 < m; [a * b = Suc 0] (mod m)\<rbrakk> \<Longrightarrow> \<exists>b'<m. [a * b' = Suc 0] (mod m)"
     by (metis cong_def mod_less_divisor [OF assms] mod_mult_right_eq)
   then show ?thesis
     using assms coprime_iff_invertible_nat by auto
 qed
 
 lemma coprime_iff_invertible'_int:
   fixes m :: int
   assumes "m > 0"
   shows "coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))"
 proof -
   have "\<And>b. \<lbrakk>0 < m; [a * b = 1] (mod m)\<rbrakk> \<Longrightarrow> \<exists>b'<m. [a * b' = 1] (mod m)"
     by (meson cong_less_unique_int cong_scalar_left cong_sym cong_trans)
   then show ?thesis
     by (metis assms coprime_iff_invertible_int cong_def cong_mult_lcancel mod_pos_pos_trivial pos_mod_conj)
 qed
 
 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
   by (meson cong_altdef_nat' lcm_least)
 
 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_iff_dvd_diff lcm_least)
 
 lemma cong_cong_prod_coprime_nat:
   "[x = y] (mod (\<Prod>i\<in>A. m i))" if
     "(\<forall>i\<in>A. [x = y] (mod m i))"
     "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   for x y :: nat
   using that by (induct A rule: infinite_finite_induct)
     (auto intro!: coprime_cong_mult_nat prod_coprime_right)
 
 lemma binary_chinese_remainder_nat:
   fixes m1 m2 :: nat
   assumes a: "coprime m1 m2"
   shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
   have "\<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 1: "[m1 * x1 = 1] (mod m2)"
       by auto
     from a have b: "coprime m2 m1"
       by (simp add: ac_simps)
     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 (simp add: cong_mult_self_left)
     moreover have "[m2 * x2 = 0] (mod m2)"
       by (simp add: cong_mult_self_left)
     ultimately show ?thesis
       using 1 2 by blast
   qed
   then obtain b1 b2
     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)"
     using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left 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:
   fixes m1 m2 :: int
   assumes a: "coprime m1 m2"
   shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
   have "\<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 1: "[m1 * x1 = 1] (mod m2)"
       by auto
     from a have b: "coprime m2 m1"
       by (simp add: ac_simps)
     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 (simp add: cong_mult_self_left)
     moreover have "[m2 * x2 = 0] (mod m2)"
       by (simp add: cong_mult_self_left)
     ultimately show ?thesis
       using 1 2 by blast
   qed
   then obtain b1 b2
     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)"
     using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast
   then have "[?x = u2] (mod m2)" by simp
   with \<open>[?x = u1] (mod m1)\<close> show ?thesis
     by blast
 qed
 
 lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
   for x y :: nat
   by (metis cong_def mod_mult_cong_right)
 
 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_def)
 
 lemma binary_chinese_remainder_unique_nat:
   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 -
   obtain y where y1: "[y = u1] (mod m1)" and y2: "[y = u2] (mod m2)"
     using binary_chinese_remainder_nat [OF a] by blast
   let ?x = "y mod (m1 * m2)"
   from nz have less: "?x < m1 * m2"
     by auto
   have 1: "[?x = u1] (mod m1)"
     using y1 mod_mult_cong_right by blast
   have 2: "[?x = u2] (mod m2)"
     using y2 mod_mult_cong_left by blast
   have "z = ?x" if "z < m1 * m2" "[z = u1] (mod m1)"  "[z = u2] (mod m2)" for z
   proof -
     have "[?x = z] (mod m1)"
       by (metis "1" cong_def that(2))
     moreover have "[?x = z] (mod m2)"
       by (metis "2" cong_def that(3))
     ultimately have "[?x = z] (mod m1 * m2)"
       using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right)
     with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
       by (auto simp add: cong_def)
   qed
   with less 1 2 show ?thesis
     by blast
  qed
 
 lemma chinese_remainder_nat:
   fixes A :: "'a set"
     and m :: "'a \<Rightarrow> nat"
     and u :: "'a \<Rightarrow> nat"
   assumes fin: "finite A"
     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 -
   have "\<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 \<in> A"
     with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
       by (intro prod_coprime_left) auto
     then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (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))"
       by (simp add: cong_0_iff)
     ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
       by blast
   qed
   then obtain b where b: "\<And>i. i \<in> A \<Longrightarrow> [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
   proof (rule exI, clarify)
     fix i
     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)
       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)"
       proof (intro cong_add cong_scalar_left cong_sum)
         show "[b i = 1] (mod m i)"
           using a b by blast
         show "[b x = 0] (mod m i)" if "x \<in> A - {i}" for x
         proof -
           have "x \<in> A" "x \<noteq> i"
             using that by auto
           then show ?thesis
             using a b [OF \<open>x \<in> A\<close>] cong_dvd_modulus_nat fin by blast
         qed
       qed
       finally show ?thesis
         by simp
     qed
   qed
 qed
 
 lemma coprime_cong_prod_nat: "[x = y] (mod (\<Prod>i\<in>A. m i))"
   if "\<And>i j. \<lbrakk>i \<in> A; j \<in> A; i \<noteq> j\<rbrakk> \<Longrightarrow> coprime (m i) (m j)"
     and "\<And>i. i \<in> A \<Longrightarrow> [x = y] (mod m i)" for x y :: nat
   using that 
 proof (induct A rule: infinite_finite_induct)
   case (insert x A)
   then show ?case
     by simp (metis coprime_cong_mult_nat prod_coprime_right)
 qed auto
 
 lemma chinese_remainder_unique_nat:
   fixes A :: "'a set"
     and m :: "'a \<Rightarrow> nat"
     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)"
   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: "(\<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: "\<forall>i\<in>A. [?x = u i] (mod m i)"
     using fin one
     by (auto simp add: cong_def dvd_prod_eqI mod_mod_cancel) 
   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: "(\<forall>i\<in>A. [z = u i] (mod m i))"
     have "\<forall>i\<in>A. [?x = z] (mod m i)"
       using cong zcong by (auto simp add: cong_def)
     with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
       by (intro coprime_cong_prod_nat) auto
     with zless less show "z = ?x"
       by (auto simp add: cong_def)
   qed
   from less cong unique show ?thesis
     by blast
 qed
 
 end
diff --git a/src/Pure/pure_thy.ML b/src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML
+++ b/src/Pure/pure_thy.ML
@@ -1,254 +1,254 @@
 (*  Title:      Pure/pure_thy.ML
     Author:     Markus Wenzel, TU Muenchen
 
 Pure theory syntax and further logical content.
 *)
 
 signature PURE_THY =
 sig
   val old_appl_syntax: theory -> bool
   val old_appl_syntax_setup: theory -> theory
   val token_markers: string list
 end;
 
 structure Pure_Thy: PURE_THY =
 struct
 
 (* auxiliary *)
 
 val typ = Simple_Syntax.read_typ;
 val prop = Simple_Syntax.read_prop;
 
 val tycon = Lexicon.mark_type;
 val const = Lexicon.mark_const;
 
 val qualify = Binding.qualify true Context.PureN;
 
 fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
 fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range);
 fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
 fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
 
 fun add_deps_type c thy =
   let
     val n = Sign.arity_number thy c;
     val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
   in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end
 
 fun add_deps_const c thy =
   let
     val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
     val typargs = Sign.const_typargs thy (c, T);
   in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end;
 
 
 (* application syntax variants *)
 
 val appl_syntax =
  [("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
   ("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
 
 val applC_syntax =
  [("",       typ "'a \<Rightarrow> cargs",                  Mixfix.mixfix "_"),
   ("_cargs", typ "'a \<Rightarrow> cargs \<Rightarrow> cargs",         mixfix ("_/ _", [1000, 1000], 1000)),
   ("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> logic", mixfix ("(1_/ _)", [1000, 1000], 999)),
   ("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> aprop", mixfix ("(1_/ _)", [1000, 1000], 999))];
 
 structure Old_Appl_Syntax = Theory_Data
 (
   type T = bool;
   val empty = false;
   val extend = I;
   fun merge (b1, b2) : T =
     if b1 = b2 then b1
     else error "Cannot merge theories with different application syntax";
 );
 
 val old_appl_syntax = Old_Appl_Syntax.get;
 
 val old_appl_syntax_setup =
   Old_Appl_Syntax.put true #>
   Sign.del_syntax Syntax.mode_default applC_syntax #>
   Sign.add_syntax Syntax.mode_default appl_syntax;
 
 
 (* main content *)
 
 val token_markers =
   ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
 
 val _ = Theory.setup
   (Sign.theory_naming #>
    Old_Appl_Syntax.put false #>
    Sign.add_types_global
    [(Binding.make ("fun", \<^here>), 2, NoSyn),
     (Binding.make ("prop", \<^here>), 0, NoSyn),
     (Binding.make ("itself", \<^here>), 1, NoSyn),
     (Binding.make ("dummy", \<^here>), 0, NoSyn),
     (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)]
   #> add_deps_type "fun"
   #> add_deps_type "prop"
   #> add_deps_type "itself"
   #> add_deps_type "dummy"
   #> add_deps_type "Pure.proof"
   #> Sign.add_nonterminals_global
     (map (fn name => Binding.make (name, \<^here>))
       (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
         "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
         "any", "prop'", "num_const", "float_const", "num_position",
         "float_position", "index", "struct", "tid_position",
         "tvar_position", "id_position", "longid_position", "var_position",
         "str_position", "string_position", "cartouche_position", "type_name",
         "class_name"]))
   #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   #> Sign.add_syntax Syntax.mode_default
    [("",            typ "prop' \<Rightarrow> prop",               Mixfix.mixfix "_"),
     ("",            typ "logic \<Rightarrow> any",                Mixfix.mixfix "_"),
     ("",            typ "prop' \<Rightarrow> any",                Mixfix.mixfix "_"),
     ("",            typ "logic \<Rightarrow> logic",              Mixfix.mixfix "'(_')"),
     ("",            typ "prop' \<Rightarrow> prop'",              Mixfix.mixfix "'(_')"),
     ("_constrain",  typ "logic \<Rightarrow> type \<Rightarrow> logic",      mixfix ("_::_", [4, 0], 3)),
     ("_constrain",  typ "prop' \<Rightarrow> type \<Rightarrow> prop'",      mixfix ("_::_", [4, 0], 3)),
     ("_ignore_type", typ "'a",                         NoSyn),
     ("",            typ "tid_position \<Rightarrow> type",        Mixfix.mixfix "_"),
     ("",            typ "tvar_position \<Rightarrow> type",       Mixfix.mixfix "_"),
     ("",            typ "type_name \<Rightarrow> type",           Mixfix.mixfix "_"),
     ("_type_name",  typ "id \<Rightarrow> type_name",             Mixfix.mixfix "_"),
     ("_type_name",  typ "longid \<Rightarrow> type_name",         Mixfix.mixfix "_"),
     ("_ofsort",     typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
     ("_ofsort",     typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
-    ("_dummy_ofsort", typ "sort \<Rightarrow> type",              mixfix ("'_()::_", [0], 1000)),
+    ("_dummy_ofsort", typ "sort \<Rightarrow> type",              mixfix ("'_' ::_", [0], 1000)),
     ("",            typ "class_name \<Rightarrow> sort",          Mixfix.mixfix "_"),
     ("_class_name", typ "id \<Rightarrow> class_name",            Mixfix.mixfix "_"),
     ("_class_name", typ "longid \<Rightarrow> class_name",        Mixfix.mixfix "_"),
     ("_dummy_sort", typ "sort",                        Mixfix.mixfix "'_"),
     ("_topsort",    typ "sort",                        Mixfix.mixfix "{}"),
     ("_sort",       typ "classes \<Rightarrow> sort",             Mixfix.mixfix "{_}"),
     ("",            typ "class_name \<Rightarrow> classes",       Mixfix.mixfix "_"),
     ("_classes",    typ "class_name \<Rightarrow> classes \<Rightarrow> classes", Mixfix.mixfix "_,_"),
     ("_tapp",       typ "type \<Rightarrow> type_name \<Rightarrow> type",   mixfix ("_ _", [1000, 0], 1000)),
     ("_tappl",      typ "type \<Rightarrow> types \<Rightarrow> type_name \<Rightarrow> type", Mixfix.mixfix "((1'(_,/ _')) _)"),
     ("",            typ "type \<Rightarrow> types",               Mixfix.mixfix "_"),
     ("_types",      typ "type \<Rightarrow> types \<Rightarrow> types",      Mixfix.mixfix "_,/ _"),
     ("\<^type>fun", typ "type \<Rightarrow> type \<Rightarrow> type",        mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
     ("_bracket",    typ "types \<Rightarrow> type \<Rightarrow> type",       mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
     ("",            typ "type \<Rightarrow> type",                Mixfix.mixfix "'(_')"),
     ("\<^type>dummy", typ "type",                      Mixfix.mixfix "'_"),
     ("_type_prop",  typ "'a",                          NoSyn),
     ("_lambda",     typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",       mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
     ("_abs",        typ "'a",                          NoSyn),
     ("",            typ "'a \<Rightarrow> args",                  Mixfix.mixfix "_"),
     ("_args",       typ "'a \<Rightarrow> args \<Rightarrow> args",          Mixfix.mixfix "_,/ _"),
     ("",            typ "id_position \<Rightarrow> idt",          Mixfix.mixfix "_"),
     ("_idtdummy",   typ "idt",                         Mixfix.mixfix "'_"),
     ("_idtyp",      typ "id_position \<Rightarrow> type \<Rightarrow> idt",  mixfix ("_::_", [], 0)),
-    ("_idtypdummy", typ "type \<Rightarrow> idt",                 mixfix ("'_()::_", [], 0)),
+    ("_idtypdummy", typ "type \<Rightarrow> idt",                 mixfix ("'_' ::_", [], 0)),
     ("",            typ "idt \<Rightarrow> idt",                  Mixfix.mixfix "'(_')"),
     ("",            typ "idt \<Rightarrow> idts",                 Mixfix.mixfix "_"),
     ("_idts",       typ "idt \<Rightarrow> idts \<Rightarrow> idts",         mixfix ("_/ _", [1, 0], 0)),
     ("",            typ "idt \<Rightarrow> pttrn",                Mixfix.mixfix "_"),
     ("",            typ "pttrn \<Rightarrow> pttrns",             Mixfix.mixfix "_"),
     ("_pttrns",     typ "pttrn \<Rightarrow> pttrns \<Rightarrow> pttrns",   mixfix ("_/ _", [1, 0], 0)),
     ("",            typ "aprop \<Rightarrow> aprop",              Mixfix.mixfix "'(_')"),
     ("",            typ "id_position \<Rightarrow> aprop",        Mixfix.mixfix "_"),
     ("",            typ "longid_position \<Rightarrow> aprop",    Mixfix.mixfix "_"),
     ("",            typ "var_position \<Rightarrow> aprop",       Mixfix.mixfix "_"),
     ("_DDDOT",      typ "aprop",                       Mixfix.mixfix "\<dots>"),
     ("_aprop",      typ "aprop \<Rightarrow> prop",               Mixfix.mixfix "PROP _"),
     ("_asm",        typ "prop \<Rightarrow> asms",                Mixfix.mixfix "_"),
     ("_asms",       typ "prop \<Rightarrow> asms \<Rightarrow> asms",        Mixfix.mixfix "_;/ _"),
     ("_bigimpl",    typ "asms \<Rightarrow> prop \<Rightarrow> prop",        mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
     ("_ofclass",    typ "type \<Rightarrow> logic \<Rightarrow> prop",       Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"),
     ("_mk_ofclass", typ "dummy",                       NoSyn),
     ("_TYPE",       typ "type \<Rightarrow> logic",               Mixfix.mixfix "(1TYPE/(1'(_')))"),
     ("",            typ "id_position \<Rightarrow> logic",        Mixfix.mixfix "_"),
     ("",            typ "longid_position \<Rightarrow> logic",    Mixfix.mixfix "_"),
     ("",            typ "var_position \<Rightarrow> logic",       Mixfix.mixfix "_"),
     ("_DDDOT",      typ "logic",                       Mixfix.mixfix "\<dots>"),
     ("_strip_positions", typ "'a", NoSyn),
     ("_position",   typ "num_token \<Rightarrow> num_position",   Mixfix.mixfix "_"),
     ("_position",   typ "float_token \<Rightarrow> float_position", Mixfix.mixfix "_"),
     ("_constify",   typ "num_position \<Rightarrow> num_const",   Mixfix.mixfix "_"),
     ("_constify",   typ "float_position \<Rightarrow> float_const", Mixfix.mixfix "_"),
     ("_index",      typ "logic \<Rightarrow> index",              Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"),
     ("_indexdefault", typ "index",                     Mixfix.mixfix ""),
     ("_indexvar",   typ "index",                       Mixfix.mixfix "'\<index>"),
     ("_struct",     typ "index \<Rightarrow> logic",              NoSyn),
     ("_update_name", typ "idt",                        NoSyn),
     ("_constrainAbs", typ "'a",                        NoSyn),
     ("_position_sort", typ "tid \<Rightarrow> tid_position",      Mixfix.mixfix "_"),
     ("_position_sort", typ "tvar \<Rightarrow> tvar_position",    Mixfix.mixfix "_"),
     ("_position",   typ "id \<Rightarrow> id_position",           Mixfix.mixfix "_"),
     ("_position",   typ "longid \<Rightarrow> longid_position",   Mixfix.mixfix "_"),
     ("_position",   typ "var \<Rightarrow> var_position",         Mixfix.mixfix "_"),
     ("_position",   typ "str_token \<Rightarrow> str_position",   Mixfix.mixfix "_"),
     ("_position",   typ "string_token \<Rightarrow> string_position", Mixfix.mixfix "_"),
     ("_position",   typ "cartouche \<Rightarrow> cartouche_position", Mixfix.mixfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
     ("_context_const", typ "id_position \<Rightarrow> logic",     Mixfix.mixfix "CONST _"),
     ("_context_const", typ "id_position \<Rightarrow> aprop",     Mixfix.mixfix "CONST _"),
     ("_context_const", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"),
     ("_context_const", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"),
     ("_context_xconst", typ "id_position \<Rightarrow> logic",    Mixfix.mixfix "XCONST _"),
     ("_context_xconst", typ "id_position \<Rightarrow> aprop",    Mixfix.mixfix "XCONST _"),
     ("_context_xconst", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"),
     ("_context_xconst", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"),
     (const "Pure.dummy_pattern", typ "aprop",          Mixfix.mixfix "'_"),
     ("_sort_constraint", typ "type \<Rightarrow> prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
     (const "Pure.term", typ "logic \<Rightarrow> prop",           Mixfix.mixfix "TERM _"),
     (const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
   #> Sign.add_syntax Syntax.mode_default applC_syntax
   #> Sign.add_syntax (Print_Mode.ASCII, true)
    [(tycon "fun",         typ "type \<Rightarrow> type \<Rightarrow> type",   mixfix ("(_/ => _)", [1, 0], 0)),
     ("_bracket",          typ "types \<Rightarrow> type \<Rightarrow> type",  mixfix ("([_]/ => _)", [0, 0], 0)),
     ("_lambda",           typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",  mixfix ("(3%_./ _)", [0, 3], 3)),
     (const "Pure.eq",     typ "'a \<Rightarrow> 'a \<Rightarrow> prop",       infix_ ("==", 2)),
     (const "Pure.all_binder", typ "idts \<Rightarrow> prop \<Rightarrow> prop", mixfix ("(3!!_./ _)", [0, 0], 0)),
     (const "Pure.imp",    typ "prop \<Rightarrow> prop \<Rightarrow> prop",   infixr_ ("==>", 1)),
     ("_DDDOT",            typ "aprop",                  Mixfix.mixfix "..."),
     ("_bigimpl",          typ "asms \<Rightarrow> prop \<Rightarrow> prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
     ("_DDDOT",            typ "logic",                  Mixfix.mixfix "...")]
   #> Sign.add_syntax ("", false)
    [(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))]
   #> Sign.add_consts
    [(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)),
     (qualify (Binding.make ("imp", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("\<Longrightarrow>", 1)),
     (qualify (Binding.make ("all", \<^here>)), typ "('a \<Rightarrow> prop) \<Rightarrow> prop", binder ("\<And>", 0, 0)),
     (qualify (Binding.make ("prop", \<^here>)), typ "prop \<Rightarrow> prop", NoSyn),
     (qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn),
     (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_"),
     (qualify (Binding.make ("Appt", \<^here>)), typ "Pure.proof \<Rightarrow> 'a \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("AppP", \<^here>)), typ "Pure.proof \<Rightarrow> Pure.proof \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("Abst", \<^here>)), typ "('a \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)]
   #> add_deps_const "Pure.eq"
   #> add_deps_const "Pure.imp"
   #> add_deps_const "Pure.all"
   #> add_deps_const "Pure.type"
   #> add_deps_const "Pure.dummy_pattern"
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
   #> Sign.add_consts
    [(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn),
     (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn),
     (qualify (Binding.make ("conjunction", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", NoSyn)]
   #> Sign.local_path
   #> (Global_Theory.add_defs false o map Thm.no_attributes)
    [(Binding.make ("prop_def", \<^here>),
       prop "(CONST Pure.prop :: prop \<Rightarrow> prop) (A::prop) \<equiv> A::prop"),
     (Binding.make ("term_def", \<^here>),
       prop "(CONST Pure.term :: 'a \<Rightarrow> prop) (x::'a) \<equiv> (\<And>A::prop. A \<Longrightarrow> A)"),
     (Binding.make ("sort_constraint_def", \<^here>),
       prop "(CONST Pure.sort_constraint :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself) \<equiv>\
       \ (CONST Pure.term :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself)"),
     (Binding.make ("conjunction_def", \<^here>),
       prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")] #> snd
   #> fold (fn (a, prop) =>
       snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms);
 
 end;
diff --git a/src/ZF/Bin.thy b/src/ZF/Bin.thy
--- a/src/ZF/Bin.thy
+++ b/src/ZF/Bin.thy
@@ -1,763 +1,763 @@
 (*  Title:      ZF/Bin.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
    The sign Pls stands for an infinite string of leading 0's.
    The sign Min stands for an infinite string of leading 1's.
 
 A number can have multiple representations, namely leading 0's with sign
 Pls and leading 1's with sign Min.  See twos-compl.ML/int_of_binary for
 the numerical interpretation.
 
 The representation expects that (m mod 2) is 0 or 1, even if m is negative;
 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
 *)
 
 section\<open>Arithmetic on Binary Integers\<close>
 
 theory Bin
 imports Int Datatype
 begin
 
 consts  bin :: i
 datatype
   "bin" = Pls
         | Min
         | Bit ("w \<in> bin", "b \<in> bool")     (infixl \<open>BIT\<close> 90)
 
 consts
   integ_of  :: "i=>i"
   NCons     :: "[i,i]=>i"
   bin_succ  :: "i=>i"
   bin_pred  :: "i=>i"
   bin_minus :: "i=>i"
   bin_adder :: "i=>i"
   bin_mult  :: "[i,i]=>i"
 
 primrec
   integ_of_Pls:  "integ_of (Pls)     = $# 0"
   integ_of_Min:  "integ_of (Min)     = $-($#1)"
   integ_of_BIT:  "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
 
     (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
 
 primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
   NCons_Pls: "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
   NCons_Min: "NCons (Min,b)     = cond(b,Min,Min BIT b)"
   NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b"
 
 primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
   bin_succ_Pls:  "bin_succ (Pls)     = Pls BIT 1"
   bin_succ_Min:  "bin_succ (Min)     = Pls"
   bin_succ_BIT:  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
 
 primrec (*predecessor*)
   bin_pred_Pls:  "bin_pred (Pls)     = Min"
   bin_pred_Min:  "bin_pred (Min)     = Min BIT 0"
   bin_pred_BIT:  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
 
 primrec (*unary negation*)
   bin_minus_Pls:
     "bin_minus (Pls)       = Pls"
   bin_minus_Min:
     "bin_minus (Min)       = Pls BIT 1"
   bin_minus_BIT:
     "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
                                 bin_minus(w) BIT 0)"
 
 primrec (*sum*)
   bin_adder_Pls:
     "bin_adder (Pls)     = (\<lambda>w\<in>bin. w)"
   bin_adder_Min:
     "bin_adder (Min)     = (\<lambda>w\<in>bin. bin_pred(w))"
   bin_adder_BIT:
     "bin_adder (v BIT x) =
        (\<lambda>w\<in>bin.
          bin_case (v BIT x, bin_pred(v BIT x),
                    %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w),
                                x xor y),
                    w))"
 
 (*The bin_case above replaces the following mutually recursive function:
 primrec
   "adding (v,x,Pls)     = v BIT x"
   "adding (v,x,Min)     = bin_pred(v BIT x)"
   "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)),
                                 x xor y)"
 *)
 
 definition
   bin_add   :: "[i,i]=>i"  where
     "bin_add(v,w) == bin_adder(v)`w"
 
 
 primrec
   bin_mult_Pls:
     "bin_mult (Pls,w)     = Pls"
   bin_mult_Min:
     "bin_mult (Min,w)     = bin_minus(w)"
   bin_mult_BIT:
     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
                                  NCons(bin_mult(v,w),0))"
 
 syntax
-  "_Int0" :: i  (\<open>#()0\<close>)
-  "_Int1" :: i  (\<open>#()1\<close>)
-  "_Int2" :: i  (\<open>#()2\<close>)
-  "_Neg_Int1" :: i  (\<open>#-()1\<close>)
-  "_Neg_Int2" :: i  (\<open>#-()2\<close>)
+  "_Int0" :: i  (\<open>#' 0\<close>)
+  "_Int1" :: i  (\<open>#' 1\<close>)
+  "_Int2" :: i  (\<open>#' 2\<close>)
+  "_Neg_Int1" :: i  (\<open>#-' 1\<close>)
+  "_Neg_Int2" :: i  (\<open>#-' 2\<close>)
 translations
   "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
   "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
   "#2" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1 BIT 0)"
   "#-1" \<rightleftharpoons> "CONST integ_of(CONST Min)"
   "#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
 
 syntax
   "_Int" :: "num_token => i"  (\<open>#_\<close> 1000)
   "_Neg_Int" :: "num_token => i"  (\<open>#-_\<close> 1000)
 
 ML_file \<open>Tools/numeral_syntax.ML\<close>
 
 
 declare bin.intros [simp,TC]
 
 lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
 by simp
 
 lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
 by simp
 
 lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
 by simp
 
 lemma NCons_Min_1: "NCons(Min,1) = Min"
 by simp
 
 lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
 by (simp add: bin.case_eqns)
 
 lemmas NCons_simps [simp] =
     NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
 
 
 
 (** Type checking **)
 
 lemma integ_of_type [TC]: "w \<in> bin ==> integ_of(w) \<in> int"
 apply (induct_tac "w")
 apply (simp_all add: bool_into_nat)
 done
 
 lemma NCons_type [TC]: "[| w \<in> bin; b \<in> bool |] ==> NCons(w,b) \<in> bin"
 by (induct_tac "w", auto)
 
 lemma bin_succ_type [TC]: "w \<in> bin ==> bin_succ(w) \<in> bin"
 by (induct_tac "w", auto)
 
 lemma bin_pred_type [TC]: "w \<in> bin ==> bin_pred(w) \<in> bin"
 by (induct_tac "w", auto)
 
 lemma bin_minus_type [TC]: "w \<in> bin ==> bin_minus(w) \<in> bin"
 by (induct_tac "w", auto)
 
 (*This proof is complicated by the mutual recursion*)
 lemma bin_add_type [rule_format]:
      "v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
 apply (unfold bin_add_def)
 apply (induct_tac "v")
 apply (rule_tac [3] ballI)
 apply (rename_tac [3] "w'")
 apply (induct_tac [3] "w'")
 apply (simp_all add: NCons_type)
 done
 
 declare bin_add_type [TC]
 
 lemma bin_mult_type [TC]: "[| v \<in> bin; w \<in> bin |] ==> bin_mult(v,w) \<in> bin"
 by (induct_tac "v", auto)
 
 
 subsubsection\<open>The Carry and Borrow Functions,
             \<^term>\<open>bin_succ\<close> and \<^term>\<open>bin_pred\<close>\<close>
 
 (*NCons preserves the integer value of its argument*)
 lemma integ_of_NCons [simp]:
      "[| w \<in> bin; b \<in> bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"
 apply (erule bin.cases)
 apply (auto elim!: boolE)
 done
 
 lemma integ_of_succ [simp]:
      "w \<in> bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)"
 apply (erule bin.induct)
 apply (auto simp add: zadd_ac elim!: boolE)
 done
 
 lemma integ_of_pred [simp]:
      "w \<in> bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)"
 apply (erule bin.induct)
 apply (auto simp add: zadd_ac elim!: boolE)
 done
 
 
 subsubsection\<open>\<^term>\<open>bin_minus\<close>: Unary Negation of Binary Integers\<close>
 
 lemma integ_of_minus: "w \<in> bin ==> integ_of(bin_minus(w)) = $- integ_of(w)"
 apply (erule bin.induct)
 apply (auto simp add: zadd_ac zminus_zadd_distrib  elim!: boolE)
 done
 
 
 subsubsection\<open>\<^term>\<open>bin_add\<close>: Binary Addition\<close>
 
 lemma bin_add_Pls [simp]: "w \<in> bin ==> bin_add(Pls,w) = w"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_Pls_right: "w \<in> bin ==> bin_add(w,Pls) = w"
 apply (unfold bin_add_def)
 apply (erule bin.induct, auto)
 done
 
 lemma bin_add_Min [simp]: "w \<in> bin ==> bin_add(Min,w) = bin_pred(w)"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_Min_right: "w \<in> bin ==> bin_add(w,Min) = bin_pred(w)"
 apply (unfold bin_add_def)
 apply (erule bin.induct, auto)
 done
 
 lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)"
 by (unfold bin_add_def, simp)
 
 lemma bin_add_BIT_BIT [simp]:
      "[| w \<in> bin;  y \<in> bool |]
       ==> bin_add(v BIT x, w BIT y) =
           NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"
 by (unfold bin_add_def, simp)
 
 lemma integ_of_add [rule_format]:
      "v \<in> bin ==>
           \<forall>w\<in>bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)"
 apply (erule bin.induct, simp, simp)
 apply (rule ballI)
 apply (induct_tac "wa")
 apply (auto simp add: zadd_ac elim!: boolE)
 done
 
 (*Subtraction*)
 lemma diff_integ_of_eq:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
 apply (unfold zdiff_def)
 apply (simp add: integ_of_add integ_of_minus)
 done
 
 
 subsubsection\<open>\<^term>\<open>bin_mult\<close>: Binary Multiplication\<close>
 
 lemma integ_of_mult:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)"
 apply (induct_tac "v", simp)
 apply (simp add: integ_of_minus)
 apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib  elim!: boolE)
 done
 
 
 subsection\<open>Computations\<close>
 
 (** extra rules for bin_succ, bin_pred **)
 
 lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
 by simp
 
 lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
 by simp
 
 lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
 by simp
 
 lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
 by simp
 
 (** extra rules for bin_minus **)
 
 lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
 by simp
 
 lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
 by simp
 
 (** extra rules for bin_add **)
 
 lemma bin_add_BIT_11: "w \<in> bin ==> bin_add(v BIT 1, w BIT 1) =
                      NCons(bin_add(v, bin_succ(w)), 0)"
 by simp
 
 lemma bin_add_BIT_10: "w \<in> bin ==> bin_add(v BIT 1, w BIT 0) =
                      NCons(bin_add(v,w), 1)"
 by simp
 
 lemma bin_add_BIT_0: "[| w \<in> bin;  y \<in> bool |]
       ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)"
 by simp
 
 (** extra rules for bin_mult **)
 
 lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
 by simp
 
 lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
 by simp
 
 
 (** Simplification rules with integer constants **)
 
 lemma int_of_0: "$#0 = #0"
 by simp
 
 lemma int_of_succ: "$# succ(n) = #1 $+ $#n"
 by (simp add: int_of_add [symmetric] natify_succ)
 
 lemma zminus_0 [simp]: "$- #0 = #0"
 by simp
 
 lemma zadd_0_intify [simp]: "#0 $+ z = intify(z)"
 by simp
 
 lemma zadd_0_right_intify [simp]: "z $+ #0 = intify(z)"
 by simp
 
 lemma zmult_1_intify [simp]: "#1 $* z = intify(z)"
 by simp
 
 lemma zmult_1_right_intify [simp]: "z $* #1 = intify(z)"
 by (subst zmult_commute, simp)
 
 lemma zmult_0 [simp]: "#0 $* z = #0"
 by simp
 
 lemma zmult_0_right [simp]: "z $* #0 = #0"
 by (subst zmult_commute, simp)
 
 lemma zmult_minus1 [simp]: "#-1 $* z = $-z"
 by (simp add: zcompare_rls)
 
 lemma zmult_minus1_right [simp]: "z $* #-1 = $-z"
 apply (subst zmult_commute)
 apply (rule zmult_minus1)
 done
 
 
 subsection\<open>Simplification Rules for Comparison of Binary Numbers\<close>
 text\<open>Thanks to Norbert Voelker\<close>
 
 (** Equals (=) **)
 
 lemma eq_integ_of_eq:
      "[| v \<in> bin;  w \<in> bin |]
       ==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
           iszero (integ_of (bin_add (v, bin_minus(w))))"
 apply (unfold iszero_def)
 apply (simp add: zcompare_rls integ_of_add integ_of_minus)
 done
 
 lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
 by (unfold iszero_def, simp)
 
 
 lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
 apply (unfold iszero_def)
 apply (simp add: zminus_equation)
 done
 
 lemma iszero_integ_of_BIT:
      "[| w \<in> bin; x \<in> bool |]
       ==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))"
 apply (unfold iszero_def, simp)
 apply (subgoal_tac "integ_of (w) \<in> int")
 apply typecheck
 apply (drule int_cases)
 apply (safe elim!: boolE)
 apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric]
                      int_of_add [symmetric])
 done
 
 lemma iszero_integ_of_0:
      "w \<in> bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))"
 by (simp only: iszero_integ_of_BIT, blast)
 
 lemma iszero_integ_of_1: "w \<in> bin ==> ~ iszero (integ_of (w BIT 1))"
 by (simp only: iszero_integ_of_BIT, blast)
 
 
 
 (** Less-than (<) **)
 
 lemma less_integ_of_eq_neg:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $< integ_of(w)
           \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
 apply (unfold zless_def zdiff_def)
 apply (simp add: integ_of_minus integ_of_add)
 done
 
 lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
 by simp
 
 lemma neg_integ_of_Min: "znegative (integ_of(Min))"
 by simp
 
 lemma neg_integ_of_BIT:
      "[| w \<in> bin; x \<in> bool |]
       ==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))"
 apply simp
 apply (subgoal_tac "integ_of (w) \<in> int")
 apply typecheck
 apply (drule int_cases)
 apply (auto elim!: boolE simp add: int_of_add [symmetric]  zcompare_rls)
 apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def
                      int_of_add [symmetric])
 apply (subgoal_tac "$#1 $- $# succ (succ (n #+ n)) = $- $# succ (n #+ n) ")
  apply (simp add: zdiff_def)
 apply (simp add: equation_zminus int_of_diff [symmetric])
 done
 
 (** Less-than-or-equals (<=) **)
 
 lemma le_integ_of_eq_not_less:
      "(integ_of(x) $\<le> (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) $< (integ_of(x)))"
 by (simp add: not_zless_iff_zle [THEN iff_sym])
 
 
 (*Delete the original rewrites, with their clumsy conditional expressions*)
 declare bin_succ_BIT [simp del]
         bin_pred_BIT [simp del]
         bin_minus_BIT [simp del]
         NCons_Pls [simp del]
         NCons_Min [simp del]
         bin_adder_BIT [simp del]
         bin_mult_BIT [simp del]
 
 (*Hide the binary representation of integer constants*)
 declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del]
 
 
 lemmas bin_arith_extra_simps =
      integ_of_add [symmetric]
      integ_of_minus [symmetric]
      integ_of_mult [symmetric]
      bin_succ_1 bin_succ_0
      bin_pred_1 bin_pred_0
      bin_minus_1 bin_minus_0
      bin_add_Pls_right bin_add_Min_right
      bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
      diff_integ_of_eq
      bin_mult_1 bin_mult_0 NCons_simps
 
 
 (*For making a minimal simpset, one must include these default simprules
   of thy.  Also include simp_thms, or at least (~False)=True*)
 lemmas bin_arith_simps =
      bin_pred_Pls bin_pred_Min
      bin_succ_Pls bin_succ_Min
      bin_add_Pls bin_add_Min
      bin_minus_Pls bin_minus_Min
      bin_mult_Pls bin_mult_Min
      bin_arith_extra_simps
 
 (*Simplification of relational operations*)
 lemmas bin_rel_simps =
      eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min
      iszero_integ_of_0 iszero_integ_of_1
      less_integ_of_eq_neg
      not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT
      le_integ_of_eq_not_less
 
 declare bin_arith_simps [simp]
 declare bin_rel_simps [simp]
 
 
 (** Simplification of arithmetic when nested to the right **)
 
 lemma add_integ_of_left [simp]:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)"
 by (simp add: zadd_assoc [symmetric])
 
 lemma mult_integ_of_left [simp]:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)"
 by (simp add: zmult_assoc [symmetric])
 
 lemma add_integ_of_diff1 [simp]:
     "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)"
 apply (unfold zdiff_def)
 apply (rule add_integ_of_left, auto)
 done
 
 lemma add_integ_of_diff2 [simp]:
      "[| v \<in> bin;  w \<in> bin |]
       ==> integ_of(v) $+ (c $- integ_of(w)) =
           integ_of (bin_add (v, bin_minus(w))) $+ (c)"
 apply (subst diff_integ_of_eq [symmetric])
 apply (simp_all add: zdiff_def zadd_ac)
 done
 
 
 (** More for integer constants **)
 
 declare int_of_0 [simp] int_of_succ [simp]
 
 lemma zdiff0 [simp]: "#0 $- x = $-x"
 by (simp add: zdiff_def)
 
 lemma zdiff0_right [simp]: "x $- #0 = intify(x)"
 by (simp add: zdiff_def)
 
 lemma zdiff_self [simp]: "x $- x = #0"
 by (simp add: zdiff_def)
 
 lemma znegative_iff_zless_0: "k \<in> int ==> znegative(k) \<longleftrightarrow> k $< #0"
 by (simp add: zless_def)
 
 lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k \<in> int|] ==> znegative($-k)"
 by (simp add: zless_def)
 
 lemma zero_zle_int_of [simp]: "#0 $\<le> $# n"
 by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
 
 lemma nat_of_0 [simp]: "nat_of(#0) = 0"
 by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
 
 lemma nat_le_int0_lemma: "[| z $\<le> $#0; z \<in> int |] ==> nat_of(z) = 0"
 by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of)
 
 lemma nat_le_int0: "z $\<le> $#0 ==> nat_of(z) = 0"
 apply (subgoal_tac "nat_of (intify (z)) = 0")
 apply (rule_tac [2] nat_le_int0_lemma, auto)
 done
 
 lemma int_of_eq_0_imp_natify_eq_0: "$# n = #0 ==> natify(n) = 0"
 by (rule not_znegative_imp_zero, auto)
 
 lemma nat_of_zminus_int_of: "nat_of($- $# n) = 0"
 by (simp add: nat_of_def int_of_def raw_nat_of zminus image_intrel_int)
 
 lemma int_of_nat_of: "#0 $\<le> z ==> $# nat_of(z) = intify(z)"
 apply (rule not_zneg_nat_of_intify)
 apply (simp add: znegative_iff_zless_0 not_zless_iff_zle)
 done
 
 declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
 
 lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $\<le> z then intify(z) else #0)"
 by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
 
 lemma zless_nat_iff_int_zless: "[| m \<in> nat; z \<in> int |] ==> (m < nat_of(z)) \<longleftrightarrow> ($#m $< z)"
 apply (case_tac "znegative (z) ")
 apply (erule_tac [2] not_zneg_nat_of [THEN subst])
 apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
             simp add: znegative_iff_zless_0)
 done
 
 
 (** nat_of and zless **)
 
 (*An alternative condition is  @{term"$#0 \<subseteq> w"}  *)
 lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w $< z)"
 apply (rule iff_trans)
 apply (rule zless_int_of [THEN iff_sym])
 apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
 apply (auto elim: zless_asym simp add: not_zle_iff_zless)
 apply (blast intro: zless_zle_trans)
 done
 
 lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> ($#0 $< z & w $< z)"
 apply (case_tac "$#0 $< z")
 apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
 done
 
 (*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
   unconditional!
   [The condition "True" is a hack to prevent looping.
     Conditional rewrite rules are tried after unconditional ones, so a rule
     like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
   lemma integ_of_reorient [simp]:
        "True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))"
   by auto
 *)
 
 lemma integ_of_minus_reorient [simp]:
      "(integ_of(w) = $- x) \<longleftrightarrow> ($- x = integ_of(w))"
 by auto
 
 lemma integ_of_add_reorient [simp]:
      "(integ_of(w) = x $+ y) \<longleftrightarrow> (x $+ y = integ_of(w))"
 by auto
 
 lemma integ_of_diff_reorient [simp]:
      "(integ_of(w) = x $- y) \<longleftrightarrow> (x $- y = integ_of(w))"
 by auto
 
 lemma integ_of_mult_reorient [simp]:
      "(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))"
 by auto
 
 (** To simplify inequalities involving integer negation and literals,
     such as -x = #3
 **)
 
 lemmas [simp] =
   zminus_equation [where y = "integ_of(w)"]
   equation_zminus [where x = "integ_of(w)"]
   for w
 
 lemmas [iff] =
   zminus_zless [where y = "integ_of(w)"]
   zless_zminus [where x = "integ_of(w)"]
   for w
 
 lemmas [iff] =
   zminus_zle [where y = "integ_of(w)"]
   zle_zminus [where x = "integ_of(w)"]
   for w
 
 lemmas [simp] =
   Let_def [where s = "integ_of(w)"] for w
 
 
 (*** Simprocs for numeric literals ***)
 
 (** Combining of literal coefficients in sums of products **)
 
 lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
   by (simp add: zcompare_rls)
 
 lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
   by (simp add: zcompare_rls)
 
 lemma zle_iff_zdiff_zle_0: "(x $\<le> y) \<longleftrightarrow> (x$-y $\<le> #0)"
   by (simp add: zcompare_rls)
 
 
 (** For combine_numerals **)
 
 lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"
   by (simp add: zadd_zmult_distrib zadd_ac)
 
 
 (** For cancel_numerals **)
 
 lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 context fixes n :: i
 begin
 
 lemmas rel_iff_rel_0_rls =
   zless_iff_zdiff_zless_0 [where y = "u $+ v"]
   eq_iff_zdiff_eq_0 [where y = "u $+ v"]
   zle_iff_zdiff_zle_0 [where y = "u $+ v"]
   zless_iff_zdiff_zless_0 [where y = n]
   eq_iff_zdiff_eq_0 [where y = n]
   zle_iff_zdiff_zle_0 [where y = n]
   for u v
 
 lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
 
 lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
 
 end
 
 lemma le_add_iff1: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $\<le> n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 lemma le_add_iff2: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> (m $\<le> (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
 ML_file \<open>int_arith.ML\<close>
 
 subsection \<open>examples:\<close>
 
 text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close>
 lemma "#5 $* x $* #3 = y" apply simp oops
 
 schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops
 
 lemma "oo : int ==> l $+ (l $+ #2) $+ oo = oo" apply simp oops
 
 lemma "#9$*x $+ y = x$*#23 $+ z" apply simp oops
 lemma "y $+ x = x $+ z" apply simp oops
 
 lemma "x : int ==> x $+ y $+ z = x $+ z" apply simp oops
 lemma "x : int ==> y $+ (z $+ x) = z $+ x" apply simp oops
 lemma "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)" apply simp oops
 lemma "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)" apply simp oops
 
 lemma "#-3 $* x $+ y $\<le> x $* #2 $+ z" apply simp oops
 lemma "y $+ x $\<le> x $+ z" apply simp oops
 lemma "x $+ y $+ z $\<le> x $+ z" apply simp oops
 
 lemma "y $+ (z $+ x) $< z $+ x" apply simp oops
 lemma "x $+ y $+ z $< (z $+ y) $+ (x $+ w)" apply simp oops
 lemma "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)" apply simp oops
 
 lemma "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu" apply simp oops
 lemma "u : int ==> #2 $* u = u" apply simp oops
 lemma "(i $+ j $+ #12 $+ k) $- #15 = y" apply simp oops
 lemma "(i $+ j $+ #12 $+ k) $- #5 = y" apply simp oops
 
 lemma "y $- b $< b" apply simp oops
 lemma "y $- (#3 $* b $+ c) $< b $- #2 $* c" apply simp oops
 
 lemma "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w" apply simp oops
 lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w" apply simp oops
 lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w" apply simp oops
 lemma "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w" apply simp oops
 
 lemma "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y" apply simp oops
 lemma "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y" apply simp oops
 
 lemma "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv" apply simp oops
 
 lemma "a $+ $-(b$+c) $+ b = d" apply simp oops
 lemma "a $+ $-(b$+c) $- b = d" apply simp oops
 
 text \<open>negative numerals\<close>
 lemma "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz" apply simp oops
 lemma "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y" apply simp oops
 lemma "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y" apply simp oops
 lemma "(i $+ j $+ #-12 $+ k) $- #15 = y" apply simp oops
 lemma "(i $+ j $+ #12 $+ k) $- #-15 = y" apply simp oops
 lemma "(i $+ j $+ #-12 $+ k) $- #-15 = y" apply simp oops
 
 text \<open>Multiplying separated numerals\<close>
 lemma "#6 $* ($# x $* #2) =  uu" apply simp oops
 lemma "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu" apply simp oops
 
 end