# HG changeset patch
# User nipkow
# Date 1510661568 -3600
# Node ID b5c1f0c76d3507111b2e81bafe2f2e523d15c54e
# Parent  f11486d3158630349ae9ef9b6e6221f4dabb2c58# Parent  a462583f0a37dde46b4364e9e10d93f1e29f264d
merged

diff -r a462583f0a37 -r b5c1f0c76d35 NEWS
--- a/NEWS	Tue Nov 14 13:12:13 2017 +0100
+++ b/NEWS	Tue Nov 14 13:12:48 2017 +0100
@@ -89,7 +89,10 @@
 * Class linordered_semiring_1 covers zero_less_one also, ruling out
 pathologic instances. Minor INCOMPATIBILITY.
 
-* Removed nat-int transfer machinery.  Rare INCOMPATIBILITY.
+* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
+
+* Predicate coprime is now a real definition, not a mere
+abbreviation. INCOMPATIBILITY.
 
 
 *** System ***
@@ -98,6 +101,12 @@
 for this session. There is no need to specify options [document = false]
 anymore.
 
+* The command-line tool "isabelle mkroot" now always produces a document
+outline: its options have been adapted accordingly. INCOMPATIBILITY.
+
+* The command-line tool "isabelle mkroot -I" initializes a Mercurial
+repository for the generated session files.
+
 * Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
 support has been discontinued.
 
diff -r a462583f0a37 -r b5c1f0c76d35 lib/Tools/mkroot
--- a/lib/Tools/mkroot	Tue Nov 14 13:12:13 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: prepare session root directory
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
-  echo
-  echo "  Options are:"
-  echo "    -d           enable document preparation"
-  echo "    -n NAME      alternative session name (default: DIR base name)"
-  echo
-  echo "  Prepare session root DIR (default: current directory)."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-DOC=""
-NAME=""
-
-while getopts "n:d" OPT
-do
-  case "$OPT" in
-    d)
-      DOC="true"
-      ;;
-    n)
-      NAME="$OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-if [ "$#" -eq 0 ]; then
-  DIR="."
-elif [ "$#" -eq 1 ]; then
-  DIR="$1"
-  shift
-else
-  usage
-fi
-
-
-## main
-
-mkdir -p "$DIR" || fail "Bad directory: \"$DIR\""
-
-[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"
-
-[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT"
-
-[ "$DOC" = true -a -e "$DIR/document" ] && \
-  fail "Cannot overwrite existing $DIR/document"
-
-echo
-echo "Preparing session \"$NAME\" in \"$DIR\""
-
-
-# ROOT
-
-echo "  creating $DIR/ROOT"
-
-if [ "$DOC" = true ]; then
-  cat > "$DIR/ROOT" <<EOF
-session "$NAME" = "$ISABELLE_LOGIC" +
-  options [document = pdf, document_output = "output"]
-  theories [document = false]
-    (* Foo *)
-    (* Bar *)
-  theories
-    (* Baz *)
-  document_files
-    "root.tex"
-EOF
-else
-  cat > "$DIR/ROOT" <<EOF
-session "$NAME" = "$ISABELLE_LOGIC" +
-  theories
-    (* Foo *)
-    (* Bar *)
-    (* Baz *)
-EOF
-fi
-
-
-# document directory
-
-if [ "$DOC" = true ]; then
-  echo "  creating $DIR/document/root.tex"
-
-  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
-  
-  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
-  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
-
-  cat > "$DIR/document/root.tex" <<EOF
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
-%\usepackage{amssymb}
-  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
-  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
-  %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage{eurosym}
-  %for \<euro>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
-  %for \<Sqinter>
-
-%\usepackage{eufrak}
-  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
-  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
-  %\<currency>
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
-
-
-\begin{document}
-
-\title{$TITLE}
-\author{$AUTHOR}
-\maketitle
-
-\tableofcontents
-
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
-
-% generated text of all theories
-\input{session}
-
-% optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-EOF
-fi
-
-# notes
-
-declare -a DIR_PARTS=($DIR)
-if [ ${#DIR_PARTS[@]} = 1 ]; then
-  OPT_DIR="-D $DIR"
-else
-  OPT_DIR="-D \"$DIR\""
-fi
-
-cat <<EOF
-
-Now use the following command line to build the session:
-
-  isabelle build $OPT_DIR
-
-EOF
-
diff -r a462583f0a37 -r b5c1f0c76d35 src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Doc/Corec/Corec.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -334,9 +334,9 @@
           primes m (n + 1))"
       apply (relation "measure (\<lambda>(m, n).
         if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
-       apply (auto simp: mod_Suc intro: Suc_lessI)
-       apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
-      by (metis diff_less_mono2 lessI mod_less_divisor)
+       apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
+      apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
+      done
 
 text \<open>
 \noindent
diff -r a462583f0a37 -r b5c1f0c76d35 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Doc/System/Environment.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -58,7 +58,7 @@
     \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
     exists) is run in the same way as the site default settings. Note that the
     variable @{setting ISABELLE_HOME_USER} has already been set before ---
-    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
+    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2017\<close>.
 
     Thus individual users may override the site-wide defaults. Typically, a
     user settings file contains only a few lines, with some assignments that
diff -r a462583f0a37 -r b5c1f0c76d35 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Doc/System/Presentation.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -94,45 +94,51 @@
   The @{tool_def mkroot} tool configures a given directory as session root,
   with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is:
   @{verbatim [display]
-\<open>Usage: isabelle mkroot [OPTIONS] [DIR]
+\<open>Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
 
   Options are:
-    -d           enable document preparation
-    -n NAME      alternative session name (default: DIR base name)
+    -A LATEX     provide author in LaTeX notation (default: user name)
+    -I           init Mercurial repository and add generated files
+    -T LATEX     provide title in LaTeX notation (default: session name)
+    -n NAME      alternative session name (default: directory base name)
 
-  Prepare session root DIR (default: current directory).\<close>}
+  Prepare session root directory (default: current directory).
+\<close>}
 
   The results are placed in the given directory \<open>dir\<close>, which refers to the
   current directory by default. The @{tool mkroot} tool is conservative in the
   sense that it does not overwrite existing files or directories. Earlier
   attempts to generate a session root need to be deleted manually.
 
-  \<^medskip>
-  Option \<^verbatim>\<open>-d\<close> indicates that the session shall be accompanied by a formal
-  document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see
-  also \chref{ch:present}).
+  The generated session template will be accompanied by a formal document,
+  with \<open>DIRECTORY\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also
+  \chref{ch:present}).
 
-  Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
-  base name of the given directory is used.
+  Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
+  using {\LaTeX} source notation.
+
+  Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and
+  adds all generated files (without commit).
+
+  Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
+  of the given directory is used.
 
   \<^medskip>
   The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
-  the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document
-  format to be filled filled into the generated \<^verbatim>\<open>ROOT\<close> file.
+  the parent session.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Produce session \<^verbatim>\<open>Test\<close> (with document preparation) within a separate
-  directory of the same name:
-  @{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
+  Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name:
+  @{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>}
 
   \<^medskip>
   Upgrade the current directory into a session ROOT with document preparation,
   and build it:
-  @{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
+  @{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>}
 \<close>
 
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -351,7 +351,7 @@
   preparation) may be produced as follows:
 
 \begin{verbatim}
-  isabelle mkroot -d MySession
+  isabelle mkroot MySession
   isabelle build -D MySession
 \end{verbatim}
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -139,7 +139,7 @@
 
 (* Deviates from the definition given in the library in number theory *)
 definition phi' :: "nat => nat"
-  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
+  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
 
 notation (latex output)
   phi' ("\<phi> _")
@@ -148,8 +148,8 @@
   assumes "m > 0"
   shows "phi' m > 0"
 proof -
-  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" using assms by simp
-  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)
+  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" using assms by simp
+  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m} > 0" by (auto simp: card_gt_0_iff)
   thus ?thesis unfolding phi'_def by simp
 qed
 
@@ -232,7 +232,7 @@
           by (simp add: gcd_mult_distrib_nat q ac_simps)
         hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
         hence "a * n div d \<in> ?F"
-          using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel)
+          using ge_1 le_n by (fastforce simp add: `d dvd n`)
       } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
       { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
         hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
@@ -256,7 +256,7 @@
     proof
       fix m assume m: "m \<in> ?R"
       thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
-        by (simp add: dvd_mult_div_cancel)
+        by simp
     qed
   qed fastforce
   finally show ?thesis by force
@@ -329,7 +329,7 @@
 lemma ord_min:
   assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
 proof -
-  def Ord \<equiv> "{d \<in> {1..order G}. a (^) d = \<one>}"
+  define Ord where "Ord = {d \<in> {1..order G}. a (^) d = \<one>}"
   have fin: "finite Ord" by (auto simp: Ord_def)
   have in_ord: "ord a \<in> Ord"
     using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
@@ -411,7 +411,7 @@
   show "?R \<subseteq> ?L" by blast
   { fix y assume "y \<in> ?L"
     then obtain x::nat where x:"y = a(^)x" by auto
-    def r \<equiv> "x mod ord a"
+    define r where "r = x mod ord a"
     then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
     hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
       using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
@@ -427,7 +427,7 @@
   assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
   shows "ord a dvd k"
 proof -
-  def r \<equiv> "k mod ord a"
+  define r where "r = k mod ord a"
   then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
   hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
       using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
@@ -486,15 +486,16 @@
     proof -
       have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"
         using div_gcd_coprime[of n "ord a"] ge_1 by fastforce
-      thus ?thesis by (simp add: gcd.commute)
+      thus ?thesis by (simp add: ac_simps)
     qed
     have dvd_d:"(ord a div gcd n (ord a)) dvd d"
     proof -
       have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq
         by (metis dvd_triv_right mult.commute)
       hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"
-        by (simp add:  mult.commute)
-      thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce
+        by (simp add: mult.commute)
+      then show ?thesis
+        using cp by (simp add: coprime_dvd_mult_left_iff)
     qed
     have "d > 0" using d_elem by simp
     hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
@@ -744,7 +745,8 @@
   shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
 proof
   assume A: ?L then show ?R
-    using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)
+    using assms ord_ge_1 [OF assms]
+    by (auto simp: nat_div_eq ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1)
 next
   assume ?R then show ?L
     using ord_pow_dvd_ord_elem[OF assms, of k] by auto
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -13,12 +13,6 @@
 
 subsection \<open>Irreducible and prime elements\<close>
 
-(* TODO: Move ? *)
-lemma (in semiring_gcd) prod_coprime' [rule_format]: 
-    "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1"
-  using prod_coprime[of A f a] by (simp add: gcd.commute)
-
-
 context comm_semiring_1
 begin
 
@@ -583,7 +577,7 @@
 end
 
 
-subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
+subsection \<open>In a semiring with GCD, each irreducible element is a prime element\<close>
 
 context semiring_gcd
 begin
@@ -620,23 +614,26 @@
   using assms by (simp add: prime_elem_imp_coprime)
 
 lemma prime_elem_imp_power_coprime:
-  "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
-  by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
+  "prime_elem p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
+  by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps)
 
 lemma prime_imp_power_coprime:
-  "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
-  by (simp add: prime_elem_imp_power_coprime)
+  "prime p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
+  by (rule prime_elem_imp_power_coprime) simp_all
 
 lemma prime_elem_divprod_pow:
   assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   shows   "p^n dvd a \<or> p^n dvd b"
   using assms
 proof -
-  from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
-    by (auto simp: coprime prime_elem_def)
-  with p have "coprime (p^n) a \<or> coprime (p^n) b"
-    by (auto intro: prime_elem_imp_coprime coprime_exp_left)
-  with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
+  from p have "\<not> is_unit p"
+    by simp
+  with ab p have "\<not> p dvd a \<or> \<not> p dvd b"
+    using not_coprimeI by blast
+  with p have "coprime (p ^ n) a \<or> coprime (p ^ n) b"
+    by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps)
+  with pab show ?thesis
+    by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff)
 qed
 
 lemma primes_coprime:
@@ -1524,6 +1521,27 @@
     with assms[of P] assms[of Q] PQ show "P = Q" by simp
 qed
 
+lemma divides_primepow:
+  assumes "prime p" and "a dvd p ^ n"
+  obtains m where "m \<le> n" and "normalize a = p ^ m"
+proof -
+  from assms have "a \<noteq> 0"
+    by auto
+  with assms
+  have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))"
+    by (simp add: prod_mset_prime_factorization)
+  then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)"
+    by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff)
+  with assms have "prime_factorization a \<subseteq># replicate_mset n p"
+    by (simp add: prime_factorization_prime_power)
+  then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p"
+    by (rule msubseteq_replicate_msetE)
+  then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)"
+    by simp
+  with \<open>a \<noteq> 0\<close> have "normalize a = p ^ m"
+    by (simp add: prod_mset_prime_factorization)
+  with \<open>m \<le> n\<close> show thesis ..
+qed
 
 
 subsection \<open>GCD and LCM computation with unique factorizations\<close>
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -16,6 +16,15 @@
   "normalize_quot = 
      (\<lambda>(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))" 
 
+lemma normalize_quot_zero [simp]:
+  "normalize_quot (a, 0) = (0, 1)"
+  by (simp add: normalize_quot_def)
+
+lemma normalize_quot_proj [simp]:
+  "fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
+  "snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
+  using that by (simp_all add: normalize_quot_def Let_def mult.commute [of _ "unit_factor b"] dvd_div_mult2_eq mult_unit_dvd_iff')
+
 definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where
   "normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}"
   
@@ -61,8 +70,8 @@
   
 lemma coprime_normalize_quot:
   "coprime (fst (normalize_quot x)) (snd (normalize_quot x))"
-  by (simp add: normalize_quot_def case_prod_unfold Let_def
-        div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime)
+  by (simp add: normalize_quot_def case_prod_unfold div_mult_unit2)
+    (metis coprime_mult_self_right_iff div_gcd_coprime unit_div_mult_self unit_factor_is_unit)
 
 lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts"
   by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold)
@@ -203,15 +212,26 @@
      and  "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))"
   shows   "normalize_quot (a * c, b * d) = (e * g, f * h)"
 proof (rule normalize_quotI)
+  from assms have "gcd a b = 1" "gcd c d = 1"
+    by simp_all
   from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
-  from normalize_quotE[OF \<open>b \<noteq> 0\<close>, of c] guess k . note k = this [folded assms]
-  from normalize_quotE[OF \<open>d \<noteq> 0\<close>, of a] guess l . note l = this [folded assms]
-  from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all)
+  with assms have "normalize b = b" "normalize d = d"
+    by (auto intro: normalize_unit_factor_eqI)
+  from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] guess k .
+  note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
+  from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] guess l .
+  note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
+  from k l show "a * c * (f * h) = b * d * (e * g)"
+    by (metis e_def f_def g_def h_def mult.commute mult.left_commute)
   from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1"
     by simp_all
   from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot)
-  with k l assms(1,2) show "(e * g, f * h) \<in> normalized_fracts"
-    by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq')
+  with k l assms(1,2) \<open>b \<noteq> 0\<close> \<open>d \<noteq> 0\<close> \<open>unit_factor b = 1\<close> \<open>unit_factor d = 1\<close>
+    \<open>normalize b = b\<close> \<open>normalize d = d\<close>
+  show "(e * g, f * h) \<in> normalized_fracts"
+    by (simp add: normalized_fracts_def unit_factor_mult e_def f_def g_def h_def
+      coprime_normalize_quot dvd_unit_factor_div unit_factor_gcd)
+      (metis coprime_mult_left_iff coprime_mult_right_iff)
 qed (insert assms(3,4), auto)
 
 lemma normalize_quot_mult:
@@ -230,8 +250,8 @@
      (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
           (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b)
       in  (e*g, f*h))"
-  by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric]
-                 coprime_normalize_quot normalize_quot_mult [symmetric])
+  by transfer
+     (simp add: split_def Let_def coprime_normalize_quot normalize_quot_mult normalize_quot_mult_coprime)
   
 lemma normalize_quot_0 [simp]: 
     "normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)"
@@ -254,7 +274,9 @@
     by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
   have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
   thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
-    using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute)
+    using assms(1,2) d
+    by (auto simp: normalized_fracts_def ac_simps)
+      (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
 qed fact+
   
 lemma quot_of_fract_inverse:
@@ -274,12 +296,19 @@
   shows "normalize_quot (x div u, y) = (x' div u, y')"
 proof (cases "y = 0")
   case False
-  from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
-  from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
-  with False d \<open>is_unit u\<close> show ?thesis
-    by (intro normalize_quotI)
-       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
-          gcd_div_unit1)
+  define v where "v = 1 div u"
+  with \<open>is_unit u\<close> have "is_unit v" and u: "\<And>a. a div u = a * v"
+    by simp_all
+  from \<open>is_unit v\<close> have "coprime v = top"
+    by (simp add: fun_eq_iff is_unit_left_imp_coprime)
+  from normalize_quotE[OF False, of x] guess d .
+  note d = this[folded assms(2,3)]
+  from assms have "coprime x' y'" "unit_factor y' = 1"
+    by (simp_all add: coprime_normalize_quot)
+  with d \<open>coprime v = top\<close> have "normalize_quot (x * v, y) = (x' * v, y')"
+    by (auto simp: normalized_fracts_def intro: normalize_quotI)
+  then show ?thesis
+    by (simp add: u)
 qed (simp_all add: assms)
 
 lemma normalize_quot_div_unit_right:
@@ -291,10 +320,8 @@
   case False
   from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
   from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
-  with False d \<open>is_unit u\<close> show ?thesis
-    by (intro normalize_quotI)
-       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
-          gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric])
+  with d \<open>is_unit u\<close> show ?thesis
+    by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI)
 qed (simp_all add: assms)
 
 lemma normalize_quot_normalize_left:
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Computational_Algebra/Nth_Powers.thy
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -111,9 +111,10 @@
     ultimately show "n dvd multiplicity p a"
       by (auto simp: not_dvd_imp_multiplicity_0)
   qed
-  from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
-  from A[of b a] assms show "is_nth_power n b" 
-    by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
+  from A [of a b] assms show "is_nth_power n a"
+    by (cases "n = 0") simp_all
+  from A [of b a] assms show "is_nth_power n b"
+    by (cases "n = 0") (simp_all add: ac_simps)
 qed
     
 lemma is_nth_power_mult_coprime_nat_iff:
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -171,7 +171,7 @@
   hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
   hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
   moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
-    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
+    by (simp_all add: a_def b_def coprime_quot_of_fract [of c] ac_simps
           normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
   ultimately show ?thesis by (intro that[of a b])
 qed
@@ -513,9 +513,12 @@
    from fract_poly_smult_eqE[OF this] guess a b . note ab = this
    hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
    with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
-   hence "normalize b = gcd a b" by simp
-   also from ab(3) have "\<dots> = 1" .
-   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
+   then have "normalize b = gcd a b"
+     by simp
+   with \<open>coprime a b\<close> have "normalize b = 1"
+     by simp
+   then have "a = 1" "is_unit b"
+     by (simp_all add: a normalize_1_iff)
    
    note eq
    also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
@@ -676,7 +679,8 @@
     from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
     from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
     with assms content_e have "a = normalize b" by (simp add: ab(4))
-    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
+    with ab have ab': "a = 1" "is_unit b"
+      by (simp_all add: normalize_1_iff)
     with ab ab' have "c' = to_fract b" by auto
     from this and \<open>is_unit b\<close> show ?thesis by (rule that)
   qed
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -245,9 +245,9 @@
   using prime_power_cancel [OF assms] assms by auto
 
 lemma prime_power_canonical:
-  fixes m::nat
+  fixes m :: nat
   assumes "prime p" "m > 0"
-  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
+  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p ^ k"
 using \<open>m > 0\<close>
 proof (induction m rule: less_induct)
   case (less m)
@@ -381,9 +381,9 @@
 
 (* TODO: Generalise? *)
 lemma prime_power_mult_nat:
-  fixes p::nat
+  fixes p :: nat
   assumes p: "prime p" and xy: "x * y = p ^ k"
-  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
+  shows "\<exists>i j. x = p ^ i \<and> y = p^ j"
 using xy
 proof(induct k arbitrary: x y)
   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
@@ -429,25 +429,10 @@
 qed
 
 lemma divides_primepow_nat:
-  fixes p::nat
+  fixes p :: nat
   assumes p: "prime p"
-  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
-proof
-  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
-    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
-  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
-  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
-  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
-  hence "i \<le> k" by arith
-  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
-next
-  {fix i assume H: "i \<le> k" "d = p^i"
-    then obtain j where j: "k = i + j"
-      by (metis le_add_diff_inverse)
-    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
-    hence "d dvd p^k" unfolding dvd_def by auto}
-  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
-qed
+  shows "d dvd p ^ k \<longleftrightarrow> (\<exists>i\<le>k. d = p ^ i)"
+  using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
 
 
 subsection \<open>Chinese Remainder Theorem Variants\<close>
@@ -481,8 +466,8 @@
   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
-  then have d12: "d1 = 1" "d2 =1"
-    by (metis ab coprime_nat)+
+  then have d12: "d1 = 1" "d2 = 1"
+    using ab coprime_common_divisor_nat [of a b] by blast+
   let ?x = "v * a * x1 + u * b * x2"
   let ?q1 = "v * x1 + u * y2"
   let ?q2 = "v * y1 + u * x2"
@@ -497,14 +482,14 @@
 lemma coprime_bezout_strong:
   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
   shows "\<exists>x y. a * x = b * y + 1"
-by (metis assms bezout_nat gcd_nat.left_neutral)
+  by (metis add.commute add.right_neutral assms(1) assms(2) chinese_remainder coprime_1_left coprime_1_right coprime_crossproduct_nat mult.commute mult.right_neutral mult_cancel_left)
 
 lemma bezout_prime:
   assumes p: "prime p" and pa: "\<not> p dvd a"
   shows "\<exists>x y. a*x = Suc (p*y)"
 proof -
   have ap: "coprime a p"
-    by (metis gcd.commute p pa prime_imp_coprime)
+    using coprime_commute p pa prime_imp_coprime by auto
   moreover from p have "p \<noteq> 1" by auto
   ultimately have "\<exists>x y. a * x = p * y + 1"
     by (rule coprime_bezout_strong)
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Computational_Algebra/Squarefree.thy
--- a/src/HOL/Computational_Algebra/Squarefree.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Squarefree.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -116,13 +116,16 @@
   show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
   proof
     fix p assume p: "p \<in> prime_factors (a * b)"
-    {
+    with nz have "prime p"
+      by (simp add: prime_factors_dvd)
+    have "\<not> (p dvd a \<and> p dvd b)"
+    proof
       assume "p dvd a \<and> p dvd b"
-      hence "p dvd gcd a b" by simp
-      also have "gcd a b = 1" by fact
-      finally have False using nz using p by (auto simp: prime_factors_dvd)
-    }
-    hence "\<not>(p dvd a \<and> p dvd b)" by blast
+      with \<open>coprime a b\<close> have "is_unit p"
+        by (auto intro: coprime_common_divisor)
+      with \<open>prime p\<close> show False
+        by simp
+    qed
     moreover from p have "p dvd a \<or> p dvd b" using nz 
       by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
     ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
@@ -138,7 +141,7 @@
   shows   "squarefree (prod f A)"
   using assms 
   by (induction A rule: infinite_finite_induct) 
-     (auto intro!: squarefree_mult_coprime prod_coprime')
+     (auto intro!: squarefree_mult_coprime prod_coprime_right)
 
 lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
   by (cases m) (auto dest: squarefree_multD)
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Corec_Examples/Paper_Examples.thy
--- a/src/HOL/Corec_Examples/Paper_Examples.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -96,9 +96,9 @@
 where "primes m n =
   (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
 apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
-apply (auto simp: mod_Suc intro: Suc_lessI )
-apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
-by (metis diff_less_mono2 lessI mod_less_divisor)
+   apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
+   apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
+  done
 
 corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
 where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Decision_Procs/Rat_Pair.thy
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -51,7 +51,8 @@
     from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
     have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
     from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
-    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
+    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1"
+      by simp
     from ab consider "b < 0" | "b > 0" by arith
     then show ?thesis
     proof cases
@@ -198,6 +199,8 @@
     from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
     have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
       by (simp_all add: x y isnormNum_def add: gcd.commute)
+    then have "coprime a b" "coprime b a" "coprime a' b'" "coprime b' a'"
+      by (simp_all add: coprime_iff_gcd_eq_1)
     from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
       apply -
       apply algebra
@@ -205,11 +208,11 @@
       apply simp
       apply algebra
       done
-    from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
-        coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
-      have eq1: "b = b'" using pos by arith
-      with eq have "a = a'" using pos by simp
-      with eq1 show ?thesis by (simp add: x y)
+    then have eq1: "b = b'"
+      using pos \<open>coprime b a\<close> \<open>coprime b' a'\<close>
+      by (auto simp add: coprime_dvd_mult_left_iff intro: associated_eqI)
+    with eq have "a = a'" using pos by simp
+    with \<open>b = b'\<close> show ?thesis by (simp add: x y)
   qed
   show ?lhs if ?rhs
     using that by simp
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Euclidean_Division.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -125,6 +125,15 @@
   "a mod b = 0" if "is_unit b"
   using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
 
+lemma coprime_mod_left_iff [simp]:
+  "coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
+  by (rule; rule coprimeI)
+    (use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>)
+
+lemma coprime_mod_right_iff [simp]:
+  "coprime a (b mod a) \<longleftrightarrow> coprime a b" if "a \<noteq> 0"
+  using that coprime_mod_left_iff [of a b] by (simp add: ac_simps)
+
 end
 
 class euclidean_ring = idom_modulo + euclidean_semiring
@@ -533,6 +542,10 @@
   with that show thesis .
 qed
 
+lemma invertible_coprime:
+  "coprime a c" if "a * b mod c = 1"
+  by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto)
+
 end
 
   
@@ -772,6 +785,18 @@
 
 end
 
+lemma coprime_Suc_0_left [simp]:
+  "coprime (Suc 0) n"
+  using coprime_1_left [of n] by simp
+
+lemma coprime_Suc_0_right [simp]:
+  "coprime n (Suc 0)"
+  using coprime_1_right [of n] by simp
+
+lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+  for a b :: nat
+  by (drule coprime_common_divisor [of _ _ x]) simp_all
+
 instantiation nat :: unique_euclidean_semiring
 begin
 
@@ -1422,6 +1447,64 @@
 
 end
 
+lemma coprime_int_iff [simp]:
+  "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  show ?Q
+  proof (rule coprimeI)
+    fix q
+    assume "q dvd m" "q dvd n"
+    then have "int q dvd int m" "int q dvd int n"
+      by (simp_all add: zdvd_int)
+    with \<open>?P\<close> have "is_unit (int q)"
+      by (rule coprime_common_divisor)
+    then show "is_unit q"
+      by simp
+  qed
+next
+  assume ?Q
+  show ?P
+  proof (rule coprimeI)
+    fix k
+    assume "k dvd int m" "k dvd int n"
+    then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
+      by (simp_all add: zdvd_int)
+    with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
+      by (rule coprime_common_divisor)
+    then show "is_unit k"
+      by simp
+  qed
+qed
+
+lemma coprime_abs_left_iff [simp]:
+  "coprime \<bar>k\<bar> l \<longleftrightarrow> coprime k l" for k l :: int
+  using coprime_normalize_left_iff [of k l] by simp
+
+lemma coprime_abs_right_iff [simp]:
+  "coprime k \<bar>l\<bar> \<longleftrightarrow> coprime k l" for k l :: int
+  using coprime_abs_left_iff [of l k] by (simp add: ac_simps)
+
+lemma coprime_nat_abs_left_iff [simp]:
+  "coprime (nat \<bar>k\<bar>) n \<longleftrightarrow> coprime k (int n)"
+proof -
+  define m where "m = nat \<bar>k\<bar>"
+  then have "\<bar>k\<bar> = int m"
+    by simp
+  moreover have "coprime k (int n) \<longleftrightarrow> coprime \<bar>k\<bar> (int n)"
+    by simp
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma coprime_nat_abs_right_iff [simp]:
+  "coprime n (nat \<bar>k\<bar>) \<longleftrightarrow> coprime (int n) k"
+  using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps)
+
+lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
+  for a b :: int
+  by (drule coprime_common_divisor [of _ _ x]) simp_all
+
 instantiation int :: idom_modulo
 begin
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/GCD.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -142,12 +142,6 @@
 class gcd = zero + one + dvd +
   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-begin
-
-abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  where "coprime x y \<equiv> gcd x y = 1"
-
-end
 
 class Gcd = gcd +
   fixes Gcd :: "'a set \<Rightarrow> 'a"
@@ -243,7 +237,8 @@
     by simp
 qed
 
-lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+lemma is_unit_gcd_iff [simp]:
+  "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
 
 sublocale gcd: abel_semigroup gcd
@@ -279,7 +274,7 @@
   show "gcd (normalize a) b = gcd a b" for a b
     using gcd_dvd1 [of "normalize a" b]
     by (auto intro: associated_eqI)
-  show "coprime 1 a" for a
+  show "gcd 1 a = 1" for a
     by (rule associated_eqI) simp_all
 qed simp_all
 
@@ -292,12 +287,6 @@
 lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   by (fact gcd.right_idem)
 
-lemma coprime_1_left: "coprime 1 a"
-  by (fact gcd.bottom_left_bottom)
-
-lemma coprime_1_right: "coprime a 1"
-  by (fact gcd.bottom_right_bottom)
-
 lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
 proof (cases "c = 0")
   case True
@@ -634,70 +623,6 @@
     by (rule dvd_trans)
 qed
 
-lemma coprime_dvd_mult:
-  assumes "coprime a b" and "a dvd c * b"
-  shows "a dvd c"
-proof (cases "c = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have unit: "is_unit (unit_factor c)"
-    by simp
-  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
-  have "gcd (c * a) (c * b) * unit_factor c = c"
-    by (simp add: ac_simps)
-  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
-    by (simp add: dvd_mult_unit_iff unit)
-  ultimately show ?thesis
-    by simp
-qed
-
-lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
-  by (auto intro: coprime_dvd_mult)
-
-lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
-  apply (rule associated_eqI)
-     apply (rule gcd_greatest)
-      apply (rule_tac b = c in coprime_dvd_mult)
-       apply (simp add: gcd.assoc)
-       apply (simp_all add: ac_simps)
-  done
-
-lemma coprime_crossproduct:
-  fixes a b c d :: 'a
-  assumes "coprime a d" and "coprime b c"
-  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
-    normalize a = normalize b \<and> normalize c = normalize d"
-    (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?rhs
-  then show ?lhs by simp
-next
-  assume ?lhs
-  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
-    by (auto intro: dvdI dest: sym)
-  with \<open>coprime a d\<close> have "a dvd b"
-    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
-  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
-    by (auto intro: dvdI dest: sym)
-  with \<open>coprime b c\<close> have "b dvd a"
-    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
-  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
-    by (auto intro: dvdI dest: sym simp add: mult.commute)
-  with \<open>coprime b c\<close> have "c dvd d"
-    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
-  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
-    by (auto intro: dvdI dest: sym simp add: mult.commute)
-  with \<open>coprime a d\<close> have "d dvd c"
-    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
-  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
-    by (rule associatedI)
-  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
-    by (rule associatedI)
-  ultimately show ?rhs ..
-qed
-
 lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
 
@@ -707,285 +632,6 @@
 lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
 
-lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
-  by (rule sym, rule gcdI) simp_all
-
-lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
-  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
-
-lemma div_gcd_coprime:
-  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
-  shows "coprime (a div gcd a b) (b div gcd a b)"
-proof -
-  let ?g = "gcd a b"
-  let ?a' = "a div ?g"
-  let ?b' = "b div ?g"
-  let ?g' = "gcd ?a' ?b'"
-  have dvdg: "?g dvd a" "?g dvd b"
-    by simp_all
-  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
-    by simp_all
-  from dvdg dvdg' obtain ka kb ka' kb' where
-    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
-    unfolding dvd_def by blast
-  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
-    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
-  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
-    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
-  have "?g \<noteq> 0"
-    using nz by simp
-  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
-  ultimately show ?thesis
-    using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
-qed
-
-lemma divides_mult:
-  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
-  shows "a * b dvd c"
-proof -
-  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
-  with \<open>a dvd c\<close> have "a dvd b' * b"
-    by (simp add: ac_simps)
-  with \<open>coprime a b\<close> have "a dvd b'"
-    by (simp add: coprime_dvd_mult_iff)
-  then obtain a' where "b' = a * a'" ..
-  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
-    by (simp add: ac_simps)
-  then show ?thesis ..
-qed
-
-lemma coprime_lmult:
-  assumes dab: "gcd d (a * b) = 1"
-  shows "gcd d a = 1"
-proof (rule coprimeI)
-  fix l
-  assume "l dvd d" and "l dvd a"
-  then have "l dvd a * b"
-    by simp
-  with \<open>l dvd d\<close> and dab show "l dvd 1"
-    by (auto intro: gcd_greatest)
-qed
-
-lemma coprime_rmult:
-  assumes dab: "gcd d (a * b) = 1"
-  shows "gcd d b = 1"
-proof (rule coprimeI)
-  fix l
-  assume "l dvd d" and "l dvd b"
-  then have "l dvd a * b"
-    by simp
-  with \<open>l dvd d\<close> and dab show "l dvd 1"
-    by (auto intro: gcd_greatest)
-qed
-
-lemma coprime_mult:
-  assumes "coprime d a"
-    and "coprime d b"
-  shows "coprime d (a * b)"
-  apply (subst gcd.commute)
-  using assms(1) apply (subst gcd_mult_cancel)
-   apply (subst gcd.commute)
-   apply assumption
-  apply (subst gcd.commute)
-  apply (rule assms(2))
-  done
-
-lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
-  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
-  by blast
-
-lemma coprime_mul_eq':
-  "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
-  using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
-
-lemma gcd_coprime:
-  assumes c: "gcd a b \<noteq> 0"
-    and a: "a = a' * gcd a b"
-    and b: "b = b' * gcd a b"
-  shows "gcd a' b' = 1"
-proof -
-  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
-    by simp
-  with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
-  also from assms have "a div gcd a b = a'"
-    using dvd_div_eq_mult local.gcd_dvd1 by blast
-  also from assms have "b div gcd a b = b'"
-    using dvd_div_eq_mult local.gcd_dvd1 by blast
-  finally show ?thesis .
-qed
-
-lemma coprime_power:
-  assumes "0 < n"
-  shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
-  using assms
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  then show ?case
-    by (cases n) (simp_all add: coprime_mul_eq)
-qed
-
-lemma gcd_coprime_exists:
-  assumes "gcd a b \<noteq> 0"
-  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
-  apply (rule_tac x = "a div gcd a b" in exI)
-  apply (rule_tac x = "b div gcd a b" in exI)
-  using assms
-  apply (auto intro: div_gcd_coprime)
-  done
-
-lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
-  by (induct n) (simp_all add: coprime_mult)
-
-lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
-  by (induct n) (simp_all add: gcd_mult_cancel)
-
-lemma coprime_exp2:
-  assumes "coprime a b"
-  shows "coprime (a ^ n) (b ^ m)"
-proof (rule coprime_exp_left)
-  from assms show "coprime a (b ^ m)"
-    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
-qed
-
-lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
-proof (cases "a = 0 \<and> b = 0")
-  case True
-  then show ?thesis
-    by (cases n) simp_all
-next
-  case False
-  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
-    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
-  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
-    by simp
-  also note gcd_mult_distrib
-  also have "unit_factor (gcd a b ^ n) = 1"
-    using False by (auto simp add: unit_factor_power unit_factor_gcd)
-  also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
-    apply (subst ac_simps)
-    apply (subst div_power)
-     apply simp
-    apply (rule dvd_div_mult_self)
-    apply (rule dvd_power_same)
-    apply simp
-    done
-  also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
-    apply (subst ac_simps)
-    apply (subst div_power)
-     apply simp
-    apply (rule dvd_div_mult_self)
-    apply (rule dvd_power_same)
-    apply simp
-    done
-  finally show ?thesis by simp
-qed
-
-lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
-  apply (subgoal_tac "a dvd gcd a b")
-   apply simp
-  apply (erule (1) gcd_greatest)
-  done
-
-lemma division_decomp:
-  assumes "a dvd b * c"
-  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
-proof (cases "gcd a b = 0")
-  case True
-  then have "a = 0 \<and> b = 0"
-    by simp
-  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
-    by simp
-  then show ?thesis by blast
-next
-  case False
-  let ?d = "gcd a b"
-  from gcd_coprime_exists [OF False]
-    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
-    by blast
-  from ab'(1) have "a' dvd a"
-    unfolding dvd_def by blast
-  with assms have "a' dvd b * c"
-    using dvd_trans [of a' a "b * c"] by simp
-  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
-    by simp
-  then have "?d * a' dvd ?d * (b' * c)"
-    by (simp add: mult_ac)
-  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
-    by simp
-  with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
-    by (subst (asm) ac_simps) blast
-  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
-    by (simp add: mult_ac)
-  then show ?thesis by blast
-qed
-
-lemma pow_divs_pow:
-  assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
-  shows "a dvd b"
-proof (cases "gcd a b = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  let ?d = "gcd a b"
-  from n obtain m where m: "n = Suc m"
-    by (cases n) simp_all
-  from False have zn: "?d ^ n \<noteq> 0"
-    by (rule power_not_zero)
-  from gcd_coprime_exists [OF False]
-  obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
-    by blast
-  from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
-    by (simp add: ab'(1,2)[symmetric])
-  then have "?d^n * a'^n dvd ?d^n * b'^n"
-    by (simp only: power_mult_distrib ac_simps)
-  with zn have "a'^n dvd b'^n"
-    by simp
-  then have "a' dvd b'^n"
-    using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
-  then have "a' dvd b'^m * b'"
-    by (simp add: m ac_simps)
-  with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
-  have "a' dvd b'" by (subst (asm) ac_simps) blast
-  then have "a' * ?d dvd b' * ?d"
-    by (rule mult_dvd_mono) simp
-  with ab'(1,2) show ?thesis
-    by simp
-qed
-
-lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
-  by (auto intro: pow_divs_pow dvd_power_same)
-
-lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
-  by (subst add_commute) simp
-
-lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
-  by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
-
-lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
-  by (induct xs) (simp_all add: gcd_mult_cancel)
-
-lemma coprime_divisors:
-  assumes "d dvd a" "e dvd b" "gcd a b = 1"
-  shows "gcd d e = 1"
-proof -
-  from assms obtain k l where "a = d * k" "b = e * l"
-    unfolding dvd_def by blast
-  with assms have "gcd (d * k) (e * l) = 1"
-    by simp
-  then have "gcd (d * k) e = 1"
-    by (rule coprime_lmult)
-  also have "gcd (d * k) e = gcd e (d * k)"
-    by (simp add: ac_simps)
-  finally have "gcd e d = 1"
-    by (rule coprime_lmult)
-  then show ?thesis
-    by (simp add: ac_simps)
-qed
-
 lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
   by (simp add: lcm_gcd)
 
@@ -1006,9 +652,6 @@
   "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
 
-lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
-  by (subst lcm_gcd) simp
-
 lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
   apply (cases "a = 0")
    apply simp
@@ -1058,7 +701,7 @@
 qed
 
 lemma dvd_productE:
-  assumes "p dvd (a * b)"
+  assumes "p dvd a * b"
   obtains x y where "p = x * y" "x dvd a" "y dvd b"
 proof (cases "a = 0")
   case True
@@ -1076,32 +719,11 @@
   ultimately show ?thesis by (rule that)
 qed
 
-lemma coprime_crossproduct':
-  fixes a b c d
-  assumes "b \<noteq> 0"
-  assumes unit_factors: "unit_factor b = unit_factor d"
-  assumes coprime: "coprime a b" "coprime c d"
-  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
-proof safe
-  assume eq: "a * d = b * c"
-  hence "normalize a * normalize d = normalize c * normalize b"
-    by (simp only: normalize_mult [symmetric] mult_ac)
-  with coprime have "normalize b = normalize d"
-    by (subst (asm) coprime_crossproduct) simp_all
-  from this and unit_factors show "b = d"
-    by (rule normalize_unit_factor_eqI)
-  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
-  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
-qed (simp_all add: mult_ac)
-
 end
 
 class ring_gcd = comm_ring_1 + semiring_gcd
 begin
 
-lemma coprime_minus_one: "coprime (n - 1) n"
-  using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
-
 lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
 
@@ -1471,36 +1093,6 @@
 lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
   by simp
 
-lemma Lcm_coprime:
-  assumes "finite A"
-    and "A \<noteq> {}"
-    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
-  shows "Lcm A = normalize (\<Prod>A)"
-  using assms
-proof (induct rule: finite_ne_induct)
-  case singleton
-  then show ?case by simp
-next
-  case (insert a A)
-  have "Lcm (insert a A) = lcm a (Lcm A)"
-    by simp
-  also from insert have "Lcm A = normalize (\<Prod>A)"
-    by blast
-  also have "lcm a \<dots> = lcm a (\<Prod>A)"
-    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
-  also from insert have "gcd a (\<Prod>A) = 1"
-    by (subst gcd.commute, intro prod_coprime) auto
-  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
-    by (simp add: lcm_coprime)
-  finally show ?case .
-qed
-
-lemma Lcm_coprime':
-  "card A \<noteq> 0 \<Longrightarrow>
-    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
-    Lcm A = normalize (\<Prod>A)"
-  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
-
 lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
   by (auto intro!: Gcd_eq_1_I)
 
@@ -1677,6 +1269,465 @@
 
 end
 
+
+subsection \<open>Coprimality\<close>
+
+context semiring_gcd
+begin
+
+lemma coprime_imp_gcd_eq_1 [simp]:
+  "gcd a b = 1" if "coprime a b"
+proof -
+  define t r s where "t = gcd a b" and "r = a div t" and "s = b div t"
+  then have "a = t * r" and "b = t * s"
+    by simp_all
+  with that have "coprime (t * r) (t * s)"
+    by simp
+  then show ?thesis
+    by (simp add: t_def)
+qed
+
+lemma gcd_eq_1_imp_coprime:
+  "coprime a b" if "gcd a b = 1"
+proof (rule coprimeI)
+  fix c
+  assume "c dvd a" and "c dvd b"
+  then have "c dvd gcd a b"
+    by (rule gcd_greatest)
+  with that show "is_unit c"
+    by simp
+qed
+
+lemma coprime_iff_gcd_eq_1 [presburger, code]:
+  "coprime a b \<longleftrightarrow> gcd a b = 1"
+  by rule (simp_all add: gcd_eq_1_imp_coprime)
+
+lemma is_unit_gcd [simp]:
+  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+  by (simp add: coprime_iff_gcd_eq_1)
+
+lemma coprime_add_one_left [simp]: "coprime (a + 1) a"
+  by (simp add: gcd_eq_1_imp_coprime ac_simps)
+
+lemma coprime_add_one_right [simp]: "coprime a (a + 1)"
+  using coprime_add_one_left [of a] by (simp add: ac_simps)
+
+lemma coprime_mult_left_iff [simp]:
+  "coprime (a * b) c \<longleftrightarrow> coprime a c \<and> coprime b c"
+proof
+  assume "coprime (a * b) c"
+  with coprime_common_divisor [of "a * b" c]
+  have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d
+    using that by blast
+  have "coprime a c"
+    by (rule coprimeI, rule *) simp_all
+  moreover have "coprime b c"
+    by (rule coprimeI, rule *) simp_all
+  ultimately show "coprime a c \<and> coprime b c" ..
+next
+  assume "coprime a c \<and> coprime b c"
+  then have "coprime a c" "coprime b c"
+    by simp_all
+  show "coprime (a * b) c"
+  proof (rule coprimeI)
+    fix d
+    assume "d dvd a * b"
+    then obtain r s where d: "d = r * s" "r dvd a" "s dvd b"
+      by (rule dvd_productE)
+    assume "d dvd c"
+    with d have "r * s dvd c"
+      by simp
+    then have "r dvd c" "s dvd c"
+      by (auto intro: dvd_mult_left dvd_mult_right)
+    from \<open>coprime a c\<close> \<open>r dvd a\<close> \<open>r dvd c\<close>
+    have "is_unit r"
+      by (rule coprime_common_divisor)
+    moreover from \<open>coprime b c\<close> \<open>s dvd b\<close> \<open>s dvd c\<close>
+    have "is_unit s"
+      by (rule coprime_common_divisor)
+    ultimately show "is_unit d"
+      by (simp add: d is_unit_mult_iff)
+  qed
+qed
+
+lemma coprime_mult_right_iff [simp]:
+  "coprime c (a * b) \<longleftrightarrow> coprime c a \<and> coprime c b"
+  using coprime_mult_left_iff [of a b c] by (simp add: ac_simps)
+
+lemma coprime_power_left_iff [simp]:
+  "coprime (a ^ n) b \<longleftrightarrow> coprime a b \<or> n = 0"
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "n > 0"
+    by simp
+  then show ?thesis
+    by (induction n rule: nat_induct_non_zero) simp_all
+qed
+
+lemma coprime_power_right_iff [simp]:
+  "coprime a (b ^ n) \<longleftrightarrow> coprime a b \<or> n = 0"
+  using coprime_power_left_iff [of b n a] by (simp add: ac_simps)
+
+lemma prod_coprime_left:
+  "coprime (\<Prod>i\<in>A. f i) a" if "\<And>i. i \<in> A \<Longrightarrow> coprime (f i) a"
+  using that by (induct A rule: infinite_finite_induct) simp_all
+
+lemma prod_coprime_right:
+  "coprime a (\<Prod>i\<in>A. f i)" if "\<And>i. i \<in> A \<Longrightarrow> coprime a (f i)"
+  using that prod_coprime_left [of A f a] by (simp add: ac_simps)
+
+lemma prod_list_coprime_left:
+  "coprime (prod_list xs) a" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime x a"
+  using that by (induct xs) simp_all
+
+lemma prod_list_coprime_right:
+  "coprime a (prod_list xs)" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime a x"
+  using that prod_list_coprime_left [of xs a] by (simp add: ac_simps)
+
+lemma coprime_dvd_mult_left_iff:
+  "a dvd b * c \<longleftrightarrow> a dvd b" if "coprime a c"
+proof
+  assume "a dvd b"
+  then show "a dvd b * c"
+    by simp
+next
+  assume "a dvd b * c"
+  show "a dvd b"
+  proof (cases "b = 0")
+    case True
+    then show ?thesis
+      by simp
+  next
+    case False
+    then have unit: "is_unit (unit_factor b)"
+      by simp
+    from \<open>coprime a c\<close> mult_gcd_left [of b a c]
+    have "gcd (b * a) (b * c) * unit_factor b = b"
+      by (simp add: ac_simps)
+    moreover from \<open>a dvd b * c\<close>
+    have "a dvd gcd (b * a) (b * c) * unit_factor b"
+      by (simp add: dvd_mult_unit_iff unit)
+    ultimately show ?thesis
+      by simp
+  qed
+qed
+
+lemma coprime_dvd_mult_right_iff:
+  "a dvd c * b \<longleftrightarrow> a dvd b" if "coprime a c"
+  using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps)
+
+lemma divides_mult:
+  "a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b"
+proof -
+  from \<open>b dvd c\<close> obtain b' where "c = b * b'" ..
+  with \<open>a dvd c\<close> have "a dvd b' * b"
+    by (simp add: ac_simps)
+  with \<open>coprime a b\<close> have "a dvd b'"
+    by (simp add: coprime_dvd_mult_left_iff)
+  then obtain a' where "b' = a * a'" ..
+  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
+    by (simp add: ac_simps)
+  then show ?thesis ..
+qed
+
+lemma div_gcd_coprime:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+  shows "coprime (a div gcd a b) (b div gcd a b)"
+proof -
+  let ?g = "gcd a b"
+  let ?a' = "a div ?g"
+  let ?b' = "b div ?g"
+  let ?g' = "gcd ?a' ?b'"
+  have dvdg: "?g dvd a" "?g dvd b"
+    by simp_all
+  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
+    by simp_all
+  from dvdg dvdg' obtain ka kb ka' kb' where
+    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
+    unfolding dvd_def by blast
+  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
+  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
+    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+  have "?g \<noteq> 0"
+    using assms by simp
+  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  ultimately show ?thesis
+    using dvd_times_left_cancel_iff [of "gcd a b" _ 1]
+    by simp (simp only: coprime_iff_gcd_eq_1)
+qed
+
+lemma gcd_coprime:
+  assumes c: "gcd a b \<noteq> 0"
+    and a: "a = a' * gcd a b"
+    and b: "b = b' * gcd a b"
+  shows "coprime a' b'"
+proof -
+  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
+    by simp
+  with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
+  also from assms have "a div gcd a b = a'"
+    using dvd_div_eq_mult local.gcd_dvd1 by blast
+  also from assms have "b div gcd a b = b'"
+    using dvd_div_eq_mult local.gcd_dvd1 by blast
+  finally show ?thesis .
+qed
+
+lemma gcd_coprime_exists:
+  assumes "gcd a b \<noteq> 0"
+  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
+  apply (rule_tac x = "a div gcd a b" in exI)
+  apply (rule_tac x = "b div gcd a b" in exI)
+  using assms
+  apply (auto intro: div_gcd_coprime)
+  done
+
+lemma pow_divides_pow_iff [simp]:
+  "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
+proof (cases "gcd a b = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    let ?d = "gcd a b"
+    from \<open>n > 0\<close> obtain m where m: "n = Suc m"
+      by (cases n) simp_all
+    from False have zn: "?d ^ n \<noteq> 0"
+      by (rule power_not_zero)
+    from gcd_coprime_exists [OF False]
+    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
+      by blast
+    assume "a ^ n dvd b ^ n"
+    then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
+      by (simp add: ab'(1,2)[symmetric])
+    then have "?d^n * a'^n dvd ?d^n * b'^n"
+      by (simp only: power_mult_distrib ac_simps)
+    with zn have "a' ^ n dvd b' ^ n"
+      by simp
+    then have "a' dvd b' ^ n"
+      using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
+    then have "a' dvd b' ^ m * b'"
+      by (simp add: m ac_simps)
+    moreover have "coprime a' (b' ^ n)"
+      using \<open>coprime a' b'\<close> by simp
+    then have "a' dvd b'"
+      using \<open>a' dvd b' ^ n\<close> coprime_dvd_mult_left_iff dvd_mult by blast
+    then have "a' * ?d dvd b' * ?d"
+      by (rule mult_dvd_mono) simp
+    with ab'(1,2) show "a dvd b"
+      by simp
+  next
+    assume "a dvd b"
+    with \<open>n > 0\<close> show "a ^ n dvd b ^ n"
+      by (induction rule: nat_induct_non_zero)
+        (simp_all add: mult_dvd_mono)
+  qed
+qed
+
+lemma coprime_crossproduct:
+  fixes a b c d :: 'a
+  assumes "coprime a d" and "coprime b c"
+  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
+    normalize a = normalize b \<and> normalize c = normalize d"
+    (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?rhs
+  then show ?lhs by simp
+next
+  assume ?lhs
+  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
+    by (auto intro: dvdI dest: sym)
+  with \<open>coprime a d\<close> have "a dvd b"
+    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
+  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
+    by (auto intro: dvdI dest: sym)
+  with \<open>coprime b c\<close> have "b dvd a"
+    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
+  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
+    by (auto intro: dvdI dest: sym simp add: mult.commute)
+  with \<open>coprime b c\<close> have "c dvd d"
+    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
+  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
+    by (auto intro: dvdI dest: sym simp add: mult.commute)
+  with \<open>coprime a d\<close> have "d dvd c"
+    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
+  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
+    by (rule associatedI)
+  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
+    by (rule associatedI)
+  ultimately show ?rhs ..
+qed
+
+lemma coprime_crossproduct':
+  fixes a b c d
+  assumes "b \<noteq> 0"
+  assumes unit_factors: "unit_factor b = unit_factor d"
+  assumes coprime: "coprime a b" "coprime c d"
+  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+  assume eq: "a * d = b * c"
+  hence "normalize a * normalize d = normalize c * normalize b"
+    by (simp only: normalize_mult [symmetric] mult_ac)
+  with coprime have "normalize b = normalize d"
+    by (subst (asm) coprime_crossproduct) simp_all
+  from this and unit_factors show "b = d"
+    by (rule normalize_unit_factor_eqI)
+  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
+lemma gcd_mult_left_left_cancel:
+  "gcd (c * a) b = gcd a b" if "coprime b c"
+proof -
+  have "coprime (gcd b (a * c)) c"
+    by (rule coprimeI) (auto intro: that coprime_common_divisor)
+  then have "gcd b (a * c) dvd a"
+    using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a]
+    by simp
+  then show ?thesis
+    by (auto intro: associated_eqI simp add: ac_simps)
+qed
+
+lemma gcd_mult_left_right_cancel:
+  "gcd (a * c) b = gcd a b" if "coprime b c"
+  using that gcd_mult_left_left_cancel [of b c a]
+  by (simp add: ac_simps)
+
+lemma gcd_mult_right_left_cancel:
+  "gcd a (c * b) = gcd a b" if "coprime a c"
+  using that gcd_mult_left_left_cancel [of a c b]
+  by (simp add: ac_simps)
+
+lemma gcd_mult_right_right_cancel:
+  "gcd a (b * c) = gcd a b" if "coprime a c"
+  using that gcd_mult_right_left_cancel [of a c b]
+  by (simp add: ac_simps)
+
+lemma gcd_exp [simp]:
+  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
+  case True
+  then show ?thesis
+    by (cases n) simp_all
+next
+  case False
+  then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0"
+    by (auto intro: div_gcd_coprime)
+  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+    by simp
+  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+    by simp
+  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
+    by simp
+  also note gcd_mult_distrib
+  also have "unit_factor (gcd a b ^ n) = 1"
+    using False by (auto simp add: unit_factor_power unit_factor_gcd)
+  also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
+    by (simp add: ac_simps div_power dvd_power_same)
+  also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
+    by (simp add: ac_simps div_power dvd_power_same)
+  finally show ?thesis by simp
+qed
+
+lemma division_decomp:
+  assumes "a dvd b * c"
+  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
+proof (cases "gcd a b = 0")
+  case True
+  then have "a = 0 \<and> b = 0"
+    by simp
+  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
+    by simp
+  then show ?thesis by blast
+next
+  case False
+  let ?d = "gcd a b"
+  from gcd_coprime_exists [OF False]
+    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
+    by blast
+  from ab'(1) have "a' dvd a" ..
+  with assms have "a' dvd b * c"
+    using dvd_trans [of a' a "b * c"] by simp
+  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
+    by simp
+  then have "?d * a' dvd ?d * (b' * c)"
+    by (simp add: mult_ac)
+  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
+    by simp
+  then have "a' dvd c"
+    using \<open>coprime a' b'\<close> by (simp add: coprime_dvd_mult_right_iff)
+  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
+    by (simp add: ac_simps)
+  then show ?thesis by blast
+qed
+
+lemma lcm_coprime: "coprime a b \<Longrightarrow> lcm a b = normalize (a * b)"
+  by (subst lcm_gcd) simp
+
+end
+
+context ring_gcd
+begin
+
+lemma coprime_minus_left_iff [simp]:
+  "coprime (- a) b \<longleftrightarrow> coprime a b"
+  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
+
+lemma coprime_minus_right_iff [simp]:
+  "coprime a (- b) \<longleftrightarrow> coprime a b"
+  using coprime_minus_left_iff [of b a] by (simp add: ac_simps)
+
+lemma coprime_diff_one_left [simp]: "coprime (a - 1) a"
+  using coprime_add_one_right [of "a - 1"] by simp
+
+lemma coprime_doff_one_right [simp]: "coprime a (a - 1)"
+  using coprime_diff_one_left [of a] by (simp add: ac_simps)
+
+end
+
+context semiring_Gcd
+begin
+
+lemma Lcm_coprime:
+  assumes "finite A"
+    and "A \<noteq> {}"
+    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b"
+  shows "Lcm A = normalize (\<Prod>A)"
+  using assms
+proof (induct rule: finite_ne_induct)
+  case singleton
+  then show ?case by simp
+next
+  case (insert a A)
+  have "Lcm (insert a A) = lcm a (Lcm A)"
+    by simp
+  also from insert have "Lcm A = normalize (\<Prod>A)"
+    by blast
+  also have "lcm a \<dots> = lcm a (\<Prod>A)"
+    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
+  also from insert have "coprime a (\<Prod>A)"
+    by (subst coprime_commute, intro prod_coprime_left) auto
+  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
+    by (simp add: lcm_coprime)
+  finally show ?case .
+qed
+
+lemma Lcm_coprime':
+  "card A \<noteq> 0 \<Longrightarrow>
+    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b) \<Longrightarrow>
+    Lcm A = normalize (\<Prod>A)"
+  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
+
+end
+
+
 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
 
 instantiation nat :: gcd
@@ -1716,9 +1767,6 @@
    apply simp_all
   done
 
-
-text \<open>Specific to \<open>int\<close>.\<close>
-
 lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   by (simp add: gcd_int_def)
 
@@ -1949,19 +1997,6 @@
   for k m n :: int
   by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
 
-lemma coprime_crossproduct_nat:
-  fixes a b c d :: nat
-  assumes "coprime a d" and "coprime b c"
-  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
-  using assms coprime_crossproduct [of a d b c] by simp
-
-lemma coprime_crossproduct_int:
-  fixes a b c d :: int
-  assumes "coprime a d" and "coprime b c"
-  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
-  using assms coprime_crossproduct [of a d b c] by simp
-
-
 text \<open>\medskip Addition laws.\<close>
 
 (* TODO: add the other variations? *)
@@ -2064,53 +2099,33 @@
   for k l :: int
   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
 
-
-subsection \<open>Coprimality\<close>
-
-lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
-  for a b :: nat
-  using coprime [of a b] by simp
-
-lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
-  for a b :: nat
-  using coprime_nat by simp
-
-lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
-  for a b :: int
-  using gcd_unique_int [of 1 a b]
-  apply clarsimp
-  apply (erule subst)
-  apply (rule iffI)
-   apply force
-  using abs_dvd_iff abs_ge_zero apply blast
-  done
-
-lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
-  for a b n :: nat
-  using pow_divs_eq[of n] by simp
-
-lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
-  using coprime_plus_one[of n] by simp
-
-lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
-  for n :: nat
-  using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
-
-lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
-  for a b :: nat
-  by (metis gcd_greatest_iff nat_dvd_1_iff_1)
-
-lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
-  for a b :: int
-  using gcd_greatest_iff [of x a b] by auto
-
-lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
-  for m x y :: nat
-  by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
-
-lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
-  for m x y :: int
-  by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
+lemma coprime_Suc_left_nat [simp]:
+  "coprime (Suc n) n"
+  using coprime_add_one_left [of n] by simp
+
+lemma coprime_Suc_right_nat [simp]:
+  "coprime n (Suc n)"
+  using coprime_Suc_left_nat [of n] by (simp add: ac_simps)
+
+lemma coprime_diff_one_left_nat [simp]:
+  "coprime (n - 1) n" if "n > 0" for n :: nat
+  using that coprime_Suc_right_nat [of "n - 1"] by simp
+
+lemma coprime_diff_one_right_nat [simp]:
+  "coprime n (n - 1)" if "n > 0" for n :: nat
+  using that coprime_diff_one_left_nat [of n] by (simp add: ac_simps)
+
+lemma coprime_crossproduct_nat:
+  fixes a b c d :: nat
+  assumes "coprime a d" and "coprime b c"
+  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
+  using assms coprime_crossproduct [of a d b c] by simp
+
+lemma coprime_crossproduct_int:
+  fixes a b c d :: int
+  assumes "coprime a d" and "coprime b c"
+  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
+  using assms coprime_crossproduct [of a d b c] by simp
 
 
 subsection \<open>Bezout's theorem\<close>
@@ -2742,14 +2757,6 @@
   for i m n :: int
   by (fact dvd_lcmI2)
 
-lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
-  for a b :: nat
-  by (fact coprime_exp2)
-
-lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
-  for a b :: int
-  by (fact coprime_exp2)
-
 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -21,10 +21,6 @@
 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
   Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
 
-
-declare One_nat_def [simp]
-
-
 subsection \<open>Fibonacci numbers\<close>
 
 fun fib :: "nat \<Rightarrow> nat"
@@ -65,12 +61,13 @@
   finally show "?P (n + 2)" .
 qed
 
-lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1"
+lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
   (is "?P n")
 proof (induct n rule: fib_induct)
   show "?P 0" by simp
   show "?P 1" by simp
   fix n
+  assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
     by simp
   also have "\<dots> = fib (n + 2) + fib (n + 1)"
@@ -79,8 +76,10 @@
     by (rule gcd_add2)
   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
     by (simp add: gcd.commute)
-  also assume "\<dots> = 1"
-  finally show "?P (n + 2)" .
+  also have "\<dots> = 1"
+    using P by simp
+  finally show "?P (n + 2)"
+    by (simp add: coprime_iff_gcd_eq_1)
 qed
 
 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
@@ -106,7 +105,8 @@
   also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
     by (simp add: gcd_mult_add)
   also have "\<dots> = gcd (fib n) (fib (k + 1))"
-    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
+    using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]
+    by (simp add: ac_simps)
   also have "\<dots> = gcd (fib m) (fib n)"
     using Suc by (simp add: gcd.commute)
   finally show ?thesis .
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -2155,6 +2155,42 @@
   "image_mset f (replicate_mset n a) = replicate_mset n (f a)"
   by (induct n) simp_all
 
+lemma replicate_mset_msubseteq_iff:
+  "replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
+  by (cases m)
+    (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
+
+lemma msubseteq_replicate_msetE:
+  assumes "A \<subseteq># replicate_mset n a"
+  obtains m where "m \<le> n" and "A = replicate_mset m a"
+proof (cases "n = 0")
+  case True
+  with assms that show thesis
+    by simp
+next
+  case False
+  from assms have "set_mset A \<subseteq> set_mset (replicate_mset n a)"
+    by (rule set_mset_mono)
+  with False have "set_mset A \<subseteq> {a}"
+    by simp
+  then have "\<exists>m. A = replicate_mset m a"
+  proof (induction A)
+    case empty
+    then show ?case
+      by simp
+  next
+    case (add b A)
+    then obtain m where "A = replicate_mset m a"
+      by auto
+    with add.prems show ?case
+      by (auto intro: exI [of _ "Suc m"])
+  qed
+  then obtain m where A: "A = replicate_mset m a" ..
+  with assms have "m \<le> n"
+    by (auto simp add: replicate_mset_msubseteq_iff)
+  then show thesis using A ..
+qed
+
 
 subsection \<open>Big operators\<close>
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Map.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -782,6 +782,20 @@
   with * \<open>x = (k, v)\<close> show ?case by simp
 qed
 
+lemma eq_key_imp_eq_value:
+  "v1 = v2"
+  if "distinct (map fst xs)" "(k, v1) \<in> set xs" "(k, v2) \<in> set xs"
+proof -
+  from that have "inj_on fst (set xs)"
+    by (simp add: distinct_map)
+  moreover have "fst (k, v1) = fst (k, v2)"
+    by simp
+  ultimately have "(k, v1) = (k, v2)"
+    by (rule inj_onD) (fact that)+
+  then show ?thesis
+    by simp
+qed
+
 lemma map_of_inject_set:
   assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
   shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Nat.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -2087,6 +2087,34 @@
   using mult_strict_left_mono [of 1 m n] by simp
 
 
+text \<open>Induction starting beyond zero\<close>
+
+lemma nat_induct_at_least [consumes 1, case_names base Suc]:
+  "P n" if "n \<ge> m" "P m" "\<And>n. n \<ge> m \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
+proof -
+  define q where "q = n - m"
+  with \<open>n \<ge> m\<close> have "n = m + q"
+    by simp
+  moreover have "P (m + q)"
+    by (induction q) (use that in simp_all)
+  ultimately show "P n"
+    by simp
+qed
+
+lemma nat_induct_non_zero [consumes 1, case_names 1 Suc]:
+  "P n" if "n > 0" "P 1" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
+proof -
+  from \<open>n > 0\<close> have "n \<ge> 1"
+    by (cases n) simp_all
+  moreover note \<open>P 1\<close>
+  moreover have "\<And>n. n \<ge> 1 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
+    using \<open>\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)\<close>
+    by (simp add: Suc_le_eq)
+  ultimately show "P n"
+    by (rule nat_induct_at_least)
+qed
+
+
 text \<open>Specialized induction principles that work "backwards":\<close>
 
 lemma inc_induct [consumes 1, case_names base step]:
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Nitpick.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -137,7 +137,7 @@
   by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
 
 definition Frac :: "int \<times> int \<Rightarrow> bool" where
-  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> gcd a b = 1"
+  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> coprime a b"
 
 consts
   Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -229,7 +229,8 @@
 lemma cong_mult_rcancel_int:
   "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   if "coprime k m" for a k m :: int
-  by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
+  using that by (simp add: cong_altdef_int)
+    (metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib') 
 
 lemma cong_mult_rcancel_nat:
   "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
@@ -242,7 +243,7 @@
   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_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
+    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 .
@@ -320,11 +321,11 @@
 
 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)
+  by (auto simp add: cong_gcd_eq_nat coprime_iff_gcd_eq_1)
 
 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)
+  by (auto simp add: cong_gcd_eq_int coprime_iff_gcd_eq_1)
 
 lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   for a b :: nat
@@ -490,36 +491,24 @@
 qed
 
 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 (simp add: cong_0_1_nat') 
-next
-  case False
-  with assms show ?thesis
-    by (metis cong_solve_nat)
-qed
+  "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n"
+  using that cong_solve_nat [of a n] by (cases "a = 0") simp_all
 
-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 (metis cong_solve_int)
-  done
+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 (cases "a = 0")
+    (auto simp add: zabs_def split: if_splits)
 
 lemma coprime_iff_invertible_nat:
-  "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)
+  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))"
+  by (auto intro: cong_solve_coprime_nat)
+    (use cong_imp_coprime_nat cong_sym coprime_Suc_0_left coprime_mult_left_iff in blast)
 
-lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>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)
-  using cong_gcd_eq_int coprime_mul_eq' apply fastforce
-  done
+  by (auto intro: cong_solve_coprime_int)
+    (meson cong_imp_coprime_int cong_sym coprime_1_left coprime_mult_left_iff)
 
 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))"
@@ -554,16 +543,16 @@
     and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   using that apply (induct A rule: infinite_finite_induct)
     apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
+  apply (metis coprime_cong_mult_nat prod_coprime_right)
   done
 
-lemma cong_cong_prod_coprime_int [rule_format]:
+lemma cong_cong_prod_coprime_int:
   "[x = y] (mod (\<Prod>i\<in>A. m i))" if
     "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
     "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   using that apply (induct A rule: infinite_finite_induct)
-  apply auto
-  apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
+    apply auto
+  apply (metis coprime_cong_mult_int prod_coprime_right)
   done
 
 lemma binary_chinese_remainder_aux_nat:
@@ -574,7 +563,7 @@
   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)
+    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)"
@@ -593,7 +582,7 @@
   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)
+    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)"
@@ -730,8 +719,8 @@
   fix i
   assume "i \<in> A"
   with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
-    by (intro prod_coprime) auto
-  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod 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
@@ -789,8 +778,8 @@
   if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
     and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat
   using that apply (induct A rule: infinite_finite_induct)
-  apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
+    apply auto
+  apply (metis coprime_cong_mult_nat prod_coprime_right)
   done
 
 lemma chinese_remainder_unique_nat:
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Number_Theory/Euler_Criterion.thy
--- a/src/HOL/Number_Theory/Euler_Criterion.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -65,7 +65,7 @@
 proof -
   have "~ p dvd x" using assms zdvd_not_zless S1_def by auto
   hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x] 
-    by (simp add: gcd.commute)
+    by (simp add: ac_simps)
   then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
   moreover define y where "y = y' * a mod p"
   ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Number_Theory/Fib.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -87,17 +87,34 @@
 
 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
   apply (induct n rule: fib.induct)
-  apply auto
-  apply (metis gcd_add1 add.commute)
+    apply (simp_all add: coprime_iff_gcd_eq_1 algebra_simps)
+  apply (simp add: add.assoc [symmetric])
   done
 
-lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
-  apply (simp add: gcd.commute [of "fib m"])
-  apply (cases m)
-  apply (auto simp add: fib_add)
-  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
-    gcd_add_mult gcd_mult_cancel gcd.commute)
-  done
+lemma gcd_fib_add:
+  "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
+proof (cases m)
+  case 0
+  then show ?thesis
+    by simp
+next
+  case (Suc q)
+  from coprime_fib_Suc_nat [of q]
+  have "coprime (fib (Suc q)) (fib q)"
+    by (simp add: ac_simps)
+  have "gcd (fib q) (fib (Suc q)) = Suc 0"
+    using coprime_fib_Suc_nat [of q] by simp
+  then have *: "gcd (fib n * fib q) (fib n * fib (Suc q)) = fib n"
+    by (simp add: gcd_mult_distrib_nat [symmetric])
+  moreover have "gcd (fib (Suc q)) (fib n * fib q + fib (Suc n) * fib (Suc q)) =
+    gcd (fib (Suc q)) (fib n * fib q)"
+    using gcd_add_mult [of "fib (Suc q)"] by (simp add: ac_simps)
+  moreover have "gcd (fib (Suc q)) (fib n * fib (Suc q)) = fib (Suc q)"
+    by simp
+  ultimately show ?thesis
+    using Suc \<open>coprime (fib (Suc q)) (fib q)\<close>
+    by (auto simp add: fib_add algebra_simps gcd_mult_right_right_cancel)
+qed
 
 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -115,8 +115,9 @@
   proof -
     from p_a_relprime have "\<not> p dvd a"
       by (simp add: cong_altdef_int)
-    with p_prime have "coprime a (int p)"
-      by (subst gcd.commute, intro prime_imp_coprime) auto
+    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
+    have "coprime a (int p)"
+      by (simp_all add: zdvd_int ac_simps)
     with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
       by simp
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -149,8 +150,9 @@
       using cong_def by blast
     from p_a_relprime have "\<not>p dvd a"
       by (simp add: cong_altdef_int)
-    with p_prime have "coprime a (int p)"
-      by (subst gcd.commute, intro prime_imp_coprime) auto
+    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
+    have "coprime a (int p)"
+      by (simp_all add: zdvd_int ac_simps)  
     with a' cong_mult_rcancel_int [of a "int p" x y]
     have "[x = y] (mod p)" by simp
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -219,13 +221,16 @@
   by (auto simp add: D_def C_def B_def A_def)
 
 lemma all_A_relprime:
-  assumes "x \<in> A"
-  shows "gcd x p = 1"
-  using p_prime A_ncong_p [OF assms]
-  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
-
-lemma A_prod_relprime: "gcd (prod id A) p = 1"
-  by (metis id_def all_A_relprime prod_coprime)
+  "coprime x p" if "x \<in> A"
+proof -
+  from A_ncong_p [OF that] have "\<not> int p dvd x"
+    by (simp add: cong_altdef_int)
+  with p_prime show ?thesis
+    by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer)
+qed
+  
+lemma A_prod_relprime: "coprime (prod id A) p"
+  by (auto intro: prod_coprime_left all_A_relprime)
 
 
 subsection \<open>Relationships Between Gauss Sets\<close>
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -11,18 +11,11 @@
 subsection \<open>Lemmas about previously defined terms\<close>
 
 lemma prime_nat_iff'': "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
-  unfolding prime_nat_iff
-proof safe
-  fix m
-  assume p: "p > 0" "p \<noteq> 1"
-    and m: "m dvd p" "m \<noteq> p"
-    and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
-  from p m have "m \<noteq> 0" by (intro notI) auto
-  moreover from p m have "m < p" by (auto dest: dvd_imp_le)
-  ultimately have "coprime p m"
-    using * by blast
-  with m show "m = 1" by simp
-qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le)
+  apply (auto simp add: prime_nat_iff)
+   apply (rule coprimeI)
+   apply (auto dest: nat_dvd_not_less simp add: ac_simps)
+  apply (metis One_nat_def dvd_1_iff_1 dvd_pos_nat gcd_nat.order_iff is_unit_gcd linorder_neqE_nat nat_dvd_not_less)
+  done
 
 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
 proof -
@@ -46,7 +39,7 @@
   from bezout_add_strong_nat [OF this]
   obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
   from dxy(1,2) have d1: "d = 1"
-    by (metis assms coprime_nat)
+    using assms coprime_common_divisor [of a n d] by simp
   with dxy(3) have "a * x * b = (n * y + 1) * b"
     by simp
   then have "a * (x * b) = n * (y * b) + b"
@@ -94,9 +87,9 @@
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
 proof -
   from pa have ap: "coprime a p"
-    by (metis gcd.commute)
-  have px: "coprime x p"
-    by (metis gcd.commute p prime_nat_iff'' x0 xp)
+    by (simp add: ac_simps)
+  from x0 xp p have px: "coprime x p"
+    by (auto simp add: prime_nat_iff'' ac_simps)
   obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
     by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
   have "y \<noteq> 0"
@@ -104,8 +97,8 @@
     assume "y = 0"
     with y(2) have "p dvd a"
       using cong_dvd_iff by auto
-    then show False
-      by (metis gcd_nat.absorb1 not_prime_1 p pa)
+    with not_prime_1 p pa show False
+      by (auto simp add: gcd_nat.order_iff)
   qed
   with y show ?thesis
     by blast
@@ -128,9 +121,9 @@
   obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
     by blast
   from ma nb x have "coprime x a" "coprime x b"
-    by (metis cong_gcd_eq_nat)+
+    using cong_imp_coprime_nat cong_sym by blast+
   then have "coprime x (a*b)"
-    by (metis coprime_mul_eq)
+    by simp
   with x show ?thesis
     by blast
 qed
@@ -164,7 +157,8 @@
       from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
         by simp
     qed
-    then show ?thesis by blast
+    then show ?thesis
+      by (auto intro: coprimeI)
   qed
 qed
 
@@ -216,8 +210,8 @@
   from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
     by simp
   from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
-  have an: "coprime a n" "coprime (a^(n - 1)) n"
-    by (auto simp add: coprime_exp gcd.commute)
+  have an: "coprime a n" "coprime (a ^ (n - 1)) n"
+    using \<open>n \<ge> 2\<close> by simp_all
   have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
   proof -
     from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
@@ -229,7 +223,7 @@
       let ?y = "a^ ((n - 1) div m * m)"
       note mdeq = div_mult_mod_eq[of "(n - 1)" m]
       have yn: "coprime ?y n"
-        by (metis an(1) coprime_exp gcd.commute)
+        using an(1) by (cases "(n - Suc 0) div m * m = 0") auto
       have "?y mod n = (a^m)^((n - 1) div m) mod n"
         by (simp add: algebra_simps power_mult)
       also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
@@ -359,9 +353,11 @@
     next
       case (Suc d')
       then have d0: "d \<noteq> 0" by simp
-      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
+      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1"
+        by (auto elim: not_coprimeE) 
       from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
-        by (metis prem d0 gcd.commute lucas_coprime_lemma)
+        using prem d0 lucas_coprime_lemma
+        by (auto elim: not_coprimeE simp add: ac_simps)
       then have "a ^ d + n * q1 - n * q2 = 1" by simp
       with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2 Suc p have "p dvd 1"
         by metis
@@ -398,8 +394,10 @@
   qed
 qed
 
-lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a"
-  by (metis euler_theorem gcd.commute ord_divides that)
+lemma order_divides_totient:
+  "ord n a dvd totient n" if "coprime n a"
+  using that euler_theorem [of a n]
+  by (simp add: ord_divides [symmetric] ac_simps)
 
 lemma order_divides_expdiff:
   fixes n::nat and a::nat assumes na: "coprime n a"
@@ -412,11 +410,11 @@
     from na ed have "\<exists>c. d = e + c" by presburger
     then obtain c where c: "d = e + c" ..
     from na have an: "coprime a n"
-      by (metis gcd.commute)
-    have aen: "coprime (a^e) n"
-      by (metis coprime_exp gcd.commute na)
-    have acn: "coprime (a^c) n"
-      by (metis coprime_exp gcd.commute na)
+      by (simp add: ac_simps)
+    then have aen: "coprime (a ^ e) n"
+      by (cases "e > 0") simp_all
+    from an have acn: "coprime (a ^ c) n"
+      by (cases "c > 0") simp_all
     from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
       by simp
     also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
@@ -620,8 +618,9 @@
       by (metis cong_to_1_nat exps)
     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
       using P0 by simp
-    with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
-    with p01 pn pd0 coprime_common_divisor_nat show False
+    with caP have "coprime (a ^ (ord p (a ^ r) * t * r) - 1) n"
+      by simp
+    with p01 pn pd0 coprime_common_divisor [of _ n p] show False
       by auto
   qed
   with d have o: "ord p (a^r) = q" by simp
@@ -632,12 +631,14 @@
     assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
     from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
     from n have "n \<noteq> 0" by simp
-    then have False using d dp pn
-      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)
+    then have False using d dp pn an
+      by auto (metis One_nat_def Suc_lessI
+        \<open>1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)\<close> \<open>a ^ (q * r) = p * l * k + 1\<close> add_diff_cancel_left' dvd_diff_nat dvd_power dvd_triv_left gcd_nat.trans nat_dvd_not_less nqr zero_less_diff zero_less_one) 
   }
-  then have cpa: "coprime p a" by auto
-  have arp: "coprime (a^r) p"
-    by (metis coprime_exp cpa gcd.commute)
+  then have cpa: "coprime p a"
+    by (auto intro: coprimeI)
+  then have arp: "coprime (a ^ r) p"
+    by (cases "r > 0") (simp_all add: ac_simps)
   from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
     by simp
   then obtain d where d:"p - 1 = q * d"
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -106,13 +106,9 @@
 
 lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
   using m_gt_one
-  unfolding Units_def R_def residue_ring_def
-  apply auto
-    apply (subgoal_tac "x \<noteq> 0")
-     apply auto
-   apply (metis invertible_coprime_int)
+  apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
   apply (subst (asm) coprime_iff_invertible'_int)
-   apply (auto simp add: cong_def mult.commute)
+   apply (auto simp add: cong_def)
   done
 
 lemma res_neg_eq: "\<ominus> x = (- x) mod m"
@@ -220,6 +216,22 @@
 context residues_prime
 begin
 
+lemma p_coprime_left:
+  "coprime p a \<longleftrightarrow> \<not> p dvd a"
+  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
+
+lemma p_coprime_right:
+  "coprime a p  \<longleftrightarrow> \<not> p dvd a"
+  using p_coprime_left [of a] by (simp add: ac_simps)
+
+lemma p_coprime_left_int:
+  "coprime (int p) a \<longleftrightarrow> \<not> int p dvd a"
+  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
+
+lemma p_coprime_right_int:
+  "coprime a (int p) \<longleftrightarrow> \<not> int p dvd a"
+  using p_coprime_left_int [of a] by (simp add: ac_simps)
+
 lemma is_field: "field R"
 proof -
   have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
@@ -231,9 +243,7 @@
 
 lemma res_prime_units_eq: "Units R = {1..p - 1}"
   apply (subst res_units_eq)
-  apply auto
-  apply (subst gcd.commute)
-  apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
+  apply (auto simp add: p_coprime_right_int zdvd_not_zless)
   done
 
 end
@@ -246,26 +256,27 @@
 
 subsection \<open>Euler's theorem\<close>
 
-lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
+lemma (in residues) totatives_eq:
+  "totatives (nat m) = nat ` Units R"
 proof -
+  from m_gt_one have "\<bar>m\<bar> > 1"
+    by simp
+  then have "totatives (nat \<bar>m\<bar>) = nat ` abs ` Units R"
+    by (auto simp add: totatives_def res_units_eq image_iff le_less)
+      (use m_gt_one zless_nat_eq_int_zless in force)
+  moreover have "\<bar>m\<bar> = m" "abs ` Units R = Units R"
+    using m_gt_one by (auto simp add: res_units_eq image_iff)
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma (in residues) totient_eq:
+  "totient (nat m) = card (Units R)"
+proof  -
   have *: "inj_on nat (Units R)"
     by (rule inj_onI) (auto simp add: res_units_eq)
-  define m' where "m' = nat m"
-  from m_gt_one have "m = int m'" "m' > 1"
-    by (simp_all add: m'_def)
-  then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
-    unfolding res_units_eq
-    by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
-  then have "Units R = int ` totatives m'"
-    by blast
-  then have "totatives m' = nat ` Units R"
-    by (simp add: image_image)
-  then have "card (totatives (nat m)) = card (nat ` Units R)"
-    by (simp add: m'_def)
-  also have "\<dots> = card (Units R)"
-    using * card_image [of nat "Units R"] by auto
-  finally show ?thesis
-    by (simp add: totient_def)
+  then show ?thesis
+    by (simp add: totient_def totatives_eq card_image)
 qed
 
 lemma (in residues_prime) totient_eq: "totient p = p - 1"
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Number_Theory/Totient.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -15,7 +15,7 @@
   
 definition totatives :: "nat \<Rightarrow> nat set" where
   "totatives n = {k \<in> {0<..n}. coprime k n}"
-  
+
 lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n"
   by (simp add: totatives_def)
   
@@ -60,7 +60,7 @@
 lemma minus_one_in_totatives:
   assumes "n \<ge> 2"
   shows "n - 1 \<in> totatives n"
-  using assms coprime_minus_one_nat [of n] by (simp add: in_totatives_iff)
+  using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
 
 lemma totatives_prime_power_Suc:
   assumes "prime p"
@@ -72,7 +72,8 @@
   fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}"
   from k have "\<not>(p dvd k)" by (auto elim!: dvdE)
   hence "coprime k (p ^ Suc n)"
-    using prime_imp_coprime[OF assms, of k] by (intro coprime_exp) (simp_all add: gcd.commute)
+    using prime_imp_coprime [OF assms, of k]
+    by (cases "n > 0") (auto simp add: ac_simps)
   with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def)
 qed (auto simp: totatives_def)
 
@@ -101,14 +102,15 @@
   proof safe
     fix x assume "x \<in> totatives (m1 * m2)"
     with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2"
-      by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I)
+      using coprime_common_divisor [of x m1 m1] coprime_common_divisor [of x m2 m2]
+      by (auto simp add: in_totatives_iff mod_greater_zero_iff_not_dvd)
   next
     fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
     with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
     with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
       where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
     from x ab assms(3) have "x \<in> totatives (m1 * m2)"
-      by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
+      by (auto intro: ccontr simp add: in_totatives_iff)
     with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
   qed
 qed
@@ -125,21 +127,18 @@
   show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}"
   proof (intro equalityI subsetI, goal_cases)
     case (1 k)
-    thus ?case using assms
-      by (auto elim!: dvdE simp: inj_on_def totatives_def mult.commute[of d]
-                                 gcd_mult_right gcd.commute)
+    then show ?case using assms
+      by (auto elim: dvdE simp add: in_totatives_iff ac_simps gcd_mult_right)
   next
     case (2 k)
     hence "d dvd k" by auto
     then obtain l where k: "k = l * d" by (elim dvdE) auto
-    from 2 and assms show ?case unfolding k
-      by (intro imageI) (auto simp: totatives_def gcd.commute mult.commute[of d] 
-                                    gcd_mult_right elim!: dvdE)
+    from 2 assms show ?case
+      using gcd_mult_right [of _ d l]
+      by (auto intro: gcd_eq_1_imp_coprime elim!: dvdE simp add: k image_iff in_totatives_iff ac_simps)
   qed
 qed
 
-
-
 definition totient :: "nat \<Rightarrow> nat" where
   "totient n = card (totatives n)"
   
@@ -272,7 +271,8 @@
   proof -
     from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I)
     from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto
-    from that and nz have "\<not>coprime x p" by auto
+    from that and nz have "\<not>coprime x p"
+      by (auto elim: dvdE)
     hence "x \<notin> totatives p" by (simp add: totatives_def)
     also note *
     finally show False using that and le by auto
@@ -299,7 +299,8 @@
   by simp_all
     
 lemma totient_6 [simp]: "totient 6 = 2"
-  using totient_mult_coprime[of 2 3] by (simp add: gcd_non_0_nat)    
+  using totient_mult_coprime [of 2 3] coprime_add_one_right [of 2]
+  by simp
 
 lemma totient_even:
   assumes "n > 2"
@@ -314,11 +315,14 @@
   have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd)
   then obtain m where m: "n = p ^ k * m" by (elim dvdE)
   with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I)
-  from k_def m_pos p have "\<not>p dvd m"
+  from k_def m_pos p have "\<not> p dvd m"
     by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib 
                           prime_elem_multiplicity_eq_zero_iff)
-  hence "coprime (p ^ k) m" by (intro coprime_exp_left prime_imp_coprime[OF p(1)])
-  thus ?thesis using p k_pos \<open>odd p\<close> 
+  with \<open>prime p\<close> have "coprime p m"
+    by (rule prime_imp_coprime)
+  with \<open>k > 0\<close> have "coprime (p ^ k) m"
+    by simp
+  then show ?thesis using p k_pos \<open>odd p\<close> 
     by (auto simp add: m totient_mult_coprime totient_prime_power)
 next
   case False
@@ -341,7 +345,7 @@
 proof (induction A rule: infinite_finite_induct)
   case (insert x A)
   have *: "coprime (prod f A) (f x)"
-  proof (rule prod_coprime)
+  proof (rule prod_coprime_left)
     fix y
     assume "y \<in> A"
     with \<open>x \<notin> A\<close> have "y \<noteq> x"
@@ -388,10 +392,12 @@
   proof (rule totient_prod_coprime)
     show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
     proof (rule pairwiseI, clarify)
-      fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
+      fix p q assume *: "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
                      "p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
-      thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
-        by (intro coprime_exp2 primes_coprime[of p q]) auto
+      then have "multiplicity p n > 0" "multiplicity q n > 0"
+        by (simp_all add: prime_factors_multiplicity)
+      with * primes_coprime [of p q] show "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
+        by auto
     qed
   next
     show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
@@ -475,20 +481,22 @@
   by (subst totient_gcd [symmetric]) simp
 
 lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1"
-  using of_nat_eq_iff[of x 1] by (simp del: of_nat_eq_iff)
+  by (fact of_nat_eq_1_iff)
 
 (* TODO Move *)
-lemma gcd_2_odd:
+lemma odd_imp_coprime_nat:
   assumes "odd (n::nat)"
-  shows   "gcd n 2 = 1"
+  shows   "coprime n 2"
 proof -
   from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE)
-  have "coprime (Suc (2 * k)) (2 * k)" by (rule coprime_Suc_nat)
-  thus ?thesis using n by (subst (asm) coprime_mul_eq) simp_all
+  have "coprime (Suc (2 * k)) (2 * k)"
+    by (fact coprime_Suc_left_nat)
+  then show ?thesis using n
+    by simp
 qed
 
 lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)"
-  by (subst totient_mult) (auto simp: gcd.commute[of 2] gcd_2_odd)
+  by (simp add: totient_mult ac_simps odd_imp_coprime_nat)
 
 lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n"
 proof (induction m arbitrary: n)
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Parity.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -318,6 +318,38 @@
   using mult_div_mod_eq [of 2 a]
   by (simp add: even_iff_mod_2_eq_zero)
 
+lemma coprime_left_2_iff_odd [simp]:
+  "coprime 2 a \<longleftrightarrow> odd a"
+proof
+  assume "odd a"
+  show "coprime 2 a"
+  proof (rule coprimeI)
+    fix b
+    assume "b dvd 2" "b dvd a"
+    then have "b dvd a mod 2"
+      by (auto intro: dvd_mod)
+    with \<open>odd a\<close> show "is_unit b"
+      by (simp add: mod_2_eq_odd)
+  qed
+next
+  assume "coprime 2 a"
+  show "odd a"
+  proof (rule notI)
+    assume "even a"
+    then obtain b where "a = 2 * b" ..
+    with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
+      by simp
+    moreover have "\<not> coprime 2 (2 * b)"
+      by (rule not_coprimeI [of 2]) simp_all
+    ultimately show False
+      by blast
+  qed
+qed
+
+lemma coprime_right_2_iff_odd [simp]:
+  "coprime a 2 \<longleftrightarrow> odd a"
+  using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
+
 end
 
 class ring_parity = ring + semiring_parity
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Rat.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -999,7 +999,7 @@
 proof (cases p)
   case (Fract a b)
   then show ?thesis
-    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute)
+    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract ac_simps)
 qed
 
 lemma rat_divide_code [code abstract]:
@@ -1008,9 +1008,10 @@
      in normalize (a * d, c * b))"
   by (cases p, cases q) (simp add: quotient_of_Fract)
 
-lemma rat_abs_code [code abstract]: "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
+lemma rat_abs_code [code abstract]:
+  "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
   by (cases p) (simp add: quotient_of_Fract)
-
+  
 lemma rat_sgn_code [code abstract]: "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)"
 proof (cases p)
   case (Fract a b)
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Real.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -1245,7 +1245,7 @@
 
 lemma Rats_abs_nat_div_natE:
   assumes "x \<in> \<rat>"
-  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
+  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "coprime m n"
 proof -
   from \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 0" and "x = real_of_int i / real n"
     by (auto simp add: Rats_eq_int_div_nat)
@@ -1281,6 +1281,8 @@
     with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
     with gcd show ?thesis by auto
   qed
+  then have "coprime ?k ?l"
+    by (simp only: coprime_iff_gcd_eq_1)
   ultimately show ?thesis ..
 qed
 
@@ -1415,8 +1417,6 @@
   for m :: nat
   by (metis not_le real_of_nat_less_numeral_iff)
 
-declare of_int_floor_le [simp]  (* FIXME duplicate!? *)
-
 lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
   by (metis floor_of_int)
 
@@ -1424,7 +1424,7 @@
   by linarith
 
 lemma floor_eq2: "real_of_int n \<le> x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
-  by linarith
+  by (fact floor_unique)
 
 lemma floor_eq3: "real n < x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n"
   by linarith
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Rings.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -1161,6 +1161,108 @@
   "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
   by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
 
+
+text \<open>Coprimality\<close>
+
+definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)"
+
+lemma coprimeI:
+  assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c"
+  shows "coprime a b"
+  using assms by (auto simp: coprime_def)
+
+lemma not_coprimeI:
+  assumes "c dvd a" and "c dvd b" and "\<not> is_unit c"
+  shows "\<not> coprime a b"
+  using assms by (auto simp: coprime_def)
+
+lemma coprime_common_divisor:
+  "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b"
+  using that by (auto simp: coprime_def)
+
+lemma not_coprimeE:
+  assumes "\<not> coprime a b"
+  obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c"
+  using assms by (auto simp: coprime_def)
+
+lemma coprime_imp_coprime:
+  "coprime a b" if "coprime c d"
+    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c"
+    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d"
+proof (rule coprimeI)
+  fix e
+  assume "e dvd a" and "e dvd b"
+  with that have "e dvd c" and "e dvd d"
+    by (auto intro: dvd_trans)
+  with \<open>coprime c d\<close> show "is_unit e"
+    by (rule coprime_common_divisor)
+qed
+
+lemma coprime_divisors:
+  "coprime a b" if "a dvd c" "b dvd d" and "coprime c d"
+using \<open>coprime c d\<close> proof (rule coprime_imp_coprime)
+  fix e
+  assume "e dvd a" then show "e dvd c"
+    using \<open>a dvd c\<close> by (rule dvd_trans)
+  assume "e dvd b" then show "e dvd d"
+    using \<open>b dvd d\<close> by (rule dvd_trans)
+qed
+
+lemma coprime_self [simp]:
+  "coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  then show ?Q
+    by (rule coprime_common_divisor) simp_all
+next
+  assume ?Q
+  show ?P
+    by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>)
+qed
+
+lemma coprime_commute [ac_simps]:
+  "coprime b a \<longleftrightarrow> coprime a b"
+  unfolding coprime_def by auto
+
+lemma is_unit_left_imp_coprime:
+  "coprime a b" if "is_unit a"
+proof (rule coprimeI)
+  fix c
+  assume "c dvd a"
+  with that show "is_unit c"
+    by (auto intro: dvd_unit_imp_unit)
+qed
+
+lemma is_unit_right_imp_coprime:
+  "coprime a b" if "is_unit b"
+  using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps)
+
+lemma coprime_1_left [simp]:
+  "coprime 1 a"
+  by (rule coprimeI)
+
+lemma coprime_1_right [simp]:
+  "coprime a 1"
+  by (rule coprimeI)
+
+lemma coprime_0_left_iff [simp]:
+  "coprime 0 a \<longleftrightarrow> is_unit a"
+  by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a])
+
+lemma coprime_0_right_iff [simp]:
+  "coprime a 0 \<longleftrightarrow> is_unit a"
+  using coprime_0_left_iff [of a] by (simp add: ac_simps)
+
+lemma coprime_mult_self_left_iff [simp]:
+  "coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b"
+  by (auto intro: coprime_common_divisor)
+    (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+
+
+lemma coprime_mult_self_right_iff [simp]:
+  "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b"
+  using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)
+
 end
 
 class unit_factor =
@@ -1430,6 +1532,14 @@
   shows "is_unit a \<longleftrightarrow> a = 1"
   using assms by (cases "a = 0") (auto dest: is_unit_normalize)
 
+lemma coprime_normalize_left_iff [simp]:
+  "coprime (normalize a) b \<longleftrightarrow> coprime a b"
+  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
+
+lemma coprime_normalize_right_iff [simp]:
+  "coprime a (normalize b) \<longleftrightarrow> coprime a b"
+  using coprime_normalize_left_iff [of b a] by (simp add: ac_simps)
+
 text \<open>
   We avoid an explicit definition of associated elements but prefer explicit
   normalisation instead. In theory we could define an abbreviation like @{prop
@@ -2435,8 +2545,8 @@
 subclass ordered_ring_abs
   by standard (auto simp: abs_if not_less mult_less_0_iff)
 
-lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
-  by (simp add: abs_if)
+lemma abs_mult_self: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
+  by (fact abs_mult_self_eq)
 
 lemma abs_mult_less:
   assumes ac: "\<bar>a\<bar> < c"
diff -r a462583f0a37 -r b5c1f0c76d35 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/HOL/Set.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -1874,6 +1874,11 @@
 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
   by (auto simp: pairwise_def)
 
+lemma pairwise_imageI:
+  "pairwise P (f ` A)"
+  if "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x \<noteq> f y \<Longrightarrow> P (f x) (f y)"
+  using that by (auto intro: pairwiseI)
+
 lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
   by (force simp: pairwise_def)
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Admin/afp.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -35,7 +35,7 @@
 
   val sessions: List[String] = entries.flatMap(_.sessions)
 
-  val sessions_structure: Sessions.T =
+  val sessions_structure: Sessions.Structure =
     Sessions.load_structure(options, dirs = List(main_dir)).
       selection(Sessions.Selection(sessions = sessions.toList))
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Admin/build_history.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -96,6 +96,7 @@
 
   /** build_history **/
 
+  private val default_user_home = Path.explode("$USER_HOME")
   private val default_rev = "tip"
   private val default_multicore = (1, 1)
   private val default_heap = 1500
@@ -104,6 +105,7 @@
   def build_history(
     options: Options,
     root: Path,
+    user_home: Path = default_user_home,
     progress: Progress = No_Progress,
     rev: String = default_rev,
     afp_rev: Option[String] = None,
@@ -170,7 +172,9 @@
 
     /* main */
 
-    val other_isabelle = new Other_Isabelle(progress, root, isabelle_identifier)
+    val other_isabelle =
+      Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
+        user_home = user_home, progress = progress)
 
     val build_host = Isabelle_System.hostname()
     val build_history_date = Date.now()
@@ -226,9 +230,10 @@
       val build_start = Date.now()
       val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
       val build_result =
-        (new Other_Isabelle(build_out_progress, root, isabelle_identifier))(
-          "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true,
-          strict = false)
+        Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
+          user_home = user_home, progress = build_out_progress)(
+            "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true,
+            strict = false)
       val build_end = Date.now()
 
       val build_info: Build_Log.Build_Info =
@@ -396,11 +401,12 @@
       var rev = default_rev
       var ml_statistics_step = 1
       var build_tags = List.empty[String]
+      var user_home = default_user_home
       var verbose = false
       var exit_code = false
 
       val getopts = Getopts("""
-Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
+Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
 
   Options are:
     -A REV       include $ISABELLE_HOME/AFP repository at given revision
@@ -421,6 +427,7 @@
     -r REV       update to revision (default: """ + default_rev + """)
     -s NUMBER    step size for ML statistics (0=none, 1=all, n=step, default: 1)
     -t TAG       free-form build tag (multiple occurrences possible)
+    -u DIR       alternative USER_HOME directory
     -v           verbose
     -x           return overall exit code from build processes
 
@@ -452,6 +459,7 @@
         "r:" -> (arg => rev = arg),
         "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
+        "u:" -> (arg => user_home = Path.explode(arg)),
         "v" -> (_ => verbose = true),
         "x" -> (_ => exit_code = true))
 
@@ -465,11 +473,12 @@
       val progress = new Console_Progress(stderr = true)
 
       val results =
-        build_history(Options.init(), root, progress = progress, rev = rev, afp_rev = afp_rev,
-          afp_partition = afp_partition, isabelle_identifier = isabelle_identifier,
-          ml_statistics_step = ml_statistics_step, components_base = components_base, fresh = fresh,
-          nonfree = nonfree, multicore_base = multicore_base, multicore_list = multicore_list,
-          arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
+        build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
+          afp_rev = afp_rev, afp_partition = afp_partition,
+          isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
+          components_base = components_base, fresh = fresh, nonfree = nonfree,
+          multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
+          heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
           max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
           verbose = verbose, build_tags = build_tags, build_args = build_args)
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -892,7 +892,7 @@
         user = user, password = password, database = database, host = host, port = port,
         ssh =
           if (ssh_host == "") None
-          else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)),
+          else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = port)),
         ssh_close = true)
     }
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Admin/build_release.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -163,7 +163,8 @@
             execute_tar("xzf " + File.bash_path(bundle))
 
             val other_isabelle =
-              new Other_Isabelle(progress, tmp_dir + Path.explode(name), name + "-build")
+              Other_Isabelle(tmp_dir + Path.explode(name),
+                isabelle_identifier = name + "-build", progress = progress)
 
             other_isabelle.bash("bin/isabelle build" + jobs_option +
                 " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -264,7 +264,7 @@
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
 
   private def remote_build_history(
-    rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task =
+    rev: String, afp_rev: Option[String], i: Int, user_home: Boolean, r: Remote_Build): Logger_Task =
   {
     val task_name = "build_history-" + r.host
     Logger_Task(task_name, logger =>
@@ -275,6 +275,14 @@
               val self_update = !r.shared_home
               val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
 
+              if (user_home && r.shared_home) {
+                ssh.execute("""
+if [ ! -e /tmp/isabelle-isatest/contrib ]
+then
+  mkdir -p /tmp/isabelle-isatest && ln -s /home/isabelle/contrib /tmp/isabelle-isatest
+fi""").check
+              }
+
               val results =
                 Build_History.remote_build_history(ssh,
                   isabelle_repos,
@@ -285,6 +293,7 @@
                   rev = rev,
                   afp_rev = afp_rev,
                   options =
+                    (if (user_home && r.shared_home) " -u /tmp/isabelle-isatest" else "") +
                     " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
                     " -f " + r.options,
                   args = "-o timeout=10800 " + r.args)
@@ -438,7 +447,9 @@
 
     val hg = Mercurial.repository(isabelle_repos)
     val hg_graph = hg.graph()
-    val rev = hg.id()
+
+    val user_home: String => Boolean =
+      hg_graph.all_succs(List("19b6091c2137")).contains(_)
 
     def history_base_filter(r: Remote_Build): Item => Boolean =
     {
@@ -463,8 +474,8 @@
                   SEQ(
                     for {
                       (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
-                      (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, history_base_filter(r))
-                    } yield remote_build_history(isabelle_rev, afp_rev, i, r)))),
+                      (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
+                    } yield remote_build_history(rev, afp_rev, i, user_home(rev), r)))),
                 Logger_Task("jenkins_logs", _ =>
                   Jenkins.download_logs(Jenkins.build_log_jobs, main_dir)),
                 Logger_Task("build_log_database",
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -7,10 +7,28 @@
 package isabelle
 
 
-class Other_Isabelle(progress: Progress, val isabelle_home: Path, val isabelle_identifier: String)
+object Other_Isabelle
+{
+  def apply(isabelle_home: Path,
+      isabelle_identifier: String = "",
+      user_home: Path = Path.explode("$USER_HOME"),
+      progress: Progress = No_Progress): Other_Isabelle =
+    new Other_Isabelle(isabelle_home, isabelle_identifier, user_home, progress)
+}
+
+class Other_Isabelle(
+  val isabelle_home: Path,
+  val isabelle_identifier: String,
+  user_home: Path,
+  progress: Progress)
 {
   other_isabelle =>
 
+  override def toString: String = isabelle_home.toString
+
+  if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
+    error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
+
 
   /* static system */
 
@@ -19,7 +37,9 @@
       redirect: Boolean = false,
       echo: Boolean = false,
       strict: Boolean = true): Process_Result =
-    progress.bash(Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
+    progress.bash(
+      "export USER_HOME=" + File.bash_path(user_home) + "\n" +
+      Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
       env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
 
   def apply(
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Admin/remote_dmg.scala
--- a/src/Pure/Admin/remote_dmg.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Admin/remote_dmg.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -56,8 +56,8 @@
             case _ => getopts.usage()
           }
 
-        val ssh = SSH.init_context(Options.init)
-        using(ssh.open_session(user = user, host = host, port = port))(
+        val options = Options.init
+        using(SSH.open_session(options, host = host, user = user, port = port))(
           remote_dmg(_, tar_gz_file, dmg_file, volume_name))
       }
     }, admin = true)
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/General/mercurial.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -52,16 +52,23 @@
     find(ssh.expand_path(start))
   }
 
-  def clone_repository(source: String, root: Path, rev: String = "", options: String = "",
-    ssh: SSH.System = SSH.Local): Repository =
+  private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
+    : Repository =
   {
     val hg = new Repository(root, ssh)
     ssh.mkdirs(hg.root.dir)
-    hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options)
-      .check
+    hg.command(cmd, args, repository = false).check
     hg
   }
 
+  def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
+    make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
+
+  def clone_repository(source: String, root: Path,
+      rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
+    make_repository(root, "clone",
+      options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
+
   def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
   {
     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
@@ -77,15 +84,19 @@
 
     override def toString: String = ssh.prefix + root.implode
 
-    def command(name: String, args: String = "", options: String = ""): Process_Result =
+    def command(name: String, args: String = "", options: String = "",
+      repository: Boolean = true): Process_Result =
     {
       val cmdline =
         "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
-          (if (name == "clone") "" else " --repository " + File.bash_path(root)) +
+          (if (repository) " --repository " + ssh.bash_path(root) else "") +
           " --noninteractive " + name + " " + options + " " + args
       ssh.execute(cmdline)
     }
 
+    def add(files: List[Path]): Unit =
+      hg.command("add", files.map(ssh.bash_path(_)).mkString(" "))
+
     def archive(target: String, rev: String = "", options: String = ""): Unit =
       hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
 
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/General/ssh.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -70,6 +70,9 @@
     new Context(options, jsch)
   }
 
+  def open_session(options: Options, host: String, user: String = "", port: Int = 0): Session =
+    init_context(options).open_session(host = host, user = user, port = port)
+
   class Context private[SSH](val options: Options, val jsch: JSch)
   {
     def update_options(new_options: Options): Context = new Context(new_options, jsch)
@@ -294,7 +297,7 @@
     }
     override def expand_path(path: Path): Path = path.expand_env(settings)
     def remote_path(path: Path): String = expand_path(path).implode
-    def bash_path(path: Path): String = Bash.string(remote_path(path))
+    override def bash_path(path: Path): String = Bash.string(remote_path(path))
 
     def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
     def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
@@ -400,6 +403,7 @@
     def prefix: String = ""
 
     def expand_path(path: Path): Path = path.expand
+    def bash_path(path: Path): String = File.bash_path(path)
     def is_file(path: Path): Boolean = path.is_file
     def is_dir(path: Path): Boolean = path.is_dir
     def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -23,7 +23,7 @@
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None,
-    sessions: Option[Sessions.T] = None,
+    sessions: Option[Sessions.Structure] = None,
     session_base: Option[Sessions.Base] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -19,25 +19,8 @@
 {
   resources =>
 
-
-  /* theory files */
-
   def thy_path(path: Path): Path = path.ext("thy")
 
-  def thy_node_name(qualifier: String, file: JFile, bootstrap: Boolean = false)
-    : Document.Node.Name =
-  {
-    session_base.known.get_file(file, bootstrap) getOrElse {
-      val node = file.getPath
-      theory_name(qualifier, Thy_Header.theory_name(node)) match {
-        case (true, theory) => Document.Node.Name.loaded_theory(theory)
-        case (false, theory) =>
-          val master_dir = if (theory == "") "" else file.getParent
-          Document.Node.Name(node, master_dir, theory)
-      }
-    }
-  }
-
 
   /* file-system operations */
 
@@ -249,10 +232,16 @@
       new Dependencies(rev_entries, seen + name)
 
     def entries: List[Document.Node.Entry] = rev_entries.reverse
-    def names: List[Document.Node.Name] = entries.map(_.name)
+    def theories: List[Document.Node.Name] = entries.map(_.name)
 
     def errors: List[String] = entries.flatMap(_.header.errors)
 
+    def check_errors: Dependencies =
+      errors match {
+        case Nil => this
+        case errs => error(cat_lines(errs))
+      }
+
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       (session_base.loaded_theories /: entries)({ case (graph, entry) =>
         val name = entry.name.theory
@@ -270,15 +259,15 @@
 
     def loaded_files: List[(String, List[Path])] =
     {
-      names.map(_.theory) zip
+      theories.map(_.theory) zip
         Par_List.map((e: () => List[Path]) => e(),
-          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+          theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
     }
 
     def imported_files: List[Path] =
     {
       val base_theories =
-        loaded_theories.all_preds(names.map(_.theory)).
+        loaded_theories.all_preds(theories.map(_.theory)).
           filter(session_base.loaded_theories.defined(_))
 
       base_theories.map(theory => session_base.known.theories(theory).path) :::
@@ -310,21 +299,23 @@
       "The error(s) above occurred for theory " + quote(name.theory) +
         required_by(initiators) + Position.here(pos)
 
-    val required1 = required + name
     if (required.seen(name)) required
-    else if (session_base.loaded_theory(name)) required1
     else {
-      try {
-        if (initiators.contains(name)) error(cycle_msg(initiators))
-        val header =
-          try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
-          catch { case ERROR(msg) => cat_error(msg, message) }
-        Document.Node.Entry(name, header) ::
-          require_thys(name :: initiators, required1, header.imports)
-      }
-      catch {
-        case e: Throwable =>
-          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
+      val required1 = required + name
+      if (session_base.loaded_theory(name)) required1
+      else {
+        try {
+          if (initiators.contains(name)) error(cycle_msg(initiators))
+          val header =
+            try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
+            catch { case ERROR(msg) => cat_error(msg, message) }
+          Document.Node.Entry(name, header) ::
+            require_thys(name :: initiators, required1, header.imports)
+        }
+        catch {
+          case e: Throwable =>
+            Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
+        }
       }
     }
   }
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/System/isabelle_process.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -20,7 +20,7 @@
     modes: List[String] = Nil,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
-    sessions: Option[Sessions.T] = None,
+    sessions: Option[Sessions.Structure] = None,
     store: Sessions.Store = Sessions.store(),
     phase_changed: Session.Phase => Unit = null)
   {
@@ -43,7 +43,7 @@
     env: Map[String, String] = Isabelle_System.settings(),
     receiver: Prover.Receiver = Console.println(_),
     xml_cache: XML.Cache = new XML.Cache(),
-    sessions: Option[Sessions.T] = None,
+    sessions: Option[Sessions.Structure] = None,
     store: Sessions.Store = Sessions.store()): Prover =
   {
     val channel = System_Channel()
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -110,6 +110,7 @@
       Check_Sources.isabelle_tool,
       Doc.isabelle_tool,
       Imports.isabelle_tool,
+      Mkroot.isabelle_tool,
       ML_Process.isabelle_tool,
       NEWS.isabelle_tool,
       Options.isabelle_tool,
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -175,7 +175,7 @@
       }
   }
 
-  def deps(sessions_structure: T,
+  def deps(sessions_structure: Structure,
       global_theories: Map[String, String],
       progress: Progress = No_Progress,
       inlined_files: Boolean = false,
@@ -227,21 +227,21 @@
               progress.echo("Session " + info.chapter + "/" + info.name + groups)
             }
 
-            val thy_deps =
+            val dependencies =
               resources.dependencies(
                 for { (_, thys) <- info.theories; (thy, pos) <- thys }
                 yield (resources.import_name(info.name, info.dir.implode, thy), pos))
 
-            val overall_syntax = thy_deps.overall_syntax
+            val overall_syntax = dependencies.overall_syntax
 
-            val theory_files = thy_deps.names.map(_.path)
+            val theory_files = dependencies.theories.map(_.path)
             val loaded_files =
               if (inlined_files) {
                 if (Sessions.is_pure(info.name)) {
                   (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
-                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
+                    dependencies.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
                 }
-                else thy_deps.loaded_files
+                else dependencies.loaded_files
               }
               else Nil
 
@@ -249,7 +249,7 @@
               (theory_files ::: loaded_files.flatMap(_._2) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
-            val imported_files = if (inlined_files) thy_deps.imported_files else Nil
+            val imported_files = if (inlined_files) dependencies.imported_files else Nil
 
             if (list_files)
               progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
@@ -283,7 +283,7 @@
                       val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
                       ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
 
-              (graph0 /: thy_deps.entries)(
+              (graph0 /: dependencies.entries)(
                 { case (g, entry) =>
                     val a = node(entry.name)
                     val bs =
@@ -294,7 +294,7 @@
 
             val known =
               Known.make(info.dir, List(imports_base),
-                theories = thy_deps.names,
+                theories = dependencies.theories,
                 loaded_files = loaded_files)
 
             val sources_errors =
@@ -304,13 +304,13 @@
               Base(
                 pos = info.pos,
                 global_theories = global_theories,
-                loaded_theories = thy_deps.loaded_theories,
+                loaded_theories = dependencies.loaded_theories,
                 known = known,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
                 sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
-                errors = thy_deps.errors ::: sources_errors,
+                errors = dependencies.errors ::: sources_errors,
                 imports = Some(imports_base))
 
             session_bases + (info.name -> base)
@@ -330,7 +330,7 @@
 
   sealed case class Base_Info(
     session: String,
-    sessions_structure: T,
+    sessions_structure: Structure,
     errors: List[String],
     base: Base,
     infos: List[Info])
@@ -542,7 +542,7 @@
     }
   }
 
-  def make(infos: List[Info]): T =
+  def make(infos: List[Info]): Structure =
   {
     def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
       : Graph[String, Info] =
@@ -577,10 +577,10 @@
     val graph1 = add_edges(graph0, "parent", _.parent)
     val graph2 = add_edges(graph1, "imports", _.imports)
 
-    new T(graph1, graph2)
+    new Structure(graph1, graph2)
   }
 
-  final class T private[Sessions](
+  final class Structure private[Sessions](
       val build_graph: Graph[String, Info],
       val imports_graph: Graph[String, Info])
   {
@@ -606,7 +606,7 @@
               }
           })
 
-    def selection(sel: Selection): T =
+    def selection(sel: Selection): Structure =
     {
       val bad_sessions =
         SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
@@ -622,7 +622,7 @@
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
-      new T(restrict(build_graph), restrict(imports_graph))
+      new Structure(restrict(build_graph), restrict(imports_graph))
     }
 
     def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
@@ -636,7 +636,7 @@
     def imports_topological_order: List[String] = imports_graph.topological_order
 
     override def toString: String =
-      imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
+      imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
   }
 
 
@@ -788,7 +788,7 @@
   def load_structure(options: Options,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
-    infos: List[Info] = Nil): T =
+    infos: List[Info] = Nil): Structure =
   {
     def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
       load_root(select, dir) ::: load_roots(select, dir)
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Thy/thy_document_model.scala
--- a/src/Pure/Thy/thy_document_model.scala	Tue Nov 14 13:12:13 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-/*  Title:      Pure/Thy/thy_document_model.scala
-    Author:     Makarius
-
-Document model for theory files: no edits, no blobs, no overlays.
-*/
-
-package isabelle
-
-
-object Thy_Document_Model
-{
-  def read_file(session: Session, path: Path,
-    qualifier: String = Sessions.DRAFT,
-    node_visible: Boolean = false,
-    node_required: Boolean = false): Thy_Document_Model =
-  {
-    val node_name = session.resources.thy_node_name(qualifier, path.file)
-    if (!node_name.is_theory) error("Not a theory file: " + path)
-    new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required)
-  }
-}
-
-final class Thy_Document_Model private(
-  val session: Session,
-  val node_name: Document.Node.Name,
-  val text: String,
-  val node_visible: Boolean,
-  val node_required: Boolean) extends Document.Model
-{
-  /* content */
-
-  def get_text(range: Text.Range): Option[String] =
-    if (0 <= range.start && range.stop <= text.length) Some(range.substring(text)) else None
-
-  def get_blob: Option[Document.Blob] = None
-
-  def bibtex_entries: List[Text.Info[String]] = Nil
-
-
-  /* header */
-
-  def node_header: Document.Node.Header =
-    resources.check_thy_reader(node_name, Scan.char_reader(text))
-
-
-  /* perspective */
-
-  def text_perspective: Text.Perspective =
-    if (node_visible) Text.Perspective.full else Text.Perspective.empty
-
-  def node_perspective: Document.Node.Perspective_Text =
-    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
-
-
-  /* prover session */
-
-  def resources: Resources = session.resources
-
-  def is_stable: Boolean = true
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits = Nil)
-}
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Thy/thy_resources.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_resources.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -0,0 +1,174 @@
+/*  Title:      Pure/Thy/thy_resources.scala
+    Author:     Makarius
+
+PIDE resources for theory files.
+*/
+
+package isabelle
+
+
+object Thy_Resources
+{
+  /* PIDE session */
+
+  def start_session(
+    options: Options,
+    session_name: String,
+    session_dirs: List[Path] = Nil,
+    session_base: Option[Sessions.Base] = None,
+    modes: List[String] = Nil,
+    log: Logger = No_Logger): Session =
+  {
+    val base =
+      session_base getOrElse
+        Sessions.base_info(options, session_name, dirs = session_dirs).check_base
+    val resources = new Thy_Resources(base, log = log)
+    val session = new Session(options, resources)
+
+    val session_error = Future.promise[String]
+    var session_phase: Session.Consumer[Session.Phase] = null
+    session_phase =
+      Session.Consumer(getClass.getName) {
+        case Session.Ready =>
+          session.phase_changed -= session_phase
+          session_error.fulfill("")
+        case Session.Terminated(result) if !result.ok =>
+          session.phase_changed -= session_phase
+          session_error.fulfill("Prover startup failed: return code " + result.rc)
+        case _ =>
+      }
+    session.phase_changed += session_phase
+
+    Isabelle_Process.start(session, options,
+      logic = session_name, dirs = session_dirs, modes = modes)
+
+    session_error.join match {
+      case "" => session
+      case msg => session.stop(); error(msg)
+    }
+  }
+
+  class Session private[Thy_Resources](
+    session_options: Options,
+    override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
+  {
+    session =>
+
+    def use_theories(
+      theories: List[(String, Position.T)],
+      qualifier: String = Sessions.DRAFT,
+      master_dir: String = ""): (List[Document.Node.Name], Document.State) =
+    {
+      val requirements =
+        resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir)
+      val state = consolidated_state(requirements)
+      (requirements, state)
+    }
+
+    def consolidated_state(requirements: List[Document.Node.Name]): Document.State =
+    {
+      val promise = Future.promise[Document.State]
+
+      def check_state
+      {
+        val state = session.current_state()
+        state.stable_tip_version match {
+          case Some(version) if requirements.forall(state.node_consolidated(version, _)) =>
+            try { promise.fulfill(state) }
+            catch { case _: IllegalStateException => }
+          case _ =>
+        }
+      }
+
+      val consumer =
+        Session.Consumer[Session.Commands_Changed](getClass.getName) {
+          case changed => if (requirements.exists(changed.nodes)) check_state
+        }
+
+      session.commands_changed += consumer
+      check_state
+      val state = promise.join
+      session.commands_changed -= consumer
+      state
+    }
+  }
+
+
+  /* internal state */
+
+  sealed case class State(theories: Map[Document.Node.Name, Theory] = Map.empty)
+
+  final class Theory private[Thy_Resources](
+    val node_name: Document.Node.Name,
+    val node_header: Document.Node.Header,
+    val text: String)
+  {
+    override def toString: String = node_name.toString
+
+    def node_perspective: Document.Node.Perspective_Text =
+      Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)
+
+    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
+    {
+      val text_edits =
+        if (old.isEmpty) Text.Edit.inserts(0, text)
+        else Text.Edit.replace(0, old.get.text, text)
+
+      if (text_edits.isEmpty) Nil
+      else
+        List(node_name -> Document.Node.Deps(node_header),
+          node_name -> Document.Node.Edits(text_edits),
+          node_name -> node_perspective)
+    }
+  }
+}
+
+class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
+  extends Resources(session_base, log = log)
+{
+  resources =>
+
+  private val state = Synchronized(Thy_Resources.State())
+
+  def read_thy(node_name: Document.Node.Name): Thy_Resources.Theory =
+  {
+    val path = node_name.path
+    if (!node_name.is_theory) error("Not a theory file: " + path)
+
+    val text = File.read(path)
+    val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
+    new Thy_Resources.Theory(node_name, node_header, text)
+  }
+
+  def load_theories(
+    session: Session,
+    theories: List[(String, Position.T)],
+    qualifier: String = Sessions.DRAFT,
+    master_dir: String = ""): List[Document.Node.Name] =
+  {
+    val import_names =
+      for ((thy, pos) <- theories)
+      yield (import_name(qualifier, master_dir, thy), pos)
+
+    val dependencies = resources.dependencies(import_names).check_errors
+    val loaded_theories = dependencies.theories.map(read_thy(_))
+
+    val edits =
+      state.change_result(st =>
+      {
+        val theory_edits =
+          for {
+            theory <- loaded_theories
+            node_name = theory.node_name
+            edits = theory.node_edits(st.theories.get(node_name))
+            if edits.nonEmpty
+          } yield ((node_name, theory), edits)
+
+        val st1 = st.copy(theories = st.theories ++ theory_edits.map(_._1))
+        (theory_edits.flatMap(_._2), st1)
+      })
+    session.update(Document.Blobs.empty, edits)
+
+    dependencies.theories
+  }
+}
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -71,7 +71,7 @@
       }
     }
 
-    def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
+    def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
     {
       val graph = sessions.build_graph
       val names = graph.keys
@@ -178,7 +178,7 @@
   private class Job(progress: Progress,
     name: String,
     val info: Sessions.Info,
-    sessions: Sessions.T,
+    sessions: Sessions.Structure,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_output: Boolean,
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/Tools/mkroot.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/mkroot.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -0,0 +1,214 @@
+/*  Title:      Pure/Tools/mkroot.scala
+    Author:     Makarius
+
+Prepare session root directory.
+*/
+
+package isabelle
+
+
+object Mkroot
+{
+  /** mkroot **/
+
+  def root_name(name: String): String =
+    Token.quote_name(Sessions.root_syntax.keywords, name)
+
+  def latex_name(name: String): String =
+    (for (c <- name.iterator if c != '\\')
+     yield if (c == '_') '-' else c).mkString
+
+  def mkroot(
+    session_name: String = "",
+    session_dir: Path = Path.current,
+    session_parent: String = "",
+    init_repos: Boolean = false,
+    title: String = "",
+    author: String = "",
+    progress: Progress = No_Progress)
+  {
+    Isabelle_System.mkdirs(session_dir)
+
+    val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
+    val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
+
+    val root_path = session_dir + Path.explode("ROOT")
+    if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
+
+    val document_path = session_dir + Path.explode("document")
+    if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
+
+    val root_tex = session_dir + Path.explode("document/root.tex")
+
+
+    progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
+
+
+    /* ROOT */
+
+    progress.echo("  creating " + root_path)
+
+    File.write(root_path,
+      "session " + root_name(name) + " = " + root_name(parent) + """ +
+  options [document = pdf, document_output = "output"]
+(*theories [document = false]
+    A
+    B
+  theories
+    C
+    D*)
+  document_files
+    "root.tex"
+""")
+
+
+    /* document directory */
+
+    {
+      progress.echo("  creating " + root_tex)
+
+      Isabelle_System.mkdirs(root_tex.dir)
+
+      File.write(root_tex,
+"""\documentclass[11pt,a4paper]{article}
+\""" + """usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\""" + """usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\""" + """usepackage{eurosym}
+  %for \<euro>
+
+%\""" + """usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\""" + """usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\""" + """usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\""" + """usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\""" + """urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{""" + (proper_string(title) getOrElse latex_name(name)) + """}
+\author{""" + (proper_string(author) getOrElse latex_name(System.getProperty("user.name"))) + """}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+""")
+    }
+
+
+    /* Mercurial repository */
+
+    if (init_repos) {
+      progress.echo("  \nInitializing Mercurial repository " + session_dir)
+
+      val hg = Mercurial.init_repository(session_dir)
+
+      val hg_ignore = session_dir + Path.explode(".hgignore")
+      File.write(hg_ignore,
+"""syntax: glob
+
+*~
+*.marks
+*.orig
+*.rej
+.DS_Store
+.swp
+
+syntax: regexp
+
+^output/
+""")
+
+      hg.add(List(root_path, root_tex, hg_ignore))
+    }
+
+
+    /* notes */
+
+    {
+      val print_dir = session_dir.implode
+      progress.echo("""
+Now use the following command line to build the session:
+
+  isabelle build -D """ +
+        (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
+    }
+  }
+
+
+
+  /** Isabelle tool wrapper **/
+
+  val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
+  {
+    var author = ""
+    var init_repos = false
+    var title = ""
+    var session_name = ""
+
+    val getopts = Getopts("""
+Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
+
+  Options are:
+    -A LATEX     provide author in LaTeX notation (default: user name)
+    -I           init Mercurial repository and add generated files
+    -T LATEX     provide title in LaTeX notation (default: session name)
+    -n NAME      alternative session name (default: directory base name)
+
+  Prepare session root directory (default: current directory).
+""",
+      "A:" -> (arg => author = arg),
+      "I" -> (arg => init_repos = true),
+      "T:" -> (arg => title = arg),
+      "n:" -> (arg => session_name = arg))
+
+    val more_args = getopts(args)
+
+    val session_dir =
+      more_args match {
+        case Nil => Path.current
+        case List(dir) => Path.explode(dir)
+        case _ => getopts.usage()
+      }
+
+    mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
+      author = author, title = title, progress = new Console_Progress)
+  })
+}
diff -r a462583f0a37 -r b5c1f0c76d35 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Pure/build-jars	Tue Nov 14 13:12:48 2017 +0100
@@ -128,8 +128,8 @@
   Thy/html.scala
   Thy/present.scala
   Thy/sessions.scala
-  Thy/thy_document_model.scala
   Thy/thy_header.scala
+  Thy/thy_resources.scala
   Thy/thy_syntax.scala
   Tools/bibtex.scala
   Tools/build.scala
@@ -139,6 +139,7 @@
   Tools/doc.scala
   Tools/imports.scala
   Tools/main.scala
+  Tools/mkroot.scala
   Tools/print_operation.scala
   Tools/profiling_report.scala
   Tools/server.scala
diff -r a462583f0a37 -r b5c1f0c76d35 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -91,7 +91,15 @@
   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
 
   def node_name(file: JFile): Document.Node.Name =
-    thy_node_name(Sessions.DRAFT, file, bootstrap = true)
+    session_base.known.get_file(file, bootstrap = true) getOrElse {
+      val node = file.getPath
+      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
+        case (true, theory) => Document.Node.Name.loaded_theory(theory)
+        case (false, theory) =>
+          val master_dir = if (theory == "") "" else file.getParent
+          Document.Node.Name(node, master_dir, theory)
+      }
+    }
 
   override def append(dir: String, source_path: Path): String =
   {
@@ -208,7 +216,7 @@
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
-        val thy_files = dependencies(thys).names
+        val thy_files = dependencies(thys).theories
 
 
         /* auxiliary files */
diff -r a462583f0a37 -r b5c1f0c76d35 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -253,7 +253,7 @@
               val pending_nodes = for ((node_name, None) <- purged) yield node_name
               (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
             }
-            val retain = PIDE.resources.dependencies(imports).names.toSet
+            val retain = PIDE.resources.dependencies(imports).theories.toSet
 
             for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
               yield edit
diff -r a462583f0a37 -r b5c1f0c76d35 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Nov 14 13:12:13 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Nov 14 13:12:48 2017 +0100
@@ -126,7 +126,7 @@
           val thys =
             (for ((node_name, model) <- models.iterator if model.is_theory)
               yield (node_name, Position.none)).toList
-          val thy_files = resources.dependencies(thys).names
+          val thy_files = resources.dependencies(thys).theories
 
           val aux_files =
             if (options.bool("jedit_auto_resolve")) {