Email Gateway (Aug 19 2022 at 09:06): Email Gateway (Aug 19 2022 at 09:06):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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" [@{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]
I didn't read much of Orderings.thy. It may be that this is all more
complicated because it depends on parameters which are here unknown. In
that case you could produce a simproc function, or organise some Data
object to store the instantiations as they are created so they can later
be looked up, or similar.
It would be nice if it were easier to follow Brian's advice. This
approach of custom simpsets is the norm in HOL4. Unfortunately in
Isabelle I often find myself missing a name for, say, the
simplifications needed for arithmetic on numeral natural numbers. I have
often ended up working with the giant kludge of writing the simproc
which spots a pattern (e.g. numeral + numeral), simplifies the pattern
with a big unpredictable simpset (e.g. global_simpset_of @{theory Nat})
and then tries to normalise and check (e.g. rewrite Suc 0 -> 1, check we
have a numeral).
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 09:20):From: René Neumann <rene.neumann@in.tum.de>
Hi,
is it possible to automa(t/g)ically instantiate a datatype as linorder,
if it is enough that there exists any order (e.g. the order of the
constructors in the definition with the restriction that all arguments
are of class linorder too)?
Use-case: Insert the datatype into a structure that needs an order on
its members. And if one does not care about the specific order, manually
defining it is quite cumbersome (especially for a large number of
constructors)...
Any hints on (semi-)automatic tools/tricks are highly appreciated :)
Email Gateway (Aug 19 2022 at 09:20):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi René,
René Thiemann has implemented such support, it is available in the Archive of
Formal Proofs: http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml
Best,
Andreas
Email Gateway (Aug 19 2022 at 09:20):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear René
as Andreas already stated, there is such an order generator in the AFP.
However, the tactics in the AFP-Entry for the Isabelle2012 release version
contain some known gaps, so that the generator may fail on some datatypes.
All known gaps have been fixed in the development version of the AFP.
So, if you are working with the development version of Isabelle, just use the development version of the AFP.
If however, you are working with Isabelle2012, then please download a fixed version of the AFP-entry at
http://cl-informatik.uibk.ac.at/software/ceta/Datatype_Order_Generator.tgz
which contains all the fixes of the order generator and works with Isabelle2012.
Best regards,
René
Email Gateway (Aug 19 2022 at 09:20):From: René Neumann <rene.neumann@in.tum.de>
Thanks for that. I didn't think of looking into the AFP to solve my
problem:).
I'm now using the version of the .tgz above and it works \o/.
Is it somehow possible, though, to disable the trace output? There are
thousands of (debug?) lines spit into the trace window whenever I use a
"derive linorder foo"...
Email Gateway (Aug 19 2022 at 09:20):From: Simon Foster <simon.foster@york.ac.uk>
Hi René
The derive linorder works really well, but I've come across an odd example
which doesn't work, namely:
datatype vbasic = BoolI bool | ListI "vbasic list"
derive linorder vbasic
Fails to prove. If I replace the bool with an int or remove the list
constructor, it works fine. There seems to be an odd interaction between
bool and list. The following works fine:
datatype vbasic = TrueI | FalseI | IntI "int" | ListI "vbasic list"
Do you know what's causing this?
Thanks,
-Simon.
Email Gateway (Aug 19 2022 at 09:20):From: René Thiemann <rene.thiemann@uibk.ac.at>
Tracing is now disabled, both in the AFP development version and in the .tgz-version
for Isabelle2012. You can download the new file at the same URL:
http://cl-informatik.uibk.ac.at/software/ceta/Datatype_Order_Generator.tgz
Cheers,
René
Email Gateway (Aug 19 2022 at 09:20):From: René Neumann <rene.neumann@in.tum.de>
Thanks :). Is it (btw) intended that the generated hashfunctions are not
automatically marked as code-equations? At the moment I do:
derive hashable com
lemmas[code] = hashcode_com_def bounded_hashcode_com_def
def_hashmap_size_com_def
Email Gateway (Aug 19 2022 at 09:21):From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi Simon,
The derive linorder works really well,
Thanks.
but I've come across an odd example
which doesn't work, namely:datatype vbasic = BoolI bool | ListI "vbasic list"
derive linorder vbasicFails to prove. If I replace the bool with an int or remove the list
constructor, it works fine. There seems to be an odd interaction between
bool and list. The following works fine:datatype vbasic = TrueI | FalseI | IntI "int" | ListI "vbasic list"
Do you know what's causing this?
I have figured out the problem, which was the simplification rule
"less_bool_def". Please try again by reloading the .tgz or checking out
the latest development version of the AFP, since this rule is explicitly deleted
for simplification in the tactics.
However, I'm not completely sure why this simplification rule was so
harmful. In principle, I had to prove the lemma
vbasic_rec (%x_0. vbasic_case (op < x_0) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) (RecursiveI a) (RecursiveI b) ==>
vbasic_rec (%x_0. vbasic_case (op < x_0) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) a b
which works via the "tactic {* asm_full_simp_tac (simpset_of ctxt) 1 *}".
However, when invoking this tactic within the larger ML tactic,
then it happens that premise gets simplified to
vbasic_rec (%x_0. vbasic_case (op < x_0) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) a b
(as expected), but then the proof goal is simplified further to
vbasic_rec (%x_0. vbasic_case (op & (~ x_0)) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) a b
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 someone else can comment on this?
Cheers,
René
Email Gateway (Aug 19 2022 at 09:22):From: Brian Huffman <huffman.brian.c@gmail.com>
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.
Email Gateway (Aug 19 2022 at 09:22):From: René Thiemann <rene.thiemann@uibk.ac.at>
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é
Last updated: Apr 19 2024 at 08:19 UTC