Email Gateway (Aug 22 2022 at 16:42): Email Gateway (Aug 22 2022 at 16:42):From: Lars Hupel <hupel@in.tum.de>
Dear Josh,
fun poly_mult :: "int list => int list => int list" where
"poly_mult xs [] = []" |
"poly_mult [] xs = []" |
"poly_mult (x#xs) ys = add_lists (scale_list ys x) (0#(poly_mult xs ys))"add_lists ?y [] == ?y
add_lists [] (?v1 # ?va1) == ?v1 # ?va1
add_lists (?x1 # ?xs1) (?y1 # ?ys1) == (?x1 + ?y1) # add_lists ?xs1 ?ys1Why are the second list arguments split into their head and tail in the
second and third rules?
this is a feature of the function package. Isabelle's internal logic
does not have a notion of "top-to-bottom" processing of patterns, as is
usual in e.g. Haskell or Scala. The function package merely pretends
that Isabelle supports that, and internally disambiguates all equations
so that they're valid independently.
In your example, the first and the third equation overlap: Let the first
argument be non-empty and the second empty. Then, both rules would
match. It is not immediately clear whether or not both rules would also
produce the same result, which would be necessary for consistency.
Hence, the function package will helpfully instantiate the last rule so
that it doesn't overlap with the first one anymore, and matches the
expected FP semantics of top-to-bottom processing.
It is possible to prevent the function package from doing that, but I
would highly recommend against that, unless you know what you're doing.
This affects some proofs I am writing where I want to just match the entire second list and not have it split.
I try to get around this by writing additional lemmas stating what I need, but this is sometimes tricky. Is there a simpler way to get the rule I want?
There is a way to transform a set of equations (e.g. the ones that come
out of the function package) into a single equation that performs the
pattern matching on the right-hand side. It can be imported from
"HOL-Library.Simps_Case_Conv". Here's an example use:
case_of_simps map_alt: list.map
thm map_alt
You could then declare the "unwanted" simp rules as [simp del] and that
one as [simp] (be careful, though, sometimes this might make internal
tools loop):
declare list.map[simp del]
declare map_alt[simp]
Cheers
Lars
Last updated: Apr 20 2024 at 12:26 UTC