Re: [isabelle] Simplifier and linorder transitivity



On 03/07/2013 08:50 PM, Makarius wrote:
> 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.

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







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