Re: [isabelle] Non-exhaustive pattern-matching in generated code for Set.image
To implement set image for an arbitrary function, I don't see any way other than first
converting the complement representation into an explicit list of the elements. You can
use the type class enum for that. For example:
"distinct ys â set (fold remove1 xs ys) = set ys - set xs"
by(induction xs arbitrary: ys) auto
"List.coset xs = set (fold remove1 xs Enum.enum)"
by(auto simp add: set_fold_remove1 enum_distinct UNIV_enum[symmetric])
lemma image_coset [code]:
"f ` List.coset xs = set (map f (fold remove1 xs Enum.enum))"
by(simp only: coset_enum set_map)
Now image has two code equations, one for set and one for coset. However, you can no
longer use image on sets whose element types are not enumerable, i.e., an instance of the
enum type class.
If you want to have both, then you have to do a bit more work. Basically you must
implement in HOL the type tests that you do manually in Scala. The theory Collection_Enum
in my AFP entry Containers does this and uses it for set comprehensions. There's currently
no setup for set complement, but it would not be hard to do so.
Hope this helps,
On 25/10/17 02:57, Brandon Bohrer wrote:
I'm currently generating code from Isabelle definitions that use " 'a set"
When I run it I get exceptions because the generated code for Set.image
(i.e. f ` set) has a non-exhaustive pattern-match, which is difficult to
avoid for infinite types but in principle should be avoidable for
enumeration types (since the coset constructor is redundant with the set
Does anyone know of a way to code-generate an exhaustive implementation for
Set.image for finite/enumeration types, without implementing my own
finite/cofinite-set data structure from scratch?
If I code-generate to Scala, I can hack the resulting code to be exhaustive
by matching on types at runtime, but (a) I'd rather avoid hacks and (b) I
may want to generate SML instead, where such hacks do not work as well.
I've attached a trivial example that reproduces the exception. The SML file
generated from the Isabelle theory raises Match on start. For good measure,
I've also included an SML file demonstrating the hacky solution.
This archive was generated by a fusion of
Pipermail (Mailman edition) and