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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and