Re: [isabelle] more beginner questions



On Tuesday 25 September 2007, Tim Newsham wrote:
> at this point I feel like I want to use split_if, but
> apply(split split_if) fails.  I'm not sure if my definition for
> onlyCh is acceptable, but I was able to dispatch part of the
> proof so perhaps it is.  Is my problem due to any of my definitions
> being unsuitable or is there a simple way to continue the current
> proof?   The last goal was:
> 
> !! a list .
>      [| case if a = ch then Some (list, a) else None of None => False
>          | Some (resid, result) => null resid;
>          s = a # list |]
>      ==> a = ch /\ list = []

If-then-else and other case-combinators each have two separate split rules: 
One is for use in the conclusion of a subgoal, and the other is for use with 
the assumptions. For if-then-else, the two split rules are called "split_if" 
and "split_if_asm".

Since your subgoal has an if-then-else in the assumptions, you should use:
apply (split split_if_asm)

The split rules for case expressions have a standard naming scheme based on 
the name of the datatype: For type nat they are "nat.split" 
and "nat.split_asm"; "nat.splits" refers to both. Rules for other datatypes 
are similarly named.

- Brian






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