# HG changeset patch # User paulson # Date 1636631485 0 # Node ID bae4731cba8f06a363d02733200bbb325d4cf58b # Parent 95643a0bff4950dcc36f8ba2bdc2189cbd6bf91a# Parent 329cb9e6b184337d723bfec8a6f86f2156c774a3 Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO diff -r 329cb9e6b184 -r bae4731cba8f src/HOL/Eisbach/Example_Metric.thy --- 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 \An Eisbach implementation of the method @{method metric}. Slower than the Isabelle/ML implementation but arguably more readable.\ +declare [[argo_timeout = 20]] + method dist_refl_sym = simp only: simp_thms dist_commute dist_self method lin_real_arith uses thms = argo thms diff -r 329cb9e6b184 -r bae4731cba8f src/HOL/HOL.thy --- 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 \Other simple lemmas and lemma duplicates\ +lemma eq_iff_swap: "(x = y \ P) \ (y = x \ P)" +by blast + lemma all_cong1: "(\x. P x = P' x) \ (\x. P x) = (\x. P' x)" by auto diff -r 329cb9e6b184 -r bae4731cba8f src/HOL/List.thy --- 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 = [] \ xs = [] \ (\x. xs = [x])" by (cases xs) auto -lemma Nil_tl: "[] = tl xs \ xs = [] \ (\x. xs = [x])" -by (cases xs) auto +lemmas Nil_tl = tl_Nil[THEN eq_iff_swap] lemma length_induct: "(\xs. \ys. length ys < length xs \ P ys \ P xs) \ P xs" @@ -847,9 +846,7 @@ lemma length_Suc_conv: "(length xs = Suc n) = (\y ys. xs = y # ys \ length ys = n)" by (induct xs) auto -lemma Suc_length_conv: - "(Suc n = length xs) = (\y ys. xs = y # ys \ 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 \ length xs) = (\x ys. xs = x # ys \ n \ length ys)" @@ -924,14 +921,12 @@ lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \ ys = [])" by (induct xs) auto -lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \ 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 \ 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 \ [] \ 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) = (\z zs. xs = z#zs \ f z = y \ 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 = []) = (\xs \ set xss. xs = [])" by (induct xss) auto -lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\xs \ 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) = (\x\set xs. set x)" by (induct xs) auto @@ -1555,6 +1545,8 @@ lemma filter_empty_conv: "(filter P xs = []) = (\x\set xs. \ 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) = (\x\set xs. P x)" proof (induct xs) case (Cons x xs) @@ -1654,10 +1646,7 @@ (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)" by(auto dest:filter_eq_ConsD) -lemma Cons_eq_filter_iff: - "(x#xs = filter P ys) = - (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ 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 \ length xs \ n" by (metis length_take min.order_iff take_all) -lemma drop_all_iff [simp]: "drop n xs = [] \ length xs \ 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 \ 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 = [] \ length xs \ 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 \ xs = [])" - by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split) - -lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs \ 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 \ (\us vs. xs = us @ vs \ ys = map f us \ 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 = [] \ xs = [] \ 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] = [] \ j < i" by (simp add: upto.simps) -lemma upto_Nil2[simp]: "[] = [i..j] \ j < i" -by (simp add: upto.simps) +lemmas upto_Nil2[simp] = upto_Nil[THEN eq_iff_swap] lemma upto_rec1: "i \ j \ [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) \ length xs" by (induct xs) auto @@ -4546,8 +4539,7 @@ lemma replicate_empty[simp]: "(replicate n x = []) \ n=0" by (induct n) auto -lemma empty_replicate[simp]: "([] = replicate n x) \ 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) \ (m=n \ (m\0 \ x=y))" diff -r 329cb9e6b184 -r bae4731cba8f src/HOL/SMT.thy --- 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 \ The option \smt_read_only_certificates\ 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 \true\, no SMT solver will ever be invoked and only the existing certificates found in the configured cache are used; when set to \false\ and there is no cached diff -r 329cb9e6b184 -r bae4731cba8f src/HOL/Tools/Mirabelle/mirabelle.ML --- 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>\mirabelle_stride\; val mirabelle_max_calls = Options.default_int \<^system_option>\mirabelle_max_calls\; val mirabelle_theories = Options.default_string \<^system_option>\mirabelle_theories\; - val mirabelle_output_dir = Options.default_string \<^system_option>\mirabelle_output_dir\ - |> Path.explode - |> Isabelle_System.make_directory; + val mirabelle_output_dir = Options.default_string \<^system_option>\mirabelle_output_dir\; 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}; diff -r 329cb9e6b184 -r bae4731cba8f src/HOL/Tools/Mirabelle/mirabelle.scala --- 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 _ => diff -r 329cb9e6b184 -r bae4731cba8f src/Pure/Thy/document_build.scala --- 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)) diff -r 329cb9e6b184 -r bae4731cba8f src/Pure/Thy/latex.scala --- 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 }