Email Gateway (Sep 03 2022 at 14:37): Email Gateway (Sep 03 2022 at 14:37):From: Lawrence Paulson <lp15@cam.ac.uk>
A “new order prover” is an advertised feature of Isabelle2021-1. But I don’t see a hint of documentation. Is there at least a brief description of it somewhere?
Larry
Email Gateway (Sep 06 2022 at 09:54):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Hi Larry,
thanks for reminding me I was meaning to put some documentation into the
NEWS file but forgot about it. I will add it soon. Here is the description.
The new order prover (~~/srcProvers/order_tac.ML) is work by Tobias and
me that replaces the old order prover (~~/src/Provers/order.ML) . It
improves upon the old prover in several ways:
The completeness of the prover is verified in Isabelle (see the ATVA
2021 paper "A Verified Decision Procedure for Orders in Isabelle/HOL").
The new prover is complete for partial orders.
The interface to register new order provers was reworked in order to
reduce boilerplate.
The partial order defined by the order typeclass, for example, can be
registered with the solver as follows:
context order
begin
local_setup ‹
HOL_Order_Tac.declare_order {
ops = {eq = @{term ‹(=) :: 'a ⇒ 'a ⇒ bool›}, le = @{term ‹(≤)›}, lt
= @{term ‹(<)›}},
thms = {trans = @{thm order_trans}, refl = @{thm order_refl}, eqD1
= @{thm eq_refl},
eqD2 = @{thm eq_refl[OF sym]}, antisym = @{thm
order_antisym}, contr = @{thm notE}},
conv_thms = {less_le = @{thm eq_reflection[OF less_le]},
nless_le = @{thm eq_reflection[OF nless_le]}}
}
›
end
The setup function for linear orders is similar. Since the solver
already works with the order and linorder typeclasses, most users won't
need to register new orders but should instantiate the appropriate
typeclass instead.
There are two configuration attributes that modify the behaviour of the
solver:
order_trace (default: False): Enables tracing for the solver that
shows information such as the premises that were passed to the solver.
order_split_limit (default: 8): Limits the number of order literals of
the form ¬ x < y that are passed to the solver since those literals
force the solver to perform case splitting.
Last updated: Apr 16 2024 at 16:19 UTC