Re: [isabelle] Simplifier and linorder transitivity



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


On 03/04/2013 11:04 AM, Ognjen Maric wrote:
> 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
> 
> On 03/01/2013 09:06 PM, Tobias Nipkow wrote:
>> 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
>>
>>
>> Am 01/03/2013 17:25, schrieb Ognjen Maric:
>>> 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
>>>
>>
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.