# HG changeset patch
# User desharna
# Date 1710934012 -3600
# Node ID 7793e3161d2bec551b2513a2a0f0e48a51c06ef3
# Parent  6a3212bedfade5eda7a9a7dc20b43f376aa51056
try proof method "order" in Sledgehammer's proof reconstruction

diff -r 6a3212bedfad -r 7793e3161d2b NEWS
--- a/NEWS	Wed Mar 20 11:55:58 2024 +0100
+++ b/NEWS	Wed Mar 20 12:26:52 2024 +0100
@@ -42,6 +42,7 @@
     . 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.
+  - Added support for "order" proof method to proof reconstruction.
 
 * Mirabelle:
   - Removed proof reconstruction from "sledgehammer" action;
diff -r 6a3212bedfad -r 7793e3161d2b src/HOL/Tools/Mirabelle/mirabelle_order.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_order.ML	Wed Mar 20 12:26:52 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
diff -r 6a3212bedfad -r 7793e3161d2b src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed Mar 20 11:55:58 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed Mar 20 12:26:52 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)
diff -r 6a3212bedfad -r 7793e3161d2b src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Mar 20 11:55:58 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Mar 20 12:26:52 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) ::