Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO
--- a/src/HOL/Eisbach/Example_Metric.thy Tue Nov 09 16:04:11 2021 +0000
+++ b/src/HOL/Eisbach/Example_Metric.thy Thu Nov 11 11:51:25 2021 +0000
@@ -8,6 +8,8 @@
text \<open>An Eisbach implementation of the method @{method metric}.
Slower than the Isabelle/ML implementation but arguably more readable.\<close>
+declare [[argo_timeout = 20]]
+
method dist_refl_sym = simp only: simp_thms dist_commute dist_self
method lin_real_arith uses thms = argo thms
--- a/src/HOL/HOL.thy Tue Nov 09 16:04:11 2021 +0000
+++ b/src/HOL/HOL.thy Thu Nov 11 11:51:25 2021 +0000
@@ -1678,6 +1678,9 @@
subsection \<open>Other simple lemmas and lemma duplicates\<close>
+lemma eq_iff_swap: "(x = y \<longleftrightarrow> P) \<Longrightarrow> (y = x \<longleftrightarrow> P)"
+by blast
+
lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)"
by auto
--- a/src/HOL/List.thy Tue Nov 09 16:04:11 2021 +0000
+++ b/src/HOL/List.thy Thu Nov 11 11:51:25 2021 +0000
@@ -795,8 +795,7 @@
lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (\<exists>x. xs = [x])"
by (cases xs) auto
-lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (\<exists>x. xs = [x])"
-by (cases xs) auto
+lemmas Nil_tl = tl_Nil[THEN eq_iff_swap]
lemma length_induct:
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
@@ -847,9 +846,7 @@
lemma length_Suc_conv: "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
by (induct xs) auto
-lemma Suc_length_conv:
- "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
-by (induct xs; simp; blast)
+lemmas Suc_length_conv = length_Suc_conv[THEN eq_iff_swap]
lemma Suc_le_length_iff:
"(Suc n \<le> length xs) = (\<exists>x ys. xs = x # ys \<and> n \<le> length ys)"
@@ -924,14 +921,12 @@
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
by (induct xs) auto
-lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
-by (induct xs) auto
+lemmas Nil_is_append_conv [iff] = append_is_Nil_conv[THEN eq_iff_swap]
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
by (induct xs) auto
-lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
-by (induct xs) auto
+lemmas self_append_conv [iff] = append_self_conv[THEN eq_iff_swap]
lemma append_eq_append_conv [simp]:
"length xs = length ys \<or> length us = length vs
@@ -958,8 +953,7 @@
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
using append_same_eq [of _ _ "[]"] by auto
-lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
-using append_same_eq [of "[]"] by auto
+lemmas self_append_conv2 [iff] = append_self_conv2[THEN eq_iff_swap]
lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
by (fact list.collapse)
@@ -1087,10 +1081,9 @@
by simp
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
-by (cases xs) auto
-
-lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
-by (cases xs) auto
+by (rule list.map_disc_iff)
+
+lemmas Nil_is_map_conv [iff] = map_is_Nil_conv[THEN eq_iff_swap]
lemma map_eq_Cons_conv:
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
@@ -1199,13 +1192,12 @@
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
by (induct xs) auto
-lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
-by (induct xs) auto
+lemmas Nil_is_rev_conv [iff] = rev_is_Nil_conv[THEN eq_iff_swap]
lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
by (cases xs) auto
-lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
+lemma singleton_rev_conv [simp]: "([x] = rev xs) = ([x] = xs)"
by (cases xs) auto
lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
@@ -1275,8 +1267,7 @@
lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
by (induct xs) auto
-lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
-by(induct xs) auto
+lemmas set_empty2[iff] = set_empty[THEN eq_iff_swap]
lemma set_rev [simp]: "set (rev xs) = set xs"
by (induct xs) auto
@@ -1429,8 +1420,7 @@
lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
by (induct xss) auto
-lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
- by (induct xss) auto
+lemmas Nil_eq_concat_conv [simp] = concat_eq_Nil_conv[THEN eq_iff_swap]
lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)"
by (induct xs) auto
@@ -1555,6 +1545,8 @@
lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
by (induct xs) simp_all
+lemmas empty_filter_conv = filter_empty_conv[THEN eq_iff_swap]
+
lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
proof (induct xs)
case (Cons x xs)
@@ -1654,10 +1646,7 @@
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
by(auto dest:filter_eq_ConsD)
-lemma Cons_eq_filter_iff:
- "(x#xs = filter P ys) =
- (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
- by(auto dest:Cons_eq_filterD)
+lemmas Cons_eq_filter_iff = filter_eq_Cons_iff[THEN eq_iff_swap]
lemma inj_on_filter_key_eq:
assumes "inj_on f (insert y (set xs))"
@@ -2128,9 +2117,21 @@
lemma take_all_iff [simp]: "take n xs = xs \<longleftrightarrow> length xs \<le> n"
by (metis length_take min.order_iff take_all)
-lemma drop_all_iff [simp]: "drop n xs = [] \<longleftrightarrow> length xs \<le> n"
+(* Looks like a good simp rule but can cause looping;
+ too much interaction between take and length
+lemmas take_all_iff2[simp] = take_all_iff[THEN eq_iff_swap]
+*)
+
+lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
+ by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
+
+lemmas take_eq_Nil2[simp] = take_eq_Nil[THEN eq_iff_swap]
+
+lemma drop_eq_Nil [simp]: "drop n xs = [] \<longleftrightarrow> length xs \<le> n"
by (metis diff_is_0_eq drop_all length_drop list.size(3))
+lemmas drop_eq_Nil2 [simp] = drop_eq_Nil[THEN eq_iff_swap]
+
lemma take_append [simp]:
"take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
by (induct n arbitrary: xs) (auto, case_tac xs, auto)
@@ -2178,12 +2179,6 @@
then show ?case by (cases xs) simp_all
qed
-lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
- by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
-
-lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs \<le> n)"
- by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
-
lemma take_map: "take n (map f xs) = map f (take n xs)"
proof (induct n arbitrary: xs)
case 0
@@ -2308,9 +2303,7 @@
using map_append by blast
qed
-lemma append_eq_map_conv:
- "ys @ zs = map f xs \<longleftrightarrow> (\<exists>us vs. xs = us @ vs \<and> ys = map f us \<and> zs = map f vs)"
-by (metis map_eq_append_conv)
+lemmas append_eq_map_conv = map_eq_append_conv[THEN eq_iff_swap]
lemma take_add: "take (i+j) xs = take i xs @ take j (drop i xs)"
proof (induct xs arbitrary: i)
@@ -2763,10 +2756,12 @@
from this that show ?thesis by fastforce
qed
-lemma zip_eq_Nil_iff:
+lemma zip_eq_Nil_iff[simp]:
"zip xs ys = [] \<longleftrightarrow> xs = [] \<or> ys = []"
by (cases xs; cases ys) simp_all
+lemmas Nil_eq_zip_iff[simp] = zip_eq_Nil_iff[THEN eq_iff_swap]
+
lemma zip_eq_ConsE:
assumes "zip xs ys = xy # xys"
obtains x xs' y ys' where "xs = x # xs'"
@@ -3434,8 +3429,7 @@
lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i"
by (simp add: upto.simps)
-lemma upto_Nil2[simp]: "[] = [i..j] \<longleftrightarrow> j < i"
-by (simp add: upto.simps)
+lemmas upto_Nil2[simp] = upto_Nil[THEN eq_iff_swap]
lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
by(simp add: upto.simps)
@@ -3601,8 +3595,7 @@
lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
by (induct x, auto)
-lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
-by (induct x, auto)
+lemmas remdups_eq_nil_right_iff [simp] = remdups_eq_nil_iff[THEN eq_iff_swap]
lemma length_remdups_leq[iff]: "length(remdups xs) \<le> length xs"
by (induct xs) auto
@@ -4546,8 +4539,7 @@
lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
by (induct n) auto
-lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
-by (induct n) auto
+lemmas empty_replicate[simp] = replicate_empty[THEN eq_iff_swap]
lemma replicate_eq_replicate[simp]:
"(replicate m x = replicate n y) \<longleftrightarrow> (m=n \<and> (m\<noteq>0 \<longrightarrow> x=y))"
--- a/src/HOL/SMT.thy Tue Nov 09 16:04:11 2021 +0000
+++ b/src/HOL/SMT.thy Thu Nov 11 11:51:25 2021 +0000
@@ -736,7 +736,7 @@
text \<open>
The option \<open>smt_read_only_certificates\<close> controls whether only
-stored certificates are should be used or invocation of an SMT solver
+stored certificates should be used or invocation of an SMT solver
is allowed. When set to \<open>true\<close>, no SMT solver will ever be
invoked and only the existing certificates found in the configured
cache are used; when set to \<open>false\<close> and there is no cached
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Tue Nov 09 16:04:11 2021 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Nov 11 11:51:25 2021 +0000
@@ -97,10 +97,8 @@
if Exn.is_interrupt exn then Exn.reraise exn
else print_exn exn;
-fun make_action_string ({index, label, name, ...} : action_context) =
- if label = "" then string_of_int index ^ "." ^ name else label;
-
-val make_action_path = Path.basic o make_action_string;
+fun make_action_path ({index, label, name, ...} : action_context) =
+ Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);
fun finalize_action ({finalize, ...} : action) context =
let
@@ -108,8 +106,6 @@
val action_path = make_action_path context;
val export_name =
Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize");
- val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log")
- (prefix_lines (make_action_string context ^ " finalize ") (YXML.content_of s) ^ "\n")
in
if s <> "" then
Export.export \<^theory> export_name [XML.Text s]
@@ -128,13 +124,6 @@
Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path +
line_path + offset_path);
val s = run_action_function (fn () => run_action command);
- val prefix = make_action_string context ^ " goal." ^ StringCvt.padRight #" " 6 (#name command) ^
- Context.theory_long_name thy ^ " " ^
- string_of_int (the (Position.line_of pos)) ^ ":" ^
- string_of_int (the (Position.offset_of pos)) ^ " "
- val _ = Substring.triml
- val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log")
- (prefix_lines prefix (YXML.content_of s) ^ "\n")
in
if s <> "" then
Export.export thy export_name [XML.Text s]
@@ -203,9 +192,7 @@
val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>;
val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>;
val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
- val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>
- |> Path.explode
- |> Isabelle_System.make_directory;
+ val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>;
val check_theory = check_theories (space_explode "," mirabelle_theories);
fun make_commands (thy_index, (thy, segments)) =
@@ -239,7 +226,8 @@
SOME f => f
| NONE => error "Unknown action");
val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label;
- val output_dir = Path.append mirabelle_output_dir (Path.basic action_subdir);
+ val output_dir =
+ Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir);
val context =
{index = n, label = label, name = name, arguments = args,
timeout = mirabelle_timeout, output_dir = output_dir};
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Nov 09 16:04:11 2021 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Nov 11 11:51:25 2021 +0000
@@ -68,12 +68,10 @@
progress.echo("Running Mirabelle ...")
- val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs)
val store = Sessions.store(build_options)
def session_setup(session_name: String, session: Session): Unit =
{
- val session_hierarchy = structure.hierarchy(session_name)
session.all_messages +=
Session.Consumer[Prover.Message]("mirabelle_export") {
case msg: Prover.Protocol_Output =>
@@ -83,23 +81,19 @@
progress.echo(
"Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")")
}
- using(store.open_database_context())(db_context =>
- {
- for (entry <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
- val prefix =
- Export.explode_name(args.name) match {
- case List("mirabelle", action, "finalize") => action + " finalize "
- case List("mirabelle", action, "goal", goal_name, line, offset) =>
- action + " goal." + goal_name + " " + args.theory_name + " " +
- line + ":" + offset + " "
- case _ => ""
- }
- val lines = Pretty.string_of(entry.uncompressed_yxml).trim()
- val body = Library.prefix_lines(prefix, lines) + "\n"
- val log_file = output_dir + Path.basic("mirabelle.log")
- File.append(log_file, body)
+ val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = store.cache)
+ val lines = Pretty.string_of(yxml).trim()
+ val prefix =
+ Export.explode_name(args.name) match {
+ case List("mirabelle", action, "finalize") => action + " finalize "
+ case List("mirabelle", action, "goal", goal_name, line, offset) =>
+ action + " goal." + goal_name + " " + args.theory_name + " " +
+ line + ":" + offset + " "
+ case _ => ""
}
- })
+ val body = Library.prefix_lines(prefix, lines) + "\n"
+ val log_file = output_dir + Path.basic("mirabelle.log")
+ File.append(log_file, body)
case _ =>
}
case _ =>
--- a/src/Pure/Thy/document_build.scala Tue Nov 09 16:04:11 2021 +0000
+++ b/src/Pure/Thy/document_build.scala Thu Nov 11 11:51:25 2021 +0000
@@ -253,11 +253,10 @@
def prepare_directory(dir: Path, doc: Document_Variant): Directory =
{
- val doc_dir = dir + Path.basic(doc.name)
- Isabelle_System.make_directory(doc_dir)
+ val doc_dir = Isabelle_System.make_directory(dir + Path.basic(doc.name))
- /* sources */
+ /* actual sources: with SHA1 digest */
isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir))
doc.isabelletags.write(doc_dir)
@@ -277,7 +276,7 @@
val sources = SHA1.digest_set(digests1 ::: digests2)
- /* derived material (without SHA1 digest) */
+ /* derived material: without SHA1 digest */
isabelle_logo.foreach(_.write(doc_dir))
--- a/src/Pure/Thy/latex.scala Tue Nov 09 16:04:11 2021 +0000
+++ b/src/Pure/Thy/latex.scala Thu Nov 11 11:51:25 2021 +0000
@@ -10,6 +10,7 @@
import java.io.{File => JFile}
import scala.annotation.tailrec
+import scala.collection.mutable
import scala.util.matching.Regex
@@ -21,14 +22,16 @@
def output(latex_text: Text, file_pos: String = ""): String =
{
- def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%"
+ var line = 1
+ val result = new mutable.ListBuffer[String]
+ val positions = new mutable.ListBuffer[String]
- var positions: List[String] =
- if (file_pos.isEmpty) Nil
- else List(position(Markup.FILE, file_pos), "\\endinput")
+ def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%\n"
- var line = 1
- var result = List.empty[String]
+ if (file_pos.nonEmpty) {
+ positions += "\\endinput\n"
+ positions += position(Markup.FILE, file_pos)
+ }
def traverse(body: XML.Body): Unit =
{
@@ -38,18 +41,19 @@
if (markup.name == Markup.DOCUMENT_LATEX) {
for { l <- Position.Line.unapply(markup.properties) if positions.nonEmpty } {
val s = position(Value.Int(line), Value.Int(l))
- if (positions.head != s) positions ::= s
+ if (positions.last != s) positions += s
}
traverse(body)
}
case XML.Text(s) =>
line += s.count(_ == '\n')
- result ::= s
+ result += s
}
}
traverse(latex_text)
- result.reverse.mkString + cat_lines(positions.reverse)
+ result ++= positions
+ result.mkString
}