The ([^</>]*) Archives

# HG changeset patch # User wenzelm # Date 1639304322 -3600 # Node ID cdd2284c8047054ff24e54bfa66631204d96363d # Parent 70be57333ea1b0e1866be2e944f2e0f70c437ae4# Parent 0dd4dbe7bed387ab84124eac5ad991486698062c merged, resolving conflict in src/Doc/Implementation/Logic.thy; diff -r 70be57333ea1 -r cdd2284c8047 Admin/components/components.sha1 --- 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 diff -r 70be57333ea1 -r cdd2284c8047 CONTRIBUTORS --- 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 ------------------------------- diff -r 70be57333ea1 -r cdd2284c8047 NEWS --- 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 \cartouche\ 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) ------------------------------------- diff -r 70be57333ea1 -r cdd2284c8047 lib/texinputs/isabelle.sty --- 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}}% } diff -r 70be57333ea1 -r cdd2284c8047 src/Doc/Implementation/Logic.thy --- 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>\ @{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} \ 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}+) \ \ diff -r 70be57333ea1 -r cdd2284c8047 src/Doc/Isar_Ref/Outer_Syntax.thy --- 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 \ A chunk of document @{syntax text} is usually given as @{syntax cartouche} - \\\\\ or @{syntax verbatim}, i.e.\ enclosed in \<^verbatim>\{*\~\\\~\<^verbatim>\*}\. For - convenience, any of the smaller text unit that conforms to @{syntax name} is - admitted as well. + \\\\\. For convenience, any of the smaller text unit that conforms to + @{syntax name} is admitted as well. \<^rail>\ - @{syntax_def text}: @{syntax embedded} | @{syntax verbatim} + @{syntax_def text}: @{syntax embedded} \ Typical uses are document markup commands, like \<^theory_text>\chapter\, \<^theory_text>\section\ etc. diff -r 70be57333ea1 -r cdd2284c8047 src/Doc/Tutorial/ToyList/ToyList.thy --- 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} diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/ATP.thy --- 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 \Automatic Theorem Provers (ATPs)\ theory ATP - imports Meson + imports Meson Hilbert_Choice begin subsection \ATP problems and proofs\ @@ -50,6 +50,9 @@ definition fequal :: "'a \ 'a \ bool" where "fequal x y \ (x = y)" +definition fChoice :: "('a \ bool) \ 'a" where + "fChoice \ Hilbert_Choice.Eps" + lemma fTrue_ne_fFalse: "fFalse \ fTrue" unfolding fFalse_def fTrue_def by simp @@ -130,6 +133,16 @@ "fequal x y = fFalse \ fequal (f x) (f y) = fTrue" unfolding fFalse_def fTrue_def fequal_def by auto +lemma fChoice_iff_Ex: "P (fChoice P) \ HOL.Ex P" + unfolding fChoice_def + by (fact some_eq_ex) + +text \ +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 "\x. P x"}, as existentials are not skolimized by the metis proof +method but @{term "Ex P"} is eta-expanded if FOOL is supported.\ subsection \Basic connection between ATPs and HOL\ diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/BNF_Def.thy --- 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 \ P a (pick_middlep P Q a c) \ 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))" diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Bali/Term.thy --- 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 \ \{\tt !} logical complement\ \ \function codes for binary operations\ -datatype binop = Mul \ \{\tt * } multiplication\ +datatype binop = Mul \ \{\tt *} multiplication\ | Div \ \{\tt /} division\ | Mod \ \{\tt \%} remainder\ | Plus \ \{\tt +} addition\ diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Computational_Algebra/Factorial_Ring.thy --- 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 \is_unit x\ 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 \is_unit p\ 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 \ k = 0" proof (rule ccontr) assume "p^k dvd x" and "k \ 0" - with `p = 0` have "p^k = 0" by auto - with `p^k dvd x` have "0 dvd x" by auto + with \p = 0\ have "p^k = 0" by auto + with \p^k dvd x\ have "0 dvd x" by auto hence "x = 0" by auto - with `x \ 0` show False by auto + with \x \ 0\ show False by auto qed ultimately show ?thesis - by (auto simp add: is_unit_power_iff `\ is_unit p`) + by (auto simp add: is_unit_power_iff \\ is_unit p\) next case False - with `x \ 0` `\ is_unit p` show ?thesis + with \x \ 0\ \\ is_unit p\ show ?thesis by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power) qed qed diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Deriv.thy --- 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: "\x. \a < x; x < b\ \ (f has_derivative f' x) (at x)" obtains \ where "a < \" "\ < b" "f b - f a = (f' \) (b - a)" proof - - have "\x. a < x \ x < b \ (\y. f' x y - (f b - f a) / (b - a) * y) = (\v. 0)" + have "\\. a < \ \ \ < b \ (\y. f' \ y - (f b - f a) / (b - a) * y) = (\v. 0)" proof (intro Rolle_deriv[OF \a < b\]) fix x assume x: "a < x" "x < b" @@ -1619,12 +1619,8 @@ has_derivative (\y. f' x y - (f b - f a) / (b - a) * y)) (at x)" by (intro derivative_intros derf[OF x]) qed (use assms in \auto intro!: continuous_intros simp: field_simps\) - then obtain \ where - "a < \" "\ < b" "(\y. f' \ y - (f b - f a) / (b - a) * y) = (\v. 0)" - by metis then show ?thesis - by (metis (no_types, opaque_lifting) that add.right_neutral add_diff_cancel_left' add_diff_eq \a < b\ - less_irrefl nonzero_eq_divide_eq) + by (smt (verit, ccfv_SIG) pos_le_divide_eq pos_less_divide_eq that) qed theorem MVT: diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Eisbach/match_method.ML --- 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>\\\ |-- Parse.token Parse.text)) + Scan.lift (for_fixes -- (\<^keyword>\\\ |-- Parse.token Parse.embedded)) >> (fn ((ctxt, ts), (fixes, body)) => (case Token.get_value body of SOME (Token.Source src) => diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Equiv_Relations.thy --- 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 \ S//?r \ finite C" for C - by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]]) + by (fact finite_equiv_class[OF \finite S\ equiv_type[OF \equiv S ?r\]]) have disjoint: "A \ S//?r \ B \ S//?r \ A \ B \ A \ B = {}" for A B using eqv quotient_disj by blast diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Examples/Rewrite_Examples.thy --- /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 \The rewrite Proof Method by Example\ + +text\ +This theory gives an overview over the features of the pattern-based rewrite proof method. + +Documentation: @{url "https://arxiv.org/abs/2111.04082"} +\ + +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 \ = _" 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 (_ + \) + 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 (\ + _) + _ = _" 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 (_ + \) + _ = _" diff_self) fact + +lemma + fixes x y :: nat + shows"x + y > c \ y + x > c" + by (rewrite at "\ > c" add.commute) assumption + +(* We can also rewrite in the assumptions. *) +lemma + fixes x y :: nat + assumes "y + x > c \ y + x > c" + shows "x + y > c \ y + x > c" + by (rewrite in asm add.commute) fact + +lemma + fixes x y :: nat + assumes "y + x > c \ y + x > c" + shows "x + y > c \ y + x > c" + by (rewrite in "x + y > c" at asm add.commute) fact + +lemma + fixes x y :: nat + assumes "y + x > c \ y + x > c" + shows "x + y > c \ y + x > c" + by (rewrite at "\ > 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. \ }" 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. \ }" add.commute) + fact + +lemma + assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. s * t + y - 3)}" + shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. y + s * t - 3)}" + by (rewrite at "b + d * e" in "$a, b, c). _ = Q (\d e. $" add.commute) fact + +(* This is not limited to the first assumption *) +lemma + assumes "PROP P \ PROP Q" + shows "PROP R \ PROP P \ PROP Q" + by (rewrite at asm assms) + +lemma + assumes "PROP P \ PROP Q" + shows "PROP R \ PROP R \ PROP P \ PROP Q" + by (rewrite at asm assms) + +(* Rewriting "at asm" selects each full assumption, not any parts *) +lemma + assumes "(PROP P \ PROP Q) \ (PROP S \ PROP R)" + shows "PROP S \ (PROP P \ PROP Q) \ 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 \ y \ x \ y \ 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 \ nat" + shows "f x \ 0 \ f x \ 0 \ 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 \ PROP Q \ PROP R \ PROP R'" + assumes A1: "PROP S \ PROP T \ PROP U \ PROP P" + assumes A2: "PROP S \ PROP T \ PROP U \ PROP Q" + assumes C: "PROP S \ PROP R' \ PROP T \ PROP U \ PROP V" + shows "PROP S \ PROP R \ PROP T \ PROP U \ 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 \ nat" where "f n = n" +definition "f_inv (I :: nat \ bool) n \ 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 (\n. f_inv (\_. True) n + 1) = x" + shows "P (\n. f n + 1) = x" + by (rewrite to "f_inv (\_. 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 (\n. f_inv (\x. n < x + 1) n + 1) = x" + shows "P (\n. f n + 1) = x" + by (rewrite in "\n. \" to "f_inv (\x. n < x + 1)" annotate_f) fact + +(* Any identifier will work *) +lemma + assumes "P (\n. f_inv (\x. n < x + 1) n + 1) = x" + shows "P (\n. f n + 1) = x" + by (rewrite in "\abc. \" to "f_inv (\x. abc < x + 1)" annotate_f) fact + +(* The "for" keyword. *) +lemma + assumes "P (2 + 1)" + shows "\x y. P (1 + 2 :: nat)" +by (rewrite in "P (1 + 2)" at for (x) add.commute) fact + +lemma + assumes "\x y. P (y + x)" + shows "\x y. P (x + y :: nat)" +by (rewrite in "P (x + _)" at for (x y) add.commute) fact + +lemma + assumes "\x y z. y + x + z = z + y + (x::int)" + shows "\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 "\x y z. z + (x + y) = z + y + (x::int)" + shows "\x y z. x + y + z = z + y + (x::int)" +by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact + +lemma + assumes "\x y z. x + y + z = y + z + (x::int)" + shows "\x y z. x + y + z = z + y + (x::int)" +by (rewrite at "\ + _" at "_ = \" in for () add.commute) fact + +lemma + assumes eq: "\x. P x \ g x = x" + assumes f1: "\x. Q x \ P x" + assumes f2: "\x. Q x \ x" + shows "\x. Q x \ 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 \-Quantifier. *) +lemma + assumes "($x::int). x < 1 + x)" + and "(x::int) + 1 > x" + shows "(\(x::int). x + 1 > x) \ (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 "\a b. P ((a + 1) * (1 + b)) " + shows "\a b :: nat. P ((a + 1) * (b + 1))" + apply (tactic \ + 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>\nat$], + Rewrite.In, + Rewrite.Term (\<^Const>\plus \<^Type>\nat\ for \Free (x, \<^Type>\nat\)\ \<^term>\1 :: nat\\, [])] + val to = NONE + in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end + \) + apply (fact assms) + done + +lemma + assumes "Q (\b :: int. P (\a. a + b) (\a. a + b))" + shows "Q (\b :: int. P (\a. a + b) (\a. b + a))" + apply (tactic \ + let + val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context> + val pat = [ + Rewrite.Concl, + Rewrite.In, + Rewrite.Term (Free ("Q", (\<^Type>\int\ --> TVar (("'b",0), [])) --> \<^Type>\bool\) + $ Abs ("x", \<^Type>\int\, Rewrite.mk_hole 1 (\<^Type>\int\ --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^Type>\int\)]), + Rewrite.In, + Rewrite.Term (\<^Const>\plus \<^Type>\int\ for \Free (x, \<^Type>\int\)\ \Var (("c", 0), \<^Type>\int\)\\, []) + ] + val to = NONE + in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end + \) + apply (fact assms) + done + +(* There is also conversion-like rewrite function: *) +ML \ + val ct = \<^cprop>\Q (\b :: int. P (\a. a + b) (\a. b + a))\ + val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context> + val pat = [ + Rewrite.Concl, + Rewrite.In, + Rewrite.Term (Free ("Q", (\<^typ>\int\ --> TVar (("'b",0), [])) --> \<^typ>\bool\) + $ Abs ("x", \<^typ>\int\, Rewrite.mk_hole 1 (\<^typ>\int\ --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>\int\)]), + Rewrite.In, + Rewrite.Term (\<^Const>\plus \<^Type>\int\ for \Free (x, \<^Type>\int\)\ \Var (("c", 0), \<^Type>\int\)\\, []) + ] + val to = NONE + val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct +\ + +text \Some regression tests\ + +ML \ + val ct = \<^cterm>$\b :: int. (\a. b + a))\ + val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context> + val pat = [ + Rewrite.In, + Rewrite.Term (\<^Const>\plus \<^Type>\int\ for \Var (("c", 0), \<^Type>\int$\ \Var (("c", 0), \<^Type>\int\)\\, []) + ] + val to = NONE + val _ = + case try (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) ct of + NONE => () + | _ => error "should not have matched anything" +\ + +ML \ + Rewrite.params_pconv (Conv.all_conv |> K |> K) \<^context> (Vartab.empty, []) \<^cterm>\\x. PROP A\ +\ + +lemma + assumes eq: "PROP A \ PROP B \ PROP C" + assumes f1: "PROP D \ PROP A" + assumes f2: "PROP D \ PROP C" + shows "\x. PROP D \ PROP B" + apply (rewrite eq) + apply (fact f1) + apply (fact f2) + done + +end diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Examples/document/root.tex --- 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} diff -r 70be57333ea1 -r cdd2284c8047 src/HOL/Library/Multiset.thy --- 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 \(Finite) Multisets\ theory Multiset -imports Cancellation + imports Cancellation begin subsection \The type of multisets\ @@ -2788,8 +2789,6 @@ subsection \The multiset order\ -subsubsection \Well-foundedness\ - definition mult1 :: "('a \ 'a) set \ ('a multiset \ 'a multiset) set" where "mult1 r = {(N, M). \a M0 K. M = add_mset a M0 \ N = M0 + K \ (\b. b \# K \ (b, a) \ r)}" @@ -2797,6 +2796,9 @@ definition mult :: "('a \ 'a) set \ ('a multiset \ 'a multiset) set" where "mult r = (mult1 r)\<^sup>+" +definition multp :: "('a \ 'a \ bool) \ 'a multiset \ 'a multiset \ bool" where + "multp r M N \ (M, N) \ mult {(x, y). r x y}" + lemma mult1I: assumes "M = add_mset a M0" and "N = M0 + K" and "\b. b \# K \ (b, a) \ r" shows "(N, M) \ mult1 r" @@ -2809,14 +2811,29 @@ lemma mono_mult1: assumes "r \ r'" shows "mult1 r \ mult1 r'" -unfolding mult1_def using assms by blast + unfolding mult1_def using assms by blast lemma mono_mult: assumes "r \ r'" shows "mult r \ 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 \ r' \