Email Gateway (Aug 19 2022 at 10:35): Email Gateway (Aug 19 2022 at 10:35):From: Ognjen Maric <ognjen.maric@gmail.com>
Hi,
given the following example
typedecl foo
arities foo :: linorder
lemma
"[| (a :: foo) <= b; b <= c |] ==> P & a <= c & Q"
I would like to simplify the conclusion to "P & Q". For int and nat,
certain arith simprocs produce the desired result, but I can't come up
with a simple way to do it for the (non-arithmetic) type foo. Any
suggestions are of course welcome.
Thanks,
Ognjen
Email Gateway (Aug 19 2022 at 10:36):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Ognjen,
There are a number of so called solvers that know about ordering type classes.
For example, this works:
lemma
"[| (a :: foo) <= b; b <= c; c <= d |] ==> ~ d < a"
apply simp
However, subformulas that are true are not simplified away, only whole
propositions are proved.
Best
Tobias
Email Gateway (Aug 19 2022 at 10:37):From: Ognjen Maric <ognjen.maric@gmail.com>
Dear Tobias,
thanks for the reply. Unfortunately, in my case splitting the goal would
yield too many new ones. I was hoping I wasn't the first one to run into
this and that somebody would have a ready-made solution.
Do you know which solvers exactly are capable of dealing with this?
Also, is there a general way to get such information from the
simplifier? simp_trace didn't seem to be useful here.
Best,
Ognjen
Email Gateway (Aug 19 2022 at 10:40):From: Ognjen Maric <ognjen.maric@gmail.com>
To reply to myself: order_tac from HOL/Orderings.thy does this. In case
anyone else runs into this, here's a solution to my problem, in form of
a simproc:
fun trans_simproc ss (t as (less as Const _) $ _ $ _) = let
val ctxt = Simplifier.the_context ss
val goal = HOLogic.mk_eq (t, @{const "True"})
|> HOLogic.mk_Trueprop
fun is_le_prem thm = (
prop_of thm
|> HOLogic.dest_Trueprop
|> head_of
|> equal less
) handle _ => false
val le_prems = Simplifier.prems_of ss |> filter is_le_prem
val solver = mk_solver "" (fn ss => Orders.order_tac
(Simplifier.the_context ss)
(Simplifier.prems_of ss)
)
val ss' = HOL_ss addSolver solver
|> Simplifier.add_prems le_prems
|> Simplifier.context ctxt
val stac = (asm_full_simp_tac ss' 1)
in
Goal.prove ctxt [] [] goal
(K (CHANGED stac))
|> (fn thm => thm RS @{thm eq_reflection})
|> SOME
handle _ => NONE
end
Email Gateway (Aug 19 2022 at 10:40):From: Makarius <makarius@sketis.net>
Just note that "handle _ => ..." makes the ML program ill-defined, subject
to the laws of phyisics instead of mathematics. See also the explanation
in section 0.5 of the Isabelle/Isar Implementation manual
http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf
After many years of practice, I am conditioned to watch out for such
snags, which is why I've spotted it in your code without looking for
anything in particular.
Makarius
Email Gateway (Aug 19 2022 at 10:40):From: Ognjen Maric <ognjen.maric@gmail.com>
Thanks. Looking at it again, it was also horribly convoluted, one can
just use order_tac directly instead of embedding it as a solver in the
simplifier. This is better:
fun trans_simproc' ss (t as (less as Const _) $ _ $ _) = let
val ctxt = Simplifier.the_context ss
val goal = HOLogic.mk_Trueprop t
fun is_le_prem thm = (
prop_of thm
|> HOLogic.dest_Trueprop
|> head_of
|> equal less
) handle TERM _ => false
val le_prems = Simplifier.prems_of ss |> filter is_le_prem
in
Goal.prove ctxt [] [] goal
((fn {context = ctxt', ...} => Orders.order_tac ctxt'
le_prems 1))
|> (fn thm => thm RS @{thm Eq_TrueI})
|> SOME
handle ERROR _ => NONE
end
Last updated: Apr 26 2024 at 12:28 UTC