Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO
authorpaulson <lp15@cam.ac.uk>
Thu, 11 Nov 2021 11:51:25 +0000
changeset 74750 bae4731cba8f
parent 74748 95643a0bff49 (diff)
parent 74749 329cb9e6b184 (current diff)
child 74757 2e3b649111f1
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
   }