--- a/Admin/components/components.sha1 Sun Dec 12 10:42:51 2021 +0100
+++ b/Admin/components/components.sha1 Sun Dec 12 11:18:42 2021 +0100
@@ -274,6 +274,8 @@
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz
810ee0f35adada9bf970c33fd80b986ab2255bf3 naproche-20210201.tar.gz
+37bb6d934cfaf157efcadb349a0244d145ce15b0 naproche-20211211.tar.gz
+d098dd0873b1720a77dc4e060267f9a6c93f341a naproche-2d99afe5c349.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
9c02ecf93863c3289002c5e5ac45a83e2505984c naproche-755224402e36.tar.gz
--- a/CONTRIBUTORS Sun Dec 12 10:42:51 2021 +0100
+++ b/CONTRIBUTORS Sun Dec 12 11:18:42 2021 +0100
@@ -3,6 +3,10 @@
listed as an author in one of the source files of this Isabelle distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
+
Contributions to Isabelle2021-1
-------------------------------
--- a/NEWS Sun Dec 12 10:42:51 2021 +0100
+++ b/NEWS Sun Dec 12 11:18:42 2021 +0100
@@ -4,6 +4,37 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
+New in this Isabelle version
+----------------------------
+
+*** General ***
+
+* Old-style {* verbatim *} tokens have been discontinued (legacy feature
+since Isabelle2019). INCOMPATIBILITY, use \<open>cartouche\<close> syntax instead.
+
+
+*** HOL ***
+
+* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
+ type class preorder.
+
+* Theory "HOL-Library.Multiset":
+ - Consolidated operation and fact names.
+ multp ~> multp_code
+ multeqp ~> multeqp_code
+ multp_cancel_add_mset ~> multp_cancel_add_mset0
+ multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
+ multp_code_iff ~> multp_code_iff_mult
+ multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
+ Minor INCOMPATIBILITY.
+ - Moved mult1_lessE out of preorder type class and add explicit
+ assumption. Minor INCOMPATIBILITY.
+ - Added predicate multp equivalent to set mult. Reuse name previously
+ used for what is now called multp_code. Minor INCOMPATIBILITY.
+ - Lifted multiple lemmas from mult to multp.
+ - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
+
+
New in Isabelle2021-1 (December 2021)
-------------------------------------
--- a/lib/texinputs/isabelle.sty Sun Dec 12 10:42:51 2021 +0100
+++ b/lib/texinputs/isabelle.sty Sun Dec 12 11:18:42 2021 +0100
@@ -140,8 +140,6 @@
\chardef\isacharbar=`\|%
\chardef\isacharbraceright=`\}%
\chardef\isachartilde=`\~%
-\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
-\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
\def\isacartoucheopen{\isatext{\guilsinglleft}}%
\def\isacartoucheclose{\isatext{\guilsinglright}}%
}
--- a/src/Doc/Implementation/Logic.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Doc/Implementation/Logic.thy Sun Dec 12 11:18:42 2021 +0100
@@ -217,10 +217,10 @@
\<^rail>\<open>
@{syntax_def type_const}: @{syntax name} (@{syntax embedded_ml}*)
;
- @{syntax_def type_const_fn}: @{syntax type_const} @'=>' @{syntax embedded}
+ @{syntax_def type_const_fn}: @{syntax type_const} @'=>' @{syntax embedded_ml}
;
- @{syntax_def embedded_ml}: @{syntax embedded} |
- @{syntax control_symbol} @{syntax embedded} | @'_'
+ @{syntax_def embedded_ml}:
+ @'_' | @{syntax embedded} | @{syntax control_symbol} @{syntax embedded}
\<close>
The text provided as @{syntax embedded_ml} is treated as regular Isabelle/ML
@@ -491,9 +491,10 @@
@{syntax_def term_const}:
@{syntax name} (@{syntax embedded_ml}*) (@{syntax for_args})?
;
- @{syntax_def term_const_fn}: @{ syntax term_const} @'=>' @{syntax embedded}
+ @{syntax_def term_const_fn}:
+ @{syntax term_const} @'=>' @{syntax embedded_ml}
;
- @{syntax_def for_args}: @'for' (@{syntax embedded_ml}*)
+ @{syntax_def for_args}: @'for' (@{syntax embedded_ml}+)
\<close>
\<close>
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Dec 12 11:18:42 2021 +0100
@@ -234,12 +234,11 @@
text \<open>
A chunk of document @{syntax text} is usually given as @{syntax cartouche}
- \<open>\<open>\<dots>\<close>\<close> or @{syntax verbatim}, i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>. For
- convenience, any of the smaller text unit that conforms to @{syntax name} is
- admitted as well.
+ \<open>\<open>\<dots>\<close>\<close>. For convenience, any of the smaller text unit that conforms to
+ @{syntax name} is admitted as well.
\<^rail>\<open>
- @{syntax_def text}: @{syntax embedded} | @{syntax verbatim}
+ @{syntax_def text}: @{syntax embedded}
\<close>
Typical uses are document markup commands, like \<^theory_text>\<open>chapter\<close>, \<^theory_text>\<open>section\<close> etc.
--- a/src/Doc/Tutorial/ToyList/ToyList.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Sun Dec 12 11:18:42 2021 +0100
@@ -107,7 +107,7 @@
When Isabelle prints a syntax error message, it refers to the HOL syntax as
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
-Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}.
+Comments\index{comment} must be in enclosed in \texttt{(*}and\texttt{*)}.
\section{Evaluation}
\index{evaluation}
--- a/src/HOL/ATP.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/ATP.thy Sun Dec 12 11:18:42 2021 +0100
@@ -7,7 +7,7 @@
section \<open>Automatic Theorem Provers (ATPs)\<close>
theory ATP
- imports Meson
+ imports Meson Hilbert_Choice
begin
subsection \<open>ATP problems and proofs\<close>
@@ -50,6 +50,9 @@
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
"fequal x y \<longleftrightarrow> (x = y)"
+definition fChoice :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
+ "fChoice \<equiv> Hilbert_Choice.Eps"
+
lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
unfolding fFalse_def fTrue_def by simp
@@ -130,6 +133,16 @@
"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
unfolding fFalse_def fTrue_def fequal_def by auto
+lemma fChoice_iff_Ex: "P (fChoice P) \<longleftrightarrow> HOL.Ex P"
+ unfolding fChoice_def
+ by (fact some_eq_ex)
+
+text \<open>
+We use the @{const HOL.Ex} constant on the right-hand side of @{thm [source] fChoice_iff_Ex} because
+we want to use the TPTP-native version if fChoice is introduced in a logic that supports FOOL.
+In logics that don't support it, it gets replaced by fEx during processing.
+Notice that we cannot use @{term "\<exists>x. P x"}, as existentials are not skolimized by the metis proof
+method but @{term "Ex P"} is eta-expanded if FOOL is supported.\<close>
subsection \<open>Basic connection between ATPs and HOL\<close>
--- a/src/HOL/BNF_Def.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/BNF_Def.thy Sun Dec 12 11:18:42 2021 +0100
@@ -139,7 +139,7 @@
lemma pick_middlep:
"(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
- unfolding pick_middlep_def apply(rule someI_ex) by auto
+ unfolding pick_middlep_def by (rule someI_ex) auto
definition fstOp where
"fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"
--- a/src/HOL/Bali/Term.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Bali/Term.thy Sun Dec 12 11:18:42 2021 +0100
@@ -110,7 +110,7 @@
| UNot \<comment> \<open>{\tt !} logical complement\<close>
\<comment> \<open>function codes for binary operations\<close>
-datatype binop = Mul \<comment> \<open>{\tt * } multiplication\<close>
+datatype binop = Mul \<comment> \<open>{\tt *} multiplication\<close>
| Div \<comment> \<open>{\tt /} division\<close>
| Mod \<comment> \<open>{\tt \%} remainder\<close>
| Plus \<comment> \<open>{\tt +} addition\<close>
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Sun Dec 12 11:18:42 2021 +0100
@@ -920,7 +920,7 @@
assumes "is_unit x"
shows "infinite {n. x^n dvd y}"
proof -
- from `is_unit x` have "is_unit (x^n)" for n
+ from \<open>is_unit x\<close> have "is_unit (x^n)" for n
using is_unit_power_iff by auto
hence "x^n dvd y" for n
by auto
@@ -2181,7 +2181,7 @@
using is_unit_power_iff by simp
hence "p^k dvd x"
by auto
- moreover from `is_unit p` have "p^k dvd p^multiplicity p x"
+ moreover from \<open>is_unit p\<close> have "p^k dvd p^multiplicity p x"
using multiplicity_unit_left is_unit_power_iff by simp
ultimately show ?thesis by simp
next
@@ -2194,16 +2194,16 @@
moreover have "p^k dvd x \<Longrightarrow> k = 0"
proof (rule ccontr)
assume "p^k dvd x" and "k \<noteq> 0"
- with `p = 0` have "p^k = 0" by auto
- with `p^k dvd x` have "0 dvd x" by auto
+ with \<open>p = 0\<close> have "p^k = 0" by auto
+ with \<open>p^k dvd x\<close> have "0 dvd x" by auto
hence "x = 0" by auto
- with `x \<noteq> 0` show False by auto
+ with \<open>x \<noteq> 0\<close> show False by auto
qed
ultimately show ?thesis
- by (auto simp add: is_unit_power_iff `\<not> is_unit p`)
+ by (auto simp add: is_unit_power_iff \<open>\<not> is_unit p\<close>)
next
case False
- with `x \<noteq> 0` `\<not> is_unit p` show ?thesis
+ with \<open>x \<noteq> 0\<close> \<open>\<not> is_unit p\<close> show ?thesis
by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power)
qed
qed
--- a/src/HOL/Deriv.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Deriv.thy Sun Dec 12 11:18:42 2021 +0100
@@ -1611,7 +1611,7 @@
and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
obtains \<xi> where "a < \<xi>" "\<xi> < b" "f b - f a = (f' \<xi>) (b - a)"
proof -
- have "\<exists>x. a < x \<and> x < b \<and> (\<lambda>y. f' x y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)"
+ have "\<exists>\<xi>. a < \<xi> \<and> \<xi> < b \<and> (\<lambda>y. f' \<xi> y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)"
proof (intro Rolle_deriv[OF \<open>a < b\<close>])
fix x
assume x: "a < x" "x < b"
@@ -1619,12 +1619,8 @@
has_derivative (\<lambda>y. f' x y - (f b - f a) / (b - a) * y)) (at x)"
by (intro derivative_intros derf[OF x])
qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
- then obtain \<xi> where
- "a < \<xi>" "\<xi> < b" "(\<lambda>y. f' \<xi> y - (f b - f a) / (b - a) * y) = (\<lambda>v. 0)"
- by metis
then show ?thesis
- by (metis (no_types, opaque_lifting) that add.right_neutral add_diff_cancel_left' add_diff_eq \<open>a < b\<close>
- less_irrefl nonzero_eq_divide_eq)
+ by (smt (verit, ccfv_SIG) pos_le_divide_eq pos_less_divide_eq that)
qed
theorem MVT:
--- a/src/HOL/Eisbach/match_method.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Eisbach/match_method.ML Sun Dec 12 11:18:42 2021 +0100
@@ -95,7 +95,7 @@
else
let val b = #1 (the opt_dyn)
in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) --
- Scan.lift (for_fixes -- (\<^keyword>\<open>\<Rightarrow>\<close> |-- Parse.token Parse.text))
+ Scan.lift (for_fixes -- (\<^keyword>\<open>\<Rightarrow>\<close> |-- Parse.token Parse.embedded))
>> (fn ((ctxt, ts), (fixes, body)) =>
(case Token.get_value body of
SOME (Token.Source src) =>
--- a/src/HOL/Equiv_Relations.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Equiv_Relations.thy Sun Dec 12 11:18:42 2021 +0100
@@ -368,7 +368,7 @@
have eqv: "equiv S ?r"
unfolding relation_of_def by (auto intro: comp_equivI)
have finite: "C \<in> S//?r \<Longrightarrow> finite C" for C
- by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]])
+ by (fact finite_equiv_class[OF \<open>finite S\<close> equiv_type[OF \<open>equiv S ?r\<close>]])
have disjoint: "A \<in> S//?r \<Longrightarrow> B \<in> S//?r \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}" for A B
using eqv quotient_disj by blast
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Rewrite_Examples.thy Sun Dec 12 11:18:42 2021 +0100
@@ -0,0 +1,301 @@
+theory Rewrite_Examples
+imports Main "HOL-Library.Rewrite"
+begin
+
+section \<open>The rewrite Proof Method by Example\<close>
+
+text\<open>
+This theory gives an overview over the features of the pattern-based rewrite proof method.
+
+Documentation: @{url "https://arxiv.org/abs/2111.04082"}
+\<close>
+
+lemma
+ fixes a::int and b::int and c::int
+ assumes "P (b + a)"
+ shows "P (a + b)"
+by (rewrite at "a + b" add.commute)
+ (rule assms)
+
+(* Selecting a specific subterm in a large, ambiguous term. *)
+lemma
+ fixes a b c :: int
+ assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c"
+ shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+ by (rewrite in "f _ + f \<hole> = _" diff_self) fact
+
+lemma
+ fixes a b c :: int
+ assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
+ shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+ by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact
+
+lemma
+ fixes a b c :: int
+ assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c"
+ shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+ by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact
+
+lemma
+ fixes a b c :: int
+ assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
+ shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+ by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact
+
+lemma
+ fixes x y :: nat
+ shows"x + y > c \<Longrightarrow> y + x > c"
+ by (rewrite at "\<hole> > c" add.commute) assumption
+
+(* We can also rewrite in the assumptions. *)
+lemma
+ fixes x y :: nat
+ assumes "y + x > c \<Longrightarrow> y + x > c"
+ shows "x + y > c \<Longrightarrow> y + x > c"
+ by (rewrite in asm add.commute) fact
+
+lemma
+ fixes x y :: nat
+ assumes "y + x > c \<Longrightarrow> y + x > c"
+ shows "x + y > c \<Longrightarrow> y + x > c"
+ by (rewrite in "x + y > c" at asm add.commute) fact
+
+lemma
+ fixes x y :: nat
+ assumes "y + x > c \<Longrightarrow> y + x > c"
+ shows "x + y > c \<Longrightarrow> y + x > c"
+ by (rewrite at "\<hole> > c" at asm add.commute) fact
+
+lemma
+ assumes "P {x::int. y + 1 = 1 + x}"
+ shows "P {x::int. y + 1 = x + 1}"
+ by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact
+
+lemma
+ assumes "P {x::int. y + 1 = 1 + x}"
+ shows "P {x::int. y + 1 = x + 1}"
+ by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute)
+ fact
+
+lemma
+ assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
+ shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
+ by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
+
+(* This is not limited to the first assumption *)
+lemma
+ assumes "PROP P \<equiv> PROP Q"
+ shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
+ by (rewrite at asm assms)
+
+lemma
+ assumes "PROP P \<equiv> PROP Q"
+ shows "PROP R \<Longrightarrow> PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
+ by (rewrite at asm assms)
+
+(* Rewriting "at asm" selects each full assumption, not any parts *)
+lemma
+ assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)"
+ shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R"
+ apply (rewrite at asm assms)
+ apply assumption
+ done
+
+
+
+(* Rewriting with conditional rewriting rules works just as well. *)
+lemma test_theorem:
+ fixes x :: nat
+ shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
+ by (rule Orderings.order_antisym)
+
+(* Premises of the conditional rule yield new subgoals. The
+ assumptions of the goal are propagated into these subgoals
+*)
+lemma
+ fixes f :: "nat \<Rightarrow> nat"
+ shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
+ apply (rewrite at "f x" to "0" test_theorem)
+ apply assumption
+ apply assumption
+ apply (rule refl)
+ done
+
+(* This holds also for rewriting in assumptions. The order of assumptions is preserved *)
+lemma
+ assumes rewr: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP R \<equiv> PROP R'"
+ assumes A1: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP P"
+ assumes A2: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP Q"
+ assumes C: "PROP S \<Longrightarrow> PROP R' \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
+ shows "PROP S \<Longrightarrow> PROP R \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
+ apply (rewrite at asm rewr)
+ apply (fact A1)
+ apply (fact A2)
+ apply (fact C)
+ done
+
+
+(*
+ Instantiation.
+
+ Since all rewriting is now done via conversions,
+ instantiation becomes fairly easy to do.
+*)
+
+(* We first introduce a function f and an extended
+ version of f that is annotated with an invariant. *)
+fun f :: "nat \<Rightarrow> nat" where "f n = n"
+definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n"
+
+lemma annotate_f: "f = f_inv I"
+ by (simp add: f_inv_def fun_eq_iff)
+
+(* We have a lemma with a bound variable n, and
+ want to add an invariant to f. *)
+lemma
+ assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x"
+ shows "P (\<lambda>n. f n + 1) = x"
+ by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact
+
+(* We can also add an invariant that contains the variable n bound in the outer context.
+ For this, we need to bind this variable to an identifier. *)
+lemma
+ assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
+ shows "P (\<lambda>n. f n + 1) = x"
+ by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
+
+(* Any identifier will work *)
+lemma
+ assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
+ shows "P (\<lambda>n. f n + 1) = x"
+ by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
+
+(* The "for" keyword. *)
+lemma
+ assumes "P (2 + 1)"
+ shows "\<And>x y. P (1 + 2 :: nat)"
+by (rewrite in "P (1 + 2)" at for (x) add.commute) fact
+
+lemma
+ assumes "\<And>x y. P (y + x)"
+ shows "\<And>x y. P (x + y :: nat)"
+by (rewrite in "P (x + _)" at for (x y) add.commute) fact
+
+lemma
+ assumes "\<And>x y z. y + x + z = z + y + (x::int)"
+ shows "\<And>x y z. x + y + z = z + y + (x::int)"
+by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact
+
+lemma
+ assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
+ shows "\<And>x y z. x + y + z = z + y + (x::int)"
+by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact
+
+lemma
+ assumes "\<And>x y z. x + y + z = y + z + (x::int)"
+ shows "\<And>x y z. x + y + z = z + y + (x::int)"
+by (rewrite at "\<hole> + _" at "_ = \<hole>" in for () add.commute) fact
+
+lemma
+ assumes eq: "\<And>x. P x \<Longrightarrow> g x = x"
+ assumes f1: "\<And>x. Q x \<Longrightarrow> P x"
+ assumes f2: "\<And>x. Q x \<Longrightarrow> x"
+ shows "\<And>x. Q x \<Longrightarrow> g x"
+ apply (rewrite at "g x" in for (x) eq)
+ apply (fact f1)
+ apply (fact f2)
+ done
+
+(* The for keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
+lemma
+ assumes "(\<And>(x::int). x < 1 + x)"
+ and "(x::int) + 1 > x"
+ shows "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x"
+by (rewrite at "x + 1" in for (x) at asm add.commute)
+ (rule assms)
+
+(* The rewrite method also has an ML interface *)
+lemma
+ assumes "\<And>a b. P ((a + 1) * (1 + b)) "
+ shows "\<And>a b :: nat. P ((a + 1) * (b + 1))"
+ apply (tactic \<open>
+ let
+ val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
+ (* Note that the pattern order is reversed *)
+ val pat = [
+ Rewrite.For [(x, SOME \<^Type>\<open>nat\<close>)],
+ Rewrite.In,
+ Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>nat\<close> for \<open>Free (x, \<^Type>\<open>nat\<close>)\<close> \<^term>\<open>1 :: nat\<close>\<close>, [])]
+ val to = NONE
+ in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
+ \<close>)
+ apply (fact assms)
+ done
+
+lemma
+ assumes "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. a + b))"
+ shows "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))"
+ apply (tactic \<open>
+ let
+ val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
+ val pat = [
+ Rewrite.Concl,
+ Rewrite.In,
+ Rewrite.Term (Free ("Q", (\<^Type>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^Type>\<open>bool\<close>)
+ $ Abs ("x", \<^Type>\<open>int\<close>, Rewrite.mk_hole 1 (\<^Type>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^Type>\<open>int\<close>)]),
+ Rewrite.In,
+ Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Free (x, \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
+ ]
+ val to = NONE
+ in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
+ \<close>)
+ apply (fact assms)
+ done
+
+(* There is also conversion-like rewrite function: *)
+ML \<open>
+ val ct = \<^cprop>\<open>Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))\<close>
+ val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
+ val pat = [
+ Rewrite.Concl,
+ Rewrite.In,
+ Rewrite.Term (Free ("Q", (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^typ>\<open>bool\<close>)
+ $ Abs ("x", \<^typ>\<open>int\<close>, Rewrite.mk_hole 1 (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>\<open>int\<close>)]),
+ Rewrite.In,
+ Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Free (x, \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
+ ]
+ val to = NONE
+ val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
+\<close>
+
+text \<open>Some regression tests\<close>
+
+ML \<open>
+ val ct = \<^cterm>\<open>(\<lambda>b :: int. (\<lambda>a. b + a))\<close>
+ val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
+ val pat = [
+ Rewrite.In,
+ Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
+ ]
+ val to = NONE
+ val _ =
+ case try (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) ct of
+ NONE => ()
+ | _ => error "should not have matched anything"
+\<close>
+
+ML \<open>
+ Rewrite.params_pconv (Conv.all_conv |> K |> K) \<^context> (Vartab.empty, []) \<^cterm>\<open>\<And>x. PROP A\<close>
+\<close>
+
+lemma
+ assumes eq: "PROP A \<Longrightarrow> PROP B \<equiv> PROP C"
+ assumes f1: "PROP D \<Longrightarrow> PROP A"
+ assumes f2: "PROP D \<Longrightarrow> PROP C"
+ shows "\<And>x. PROP D \<Longrightarrow> PROP B"
+ apply (rewrite eq)
+ apply (fact f1)
+ apply (fact f2)
+ done
+
+end
--- a/src/HOL/Examples/document/root.tex Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Examples/document/root.tex Sun Dec 12 11:18:42 2021 +0100
@@ -1,7 +1,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
+\usepackage{ifthen,proof,amssymb,isabelle,isabellesym,wasysym}
\isabellestyle{literal}
\usepackage{pdfsetup}\urlstyle{rm}
--- a/src/HOL/Library/Multiset.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Dec 12 11:18:42 2021 +0100
@@ -4,12 +4,13 @@
Author: Jasmin Blanchette, Inria, LORIA, MPII
Author: Dmitriy Traytel, TU Muenchen
Author: Mathias Fleury, MPII
+ Author: Martin Desharnais, MPI-INF Saarbruecken
*)
section \<open>(Finite) Multisets\<close>
theory Multiset
-imports Cancellation
+ imports Cancellation
begin
subsection \<open>The type of multisets\<close>
@@ -2788,8 +2789,6 @@
subsection \<open>The multiset order\<close>
-subsubsection \<open>Well-foundedness\<close>
-
definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
"mult1 r = {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and>
(\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
@@ -2797,6 +2796,9 @@
definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
"mult r = (mult1 r)\<^sup>+"
+definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "multp r M N \<longleftrightarrow> (M, N) \<in> mult {(x, y). r x y}"
+
lemma mult1I:
assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
shows "(N, M) \<in> mult1 r"
@@ -2809,14 +2811,29 @@
lemma mono_mult1:
assumes "r \<subseteq> r'" shows "mult1 r \<subseteq> mult1 r'"
-unfolding mult1_def using assms by blast
+ unfolding mult1_def using assms by blast
lemma mono_mult:
assumes "r \<subseteq> r'" shows "mult r \<subseteq> mult r'"
-unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+ unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+
+lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
+ unfolding le_fun_def le_bool_def
+proof (intro allI impI)
+ fix M N :: "'a multiset"
+ assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
+ hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
+ by blast
+ thus "multp r M N \<Longrightarrow> multp r' M N"
+ unfolding multp_def
+ by (fact mono_mult[THEN subsetD, rotated])
+qed
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-by (simp add: mult1_def)
+ by (simp add: mult1_def)
+
+
+subsubsection \<open>Well-foundedness\<close>
lemma less_add:
assumes mult1: "(N, add_mset a M0) \<in> mult1 r"
@@ -2918,11 +2935,15 @@
qed
qed
-theorem wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
-by (rule acc_wfI) (rule all_accessible)
-
-theorem wf_mult: "wf r \<Longrightarrow> wf (mult r)"
-unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+lemma wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
+ by (rule acc_wfI) (rule all_accessible)
+
+lemma wf_mult: "wf r \<Longrightarrow> wf (mult r)"
+ unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+
+lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
+ unfolding multp_def wfP_def
+ by (simp add: wf_mult)
subsubsection \<open>Closure-free presentation\<close>
@@ -2965,6 +2986,9 @@
qed
qed
+lemmas multp_implies_one_step =
+ mult_implies_one_step[of "{(x, y). r x y}" for r, folded multp_def transp_trans, simplified]
+
lemma one_step_implies_mult:
assumes
"J \<noteq> {#}" and
@@ -2997,6 +3021,9 @@
qed
qed
+lemmas one_step_implies_multp =
+ one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified]
+
lemma subset_implies_mult:
assumes sub: "A \<subset># B"
shows "(A, B) \<in> mult r"
@@ -3009,8 +3036,10 @@
by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
qed
-
-subsection \<open>The multiset extension is cancellative for multiset union\<close>
+lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
+
+
+subsubsection \<open>The multiset extension is cancellative for multiset union\<close>
lemma mult_cancel:
assumes "trans s" and "irrefl s"
@@ -3045,10 +3074,18 @@
thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
qed
+lemmas multp_cancel =
+ mult_cancel[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
lemmas mult_cancel_add_mset =
mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
-lemma mult_cancel_max:
+lemmas multp_cancel_add_mset =
+ mult_cancel_add_mset[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
+lemma mult_cancel_max0:
assumes "trans s" and "irrefl s"
shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
proof -
@@ -3056,6 +3093,112 @@
thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y" "X \<inter># Y" "Y - X \<inter># Y"] by auto
qed
+lemmas mult_cancel_max = mult_cancel_max0[simplified]
+
+lemmas multp_cancel_max =
+ mult_cancel_max[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
+
+subsubsection \<open>Partial-order properties\<close>
+
+lemma mult1_lessE:
+ assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
+ obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
+ "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+proof -
+ from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
+ *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
+ moreover from * [of a] have "a \<notin># K"
+ using \<open>asymp r\<close> by (meson asymp.cases)
+ ultimately show thesis by (auto intro: that)
+qed
+
+lemma trans_mult: "trans r \<Longrightarrow> trans (mult r)"
+ by (simp add: mult_def)
+
+lemma transp_multp: "transp r \<Longrightarrow> transp (multp r)"
+ unfolding multp_def transp_trans_eq
+ by (fact trans_mult[of "{(x, y). r x y}" for r, folded transp_trans])
+
+lemma irrefl_mult:
+ assumes "trans r" "irrefl r"
+ shows "irrefl (mult r)"
+proof (intro irreflI notI)
+ fix M
+ assume "(M, M) \<in> mult r"
+ then obtain I J K where "M = I + J" and "M = I + K"
+ and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> r)"
+ using mult_implies_one_step[OF \<open>trans r\<close>] by blast
+ then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. (k, j) \<in> r" by auto
+ have "finite (set_mset K)" by simp
+ hence "set_mset K = {}"
+ using **
+ proof (induction rule: finite_induct)
+ case empty
+ thus ?case by simp
+ next
+ case (insert x F)
+ have False
+ using \<open>irrefl r\<close>[unfolded irrefl_def, rule_format]
+ using \<open>trans r\<close>[THEN transD]
+ by (metis equals0D insert.IH insert.prems insertE insertI1 insertI2)
+ thus ?case ..
+ qed
+ with * show False by simp
+qed
+
+lemmas irreflp_multp =
+ irrefl_mult[of "{(x, y). r x y}" for r,
+ folded transp_trans_eq irreflp_irrefl_eq, simplified, folded multp_def]
+
+instantiation multiset :: (preorder) order begin
+
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "M < N \<longleftrightarrow> multp (<) M N"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "less_eq_multiset M N \<longleftrightarrow> M < N \<or> M = N"
+
+instance
+proof intro_classes
+ fix M N :: "'a multiset"
+ show "(M < N) = (M \<le> N \<and> \<not> N \<le> M)"
+ unfolding less_eq_multiset_def less_multiset_def
+ by (metis irreflp_def irreflp_less irreflp_multp transpE transp_less transp_multp)
+next
+ fix M :: "'a multiset"
+ show "M \<le> M"
+ unfolding less_eq_multiset_def
+ by simp
+next
+ fix M1 M2 M3 :: "'a multiset"
+ show "M1 \<le> M2 \<Longrightarrow> M2 \<le> M3 \<Longrightarrow> M1 \<le> M3"
+ unfolding less_eq_multiset_def less_multiset_def
+ using transp_multp[OF transp_less, THEN transpD]
+ by blast
+next
+ fix M N :: "'a multiset"
+ show "M \<le> N \<Longrightarrow> N \<le> M \<Longrightarrow> M = N"
+ unfolding less_eq_multiset_def less_multiset_def
+ using transp_multp[OF transp_less, THEN transpD]
+ using irreflp_multp[OF transp_less irreflp_less, unfolded irreflp_def, rule_format]
+ by blast
+qed
+
+end
+
+lemma mset_le_irrefl [elim!]:
+ fixes M :: "'a::preorder multiset"
+ shows "M < M \<Longrightarrow> R"
+ by simp
+
+lemma wfP_less_multiset[simp]:
+ assumes wfP_less: "wfP ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
+ shows "wfP ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+ using wfP_multp[OF wfP_less] less_multiset_def
+ by (metis wfPUNIVI wfP_induct)
+
subsection \<open>Quasi-executable version of the multiset extension\<close>
@@ -3063,22 +3206,22 @@
Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are
executable whenever the given predicate \<open>P\<close> is. Together with the standard
code equations for \<open>(\<inter>#\<close>) and \<open>(-\<close>) this should yield quadratic
- (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>.
+ (with respect to calls to \<open>P\<close>) implementations of \<open>multp_code\<close> and \<open>multeqp_code\<close>.
\<close>
-definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "multp P N M =
+definition multp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "multp_code P N M =
(let Z = M \<inter># N; X = M - Z in
X \<noteq> {#} \<and> (let Y = N - Z in (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x)))"
-definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- "multeqp P N M =
+definition multeqp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "multeqp_code P N M =
(let Z = M \<inter># N; X = M - Z; Y = N - Z in
(\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
-lemma multp_iff:
+lemma multp_code_iff_mult:
assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
- shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
+ shows "multp_code P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
proof -
have *: "M \<inter># N + (N - M \<inter># N) = N" "M \<inter># N + (M - M \<inter># N) = M"
"(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp flip: count_inject)
@@ -3086,87 +3229,40 @@
proof
assume ?L thus ?R
using one_step_implies_mult[of "M - M \<inter># N" "N - M \<inter># N" R "M \<inter># N"] *
- by (auto simp: multp_def Let_def)
+ by (auto simp: multp_code_def Let_def)
next
{ fix I J K :: "'a multiset" assume "(I + J) \<inter># (I + K) = {#}"
then have "I = {#}" by (metis inter_union_distrib_right union_eq_empty)
} note [dest!] = this
assume ?R thus ?L
using mult_implies_one_step[OF assms(2), of "N - M \<inter># N" "M - M \<inter># N"]
- mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def)
+ mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_code_def)
qed
qed
-lemma multeqp_iff:
+lemma multp_code_eq_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multp_code r = multp r"
+ using multp_code_iff_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans multp_def, simplified]
+ by blast
+
+lemma multeqp_code_iff_reflcl_mult:
assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
- shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
+ shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
proof -
{ assume "N \<noteq> M" "M - M \<inter># N = {#}"
then obtain y where "count N y \<noteq> count M y" by (auto simp flip: count_inject)
then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
by (auto simp flip: count_inject dest!: le_neq_implies_less fun_cong[of _ _ y])
}
- then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
- by (auto simp: multeqp_def multp_def Let_def in_diff_count)
- thus ?thesis using multp_iff[OF assms] by simp
-qed
-
-
-subsubsection \<open>Partial-order properties\<close>
-
-lemma (in preorder) mult1_lessE:
- assumes "(N, M) \<in> mult1 {(a, b). a < b}"
- obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
- "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
-proof -
- from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
- *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
- moreover from * [of a] have "a \<notin># K" by auto
- ultimately show thesis by (auto intro: that)
+ then have "multeqp_code P N M \<longleftrightarrow> multp_code P N M \<or> N = M"
+ by (auto simp: multeqp_code_def multp_code_def Let_def in_diff_count)
+ thus ?thesis using multp_code_iff_mult[OF assms] by simp
qed
-instantiation multiset :: (preorder) order
-begin
-
-definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
- where "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
- where "less_eq_multiset M' M \<longleftrightarrow> M' < M \<or> M' = M"
-
-instance
-proof -
- have irrefl: "\<not> M < M" for M :: "'a multiset"
- proof
- assume "M < M"
- then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
- have "trans {(x'::'a, x). x' < x}"
- by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
- moreover note MM
- ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
- \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
- by (rule mult_implies_one_step)
- then obtain I J K where "M = I + J" and "M = I + K"
- and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
- then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
- have "finite (set_mset K)" by simp
- moreover note **
- ultimately have "set_mset K = {}"
- by (induct rule: finite_induct) (auto intro: order_less_trans)
- with * show False by simp
- qed
- have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
- unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "OFCLASS('a multiset, order_class)"
- by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
-qed
-
-end
-
-lemma mset_le_irrefl [elim!]:
- fixes M :: "'a::preorder multiset"
- shows "M < M \<Longrightarrow> R"
- by simp
+lemma multeqp_code_eq_reflclp_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multeqp_code r = (multp r)\<^sup>=\<^sup>="
+ using multeqp_code_iff_reflcl_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans, simplified, folded multp_def]
+ by blast
subsubsection \<open>Monotonicity of multiset union\<close>
@@ -3175,7 +3271,7 @@
by (force simp: mult1_def)
lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def mult_def)
+apply (unfold less_multiset_def multp_def mult_def)
apply (erule trancl_induct)
apply (blast intro: mult1_union)
apply (blast intro: mult1_union trancl_trans)
--- a/src/HOL/Library/Multiset_Order.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Sun Dec 12 11:18:42 2021 +0100
@@ -11,6 +11,135 @@
subsection \<open>Alternative Characterizations\<close>
+subsubsection \<open>The Dershowitz--Manna Ordering\<close>
+
+definition multp\<^sub>D\<^sub>M where
+ "multp\<^sub>D\<^sub>M r M N \<longleftrightarrow>
+ (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)))"
+
+lemma multp\<^sub>D\<^sub>M_imp_multp:
+ "multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N"
+proof -
+ assume "multp\<^sub>D\<^sub>M r M N"
+ then obtain X Y where
+ "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
+ unfolding multp\<^sub>D\<^sub>M_def by blast
+ then have "multp r (N - X + Y) (N - X + X)"
+ by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
+ with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "multp r M N"
+ by (metis subset_mset.diff_add)
+qed
+
+subsubsection \<open>The Huet--Oppen Ordering\<close>
+
+definition multp\<^sub>H\<^sub>O where
+ "multp\<^sub>H\<^sub>O r M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. r y x \<and> count M x < count N x))"
+
+lemma multp_imp_multp\<^sub>H\<^sub>O:
+ assumes "asymp r" and "transp r"
+ shows "multp r M N \<Longrightarrow> multp\<^sub>H\<^sub>O r M N"
+ unfolding multp_def mult_def
+proof (induction rule: trancl_induct)
+ case (base P)
+ then show ?case
+ using \<open>asymp r\<close>
+ by (auto elim!: mult1_lessE simp: count_eq_zero_iff multp\<^sub>H\<^sub>O_def split: if_splits
+ dest!: Suc_lessD)
+next
+ case (step N P)
+ from step(3) have "M \<noteq> N" and
+ **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x. r y x \<and> count M x < count N x)"
+ by (simp_all add: multp\<^sub>H\<^sub>O_def)
+ from step(2) obtain M0 a K where
+ *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+ using \<open>asymp r\<close> by (auto elim: mult1_lessE)
+ from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P"
+ using *(4) \<open>asymp r\<close>
+ by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
+ count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
+ moreover
+ { assume "count P a \<le> count M a"
+ with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
+ by (auto simp add: not_in_iff)
+ with ** obtain z where z: "r a z" "count M z < count N z"
+ by blast
+ with * have "count N z \<le> count P z"
+ using \<open>asymp r\<close>
+ by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset
+ diff_single_trivial in_diff_count not_le_imp_less)
+ with z have "\<exists>z. r a z \<and> count M z < count P z" by auto
+ } note count_a = this
+ { fix y
+ assume count_y: "count P y < count M y"
+ have "\<exists>x. r y x \<and> count M x < count P x"
+ proof (cases "y = a")
+ case True
+ with count_y count_a show ?thesis by auto
+ next
+ case False
+ show ?thesis
+ proof (cases "y \<in># K")
+ case True
+ with *(4) have "r y a" by simp
+ then show ?thesis
+ by (cases "count P a \<le> count M a") (auto dest: count_a intro: \<open>transp r\<close>[THEN transpD])
+ next
+ case False
+ with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
+ by (simp add: not_in_iff)
+ with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
+ show ?thesis
+ proof (cases "z \<in># K")
+ case True
+ with *(4) have "r z a" by simp
+ with z(1) show ?thesis
+ by (cases "count P a \<le> count M a") (auto dest!: count_a intro: \<open>transp r\<close>[THEN transpD])
+ next
+ case False
+ with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
+ by (auto simp add: not_in_iff)
+ with z show ?thesis by auto
+ qed
+ qed
+ qed
+ }
+ ultimately show ?case unfolding multp\<^sub>H\<^sub>O_def by blast
+qed
+
+lemma multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M: "multp\<^sub>H\<^sub>O r M N \<Longrightarrow> multp\<^sub>D\<^sub>M r M N"
+unfolding multp\<^sub>D\<^sub>M_def
+proof (intro iffI exI conjI)
+ assume "multp\<^sub>H\<^sub>O r M N"
+ then obtain z where z: "count M z < count N z"
+ unfolding multp\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
+ define X where "X = N - M"
+ define Y where "Y = M - N"
+ from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
+ from z show "X \<subseteq># N" unfolding X_def by auto
+ show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
+ show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
+ proof (intro allI impI)
+ fix k
+ assume "k \<in># Y"
+ then have "count N k < count M k" unfolding Y_def
+ by (auto simp add: in_diff_count)
+ with \<open>multp\<^sub>H\<^sub>O r M N\<close> obtain a where "r k a" and "count M a < count N a"
+ unfolding multp\<^sub>H\<^sub>O_def by blast
+ then show "\<exists>a. a \<in># X \<and> r k a" unfolding X_def
+ by (auto simp add: in_diff_count)
+ qed
+qed
+
+lemma multp_eq_multp\<^sub>D\<^sub>M: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>D\<^sub>M r"
+ using multp\<^sub>D\<^sub>M_imp_multp multp_imp_multp\<^sub>H\<^sub>O[THEN multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M]
+ by blast
+
+lemma multp_eq_multp\<^sub>H\<^sub>O: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>H\<^sub>O r"
+ using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
+ by blast
+
+subsubsection \<open>Properties of Preorders\<close>
+
context preorder
begin
@@ -59,107 +188,29 @@
lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
"(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
-proof (unfold mult_def, induct rule: trancl_induct)
- case (base P)
- then show ?case
- by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
-next
- case (step N P)
- from step(3) have "M \<noteq> N" and
- **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
- by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
- from step(2) obtain M0 a K where
- *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
- by (blast elim: mult1_lessE)
- from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
- moreover
- { assume "count P a \<le> count M a"
- with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
- by (auto simp add: not_in_iff)
- with ** obtain z where z: "z > a" "count M z < count N z"
- by blast
- with * have "count N z \<le> count P z"
- by (auto elim: less_asym intro: count_inI)
- with z have "\<exists>z > a. count M z < count P z" by auto
- } note count_a = this
- { fix y
- assume count_y: "count P y < count M y"
- have "\<exists>x>y. count M x < count P x"
- proof (cases "y = a")
- case True
- with count_y count_a show ?thesis by auto
- next
- case False
- show ?thesis
- proof (cases "y \<in># K")
- case True
- with *(4) have "y < a" by simp
- then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
- next
- case False
- with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
- by (simp add: not_in_iff)
- with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
- show ?thesis
- proof (cases "z \<in># K")
- case True
- with *(4) have "z < a" by simp
- with z(1) show ?thesis
- by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
- next
- case False
- with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
- by (auto simp add: not_in_iff)
- with z show ?thesis by auto
- qed
- qed
- qed
- }
- ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
-qed
+ unfolding multp_def[of "(<)", symmetric]
+ using multp_imp_multp\<^sub>H\<^sub>O[of "(<)"]
+ by (simp add: less_multiset\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_def)
lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
"less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
-proof -
- assume "less_multiset\<^sub>D\<^sub>M M N"
- then obtain X Y where
- "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
- unfolding less_multiset\<^sub>D\<^sub>M_def by blast
- then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
- by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
- with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
- by (metis subset_mset.diff_add)
-qed
+ unfolding multp_def[of "(<)", symmetric]
+ by (rule multp\<^sub>D\<^sub>M_imp_multp[of "(<)" M N]) (simp add: less_multiset\<^sub>D\<^sub>M_def multp\<^sub>D\<^sub>M_def)
lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
-unfolding less_multiset\<^sub>D\<^sub>M_def
-proof (intro iffI exI conjI)
- assume "less_multiset\<^sub>H\<^sub>O M N"
- then obtain z where z: "count M z < count N z"
- unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
- define X where "X = N - M"
- define Y where "Y = M - N"
- from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
- from z show "X \<subseteq># N" unfolding X_def by auto
- show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
- show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
- proof (intro allI impI)
- fix k
- assume "k \<in># Y"
- then have "count N k < count M k" unfolding Y_def
- by (auto simp add: in_diff_count)
- with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
- unfolding less_multiset\<^sub>H\<^sub>O_def by blast
- then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
- by (auto simp add: in_diff_count)
- qed
-qed
+ unfolding less_multiset\<^sub>D\<^sub>M_def less_multiset\<^sub>H\<^sub>O_def
+ unfolding multp\<^sub>D\<^sub>M_def[symmetric] multp\<^sub>H\<^sub>O_def[symmetric]
+ by (rule multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M)
lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N"
- by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+ unfolding multp_def[of "(<)", symmetric]
+ using multp_eq_multp\<^sub>D\<^sub>M[of "(<)", simplified]
+ by (simp add: multp\<^sub>D\<^sub>M_def less_multiset\<^sub>D\<^sub>M_def)
lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
- by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+ unfolding multp_def[of "(<)", symmetric]
+ using multp_eq_multp\<^sub>H\<^sub>O[of "(<)", simplified]
+ by (simp add: multp\<^sub>H\<^sub>O_def less_multiset\<^sub>H\<^sub>O_def)
lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
@@ -167,10 +218,15 @@
end
lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
- unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
+ unfolding less_multiset_def multp_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
-lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
-lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
+lemma less_multiset\<^sub>D\<^sub>M:
+ "M < N \<longleftrightarrow> (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
+ by (rule mult\<^sub>D\<^sub>M[folded multp_def less_multiset_def])
+
+lemma less_multiset\<^sub>H\<^sub>O:
+ "M < N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x>y. count M x < count N x))"
+ by (rule mult\<^sub>H\<^sub>O[folded multp_def less_multiset_def])
lemma subset_eq_imp_le_multiset:
shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
@@ -198,7 +254,7 @@
(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
- using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
+ using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M by blast
(* FIXME: "le" should be "less" in this and other names *)
lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
@@ -381,9 +437,9 @@
begin
lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
- unfolding less_multiset_def by (auto intro: wf_mult wf)
+ unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)
-instance by standard (metis less_multiset_def wf wf_def wf_mult)
+instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)
end
--- a/src/HOL/Library/Rewrite.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Library/Rewrite.thy Sun Dec 12 11:18:42 2021 +0100
@@ -2,6 +2,8 @@
Author: Christoph Traut, Lars Noschinski, TU Muenchen
Proof method "rewrite" with support for subterm-selection based on patterns.
+
+Documentation: https://arxiv.org/abs/2111.04082
*)
theory Rewrite
--- a/src/HOL/List.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/List.thy Sun Dec 12 11:18:42 2021 +0100
@@ -4238,6 +4238,8 @@
case (Cons x xs) thus ?case by (fastforce split: if_splits)
qed
+lemmas find_None_iff2 = find_None_iff[THEN eq_iff_swap]
+
lemma find_Some_iff:
"List.find P xs = Some x \<longleftrightarrow>
(\<exists>i<length xs. P (xs!i) \<and> x = xs!i \<and> (\<forall>j<i. \<not> P (xs!j)))"
@@ -4249,6 +4251,8 @@
using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce
qed
+lemmas find_Some_iff2 = find_Some_iff[THEN eq_iff_swap]
+
lemma find_cong[fundef_cong]:
assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x"
shows "List.find P xs = List.find Q ys"
--- a/src/HOL/Map.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Map.thy Sun Dec 12 11:18:42 2021 +0100
@@ -667,6 +667,10 @@
lemma fun_upd_None_if_notin_dom[simp]: "k \<notin> dom m \<Longrightarrow> m(k := None) = m"
by auto
+lemma ran_map_upd_Some:
+ "\<lbrakk> m x = Some y; inj_on m (dom m); z \<notin> ran m \<rbrakk> \<Longrightarrow> ran(m(x := Some z)) = ran m - {y} \<union> {z}"
+by(force simp add: ran_def domI inj_onD)
+
lemma ran_map_add:
assumes "dom m1 \<inter> dom m2 = {}"
shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
--- a/src/HOL/ROOT Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/ROOT Sun Dec 12 11:18:42 2021 +0100
@@ -36,6 +36,7 @@
"ML"
Peirce
Records
+ Rewrite_Examples
Seq
Sqrt
document_files
@@ -695,7 +696,6 @@
Reflection_Examples
Refute_Examples
Residue_Ring
- Rewrite_Examples
SOS
SOS_Cert
Serbian
--- a/src/HOL/Relation.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Relation.thy Sun Dec 12 11:18:42 2021 +0100
@@ -241,6 +241,11 @@
lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
by (auto simp add: irrefl_def)
+lemma (in preorder) irreflp_less[simp]: "irreflp (<)"
+ by (simp add: irreflpI)
+
+lemma (in preorder) irreflp_greater[simp]: "irreflp (>)"
+ by (simp add: irreflpI)
subsubsection \<open>Asymmetry\<close>
@@ -259,6 +264,17 @@
lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
by (blast intro: asymI dest: asymD)
+context preorder begin
+
+lemma asymp_less[simp]: "asymp (<)"
+ by (auto intro: asympI dual_order.asym)
+
+lemma asymp_greater[simp]: "asymp (>)"
+ by (auto intro: asympI dual_order.asym)
+
+end
+
+
subsubsection \<open>Symmetry\<close>
definition sym :: "'a rel \<Rightarrow> bool"
--- a/src/HOL/Set_Interval.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Set_Interval.thy Sun Dec 12 11:18:42 2021 +0100
@@ -1581,7 +1581,7 @@
assume "finite S" and "\<not> Suc (Max S) \<ge> card S"
then have "Suc (Max S) < card S"
by simp
- with `finite S` have "S \<subseteq> {0..Max S}"
+ with \<open>finite S\<close> have "S \<subseteq> {0..Max S}"
by auto
hence "card S \<le> card {0..Max S}"
by (intro card_mono; auto)
@@ -2110,14 +2110,14 @@
let ?S' = "S - {Max S}"
from Suc have "Max S \<in> S" by (auto intro: Max_in)
hence cards: "card S = Suc (card ?S')"
- using `finite S` by (intro card.remove; auto)
+ using \<open>finite S\<close> by (intro card.remove; auto)
hence "\<Sum> {0..<card ?S'} \<le> \<Sum> ?S'"
using Suc by (intro Suc; auto)
hence "\<Sum> {0..<card ?S'} + x \<le> \<Sum> ?S' + Max S"
- using `Max S \<ge> x` by simp
+ using \<open>Max S \<ge> x\<close> by simp
also have "... = \<Sum> S"
- using sum.remove[OF `finite S` `Max S \<in> S`, where g="\<lambda>x. x"]
+ using sum.remove[OF \<open>finite S\<close> \<open>Max S \<in> S\<close>, where g="\<lambda>x. x"]
by simp
finally show ?case
using cards Suc by auto
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Sun Dec 12 11:18:42 2021 +0100
@@ -26,7 +26,8 @@
if do_it then
"/tmp/isa_filter"
|> generate_casc_lbt_isa_files_for_theory ctxt thy
- (THF (Without_FOOL, Polymorphic, THF_Without_Choice)) infer_policy "poly_native_higher"
+ (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice)) infer_policy
+ "poly_native_higher"
else
()
\<close>
--- a/src/HOL/TPTP/atp_problem_import.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Sun Dec 12 11:18:42 2021 +0100
@@ -246,8 +246,6 @@
ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac lthy i)
-fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
-
fun make_conj (defs, nondefs) conjs =
Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => \<^prop>\<open>False\<close>)
@@ -298,9 +296,9 @@
val (format, type_enc, lam_trans) =
(case format_str of
"FOF" => (FOF, "mono_guards??", liftingN)
- | "TF0" => (TFF (Without_FOOL, Monomorphic), "mono_native", liftingN)
- | "TH0" => (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher",
- keep_lamsN)
+ | "TF0" => (TFF (Monomorphic, Without_FOOL), "mono_native", liftingN)
+ | "TH0" => (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice),
+ "mono_native_higher", keep_lamsN)
| "DFG" => (DFG Monomorphic, "mono_native", liftingN)
| _ => error ("Unknown format " ^ quote format_str ^
" (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
--- a/src/HOL/TPTP/atp_theory_export.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Sun Dec 12 11:18:42 2021 +0100
@@ -36,11 +36,11 @@
val prefix = Library.prefix
val fact_name_of = prefix fact_prefix o ascii_of
-fun atp_of_format (THF (_, Polymorphic, _)) = leo3N
- | atp_of_format (THF (_, Monomorphic, _)) = satallaxN
+fun atp_of_format (THF (Polymorphic, _, _)) = leo3N
+ | atp_of_format (THF (Monomorphic, _, _)) = satallaxN
| atp_of_format (DFG Monomorphic) = spassN
- | atp_of_format (TFF (_, Polymorphic)) = alt_ergoN
- | atp_of_format (TFF (_, Monomorphic)) = vampireN
+ | atp_of_format (TFF (Polymorphic, _)) = alt_ergoN
+ | atp_of_format (TFF (Monomorphic, _)) = vampireN
| atp_of_format FOF = eN (* FIXME? *)
| atp_of_format CNF_UEQ = waldmeisterN
| atp_of_format CNF = eN (* FIXME? *)
--- a/src/HOL/Tools/ATP/atp_problem.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun Dec 12 11:18:42 2021 +0100
@@ -32,7 +32,8 @@
gen_prec : bool,
gen_simp : bool}
- datatype fool = Without_FOOL | With_FOOL
+ type syntax = {with_ite : bool, with_let : bool}
+ datatype fool = Without_FOOL | With_FOOL of syntax
datatype polymorphism = Monomorphic | Polymorphic
datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
@@ -40,8 +41,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of fool * polymorphism |
- THF of fool * polymorphism * thf_flavor |
+ TFF of polymorphism * fool |
+ THF of polymorphism * syntax * thf_flavor |
DFG of polymorphism
datatype atp_formula_role =
@@ -196,7 +197,9 @@
gen_prec : bool,
gen_simp : bool}
-datatype fool = Without_FOOL | With_FOOL
+
+type syntax = {with_ite : bool, with_let : bool}
+datatype fool = Without_FOOL | With_FOOL of syntax
datatype polymorphism = Monomorphic | Polymorphic
datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
@@ -204,8 +207,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of fool * polymorphism |
- THF of fool * polymorphism * thf_flavor |
+ TFF of polymorphism * fool |
+ THF of polymorphism * syntax * thf_flavor |
DFG of polymorphism
datatype atp_formula_role =
@@ -274,7 +277,7 @@
fun make_builtin arity is_predicate name = (name, {arity = arity, is_predicate = is_predicate})
in
map (make_builtin 0 true) [tptp_false, tptp_true] @
- map (make_builtin 1 true) [tptp_not] @
+ map (make_builtin 1 true) [tptp_not, tptp_ho_forall, tptp_ho_exists] @
map (make_builtin 2 true) [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
tptp_equal, tptp_old_equal] @
map (make_builtin 2 false) [tptp_let] @
@@ -390,13 +393,17 @@
fun is_format_higher_order (THF _) = true
| is_format_higher_order _ = false
+
+fun is_format_higher_order_with_choice (THF (_, _, THF_With_Choice)) = true
+ | is_format_higher_order_with_choice _ = false
+
fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
| is_format_typed (DFG _) = true
| is_format_typed _ = false
-fun is_format_with_fool (THF (With_FOOL, _, _)) = true
- | is_format_with_fool (TFF (With_FOOL, _)) = true
+fun is_format_with_fool (THF _) = true
+ | is_format_with_fool (TFF (_, With_FOOL _)) = true
| is_format_with_fool _ = false
fun tptp_string_of_role Axiom = "axiom"
@@ -516,7 +523,7 @@
if ts = [] orelse is_format_higher_order format then
app0 (s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")") [] ts
else
- error (tptp_let ^ " is special syntax and more than three arguments is only \
+ error (tptp_let ^ " is special syntax and more than two arguments is only \
\supported in higher order")
end
| _ => error (tptp_let ^ " is special syntax and must have at least two arguments"))
@@ -526,19 +533,21 @@
if ts = [] orelse is_format_higher_order format then
app0 (s ^ "(" ^ of_term t1 ^ ", " ^ of_term t2 ^ ", " ^ of_term t3 ^ ")") [] ts
else
- error (tptp_ite ^" is special syntax and more than three arguments is only supported \
+ error (tptp_ite ^ " is special syntax and more than three arguments is only supported \
\in higher order")
- | _ => error "$ite is special syntax and must have at least three arguments")
+ | _ => error (tptp_ite ^ " is special syntax and must have at least three arguments"))
else if s = tptp_choice then
(case ts of
- [AAbs (((s', ty), tm), args)] =>
+ (AAbs (((s', ty), tm), args) :: ts) =>
(* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an
abstraction. *)
- tptp_string_of_app format
- (tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^
- "]: " ^ of_term tm ^ ""
- |> parens) (map of_term args)
- | _ => app ())
+ if ts = [] orelse is_format_higher_order_with_choice format then
+ let val declaration = s' ^ " : " ^ of_type ty in
+ app0 ("(" ^ tptp_choice ^ "[" ^ declaration ^ "]: " ^ of_term tm ^ ")") [] (args @ ts)
+ end
+ else
+ error (tptp_choice ^ " is only supported in higher order")
+ | _ => error (tptp_choice ^ " must be followed by a lambda abstraction"))
else
(case (Symtab.lookup tptp_builtins s, ts) of
(SOME {arity = 1, is_predicate = true}, [t]) =>
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Dec 12 11:18:42 2021 +0100
@@ -153,10 +153,8 @@
Const_Types of ctr_optim |
No_Types
-type syntax = {with_ite: bool}
-
datatype type_enc =
- Native of order * fool * syntax * polymorphism * type_level |
+ Native of order * fool * polymorphism * type_level |
Guards of polymorphism * type_level |
Tags of polymorphism * type_level
@@ -165,17 +163,22 @@
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
-fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _, _)) = false
- | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _, _)) = true
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false
+ | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_full_higher_order _ = false
-fun is_type_enc_fool (Native (_, With_FOOL, _, _, _)) = true
+fun is_type_enc_fool (Native (_, With_FOOL _, _, _)) = true
| is_type_enc_fool _ = false
-fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _, _)) = true
+fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_higher_order _ = false
-fun has_type_enc_ite (Native (_, _, {with_ite, ...}, _, _)) = with_ite
+
+fun has_type_enc_choice (Native (Higher_Order THF_With_Choice, _, _, _)) = true
+ | has_type_enc_choice _ = false
+fun has_type_enc_ite (Native (_, With_FOOL {with_ite, ...}, _, _)) = with_ite
| has_type_enc_ite _ = false
+fun has_type_enc_let (Native (_, With_FOOL {with_let, ...}, _, _)) = with_let
+ | has_type_enc_let _ = false
-fun polymorphism_of_type_enc (Native (_, _, _, poly, _)) = poly
+fun polymorphism_of_type_enc (Native (_, _, poly, _)) = poly
| polymorphism_of_type_enc (Guards (poly, _)) = poly
| polymorphism_of_type_enc (Tags (poly, _)) = poly
@@ -188,7 +191,7 @@
fun is_type_enc_mangling type_enc =
polymorphism_of_type_enc type_enc = Mangled_Monomorphic
-fun level_of_type_enc (Native (_, _, _, _, level)) = level
+fun level_of_type_enc (Native (_, _, _, level)) = level
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
@@ -330,7 +333,8 @@
("c_implies", (\<^const_name>\<open>implies\<close>, (@{thm fimplies_def}, ("fimplies", \<^const_name>\<open>fimplies\<close>)))),
("equal", (\<^const_name>\<open>HOL.eq\<close>, (@{thm fequal_def}, ("fequal", \<^const_name>\<open>fequal\<close>)))),
("c_All", (\<^const_name>\<open>All\<close>, (@{thm fAll_def}, ("fAll", \<^const_name>\<open>fAll\<close>)))),
- ("c_Ex", (\<^const_name>\<open>Ex\<close>, (@{thm fEx_def}, ("fEx", \<^const_name>\<open>fEx\<close>))))]
+ ("c_Ex", (\<^const_name>\<open>Ex\<close>, (@{thm fEx_def}, ("fEx", \<^const_name>\<open>fEx\<close>)))),
+ ("c_Choice", (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, (@{thm fChoice_def}, ("fChoice", \<^const_name>\<open>fChoice\<close>))))]
val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
@@ -349,6 +353,7 @@
(\<^const_name>\<open>If\<close>, "If"),
(\<^const_name>\<open>Set.member\<close>, "member"),
(\<^const_name>\<open>HOL.Let\<close>, "Let"),
+ (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, "Choice"),
(\<^const_name>\<open>Meson.COMBI\<close>, combinator_prefix ^ "I"),
(\<^const_name>\<open>Meson.COMBK\<close>, combinator_prefix ^ "K"),
(\<^const_name>\<open>Meson.COMBB\<close>, combinator_prefix ^ "B"),
@@ -386,15 +391,8 @@
fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
-local
- val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
- fun default c = const_prefix ^ lookup_const c
-in
- fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
- | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _, _))) c =
- if c = choice_const then tptp_choice else default c
- | make_fixed_const _ c = default c
-end
+fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
+ | make_fixed_const _ c = const_prefix ^ lookup_const c
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
@@ -680,33 +678,37 @@
fun native_of_string s =
let
+ val (_, s) =
+ (case try (unsuffix "_arith") s of
+ SOME s => (true, s)
+ | NONE => (false, s))
+ val syntax = {with_ite = true, with_let = true}
val (fool, core) =
(case try (unsuffix "_fool") s of
- SOME s => (With_FOOL, s)
+ SOME s => (With_FOOL syntax, s)
| NONE => (Without_FOOL, s))
- val syntax = {with_ite = (fool = With_FOOL)}
in
(case (core, poly) of
("native", SOME poly) =>
(case (poly, level) of
(Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (First_Order, fool, syntax, Mangled_Monomorphic, level)
+ Native (First_Order, fool, Mangled_Monomorphic, level)
else
raise Same.SAME
| (Raw_Monomorphic, _) => raise Same.SAME
- | (poly, All_Types) => Native (First_Order, fool, syntax, poly, All_Types))
+ | (poly, All_Types) => Native (First_Order, fool, poly, All_Types))
| ("native_higher", SOME poly) =>
(case (poly, level) of
(_, Nonmono_Types _) => raise Same.SAME
| (_, Undercover_Types) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (Higher_Order THF_With_Choice, fool, syntax, Mangled_Monomorphic, level)
+ Native (Higher_Order THF_With_Choice, With_FOOL syntax, Mangled_Monomorphic, level)
else
raise Same.SAME
| (poly as Raw_Polymorphic _, All_Types) =>
- Native (Higher_Order THF_With_Choice, fool, syntax, poly, All_Types)
+ Native (Higher_Order THF_With_Choice, With_FOOL syntax, poly, All_Types)
| _ => raise Same.SAME))
end
@@ -752,28 +754,28 @@
fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
| adjust_hologic _ type_enc = type_enc
-fun adjust_fool Without_FOOL _ = Without_FOOL
- | adjust_fool _ fool = fool
+fun adjust_syntax {with_ite = ite1, with_let = let1} {with_ite = ite2, with_let = let2} =
+ {with_ite = ite1 andalso ite2, with_let = let1 andalso let2}
+
+fun adjust_fool (With_FOOL syntax) (With_FOOL syntax') = With_FOOL (adjust_syntax syntax syntax')
+ | adjust_fool _ _ = Without_FOOL
fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (fool, Polymorphic, hologic))
- (Native (order, fool', syntax, poly, level)) =
- Native (adjust_hologic hologic order, adjust_fool fool fool', syntax, no_type_classes poly,
- level)
- | adjust_type_enc (THF (fool, Monomorphic, hologic)) (Native (order, fool', syntax, _, level)) =
- Native (adjust_hologic hologic order, adjust_fool fool fool', syntax, Mangled_Monomorphic,
+fun adjust_type_enc (THF (poly, syntax, hologic)) (Native (order, fool, poly', level)) =
+ Native (adjust_hologic hologic order, adjust_fool (With_FOOL syntax) fool,
+ (case poly of Polymorphic => no_type_classes poly' | Monomorphic => Mangled_Monomorphic),
level)
- | adjust_type_enc (TFF (fool, Monomorphic)) (Native (_, fool', syntax, _, level)) =
- Native (First_Order, adjust_fool fool fool', syntax, Mangled_Monomorphic, level)
- | adjust_type_enc (DFG Polymorphic) (Native (_, _, syntax, poly, level)) =
- Native (First_Order, Without_FOOL, syntax, poly, level)
- | adjust_type_enc (DFG Monomorphic) (Native (_, _, syntax, _, level)) =
- Native (First_Order, Without_FOOL, syntax, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF (fool, _)) (Native (_, fool', syntax, poly, level)) =
- Native (First_Order, adjust_fool fool fool', syntax, no_type_classes poly, level)
- | adjust_type_enc format (Native (_, _, _, poly, level)) =
+ | adjust_type_enc (TFF (poly, fool)) (Native (_, fool', poly', level)) =
+ Native (First_Order, adjust_fool fool fool',
+ (case poly of Polymorphic => no_type_classes poly' | Monomorphic => Mangled_Monomorphic),
+ level)
+ | adjust_type_enc (DFG Polymorphic) (Native (_, _, poly, level)) =
+ Native (First_Order, Without_FOOL, poly, level)
+ | adjust_type_enc (DFG Monomorphic) (Native (_, _, _, level)) =
+ Native (First_Order, Without_FOOL, Mangled_Monomorphic, level)
+ | adjust_type_enc format (Native (_, _, poly, level)) =
adjust_type_enc format (Guards (no_type_classes poly, level))
| adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
(if is_type_enc_sound type_enc then Tags else Guards) stuff
@@ -949,8 +951,8 @@
T_args
else
(case type_enc of
- Native (_, _, _, Raw_Polymorphic _, _) => T_args
- | Native (_, _, _, Type_Class_Polymorphic, _) => T_args
+ Native (_, _, Raw_Polymorphic _, _) => T_args
+ | Native (_, _, Type_Class_Polymorphic, _) => T_args
| _ =>
let
fun gen_type_args _ _ [] = []
@@ -1086,7 +1088,7 @@
val tm_args =
tm_args @
(case type_enc of
- Native (_, _, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+ Native (_, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
[ATerm ((TYPE_name, ty_args), [])]
| _ => [])
in AAtom (ATerm ((cl, ty_args), tm_args)) end
@@ -1187,10 +1189,10 @@
val unmangled_invert_const = invert_const o hd o unmangled_const_name
-fun vars_of_iterm vars (IConst ((s, _), _, _)) = insert (op =) s vars
- | vars_of_iterm vars (IVar ((s, _), _)) = insert (op =) s vars
- | vars_of_iterm vars (IApp (tm1, tm2)) = union (op =) (vars_of_iterm vars tm1) (vars_of_iterm vars tm2)
- | vars_of_iterm vars (IAbs (_, tm)) = vars_of_iterm vars tm
+fun vars_of_iterm (IConst ((s, _), _, _)) = [s]
+ | vars_of_iterm (IVar ((s, _), _)) = [s]
+ | vars_of_iterm (IApp (tm1, tm2)) = union (op =) (vars_of_iterm tm1) (vars_of_iterm tm2)
+ | vars_of_iterm (IAbs (((s, _), _), tm)) = insert (op =) s (vars_of_iterm tm)
fun generate_unique_name gen unique n =
let val x = gen n in
@@ -1201,7 +1203,7 @@
| eta_expand_quantifier_body tm =
let
(* We accumulate all variables because E 2.5 does not support variable shadowing. *)
- val vars = vars_of_iterm [] tm
+ val vars = vars_of_iterm tm
val x = generate_unique_name
(fn n => "X" ^ (if n = 0 then "" else string_of_int n))
(fn name => not (exists (equal name) vars)) 0
@@ -1215,6 +1217,8 @@
let
val is_fool = is_type_enc_fool type_enc
val has_ite = has_type_enc_ite type_enc
+ val has_let = has_type_enc_let type_enc
+ val has_choice = has_type_enc_choice type_enc
fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] =
(* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser
limitations. This works in conjunction with special code in "ATP_Problem" that uses the
@@ -1258,7 +1262,7 @@
else
tm2'
| IConst ((s, _), _, _) =>
- if s = tptp_ho_forall orelse s = tptp_ho_exists then
+ if s = tptp_ho_forall orelse s = tptp_ho_exists orelse s = tptp_choice then
eta_expand_quantifier_body tm2'
else
tm2'
@@ -1270,7 +1274,7 @@
let val argc = length args in
if has_ite andalso s = "c_If" andalso argc >= 3 then
IConst (`I tptp_ite, T, [])
- else if is_fool andalso s = "c_Let" andalso argc >= 2 then
+ else if has_let andalso s = "c_Let" andalso argc >= 2 then
IConst (`I tptp_let, T, [])
else
(case proxify_const s of
@@ -1279,6 +1283,7 @@
fun plain_const () = IConst (name, T, [])
fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
fun handle_fool card x = if card = argc then x else proxy_const ()
+ fun handle_min_card card x = if argc < card then proxy_const () else x
in
if top_level then
(case s of
@@ -1295,6 +1300,11 @@
| "c_implies" => IConst (`I tptp_implies, T, [])
| "c_All" => tweak_ho_quant tptp_ho_forall T args
| "c_Ex" => tweak_ho_quant tptp_ho_exists T args
+ | "c_Choice" =>
+ if has_choice then
+ handle_min_card 1 (IConst (`I tptp_choice, T, []))
+ else
+ proxy_const ()
| s =>
if is_tptp_equal s then
tweak_ho_equal T argc
@@ -1310,6 +1320,7 @@
| "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, []))
| "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args)
| "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args)
+ | "c_Choice" => proxy_const ()
| s =>
if is_tptp_equal s then
handle_fool 2 (IConst (`I tptp_equal, T, []))
@@ -1610,7 +1621,8 @@
fun consider_var_ary const_T var_T max_ary =
let
fun iter ary T =
- if ary = max_ary orelse type_instance thy var_T T orelse type_instance thy T var_T then
+ if ary = max_ary orelse type_instance thy var_T T orelse type_instance thy T var_T orelse
+ not (can dest_funT T) then
ary
else
iter (ary + 1) (range_type T)
@@ -1850,9 +1862,26 @@
(* Partial characterization of "fAll" and "fEx". A complete characterization
would require the axiom of choice for replay with Metis. *)
(("fAll", false), [(General, @{lemma "\<not> fAll P \<or> P x" by (auto simp: fAll_def)})]),
- (("fEx", false), [(General, @{lemma "\<not> P x \<or> fEx P" by (auto simp: fEx_def)})])]
+ (("fEx", false), [(General, @{lemma "\<not> P x \<or> fEx P" by (auto simp: fEx_def)})]),
+ (("fChoice", true), [(General, @{thm fChoice_iff_Ex})])]
|> map (apsnd (map (apsnd zero_var_indexes)))
+val () =
+ let
+ fun is_skolemizable \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> = true
+ | is_skolemizable _ = false
+
+ fun check_no_skolemizable_thm thm =
+ if Term.exists_subterm is_skolemizable (Thm.full_prop_of thm) then
+ error "Theorems of the helper table cannot contain skolemizable terms because they don't \
+ \get skolimized in metis."
+ else
+ ()
+ in
+ helper_table true
+ |> List.app (fn (_, thms) => List.app (check_no_skolemizable_thm o snd) thms)
+ end
+
fun completish_helper_table with_combs =
helper_table with_combs @
[((predicator_name, true),
@@ -1881,10 +1910,10 @@
|> class_membs_of_types type_enc add_sorts_on_tvar
|> map (class_atom type_enc)))
#> (case type_enc of
- Native (_, _, _, Type_Class_Polymorphic, _) =>
+ Native (_, _, Type_Class_Polymorphic, _) =>
mk_atyquant AForall (map (fn TVar (z as (_, S)) =>
(AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts)
- | Native (_, _, _, Raw_Polymorphic _, _) =>
+ | Native (_, _, Raw_Polymorphic _, _) =>
mk_atyquant AForall (map (fn TVar (z as _) => (AType ((tvar_name z, []), []), [])) Ts)
| _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)))
@@ -1940,10 +1969,11 @@
in
fold (fn ((helper_s, needs_sound), ths) =>
let
- fun map_syntax_of_type_enc f (Native (order, fool, syntax, polymorphism, type_level)) =
- Native (order, fool, f syntax, polymorphism, type_level)
- | map_syntax_of_type_enc _ type_enc = type_enc
- val remove_ite_syntax = map_syntax_of_type_enc (K {with_ite = false})
+ fun map_syntax f (Native (order, With_FOOL syntax, polymorphism, type_level)) =
+ Native (order, With_FOOL (f syntax), polymorphism, type_level)
+ | map_syntax _ type_enc = type_enc
+ val remove_ite_syntax = map_syntax
+ (fn {with_let, ...} => {with_ite = false, with_let = with_let})
in
if (needs_sound andalso not sound) orelse
(helper_s <> unmangled_s andalso
@@ -2313,7 +2343,7 @@
fun decl_lines_of_classes type_enc =
(case type_enc of
- Native (_, _, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
+ Native (_, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
| _ => K [])
fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
@@ -2375,7 +2405,7 @@
? (fold (fold add_fact_syms) [conjs, facts]
#> fold add_iterm_syms extra_tms
#> (case type_enc of
- Native (_, _, _, Raw_Polymorphic phantoms, _) =>
+ Native (_, _, Raw_Polymorphic phantoms, _) =>
phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
| Native _ => I
| _ => fold add_undefined_const (var_types ())))
@@ -2815,9 +2845,8 @@
if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
else lam_trans
val simp_options =
- let val simp = not (is_type_enc_fool type_enc) in
- {if_simps = simp, let_simps = simp}
- end
+ {if_simps = not (has_type_enc_ite type_enc),
+ let_simps = not (has_type_enc_let type_enc)}
val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts
concl_t facts
--- a/src/HOL/Tools/Metis/metis_generate.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML Sun Dec 12 11:18:42 2021 +0100
@@ -206,12 +206,9 @@
|> Monomorph.monomorph atp_schematic_consts_of ctxt
|> chop (length conj_clauses)
|> apply2 (maps (map (zero_var_indexes o snd)))
- val num_conjs = length conj_clauses
(* Pretend every clause is a "simp" rule, to guide the term ordering. *)
val clauses =
- map2 (fn j => pair (Int.toString j, (Local, Simp))) (0 upto num_conjs - 1) conj_clauses @
- map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
- (0 upto length fact_clauses - 1) fact_clauses
+ map_index (apfst (fn j => (Int.toString j, (Local, Simp)))) (conj_clauses @ fact_clauses)
val (old_skolems, props) =
fold_rev (fn (name, th) => fn (old_skolems, props) =>
th |> Thm.prop_of |> Logic.strip_imp_concl
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Dec 12 11:18:42 2021 +0100
@@ -682,10 +682,10 @@
SOME ((ax_no, cluster_no),
clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
| _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]))
-
val prems = Logic.strip_imp_prems (Thm.prop_of prems_imp_false)
- val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
- |> sort (int_ord o apply2 fst)
+ val substs =
+ map_index (fn (i, prem) => subst_info_of_prem (i + 1) prem) prems
+ |> sort (int_ord o apply2 fst)
val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
val clusters = maps (op ::) depss
val ordered_clusters =
@@ -702,7 +702,7 @@
(Integer.add 1)) substs
|> Int_Tysubst_Table.dest
val needed_axiom_props =
- 0 upto length axioms - 1 ~~ axioms
+ map_index I axioms
|> map_filter (fn (_, NONE) => NONE
| (ax_no, SOME (_, t)) =>
if exists (fn ((ax_no', _), n) =>
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Dec 12 11:18:42 2021 +0100
@@ -151,14 +151,14 @@
val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt
val th_cls_pairs =
- map2 (fn j => fn th =>
+ map_index (fn (j, th) =>
(Thm.get_name_hint th,
th
|> Drule.eta_contraction_rule
|> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem
(lam_trans = combsN) j
||> map do_lams))
- (0 upto length ths0 - 1) ths0
+ ths0
val ths = maps (snd o snd) th_cls_pairs
val dischargers = map (fst o snd) th_cls_pairs
val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sun Dec 12 11:18:42 2021 +0100
@@ -3,7 +3,7 @@
Author: Sascha Boehme, TU Munich
Author: Tobias Nipkow, TU Munich
Author: Makarius
- Author: Martin Desharnais, UniBw Munich
+ Author: Martin Desharnais, UniBw Munich, MPI-INF Saarbruecken
Mirabelle action: "sledgehammer".
*)
@@ -21,48 +21,16 @@
val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*)
val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*)
-val fact_filterK = "fact_filter" (*=STRING: fact filter*)
val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*)
-val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*)
val keepK = "keep" (*=BOOL: keep temporary files created by sledgehammer*)
-val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*)
-val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
-val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*)
-val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*)
-val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*)
-val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*)
-val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*)
val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*)
val proverK = "prover" (*=STRING: name of the external prover to call*)
-val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*)
-val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*)
-val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*)
-val strictK = "strict" (*=BOOL: run in strict mode*)
val term_orderK = "term_order" (*=STRING: term order (in E)*)
-val type_encK = "type_enc" (*=STRING: type encoding scheme*)
-val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*)
-(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
(*defaults used in this Mirabelle action*)
-val preplay_timeout_default = "1"
-val lam_trans_default = "smart"
-val uncurried_aliases_default = "smart"
-val fact_filter_default = "smart"
-val type_enc_default = "smart"
-val strict_default = "false"
-val max_facts_default = "smart"
-val slice_default = "true"
val check_trivial_default = false
val keep_default = false
-(*If a key is present in args then augment a list with its pair*)
-(*This is used to avoid fixing default values at the Mirabelle level, and
- instead use the default values of the tool (Sledgehammer in this case).*)
-fun available_parameter args key label list =
- let
- val value = AList.lookup (op =) args key
- in if is_some value then (label, the value) :: list else list end
-
datatype sh_data = ShData of {
calls: int,
success: int,
@@ -336,23 +304,22 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name fact_filter type_enc strict max_facts slice
- lam_trans uncurried_aliases e_selection_heuristic term_order force_sos
- hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST
- minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st =
+fun run_sh (params as {max_facts, minimize, preplay_timeout, ...}) prover_name e_selection_heuristic
+ term_order force_sos hard_timeout dir pos st =
let
val thy = Proof.theory_of st
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
fun set_file_name (SOME dir) =
- Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
- #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix
- ("prob_" ^
+ let
+ val filename = "prob_" ^
StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
- StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos)) ^ "__")
- #> Config.put SMT_Config.debug_files
- (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_"
- ^ serial_string ())
+ StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
+ in
+ Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
+ #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
+ #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
+ end
| set_file_name NONE = I
val st' =
st
@@ -364,30 +331,13 @@
term_order |> the_default I)
#> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos)
force_sos |> the_default I))
- val params as {max_facts, minimize, preplay_timeout, ...} =
- Sledgehammer_Commands.default_params thy
- ([(* ("verbose", "true"), *)
- ("fact_filter", fact_filter),
- ("type_enc", type_enc),
- ("strict", strict),
- ("lam_trans", lam_trans |> the_default lam_trans_default),
- ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default),
- ("max_facts", max_facts),
- ("slice", slice),
- ("timeout", string_of_int timeout),
- ("preplay_timeout", preplay_timeout)]
- |> isar_proofsLST
- |> smt_proofsLST
- |> minimizeLST (*don't confuse the two minimization flags*)
- |> max_new_mono_instancesLST
- |> max_mono_itersLST)
val default_max_facts =
Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
val time_limit =
(case hard_timeout of
NONE => I
- | SOME secs => Timeout.apply (Time.fromSeconds secs))
+ | SOME t => Timeout.apply t)
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime,
@@ -431,33 +381,17 @@
in
-fun run_sledgehammer change_data thy_index trivial output_dir args proof_method named_thms pos st =
+fun run_sledgehammer change_data (params as {provers, timeout, ...}) output_dir
+ e_selection_heuristic term_order force_sos keep proof_method_from_msg thy_index trivial
+ proof_method named_thms pos st =
let
val thy = Proof.theory_of st
val thy_name = Context.theory_name thy
val triv_str = if trivial then "[T] " else ""
val _ = change_data inc_sh_calls
val _ = if trivial then () else change_data inc_sh_nontriv_calls
- val prover_name = get_prover_name thy args
- val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default
- val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
- val strict = AList.lookup (op =) args strictK |> the_default strict_default
- val max_facts =
- (case AList.lookup (op =) args max_factsK of
- SOME max => max
- | NONE =>
- (case AList.lookup (op =) args max_relevantK of
- SOME max => max
- | NONE => max_facts_default))
- val slice = AList.lookup (op =) args sliceK |> the_default slice_default
- val lam_trans = AList.lookup (op =) args lam_transK
- val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
- val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK
- val term_order = AList.lookup (op =) args term_orderK
- val force_sos = AList.lookup (op =) args force_sosK
- |> Option.map (curry (op <>) "false")
val keep_dir =
- if Mirabelle.get_bool_argument args (keepK, keep_default) then
+ if keep then
let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in
Path.append output_dir (Path.basic subdir)
|> Isabelle_System.make_directory
@@ -466,23 +400,13 @@
end
else
NONE
- val timeout = Mirabelle.get_int_argument args (prover_timeoutK, 30)
(* always use a hard timeout, but give some slack so that the automatic
minimizer has a chance to do its magic *)
- val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
- |> the_default preplay_timeout_default
- val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs"
- val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs"
- val minimizeLST = available_parameter args minimizeK "minimize"
- val max_new_mono_instancesLST =
- available_parameter args max_new_mono_instancesK max_new_mono_instancesK
- val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
- val hard_timeout = SOME (4 * timeout)
+ val hard_timeout = SOME (Time.scale 4.0 timeout)
+ val prover_name = hd provers
val (msg, result) =
- run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans
- uncurried_aliases e_selection_heuristic term_order force_sos
- hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST
- minimizeLST max_new_mono_instancesLST max_mono_itersLST keep_dir pos st
+ run_sh params prover_name e_selection_heuristic term_order force_sos hard_timeout keep_dir pos
+ st
in
(case result of
SH_OK (time_isa, time_prover, names) =>
@@ -498,7 +422,7 @@
change_data (inc_sh_max_lems (length names));
change_data (inc_sh_time_isa time_isa);
change_data (inc_sh_time_prover time_prover);
- proof_method := proof_method_from_msg args msg;
+ proof_method := proof_method_from_msg msg;
named_thms := SOME (map_filter get_thms names);
triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg
@@ -592,8 +516,22 @@
fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) =
let
+ (* Parse Mirabelle-specific parameters *)
val check_trivial =
Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default)
+ val keep = Mirabelle.get_bool_argument arguments (keepK, keep_default)
+ val e_selection_heuristic = AList.lookup (op =) arguments e_selection_heuristicK
+ val term_order = AList.lookup (op =) arguments term_orderK
+ val force_sos = AList.lookup (op =) arguments force_sosK
+ |> Option.map (curry (op <>) "false")
+ val proof_method_from_msg = proof_method_from_msg arguments
+
+ (* Parse Sledgehammer parameters *)
+ val params = Sledgehammer_Commands.default_params \<^theory> arguments
+ |> (fn (params as {provers, ...}) =>
+ (case provers of
+ prover :: _ => Sledgehammer_Prover.set_params_provers params [prover]
+ | _ => error "sledgehammer action requires one prover"))
val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data
val change_data = Synchronized.change data
@@ -611,8 +549,8 @@
check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre
handle Timeout.TIMEOUT _ => false
val log1 =
- run_sledgehammer change_data theory_index trivial output_dir arguments meth named_thms
- pos pre
+ run_sledgehammer change_data params output_dir e_selection_heuristic term_order
+ force_sos keep proof_method_from_msg theory_index trivial meth named_thms pos pre
val log2 =
(case !named_thms of
SOME thms =>
@@ -627,4 +565,4 @@
val () = Mirabelle.register_action "sledgehammer" make_action
-end
+end
\ No newline at end of file
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Dec 12 11:18:42 2021 +0100
@@ -67,6 +67,13 @@
(* ATP configuration *)
+val TF0 = TFF (Monomorphic, Without_FOOL)
+val TF1 = TFF (Polymorphic, Without_FOOL)
+val TX0 = TFF (Monomorphic, With_FOOL {with_ite = true, with_let = true})
+val TX1 = TFF (Polymorphic, With_FOOL {with_ite = true, with_let = true})
+val TH0 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice)
+val TH1 = THF (Polymorphic, {with_ite = true, with_let = true}, THF_With_Choice)
+
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 100 (* FUDGE *)
@@ -160,7 +167,6 @@
val term_order =
Attrib.setup_config_string \<^binding>\<open>atp_term_order\<close> (K smartN)
-
(* agsyHOL *)
val agsyhol_config : atp_config =
@@ -172,7 +178,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((60, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -194,7 +200,7 @@
prem_role = Hypothesis,
best_slices = fn _ =>
(* FUDGE *)
- [(1.0, (((100, ""), TFF (Without_FOOL, Polymorphic), "poly_native", liftingN, false), ""))],
+ [(1.0, (((100, ""), TF1, "poly_native", liftingN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -294,11 +300,11 @@
val heuristic = Config.get ctxt e_selection_heuristic
val (format, enc, main_lam_trans) =
if string_ord (getenv "E_VERSION", "2.7") <> LESS then
- (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool", keep_lamsN)
+ (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
- (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+ (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
else
- (THF (Without_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher", combsN)
+ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
in
(* FUDGE *)
if heuristic = e_smartN then
@@ -357,7 +363,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((40, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -378,7 +384,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -401,7 +407,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((150, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((150, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -465,35 +471,31 @@
" --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
val vampire_config : atp_config =
- let
- val format = TFF (With_FOOL, Polymorphic)
- in
- {exec = (["VAMPIRE_HOME"], ["vampire"]),
- arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
- [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
- " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
- |> sos = sosN ? prefix "--sos on "],
- proof_delims =
- [("=========== Refutation ==========",
- "======= End of refutation =======")] @
- tstp_proof_delims,
- known_failures =
- [(GaveUp, "UNPROVABLE"),
- (GaveUp, "CANNOT PROVE"),
- (Unprovable, "Satisfiability detected"),
- (Unprovable, "Termination reason: Satisfiable"),
- (Interrupted, "Aborted by signal SIGINT")] @
- known_szs_status_failures,
- prem_role = Hypothesis,
- best_slices = fn ctxt =>
- (* FUDGE *)
- [(0.333, (((500, meshN), format, "mono_native_fool", combs_or_liftingN, false), sosN)),
- (0.333, (((150, meshN), format, "poly_native_fool", combs_or_liftingN, false), sosN)),
- (0.334, (((50, meshN), format, "mono_native_fool", combs_or_liftingN, false), no_sosN))]
- |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
- end
+ {exec = (["VAMPIRE_HOME"], ["vampire"]),
+ arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
+ [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
+ |> sos = sosN ? prefix "--sos on "],
+ proof_delims =
+ [("=========== Refutation ==========",
+ "======= End of refutation =======")] @
+ tstp_proof_delims,
+ known_failures =
+ [(GaveUp, "UNPROVABLE"),
+ (GaveUp, "CANNOT PROVE"),
+ (Unprovable, "Satisfiability detected"),
+ (Unprovable, "Termination reason: Satisfiable"),
+ (Interrupted, "Aborted by signal SIGINT")] @
+ known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.333, (((500, meshN), TX1, "mono_native_fool", combs_or_liftingN, false), sosN)),
+ (0.333, (((150, meshN), TX1, "poly_native_fool", combs_or_liftingN, false), sosN)),
+ (0.334, (((50, meshN), TX1, "mono_native_fool", combs_or_liftingN, false), no_sosN))]
+ |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
val vampire = (vampireN, fn () => vampire_config)
@@ -501,24 +503,20 @@
(* Z3 with TPTP syntax (half experimental, half legacy) *)
val z3_tptp_config : atp_config =
- let
- val format = TFF (Without_FOOL, Monomorphic)
- in
- {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
- ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
- proof_delims = [("SZS status Theorem", "")],
- known_failures = known_szs_status_failures,
- prem_role = Hypothesis,
- best_slices =
- (* FUDGE *)
- K [(0.5, (((250, meshN), format, "mono_native", combsN, false), "")),
- (0.25, (((125, mepoN), format, "mono_native", combsN, false), "")),
- (0.125, (((62, mashN), format, "mono_native", combsN, false), "")),
- (0.125, (((31, meshN), format, "mono_native", combsN, false), ""))],
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
- end
+ {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
+ ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
+ proof_delims = [("SZS status Theorem", "")],
+ known_failures = known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices =
+ (* FUDGE *)
+ K [(0.5, (((250, meshN), TF0, "mono_native", combsN, false), "")),
+ (0.25, (((125, mepoN), TF0, "mono_native", combsN, false), "")),
+ (0.125, (((62, mashN), TF0, "mono_native", combsN, false), "")),
+ (0.125, (((31, meshN), TF0, "mono_native", combsN, false), ""))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
@@ -527,8 +525,9 @@
val zipperposition_config : atp_config =
let
- val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
- val enc = ((512, "meshN"), format, "mono_native_higher", keep_lamsN, false)
+ val format =
+ THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice)
+ val enc = ((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false)
in
{exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
@@ -627,26 +626,26 @@
val remote_agsyhol =
remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
- (K (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((60, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_alt_ergo =
remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"]
- (K (((250, ""), TFF (Without_FOOL, Polymorphic), "poly_native", keep_lamsN, false), "") (* FUDGE *))
+ (K (((250, ""), TF1, "poly_native", keep_lamsN, false), "") (* FUDGE *))
val remote_e =
remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
- (K (((750, ""), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "") (* FUDGE *))
+ (K (((750, ""), TF0, "mono_native", combsN, false), "") (* FUDGE *))
val remote_iprover =
remotify_atp iprover "iProver" ["0.99"]
(K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
- (K (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
+ (K (((40, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
val remote_leo3 =
remotify_atp leo3 "Leo-III" ["1.1"]
- (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((150, ""), THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
val remote_zipperposition =
remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"]
- (K (((512, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((512, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
(* Dummy prover *)
@@ -664,19 +663,26 @@
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
+val dummy_fof =
+ let
+ val config = dummy_config Hypothesis FOF "mono_guards??" false
+ in (dummy_fofN, fn () => config) end
-val dummy_fof_format = FOF
-val dummy_fof_config = dummy_config Hypothesis dummy_fof_format "mono_guards??" false
-val dummy_fof = (dummy_fofN, fn () => dummy_fof_config)
+val dummy_tfx =
+ let
+ val config = dummy_config Hypothesis TX1 "poly_native_fool" false
+ in (dummy_tfxN, fn () => config) end
-val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
-val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
-val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
+val dummy_thf =
+ let
+ val config = dummy_config Hypothesis TH1 "poly_native_higher" false
+ in (dummy_thfN, fn () => config) end
-val dummy_thf_format = THF (With_FOOL, Polymorphic, THF_With_Choice)
-val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "mono_native_higher_fool" false
-val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
-
+val dummy_thf_reduced =
+ let
+ val format = THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice)
+ val config = dummy_config Hypothesis format "poly_native_higher" false
+ in (dummy_thfN ^ "_reduced", fn () => config) end
(* Setup *)
@@ -713,7 +719,7 @@
val atps =
[agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
- remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf]
+ remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]
val _ = Theory.setup (fold add_atp atps)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Dec 12 11:18:42 2021 +0100
@@ -47,6 +47,8 @@
preplay_timeout : Time.time,
expect : string}
+ val set_params_provers : params -> string list -> params
+
type prover_problem =
{comment : string,
state : Proof.state,
@@ -141,6 +143,33 @@
preplay_timeout : Time.time,
expect : string}
+fun set_params_provers params provers =
+ {debug = #debug params,
+ verbose = #verbose params,
+ overlord = #overlord params,
+ spy = #spy params,
+ provers = provers,
+ type_enc = #type_enc params,
+ strict = #strict params,
+ lam_trans = #lam_trans params,
+ uncurried_aliases = #uncurried_aliases params,
+ learn = #learn params,
+ fact_filter = #fact_filter params,
+ induction_rules = #induction_rules params,
+ max_facts = #max_facts params,
+ fact_thresholds = #fact_thresholds params,
+ max_mono_iters = #max_mono_iters params,
+ max_new_mono_instances = #max_new_mono_instances params,
+ isar_proofs = #isar_proofs params,
+ compress = #compress params,
+ try0 = #try0 params,
+ smt_proofs = #smt_proofs params,
+ slice = #slice params,
+ minimize = #minimize params,
+ timeout = #timeout params,
+ preplay_timeout = #preplay_timeout params,
+ expect = #expect params}
+
type prover_problem =
{comment : string,
state : Proof.state,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Dec 12 11:18:42 2021 +0100
@@ -151,6 +151,7 @@
val problem_file_name =
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
+ |> Path.ext "p"
val prob_path =
if dest_dir = "" then
File.tmp_path problem_file_name
@@ -342,8 +343,16 @@
the proof file too. *)
fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else ()
fun export (_, (output, _, _, _, _), _) =
- if dest_dir = "" then ()
- else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
+ let
+ val make_export_path =
+ Path.split_ext
+ #> apfst (Path.explode o suffix "_proof" o Path.implode)
+ #> swap
+ #> uncurry Path.ext
+ in
+ if dest_dir = "" then ()
+ else File.write (make_export_path prob_path) output
+ end
val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome),
SOME (format, type_enc)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sun Dec 12 11:18:42 2021 +0100
@@ -76,11 +76,17 @@
not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT])
fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
- ...} : params) state goal i =
+ type_enc, ...} : params) state goal i =
let
+ val (higher_order, nat_as_int) =
+ (case type_enc of
+ SOME s => (String.isSubstring "native_higher" s, String.isSubstring "arith" s)
+ | NONE => (false, false))
fun repair_context ctxt =
ctxt |> Context.proof_map (SMT_Config.select_solver name)
|> Config.put SMT_Config.verbose debug
+ |> Config.put SMT_Config.higher_order higher_order
+ |> Config.put SMT_Config.nat_as_int nat_as_int
|> (if overlord then
Config.put SMT_Config.debug_files
(overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
--- a/src/HOL/Wellfounded.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/HOL/Wellfounded.thy Sun Dec 12 11:18:42 2021 +0100
@@ -79,6 +79,9 @@
lemma (in wellorder) wf: "wf {(x, y). x < y}"
unfolding wf_def by (blast intro: less_induct)
+lemma (in wellorder) wfP_less[simp]: "wfP (<)"
+ by (simp add: wf wfP_def)
+
subsection \<open>Basic Results\<close>
--- a/src/HOL/ex/Rewrite_Examples.thy Sun Dec 12 10:42:51 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,300 +0,0 @@
-theory Rewrite_Examples
-imports Main "HOL-Library.Rewrite"
-begin
-
-section \<open>The rewrite Proof Method by Example\<close>
-
-(* This file is intended to give an overview over
- the features of the pattern-based rewrite proof method.
-
- See also https://www21.in.tum.de/~noschinl/Pattern-2014/
-*)
-lemma
- fixes a::int and b::int and c::int
- assumes "P (b + a)"
- shows "P (a + b)"
-by (rewrite at "a + b" add.commute)
- (rule assms)
-
-(* Selecting a specific subterm in a large, ambiguous term. *)
-lemma
- fixes a b c :: int
- assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c"
- shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
- by (rewrite in "f _ + f \<hole> = _" diff_self) fact
-
-lemma
- fixes a b c :: int
- assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
- shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
- by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact
-
-lemma
- fixes a b c :: int
- assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c"
- shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
- by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact
-
-lemma
- fixes a b c :: int
- assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
- shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
- by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact
-
-lemma
- fixes x y :: nat
- shows"x + y > c \<Longrightarrow> y + x > c"
- by (rewrite at "\<hole> > c" add.commute) assumption
-
-(* We can also rewrite in the assumptions. *)
-lemma
- fixes x y :: nat
- assumes "y + x > c \<Longrightarrow> y + x > c"
- shows "x + y > c \<Longrightarrow> y + x > c"
- by (rewrite in asm add.commute) fact
-
-lemma
- fixes x y :: nat
- assumes "y + x > c \<Longrightarrow> y + x > c"
- shows "x + y > c \<Longrightarrow> y + x > c"
- by (rewrite in "x + y > c" at asm add.commute) fact
-
-lemma
- fixes x y :: nat
- assumes "y + x > c \<Longrightarrow> y + x > c"
- shows "x + y > c \<Longrightarrow> y + x > c"
- by (rewrite at "\<hole> > c" at asm add.commute) fact
-
-lemma
- assumes "P {x::int. y + 1 = 1 + x}"
- shows "P {x::int. y + 1 = x + 1}"
- by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact
-
-lemma
- assumes "P {x::int. y + 1 = 1 + x}"
- shows "P {x::int. y + 1 = x + 1}"
- by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute)
- fact
-
-lemma
- assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
- shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
- by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
-
-(* This is not limited to the first assumption *)
-lemma
- assumes "PROP P \<equiv> PROP Q"
- shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
- by (rewrite at asm assms)
-
-lemma
- assumes "PROP P \<equiv> PROP Q"
- shows "PROP R \<Longrightarrow> PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
- by (rewrite at asm assms)
-
-(* Rewriting "at asm" selects each full assumption, not any parts *)
-lemma
- assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)"
- shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R"
- apply (rewrite at asm assms)
- apply assumption
- done
-
-
-
-(* Rewriting with conditional rewriting rules works just as well. *)
-lemma test_theorem:
- fixes x :: nat
- shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
- by (rule Orderings.order_antisym)
-
-(* Premises of the conditional rule yield new subgoals. The
- assumptions of the goal are propagated into these subgoals
-*)
-lemma
- fixes f :: "nat \<Rightarrow> nat"
- shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
- apply (rewrite at "f x" to "0" test_theorem)
- apply assumption
- apply assumption
- apply (rule refl)
- done
-
-(* This holds also for rewriting in assumptions. The order of assumptions is preserved *)
-lemma
- assumes rewr: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP R \<equiv> PROP R'"
- assumes A1: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP P"
- assumes A2: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP Q"
- assumes C: "PROP S \<Longrightarrow> PROP R' \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
- shows "PROP S \<Longrightarrow> PROP R \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
- apply (rewrite at asm rewr)
- apply (fact A1)
- apply (fact A2)
- apply (fact C)
- done
-
-
-(*
- Instantiation.
-
- Since all rewriting is now done via conversions,
- instantiation becomes fairly easy to do.
-*)
-
-(* We first introduce a function f and an extended
- version of f that is annotated with an invariant. *)
-fun f :: "nat \<Rightarrow> nat" where "f n = n"
-definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n"
-
-lemma annotate_f: "f = f_inv I"
- by (simp add: f_inv_def fun_eq_iff)
-
-(* We have a lemma with a bound variable n, and
- want to add an invariant to f. *)
-lemma
- assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x"
- shows "P (\<lambda>n. f n + 1) = x"
- by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact
-
-(* We can also add an invariant that contains the variable n bound in the outer context.
- For this, we need to bind this variable to an identifier. *)
-lemma
- assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
- shows "P (\<lambda>n. f n + 1) = x"
- by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
-
-(* Any identifier will work *)
-lemma
- assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
- shows "P (\<lambda>n. f n + 1) = x"
- by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
-
-(* The "for" keyword. *)
-lemma
- assumes "P (2 + 1)"
- shows "\<And>x y. P (1 + 2 :: nat)"
-by (rewrite in "P (1 + 2)" at for (x) add.commute) fact
-
-lemma
- assumes "\<And>x y. P (y + x)"
- shows "\<And>x y. P (x + y :: nat)"
-by (rewrite in "P (x + _)" at for (x y) add.commute) fact
-
-lemma
- assumes "\<And>x y z. y + x + z = z + y + (x::int)"
- shows "\<And>x y z. x + y + z = z + y + (x::int)"
-by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact
-
-lemma
- assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
- shows "\<And>x y z. x + y + z = z + y + (x::int)"
-by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact
-
-lemma
- assumes "\<And>x y z. x + y + z = y + z + (x::int)"
- shows "\<And>x y z. x + y + z = z + y + (x::int)"
-by (rewrite at "\<hole> + _" at "_ = \<hole>" in for () add.commute) fact
-
-lemma
- assumes eq: "\<And>x. P x \<Longrightarrow> g x = x"
- assumes f1: "\<And>x. Q x \<Longrightarrow> P x"
- assumes f2: "\<And>x. Q x \<Longrightarrow> x"
- shows "\<And>x. Q x \<Longrightarrow> g x"
- apply (rewrite at "g x" in for (x) eq)
- apply (fact f1)
- apply (fact f2)
- done
-
-(* The for keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
-lemma
- assumes "(\<And>(x::int). x < 1 + x)"
- and "(x::int) + 1 > x"
- shows "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x"
-by (rewrite at "x + 1" in for (x) at asm add.commute)
- (rule assms)
-
-(* The rewrite method also has an ML interface *)
-lemma
- assumes "\<And>a b. P ((a + 1) * (1 + b)) "
- shows "\<And>a b :: nat. P ((a + 1) * (b + 1))"
- apply (tactic \<open>
- let
- val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
- (* Note that the pattern order is reversed *)
- val pat = [
- Rewrite.For [(x, SOME \<^Type>\<open>nat\<close>)],
- Rewrite.In,
- Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>nat\<close> for \<open>Free (x, \<^Type>\<open>nat\<close>)\<close> \<^term>\<open>1 :: nat\<close>\<close>, [])]
- val to = NONE
- in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
- \<close>)
- apply (fact assms)
- done
-
-lemma
- assumes "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. a + b))"
- shows "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))"
- apply (tactic \<open>
- let
- val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
- val pat = [
- Rewrite.Concl,
- Rewrite.In,
- Rewrite.Term (Free ("Q", (\<^Type>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^Type>\<open>bool\<close>)
- $ Abs ("x", \<^Type>\<open>int\<close>, Rewrite.mk_hole 1 (\<^Type>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^Type>\<open>int\<close>)]),
- Rewrite.In,
- Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Free (x, \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
- ]
- val to = NONE
- in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
- \<close>)
- apply (fact assms)
- done
-
-(* There is also conversion-like rewrite function: *)
-ML \<open>
- val ct = \<^cprop>\<open>Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))\<close>
- val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
- val pat = [
- Rewrite.Concl,
- Rewrite.In,
- Rewrite.Term (Free ("Q", (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^typ>\<open>bool\<close>)
- $ Abs ("x", \<^typ>\<open>int\<close>, Rewrite.mk_hole 1 (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>\<open>int\<close>)]),
- Rewrite.In,
- Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Free (x, \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
- ]
- val to = NONE
- val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
-\<close>
-
-section \<open>Regression tests\<close>
-
-ML \<open>
- val ct = \<^cterm>\<open>(\<lambda>b :: int. (\<lambda>a. b + a))\<close>
- val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
- val pat = [
- Rewrite.In,
- Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
- ]
- val to = NONE
- val _ =
- case try (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) ct of
- NONE => ()
- | _ => error "should not have matched anything"
-\<close>
-
-ML \<open>
- Rewrite.params_pconv (Conv.all_conv |> K |> K) \<^context> (Vartab.empty, []) \<^cterm>\<open>\<And>x. PROP A\<close>
-\<close>
-
-lemma
- assumes eq: "PROP A \<Longrightarrow> PROP B \<equiv> PROP C"
- assumes f1: "PROP D \<Longrightarrow> PROP A"
- assumes f2: "PROP D \<Longrightarrow> PROP C"
- shows "\<And>x. PROP D \<Longrightarrow> PROP B"
- apply (rewrite eq)
- apply (fact f1)
- apply (fact f2)
- done
-
-end
--- a/src/Pure/Admin/build_release.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Admin/build_release.scala Sun Dec 12 11:18:42 2021 +0100
@@ -837,6 +837,9 @@
val other_isabelle = context.other_isabelle(tmp_dir)
+ Isabelle_System.make_directory(other_isabelle.etc)
+ File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
+
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
--- a/src/Pure/Admin/build_status.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Sun Dec 12 11:18:42 2021 +0100
@@ -204,7 +204,7 @@
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
ml_statistics: Boolean = false,
- ml_statistics_domain: String => Boolean = (key: String) => true,
+ ml_statistics_domain: String => Boolean = _ => true,
verbose: Boolean = false): Data =
{
val date = Date.now()
@@ -377,7 +377,7 @@
List(HTML.description(
List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
HTML.par(
- List(HTML.itemize(data.entries.map({ case data_entry =>
+ List(HTML.itemize(data.entries.map(data_entry =>
List(
HTML.link(clean_name(data_entry.name) + "/index.html",
HTML.text(data_entry.name))) :::
@@ -388,7 +388,7 @@
List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
})
- }))))))
+ ))))))
for (data_entry <- data.entries) {
val data_name = data_entry.name
@@ -423,10 +423,10 @@
entry.ml_timing.elapsed.minutes.toString,
entry.ml_timing.resources.minutes.toString,
entry.maximum_code.toString,
- entry.maximum_code.toString,
+ entry.average_code.toString,
+ entry.maximum_stack.toString,
entry.average_stack.toString,
- entry.maximum_stack.toString,
- entry.average_heap.toString,
+ entry.maximum_heap.toString,
entry.average_heap.toString,
entry.stored_heap.toString).mkString(" "))))
@@ -608,7 +608,7 @@
"l:" -> (arg => options = options + ("build_log_history=" + arg)),
"o:" -> (arg => options = options + arg),
"s:" -> (arg =>
- space_explode('x', arg).map(Value.Int.parse(_)) match {
+ space_explode('x', arg).map(Value.Int.parse) match {
case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
case _ => error("Error bad PNG image size: " + quote(arg))
}),
--- a/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 12 11:18:42 2021 +0100
@@ -314,7 +314,7 @@
{
List(
List(Remote_Build("Linux A", "augsburg1",
- options = "-m32 -B -M1x2,2,4" +
+ options = "-m32 -B -M4" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=mlton" +
--- a/src/Pure/General/mailman.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/General/mailman.scala Sun Dec 12 11:18:42 2021 +0100
@@ -9,63 +9,93 @@
import java.net.URL
+import scala.util.matching.Regex
+
object Mailman
{
/* mailing list archives */
- def archive(url: URL, name: String = ""): Archive =
+ def archive(url: URL, msg_format: Msg_Format, name: String = ""): Archive =
{
- val text = Url.read(url)
- val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
- val title =
- """<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(text).map(_.group(1))
val list_url =
Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
+
+ val html = Url.read(list_url)
+ val title =
+ """<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(html).map(_.group(1))
+ val hrefs_text =
+ """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(html).map(_.group(1)).toList
+
val list_name =
(proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
- new Archive(list_url, list_name, hrefs)
+ new Archive(list_url, list_name, msg_format, hrefs_text)
}
- class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])
+ abstract class Msg_Format
+ {
+ def regex: Regex
+ }
+
+ class Archive private[Mailman](
+ val list_url: URL,
+ val list_name: String,
+ msg_format: Msg_Format,
+ hrefs_text: List[String])
{
override def toString: String = list_name
- def download(target_dir: Path, progress: Progress = new Progress): List[Path] =
+ private def hrefs_msg: List[String] =
+ (for {
+ href <- """href="([^"]+)/date.html"""".r.findAllMatchIn(Url.read(list_url)).map(_.group(1))
+ html = Url.read(new URL(list_url, href + "/date.html"))
+ msg <- msg_format.regex.findAllMatchIn(html).map(_.group(1))
+ } yield href + "/" + msg).toList
+
+ def get(target_dir: Path, href: String, progress: Progress = new Progress): Option[Path] =
{
val dir = target_dir + Path.basic(list_name)
- Isabelle_System.make_directory(dir)
+ val path = dir + Path.explode(href)
+ val url = new URL(list_url, href)
+ val connection = url.openConnection
+ try {
+ val length = connection.getContentLengthLong
+ val timestamp = connection.getLastModified
+ val file = path.file
+ if (file.isFile && file.length == length && file.lastModified == timestamp) None
+ else {
+ Isabelle_System.make_directory(path.dir)
+ progress.echo("Getting " + url)
+ val bytes =
+ using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024))
+ Bytes.write(file, bytes)
+ file.setLastModified(timestamp)
+ Some(path)
+ }
+ }
+ finally { connection.getInputStream.close() }
+ }
- hrefs.flatMap(name =>
- {
- val path = dir + Path.basic(name)
- val url = new URL(list_url, name)
- val connection = url.openConnection
- try {
- val length = connection.getContentLengthLong
- val timestamp = connection.getLastModified
- val file = path.file
- if (file.isFile && file.length == length && file.lastModified == timestamp) None
- else {
- progress.echo("Getting " + url)
- val bytes =
- using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024))
- Bytes.write(file, bytes)
- file.setLastModified(timestamp)
- Some(path)
- }
- }
- finally { connection.getInputStream.close() }
- })
- }
+ def download_text(target_dir: Path, progress: Progress = new Progress): List[Path] =
+ hrefs_text.flatMap(get(target_dir, _, progress = progress))
+
+ def download_msg(target_dir: Path, progress: Progress = new Progress): List[Path] =
+ hrefs_msg.flatMap(get(target_dir, _, progress = progress))
+
+ def download(target_dir: Path, progress: Progress = new Progress): List[Path] =
+ download_text(target_dir, progress = progress) :::
+ download_msg(target_dir, progress = progress)
}
/* Isabelle mailing lists */
def isabelle_users: Archive =
- archive(Url("https://lists.cam.ac.uk/pipermail/cl-isabelle-users"), name = "isabelle-users")
+ archive(Url("https://lists.cam.ac.uk/pipermail/cl-isabelle-users"), name = "isabelle-users",
+ msg_format =
+ new Msg_Format { val regex: Regex = """<li><a name="\d+" href="(msg\d+\.html)">""".r })
def isabelle_dev: Archive =
- archive(Url("https://mailmanbroy.in.tum.de/pipermail/isabelle-dev"))
+ archive(Url("https://mailmanbroy.in.tum.de/pipermail/isabelle-dev"),
+ new Msg_Format { val regex: Regex = """<LI><A HREF="(\d+\.html)">""".r })
}
--- a/src/Pure/General/scan.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/General/scan.scala Sun Dec 12 11:18:42 2021 +0100
@@ -24,7 +24,6 @@
abstract class Line_Context
case object Finished extends Line_Context
case class Quoted(quote: String) extends Line_Context
- case object Verbatim extends Line_Context
case class Cartouche(depth: Int) extends Line_Context
case class Comment_Prefix(symbol: Symbol.Symbol) extends Line_Context
case class Cartouche_Comment(depth: Int) extends Line_Context
@@ -136,41 +135,6 @@
quote ~ quoted_body(quote) ^^ { case x ~ y => x + y }
- /* verbatim text */
-
- private def verbatim_body: Parser[String] =
- rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString)
-
- def verbatim: Parser[String] =
- {
- "{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z }
- }.named("verbatim")
-
- def verbatim_content(source: String): String =
- {
- require(parseAll(verbatim, source).successful, "no verbatim text")
- source.substring(2, source.length - 2)
- }
-
- def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
- {
- ctxt match {
- case Finished =>
- "{*" ~ verbatim_body ~ opt_term("*}") ^^
- { case x ~ y ~ Some(z) => (x + y + z, Finished)
- case x ~ y ~ None => (x + y, Verbatim) }
- case Verbatim =>
- verbatim_body ~ opt_term("*}") ^^
- { case x ~ Some(y) => (x + y, Finished)
- case x ~ None => (x, Verbatim) }
- case _ => failure("")
- }
- }.named("verbatim_line")
-
- val recover_verbatim: Parser[String] =
- "{*" ~ verbatim_body ^^ { case x ~ y => x + y }
-
-
/* nested text cartouches */
def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
--- a/src/Pure/Isar/args.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Isar/args.ML Sun Dec 12 11:18:42 2021 +0100
@@ -27,9 +27,6 @@
val name_position: (string * Position.T) parser
val cartouche_inner_syntax: string parser
val cartouche_input: Input.source parser
- val text_token: Token.T parser
- val text_input: Input.source parser
- val text: string parser
val binding: binding parser
val alt_name: string parser
val liberal_name: string parser
@@ -47,8 +44,7 @@
val named_fact: (string -> string option * thm list) -> thm list parser
val named_attribute: (string * Position.T -> morphism -> attribute) ->
(morphism -> attribute) parser
- val text_declaration: (Input.source -> declaration) -> declaration parser
- val cartouche_declaration: (Input.source -> declaration) -> declaration parser
+ val embedded_declaration: (Input.source -> declaration) -> declaration parser
val typ_abbrev: typ context_parser
val typ: typ context_parser
val term: term context_parser
@@ -110,10 +106,6 @@
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_input = cartouche >> Token.input_of;
-val text_token = Parse.token (Parse.embedded || Parse.verbatim);
-val text_input = text_token >> Token.input_of;
-val text = text_token >> Token.content_of;
-
val binding = Parse.input name >> (Binding.make o Input.source_content);
val alt_name = alt_string >> Token.content_of;
val liberal_name = (symbolic >> Token.content_of) || name;
@@ -157,11 +149,9 @@
name_token >>
Token.evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
-fun text_declaration read =
- internal_declaration || text_token >> Token.evaluate Token.Declaration (read o Token.input_of);
-
-fun cartouche_declaration read =
- internal_declaration || cartouche >> Token.evaluate Token.Declaration (read o Token.input_of);
+fun embedded_declaration read =
+ internal_declaration ||
+ Parse.token Parse.embedded >> Token.evaluate Token.Declaration (read o Token.input_of);
(* terms and types *)
--- a/src/Pure/Isar/method.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Isar/method.ML Sun Dec 12 11:18:42 2021 +0100
@@ -327,7 +327,7 @@
val parse_tactic =
Scan.state :|-- (fn context =>
- Scan.lift (Args.text_declaration (fn source =>
+ Scan.lift (Args.embedded_declaration (fn source =>
let
val tac =
context
@@ -749,7 +749,7 @@
in Parse.read_embedded ctxt keywords (Scan.many Token.not_eof) #> read_closure ctxt end;
val text_closure =
- Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
+ Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) =>
(case Token.get_value tok of
SOME (Token.Source src) => read ctxt src
| _ =>
--- a/src/Pure/Isar/parse.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Isar/parse.ML Sun Dec 12 11:18:42 2021 +0100
@@ -30,7 +30,6 @@
val string: string parser
val string_position: (string * Position.T) parser
val alt_string: string parser
- val verbatim: string parser
val cartouche: string parser
val control: Antiquote.control parser
val eof: string parser
@@ -70,7 +69,6 @@
val embedded_inner_syntax: string parser
val embedded_input: Input.source parser
val embedded_position: (string * Position.T) parser
- val text: string parser
val path_input: Input.source parser
val path: string parser
val path_binding: (string * Position.T) parser
@@ -120,7 +118,6 @@
val thms1: (Facts.ref * Token.src list) list parser
val options: ((string * Position.T) * (string * Position.T)) list parser
val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
- val embedded_ml_underscore: ML_Lex.token Antiquote.antiquote list parser
val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a
val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a
@@ -200,7 +197,6 @@
val float_number = kind Token.Float;
val string = kind Token.String;
val alt_string = kind Token.Alt_String;
-val verbatim = kind Token.Verbatim;
val cartouche = kind Token.Cartouche;
val control = token (kind Token.control_kind) >> (the o Token.get_control);
val eof = kind Token.EOF;
@@ -289,8 +285,6 @@
val embedded_input = input embedded;
val embedded_position = embedded_input >> Input.source_content;
-val text = group (fn () => "text") (embedded || verbatim);
-
val path_input = group (fn () => "file name/path specification") embedded_input;
val path = path_input >> Input.string_of;
val path_binding = group (fn () => "path binding (strict file name)") (position embedded);
@@ -400,8 +394,8 @@
(* embedded source text *)
-val ML_source = input (group (fn () => "ML source") text);
-val document_source = input (group (fn () => "document source") text);
+val ML_source = input (group (fn () => "ML source") embedded);
+val document_source = input (group (fn () => "document source") embedded);
val document_marker =
group (fn () => "document marker")
@@ -441,7 +435,7 @@
val argument_kinds =
[Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var,
- Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche, Token.Verbatim];
+ Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche];
fun arguments is_symid =
let
@@ -505,12 +499,10 @@
(* embedded ML *)
val embedded_ml =
+ input underscore >> ML_Lex.read_source ||
embedded_input >> ML_Lex.read_source ||
control >> (ML_Lex.read_symbols o Antiquote.control_symbols);
-val embedded_ml_underscore =
- input underscore >> ML_Lex.read_source || embedded_ml;
-
(* read embedded source, e.g. for antiquotations *)
--- a/src/Pure/Isar/parse.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Isar/parse.scala Sun Dec 12 11:18:42 2021 +0100
@@ -65,9 +65,9 @@
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
def name: Parser[String] = atom("name", _.is_name)
def embedded: Parser[String] = atom("embedded content", _.is_embedded)
- def text: Parser[String] = atom("text", _.is_text)
- def ML_source: Parser[String] = atom("ML source", _.is_text)
- def document_source: Parser[String] = atom("document source", _.is_text)
+ def text: Parser[String] = atom("text", _.is_embedded)
+ def ML_source: Parser[String] = atom("ML source", _.is_embedded)
+ def document_source: Parser[String] = atom("document source", _.is_embedded)
def opt_keyword(s: String): Parser[Boolean] =
($$$("(") ~! $$$(s) ~ $$$(")")) ^^ { case _ => true } | success(false)
--- a/src/Pure/Isar/token.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Isar/token.ML Sun Dec 12 11:18:42 2021 +0100
@@ -11,7 +11,7 @@
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
Float | Space |
(*delimited content*)
- String | Alt_String | Verbatim | Cartouche |
+ String | Alt_String | Cartouche |
Control of Antiquote.control |
Comment of Comment.kind option |
(*special content*)
@@ -123,7 +123,7 @@
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
Float | Space |
(*delimited content*)
- String | Alt_String | Verbatim | Cartouche |
+ String | Alt_String | Cartouche |
Control of Antiquote.control |
Comment of Comment.kind option |
(*special content*)
@@ -151,7 +151,6 @@
| Space => "white space"
| String => "quoted string"
| Alt_String => "back-quoted string"
- | Verbatim => "verbatim text"
| Cartouche => "text cartouche"
| Control _ => "control cartouche"
| Comment NONE => "informal comment"
@@ -166,7 +165,6 @@
val delimited_kind =
(fn String => true
| Alt_String => true
- | Verbatim => true
| Cartouche => true
| Control _ => true
| Comment _ => true
@@ -323,7 +321,6 @@
| Type_Var => (Markup.tvar, "")
| String => (Markup.string, "")
| Alt_String => (Markup.alt_string, "")
- | Verbatim => (Markup.verbatim, "")
| Cartouche => (Markup.cartouche, "")
| Control _ => (Markup.cartouche, "")
| Comment _ => (Markup.comment, "")
@@ -374,7 +371,6 @@
(case kind of
String => Symbol_Pos.quote_string_qq x
| Alt_String => Symbol_Pos.quote_string_bq x
- | Verbatim => enclose "{*" "*}" x
| Cartouche => cartouche x
| Control control => Symbol_Pos.content (Antiquote.control_symbols control)
| Comment NONE => enclose "(*" "*)" x
@@ -624,22 +620,6 @@
| ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s;
-(* scan verbatim text *)
-
-val scan_verb =
- $$$ "*" --| Scan.ahead (~$$ "}") ||
- Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single;
-
-val scan_verbatim =
- Scan.ahead ($$ "{" -- $$ "*") |--
- !!! "unclosed verbatim text"
- ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
- (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
-
-val recover_verbatim =
- $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb;
-
-
(* scan cartouche *)
val scan_cartouche =
@@ -678,7 +658,6 @@
fun scan_token keywords = !!! "bad input"
(Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
- scan_verbatim >> token_range Verbatim ||
scan_comment >> token_range (Comment NONE) ||
Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
scan_cartouche >> token_range Cartouche ||
@@ -701,7 +680,6 @@
fun recover msg =
(Symbol_Pos.recover_string_qq ||
Symbol_Pos.recover_string_bq ||
- recover_verbatim ||
Symbol_Pos.recover_cartouche ||
Symbol_Pos.recover_comment ||
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
--- a/src/Pure/Isar/token.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Isar/token.scala Sun Dec 12 11:18:42 2021 +0100
@@ -32,7 +32,6 @@
/*delimited content*/
val STRING = Value("string")
val ALT_STRING = Value("back-quoted string")
- val VERBATIM = Value("verbatim text")
val CARTOUCHE = Value("text cartouche")
val CONTROL = Value("control cartouche")
val INFORMAL_COMMENT = Value("informal comment")
@@ -53,13 +52,12 @@
{
val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
- val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
val cmt = comment ^^ (x => Token(Token.Kind.INFORMAL_COMMENT, x))
val formal_cmt = comment_cartouche ^^ (x => Token(Token.Kind.FORMAL_COMMENT, x))
val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
val ctrl = control_cartouche ^^ (x => Token(Token.Kind.CONTROL, x))
- string | (alt_string | (verb | (cmt | (formal_cmt | (cart | ctrl)))))
+ string | (alt_string | (cmt | (formal_cmt | (cart | ctrl))))
}
private def other_token(keywords: Keyword.Keywords): Parser[Token] =
@@ -99,8 +97,7 @@
val recover_delimited =
(recover_quoted("\"") |
(recover_quoted("`") |
- (recover_verbatim |
- (recover_cartouche | recover_comment)))) ^^ (x => Token(Token.Kind.ERROR, x))
+ (recover_cartouche | recover_comment))) ^^ (x => Token(Token.Kind.ERROR, x))
val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
@@ -119,14 +116,13 @@
quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
val alt_string =
quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
- val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.INFORMAL_COMMENT, x), c) }
val formal_cmt =
comment_cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.FORMAL_COMMENT, x), c) }
val other = other_token(keywords) ^^ { case x => (x, Scan.Finished) }
- string | (alt_string | (verb | (cart | (cmt | (formal_cmt | other)))))
+ string | (alt_string | (cart | (cmt | (formal_cmt | other))))
}
}
@@ -286,7 +282,6 @@
kind == Token.Kind.VAR ||
kind == Token.Kind.TYPE_IDENT ||
kind == Token.Kind.TYPE_VAR
- def is_text: Boolean = is_embedded || kind == Token.Kind.VERBATIM
def is_space: Boolean = kind == Token.Kind.SPACE
def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
@@ -302,7 +297,6 @@
def is_unfinished: Boolean = is_error &&
(source.startsWith("\"") ||
source.startsWith("`") ||
- source.startsWith("{*") ||
source.startsWith("(*") ||
source.startsWith(Symbol.open) ||
source.startsWith(Symbol.open_decoded))
@@ -319,7 +313,6 @@
def content: String =
if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)
- else if (kind == Token.Kind.VERBATIM) Scan.Parsers.verbatim_content(source)
else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source)
else if (kind == Token.Kind.INFORMAL_COMMENT) Scan.Parsers.comment_content(source)
else if (kind == Token.Kind.FORMAL_COMMENT) Comment.content(source)
--- a/src/Pure/ML/ml_antiquotations.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Sun Dec 12 11:18:42 2021 +0100
@@ -205,14 +205,14 @@
val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords;
-val parse_name = Parse.input Parse.name;
+val parse_name_args =
+ Parse.input Parse.name -- Scan.repeat Parse.embedded_ml;
-val parse_args = Scan.repeat Parse.embedded_ml_underscore;
-val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) [];
+val parse_for_args =
+ Scan.optional (Parse.$$$ "for" |-- Parse.!!! (Scan.repeat1 Parse.embedded_ml)) [];
fun parse_body b =
- if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single)
- else Scan.succeed [];
+ if b then Parse.$$$ "=>" |-- Parse.!!! (Parse.embedded_ml >> single) else Scan.succeed [];
fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_"
| is_dummy _ = false;
@@ -233,7 +233,7 @@
(fn range => fn src => fn ctxt =>
let
val ((s, type_args), fn_body) = src
- |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_body function);
+ |> Parse.read_embedded_src ctxt keywords (parse_name_args -- parse_body function);
val pos = Input.pos_of s;
val Type (c, Ts) =
@@ -269,7 +269,7 @@
let
val (((s, type_args), term_args), fn_body) = src
|> Parse.read_embedded_src ctxt keywords
- (parse_name -- parse_args -- parse_for_args -- parse_body function);
+ (parse_name_args -- parse_for_args -- parse_body function);
val Const (c, T) =
Proof_Context.read_const {proper = true, strict = true} ctxt
--- a/src/Pure/ML/ml_statistics.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala Sun Dec 12 11:18:42 2021 +0100
@@ -194,7 +194,7 @@
val empty: ML_Statistics = apply(Nil)
def apply(ml_statistics0: List[Properties.T], heading: String = "",
- domain: String => Boolean = (key: String) => true): ML_Statistics =
+ domain: String => Boolean = _ => true): ML_Statistics =
{
require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
@@ -260,6 +260,11 @@
val time_start: Double,
val duration: Double)
{
+ override def toString: String =
+ if (content.isEmpty) "ML_Statistics.empty"
+ else "ML_Statistics(length = " + content.length + ", fields = " + fields.size + ")"
+
+
/* content */
def maximum(field: String): Double =
@@ -286,7 +291,7 @@
def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
{
- data.removeAllSeries
+ data.removeAllSeries()
for (field <- selected_fields) {
val series = new XYSeries(field)
content.foreach(entry => series.add(entry.time, entry.get(field)))
--- a/src/Pure/PIDE/command.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/PIDE/command.ML Sun Dec 12 11:18:42 2021 +0100
@@ -147,14 +147,6 @@
val token_reports = map (reports_of_token keywords) span;
val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
- val verbatim =
- span |> map_filter (fn tok =>
- if Token.kind_of tok = Token.Verbatim then SOME (Token.pos_of tok) else NONE);
- val _ =
- if null verbatim then ()
- else legacy_feature ("Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead" ^
- Position.here_list verbatim);
-
val core_range = Token.core_range_of span;
val tr =
if exists #1 token_reports
--- a/src/Pure/PIDE/markup.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Dec 12 11:18:42 2021 +0100
@@ -433,7 +433,6 @@
val OPERATOR = "operator"
val STRING = "string"
val ALT_STRING = "alt_string"
- val VERBATIM = "verbatim"
val CARTOUCHE = "cartouche"
val COMMENT = "comment"
--- a/src/Pure/PIDE/rendering.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/PIDE/rendering.scala Sun Dec 12 11:18:42 2021 +0100
@@ -117,7 +117,6 @@
Markup.OPERATOR -> Color.operator,
Markup.STRING -> Color.main,
Markup.ALT_STRING -> Color.main,
- Markup.VERBATIM -> Color.main,
Markup.CARTOUCHE -> Color.main,
Markup.LITERAL -> Color.keyword1,
Markup.DELIMITER -> Color.main,
@@ -151,7 +150,6 @@
Map(
Markup.STRING -> Color.quoted,
Markup.ALT_STRING -> Color.quoted,
- Markup.VERBATIM -> Color.quoted,
Markup.CARTOUCHE -> Color.quoted,
Markup.ANTIQUOTED -> Color.antiquoted)
@@ -209,7 +207,7 @@
Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
val language_context_elements =
- Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
+ Markup.Elements(Markup.STRING, Markup.ALT_STRING,
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
--- a/src/Pure/Pure.thy Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Pure.thy Sun Dec 12 11:18:42 2021 +0100
@@ -301,13 +301,13 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>attribute_setup\<close> "define attribute in ML"
(Parse.name_position --
- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
+ Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.embedded "")
>> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>method_setup\<close> "define proof method in ML"
(Parse.name_position --
- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
+ Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.embedded "")
>> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
val _ =
@@ -572,7 +572,7 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>named_theorems\<close>
"declare named collection of theorems"
- (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
+ (Parse.and_list1 (Parse.binding -- Scan.optional Parse.embedded "") >>
fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
in end\<close>
--- a/src/Pure/Thy/bibtex.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Thy/bibtex.ML Sun Dec 12 11:18:42 2021 +0100
@@ -42,8 +42,7 @@
Theory.setup
(Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
Document_Output.antiquotation_raw \<^binding>\<open>cite\<close>
- (Scan.lift
- (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position))
+ (Scan.lift (Scan.option Parse.cartouche -- Parse.and_list1 Args.name_position))
(fn ctxt => fn (opt, citations) =>
let
val _ =
--- a/src/Pure/Thy/document_antiquotations.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Sun Dec 12 11:18:42 2021 +0100
@@ -195,7 +195,7 @@
Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
fun text_antiquotation name =
- Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
+ Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
(fn ctxt => fn text =>
let
val _ = report_text ctxt text;
@@ -206,7 +206,7 @@
end);
val theory_text_antiquotation =
- Document_Output.antiquotation_raw_embedded \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
+ Document_Output.antiquotation_raw_embedded \<^binding>\<open>theory_text\<close> (Scan.lift Parse.embedded_input)
(fn ctxt => fn text =>
let
val keywords = Thy_Header.get_keywords' ctxt;
@@ -273,7 +273,7 @@
(* verbatim text *)
val _ = Theory.setup
- (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
+ (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Parse.embedded_input)
(fn ctxt => fn text =>
let
val pos = Input.pos_of text;
@@ -327,17 +327,17 @@
ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
| test_functor _ = raise Fail "Bad ML functor specification";
-val parse_ml0 = Args.text_input >> (fn source => ("", (source, Input.empty)));
+val parse_ml0 = Parse.embedded_input >> (fn source => ("", (source, Input.empty)));
val parse_ml =
- Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty >> pair "";
+ Parse.embedded_input -- Scan.optional (Args.colon |-- Parse.embedded_input) Input.empty >> pair "";
val parse_exn =
- Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty >> pair "";
+ Parse.embedded_input -- Scan.optional (Args.$$$ "of" |-- Parse.embedded_input) Input.empty >> pair "";
val parse_type =
(Parse.type_args >> (fn [] => "" | [a] => a ^ " " | bs => enclose "(" ") " (commas bs))) --
- (Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty);
+ (Parse.embedded_input -- Scan.optional (Args.$$$ "=" |-- Parse.embedded_input) Input.empty);
fun eval ctxt pos ml =
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos ml
--- a/src/Pure/Thy/document_output.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Thy/document_output.ML Sun Dec 12 11:18:42 2021 +0100
@@ -92,7 +92,7 @@
fun output_block (Markdown.Par lines) =
separate (XML.Text "\n") (map (Latex.block o output_line) lines)
| output_block (Markdown.List {kind, body, ...}) =
- Latex.environment_text (Markdown.print_kind kind) (output_blocks body)
+ Latex.environment (Markdown.print_kind kind) (output_blocks body)
and output_blocks blocks =
separate (XML.Text "\n\n") (map (Latex.block o output_block) blocks);
in
@@ -172,7 +172,6 @@
else output false "" ""
| Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
| Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
- | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
| Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
| Token.Control control => output_body ctxt false "" "" (Antiquote.control_symbols control)
| _ => output false "" "")
--- a/src/Pure/Thy/latex.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Thy/latex.ML Sun Dec 12 11:18:42 2021 +0100
@@ -14,15 +14,12 @@
val macro0: string -> text
val macro: string -> text -> text
val environment: string -> text -> text
- val enclose_text: string -> string -> text -> text
- val output_name: string -> string
val output_ascii: string -> string
val output_ascii_breakable: string -> string -> string
val output_symbols: Symbol.symbol list -> string
val output_syms: string -> string
val symbols: Symbol_Pos.T list -> text
val symbols_output: Symbol_Pos.T list -> text
- val environment_text: string -> text -> text
val isabelle_body: string -> text -> text
val theory_entry: string -> string
type index_item = {text: text, like: string}
@@ -30,9 +27,7 @@
val index_entry: index_entry -> text
val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
val latexN: string
- val latex_output: string -> string * int
val latex_markup: string * Properties.T -> Markup.output
- val latex_indent: string -> int -> string
end;
structure Latex: LATEX =
@@ -57,8 +52,6 @@
fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
-fun enclose_text bg en body = string bg @ body @ string en;
-
(* output name for LaTeX macros *)
@@ -194,13 +187,8 @@
(* theory presentation *)
-fun environment_text name =
- enclose_text
- ("%\n\\begin{" ^ output_name name ^ "}%\n")
- ("%\n\\end{" ^ output_name name ^ "}");
-
fun isabelle_body name =
- enclose_text
+ XML.enclose
("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
"%\n\\end{isabellebody}%\n";
@@ -230,22 +218,29 @@
val latexN = "latex";
+local
+
fun latex_output str =
let val syms = Symbol.explode str
in (output_symbols syms, length_symbols syms) end;
+val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
+val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
+val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
+
+in
+
fun latex_markup (s, _: Properties.T) =
- if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
- then ("\\isacommand{", "}")
- else if s = Markup.keyword2N
- then ("\\isakeyword{", "}")
+ if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup
+ else if s = Markup.keyword2N then keyword_markup
else Markup.no_output;
-fun latex_indent "" _ = ""
- | latex_indent s _ = enclose "\\isaindent{" "}" s;
-
val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
val _ = Markup.add_mode latexN latex_markup;
-val _ = Pretty.add_mode latexN latex_indent;
+
+val _ = Pretty.add_mode latexN
+ (fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s);
end;
+
+end;
--- a/src/Pure/Thy/sessions.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Thy/sessions.ML Sun Dec 12 11:18:42 2021 +0100
@@ -52,7 +52,7 @@
Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
(Parse.$$$ "=" |--
Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
- Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
+ Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) Input.empty --
Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
Scan.optional (Parse.$$$ "sessions" |--
Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
--- a/src/Pure/Thy/thy_header.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Thy/thy_header.ML Sun Dec 12 11:18:42 2021 +0100
@@ -147,7 +147,7 @@
val abbrevs =
Parse.and_list1
- (Scan.repeat1 Parse.text -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.text))
+ (Scan.repeat1 Parse.embedded -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.embedded))
>> uncurry (map_product pair)) >> flat;
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
--- a/src/Pure/Tools/rail.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Tools/rail.ML Sun Dec 12 11:18:42 2021 +0100
@@ -384,10 +384,10 @@
output "" rail' @
Latex.string "\\rail@end\n"
end;
- in Latex.environment_text "railoutput" (maps output_rule rules) end;
+ in Latex.environment "railoutput" (maps output_rule rules) end;
val _ = Theory.setup
- (Document_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
+ (Document_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Parse.embedded_input)
(fn ctxt => output_rules ctxt o read ctxt));
end;
--- a/src/Pure/Tools/update_cartouches.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Tools/update_cartouches.scala Sun Dec 12 11:18:42 2021 +0100
@@ -14,8 +14,6 @@
{
/* update cartouches */
- private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
-
val Text_Antiq: Regex = """(?s)@\{\s*text\b\s*(.+)\}""".r
def update_text(content: String): String =
@@ -46,12 +44,6 @@
(for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
yield {
if (tok.kind == Token.Kind.ALT_STRING) Symbol.cartouche(tok.content)
- else if (tok.kind == Token.Kind.VERBATIM) {
- tok.content match {
- case Verbatim_Body(s) => Symbol.cartouche(s)
- case s => tok.source
- }
- }
else tok.source
}
).mkString
@@ -96,7 +88,7 @@
-t replace @{text} antiquotations within text tokens
Recursively find .thy or ROOT files and update theory syntax to use
- cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
+ cartouches instead of `alt_string` tokens.
Old versions of files are preserved by appending "~~".
""",
--- a/src/Pure/Tools/update_comments.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/Tools/update_comments.scala Sun Dec 12 11:18:42 2021 +0100
@@ -23,7 +23,7 @@
case tok :: rest
if tok.source == "--" || tok.source == Symbol.comment =>
rest.dropWhile(_.is_space) match {
- case tok1 :: rest1 if tok1.is_text =>
+ case tok1 :: rest1 if tok1.is_embedded =>
update(rest1, make_comment(tok1) :: result)
case _ => update(rest, tok.source :: result)
}
--- a/src/Pure/pure_syn.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Pure/pure_syn.ML Sun Dec 12 11:18:42 2021 +0100
@@ -43,7 +43,7 @@
Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
(Parse.opt_target -- Parse.document_source >>
Document_Output.document_output
- {markdown = true, markup = Latex.enclose_text "%\n" "\n"});
+ {markdown = true, markup = XML.enclose "%\n" "\n"});
val _ =
Outer_Syntax.command ("theory", \<^here>) "begin theory"
--- a/src/Tools/Code/code_target.ML Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Tools/Code/code_target.ML Sun Dec 12 11:18:42 2021 +0100
@@ -746,7 +746,7 @@
Outer_Syntax.command \<^command_keyword>\<open>code_printing\<close> "declare dedicated printing for code symbols"
(parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
- (Parse.text -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
+ (Parse.embedded -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
>> (Toplevel.theory o fold set_printings_cmd));
val _ =
--- a/src/Tools/VSCode/extension/README.md Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Tools/VSCode/extension/README.md Sun Dec 12 11:18:42 2021 +0100
@@ -1,14 +1,15 @@
# Isabelle Prover IDE support
This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
-requires Isabelle2021-1.
+requires a suitable repository version of Isabelle.
The implementation is centered around the VSCode Language Server protocol, but
with many add-ons that are specific to VSCode and Isabelle/PIDE.
See also:
- * <https://isabelle.in.tum.de/website-Isabelle2021-1>
+ * <https://isabelle.sketis.net/repos/isabelle/file/tip/src/Tools/VSCode>
+ * <https://github.com/Microsoft/language-server-protocol>
## Screenshot
@@ -57,8 +58,8 @@
### Isabelle/VSCode Installation
- * Download Isabelle2021-1 from <https://isabelle.in.tum.de/website-Isabelle2021-1>
- or any of its mirror sites.
+ * Download a recent Isabelle development snapshot from
+ <https://isabelle.sketis.net/devel/release_snapshot>
* Unpack and run the main Isabelle/jEdit application as usual, to ensure that
the logic image is built properly and Isabelle works as expected.
@@ -88,17 +89,17 @@
+ Linux:
```
- "isabelle.home": "/home/makarius/Isabelle2021-1"
+ "isabelle.home": "/home/makarius/Isabelle"
```
+ Mac OS X:
```
- "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2021-1"
+ "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
```
+ Windows:
```
- "isabelle.home": "C:\\Users\\makarius\\Isabelle2021-1"
+ "isabelle.home": "C:\\Users\\makarius\\Isabelle"
```
* Restart the VSCode application to ensure that all extensions are properly
--- a/src/Tools/VSCode/extension/package.json Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Tools/VSCode/extension/package.json Sun Dec 12 11:18:42 2021 +0100
@@ -1,6 +1,6 @@
{
- "name": "Isabelle2021-1",
- "displayName": "Isabelle2021-1",
+ "name": "Isabelle",
+ "displayName": "Isabelle",
"description": "Isabelle Prover IDE",
"keywords": [
"theorem prover",
--- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Dec 12 10:42:51 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Dec 12 11:18:42 2021 +0100
@@ -70,7 +70,6 @@
Token.Kind.SPACE -> NULL,
Token.Kind.STRING -> LITERAL1,
Token.Kind.ALT_STRING -> LITERAL2,
- Token.Kind.VERBATIM -> COMMENT3,
Token.Kind.CARTOUCHE -> COMMENT3,
Token.Kind.CONTROL -> COMMENT3,
Token.Kind.INFORMAL_COMMENT -> COMMENT1,