--- a/etc/options Fri Nov 08 16:07:22 2019 +0000
+++ b/etc/options Fri Nov 08 16:07:31 2019 +0000
@@ -343,22 +343,6 @@
option build_log_transaction_size : int = 1 -- "number of log files for each db update"
-section "Phabricator server"
-
-option phabricator_www_user : string = "www-data"
-option phabricator_www_root : string = "/var/www"
-
-option phabricator_mysql_config : string = "/etc/mysql/debian.cnf"
-option phabricator_apache_root : string = "/etc/apache2"
-
-option phabricator_smtp_host : string = ""
-option phabricator_smtp_port : int = 465
-option phabricator_smtp_user : string = ""
-option phabricator_smtp_passwd : string = ""
-option phabricator_smtp_protocol : string = "ssl"
-option phabricator_smtp_message_id : bool = true
-
-
section "Isabelle/Scala/ML system channel"
option system_channel_address : string = ""
--- a/src/HOL/Analysis/Elementary_Topology.thy Fri Nov 08 16:07:22 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy Fri Nov 08 16:07:31 2019 +0000
@@ -16,11 +16,6 @@
section \<open>Elementary Topology\<close>
-subsection \<open>TODO: move?\<close>
-
-lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
- using openI by auto
-
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>
@@ -49,7 +44,6 @@
by (simp add: field_simps)
-
subsection \<open>Topological Basis\<close>
context topological_space
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Nov 08 16:07:22 2019 +0000
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Nov 08 16:07:31 2019 +0000
@@ -455,7 +455,7 @@
lemma ev_at_shift: "ev_at (HLD X) i (stake (Suc i) \<omega> @- \<omega>' :: 's stream) \<longleftrightarrow> ev_at (HLD X) i \<omega>"
by (induction i arbitrary: \<omega>) (auto simp: HLD_iff)
-lemma ev_iff_ev_at_unqiue: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)"
+lemma ev_iff_ev_at_unique: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)"
by (auto intro: ev_at_unique simp: ev_iff_ev_at)
lemma alw_HLD_iff_streams: "alw (HLD X) \<omega> \<longleftrightarrow> \<omega> \<in> streams X"
@@ -787,4 +787,44 @@
by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
qed (auto simp: ev_suntil)
+section \<open>Weak vs. strong until (contributed by Michael Foster, University of Sheffield)\<close>
+
+lemma suntil_implies_until: "(\<phi> suntil \<psi>) \<omega> \<Longrightarrow> (\<phi> until \<psi>) \<omega>"
+ by (induct rule: suntil_induct_strong) (auto intro: UNTIL.intros)
+
+lemma alw_implies_until: "alw \<phi> \<omega> \<Longrightarrow> (\<phi> until \<psi>) \<omega>"
+ unfolding until_false[symmetric] by (auto elim: until_mono)
+
+lemma until_ev_suntil: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> ev \<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
+proof (rotate_tac, induction rule: ev.induct)
+ case (base xs)
+ then show ?case
+ by (simp add: suntil.base)
+next
+ case (step xs)
+ then show ?case
+ by (metis UNTIL.cases suntil.base suntil.step)
+qed
+
+lemma suntil_as_until: "(\<phi> suntil \<psi>) \<omega> = ((\<phi> until \<psi>) \<omega> \<and> ev \<psi> \<omega>)"
+ using ev_suntil suntil_implies_until until_ev_suntil by blast
+
+lemma until_not_relesased_now: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> \<not> \<psi> \<omega> \<Longrightarrow> \<phi> \<omega>"
+ using UNTIL.cases by auto
+
+lemma until_must_release_ev: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> ev (not \<phi>) \<omega> \<Longrightarrow> ev \<psi> \<omega>"
+proof (rotate_tac, induction rule: ev.induct)
+ case (base xs)
+ then show ?case
+ using until_not_relesased_now by blast
+next
+ case (step xs)
+ then show ?case
+ using UNTIL.cases by blast
+qed
+
+lemma until_as_suntil: "(\<phi> until \<psi>) \<omega> = ((\<phi> suntil \<psi>) or (alw \<phi>)) \<omega>"
+ using alw_implies_until not_alw_iff suntil_implies_until until_ev_suntil until_must_release_ev
+ by blast
+
end
--- a/src/HOL/Topological_Spaces.thy Fri Nov 08 16:07:22 2019 +0000
+++ b/src/HOL/Topological_Spaces.thy Fri Nov 08 16:07:31 2019 +0000
@@ -49,6 +49,9 @@
ultimately show "open S" by simp
qed
+lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
+by (auto intro: openI)
+
lemma closed_empty [continuous_intros, intro, simp]: "closed {}"
unfolding closed_def by simp
--- a/src/Pure/Tools/phabricator.scala Fri Nov 08 16:07:22 2019 +0000
+++ b/src/Pure/Tools/phabricator.scala Fri Nov 08 16:07:31 2019 +0000
@@ -1,7 +1,9 @@
/* Title: Pure/Tools/phabricator.scala
Author: Makarius
-Support for Phabricator server. See also:
+Support for Phabricator server, notably for Ubuntu 18.04 LTS.
+
+See also:
- https://www.phacility.com/phabricator
- https://secure.phabricator.com/book/phabricator
*/
@@ -30,6 +32,8 @@
/* global system resources */
+ val www_user = "www-data"
+
val daemon_user = "phabricator"
val ssh_standard = 22
@@ -47,12 +51,12 @@
def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
"isabelle-" + phabricator_name(name = name, ext = ext)
- def default_root(options: Options, name: String): Path =
- Path.explode(options.string("phabricator_www_root")) +
- Path.basic(phabricator_name(name = name))
+ def default_root(name: String): Path =
+ Path.explode("/var/www") + Path.basic(phabricator_name(name = name))
- def default_repo(options: Options, name: String): Path =
- default_root(options, name) + Path.basic("repo")
+ def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
+
+ val default_mailers: Path = Path.explode("mailers.json")
@@ -65,7 +69,7 @@
def home: Path = root + Path.explode(phabricator_name())
def execute(command: String): Process_Result =
- Isabelle_System.bash("./bin/" + command, cwd = home.file).check
+ Isabelle_System.bash("./bin/" + command, cwd = home.file, redirect = true).check
}
def read_config(): List[Config] =
@@ -108,7 +112,6 @@
}
def phabricator_setup(
- options: Options,
name: String = default_name,
root: String = "",
repo: String = "",
@@ -119,6 +122,8 @@
Linux.check_system_root()
+ progress.echo("System packages ...")
+
if (package_update) {
Linux.package_update(progress = progress)
Linux.check_reboot_required()
@@ -137,13 +142,13 @@
user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true)
user_setup(name, "Phabricator SSH User")
- val www_user = options.string("phabricator_www_user")
-
/* basic installation */
- val root_path = if (root.nonEmpty) Path.explode(root) else default_root(options, name)
- val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(options, name)
+ progress.echo("\nPhabricator installation ...")
+
+ val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name)
+ val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name)
val configs = read_config()
@@ -190,7 +195,7 @@
/* MySQL setup */
- progress.echo("MySQL setup...")
+ progress.echo("\nMySQL setup ...")
File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")),
"""[mysqld]
@@ -203,8 +208,7 @@
def mysql_conf(R: Regex): Option[String] =
- split_lines(File.read(Path.explode(options.string("phabricator_mysql_config")))).
- collectFirst({ case R(a) => a })
+ split_lines(File.read(Path.explode("/etc/mysql/debian.cnf"))).collectFirst({ case R(a) => a })
for (user <- mysql_conf("""^user\s*=\s*(\S*)\s*$""".r)) {
config.execute("config set mysql.user " + Bash.string(user))
@@ -219,12 +223,12 @@
config.execute("config set storage.mysql-engine.max-size 8388608")
- config.execute("storage upgrade --force")
+ progress.bash("./bin/storage upgrade --force", cwd = config.home.file, echo = true).check
/* SSH hosting */
- progress.echo("SSH hosting setup...")
+ progress.echo("\nSSH hosting setup ...")
val ssh_port = ssh_alternative2
@@ -258,9 +262,9 @@
/* Apache setup */
- progress.echo("Apache setup...")
+ progress.echo("Apache setup ...")
- val apache_root = Path.explode(options.string("phabricator_apache_root"))
+ val apache_root = Path.explode("/etc/apache2")
val apache_sites = apache_root + Path.explode("sites-available")
if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites)
@@ -294,7 +298,7 @@
/* PHP daemon */
- progress.echo("PHP daemon setup...")
+ progress.echo("PHP daemon setup ...")
config.execute("config set phd.user " + Bash.string(daemon_user))
@@ -328,81 +332,139 @@
{
var repo = ""
var package_update = false
- var options = Options.init()
+ var name = default_name
var root = ""
val getopts =
Getopts("""
-Usage: isabelle phabricator_setup [OPTIONS] [NAME]
+Usage: isabelle phabricator_setup [OPTIONS]
Options are:
- -R DIR repository directory (default: """ + default_repo(options, "NAME") + """)
+ -R DIR repository directory (default: """ + default_repo("NAME") + """)
-U full update of system packages before installation
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r DIR installation root directory (default: """ + default_root(options, "NAME") + """)
+ -n NAME Phabricator installation name (default: """ + quote(default_name) + """)
+ -r DIR installation root directory (default: """ + default_root("NAME") + """)
Install Phabricator as Ubuntu LAMP application (Linux, Apache, MySQL, PHP).
Slogan: "Discuss. Plan. Code. Review. Test.
Every application your project needs, all in one tool."
- The installation NAME (default: """ + quote(default_name) + """) is mapped to
- a regular Unix user and used for public SSH access.
+ The installation name (default: """ + quote(default_name) + """) is mapped to a regular
+ Unix user; this is relevant for public SSH access.
""",
"R:" -> (arg => repo = arg),
"U" -> (_ => package_update = true),
- "o:" -> (arg => options = options + arg),
+ "n:" -> (arg => name = arg),
"r:" -> (arg => root = arg))
val more_args = getopts(args)
-
- val name =
- more_args match {
- case Nil => default_name
- case List(name) => name
- case _ => getopts.usage()
- }
+ if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress
- phabricator_setup(options, name, root = root, repo = repo,
+ phabricator_setup(name = name, root = root, repo = repo,
package_update = package_update, progress = progress)
})
- /** update **/
+ /** setup mail **/
- def phabricator_update(name: String, progress: Progress = No_Progress)
+ val mailers_template: String =
+"""[
+ {
+ "key": "example.org",
+ "type": "smtp",
+ "options": {
+ "host": "mail.example.org",
+ "port": 465,
+ "user": "phabricator@example.org",
+ "password": "********",
+ "protocol": "ssl",
+ "message-id": true
+ }
+ }
+]"""
+
+ def phabricator_setup_mail(
+ name: String = default_name,
+ config_file: Option[Path] = None,
+ test_user: String = "",
+ progress: Progress = No_Progress)
{
Linux.check_system_root()
- ???
+ val config = get_config(name)
+ val default_config_file = config.root + default_mailers
+
+ val mail_config = config_file getOrElse default_config_file
+
+ def setup_mail
+ {
+ progress.echo("Using mail configuration from " + mail_config)
+ config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config))
+
+ if (test_user.nonEmpty) {
+ progress.echo("Sending test mail to " + quote(test_user))
+ progress.bash(cwd = config.home.file, echo = true,
+ script = """echo "Test from Phabricator ($(date))" | ./bin/mail send-test --subject "Test" --to """ +
+ Bash.string(test_user)).check
+ }
+ }
+
+ if (config_file.isEmpty) {
+ if (!default_config_file.is_file) {
+ File.write(default_config_file, mailers_template)
+ Isabelle_System.bash("chmod 600 " + File.bash_path(default_config_file)).check
+ }
+ if (File.read(default_config_file) == mailers_template) {
+ progress.echo(
+"""
+Please invoke the tool again, after providing details in
+ """ + default_config_file.implode + """
+
+See also section "Mailer: SMTP" in
+ https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email
+""")
+ }
+ else setup_mail
+ }
+ else setup_mail
}
/* Isabelle tool wrapper */
val isabelle_tool2 =
- Isabelle_Tool("phabricator_update", "update Phabricator server installation", args =>
+ Isabelle_Tool("phabricator_setup_mail",
+ "setup mail configuration for existing Phabricator server", args =>
{
+ var test_user = ""
+ var name = default_name
+ var config_file: Option[Path] = None
+
val getopts =
Getopts("""
-Usage: isabelle phabricator_update [NAME]
+Usage: isabelle phabricator_setup_mail [OPTIONS]
- Update Phabricator installation, with lookup of NAME (default + """ + quote(default_name) + """)
- in """ + global_config + "\n")
+ Options are:
+ -T USER send test mail to Phabricator user
+ -f FILE config file (default: """ + default_mailers + """ within installation root)
+ -n NAME Phabricator installation name (default: """ + quote(default_name) + """)
+
+ Provide mail configuration for existing Phabricator installation.
+""",
+ "T:" -> (arg => test_user = arg),
+ "f:" -> (arg => config_file = Some(Path.explode(arg))),
+ "n:" -> (arg => name = arg))
val more_args = getopts(args)
- val name =
- more_args match {
- case Nil => default_name
- case List(name) => name
- case _ => getopts.usage()
- }
+ if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress
- phabricator_update(name, progress = progress)
+ phabricator_setup_mail(name = name, config_file = config_file,
+ test_user = test_user, progress = progress)
})
}
--- a/src/ZF/Bin.thy Fri Nov 08 16:07:22 2019 +0000
+++ b/src/ZF/Bin.thy Fri Nov 08 16:07:31 2019 +0000
@@ -162,7 +162,7 @@
by (induct_tac "w", auto)
(*This proof is complicated by the mutual recursion*)
-lemma bin_add_type [rule_format,TC]:
+lemma bin_add_type [rule_format]:
"v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
apply (unfold bin_add_def)
apply (induct_tac "v")
@@ -172,6 +172,8 @@
apply (simp_all add: NCons_type)
done
+declare bin_add_type [TC]
+
lemma bin_mult_type [TC]: "[| v \<in> bin; w \<in> bin |] ==> bin_mult(v,w) \<in> bin"
by (induct_tac "v", auto)
--- a/src/ZF/List.thy Fri Nov 08 16:07:22 2019 +0000
+++ b/src/ZF/List.thy Fri Nov 08 16:07:31 2019 +0000
@@ -567,7 +567,7 @@
apply (auto simp add: length_app)
done
-lemma append_eq_append_iff [rule_format,simp]:
+lemma append_eq_append_iff [rule_format]:
"xs:list(A) ==> \<forall>ys \<in> list(A).
length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
apply (erule list.induct)
@@ -575,6 +575,7 @@
apply clarify
apply (erule_tac a = ys in list.cases, auto)
done
+declare append_eq_append_iff [simp]
lemma append_eq_append [rule_format]:
"xs:list(A) ==>
@@ -604,7 +605,7 @@
(* Can also be proved from append_eq_append_iff2,
but the proof requires two more hypotheses: x \<in> A and y \<in> A *)
-lemma append1_eq_iff [rule_format,simp]:
+lemma append1_eq_iff [rule_format]:
"xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
apply (erule list.induct)
apply clarify
@@ -614,7 +615,7 @@
apply clarify
apply (erule_tac a=ys in list.cases, simp_all)
done
-
+declare append1_eq_iff [simp]
lemma append_right_is_self_iff [simp]:
"[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
@@ -626,13 +627,15 @@
apply (drule sym, auto)
done
-lemma hd_append [rule_format,simp]:
+lemma hd_append [rule_format]:
"xs:list(A) ==> xs \<noteq> Nil \<longrightarrow> hd(xs @ ys) = hd(xs)"
by (induct_tac "xs", auto)
+declare hd_append [simp]
-lemma tl_append [rule_format,simp]:
+lemma tl_append [rule_format]:
"xs:list(A) ==> xs\<noteq>Nil \<longrightarrow> tl(xs @ ys) = tl(xs)@ys"
by (induct_tac "xs", auto)
+declare tl_append [simp]
(** rev **)
lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
@@ -641,11 +644,12 @@
lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
by (erule list.induct, auto)
-lemma rev_is_rev_iff [rule_format,simp]:
+lemma rev_is_rev_iff [rule_format]:
"xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
apply (erule list.induct, force, clarify)
apply (erule_tac a = ys in list.cases, auto)
done
+declare rev_is_rev_iff [simp]
lemma rev_list_elim [rule_format]:
"xs:list(A) ==>
@@ -655,17 +659,19 @@
(** more theorems about drop **)
-lemma length_drop [rule_format,simp]:
+lemma length_drop [rule_format]:
"n \<in> nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
apply (erule nat_induct)
apply (auto elim: list.cases)
done
+declare length_drop [simp]
-lemma drop_all [rule_format,simp]:
+lemma drop_all [rule_format]:
"n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> drop(n, xs)=Nil"
apply (erule nat_induct)
apply (auto elim: list.cases)
done
+declare drop_all [simp]
lemma drop_append [rule_format]:
"n \<in> nat ==>
@@ -695,25 +701,28 @@
lemma take_Nil [simp]: "n \<in> nat ==> take(n, Nil) = Nil"
by (unfold take_def, auto)
-lemma take_all [rule_format,simp]:
+lemma take_all [rule_format]:
"n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> take(n, xs) = xs"
apply (erule nat_induct)
apply (auto elim: list.cases)
done
+declare take_all [simp]
-lemma take_type [rule_format,simp,TC]:
+lemma take_type [rule_format]:
"xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
apply (erule list.induct, simp, clarify)
apply (erule natE, auto)
done
+declare take_type [simp,TC]
-lemma take_append [rule_format,simp]:
+lemma take_append [rule_format]:
"xs:list(A) ==>
\<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
take(n, xs) @ take(n #- length(xs), ys)"
apply (erule list.induct, simp, clarify)
apply (erule natE, auto)
done
+declare take_append [simp]
lemma take_take [rule_format]:
"m \<in> nat ==>
@@ -736,12 +745,13 @@
lemma nth_empty [simp]: "nth(n, Nil) = 0"
by (simp add: nth_def)
-lemma nth_type [rule_format,simp,TC]:
+lemma nth_type [rule_format]:
"xs:list(A) ==> \<forall>n. n < length(xs) \<longrightarrow> nth(n,xs) \<in> A"
apply (erule list.induct, simp, clarify)
apply (subgoal_tac "n \<in> nat")
apply (erule natE, auto dest!: le_in_nat)
done
+declare nth_type [simp,TC]
lemma nth_eq_0 [rule_format]:
"xs:list(A) ==> \<forall>n \<in> nat. length(xs) \<le> n \<longrightarrow> nth(n,xs) = 0"
@@ -894,22 +904,24 @@
apply (blast intro: list_on_set_of_list list_mono [THEN subsetD])
done
-lemma zip_type [rule_format,simp,TC]:
+lemma zip_type [rule_format]:
"xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
apply (erule_tac a = ys in list.cases, auto)
done
+declare zip_type [simp,TC]
(* zip length *)
-lemma length_zip [rule_format,simp]:
+lemma length_zip [rule_format]:
"xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
min(length(xs), length(ys))"
apply (unfold min_def)
apply (induct_tac "xs", simp_all, clarify)
apply (erule_tac a = ys in list.cases, auto)
done
+declare length_zip [simp]
lemma zip_append1 [rule_format]:
"[| ys:list(A); zs:list(B) |] ==>
@@ -933,15 +945,16 @@
by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
-lemma zip_rev [rule_format,simp]:
+lemma zip_rev [rule_format]:
"ys:list(B) ==> \<forall>xs \<in> list(A).
length(xs) = length(ys) \<longrightarrow> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
apply (induct_tac "ys", force, clarify)
apply (erule_tac a = xs in list.cases)
apply (auto simp add: length_rev)
done
+declare zip_rev [simp]
-lemma nth_zip [rule_format,simp]:
+lemma nth_zip [rule_format]:
"ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
i < length(xs) \<longrightarrow> i < length(ys) \<longrightarrow>
nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
@@ -949,6 +962,7 @@
apply (erule_tac a = xs in list.cases, simp)
apply (auto elim: natE)
done
+declare nth_zip [simp]
lemma set_of_list_zip [rule_format]:
"[| xs:list(A); ys:list(B); i \<in> nat |]
@@ -971,21 +985,23 @@
apply (unfold list_update_def, auto)
done
-lemma list_update_type [rule_format,simp,TC]:
+lemma list_update_type [rule_format]:
"[| xs:list(A); v \<in> A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
apply (erule natE, auto)
done
+declare list_update_type [simp,TC]
-lemma length_list_update [rule_format,simp]:
+lemma length_list_update [rule_format]:
"xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
apply (induct_tac "xs")
apply (simp (no_asm))
apply clarify
apply (erule natE, auto)
done
+declare length_list_update [simp]
lemma nth_list_update [rule_format]:
"[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs) \<longrightarrow>
@@ -1004,7 +1020,7 @@
by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
-lemma nth_list_update_neq [rule_format,simp]:
+lemma nth_list_update_neq [rule_format]:
"xs:list(A) ==>
\<forall>i \<in> nat. \<forall>j \<in> nat. i \<noteq> j \<longrightarrow> nth(j, list_update(xs,i,x)) = nth(j,xs)"
apply (induct_tac "xs")
@@ -1014,8 +1030,9 @@
apply (erule_tac [2] natE, simp_all)
apply (erule natE, simp_all)
done
+declare nth_list_update_neq [simp]
-lemma list_update_overwrite [rule_format,simp]:
+lemma list_update_overwrite [rule_format]:
"xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
\<longrightarrow> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
apply (induct_tac "xs")
@@ -1023,6 +1040,7 @@
apply clarify
apply (erule natE, auto)
done
+declare list_update_overwrite [simp]
lemma list_update_same_conv [rule_format]:
"xs:list(A) ==>
@@ -1105,15 +1123,16 @@
apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
done
-lemma nth_upt [rule_format,simp]:
+lemma nth_upt [rule_format]:
"[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k"
apply (induct_tac "j", simp)
apply (simp add: nth_append le_iff)
apply (auto dest!: not_lt_imp_le
simp add: nth_append less_diff_conv add_commute)
done
+declare nth_upt [simp]
-lemma take_upt [rule_format,simp]:
+lemma take_upt [rule_format]:
"[| m \<in> nat; n \<in> nat |] ==>
\<forall>i \<in> nat. i #+ m \<le> n \<longrightarrow> take(m, upt(i,n)) = upt(i,i#+m)"
apply (induct_tac "m")
@@ -1126,6 +1145,7 @@
apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
apply auto
done
+declare take_upt [simp]
lemma map_succ_upt:
"[| m \<in> nat; n \<in> nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
@@ -1133,13 +1153,14 @@
apply (auto simp add: map_app_distrib)
done
-lemma nth_map [rule_format,simp]:
+lemma nth_map [rule_format]:
"xs:list(A) ==>
\<forall>n \<in> nat. n < length(xs) \<longrightarrow> nth(n, map(f, xs)) = f(nth(n, xs))"
apply (induct_tac "xs", simp)
apply (rule ballI)
apply (induct_tac "n", auto)
done
+declare nth_map [simp]
lemma nth_map_upt [rule_format]:
"[| m \<in> nat; n \<in> nat |] ==>
@@ -1213,13 +1234,14 @@
"sublist([x], A) = (if 0 \<in> A then [x] else [])"
by (simp add: sublist_Cons)
-lemma sublist_upt_eq_take [rule_format, simp]:
+lemma sublist_upt_eq_take [rule_format]:
"xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
apply (erule list.induct, simp)
apply (clarify )
apply (erule natE)
apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
done
+declare sublist_upt_eq_take [simp]
lemma sublist_Int_eq:
"xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"
--- a/src/ZF/Tools/inductive_package.ML Fri Nov 08 16:07:22 2019 +0000
+++ b/src/ZF/Tools/inductive_package.ML Fri Nov 08 16:07:31 2019 +0000
@@ -57,9 +57,9 @@
(*internal version, accepting terms*)
fun add_inductive_i verbose (rec_tms, dom_sum)
- raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
+ raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy0 =
let
- val ctxt = Proof_Context.init_global thy;
+ val ctxt0 = Proof_Context.init_global thy0;
val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
@@ -70,7 +70,7 @@
val dummy = rec_hds |> forall (fn t => is_Const t orelse
error ("Recursive set not previously declared as constant: " ^
- Syntax.string_of_term ctxt t));
+ Syntax.string_of_term ctxt0 t));
(*Now we know they are all Consts, so get their names, type and params*)
val rec_names = map (#1 o dest_Const) rec_hds
@@ -81,18 +81,18 @@
error ("Base name of recursive set not an identifier: " ^ a));
local (*Checking the introduction rules*)
- val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms;
+ val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy0) intr_tms;
fun intr_ok set =
case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
in
val dummy = intr_sets |> forall (fn t => intr_ok t orelse
error ("Conclusion of rule does not name a recursive set: " ^
- Syntax.string_of_term ctxt t));
+ Syntax.string_of_term ctxt0 t));
end;
val dummy = rec_params |> forall (fn t => is_Free t orelse
error ("Param in recursion term not a free variable: " ^
- Syntax.string_of_term ctxt t));
+ Syntax.string_of_term ctxt0 t));
(*** Construct the fixedpoint definition ***)
val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));
@@ -101,7 +101,7 @@
fun dest_tprop (Const(\<^const_name>\<open>Trueprop\<close>,_) $ P) = P
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
- Syntax.string_of_term ctxt Q);
+ Syntax.string_of_term ctxt0 Q);
(*Makes a disjunct from an introduction rule*)
fun fp_part intr = (*quantify over rule's free vars except parameters*)
@@ -142,7 +142,7 @@
If no mutual recursion then it equals the one recursive set.
If mutual recursion then it differs from all the recursive sets. *)
val big_rec_base_name = space_implode "_" rec_base_names;
- val big_rec_name = Proof_Context.intern_const ctxt big_rec_base_name;
+ val big_rec_name = Proof_Context.intern_const ctxt0 big_rec_base_name;
val _ =
@@ -163,12 +163,12 @@
(*tracing: print the fixedpoint definition*)
val dummy = if !Ind_Syntax.trace then
- writeln (cat_lines (map (Syntax.string_of_term ctxt o #2) axpairs))
+ writeln (cat_lines (map (Syntax.string_of_term ctxt0 o #2) axpairs))
else ()
(*add definitions of the inductive sets*)
val (_, thy1) =
- thy
+ thy0
|> Sign.add_path big_rec_base_name
|> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
@@ -189,13 +189,16 @@
[resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]);
- val (bnd_mono, thy2) = thy1
- |> Global_Theory.add_thm ((Binding.name "bnd_mono", bnd_mono0), [])
+ val dom_subset0 = Drule.export_without_context (big_rec_def RS Fp.subs);
- val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
+ val ([bnd_mono, dom_subset], thy2) = thy1
+ |> Global_Theory.add_thms
+ [((Binding.name "bnd_mono", bnd_mono0), []),
+ ((Binding.name "dom_subset", dom_subset0), [])];
val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski);
+
(********)
val dummy = writeln " Proving the introduction rules...";
@@ -337,7 +340,7 @@
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
If the premises get simplified, then the proofs could fail.*)
val min_ss =
- (empty_simpset (Proof_Context.init_global thy4)
+ (empty_simpset ctxt4
|> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt))
setSolver (mk_solver "minimal"
(fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
@@ -513,18 +516,18 @@
val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (pred_var $ _) = Thm.concl_of induct0
- val induct =
- CP.split_rule_var (Proof_Context.init_global thy4)
+ val induct0 =
+ CP.split_rule_var ctxt4
(pred_var, elem_type-->FOLogic.oT, induct0)
|> Drule.export_without_context
- and mutual_induct = CP.remove_split (Proof_Context.init_global thy4) mutual_induct_fsplit
+ and mutual_induct = CP.remove_split ctxt4 mutual_induct_fsplit
- val ([induct', mutual_induct'], thy') =
+ val ([induct, mutual_induct], thy5) =
thy4
- |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
+ |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct0),
[case_names, Induct.induct_pred big_rec_name]),
((Binding.name "mutual_induct", mutual_induct), [case_names])];
- in ((induct', mutual_induct'), thy')
+ in ((induct, mutual_induct), thy5)
end; (*of induction_rules*)
val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct)
@@ -534,28 +537,27 @@
else
thy4
|> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
- |> apfst (hd #> pair @{thm TrueI})
- and defs = big_rec_def :: part_rec_defs
+ |> apfst (hd #> pair @{thm TrueI});
- val (([dom_subset', elim'], [defs']), thy6) =
+ val (([cases], [defs]), thy6) =
thy5
|> IndCases.declare big_rec_name make_cases
|> Global_Theory.add_thms
- [((Binding.name "dom_subset", dom_subset), []),
- ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
- ||>> (Global_Theory.add_thmss o map Thm.no_attributes) [(Binding.name "defs", defs)];
- val (intrs', thy7) =
+ [((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
+ ||>> (Global_Theory.add_thmss o map Thm.no_attributes)
+ [(Binding.name "defs", big_rec_def :: part_rec_defs)];
+ val (named_intrs, thy7) =
thy6
|> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs) ~~ map #2 intr_specs)
||> Sign.parent_path;
in
(thy7,
- {defs = defs',
+ {defs = defs,
bnd_mono = bnd_mono,
- dom_subset = dom_subset',
- intrs = intrs',
- elim = elim',
+ dom_subset = dom_subset,
+ intrs = named_intrs,
+ elim = cases,
induct = induct,
mutual_induct = mutual_induct})
end;
--- a/src/ZF/Tools/primrec_package.ML Fri Nov 08 16:07:22 2019 +0000
+++ b/src/ZF/Tools/primrec_package.ML Fri Nov 08 16:07:31 2019 +0000
@@ -8,8 +8,8 @@
signature PRIMREC_PACKAGE =
sig
- val primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
- val primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
+ val primrec: ((binding * string) * Token.src list) list -> theory -> thm list * theory
+ val primrec_i: ((binding * term) * attribute list) list -> theory -> thm list * theory
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -173,20 +173,19 @@
|> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)];
val rewrites = def_thm :: map (mk_meta_eq o Thm.transfer thy1) (#rec_rewrites con_info)
- val eqn_thms =
+ val eqn_thms0 =
eqn_terms |> map (fn t =>
Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
(fn {context = ctxt, ...} =>
EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt @{thms refl} 1]));
-
- val (eqn_thms', thy2) =
- thy1
- |> Global_Theory.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
- val (_, thy3) =
- thy2
- |> Global_Theory.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
- ||> Sign.parent_path;
- in (thy3, eqn_thms') end;
+ in
+ thy1
+ |> Global_Theory.add_thms ((eqn_names ~~ eqn_thms0) ~~ eqn_atts)
+ |-> (fn eqn_thms =>
+ Global_Theory.add_thmss [((Binding.name "simps", eqn_thms), [Simplifier.simp_add])])
+ |>> the_single
+ ||> Sign.parent_path
+ end;
fun primrec args thy =
primrec_i (map (fn ((name, s), srcs) =>
@@ -199,7 +198,7 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>primrec\<close> "define primitive recursive functions on datatypes"
(Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
- >> (Toplevel.theory o (#1 oo (primrec o map (fn ((x, y), z) => ((x, z), y))))));
+ >> (Toplevel.theory o (#2 oo (primrec o map (fn ((x, y), z) => ((x, z), y))))));
end;