--- a/NEWS Wed Mar 20 17:30:44 2024 +0100
+++ b/NEWS Wed Mar 20 20:45:36 2024 +0100
@@ -42,12 +42,15 @@
. veriT 2021.06.1-rmx - rebuild for arm64-linux
. Z3 4.4.1 for arm64-linux has been removed: unreliable, unstable.
- New implementation of moura tactic. INCOMPATIBILITY.
-
-* Mirabelle: Removed proof reconstruction from "sledgehammer" action;
-the related option "proof_method" was removed. Proof reconstruction is
-supported directly by Sledgehammer and should be used instead. For more
-information, see Sledgehammer's documentation relating to
-"preplay_timeout". INCOMPATIBILITY.
+ - Added support for "order" proof method to proof reconstruction.
+
+* Mirabelle:
+ - Removed proof reconstruction from "sledgehammer" action;
+ the related option "proof_method" was removed. Proof reconstruction is
+ supported directly by Sledgehammer and should be used instead. For
+ more information, see Sledgehammer's documentation relating to
+ "preplay_timeout". INCOMPATIBILITY.
+ - Added the action "order" testing the proof method of the same name.
* Explicit type class for discrete_linear_ordered_semidom for integral
semidomains with a discrete linear order.
@@ -76,7 +79,12 @@
transp_on_image
* Theory "HOL.Transitive_Closure":
+ - Renamed lemma antisymp_on_reflcp to antisymp_on_reflclp.
+ Minor INCOMPATIBILITY.
- Added lemmas.
+ antisym_on_reflcl_if_asym_on
+ antisymp_on_reflclp_if_asymp_on
+ order_reflclp_if_transp_and_asymp
reflclp_greater_eq[simp]
reflclp_less_eq[simp]
relpow_left_unique
--- a/src/HOL/Mirabelle.thy Wed Mar 20 17:30:44 2024 +0100
+++ b/src/HOL/Mirabelle.thy Wed Mar 20 20:45:36 2024 +0100
@@ -19,6 +19,7 @@
\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_order.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_presburger.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_order.ML Wed Mar 20 20:45:36 2024 +0100
@@ -0,0 +1,21 @@
+(* Title: HOL/Tools/Mirabelle/mirabelle_order.ML
+ Author: Martin Desharnais, MPI-INF Saarbrücken
+
+Mirabelle action: "order".
+*)
+
+structure Mirabelle_Order: MIRABELLE_ACTION =
+struct
+
+fun make_action ({timeout, ...} : Mirabelle.action_context) =
+ let
+ val _ = HOL_Order_Tac.tac []
+ fun run ({pre, ...} : Mirabelle.command) =
+ (case Timing.timing (Mirabelle.can_apply timeout (HOL_Order_Tac.tac [])) pre of
+ ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
+ | (_, false) => "failed")
+ in ("", {run = run, finalize = K ""}) end
+
+val () = Mirabelle.register_action "order" make_action
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Mar 20 17:30:44 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Mar 20 20:45:36 2024 +0100
@@ -27,7 +27,8 @@
Moura_Method |
Linarith_Method |
Presburger_Method |
- Algebra_Method
+ Algebra_Method |
+ Order_Method
datatype play_outcome =
Played of Time.time |
@@ -70,7 +71,8 @@
Moura_Method |
Linarith_Method |
Presburger_Method |
- Algebra_Method
+ Algebra_Method |
+ Order_Method
datatype play_outcome =
Played of Time.time |
@@ -112,7 +114,8 @@
| Moura_Method => "moura"
| Linarith_Method => "linarith"
| Presburger_Method => "presburger"
- | Algebra_Method => "algebra")
+ | Algebra_Method => "algebra"
+ | Order_Method => "order")
in
maybe_paren (space_implode " " (meth_s :: ss))
end
@@ -152,7 +155,8 @@
| Moura_Method => moura_tac ctxt
| Linarith_Method => Lin_Arith.tac ctxt
| Presburger_Method => Cooper.tac true [] [] ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt)))
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt
+ | Order_Method => HOL_Order_Tac.tac [] ctxt)))
end
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Mar 20 17:30:44 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Mar 20 20:45:36 2024 +0100
@@ -218,7 +218,7 @@
val misc_methodss =
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method,
- Argo_Method]]
+ Argo_Method, Order_Method]]
val metis_methodss =
[Metis_Method (SOME full_typesN, NONE) ::
--- a/src/HOL/Transitive_Closure.thy Wed Mar 20 17:30:44 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Mar 20 20:45:36 2024 +0100
@@ -79,7 +79,7 @@
lemma antisym_on_reflcl[simp]: "antisym_on A (r\<^sup>=) \<longleftrightarrow> antisym_on A r"
by (simp add: antisym_on_def)
-lemma antisymp_on_reflcp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \<longleftrightarrow> antisymp_on A R"
+lemma antisymp_on_reflclp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \<longleftrightarrow> antisymp_on A R"
by (rule antisym_on_reflcl[to_pred])
lemma trans_on_reflcl[simp]: "trans_on A r \<Longrightarrow> trans_on A (r\<^sup>=)"
@@ -88,6 +88,15 @@
lemma transp_on_reflclp[simp]: "transp_on A R \<Longrightarrow> transp_on A R\<^sup>=\<^sup>="
by (rule trans_on_reflcl[to_pred])
+lemma antisymp_on_reflclp_if_asymp_on:
+ assumes "asymp_on A R"
+ shows "antisymp_on A R\<^sup>=\<^sup>="
+ unfolding antisymp_on_reflclp
+ using antisymp_on_if_asymp_on[OF \<open>asymp_on A R\<close>] .
+
+lemma antisym_on_reflcl_if_asym_on: "asym_on A R \<Longrightarrow> antisym_on A (R\<^sup>=)"
+ using antisymp_on_reflclp_if_asymp_on[to_set] .
+
lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
by blast
@@ -103,6 +112,23 @@
lemma (in preorder) reflclp_greater_eq[simp]: "(\<ge>)\<^sup>=\<^sup>= = (\<ge>)"
using reflp_on_ge by (simp only: reflclp_ident_if_reflp)
+lemma order_reflclp_if_transp_and_asymp:
+ assumes "transp R" and "asymp R"
+ shows "class.order R\<^sup>=\<^sup>= R"
+proof unfold_locales
+ show "\<And>x y. R x y = (R\<^sup>=\<^sup>= x y \<and> \<not> R\<^sup>=\<^sup>= y x)"
+ using \<open>asymp R\<close> asympD by fastforce
+next
+ show "\<And>x. R\<^sup>=\<^sup>= x x"
+ by simp
+next
+ show "\<And>x y z. R\<^sup>=\<^sup>= x y \<Longrightarrow> R\<^sup>=\<^sup>= y z \<Longrightarrow> R\<^sup>=\<^sup>= x z"
+ using transp_on_reflclp[OF \<open>transp R\<close>, THEN transpD] .
+next
+ show "\<And>x y. R\<^sup>=\<^sup>= x y \<Longrightarrow> R\<^sup>=\<^sup>= y x \<Longrightarrow> x = y"
+ using antisymp_on_reflclp_if_asymp_on[OF \<open>asymp R\<close>, THEN antisympD] .
+qed
+
subsection \<open>Reflexive-transitive closure\<close>