diff --git a/admin/jenkins/ci_build_all.scala b/admin/jenkins/ci_build_all.scala
--- a/admin/jenkins/ci_build_all.scala
+++ b/admin/jenkins/ci_build_all.scala
@@ -1,257 +1,257 @@
object profile extends isabelle.CI_Profile
{
import isabelle._
import java.io.FileReader
import scala.sys.process._
import org.apache.commons.configuration2._
override def clean = false
val afp = Path.explode("$AFP_BASE")
val afp_thys = afp + Path.explode("thys")
val afp_id = hg_id(afp)
sealed abstract class Status(val str: String)
{
def merge(that: Status): Status = (this, that) match {
case (Ok, s) => s
case (Failed, s) => Failed
case (Skipped, Failed) => Failed
case (Skipped, s) => Skipped
}
}
object Status
{
def merge(statuses: List[Status]): Status =
statuses.foldLeft(Ok: Status)(_ merge _)
def from_results(results: Build.Results, session: String): Status =
if (results.cancelled(session))
Skipped
else if (results(session).ok)
Ok
else
Failed
}
case object Ok extends Status("ok")
case object Skipped extends Status("skipped")
case object Failed extends Status("failed")
case class Mail(subject: String, recipients: List[String], text: String) {
import java.util._
import javax.mail._
import javax.mail.internet._
import javax.activation._
def send(): Unit = {
val authenticator = new Authenticator() {
override def getPasswordAuthentication() =
new PasswordAuthentication(System.getProperty("mail.smtp.user"), System.getProperty("mail.smtp.password"))
}
val session = Session.getDefaultInstance(System.getProperties(), authenticator)
val message = new MimeMessage(session)
message.setFrom(new InternetAddress("ci@isabelle.systems", "Isabelle/Jenkins"))
message.setSender(new InternetAddress("ge73ruk@mytum.de"))
message.setSubject(subject)
message.setText(text, "UTF-8")
message.setSentDate(new java.util.Date())
recipients.foreach { recipient =>
message.addRecipient(Message.RecipientType.TO, new InternetAddress(recipient))
}
try {
Transport.send(message)
}
catch {
case ex: MessagingException => println(s"Sending mail failed: ${ex.getMessage}")
}
}
}
class Metadata(ini: INIConfiguration)
{
def maintainers(entry: String): List[String] =
{
val config = ini.getSection(entry)
val raw =
if (config.containsKey("notify"))
config.getString("notify")
else
""
List(raw.split(','): _*).map(_.trim).filterNot(_.isEmpty)
}
def entry_of_session(info: Sessions.Info): Option[String] =
if (info.dir.dir.file == afp_thys.file)
Some(info.dir.base.implode)
else
None
def notify(name: String, result: Process_Result, info: Sessions.Info): Unit =
entry_of_session(info).foreach { entry =>
val mails = maintainers(entry)
val text =
s"""|The build for the session
| $name,
|belonging to the AFP entry
| $entry
|failed.
|
|You are receiving this mail because you are the maintainer of that AFP
|entry.
|
|The following information might help you with resolving the problem.
|
|Build log: ${Isabelle_System.getenv("BUILD_URL")}
|Isabelle ID: $isabelle_id
|AFP ID: $afp_id
|Timeout? ${result.timeout}
|Exit code: ${result.rc}
|
|Last 50 lines from stdout (if available):
|
|${result.out_lines.takeRight(50).mkString("\n")}
|
|Last 50 lines from stderr (if available):
|
|${result.err_lines.takeRight(50).mkString("\n")}
|""".stripMargin
val subject = s"Build of AFP entry $entry failed"
if (mails.isEmpty)
println(s"Entry $entry: WARNING no maintainers specified")
else
Mail(text = text, subject = subject, recipients = mails).send()
}
def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
results.sessions.toList.map { name =>
entry_of_session(results.info(name)) -> name
- }.groupBy(_._1).mapValues(_.map(_._2))
+ }.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
def status_as_json(status: Map[Option[String], Status]): String =
{
val entries_strings = status.collect {
case (Some(entry), status) =>
s"""{"entry": "$entry", "status": "${status.str}"}"""
}
val entries_string = entries_strings.mkString("[", ",\n", "]")
s"""
{"build_data":
{"isabelle_id": "$isabelle_id",
"afp_id": "$afp_id",
"time": "$start_time",
"url": "${Isabelle_System.getenv("BUILD_URL")}",
"job": "${Isabelle_System.getenv("JOB_NAME")}"
},
"entries":
$entries_string
}
"""
}
def status_as_html(status: Map[Option[String], Status]): String =
{
val entries_strings = status.collect {
case (None, Failed) =>
s"
Distribution"
case (Some(entry), Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
}
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
def can_send_mails = System.getProperties().containsKey("mail.smtp.host")
def include = List(afp_thys)
def select = Nil
def pre_hook(args: List[String]) =
{
println(s"AFP id $afp_id")
if (status_file.exists())
status_file.delete()
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
if (!can_send_mails)
println(s"Mail configuration not found.")
}
def post_hook(results: Build.Results) =
{
print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
val metadata = {
val path = afp + Path.explode("metadata/metadata")
val ini = new INIConfiguration()
if (path.is_file) {
val reader = new FileReader(path.file)
ini.read(reader)
reader.close()
}
new Metadata(ini)
}
val status =
- metadata.group_by_entry(results).mapValues { sessions =>
+ metadata.group_by_entry(results).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
- }
+ }.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, metadata.status_as_html(status))
print_section("SITEGEN")
println("Writing status file ...")
File.write(status_file, metadata.status_as_json(status))
println("Running sitegen ...")
val script = afp + Path.explode("admin/sitegen-devel")
val sitegen_result = List(script.file.toString, status_file.toString, deps_file.toString).!
if (sitegen_result > 0)
println("sitegen failed")
if (!results.ok)
{
print_section("NOTIFICATIONS")
for (name <- results.sessions)
{
val result = results(name)
if (!result.ok && !results.cancelled(name) && can_send_mails)
metadata.notify(name, result, results.info(name))
}
}
print_section("COMPLETED")
}
def selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow"))
}
diff --git a/admin/jenkins/ci_build_testboard.scala b/admin/jenkins/ci_build_testboard.scala
--- a/admin/jenkins/ci_build_testboard.scala
+++ b/admin/jenkins/ci_build_testboard.scala
@@ -1,114 +1,114 @@
object profile extends isabelle.CI_Profile
{
import isabelle._
import java.io.FileReader
import scala.sys.process._
import org.apache.commons.configuration2._
override def clean = false
val afp = Path.explode("$AFP_BASE")
val afp_thys = afp + Path.explode("thys")
val afp_id = hg_id(afp)
sealed abstract class Status(val str: String)
{
def merge(that: Status): Status = (this, that) match {
case (Ok, s) => s
case (Failed, s) => Failed
case (Skipped, Failed) => Failed
case (Skipped, s) => Skipped
}
}
object Status
{
def merge(statuses: List[Status]): Status =
statuses.foldLeft(Ok: Status)(_ merge _)
def from_results(results: Build.Results, session: String): Status =
if (results.cancelled(session))
Skipped
else if (results(session).ok)
Ok
else
Failed
}
case object Ok extends Status("ok")
case object Skipped extends Status("skipped")
case object Failed extends Status("failed")
class Metadata(ini: INIConfiguration)
{
def entry_of_session(info: Sessions.Info): Option[String] =
if (info.dir.dir.file == afp_thys.file)
Some(info.dir.base.implode)
else
None
def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
results.sessions.toList.map { name =>
entry_of_session(results.info(name)) -> name
- }.groupBy(_._1).mapValues(_.map(_._2))
+ }.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
def status_as_html(status: Map[Option[String], Status]): String =
{
val entries_strings = status.collect {
case (None, Failed) =>
s"Distribution"
case (Some(entry), Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
}
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
def include = List(afp_thys)
def select = Nil
def pre_hook(args: List[String]) =
{
println(s"AFP id $afp_id")
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
}
def post_hook(results: Build.Results) =
{
val metadata = {
val path = afp + Path.explode("metadata/metadata")
val ini = new INIConfiguration()
if (path.is_file) {
val reader = new FileReader(path.file)
ini.read(reader)
reader.close()
}
new Metadata(ini)
}
val status =
- metadata.group_by_entry(results).mapValues { sessions =>
+ metadata.group_by_entry(results).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
- }
+ }.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, metadata.status_as_html(status))
print_section("COMPLETED")
}
def selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow"))
}
diff --git a/thys/Complete_Non_Orders/Binary_Relations.thy b/thys/Complete_Non_Orders/Binary_Relations.thy
--- a/thys/Complete_Non_Orders/Binary_Relations.thy
+++ b/thys/Complete_Non_Orders/Binary_Relations.thy
@@ -1,992 +1,2245 @@
(*
-Author: Akihisa Yamada (2018-2019)
+Author: Akihisa Yamada (2018-2021)
License: LGPL (see file COPYING.LESSER)
*)
section \Binary Relations\
text \We start with basic properties of binary relations.\
theory Binary_Relations
-imports Main
-(* uses mainly concepts from the theories Complete_Partial_Order, Wellfounded, Partial_Function *)
+ imports
+(* To verify that we don't use the axiom of choice, import
+ HOL.Complete_Partial_Order HOL.Wellfounded
+ instead of *) Main
begin
+lemma conj_imp_eq_imp_imp: "(P \ Q \ PROP R) \ (P \ Q \ PROP R)"
+ by standard simp_all
+
+lemma tranclp_trancl: "r\<^sup>+\<^sup>+ = (\x y. (x,y) \ {(a,b). r a b}\<^sup>+)"
+ by (auto simp: tranclp_trancl_eq[symmetric])
+
+lemma tranclp_id[simp]: "transp r \ tranclp r = r"
+ using trancl_id[of "{(x,y). r x y}", folded transp_trans] by (auto simp:tranclp_trancl)
+
+lemma transp_tranclp[simp]: "transp (tranclp r)" by (auto simp: tranclp_trancl transp_trans)
+
+lemma funpow_dom: "f ` A \ A \ (f^^n) ` A \ A" by (induct n, auto)
+
text \Below we introduce an Isabelle-notation for $\{ \ldots x\ldots \mid x \in X \}$.\
syntax
- "_range" :: "'a \ pttrn \ 'a set" ("(1{_ /|./ _})")
+ "_range" :: "'a \ idts \ 'a set" ("(1{_ /|./ _})")
"_image" :: "'a \ pttrn \ 'a set \ 'a set" ("(1{_ /|./ (_/ \ _)})")
translations
- "{e |. p}" \ "CONST range (\p. e)"
+ "{e |. p}" \ "{e | p. CONST True}"
"{e |. p \ A}" \ "CONST image (\p. e) A"
lemma image_constant:
assumes "\i. i \ I \ f i = y"
shows "f ` I = (if I = {} then {} else {y})"
using assms by auto
subsection \Various Definitions\
text \Here we introduce various definitions for binary relations.
The first one is our abbreviation for the dual of a relation.\
abbreviation(input) dual ("(_\<^sup>-)" [1000] 1000) where "r\<^sup>- x y \ r y x"
-lemma conversep_as_dual[simp]: "conversep r = r\<^sup>-" by auto
-
-text \Monotonicity is already defined in the library.\
-lemma monotone_dual: "monotone r s f \ monotone r\<^sup>- s\<^sup>- f"
- by (auto simp: monotone_def)
-
-lemma monotone_id: "monotone r r id"
- by (auto simp: monotone_def)
-
-text \So is the chain, but it is somehow hidden. We reactivate it.\
-abbreviation "chain \ Complete_Partial_Order.chain"
-
-context fixes r :: "'a \ 'a \ bool" (infix "\" 50) begin
-
-text \Here we define the following notions in a standard manner:
-(upper) bounds of a set:\
-definition "bound X b \ \x \ X. x \ b"
-
-lemma boundI[intro!]: "(\x. x \ X \ x \ b) \ bound X b"
- and boundE[elim]: "bound X b \ ((\x. x \ X \ x \ b) \ thesis) \ thesis"
+lemma conversep_is_dual[simp]: "conversep = dual" by auto
+
+text \Monotonicity is already defined in the library, but we want one restricted to a domain.\
+
+definition "monotone_on X r s f \ \x y. x \ X \ y \ X \ r x y \ s (f x) (f y)"
+
+lemmas monotone_onI = monotone_on_def[unfolded atomize_eq, THEN iffD2, rule_format]
+lemma monotone_onD: "monotone_on X r s f \ r x y \ x \ X \ y \ X \ s (f x) (f y)"
+ by (auto simp: monotone_on_def)
+
+lemmas monotone_onE = monotone_on_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format]
+
+lemma monotone_on_UNIV[simp]: "monotone_on UNIV = monotone"
+ by (intro ext, auto simp: monotone_on_def monotone_def)
+
+lemma monotone_on_dual: "monotone_on X r s f \ monotone_on X r\<^sup>- s\<^sup>- f"
+ by (auto simp: monotone_on_def)
+
+lemma monotone_on_id: "monotone_on X r r id"
+ by (auto simp: monotone_on_def)
+
+lemma monotone_on_cmono: "A \ B \ monotone_on B \ monotone_on A"
+ by (intro le_funI, auto simp: monotone_on_def)
+
+text \Here we define the following notions in a standard manner\
+
+text \The symmetric part of a relation:\
+
+definition sympartp where "sympartp r x y \ r x y \ r y x"
+
+lemma sympartpI[intro]:
+ fixes r (infix "\" 50)
+ assumes "x \ y" and "y \ x" shows "sympartp (\) x y"
+ using assms by (auto simp: sympartp_def)
+
+lemma sympartpE[elim]:
+ fixes r (infix "\" 50)
+ assumes "sympartp (\) x y" and "x \ y \ y \ x \ thesis" shows thesis
+ using assms by (auto simp: sympartp_def)
+
+lemma sympartp_dual: "sympartp r\<^sup>- = sympartp r"
+ by (auto intro!:ext simp: sympartp_def)
+
+lemma sympartp_eq[simp]: "sympartp (=) = (=)" by auto
+
+lemma reflclp_sympartp[simp]: "(sympartp r)\<^sup>=\<^sup>= = sympartp r\<^sup>=\<^sup>=" by auto
+
+definition "equivpartp r x y \ x = y \ r x y \ r y x"
+
+lemma sympartp_reflclp_equivp[simp]: "sympartp r\<^sup>=\<^sup>= = equivpartp r" by (auto intro!:ext simp: equivpartp_def)
+
+lemma equivpartI[simp]: "equivpartp r x x"
+ and sympartp_equivpartpI: "sympartp r x y \ equivpartp r x y"
+ and equivpartpCI[intro]: "(x \ y \ sympartp r x y) \ equivpartp r x y"
+ by (auto simp:equivpartp_def)
+
+lemma equivpartpE[elim]:
+ assumes "equivpartp r x y"
+ and "x = y \ thesis"
+ and "r x y \ r y x \ thesis"
+ shows "thesis"
+ using assms by (auto simp: equivpartp_def)
+
+lemma equivpartp_eq[simp]: "equivpartp (=) = (=)" by auto
+
+lemma sympartp_equivpartp[simp]: "sympartp (equivpartp r) = (equivpartp r)"
+ and equivpartp_equivpartp[simp]: "equivpartp (equivpartp r) = (equivpartp r)"
+ and equivpartp_sympartp[simp]: "equivpartp (sympartp r) = (equivpartp r)"
+ by (auto 0 5 intro!:ext)
+
+lemma equivpartp_dual: "equivpartp r\<^sup>- = equivpartp r"
+ by (auto intro!:ext simp: equivpartp_def)
+
+text \The asymmetric part:\
+
+definition "asympartp r x y \ r x y \ \ r y x"
+
+lemma asympartpE[elim]:
+ fixes r (infix "\" 50)
+ shows "asympartp (\) x y \ (x \ y \ \y \ x \ thesis) \ thesis"
+ by (auto simp: asympartp_def)
+
+lemmas asympartpI[intro] = asympartp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format]
+
+lemma asympartp_eq[simp]: "asympartp (=) = bot" by auto
+
+lemma asympartp_sympartp [simp]: "asympartp (sympartp r) = bot"
+ and sympartp_asympartp [simp]: "sympartp (asympartp r) = bot"
+ by (auto intro!: ext)
+
+text \Restriction to a set:\
+
+definition Restrp (infixl "\" 60) where "(r \ A) a b \ a \ A \ b \ A \ r a b"
+
+lemmas RestrpI[intro!] = Restrp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp]
+lemmas RestrpE[elim!] = Restrp_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp]
+
+lemma Restrp_UNIV[simp]: "r \ UNIV \ r" by (auto simp: atomize_eq)
+
+lemma Restrp_Restrp[simp]: "r \ A \ B \ r \ A \ B" by (auto simp: atomize_eq Restrp_def)
+
+lemma sympartp_Restrp[simp]: "sympartp (r \ A) \ sympartp r \ A"
+ by (auto simp: atomize_eq)
+
+text \Relational images:\
+definition Imagep (infixr "```" 59) where "r ``` A \ {b. \a \ A. r a b}"
+
+lemma Imagep_Image: "r ``` A = {(a,b). r a b} `` A"
+ by (auto simp: Imagep_def)
+
+lemma in_Imagep: "b \ r ``` A \ (\a \ A. r a b)" by (auto simp: Imagep_def)
+
+lemma ImagepI: "a \ A \ r a b \ b \ r ``` A" by (auto simp: in_Imagep)
+
+lemma subset_Imagep: "B \ r ``` A \ (\b\B. \a\A. r a b)"
+ by (auto simp: Imagep_def)
+
+text \Bounds of a set:\
+definition "bound X r b \ \x \ X. r x b"
+
+lemma
+ fixes r (infix "\" 50)
+ shows boundI[intro!]: "(\x. x \ X \ x \ b) \ bound X (\) b"
+ and boundE[elim]: "bound X (\) b \ ((\x. x \ X \ x \ b) \ thesis) \ thesis"
by (auto simp: bound_def)
-lemma bound_empty: "bound {} = (\x. True)" by auto
-lemma bound_insert[simp]: "bound (insert x X) b \ x \ b \ bound X b" by auto
-
-lemma bound_cmono: assumes "X \ Y" shows "bound Y x \ bound X x"
- using assms by auto
+lemma bound_empty: "bound {} = (\r x. True)" by auto
+
+lemma bound_insert[simp]:
+ fixes r (infix "\" 50)
+ shows "bound (insert x X) (\) b \ x \ b \ bound X (\) b" by auto
text \Extreme (greatest) elements in a set:\
-definition "extreme X e \ e \ X \ (\x \ X. x \ e)"
-
-lemma extremeI[intro]: "e \ X \ (\x. x \ X \ x \ e) \ extreme X e"
- and extremeD: "extreme X e \ e \ X" "extreme X e \ (\x. x \ X \ x \ e)"
- and extremeE[elim]: "extreme X e \ (e \ X \ (\x. x \ X \ x \ e) \ thesis) \ thesis"
+definition "extreme X r e \ e \ X \ (\x \ X. r x e)"
+
+lemma
+ fixes r (infix "\" 50)
+ shows extremeI[intro]: "e \ X \ (\x. x \ X \ x \ e) \ extreme X (\) e"
+ and extremeD: "extreme X (\) e \ e \ X" "extreme X (\) e \ (\x. x \ X \ x \ e)"
+ and extremeE[elim]: "extreme X (\) e \ (e \ X \