Email Gateway (Sep 30 2022 at 10:51): Email Gateway (Sep 30 2022 at 10:51):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
* HOL *
The new prover (src/Provers/order_tac.ML) replaces the old prover
(src/Provers/order.ML) and improves upon the old one 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 orders was reworked to reduce
boilerplate.
The prover has two configuration attributes that control its behaviour:
- order_trace (default: false): Enables tracing for 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 lead to case splitting and thus exponential runtime. This
only applies to partial orders.
The prover is agnostic to the object logic. For HOL, the setup for the
prover is performed in src/HOL/Orderings.thy where the structure
HOL_Order_Tac is obtained. The structure allows us to register new
orders with the functions HOL_Order_Tac.declare_order and
HOL_Order_Tac.declare_linorder. Using these functions, we register the
orders of the type classes order and linorder with the solver. If
possible, one should instantiate these type classes instead of adding
new orders to the solver. One can also interpret the type class locale
as in src/HOL/Library/Sublist.thy, which contains e.g. the prefix
order on lists.
The method order calls the prover in a standalone fashion.
The diagnostic command print_orders shows all orders known to the prover
in the current context.
The last change to the prover itself was made in Isabelle/e6f0c9bf966c.
Cheers,
Lukas
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 30 2022 at 17:58):From: Makarius <makarius@sketis.net>
Just for formal correctness and completeness of NEWS vs. repository vs.
isabelle-dev mailing list, the relevant changesets are as follows:
changeset: 76226:2aad8698f82f
user: Lukas Stevens <mail@lukas-stevens.de>
date: Fri Sep 30 12:41:32 2022 +0200
files: NEWS src/HOL/Orderings.thy
description:
tweaked
changeset: 76227:10945fc183cd
user: Lukas Stevens <mail@lukas-stevens.de>
date: Fri Sep 30 12:44:21 2022 +0200
files: NEWS
description:
added documentation about new order prover
new prover for partial and linear orders by Lukas Stevens and Tobias Nipkow
See NEWS for more context
changeset: 76228:3c46356d241f
user: wenzelm
date: Fri Sep 30 19:26:28 2022 +0200
files: NEWS
description:
restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;
changeset: 76229:6ee5306d143a
tag: tip
user: wenzelm
date: Fri Sep 30 19:42:08 2022 +0200
files: NEWS
description:
more explanations on the new order prover (based on 10945fc183cd), without
violating strict monotonicity of NEWS wrt. official releases;
As usual, I have tried my best to explain the purpose and intention of the
change in the informal log, while making the formal diff as clear as possible.
When studying the history, both the log and the diff together need to explain
what was going in back in time.
The Isabelle Mercurial history serves like a formal proof of the final state
of the sources. It needs to be written with great care, because it is ethernal
and immutable --- nothing can be taken back without causing even greater harm.
We also have general explanations in README_REPOSITORY.
This is not the average Github project with incomprehensible history.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC