Re: [isabelle] Using case_tac with functions that have not been exhaustively defined



On Wed, 23 Jul 2008, Duncan Higgins wrote:

> Suppose I define the following type:
>  
> datatype t = T;
>  
> What I don't understand is that I am able to prove the following lemma using
> case_tac:
>  
> lemma hd_t_list_equals_T : "hd xs = T"
> by ( case_tac "hd xs", simp )
>  
> With this lemma I can then go on to prove things like:
>  
> lemma "hd [] = T"
> by ( simp add : hd_t_list_equals_T )
>  
> As far as I know, this behaviour only occurs with case expressions and
> functions defined using pattern matching, that don't provide an exhaustive
> list of matches, or functions that explicitly use the 'arbitrary' constant
> as a result.

Since datatype t is singleton, every expression of that type is 
mathematically equal to T.  It does not matter how other functions, even 
seemingly ``partial'' ones get involved.


Just two side notes on proofs by cases/simp:

  - case_tac (and any other foo_tac) is only needed when referring 
    implicitly to hidden parameters of the goal state; when eliminating 
    expressions that are visible in the proof text you can use plain 
    "cases" instead

  - The Isar command 'by' takes two method arguments: an initial method to 
    split up the problem, and an (optional) terminal method to solve the 
    remaining situation.

So the canonical Isar one-liner for the above reasoning looks like this:

  lemma "x = T" by (cases x) simp

To solve several goals in the terminal step, methods "simp_all" and "auto" 
are quite handy.  In this particular case, the terminal step is by 
assumption, which is already implicit in the structure of Isar proofs, so 
you can actually write it without the terminal method:

  lemma "x = T" by (cases x)


	Makarius





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