isabelle: changeset 76402:2fd70eb1e9b6

--- a/Admin/components/components.sha1	Fri Oct 28 15:39:35 2022 +0200
+++ b/Admin/components/components.sha1	Wed Nov 02 18:58:38 2022 +0100
@@ -90,6 +90,7 @@
 813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz
 6e63f9f354b8c06035952845b987080699a12d55 e-2.6-1.tar.gz
 a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz
+239e7b8bebbfc29a1c5151e8fb261ffad44877f1 easychair-3.5.tar.gz
 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
 8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
 e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
@@ -104,6 +105,7 @@
 9534b721b7b78344f3225067ee4df28a5440b87e flatlaf-1.6.4.tar.gz
 212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz
 6d4dbb6f2bde5804298d9008e3edceb0b9ee20ae flatlaf-2.4.tar.gz
+b1c40ce6c087da7e70e221ddd3fcadfa569acb2f foiltex-2.1.4b.tar.gz
 f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
 71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz
 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
@@ -279,6 +281,7 @@
 377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
 759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz
 1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz
+5557b396f5a9aa22388d3e2171f9bc58e4bd6cd7 lipics-3.1.2.tar.gz
 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
 ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
 400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz

--- a/Admin/components/main	Fri Oct 28 15:39:35 2022 +0200
+++ b/Admin/components/main	Wed Nov 02 18:58:38 2022 +0100
@@ -6,7 +6,9 @@
 csdp-6.1.1
 cvc4-1.8
 e-2.6-1
+easychair-3.5
 flatlaf-2.4
+foiltex-2.1.4b
 idea-icons-20210508
 isabelle_fonts-20211004
 isabelle_setup-20221028
@@ -15,6 +17,7 @@
 jfreechart-1.5.3
 jortho-1.0-2
 kodkodi-1.5.7
+lipics-3.1.2
 minisat-2.2.1-1
 mlton-20210117-1
 nunchaku-0.5

--- a/NEWS	Fri Oct 28 15:39:35 2022 +0200
+++ b/NEWS	Wed Nov 02 18:58:38 2022 +0100
@@ -7,6 +7,16 @@
 New in this Isabelle version
 ----------------------------
 
+*** Document preparation ***
+
+* Various well-known LaTeX styles are included as Isabelle components,
+with demo documents in the regular Isabelle "doc" space:
+
+  - Easychair as session "Demo_Easychair" / doc "demo_easychair"
+  - FoilTeX as session "Demo_FoilTeX" / doc "demo_foiltex"
+  - Dagstuhl LIPIcs style as session "Demo_LIPIcs" / doc "demo_lipics"
+
+
 *** HOL ***
 
 * Theory "HOL.Fun":

--- a/doc/Contents	Fri Oct 28 15:39:35 2022 +0200
+++ b/doc/Contents	Wed Nov 02 18:58:38 2022 +0100
@@ -18,8 +18,14 @@
   system          The Isabelle System Manual
   jedit           Isabelle/jEdit
 
+Demo Documents
+  demo_easychair  Demo for Easychair style
+  demo_foiltex    Demo for FoilTeX: slides in LaTeX
+  demo_lipics     Demo for Dagstuhl LIPIcs style
+
 Old Isabelle Manuals
   tutorial        Tutorial on Isabelle/HOL
   intro           Old Introduction to Isabelle
   logics          Isabelle's Logics: HOL and misc logics
   logics-ZF       Isabelle's Logics: FOL and ZF
+

--- a/etc/build.props	Fri Oct 28 15:39:35 2022 +0200
+++ b/etc/build.props	Wed Nov 02 18:58:38 2022 +0100
@@ -11,16 +11,19 @@
   src/HOL/Tools/Mirabelle/mirabelle.scala \
   src/HOL/Tools/Nitpick/kodkod.scala \
   src/Pure/Admin/afp.scala \
+  src/Pure/Admin/build_csdp.scala \
   src/Pure/Admin/build_cvc5.scala \
-  src/Pure/Admin/build_csdp.scala \
   src/Pure/Admin/build_cygwin.scala \
   src/Pure/Admin/build_doc.scala \
   src/Pure/Admin/build_e.scala \
+  src/Pure/Admin/build_easychair.scala \
+  src/Pure/Admin/build_foiltex.scala \
   src/Pure/Admin/build_fonts.scala \
   src/Pure/Admin/build_history.scala \
   src/Pure/Admin/build_jcef.scala \
   src/Pure/Admin/build_jdk.scala \
   src/Pure/Admin/build_jedit.scala \
+  src/Pure/Admin/build_lipics.scala \
   src/Pure/Admin/build_log.scala \
   src/Pure/Admin/build_minisat.scala \
   src/Pure/Admin/build_pdfjs.scala \
@@ -251,7 +254,6 @@
   src/Tools/jEdit/src/isabelle.scala \
   src/Tools/jEdit/src/isabelle_encoding.scala \
   src/Tools/jEdit/src/isabelle_export.scala \
-  src/Tools/jEdit/src/isabelle_options.scala \
   src/Tools/jEdit/src/isabelle_session.scala \
   src/Tools/jEdit/src/isabelle_vfs.scala \
   src/Tools/jEdit/src/jedit_bibtex.scala \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_Easychair/Document.thy	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,64 @@
+theory Document
+  imports Main
+begin
+
+section \<open>Some section\<close>
+
+subsection \<open>Some subsection\<close>
+
+subsection \<open>Some subsubsection\<close>
+
+subsubsection \<open>Some subsubsubsection\<close>
+
+paragraph \<open>A paragraph.\<close>
+
+text \<open>Informal bla bla.\<close>
+
+definition "foo = True"  \<comment> \<open>side remark on \<^const>\<open>foo\<close>\<close>
+
+definition "bar = False"  \<comment> \<open>side remark on \<^const>\<open>bar\<close>\<close>
+
+lemma foo unfolding foo_def ..
+
+
+paragraph \<open>Another paragraph.\<close>
+
+text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+
+
+section \<open>Formal proof of Cantor's theorem\<close>
+
+text_raw \<open>\isakeeptag{proof}\<close>
+text \<open>
+  Cantor's Theorem states that there is no surjection from
+  a set to its powerset.  The proof works by diagonalization.  E.g.\ see
+  \<^item> \<^url>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
+  \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
+\<close>
+
+theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+proof
+  assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+  then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
+  let ?D = "{x. x \<notin> f x}"
+  from * obtain a where "?D = f a" by blast
+  moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
+  ultimately show False by blast
+qed
+
+
+subsection \<open>Lorem ipsum dolor\<close>
+
+text \<open>
+  Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec id ipsum
+  sapien. Vivamus malesuada enim nibh, a tristique nisi sodales ac. Praesent
+  ut sem consectetur, interdum tellus ac, sodales nulla. Quisque vel diam at
+  risus tempus tempor eget a tortor. Suspendisse potenti. Nulla erat lacus,
+  dignissim sed volutpat nec, feugiat non leo. Nunc blandit et justo sed
+  venenatis. Donec scelerisque placerat magna, et congue nulla convallis vel.
+  Cras tristique dolor consequat dolor tristique rutrum. Suspendisse ultrices
+  sem nibh, et suscipit felis ultricies at. Aliquam venenatis est vel nulla
+  efficitur ornare. Lorem ipsum dolor sit amet, consectetur adipiscing elit.
+\<close>
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_Easychair/document/root.bib	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,4 @@
+@manual{isabelle-system,
+  author = {Makarius Wenzel},
+  title = {The {Isabelle} System Manual},
+  note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_Easychair/document/root.tex	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,31 @@
+\documentclass[a4paper,11pt]{easychair}
+\usepackage{amssymb}
+\usepackage{hyperref}\urlstyle{rm}
+
+\usepackage{isabelle,isabellesym}\isabellestyle{it}
+
+\isadroptag{theory}
+\isafoldtag{proof}
+
+
+\begin{document}
+
+\title{Isabelle document preparation with Easychair style}
+\titlerunning{Easychair style}
+\author{Makarius Wenzel}
+\authorrunning{M. Wenzel}
+\institute{\url{https://sketis.net}}
+\maketitle
+
+\begin{abstract}
+Isabelle is a formal document preparation system. This example shows how to
+use it together with the Easychair style. See
+\url{https://easychair.org/publications/for_authors} for further information.
+\end{abstract}
+
+\input{session}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_FoilTeX/Document.thy	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,85 @@
+theory Document
+  imports Main
+begin
+
+section \<open>Abstract\<close>
+
+text \<open>
+  \small
+  Isabelle is a formal document preparation system. This example shows how to
+  use it together with Foil{\TeX} to produce slides in {\LaTeX}. See
+  \<^url>\<open>https://ctan.org/pkg/foiltex\<close> for further information.
+\<close>
+
+
+chapter \<open>Introduction\<close>
+
+section \<open>Some slide\<close>
+
+paragraph \<open>Point 1:
+  \plainstyle ABC\<close>
+
+text \<open>
+  \<^item> something
+  \<^item> to say \dots
+\<close>
+
+paragraph \<open>Point 2:
+  \plainstyle XYZ\<close>
+
+text \<open>
+  \<^item> more
+  \<^item> to say \dots
+\<close>
+
+
+section \<open>Another slide\<close>
+
+paragraph \<open>Key definitions:\<close>
+
+text \<open>Informal bla bla.\<close>
+
+definition "foo = True"  \<comment> \<open>side remark on \<^const>\<open>foo\<close>\<close>
+
+definition "bar = False"  \<comment> \<open>side remark on \<^const>\<open>bar\<close>\<close>
+
+lemma foo unfolding foo_def ..
+
+
+chapter \<open>Application: Cantor's theorem\<close>
+
+section \<open>Informal notes\<close>
+
+text_raw \<open>\isakeeptag{proof}\<close>
+text \<open>
+  Cantor's Theorem states that there is no surjection from
+  a set to its powerset.  The proof works by diagonalization.  E.g.\ see
+  \<^item> \<^url>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
+  \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
+\<close>
+
+section \<open>Formal proof\<close>
+
+theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+proof
+  assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+  then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
+  let ?D = "{x. x \<notin> f x}"
+  from * obtain a where "?D = f a" by blast
+  moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
+  ultimately show False by blast
+qed
+
+
+chapter \<open>Conclusion\<close>
+
+section \<open>Lorem ipsum dolor\<close>
+
+text \<open>
+  \<^item> Lorem ipsum dolor sit amet, consectetur adipiscing elit.
+  \<^item> Donec id ipsum sapien.
+  \<^item> Vivamus malesuada enim nibh, a tristique nisi sodales ac.
+  \<^item> Praesent ut sem consectetur, interdum tellus ac, sodales nulla.
+\<close>
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_FoilTeX/document/root.tex	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,65 @@
+\documentclass[a4paper,landscape]{foils}
+\usepackage[utf8]{inputenc}
+\usepackage{amssymb}
+\usepackage[svgnames]{xcolor}
+\usepackage{graphicx}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
+
+
+\makeatletter
+
+%colors
+\newcommand{\titlestyle}{\color{DarkGreen}}
+\newcommand{\hilitecolor}{\color{Blue}}
+\newcommand{\hilite}[1]{{\hilitecolor#1}}
+\newcommand{\red}[1]{{\color{Red}#1}}
+\newcommand{\green}[1]{{\color{DarkGreen}#1}}
+
+%headings
+\renewcommand{\isamarkupchapter}[1]{\newpage\thispagestyle{empty}\MyLogo{\let\\=\relax #1}\vspace*{0.4\textheight}\begin{center}\LARGE\bf\color{DarkGreen} #1\end{center}}
+\renewcommand{\isamarkupsection}[1]{\foilhead{\color{DarkGreen}#1}}
+\renewcommand\isamarkupparagraph{\@startsection{paragraph}{4}{0pt}{\bigskipamount}{0.5ex \@plus .1ex}{\normalsize\bf\color{DarkBlue}}}
+
+%item spacing
+\renewcommand\@listIa{\leftmargin\leftmargini
+\topsep 0\p@ \@plus 0.5\p@ \@minus 1\p@
+\parsep 2\p@ \@plus 1\p@ \@minus 1\p@
+\itemsep 2\p@ \@plus 1\p@ \@minus 0.5\p@}
+
+\makeatother
+
+
+\parindent 0pt\parskip 0.5ex
+
+\urlstyle{sf}
+\isabellestyle{it}
+\MyLogo{}
+
+\newcommand{\plainstyle}{\normalsize\sf\color{black}}
+\renewcommand{\isastyletext}{\normalsize\sf}
+\renewcommand{\isastyletxt}{\sf}
+\renewcommand{\isastylecmt}{\sf}
+
+\isadroptag{theory}
+\isafoldtag{proof}
+
+
+\begin{document}
+
+\title{\titlestyle Simple slides with with FoilTeX}
+\author{Makarius Wenzel, Augsburg \\ \url{https://sketis.net}}
+\date{}
+\maketitle
+
+\vfill
+
+\begin{center}
+  \includegraphics[width=0.15\textwidth]{isabelle_logo}
+\end{center}
+
+\vfill
+
+\input{session}
+
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_LIPIcs/Document.thy	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,64 @@
+theory Document
+  imports Main
+begin
+
+section \<open>Some section\<close>
+
+subsection \<open>Some subsection\<close>
+
+subsection \<open>Some subsubsection\<close>
+
+subsubsection \<open>Some subsubsubsection\<close>
+
+paragraph \<open>A paragraph.\<close>
+
+text \<open>Informal bla bla.\<close>
+
+definition "foo = True"  \<comment> \<open>side remark on \<^const>\<open>foo\<close>\<close>
+
+definition "bar = False"  \<comment> \<open>side remark on \<^const>\<open>bar\<close>\<close>
+
+lemma foo unfolding foo_def ..
+
+
+paragraph \<open>Another paragraph.\<close>
+
+text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+
+
+section \<open>Formal proof of Cantor's theorem\<close>
+
+text_raw \<open>\isakeeptag{proof}\<close>
+text \<open>
+  Cantor's Theorem states that there is no surjection from
+  a set to its powerset.  The proof works by diagonalization.  E.g.\ see
+  \<^item> \<^url>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
+  \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
+\<close>
+
+theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+proof
+  assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+  then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
+  let ?D = "{x. x \<notin> f x}"
+  from * obtain a where "?D = f a" by blast
+  moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
+  ultimately show False by blast
+qed
+
+
+subsection \<open>Lorem ipsum dolor\<close>
+
+text \<open>
+  Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec id ipsum
+  sapien. Vivamus malesuada enim nibh, a tristique nisi sodales ac. Praesent
+  ut sem consectetur, interdum tellus ac, sodales nulla. Quisque vel diam at
+  risus tempus tempor eget a tortor. Suspendisse potenti. Nulla erat lacus,
+  dignissim sed volutpat nec, feugiat non leo. Nunc blandit et justo sed
+  venenatis. Donec scelerisque placerat magna, et congue nulla convallis vel.
+  Cras tristique dolor consequat dolor tristique rutrum. Suspendisse ultrices
+  sem nibh, et suscipit felis ultricies at. Aliquam venenatis est vel nulla
+  efficitur ornare. Lorem ipsum dolor sit amet, consectetur adipiscing elit.
+\<close>
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_LIPIcs/document/root.bib	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,4 @@
+@manual{isabelle-system,
+  author = {Makarius Wenzel},
+  title = {The {Isabelle} System Manual},
+  note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_LIPIcs/document/root.tex	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,59 @@
+\documentclass[a4paper,UKenglish,cleveref,autoref]{lipics-v2021}
+
+\usepackage{isabelle,isabellesym}
+\isabellestyle{it}
+
+\isadroptag{theory}
+\isafoldtag{proof}
+
+
+\bibliographystyle{plainurl}% the mandatory bibstyle (e.g. from texlive-bibtex-extra)
+
+\title{Isabelle document preparation with Dagstuhl LIPIcs style}
+
+\author{Makarius Wenzel}{Augsburg, Germany \and \url{https://sketis.net}}{}{https://orcid.org/0000-0002-3753-8280}{}
+\authorrunning{M. Wenzel}
+
+\Copyright{}
+
+\ccsdesc[100]{General and reference~General literature}
+\ccsdesc[100]{General and reference}
+
+\keywords{Document preparation}
+
+\category{}
+
+\nolinenumbers
+
+%\hideLIPIcs  %uncomment to remove references to LIPIcs series (logo, DOI, ...), e.g. when preparing a pre-final version to be uploaded to arXiv or another public repository
+
+%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\EventEditors{John Q. Open and Joan R. Access}
+\EventNoEds{2}
+\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+\EventShortTitle{CVIT 2016}
+\EventAcronym{CVIT}
+\EventYear{2016}
+\EventDate{December 24--27, 2016}
+\EventLocation{Little Whinging, United Kingdom}
+\EventLogo{}
+\SeriesVolume{42}
+\ArticleNo{23}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+Isabelle is a formal document preparation system. This example shows how to
+use it together with the Dagstuhl LIPIcs style. See
+\url{https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors}
+for further information.
+\end{abstract}
+
+\input{session}
+
+\bibliography{root}
+
+\end{document}

--- a/src/Doc/ROOT	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Doc/ROOT	Wed Nov 02 18:58:38 2022 +0100
@@ -488,3 +488,38 @@
   document_files
     "root.tex"
     "style.sty"
+
+session Demo_Easychair (doc) in "Demo_Easychair" = HOL +
+  options [document_variants = "demo_easychair"]
+  theories
+    Document
+  document_files (in "$ISABELLE_EASYCHAIR_HOME")
+    "easychair.cls"
+  document_files
+    "root.bib"
+    "root.tex"
+
+session Demo_FoilTeX (doc) in "Demo_FoilTeX" = HOL +
+  options [document_variants = "demo_foiltex",
+    document_build = "pdflatex", document_logo = "FoilTeX"]
+  theories
+    Document
+  document_files (in "$ISABELLE_FOILTEX_HOME")
+    "fltfonts.def"
+    "foil20.clo"
+    "foils.cls"
+  document_files
+    "root.tex"
+
+session Demo_LIPIcs (doc) in "Demo_LIPIcs" = HOL +
+  options [document_variants = "demo_lipics",
+    document_build = "pdflatex", document_heading_prefix = "", document_comment_latex]
+  theories
+    Document
+  document_files (in "$ISABELLE_LIPICS_HOME")
+    "cc-by.pdf"
+    "lipics-logo-bw.pdf"
+    "lipics-v2021.cls"
+  document_files
+    "root.bib"
+    "root.tex"

--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Nov 02 18:58:38 2022 +0100
@@ -4064,6 +4064,25 @@
     by simp_all
 qed
 
+lemma mod_mult_unit_eq:
+  \<open>x mod (z * y) = x mod y\<close>
+  if \<open>is_unit z\<close>
+  for x y z :: \<open>'a::field poly\<close>
+proof (cases \<open>y = 0\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  moreover have \<open>z \<noteq> 0\<close>
+    using that by auto
+  moreover define a where \<open>a = lead_coeff z\<close>
+  ultimately have \<open>z = [:a:]\<close> \<open>a \<noteq> 0\<close>
+    using that monom_0 [of a] by (simp_all add: is_unit_monom_trivial)
+  then show ?thesis
+    by (simp add: mod_smult_right)
+qed
+
 lemma poly_div_minus_right [simp]: "x div (- y) = - (x div y)"
   for x y :: "'a::field poly"
   using div_smult_right [of _ "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)

--- a/src/HOL/Euclidean_Division.thy	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy	Wed Nov 02 18:58:38 2022 +0100
@@ -844,7 +844,7 @@
 end
 
 
-subsection \<open>Euclidean division on \<^typ>\<open>nat\<close>\<close>
+subsection \<open>Division on \<^typ>\<open>nat\<close>\<close>
 
 instantiation nat :: normalization_semidom
 begin
@@ -1652,7 +1652,7 @@
 
 
 
-subsection \<open>Elementary euclidean division on \<^typ>\<open>int\<close>\<close>
+subsection \<open>Division on \<^typ>\<open>int\<close>\<close>
 
 subsubsection \<open>Basic instantiation\<close>
 
@@ -1956,286 +1956,6 @@
 qed
 
 
-subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
-
-class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
-  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
-    and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
-    and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
-begin
-
-lemma division_segment_eq_iff:
-  "a = b" if "division_segment a = division_segment b"
-    and "euclidean_size a = euclidean_size b"
-  using that division_segment_euclidean_size [of a] by simp
-
-lemma euclidean_size_of_nat [simp]:
-  "euclidean_size (of_nat n) = n"
-proof -
-  have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
-    by (fact division_segment_euclidean_size)
-  then show ?thesis by simp
-qed
-
-lemma of_nat_euclidean_size:
-  "of_nat (euclidean_size a) = a div division_segment a"
-proof -
-  have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
-    by (subst nonzero_mult_div_cancel_left) simp_all
-  also have "\<dots> = a div division_segment a"
-    by simp
-  finally show ?thesis .
-qed
-
-lemma division_segment_1 [simp]:
-  "division_segment 1 = 1"
-  using division_segment_of_nat [of 1] by simp
-
-lemma division_segment_numeral [simp]:
-  "division_segment (numeral k) = 1"
-  using division_segment_of_nat [of "numeral k"] by simp
-
-lemma euclidean_size_1 [simp]:
-  "euclidean_size 1 = 1"
-  using euclidean_size_of_nat [of 1] by simp
-
-lemma euclidean_size_numeral [simp]:
-  "euclidean_size (numeral k) = numeral k"
-  using euclidean_size_of_nat [of "numeral k"] by simp
-
-lemma of_nat_dvd_iff:
-  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
-proof (cases "m = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  show ?thesis
-  proof
-    assume ?Q
-    then show ?P
-      by auto
-  next
-    assume ?P
-    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
-      by simp
-    then have "of_nat n = of_nat (n div m * m)"
-      by (simp add: of_nat_div)
-    then have "n = n div m * m"
-      by (simp only: of_nat_eq_iff)
-    then have "n = m * (n div m)"
-      by (simp add: ac_simps)
-    then show ?Q ..
-  qed
-qed
-
-lemma of_nat_mod:
-  "of_nat (m mod n) = of_nat m mod of_nat n"
-proof -
-  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
-    by (simp add: div_mult_mod_eq)
-  also have "of_nat m = of_nat (m div n * n + m mod n)"
-    by simp
-  finally show ?thesis
-    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
-qed
-
-lemma one_div_two_eq_zero [simp]:
-  "1 div 2 = 0"
-proof -
-  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
-    by (simp only:) simp
-  then show ?thesis
-    by simp
-qed
-
-lemma one_mod_two_eq_one [simp]:
-  "1 mod 2 = 1"
-proof -
-  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
-    by (simp only:) simp
-  then show ?thesis
-    by simp
-qed
-
-lemma one_mod_2_pow_eq [simp]:
-  "1 mod (2 ^ n) = of_bool (n > 0)"
-proof -
-  have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
-    using of_nat_mod [of 1 "2 ^ n"] by simp
-  also have "\<dots> = of_bool (n > 0)"
-    by simp
-  finally show ?thesis .
-qed
-
-lemma one_div_2_pow_eq [simp]:
-  "1 div (2 ^ n) = of_bool (n = 0)"
-  using div_mult_mod_eq [of 1 "2 ^ n"] by auto
-
-lemma div_mult2_eq':
-  \<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close>
-proof (cases \<open>m = 0 \<or> n = 0\<close>)
-  case True
-  then show ?thesis
-    by auto
-next
-  case False
-  then have \<open>m > 0\<close> \<open>n > 0\<close>
-    by simp_all
-  show ?thesis
-  proof (cases \<open>of_nat m * of_nat n dvd a\<close>)
-    case True
-    then obtain b where \<open>a = (of_nat m * of_nat n) * b\<close> ..
-    then have \<open>a = of_nat m * (of_nat n * b)\<close>
-      by (simp add: ac_simps)
-    then show ?thesis
-      by simp
-  next
-    case False
-    define q where \<open>q = a div (of_nat m * of_nat n)\<close>
-    define r where \<open>r = a mod (of_nat m * of_nat n)\<close>
-    from \<open>m > 0\<close> \<open>n > 0\<close> \<open>\<not> of_nat m * of_nat n dvd a\<close> r_def have "division_segment r = 1"
-      using division_segment_of_nat [of "m * n"] by (simp add: division_segment_mod)
-    with division_segment_euclidean_size [of r]
-    have "of_nat (euclidean_size r) = r"
-      by simp
-    have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
-      by simp
-    with \<open>m > 0\<close> \<open>n > 0\<close> r_def have "r div (of_nat m * of_nat n) = 0"
-      by simp
-    with \<open>of_nat (euclidean_size r) = r\<close>
-    have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
-      by simp
-    then have "of_nat (euclidean_size r div (m * n)) = 0"
-      by (simp add: of_nat_div)
-    then have "of_nat (euclidean_size r div m div n) = 0"
-      by (simp add: div_mult2_eq)
-    with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0"
-      by (simp add: of_nat_div)
-    with \<open>m > 0\<close> \<open>n > 0\<close> q_def
-    have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
-      by simp
-    moreover have \<open>a = q * (of_nat m * of_nat n) + r\<close>
-      by (simp add: q_def r_def div_mult_mod_eq)
-    ultimately show \<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close>
-      using q_def [symmetric] div_plus_div_distrib_dvd_right [of \<open>of_nat m\<close> \<open>q * (of_nat m * of_nat n)\<close> r]
-      by (simp add: ac_simps)
-  qed
-qed
-
-lemma mod_mult2_eq':
-  "a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m"
-proof -
-  have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)"
-    by (simp add: combine_common_factor div_mult_mod_eq)
-  moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)"
-    by (simp add: ac_simps)
-  ultimately show ?thesis
-    by (simp add: div_mult2_eq' mult_commute)
-qed
-
-lemma div_mult2_numeral_eq:
-  "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
-proof -
-  have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
-    by simp
-  also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))"
-    by (fact div_mult2_eq' [symmetric])
-  also have "\<dots> = ?B"
-    by simp
-  finally show ?thesis .
-qed
-
-lemma numeral_Bit0_div_2:
-  "numeral (num.Bit0 n) div 2 = numeral n"
-proof -
-  have "numeral (num.Bit0 n) = numeral n + numeral n"
-    by (simp only: numeral.simps)
-  also have "\<dots> = numeral n * 2"
-    by (simp add: mult_2_right)
-  finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2"
-    by simp
-  also have "\<dots> = numeral n"
-    by (rule nonzero_mult_div_cancel_right) simp
-  finally show ?thesis .
-qed
-
-lemma numeral_Bit1_div_2:
-  "numeral (num.Bit1 n) div 2 = numeral n"
-proof -
-  have "numeral (num.Bit1 n) = numeral n + numeral n + 1"
-    by (simp only: numeral.simps)
-  also have "\<dots> = numeral n * 2 + 1"
-    by (simp add: mult_2_right)
-  finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2"
-    by simp
-  also have "\<dots> = numeral n * 2 div 2 + 1 div 2"
-    using dvd_triv_right by (rule div_plus_div_distrib_dvd_left)
-  also have "\<dots> = numeral n * 2 div 2"
-    by simp
-  also have "\<dots> = numeral n"
-    by (rule nonzero_mult_div_cancel_right) simp
-  finally show ?thesis .
-qed
-
-lemma exp_mod_exp:
-  \<open>2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close>
-proof -
-  have \<open>(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> (is \<open>?lhs = ?rhs\<close>)
-    by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex)
-  then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
-    by simp
-  then show ?thesis
-    by (simp add: of_nat_mod)
-qed
-
-lemma mask_mod_exp:
-  \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close>
-proof -
-  have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>)
-  proof (cases \<open>n \<le> m\<close>)
-    case True
-    then show ?thesis
-      by (simp add: Suc_le_lessD)
-  next
-    case False
-    then have \<open>m < n\<close>
-      by simp
-    then obtain q where n: \<open>n = Suc q + m\<close>
-      by (auto dest: less_imp_Suc_add)
-    then have \<open>min m n = m\<close>
-      by simp
-    moreover have \<open>(2::nat) ^ m \<le> 2 * 2 ^ q * 2 ^ m\<close>
-      using mult_le_mono1 [of 1 \<open>2 * 2 ^ q\<close> \<open>2 ^ m\<close>] by simp
-    with n have \<open>2 ^ n - 1 = (2 ^ Suc q - 1) * 2 ^ m + (2 ^ m - (1::nat))\<close>
-      by (simp add: monoid_mult_class.power_add algebra_simps)
-    ultimately show ?thesis
-      by (simp only: euclidean_semiring_cancel_class.mod_mult_self3) simp
-  qed
-  then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
-    by simp
-  then show ?thesis
-    by (simp add: of_nat_mod of_nat_diff)
-qed
-
-lemma of_bool_half_eq_0 [simp]:
-  \<open>of_bool b div 2 = 0\<close>
-  by simp
-
-end
-
-class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
-
-instance nat :: unique_euclidean_semiring_with_nat
-  by standard (simp_all add: dvd_eq_mod_eq_0)
-
-instance int :: unique_euclidean_ring_with_nat
-  by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np)
-
-
-subsection \<open>More on euclidean division on \<^typ>\<open>int\<close>\<close>
-
 subsubsection \<open>Trivial reduction steps\<close>
 
 lemma div_pos_pos_trivial [simp]:
@@ -2478,16 +2198,54 @@
 
 subsubsection \<open>Algebraic rewrites\<close>
 
-lemma zdiv_zmult2_eq:
-  \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
-proof (cases \<open>b \<ge> 0\<close>)
-  case True
-  with that show ?thesis
-    using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
-next
-  case False
-  with that show ?thesis
-    using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+lemma zdiv_zmult2_eq: \<open>a div (b * c) = (a div b) div c\<close>  (is ?Q)
+  and zmod_zmult2_eq: \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close>  (is ?P)
+  if \<open>c \<ge> 0\<close> for a b c :: int
+proof -
+  have *: \<open>(a div (b * c), a mod (b * c)) = ((a div b) div c, b * (a div b mod c) + a mod b)\<close>
+    if \<open>b > 0\<close> for a b
+  proof (induction rule: euclidean_relationI)
+    case by0
+    then show ?case by auto
+  next
+    case divides
+    then obtain d where \<open>a = b * c * d\<close>
+      by blast
+    with divides that show ?case
+      by (simp add: ac_simps)
+  next
+    case euclidean_relation
+    with \<open>b > 0\<close> \<open>c \<ge> 0\<close> have \<open>0 < c\<close> \<open>b > 0\<close>
+      by simp_all
+    then have \<open>a mod b < b\<close>
+      by simp
+    moreover have \<open>1 \<le> c - a div b mod c\<close>
+      using \<open>c > 0\<close> by (simp add: int_one_le_iff_zero_less)
+    ultimately have \<open>a mod b * 1 < b * (c - a div b mod c)\<close>
+      by (rule mult_less_le_imp_less) (use \<open>b > 0\<close> in simp_all)
+    with \<open>0 < b\<close> \<open>0 < c\<close> show ?case
+      by (simp add: division_segment_int_def algebra_simps flip: minus_mod_eq_mult_div)
+  qed
+  show ?Q
+  proof (cases \<open>b \<ge> 0\<close>)
+    case True
+    with * [of b a] show ?thesis
+      by (cases \<open>b = 0\<close>) simp_all
+  next
+    case False
+    with * [of \<open>- b\<close> \<open>- a\<close>] show ?thesis
+      by simp
+  qed
+  show ?P
+  proof (cases \<open>b \<ge> 0\<close>)
+    case True
+    with * [of b a] show ?thesis
+      by (cases \<open>b = 0\<close>) simp_all
+  next
+    case False
+    with * [of \<open>- b\<close> \<open>- a\<close>] show ?thesis
+      by simp
+  qed
 qed
 
 lemma zdiv_zmult2_eq':
@@ -2502,18 +2260,6 @@
   finally show ?thesis .
 qed
 
-lemma zmod_zmult2_eq:
-  \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
-proof (cases \<open>b \<ge> 0\<close>)
-  case True
-  with that show ?thesis
-    using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
-next
-  case False
-  with that show ?thesis
-    using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
-qed
-
 lemma half_nonnegative_int_iff [simp]:
   \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
   by auto
@@ -2526,12 +2272,12 @@
 subsubsection \<open>Distributive laws for conversions.\<close>
 
 lemma zdiv_int:
-  "int (a div b) = int a div int b"
-  by (fact of_nat_div)
+  \<open>int (m div n) = int m div int n\<close>
+  by (cases \<open>m = 0\<close>) (auto simp add: divide_int_def)
 
 lemma zmod_int:
-  "int (a mod b) = int a mod int b"
-  by (fact of_nat_mod)
+  \<open>int (m mod n) = int m mod int n\<close>
+  by (cases \<open>m = 0\<close>) (auto simp add: modulo_int_def)
 
 lemma nat_div_distrib:
   \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> x\<close>
@@ -2961,384 +2707,7 @@
   by (rule pos_zmod_mult_2) simp
 
 
-subsection \<open>Generic symbolic computations\<close>
-
-text \<open>
-  The following type class contains everything necessary to formulate
-  a division algorithm in ring structures with numerals, restricted
-  to its positive segments.
-\<close>
-
-class unique_euclidean_semiring_with_nat_division = unique_euclidean_semiring_with_nat +
-  fixes divmod :: \<open>num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a\<close>
-    and divmod_step :: \<open>'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a\<close> \<comment> \<open>
-      These are conceptually definitions but force generated code
-      to be monomorphic wrt. particular instances of this class which
-      yields a significant speedup.\<close>
-  assumes divmod_def: \<open>divmod m n = (numeral m div numeral n, numeral m mod numeral n)\<close>
-    and divmod_step_def [simp]: \<open>divmod_step l (q, r) =
-      (if euclidean_size l \<le> euclidean_size r then (2 * q + 1, r - l)
-       else (2 * q, r))\<close> \<comment> \<open>
-         This is a formulation of one step (referring to one digit position)
-         in school-method division: compare the dividend at the current
-         digit position with the remainder from previous division steps
-         and evaluate accordingly.\<close>
-begin
-
-lemma fst_divmod:
-  \<open>fst (divmod m n) = numeral m div numeral n\<close>
-  by (simp add: divmod_def)
-
-lemma snd_divmod:
-  \<open>snd (divmod m n) = numeral m mod numeral n\<close>
-  by (simp add: divmod_def)
-
-text \<open>
-  Following a formulation of school-method division.
-  If the divisor is smaller than the dividend, terminate.
-  If not, shift the dividend to the right until termination
-  occurs and then reiterate single division steps in the
-  opposite direction.
-\<close>
-
-lemma divmod_divmod_step:
-  \<open>divmod m n = (if m < n then (0, numeral m)
-    else divmod_step (numeral n) (divmod m (Num.Bit0 n)))\<close>
-proof (cases \<open>m < n\<close>)
-  case True
-  then show ?thesis
-    by (simp add: prod_eq_iff fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod)
-next
-  case False
-  define r s t where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close> \<open>t = 2 * s\<close>
-  then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close> \<open>numeral (num.Bit0 n) = of_nat t\<close>
-    and \<open>\<not> s \<le> r mod s\<close>
-    by (simp_all add: not_le)
-  have t: \<open>2 * (r div t) = r div s - r div s mod 2\<close>
-    \<open>r mod t = s * (r div s mod 2) + r mod s\<close>
-    by (simp add: Rings.minus_mod_eq_mult_div Groups.mult.commute [of 2] Euclidean_Division.div_mult2_eq \<open>t = 2 * s\<close>)
-      (use mod_mult2_eq [of r s 2] in \<open>simp add: ac_simps \<open>t = 2 * s\<close>\<close>)
-  have rs: \<open>r div s mod 2 = 0 \<or> r div s mod 2 = Suc 0\<close>
-    by auto
-  from \<open>\<not> s \<le> r mod s\<close> have \<open>s \<le> r mod t \<Longrightarrow>
-     r div s = Suc (2 * (r div t)) \<and>
-     r mod s = r mod t - s\<close>
-    using rs
-    by (auto simp add: t)
-  moreover have \<open>r mod t < s \<Longrightarrow>
-     r div s = 2 * (r div t) \<and>
-     r mod s = r mod t\<close>
-    using rs
-    by (auto simp add: t)
-  ultimately show ?thesis
-    by (simp add: divmod_def prod_eq_iff split_def Let_def
-        not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *)
-    (simp add: flip: of_nat_numeral of_nat_mult add.commute [of 1] of_nat_div of_nat_mod of_nat_Suc of_nat_diff)
-qed
-
-text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
-
-lemma divmod_trivial [simp]:
-  "divmod m Num.One = (numeral m, 0)"
-  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
-  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
-  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
-
-text \<open>Division by an even number is a right-shift\<close>
-
-lemma divmod_cancel [simp]:
-  \<open>divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))\<close> (is ?P)
-  \<open>divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))\<close> (is ?Q)
-proof -
-  define r s where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close>
-  then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close>
-    \<open>numeral (num.Bit0 m) = of_nat (2 * r)\<close> \<open>numeral (num.Bit0 n) = of_nat (2 * s)\<close>
-    \<open>numeral (num.Bit1 m) = of_nat (Suc (2 * r))\<close>
-    by simp_all
-  have **: \<open>Suc (2 * r) div 2 = r\<close>
-    by simp
-  show ?P and ?Q
-    by (simp_all add: divmod_def *)
-      (simp_all flip: of_nat_numeral of_nat_div of_nat_mod of_nat_mult add.commute [of 1] of_nat_Suc
-       add: Euclidean_Division.mod_mult_mult1 div_mult2_eq [of _ 2] mod_mult2_eq [of _ 2] **)
-qed
-
-text \<open>The really hard work\<close>
-
-lemma divmod_steps [simp]:
-  "divmod (num.Bit0 m) (num.Bit1 n) =
-      (if m \<le> n then (0, numeral (num.Bit0 m))
-       else divmod_step (numeral (num.Bit1 n))
-             (divmod (num.Bit0 m)
-               (num.Bit0 (num.Bit1 n))))"
-  "divmod (num.Bit1 m) (num.Bit1 n) =
-      (if m < n then (0, numeral (num.Bit1 m))
-       else divmod_step (numeral (num.Bit1 n))
-             (divmod (num.Bit1 m)
-               (num.Bit0 (num.Bit1 n))))"
-  by (simp_all add: divmod_divmod_step)
-
-lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps
-
-text \<open>Special case: divisibility\<close>
-
-definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
-where
-  "divides_aux qr \<longleftrightarrow> snd qr = 0"
-
-lemma divides_aux_eq [simp]:
-  "divides_aux (q, r) \<longleftrightarrow> r = 0"
-  by (simp add: divides_aux_def)
-
-lemma dvd_numeral_simp [simp]:
-  "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
-  by (simp add: divmod_def mod_eq_0_iff_dvd)
-
-text \<open>Generic computation of quotient and remainder\<close>
-
-lemma numeral_div_numeral [simp]:
-  "numeral k div numeral l = fst (divmod k l)"
-  by (simp add: fst_divmod)
-
-lemma numeral_mod_numeral [simp]:
-  "numeral k mod numeral l = snd (divmod k l)"
-  by (simp add: snd_divmod)
-
-lemma one_div_numeral [simp]:
-  "1 div numeral n = fst (divmod num.One n)"
-  by (simp add: fst_divmod)
-
-lemma one_mod_numeral [simp]:
-  "1 mod numeral n = snd (divmod num.One n)"
-  by (simp add: snd_divmod)
-
-end
-
-instantiation nat :: unique_euclidean_semiring_with_nat_division
-begin
-
-definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
-where
-  divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_nat :: "nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
-  "divmod_step_nat l qr = (let (q, r) = qr
-    in if r \<ge> l then (2 * q + 1, r - l)
-    else (2 * q, r))"
-
-instance
-  by standard (simp_all add: divmod'_nat_def divmod_step_nat_def)
-
-end
-
-declare divmod_algorithm_code [where ?'a = nat, code]
-
-lemma Suc_0_div_numeral [simp]:
-  \<open>Suc 0 div numeral Num.One = 1\<close>
-  \<open>Suc 0 div numeral (Num.Bit0 n) = 0\<close>
-  \<open>Suc 0 div numeral (Num.Bit1 n) = 0\<close>
-  by simp_all
-
-lemma Suc_0_mod_numeral [simp]:
-  \<open>Suc 0 mod numeral Num.One = 0\<close>
-  \<open>Suc 0 mod numeral (Num.Bit0 n) = 1\<close>
-  \<open>Suc 0 mod numeral (Num.Bit1 n) = 1\<close>
-  by simp_all
-
-instantiation int :: unique_euclidean_semiring_with_nat_division
-begin
-
-definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
-where
-  "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_int :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
-where
-  "divmod_step_int l qr = (let (q, r) = qr
-    in if \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
-    else (2 * q, r))"
-
-instance
-  by standard (auto simp add: divmod_int_def divmod_step_int_def)
-
-end
-
-declare divmod_algorithm_code [where ?'a = int, code]
-
-context
-begin
-
-qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
-where
-  "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
-
-qualified lemma adjust_div_eq [simp, code]:
-  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
-  by (simp add: adjust_div_def)
-
-qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int"
-where
-  [simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"
-
-lemma minus_numeral_div_numeral [simp]:
-  "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
-  have "int (fst (divmod m n)) = fst (divmod m n)"
-    by (simp only: fst_divmod divide_int_def) auto
-  then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-
-lemma minus_numeral_mod_numeral [simp]:
-  "- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
-  case True
-  then show ?thesis
-    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
-  case False
-  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    by (simp only: snd_divmod modulo_int_def) auto
-  then show ?thesis
-    by (simp add: divides_aux_def adjust_div_def)
-      (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma numeral_div_minus_numeral [simp]:
-  "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
-  have "int (fst (divmod m n)) = fst (divmod m n)"
-    by (simp only: fst_divmod divide_int_def) auto
-  then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-
-lemma numeral_mod_minus_numeral [simp]:
-  "numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
-  case True
-  then show ?thesis
-    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
-  case False
-  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    by (simp only: snd_divmod modulo_int_def) auto
-  then show ?thesis
-    by (simp add: divides_aux_def adjust_div_def)
-      (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma minus_one_div_numeral [simp]:
-  "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
-  using minus_numeral_div_numeral [of Num.One n] by simp
-
-lemma minus_one_mod_numeral [simp]:
-  "- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
-  using minus_numeral_mod_numeral [of Num.One n] by simp
-
-lemma one_div_minus_numeral [simp]:
-  "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
-  using numeral_div_minus_numeral [of Num.One n] by simp
-
-lemma one_mod_minus_numeral [simp]:
-  "1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
-  using numeral_mod_minus_numeral [of Num.One n] by simp
-
-lemma [code]:
-  fixes k :: int
-  shows
-    "k div 0 = 0"
-    "k mod 0 = k"
-    "0 div k = 0"
-    "0 mod k = 0"
-    "k div Int.Pos Num.One = k"
-    "k mod Int.Pos Num.One = 0"
-    "k div Int.Neg Num.One = - k"
-    "k mod Int.Neg Num.One = 0"
-    "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
-    "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
-    "Int.Neg m div Int.Pos n = - (adjust_div (divmod m n) :: int)"
-    "Int.Neg m mod Int.Pos n = adjust_mod n (snd (divmod m n) :: int)"
-    "Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)"
-    "Int.Pos m mod Int.Neg n = - adjust_mod n (snd (divmod m n) :: int)"
-    "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
-    "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
-  by simp_all
-
-end
-
-lemma divmod_BitM_2_eq [simp]:
-  \<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close>
-  by (cases m) simp_all
-
-
-subsubsection \<open>Computation by simplification\<close>
-
-lemma euclidean_size_nat_less_eq_iff:
-  \<open>euclidean_size m \<le> euclidean_size n \<longleftrightarrow> m \<le> n\<close> for m n :: nat
-  by simp
-
-lemma euclidean_size_int_less_eq_iff:
-  \<open>euclidean_size k \<le> euclidean_size l \<longleftrightarrow> \<bar>k\<bar> \<le> \<bar>l\<bar>\<close> for k l :: int
-  by auto
-
-simproc_setup numeral_divmod
-  ("0 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "0 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "0 div - 1 :: int" | "0 mod - 1 :: int" |
-   "0 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
-   "1 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "1 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "1 div - 1 :: int" | "1 mod - 1 :: int" |
-   "1 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
-   "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
-   "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
-   "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
-   "numeral a div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "numeral a div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
-   "numeral a div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
-   "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
-   "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
-   "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
-   "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
-   "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
-   "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") = \<open>
-  let
-    val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>);
-    fun successful_rewrite ctxt ct =
-      let
-        val thm = Simplifier.rewrite ctxt ct
-      in if Thm.is_reflexive thm then NONE else SOME thm end;
-  in fn phi =>
-    let
-      val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
-        one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
-        one_div_minus_numeral one_mod_minus_numeral
-        numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
-        numeral_div_minus_numeral numeral_mod_minus_numeral
-        div_minus_minus mod_minus_minus Euclidean_Division.adjust_div_eq of_bool_eq one_neq_zero
-        numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
-        divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One
-        case_prod_beta rel_simps Euclidean_Division.adjust_mod_def div_minus1_right mod_minus1_right
-        minus_minus numeral_times_numeral mult_zero_right mult_1_right
-        euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
-        @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
-      fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
-        (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
-    in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
-  end
-\<close> \<comment> \<open>
-  There is space for improvement here: the calculation itself
-  could be carried out outside the logic, and a generic simproc
-  (simplifier setup) for generic calculation would be helpful.
-\<close>
-
-
-subsubsection \<open>Code generation\<close>
+subsection \<open>Code generation\<close>
 
 context
 begin

--- a/src/HOL/Matrix_LP/ComputeNumeral.thy	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/HOL/Matrix_LP/ComputeNumeral.thy	Wed Nov 02 18:58:38 2022 +0100
@@ -51,10 +51,10 @@
   one_div_minus_numeral one_mod_minus_numeral
   numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
   numeral_div_minus_numeral numeral_mod_minus_numeral
-  div_minus_minus mod_minus_minus Euclidean_Division.adjust_div_eq of_bool_eq one_neq_zero
+  div_minus_minus mod_minus_minus Parity.adjust_div_eq of_bool_eq one_neq_zero
   numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
   divmod_steps divmod_cancel divmod_step_def fst_conv snd_conv numeral_One
-  case_prod_beta rel_simps Euclidean_Division.adjust_mod_def div_minus1_right mod_minus1_right
+  case_prod_beta rel_simps Parity.adjust_mod_def div_minus1_right mod_minus1_right
   minus_minus numeral_times_numeral mult_zero_right mult_1_right

--- a/src/HOL/Parity.thy	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/HOL/Parity.thy	Wed Nov 02 18:58:38 2022 +0100
@@ -23,6 +23,24 @@
 abbreviation odd :: "'a \<Rightarrow> bool"
   where "odd a \<equiv> \<not> 2 dvd a"
 
+end
+
+class ring_parity = ring + semiring_parity
+begin
+
+subclass comm_ring_1 ..
+
+end
+
+instance nat :: semiring_parity
+  by standard (simp_all add: dvd_eq_mod_eq_0)
+
+instance int :: ring_parity
+  by standard (auto simp add: dvd_eq_mod_eq_0)
+
+context semiring_parity
+begin
+
 lemma parity_cases [case_names even odd]:
   assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
   assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
@@ -159,6 +177,10 @@
 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   by (induct n) auto
 
+lemma even_prod_iff:
+  \<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close>
+  using that by (induction A) simp_all
+
 lemma mask_eq_sum_exp:
   \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
 proof -
@@ -172,13 +194,15 @@
     by simp
 qed
 
+lemma (in -) mask_eq_sum_exp_nat:
+  \<open>2 ^ n - Suc 0 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
+  using mask_eq_sum_exp [where ?'a = nat] by simp
+
 end
 
-class ring_parity = ring + semiring_parity
+context ring_parity
 begin
 
-subclass comm_ring_1 ..
-
 lemma even_minus:
   "even (- a) \<longleftrightarrow> even a"
   by (fact dvd_minus_iff)
@@ -190,135 +214,8 @@
 end
 
 
-subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
-
-context unique_euclidean_semiring_with_nat
-begin
-
-subclass semiring_parity
-proof
-  show "2 dvd a \<longleftrightarrow> a mod 2 = 0" for a
-    by (fact dvd_eq_mod_eq_0)
-  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" for a
-  proof
-    assume "a mod 2 = 1"
-    then show "\<not> 2 dvd a"
-      by auto
-  next
-    assume "\<not> 2 dvd a"
-    have eucl: "euclidean_size (a mod 2) = 1"
-    proof (rule order_antisym)
-      show "euclidean_size (a mod 2) \<le> 1"
-        using mod_size_less [of 2 a] by simp
-      show "1 \<le> euclidean_size (a mod 2)"
-        using \<open>\<not> 2 dvd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
-    qed 
-    from \<open>\<not> 2 dvd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
-      by simp
-    then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
-      by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
-    then have "\<not> 2 dvd euclidean_size a"
-      using of_nat_dvd_iff [of 2] by simp
-    then have "euclidean_size a mod 2 = 1"
-      by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
-    then have "of_nat (euclidean_size a mod 2) = of_nat 1"
-      by simp
-    then have "of_nat (euclidean_size a) mod 2 = 1"
-      by (simp add: of_nat_mod)
-    from \<open>\<not> 2 dvd a\<close> eucl
-    show "a mod 2 = 1"
-      by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
-  qed
-  show "\<not> is_unit 2"
-  proof (rule notI)
-    assume "is_unit 2"
-    then have "of_nat 2 dvd of_nat 1"
-      by simp
-    then have "is_unit (2::nat)"
-      by (simp only: of_nat_dvd_iff)
-    then show False
-      by simp
-  qed
-qed
-
-lemma even_succ_div_two [simp]:
-  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
-  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
-
-lemma odd_succ_div_two [simp]:
-  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
-  by (auto elim!: oddE simp add: add.assoc)
-
-lemma even_two_times_div_two:
-  "even a \<Longrightarrow> 2 * (a div 2) = a"
-  by (fact dvd_mult_div_cancel)
-
-lemma odd_two_times_div_two_succ [simp]:
-  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
-  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
-
-context unique_euclidean_ring_with_nat
-begin
-
-subclass ring_parity ..
-
-lemma minus_1_mod_2_eq [simp]:
-  "- 1 mod 2 = 1"
-  by (simp add: mod_2_eq_odd)
-
-lemma minus_1_div_2_eq [simp]:
-  "- 1 div 2 = - 1"
-proof -
-  from div_mult_mod_eq [of "- 1" 2]
-  have "- 1 div 2 * 2 = - 1 * 2"
-    using add_implies_diff by fastforce
-  then show ?thesis
-    using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
-qed
-
-end
-
-
 subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close>
 
-instance nat :: unique_euclidean_semiring_with_nat
-  by standard (simp_all add: dvd_eq_mod_eq_0)
-
 lemma even_Suc_Suc_iff [simp]:
   "even (Suc (Suc n)) \<longleftrightarrow> even n"
   using dvd_add_triv_right_iff [of 2 n] by simp
@@ -361,18 +258,18 @@
 
 lemma even_Suc_div_two [simp]:
   "even n \<Longrightarrow> Suc n div 2 = n div 2"
-  using even_succ_div_two [of n] by simp
+  by auto
 
 lemma odd_Suc_div_two [simp]:
   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
-  using odd_succ_div_two [of n] by simp
+  by (auto elim: oddE)
 
 lemma odd_two_times_div_two_nat [simp]:
   assumes "odd n"
   shows "2 * (n div 2) = n - (1 :: nat)"
 proof -
   from assms have "2 * (n div 2) + 1 = n"
-    by (rule odd_two_times_div_two_succ)
+    by (auto elim: oddE)
   then have "Suc (2 * (n div 2)) - 1 = n - 1"
     by simp
   then show ?thesis
@@ -410,17 +307,9 @@
   qed
 qed
 
-lemma mask_eq_sum_exp_nat:
-  \<open>2 ^ n - Suc 0 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
-  using mask_eq_sum_exp [where ?'a = nat] by simp
-
 context semiring_parity
 begin
 
-lemma even_of_nat_iff [simp]:
-  "even (of_nat n) \<longleftrightarrow> even n"
-  by (induction n) simp_all
-
 lemma even_sum_iff:
   \<open>even (sum f A) \<longleftrightarrow> even (card {a\<in>A. odd (f a)})\<close> if \<open>finite A\<close>
 using that proof (induction A)
@@ -435,10 +324,6 @@
     by simp
 qed
 
-lemma even_prod_iff:
-  \<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close>
-  using that by (induction A) simp_all
-
 lemma even_mask_iff [simp]:
   \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
 proof (cases \<open>n = 0\<close>)
@@ -453,6 +338,10 @@
     by (auto simp add: mask_eq_sum_exp even_sum_iff)
 qed
 
+lemma even_of_nat_iff [simp]:
+  "even (of_nat n) \<longleftrightarrow> even n"
+  by (induction n) simp_all
+
 end
 
 
@@ -580,46 +469,9 @@
 
 end
 
-context unique_euclidean_semiring_with_nat
-begin
-
-lemma even_mask_div_iff':
-  \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
-proof -
-  have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close>
-    by (simp only: of_nat_div) (simp add: of_nat_diff)
-  also have \<open>\<dots> \<longleftrightarrow> even ((2 ^ m - Suc 0) div 2 ^ n)\<close>
-    by simp
-  also have \<open>\<dots> \<longleftrightarrow> m \<le> n\<close>
-  proof (cases \<open>m \<le> n\<close>)
-    case True
-    then show ?thesis
-      by (simp add: Suc_le_lessD)
-  next
-    case False
-    then obtain r where r: \<open>m = n + Suc r\<close>
-      using less_imp_Suc_add by fastforce
-    from r have \<open>{q. q < m} \<inter> {q. 2 ^ n dvd (2::nat) ^ q} = {q. n \<le> q \<and> q < m}\<close>
-      by (auto simp add: dvd_power_iff_le)
-    moreover from r have \<open>{q. q < m} \<inter> {q. \<not> 2 ^ n dvd (2::nat) ^ q} = {q. q < n}\<close>
-      by (auto simp add: dvd_power_iff_le)
-    moreover from False have \<open>{q. n \<le> q \<and> q < m \<and> q \<le> n} = {n}\<close>
-      by auto
-    then have \<open>odd ((\<Sum>a\<in>{q. n \<le> q \<and> q < m}. 2 ^ a div (2::nat) ^ n) + sum ((^) 2) {q. q < n} div 2 ^ n)\<close>
-      by (simp_all add: euclidean_semiring_cancel_class.power_diff_power_eq semiring_parity_class.even_sum_iff not_less mask_eq_sum_exp_nat [symmetric])
-    ultimately have \<open>odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)\<close>
-      by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all
-    with False show ?thesis
-      by (simp add: mask_eq_sum_exp_nat)
-  qed
-  finally show ?thesis .
-qed
-
-end
-
 
 subsection \<open>Instance for \<^typ>\<open>int\<close>\<close>
-
+  
 lemma even_diff_iff:
   "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
   by (fact even_diff)
@@ -670,6 +522,820 @@
 end
 
 
+subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
+
+class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
+  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
+    and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
+    and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
+begin
+
+lemma division_segment_eq_iff:
+  "a = b" if "division_segment a = division_segment b"
+    and "euclidean_size a = euclidean_size b"
+  using that division_segment_euclidean_size [of a] by simp
+
+lemma euclidean_size_of_nat [simp]:
+  "euclidean_size (of_nat n) = n"
+proof -
+  have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
+    by (fact division_segment_euclidean_size)
+  then show ?thesis by simp
+qed
+
+lemma of_nat_euclidean_size:
+  "of_nat (euclidean_size a) = a div division_segment a"
+proof -
+  have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
+    by (subst nonzero_mult_div_cancel_left) simp_all
+  also have "\<dots> = a div division_segment a"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma division_segment_1 [simp]:
+  "division_segment 1 = 1"
+  using division_segment_of_nat [of 1] by simp
+
+lemma division_segment_numeral [simp]:
+  "division_segment (numeral k) = 1"
+  using division_segment_of_nat [of "numeral k"] by simp
+
+lemma euclidean_size_1 [simp]:
+  "euclidean_size 1 = 1"
+  using euclidean_size_of_nat [of 1] by simp
+
+lemma euclidean_size_numeral [simp]:
+  "euclidean_size (numeral k) = numeral k"
+  using euclidean_size_of_nat [of "numeral k"] by simp
+
+lemma of_nat_dvd_iff:
+  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
+proof (cases "m = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    assume ?Q
+    then show ?P
+      by auto
+  next
+    assume ?P
+    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
+      by simp
+    then have "of_nat n = of_nat (n div m * m)"
+      by (simp add: of_nat_div)
+    then have "n = n div m * m"
+      by (simp only: of_nat_eq_iff)
+    then have "n = m * (n div m)"
+      by (simp add: ac_simps)
+    then show ?Q ..
+  qed
+qed
+
+lemma of_nat_mod:
+  "of_nat (m mod n) = of_nat m mod of_nat n"
+proof -
+  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
+    by (simp add: div_mult_mod_eq)
+  also have "of_nat m = of_nat (m div n * n + m mod n)"
+    by simp
+  finally show ?thesis
+    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
+qed
+
+lemma one_div_two_eq_zero [simp]:
+  "1 div 2 = 0"
+proof -
+  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
+    by (simp only:) simp
+  then show ?thesis
+    by simp
+qed
+
+lemma one_mod_two_eq_one [simp]:
+  "1 mod 2 = 1"
+proof -
+  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
+    by (simp only:) simp
+  then show ?thesis
+    by simp
+qed
+
+lemma one_mod_2_pow_eq [simp]:
+  "1 mod (2 ^ n) = of_bool (n > 0)"
+proof -
+  have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
+    using of_nat_mod [of 1 "2 ^ n"] by simp
+  also have "\<dots> = of_bool (n > 0)"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma one_div_2_pow_eq [simp]:
+  "1 div (2 ^ n) = of_bool (n = 0)"
+  using div_mult_mod_eq [of 1 "2 ^ n"] by auto
+
+lemma div_mult2_eq':
+  \<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close>
+proof (cases \<open>m = 0 \<or> n = 0\<close>)
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  then have \<open>m > 0\<close> \<open>n > 0\<close>
+    by simp_all
+  show ?thesis
+  proof (cases \<open>of_nat m * of_nat n dvd a\<close>)
+    case True
+    then obtain b where \<open>a = (of_nat m * of_nat n) * b\<close> ..
+    then have \<open>a = of_nat m * (of_nat n * b)\<close>
+      by (simp add: ac_simps)
+    then show ?thesis
+      by simp
+  next
+    case False
+    define q where \<open>q = a div (of_nat m * of_nat n)\<close>
+    define r where \<open>r = a mod (of_nat m * of_nat n)\<close>
+    from \<open>m > 0\<close> \<open>n > 0\<close> \<open>\<not> of_nat m * of_nat n dvd a\<close> r_def have "division_segment r = 1"
+      using division_segment_of_nat [of "m * n"] by (simp add: division_segment_mod)
+    with division_segment_euclidean_size [of r]
+    have "of_nat (euclidean_size r) = r"
+      by simp
+    have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
+      by simp
+    with \<open>m > 0\<close> \<open>n > 0\<close> r_def have "r div (of_nat m * of_nat n) = 0"
+      by simp
+    with \<open>of_nat (euclidean_size r) = r\<close>
+    have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
+      by simp
+    then have "of_nat (euclidean_size r div (m * n)) = 0"
+      by (simp add: of_nat_div)
+    then have "of_nat (euclidean_size r div m div n) = 0"
+      by (simp add: div_mult2_eq)
+    with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0"
+      by (simp add: of_nat_div)
+    with \<open>m > 0\<close> \<open>n > 0\<close> q_def
+    have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
+      by simp
+    moreover have \<open>a = q * (of_nat m * of_nat n) + r\<close>
+      by (simp add: q_def r_def div_mult_mod_eq)
+    ultimately show \<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close>
+      using q_def [symmetric] div_plus_div_distrib_dvd_right [of \<open>of_nat m\<close> \<open>q * (of_nat m * of_nat n)\<close> r]
+      by (simp add: ac_simps)
+  qed
+qed
+
+lemma mod_mult2_eq':
+  "a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m"
+proof -
+  have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)"
+    by (simp add: combine_common_factor div_mult_mod_eq)
+  moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)"
+    by (simp add: ac_simps)
+  ultimately show ?thesis
+    by (simp add: div_mult2_eq' mult_commute)
+qed
+
+lemma div_mult2_numeral_eq:
+  "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
+proof -
+  have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
+    by simp
+  also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))"
+    by (fact div_mult2_eq' [symmetric])
+  also have "\<dots> = ?B"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma numeral_Bit0_div_2:
+  "numeral (num.Bit0 n) div 2 = numeral n"
+proof -
+  have "numeral (num.Bit0 n) = numeral n + numeral n"
+    by (simp only: numeral.simps)
+  also have "\<dots> = numeral n * 2"
+    by (simp add: mult_2_right)
+  finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2"
+    by simp
+  also have "\<dots> = numeral n"
+    by (rule nonzero_mult_div_cancel_right) simp
+  finally show ?thesis .
+qed
+
+lemma numeral_Bit1_div_2:
+  "numeral (num.Bit1 n) div 2 = numeral n"
+proof -
+  have "numeral (num.Bit1 n) = numeral n + numeral n + 1"
+    by (simp only: numeral.simps)
+  also have "\<dots> = numeral n * 2 + 1"
+    by (simp add: mult_2_right)
+  finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2"
+    by simp
+  also have "\<dots> = numeral n * 2 div 2 + 1 div 2"
+    using dvd_triv_right by (rule div_plus_div_distrib_dvd_left)
+  also have "\<dots> = numeral n * 2 div 2"
+    by simp
+  also have "\<dots> = numeral n"
+    by (rule nonzero_mult_div_cancel_right) simp
+  finally show ?thesis .
+qed
+
+lemma exp_mod_exp:
+  \<open>2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close>
+proof -
+  have \<open>(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> (is \<open>?lhs = ?rhs\<close>)
+    by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex)
+  then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_mod)
+qed
+
+lemma mask_mod_exp:
+  \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close>
+proof -
+  have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>)
+  proof (cases \<open>n \<le> m\<close>)
+    case True
+    then show ?thesis
+      by (simp add: Suc_le_lessD)
+  next
+    case False
+    then have \<open>m < n\<close>
+      by simp
+    then obtain q where n: \<open>n = Suc q + m\<close>
+      by (auto dest: less_imp_Suc_add)
+    then have \<open>min m n = m\<close>
+      by simp
+    moreover have \<open>(2::nat) ^ m \<le> 2 * 2 ^ q * 2 ^ m\<close>
+      using mult_le_mono1 [of 1 \<open>2 * 2 ^ q\<close> \<open>2 ^ m\<close>] by simp
+    with n have \<open>2 ^ n - 1 = (2 ^ Suc q - 1) * 2 ^ m + (2 ^ m - (1::nat))\<close>
+      by (simp add: monoid_mult_class.power_add algebra_simps)
+    ultimately show ?thesis
+      by (simp only: euclidean_semiring_cancel_class.mod_mult_self3) simp
+  qed
+  then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_mod of_nat_diff)
+qed
+
+lemma of_bool_half_eq_0 [simp]:
+  \<open>of_bool b div 2 = 0\<close>
+  by simp
+
+end
+
+class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
+
+instance nat :: unique_euclidean_semiring_with_nat
+  by standard (simp_all add: dvd_eq_mod_eq_0)
+
+instance int :: unique_euclidean_ring_with_nat
+  by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np)
+
+
+context unique_euclidean_semiring_with_nat
+begin
+
+subclass semiring_parity
+proof
+  show "2 dvd a \<longleftrightarrow> a mod 2 = 0" for a
+    by (fact dvd_eq_mod_eq_0)
+  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" for a
+  proof
+    assume "a mod 2 = 1"
+    then show "\<not> 2 dvd a"
+      by auto
+  next
+    assume "\<not> 2 dvd a"
+    have eucl: "euclidean_size (a mod 2) = 1"
+    proof (rule order_antisym)
+      show "euclidean_size (a mod 2) \<le> 1"
+        using mod_size_less [of 2 a] by simp
+      show "1 \<le> euclidean_size (a mod 2)"
+        using \<open>\<not> 2 dvd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
+    qed 
+    from \<open>\<not> 2 dvd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
+      by simp
+    then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
+      by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
+    then have "\<not> 2 dvd euclidean_size a"
+      using of_nat_dvd_iff [of 2] by simp
+    then have "euclidean_size a mod 2 = 1"
+      by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
+    then have "of_nat (euclidean_size a mod 2) = of_nat 1"
+      by simp
+    then have "of_nat (euclidean_size a) mod 2 = 1"
+      by (simp add: of_nat_mod)
+    from \<open>\<not> 2 dvd a\<close> eucl
+    show "a mod 2 = 1"
+      by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
+  qed
+  show "\<not> is_unit 2"
+  proof (rule notI)
+    assume "is_unit 2"
+    then have "of_nat 2 dvd of_nat 1"
+      by simp
+    then have "is_unit (2::nat)"
+      by (simp only: of_nat_dvd_iff)
+    then show False
+      by simp
+  qed
+qed
+
+lemma even_succ_div_two [simp]:
+  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
+  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
+
+lemma odd_succ_div_two [simp]:
+  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
+  by (auto elim!: oddE simp add: add.assoc)
+
+lemma even_two_times_div_two:
+  "even a \<Longrightarrow> 2 * (a div 2) = a"
+  by (fact dvd_mult_div_cancel)
+
+lemma odd_two_times_div_two_succ [simp]:
+  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
+  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
+
+context unique_euclidean_ring_with_nat
+begin
+
+subclass ring_parity ..
+
+lemma minus_1_mod_2_eq [simp]:
+  "- 1 mod 2 = 1"
+  by (simp add: mod_2_eq_odd)
+
+lemma minus_1_div_2_eq [simp]:
+  "- 1 div 2 = - 1"
+proof -
+  from div_mult_mod_eq [of "- 1" 2]
+  have "- 1 div 2 * 2 = - 1 * 2"
+    using add_implies_diff by fastforce
+  then show ?thesis
+    using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
+qed
+
+end
+
+context unique_euclidean_semiring_with_nat
+begin
+
+lemma even_mask_div_iff':
+  \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
+proof -
+  have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close>
+    by (simp only: of_nat_div) (simp add: of_nat_diff)
+  also have \<open>\<dots> \<longleftrightarrow> even ((2 ^ m - Suc 0) div 2 ^ n)\<close>
+    by simp
+  also have \<open>\<dots> \<longleftrightarrow> m \<le> n\<close>
+  proof (cases \<open>m \<le> n\<close>)
+    case True
+    then show ?thesis
+      by (simp add: Suc_le_lessD)
+  next
+    case False
+    then obtain r where r: \<open>m = n + Suc r\<close>
+      using less_imp_Suc_add by fastforce
+    from r have \<open>{q. q < m} \<inter> {q. 2 ^ n dvd (2::nat) ^ q} = {q. n \<le> q \<and> q < m}\<close>
+      by (auto simp add: dvd_power_iff_le)
+    moreover from r have \<open>{q. q < m} \<inter> {q. \<not> 2 ^ n dvd (2::nat) ^ q} = {q. q < n}\<close>
+      by (auto simp add: dvd_power_iff_le)
+    moreover from False have \<open>{q. n \<le> q \<and> q < m \<and> q \<le> n} = {n}\<close>
+      by auto
+    then have \<open>odd ((\<Sum>a\<in>{q. n \<le> q \<and> q < m}. 2 ^ a div (2::nat) ^ n) + sum ((^) 2) {q. q < n} div 2 ^ n)\<close>
+      by (simp_all add: euclidean_semiring_cancel_class.power_diff_power_eq semiring_parity_class.even_sum_iff not_less mask_eq_sum_exp_nat [symmetric])
+    ultimately have \<open>odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)\<close>
+      by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all
+    with False show ?thesis
+      by (simp add: mask_eq_sum_exp_nat)
+  qed
+  finally show ?thesis .
+qed
+
+end
+
+
+subsection \<open>Generic symbolic computations\<close>
+
+text \<open>
+  The following type class contains everything necessary to formulate
+  a division algorithm in ring structures with numerals, restricted
+  to its positive segments.
+\<close>
+
+class unique_euclidean_semiring_with_nat_division = unique_euclidean_semiring_with_nat +
+  fixes divmod :: \<open>num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a\<close>
+    and divmod_step :: \<open>'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a\<close> \<comment> \<open>
+      These are conceptually definitions but force generated code
+      to be monomorphic wrt. particular instances of this class which
+      yields a significant speedup.\<close>
+  assumes divmod_def: \<open>divmod m n = (numeral m div numeral n, numeral m mod numeral n)\<close>
+    and divmod_step_def [simp]: \<open>divmod_step l (q, r) =
+      (if euclidean_size l \<le> euclidean_size r then (2 * q + 1, r - l)
+       else (2 * q, r))\<close> \<comment> \<open>
+         This is a formulation of one step (referring to one digit position)
+         in school-method division: compare the dividend at the current
+         digit position with the remainder from previous division steps
+         and evaluate accordingly.\<close>
+begin
+
+lemma fst_divmod:
+  \<open>fst (divmod m n) = numeral m div numeral n\<close>
+  by (simp add: divmod_def)
+
+lemma snd_divmod:
+  \<open>snd (divmod m n) = numeral m mod numeral n\<close>
+  by (simp add: divmod_def)
+
+text \<open>
+  Following a formulation of school-method division.
+  If the divisor is smaller than the dividend, terminate.
+  If not, shift the dividend to the right until termination
+  occurs and then reiterate single division steps in the
+  opposite direction.
+\<close>
+
+lemma divmod_divmod_step:
+  \<open>divmod m n = (if m < n then (0, numeral m)
+    else divmod_step (numeral n) (divmod m (Num.Bit0 n)))\<close>
+proof (cases \<open>m < n\<close>)
+  case True
+  then show ?thesis
+    by (simp add: prod_eq_iff fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod)
+next
+  case False
+  define r s t where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close> \<open>t = 2 * s\<close>
+  then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close> \<open>numeral (num.Bit0 n) = of_nat t\<close>
+    and \<open>\<not> s \<le> r mod s\<close>
+    by (simp_all add: not_le)
+  have t: \<open>2 * (r div t) = r div s - r div s mod 2\<close>
+    \<open>r mod t = s * (r div s mod 2) + r mod s\<close>
+    by (simp add: Rings.minus_mod_eq_mult_div Groups.mult.commute [of 2] Euclidean_Division.div_mult2_eq \<open>t = 2 * s\<close>)
+      (use mod_mult2_eq [of r s 2] in \<open>simp add: ac_simps \<open>t = 2 * s\<close>\<close>)
+  have rs: \<open>r div s mod 2 = 0 \<or> r div s mod 2 = Suc 0\<close>
+    by auto
+  from \<open>\<not> s \<le> r mod s\<close> have \<open>s \<le> r mod t \<Longrightarrow>
+     r div s = Suc (2 * (r div t)) \<and>
+     r mod s = r mod t - s\<close>
+    using rs
+    by (auto simp add: t)
+  moreover have \<open>r mod t < s \<Longrightarrow>
+     r div s = 2 * (r div t) \<and>
+     r mod s = r mod t\<close>
+    using rs
+    by (auto simp add: t)
+  ultimately show ?thesis
+    by (simp add: divmod_def prod_eq_iff split_def Let_def
+        not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *)
+    (simp add: flip: of_nat_numeral of_nat_mult add.commute [of 1] of_nat_div of_nat_mod of_nat_Suc of_nat_diff)
+qed
+
+text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
+
+lemma divmod_trivial [simp]:
+  "divmod m Num.One = (numeral m, 0)"
+  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
+  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
+  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
+
+text \<open>Division by an even number is a right-shift\<close>
+
+lemma divmod_cancel [simp]:
+  \<open>divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))\<close> (is ?P)
+  \<open>divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))\<close> (is ?Q)
+proof -
+  define r s where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close>
+  then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close>
+    \<open>numeral (num.Bit0 m) = of_nat (2 * r)\<close> \<open>numeral (num.Bit0 n) = of_nat (2 * s)\<close>
+    \<open>numeral (num.Bit1 m) = of_nat (Suc (2 * r))\<close>
+    by simp_all
+  have **: \<open>Suc (2 * r) div 2 = r\<close>
+    by simp
+  show ?P and ?Q
+    by (simp_all add: divmod_def *)
+      (simp_all flip: of_nat_numeral of_nat_div of_nat_mod of_nat_mult add.commute [of 1] of_nat_Suc
+       add: Euclidean_Division.mod_mult_mult1 div_mult2_eq [of _ 2] mod_mult2_eq [of _ 2] **)
+qed
+
+text \<open>The really hard work\<close>
+
+lemma divmod_steps [simp]:
+  "divmod (num.Bit0 m) (num.Bit1 n) =
+      (if m \<le> n then (0, numeral (num.Bit0 m))
+       else divmod_step (numeral (num.Bit1 n))
+             (divmod (num.Bit0 m)
+               (num.Bit0 (num.Bit1 n))))"
+  "divmod (num.Bit1 m) (num.Bit1 n) =
+      (if m < n then (0, numeral (num.Bit1 m))
+       else divmod_step (numeral (num.Bit1 n))
+             (divmod (num.Bit1 m)
+               (num.Bit0 (num.Bit1 n))))"
+  by (simp_all add: divmod_divmod_step)
+
+lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps
+
+text \<open>Special case: divisibility\<close>
+
+definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
+where
+  "divides_aux qr \<longleftrightarrow> snd qr = 0"
+
+lemma divides_aux_eq [simp]:
+  "divides_aux (q, r) \<longleftrightarrow> r = 0"
+  by (simp add: divides_aux_def)
+
+lemma dvd_numeral_simp [simp]:
+  "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
+  by (simp add: divmod_def mod_eq_0_iff_dvd)
+
+text \<open>Generic computation of quotient and remainder\<close>
+
+lemma numeral_div_numeral [simp]:
+  "numeral k div numeral l = fst (divmod k l)"
+  by (simp add: fst_divmod)
+
+lemma numeral_mod_numeral [simp]:
+  "numeral k mod numeral l = snd (divmod k l)"
+  by (simp add: snd_divmod)
+
+lemma one_div_numeral [simp]:
+  "1 div numeral n = fst (divmod num.One n)"
+  by (simp add: fst_divmod)
+
+lemma one_mod_numeral [simp]:
+  "1 mod numeral n = snd (divmod num.One n)"
+  by (simp add: snd_divmod)
+
+end
+
+instantiation nat :: unique_euclidean_semiring_with_nat_division
+begin
+
+definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
+where
+  divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_nat :: "nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+where
+  "divmod_step_nat l qr = (let (q, r) = qr
+    in if r \<ge> l then (2 * q + 1, r - l)
+    else (2 * q, r))"
+
+instance
+  by standard (simp_all add: divmod'_nat_def divmod_step_nat_def)
+
+end
+
+declare divmod_algorithm_code [where ?'a = nat, code]
+
+lemma Suc_0_div_numeral [simp]:
+  \<open>Suc 0 div numeral Num.One = 1\<close>
+  \<open>Suc 0 div numeral (Num.Bit0 n) = 0\<close>
+  \<open>Suc 0 div numeral (Num.Bit1 n) = 0\<close>
+  by simp_all
+
+lemma Suc_0_mod_numeral [simp]:
+  \<open>Suc 0 mod numeral Num.One = 0\<close>
+  \<open>Suc 0 mod numeral (Num.Bit0 n) = 1\<close>
+  \<open>Suc 0 mod numeral (Num.Bit1 n) = 1\<close>
+  by simp_all
+
+instantiation int :: unique_euclidean_semiring_with_nat_division
+begin
+
+definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
+where
+  "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_int :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
+where
+  "divmod_step_int l qr = (let (q, r) = qr
+    in if \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
+    else (2 * q, r))"
+
+instance
+  by standard (auto simp add: divmod_int_def divmod_step_int_def)
+
+end
+
+declare divmod_algorithm_code [where ?'a = int, code]
+
+context
+begin
+
+qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
+where
+  "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
+
+qualified lemma adjust_div_eq [simp, code]:
+  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
+  by (simp add: adjust_div_def)
+
+qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int"
+where
+  [simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"
+
+lemma minus_numeral_div_numeral [simp]:
+  "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
+proof -
+  have "int (fst (divmod m n)) = fst (divmod m n)"
+    by (simp only: fst_divmod divide_int_def) auto
+  then show ?thesis
+    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
+qed
+
+lemma minus_numeral_mod_numeral [simp]:
+  "- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
+  then show ?thesis
+    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+  case False
+  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+    by (simp only: snd_divmod modulo_int_def) auto
+  then show ?thesis
+    by (simp add: divides_aux_def adjust_div_def)
+      (simp add: divides_aux_def modulo_int_def)
+qed
+
+lemma numeral_div_minus_numeral [simp]:
+  "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
+proof -
+  have "int (fst (divmod m n)) = fst (divmod m n)"
+    by (simp only: fst_divmod divide_int_def) auto
+  then show ?thesis
+    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
+qed
+
+lemma numeral_mod_minus_numeral [simp]:
+  "numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
+  then show ?thesis
+    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+  case False
+  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+    by (simp only: snd_divmod modulo_int_def) auto
+  then show ?thesis
+    by (simp add: divides_aux_def adjust_div_def)
+      (simp add: divides_aux_def modulo_int_def)
+qed
+
+lemma minus_one_div_numeral [simp]:
+  "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
+  using minus_numeral_div_numeral [of Num.One n] by simp
+
+lemma minus_one_mod_numeral [simp]:
+  "- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
+  using minus_numeral_mod_numeral [of Num.One n] by simp
+
+lemma one_div_minus_numeral [simp]:
+  "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
+  using numeral_div_minus_numeral [of Num.One n] by simp
+
+lemma one_mod_minus_numeral [simp]:
+  "1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
+  using numeral_mod_minus_numeral [of Num.One n] by simp
+
+lemma [code]:
+  fixes k :: int
+  shows
+    "k div 0 = 0"
+    "k mod 0 = k"
+    "0 div k = 0"
+    "0 mod k = 0"
+    "k div Int.Pos Num.One = k"
+    "k mod Int.Pos Num.One = 0"
+    "k div Int.Neg Num.One = - k"
+    "k mod Int.Neg Num.One = 0"
+    "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
+    "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
+    "Int.Neg m div Int.Pos n = - (adjust_div (divmod m n) :: int)"
+    "Int.Neg m mod Int.Pos n = adjust_mod n (snd (divmod m n) :: int)"
+    "Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)"
+    "Int.Pos m mod Int.Neg n = - adjust_mod n (snd (divmod m n) :: int)"
+    "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
+    "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
+  by simp_all
+
+end
+
+lemma divmod_BitM_2_eq [simp]:
+  \<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close>
+  by (cases m) simp_all
+
+
+subsubsection \<open>Computation by simplification\<close>
+
+lemma euclidean_size_nat_less_eq_iff:
+  \<open>euclidean_size m \<le> euclidean_size n \<longleftrightarrow> m \<le> n\<close> for m n :: nat
+  by simp
+
+lemma euclidean_size_int_less_eq_iff:
+  \<open>euclidean_size k \<le> euclidean_size l \<longleftrightarrow> \<bar>k\<bar> \<le> \<bar>l\<bar>\<close> for k l :: int
+  by auto
+
+simproc_setup numeral_divmod
+  ("0 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "0 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "0 div - 1 :: int" | "0 mod - 1 :: int" |
+   "0 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
+   "1 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "1 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "1 div - 1 :: int" | "1 mod - 1 :: int" |
+   "1 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
+   "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
+   "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
+   "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
+   "numeral a div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "numeral a div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
+   "numeral a div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
+   "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
+   "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
+   "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
+   "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
+   "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") = \<open>
+  let
+    val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>);
+    fun successful_rewrite ctxt ct =
+      let
+        val thm = Simplifier.rewrite ctxt ct
+      in if Thm.is_reflexive thm then NONE else SOME thm end;
+  in fn phi =>
+    let
+      val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
+        one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
+        one_div_minus_numeral one_mod_minus_numeral
+        numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
+        numeral_div_minus_numeral numeral_mod_minus_numeral
+        div_minus_minus mod_minus_minus Parity.adjust_div_eq of_bool_eq one_neq_zero
+        numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
+        divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One
+        case_prod_beta rel_simps Parity.adjust_mod_def div_minus1_right mod_minus1_right
+        minus_minus numeral_times_numeral mult_zero_right mult_1_right
+        euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
+        @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
+      fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
+        (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
+    in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
+  end
+\<close> \<comment> \<open>
+  There is space for improvement here: the calculation itself
+  could be carried out outside the logic, and a generic simproc
+  (simplifier setup) for generic calculation would be helpful.
+\<close>
+
+
 subsection \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
 
 context unique_euclidean_semiring_with_nat_division

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_easychair.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,108 @@
+/*  Title:      Pure/Admin/build_easychair.scala
+    Author:     Makarius
+
+Build Isabelle component for Easychair style.
+
+See also https://easychair.org/publications/for_authors
+*/
+
+package isabelle
+
+
+object Build_Easychair {
+  /* build easychair component */
+
+  val default_url = "https://easychair.org/publications/easychair.zip"
+
+  def build_easychair(
+    download_url: String = default_url,
+    target_dir: Path = Path.current,
+    progress: Progress = new Progress
+  ): Unit = {
+    Isabelle_System.require_command("unzip", test = "-h")
+
+    Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
+      Isabelle_System.with_tmp_dir("download") { download_dir =>
+
+        /* download */
+
+        Isabelle_System.download_file(download_url, download_file, progress = progress)
+        Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
+          cwd = download_dir.file).check
+
+        val easychair_dir =
+          File.read_dir(download_dir) match {
+            case List(name) => download_dir + Path.explode(name)
+            case bad =>
+              error("Expected exactly one directory entry in " + download_file +
+                bad.mkString("\n", "\n  ", ""))
+          }
+
+
+        /* component */
+
+        val version =
+          Library.try_unprefix("EasyChair", easychair_dir.file_name)
+            .getOrElse("Failed to detect version from " + quote(easychair_dir.file_name))
+
+        val component = "easychair-" + version
+        val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
+        progress.echo("Component " + component_dir)
+
+        component_dir.file.delete
+        Isabelle_System.copy_dir(easychair_dir, component_dir)
+
+
+        /* settings */
+
+        val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+        File.write(etc_dir + Path.basic("settings"),
+          """# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_EASYCHAIR_HOME="$COMPONENT"
+""")
+
+
+        /* README */
+
+        File.write(component_dir + Path.basic("README"),
+          """This is the Easychair style for authors from
+""" + download_url + """
+
+
+    Makarius
+    """ + Date.Format.date(Date.now()) + "\n")
+      }
+    }
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_easychair", "build component for Easychair style",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+        var download_url = default_url
+
+        val getopts = Getopts("""
+Usage: isabelle build_easychair [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -U URL       download URL (default: """" + default_url + """")
+
+  Build component for Easychair style.
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "U:" -> (arg => download_url = arg))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress()
+
+        build_easychair(download_url = download_url, target_dir = target_dir, progress = progress)
+      })
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_foiltex.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,117 @@
+/*  Title:      Pure/Admin/build_foiltex.scala
+    Author:     Makarius
+
+Build Isabelle component for FoilTeX.
+
+See also https://ctan.org/pkg/foiltex
+*/
+
+package isabelle
+
+
+object Build_Foiltex {
+  /* build FoilTeX component */
+
+  val default_url = "https://mirrors.ctan.org/macros/latex/contrib/foiltex.zip"
+
+  def build_foiltex(
+    download_url: String = default_url,
+    target_dir: Path = Path.current,
+    progress: Progress = new Progress
+  ): Unit = {
+    Isabelle_System.require_command("unzip", test = "-h")
+
+    Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
+      Isabelle_System.with_tmp_dir("download") { download_dir =>
+
+        /* download */
+
+        Isabelle_System.download_file(download_url, download_file, progress = progress)
+        Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
+          cwd = download_dir.file).check
+
+        val foiltex_dir =
+          File.read_dir(download_dir) match {
+            case List(name) => download_dir + Path.explode(name)
+            case bad =>
+              error("Expected exactly one directory entry in " + download_file +
+                bad.mkString("\n", "\n  ", ""))
+          }
+
+        val README = Path.explode("README")
+        val README_flt = Path.explode("README.flt")
+        Isabelle_System.move_file(foiltex_dir + README, foiltex_dir + README_flt)
+
+        Isabelle_System.bash("pdflatex foiltex.ins", cwd = foiltex_dir.file).check
+
+
+        /* component */
+
+        val version = {
+          val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r
+          split_lines(File.read(foiltex_dir + README_flt))
+            .collectFirst({ case Version(v) => v })
+            .getOrElse(error("Failed to detect version in " + README_flt))
+        }
+
+        val component = "foiltex-" + version
+        val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
+        progress.echo("Component " + component_dir)
+
+        component_dir.file.delete
+        Isabelle_System.copy_dir(foiltex_dir, component_dir)
+
+
+        /* settings */
+
+        val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+        File.write(etc_dir + Path.basic("settings"),
+          """# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_FOILTEX_HOME="$COMPONENT"
+""")
+
+
+        /* README */
+
+        File.write(component_dir + Path.basic("README"),
+          """This is FoilTeX from
+""" + download_url + """
+
+
+    Makarius
+    """ + Date.Format.date(Date.now()) + "\n")
+      }
+    }
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_foiltex", "build component for FoilTeX",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+        var download_url = default_url
+
+        val getopts = Getopts("""
+Usage: isabelle build_foiltex [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -U URL       download URL (default: """" + default_url + """")
+
+  Build component for FoilTeX: slides in LaTeX.
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "U:" -> (arg => download_url = arg))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress()
+
+        build_foiltex(download_url = download_url, target_dir = target_dir, progress = progress)
+      })
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_lipics.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -0,0 +1,107 @@
+/*  Title:      Pure/Admin/build_lipics.scala
+    Author:     Makarius
+
+Build Isabelle component for Dagstuhl LIPIcs style.
+
+See also:
+
+  - https://github.com/dagstuhl-publishing/styles
+  - https://submission.dagstuhl.de/documentation/authors
+  - https://www.dagstuhl.de/en/publications/lipics
+*/
+
+package isabelle
+
+
+object Build_LIPIcs {
+  /* build lipics component */
+
+  val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz"
+
+  def build_lipics(
+    download_url: String = default_url,
+    target_dir: Path = Path.current,
+    progress: Progress = new Progress
+  ): Unit = {
+    Isabelle_System.with_tmp_file("download", ext = "tar.gz") { download_file =>
+      Isabelle_System.with_tmp_dir("download") { download_dir =>
+
+        /* download */
+
+        Isabelle_System.download_file(download_url, download_file, progress = progress)
+        Isabelle_System.gnutar("-xzf " + File.bash_path(download_file),
+          dir = download_dir, strip = 1).check
+
+        val lipics_dir = download_dir + Path.explode("LIPIcs/authors")
+
+
+        /* component */
+
+        val version = {
+          val Version = """^*.* v(.*)$""".r
+          val changelog = Path.explode("CHANGELOG.md")
+          split_lines(File.read(lipics_dir + changelog))
+            .collectFirst({ case Version(v) => v })
+            .getOrElse(error("Failed to detect version in " + changelog))
+        }
+
+        val component = "lipics-" + version
+        val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
+        progress.echo("Component " + component_dir)
+
+        Isabelle_System.copy_dir(lipics_dir, component_dir)
+
+
+        /* settings */
+
+        val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+        File.write(etc_dir + Path.basic("settings"),
+          """# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_LIPICS_HOME="$COMPONENT/authors"
+""")
+
+
+        /* README */
+
+        File.write(component_dir + Path.basic("README"),
+          """This is the Dagstuhl LIPIcs style for authors from
+""" + download_url + """
+
+
+    Makarius
+    """ + Date.Format.date(Date.now()) + "\n")
+      }
+    }
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_lipics", "build component for Dagstuhl LIPIcs style",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+        var download_url = default_url
+
+        val getopts = Getopts("""
+Usage: isabelle build_lipics [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -U URL       download URL (default: """" + default_url + """")
+
+  Build component for Dagstuhl LIPIcs style.
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "U:" -> (arg => download_url = arg))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress()
+
+        build_lipics(download_url = download_url, target_dir = target_dir, progress = progress)
+      })
+}

--- a/src/Pure/PIDE/markup.ML	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 02 18:58:38 2022 +0100
@@ -237,7 +237,7 @@
   val padding_command: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
-  val functionN: string
+  val function: string -> Properties.entry
   val ML_statistics: {pid: int, stats_dir: string} -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
@@ -250,7 +250,6 @@
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val build_session_finished: Properties.T
-  val print_operationsN: string
   val print_operations: Properties.T
   val exportN: string
   type export_args =
@@ -751,34 +750,33 @@
 
 (* protocol message functions *)
 
-val functionN = "function"
+fun function name = ("function", name);
 
 fun ML_statistics {pid, stats_dir} =
-  [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
+  [function "ML_statistics", ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
 
-val commands_accepted = [(functionN, "commands_accepted")];
+val commands_accepted = [function "commands_accepted"];
 
-val assign_update = [(functionN, "assign_update")];
-val removed_versions = [(functionN, "removed_versions")];
+val assign_update = [function "assign_update"];
+val removed_versions = [function "removed_versions"];
 
-fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+fun invoke_scala name id = [function "invoke_scala", (nameN, name), (idN, id)];
 
-fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
-
-val task_statistics = (functionN, "task_statistics");
+fun cancel_scala id = [function "cancel_scala", (idN, id)];
 
-val command_timing = (functionN, "command_timing");
+val task_statistics = function "task_statistics";
 
-val theory_timing = (functionN, "theory_timing");
+val command_timing = function "command_timing";
 
-val session_timing = (functionN, "session_timing");
+val theory_timing = function "theory_timing";
 
-fun loading_theory name = [("function", "loading_theory"), (nameN, name)];
+val session_timing = function "session_timing";
+
+fun loading_theory name = [function "loading_theory", (nameN, name)];
 
-val build_session_finished = [("function", "build_session_finished")];
+val build_session_finished = [function "build_session_finished"];
 
-val print_operationsN = "print_operations";
-val print_operations = [(functionN, print_operationsN)];
+val print_operations = [function "print_operations"];
 
 
 (* export *)
@@ -795,7 +793,7 @@
   strict: bool};
 
 fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) =
- [(functionN, exportN),
+ [function exportN,
   (idN, the_default "" id),
   (serialN, Value.print_int serial),
   ("theory_name", theory_name),
@@ -807,8 +805,8 @@
 
 (* debugger *)
 
-fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)];
-fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
+fun debugger_state name = [function "debugger_state", (nameN, name)];
+fun debugger_output name = [function "debugger_output", (nameN, name)];
 
 
 (* simplifier trace *)
@@ -821,7 +819,7 @@
 val simp_trace_hintN = "simp_trace_hint";
 val simp_trace_ignoreN = "simp_trace_ignore";
 
-fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)];
+fun simp_trace_cancel i = [function "simp_trace_cancel", (serialN, Value.print_int i)];

--- a/src/Pure/PIDE/markup.scala	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -612,13 +612,13 @@
   val FUNCTION = "function"
 
   class Function(val name: String) {
-    val PROPERTY: Properties.Entry = (FUNCTION, name)
+    val THIS: Properties.Entry = (FUNCTION, name)
   }
 
   class Properties_Function(name: String) extends Function(name) {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
-        case PROPERTY :: args => Some(args)
+        case THIS :: args => Some(args)
         case _ => None
       }
   }
@@ -626,7 +626,7 @@
   class Name_Function(name: String) extends Function(name) {
     def unapply(props: Properties.T): Option[String] =
       props match {
-        case List(PROPERTY, (NAME, a)) => Some(a)
+        case List(THIS, (NAME, a)) => Some(a)
         case _ => None
       }
   }
@@ -634,7 +634,7 @@
   object ML_Statistics extends Function("ML_statistics") {
     def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
-        case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
+        case List(THIS, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
           Some((pid, stats_dir))
         case _ => None
       }
@@ -660,7 +660,7 @@
   object Invoke_Scala extends Function("invoke_scala") {
     def unapply(props: Properties.T): Option[(String, String)] =
       props match {
-        case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
+        case List(THIS, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
@@ -668,7 +668,7 @@
   object Cancel_Scala extends Function("cancel_scala") {
     def unapply(props: Properties.T): Option[String] =
       props match {
-        case List(PROPERTY, (ID, id)) => Some(id)
+        case List(THIS, (ID, id)) => Some(id)
         case _ => None
       }
   }

--- a/src/Pure/PIDE/session.scala	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -487,7 +487,7 @@
                 try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }
                 catch { case _: Document.State.Fail => bad_output() }
 
-              case List(Markup.Commands_Accepted.PROPERTY) =>
+              case List(Markup.Commands_Accepted.THIS) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
                     ids.foreach(id =>
@@ -495,7 +495,7 @@
                   case _ => bad_output()
                 }
 
-              case List(Markup.Assign_Update.PROPERTY) =>
+              case List(Markup.Assign_Update.THIS) =>
                 msg.text match {
                   case Protocol.Assign_Update(id, edited, update) =>
                     try {
@@ -509,7 +509,7 @@
                 }
                 delay_prune.invoke()
 
-              case List(Markup.Removed_Versions.PROPERTY) =>
+              case List(Markup.Removed_Versions.THIS) =>
                 msg.text match {
                   case Protocol.Removed(removed) =>
                     try {

--- a/src/Pure/System/isabelle_tool.scala	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -159,10 +159,13 @@
   Build_Cygwin.isabelle_tool,
   Build_Doc.isabelle_tool,
   Build_E.isabelle_tool,
+  Build_Easychair.isabelle_tool,
+  Build_Foiltex.isabelle_tool,
   Build_Fonts.isabelle_tool,
   Build_JCEF.isabelle_tool,
   Build_JDK.isabelle_tool,
   Build_JEdit.isabelle_tool,
+  Build_LIPIcs.isabelle_tool,
   Build_Minisat.isabelle_tool,
   Build_PDFjs.isabelle_tool,
   Build_PolyML.isabelle_tool1,

--- a/src/Pure/Tools/build_docker.scala	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Pure/Tools/build_docker.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -20,7 +20,12 @@
   val package_collections: Map[String, List[String]] =
     Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
       "latex" ->
-        List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science"))
+        List(
+          "texlive-bibtex-extra",
+          "texlive-fonts-extra",
+          "texlive-font-utils",
+          "texlive-latex-extra",
+          "texlive-science"))
 
   def all_packages: List[String] =
     packages ::: package_collections.valuesIterator.flatten.toList

--- a/src/Tools/jEdit/jedit_main/plugin.props	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/plugin.props	Wed Nov 02 18:58:38 2022 +0100
@@ -23,9 +23,9 @@
 #options
 plugin.isabelle.jedit_main.Plugin.option-group=isabelle-general isabelle-rendering
 options.isabelle-general.label=General
-options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1();
+options.isabelle-general.code=new isabelle.jedit.JEdit_Options$Isabelle_General_Options();
 options.isabelle-rendering.label=Rendering
-options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
+options.isabelle-rendering.code=new isabelle.jedit.JEdit_Options$Isabelle_Rendering_Options();
 
 #menu actions and dockables
 plugin.isabelle.jedit_main.Plugin.menu.label=Isabelle

--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 28 15:39:35 2022 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-/*  Title:      Tools/jEdit/src/isabelle_options.scala
-    Author:     Makarius
-
-Editor pane for plugin options.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
-
-
-abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
-  protected val components: List[(String, List[Option_Component])]
-
-  override def _init(): Unit = {
-    val dummy_property = "options.isabelle.dummy"
-
-    for ((s, cs) <- components) {
-      if (s != "") {
-        jEdit.setProperty(dummy_property, s)
-        addSeparator(dummy_property)
-        jEdit.setProperty(dummy_property, null)
-      }
-      cs.foreach(c => addComponent(c.title, c.peer))
-    }
-  }
-
-  override def _save(): Unit = {
-    for ((_, cs) <- components) cs.foreach(_.save())
-  }
-}
-
-
-class Isabelle_Options1 extends Isabelle_Options("isabelle-general") {
-  val options: JEdit_Options = PIDE.options
-
-  private val predefined =
-    List(JEdit_Sessions.logic_selector(options),
-      JEdit_Spell_Checker.dictionaries_selector())
-
-  protected val components =
-    options.make_components(predefined,
-      (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
-}
-
-
-class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") {
-  private val predefined =
-    (for {
-      (name, opt) <- PIDE.options.value.opt_iterator
-      if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
-    } yield PIDE.options.make_color_component(opt)).toList
-
-  assert(predefined.nonEmpty)
-
-  protected val components = PIDE.options.make_components(predefined, _ => false)
-}

--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -16,20 +16,10 @@
 import scala.swing.{Component, CheckBox, TextArea}
 
 import org.gjt.sp.jedit.gui.ColorWellButton
+import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
 
 
-trait Option_Component extends Component {
-  val title: String
-  def load(): Unit
-  def save(): Unit
-}
-
 object JEdit_Options {
-  /* sections */
-
-  val RENDERING_SECTION = "Rendering of Document Content"
-
-
   /* typed access and GUI components */
 
   class Access[A](access: Options.Access_Variable[A], val name: String) {
@@ -81,30 +71,86 @@
       tooltip = "Output of proof state (normally shown on State panel)"
     }
   }
+
+
+  /* editor pane for plugin options */
+
+  trait Entry extends Component {
+    val title: String
+    def load(): Unit
+    def save(): Unit
+  }
+
+  abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
+    protected val components: List[(String, List[Entry])]
+
+    override def _init(): Unit = {
+      val dummy_property = "options.isabelle.dummy"
+
+      for ((s, cs) <- components) {
+        if (s.nonEmpty) {
+          jEdit.setProperty(dummy_property, s)
+          addSeparator(dummy_property)
+          jEdit.setProperty(dummy_property, null)
+        }
+        for (c <- cs) addComponent(c.title, c.peer)
+      }
+    }
+
+    override def _save(): Unit = {
+      for ((_, cs) <- components; c <- cs) c.save()
+    }
+  }
+
+  class Isabelle_General_Options extends Isabelle_Options("isabelle-general") {
+    val options: JEdit_Options = PIDE.options
+
+    private val predefined =
+      List(JEdit_Sessions.logic_selector(options),
+        JEdit_Spell_Checker.dictionaries_selector())
+
+    protected val components: List[(String, List[Entry])] =
+      options.make_components(predefined,
+        (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
+  }
+
+  class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") {
+    private val predefined =
+      (for {
+        (name, opt) <- PIDE.options.value.opt_iterator
+        if name.endsWith("_color") && opt.section == "Rendering of Document Content"
+      } yield PIDE.options.make_color_component(opt)).toList
+
+    assert(predefined.nonEmpty)
+
+    protected val components: List[(String, List[Entry])] =
+      PIDE.options.make_components(predefined, _ => false)
+  }
 }
 
 class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
   def color_value(s: String): Color = Color_Value(string(s))
 
-  def make_color_component(opt: Options.Opt): Option_Component = {
+  def make_color_component(opt: Options.Opt): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
 
     val button = new ColorWellButton(Color_Value(opt.value))
-    val component = new Component with Option_Component {
-      override lazy val peer: JComponent = button
-      name = opt_name
-      val title: String = opt_title
-      def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
-      def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
-    }
+    val component =
+      new Component with JEdit_Options.Entry {
+        override lazy val peer: JComponent = button
+        name = opt_name
+        val title: String = opt_title
+        def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
+        def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
+      }
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
-  def make_component(opt: Options.Opt): Option_Component = {
+  def make_component(opt: Options.Opt): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
@@ -112,7 +158,7 @@
 
     val component =
       if (opt.typ == Options.Bool)
-        new CheckBox with Option_Component {
+        new CheckBox with JEdit_Options.Entry {
           name = opt_name
           val title: String = opt_title
           def load(): Unit = selected = bool(opt_name)
@@ -121,7 +167,7 @@
       else {
         val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
         val text_area =
-          new TextArea with Option_Component {
+          new TextArea with JEdit_Options.Entry {
             if (default_font != null) font = default_font
             name = opt_name
             val title: String = opt_title
@@ -149,10 +195,10 @@
   }
 
   def make_components(
-    predefined: List[Option_Component],
+    predefined: List[JEdit_Options.Entry],
     filter: String => Boolean
-  ) : List[(String, List[Option_Component])] = {
-    def mk_component(opt: Options.Opt): List[Option_Component] =
+  ) : List[(String, List[JEdit_Options.Entry])] = {
+    def mk_component(opt: Options.Opt): List[JEdit_Options.Entry] =
       predefined.find(opt.name == _.name) match {
         case Some(c) => List(c)
         case None => if (filter(opt.name)) List(make_component(opt)) else Nil
@@ -162,4 +208,3 @@
       .filterNot(_._2.isEmpty)
   }
 }
-

--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -73,7 +73,7 @@
     override def toString: String = proper_string(description) getOrElse name
   }
 
-  def logic_selector(options: Options_Variable, autosave: Boolean = false): Option_Component = {
+  def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")")
@@ -85,7 +85,8 @@
       (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name))
     }
 
-    new GUI.Selector[Logic_Entry](default_entry :: session_entries) with Option_Component {
+    new GUI.Selector[Logic_Entry](default_entry :: session_entries)
+    with JEdit_Options.Entry {
       name = jedit_logic_option
       tooltip = "Logic session name (change requires restart)"
       val title = "Logic"

--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Fri Oct 28 15:39:35 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Wed Nov 02 18:58:38 2022 +0100
@@ -79,13 +79,13 @@
 
   /* dictionaries */
 
-  def dictionaries_selector(): Option_Component = {
+  def dictionaries_selector(): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
-    new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with Option_Component {
+    new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with JEdit_Options.Entry {
       name = option_name
       tooltip = GUI.tooltip_lines(opt.print_default)
       val title = opt.title()

author	desharna
	Wed, 02 Nov 2022 18:58:38 +0100
changeset 76402	2fd70eb1e9b6
parent 76401	e7e8fbc89870 (current diff)
parent 76400	d9c78a18b44b (diff)
child 76421	e800cc580c80
child 76422	2612b3406b61