Re: [isabelle] Dealing with Cases



Aaron,

On 08/05/2012, at 8:26 AM, Aaron W. Hsu wrote:

> 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. 

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

-- 
http://peteg.org/






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.