Email Gateway (Aug 18 2022 at 19:40): Email Gateway (Aug 18 2022 at 19:40):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Thanks for the tip! I am working with my own datatype, which I am
building up, and this is pretty new for me. Most things are working just
fine now, but I have not read up on what Datatype does to get the cases
and other nice little features yet, so I may have to do that some time in
the future to make working with my own datatype that much easier.
Email Gateway (Aug 18 2022 at 19:40):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Your examples help a lot. Thank you!
Email Gateway (Aug 18 2022 at 20:05):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Hey all:
I am now at the point where I need to start understanding a bit more
about cases and how to work with case statements. In particular, I have
read about this thing called split, and it sort of makes senses, but I
have not been able to use it very well. In some specific cases I have
been able to use the cases method quite well. Here is a simple one that
kind of has me stumped though, how do I show this?
(case X of Blah x y => f x y)
= f (case X of Blah x y => x) (case X of Blah x y => y)
I guess that I am not sure how cases work under the hood, so I am not
sure how I would go about handling this, as splitting twice does not seem
to quite work the way that I want.
Email Gateway (Aug 18 2022 at 20:06):From: Peter Gammie <peteg42@gmail.com>
Aaron,
If you have manifest case combinators (as you do here) then you can use the split rules that are created for the datatype.
datatype Blah = Blah nat nat
print_theorems
lemma "(case X of Blah x y \<Rightarrow> f x y) = f (case X of Blah x y \<Rightarrow> x) (case X of Blah x y \<Rightarrow> y)"
by (cases X) simp
lemma "(case X of Blah x y \<Rightarrow> f x y) = f (case X of Blah x y \<Rightarrow> x) (case X of Blah x y \<Rightarrow> y)"
by (simp split: Blah.splits)
This is covered in the (old?) Isabelle Tutorial, though I did find it opaque until I realised how the syntax for case was implemented. It pays to re-read that section on splitting as your understanding of other parts of the system deepens.
Take a look at the output of print_theorems to see what wonderful things datatype gives you for free.
cheers
peter
Email Gateway (Aug 18 2022 at 20:07):From: Makarius <makarius@sketis.net>
Just to understand the notation, you can use this in Isabelle2012 (e.g.
RC2) to disable the heavy sugar coating:
declare [[show_cases = false]]
Makarius
Last updated: Apr 18 2024 at 16:19 UTC