*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Automatic derivation of a total order on datatypes*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Mon, 19 Nov 2012 12:02:47 +1100*In-reply-to*: <B7544904-069B-40FA-A0E6-9DED404E7D50@uibk.ac.at>*References*: <50A2D9ED.7060406@in.tum.de> <50A343ED.2060501@kit.edu> <48D999C6-55BE-45B4-99BA-62B571846791@uibk.ac.at> <CALOYH0FLfej+JsENGuMjE=Jz8LNqXKUsyxRHyTLZr5QOK3DbHg@mail.gmail.com> <7B83ED65-3252-438E-A9E6-2D1F31241D18@uibk.ac.at> <CAAMXsiYPJkwpXQd2XVtpfLcesY+NC5q674PSSvHjKe+rDjhaxA@mail.gmail.com> <B7544904-069B-40FA-A0E6-9DED404E7D50@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

The add_simprocs mechanism from HOL/Orderings seems to be obscuring things. Normally I would construct and name the simproc objects explicitly, e.g.: val antisym_le_simproc = Simplifier.simproc_global_i @{theory} "antisym le" [ at {term "(x::'a::order) <= y"}] prove_antisym_le (etc) These are later added to the global simpset, e.g.: Simplifier.map_simpset_global (fn ss => ss addsimprocs [antisym_le_simproc]) You can then add the simprocs to custom simpsets any time you want, e.g.: HOL_basic_ss addsimprocs [antisym_le_simproc]

Yours, Thomas. On 16/11/12 23:57, René Thiemann wrote:

So the rule less_bool_def (x< y == ~ x& y) simplifies (op< x_0) to (op& (~ x_0)) in the goal, but not in the premise. This is what I do not understand when calling asm_full_simp_tac.Perhaps the occurrence of "(op< x_0)" in the goal was eta-expanded, while other occurrences were not. You should disable eta-contraction in the pretty-printer to see whether this is the case. My general advice, when writing internal ML tactics, is to use simp_tac only with purpose-built simpsets. Usually I start with HOL_basic_ss and add only the rules I need; I never use the simpset from the current context, as the behavior is just too unpredictable.Hi Brian, thanks for the hints. It is definitely a good idea to use special-purpose simpsets, however, it is not clear to me, how this can be built, since I had difficulties to integrate simprocs, etc. which were essential for the simplication. E.g., in Orderings, add_simprocs [ ("antisym le", ["(x::'a::order)<= y"], prove_antisym_le), ("antisym less", ["~ (x::'a::linorder)< y"], prove_antisym_less) ] is used to add the locally defined "prove_antisym_le"-simproc to the global simpset. It would be nice, if I can just add these simprocs to HOL_basic_ss, however I did not see a way to access them, so that afterwards I can add them via addsimprocs: - using simpset_of @{context} |> dest_ss |> #procs |> List.find (fn a => fst a = "antisym le") delivers an entry, however of type string * cterm list and not string * simproc! - using Simplifier.the_simproc @{context} "antisym le" would deliver a simproc as return type, but one gets an error message: Undefined simproc: "antisym le" - so my current workaround is to use val my_starting_simpset = simpset_of @{context} delsimps (simpset_of @{context} |> dest_ss |> #simps |> map snd) addsimps @{thms HOL.simp_thms} but I think this is not really a nice workaround. Cheers, René

**References**:**[isabelle] Automatic derivation of a total order on datatypes***From:*René Neumann

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*Andreas Lochbihler

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*René Thiemann

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*Simon Foster

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*René Thiemann

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*Brian Huffman

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*René Thiemann

- Previous by Date: Re: [isabelle] Feature wish: Minimal simp/auto invocations
- Next by Date: Re: [isabelle] Highlight sorry in jEdit
- Previous by Thread: Re: [isabelle] Automatic derivation of a total order on datatypes
- Next by Thread: [isabelle] New AFP entry: A Separation Logic Framework for Imperative HOL
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list