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

```This is my first post to the list, so firstly, a big thank you to Larry,
Tobias and everyone else involved for producing such a powerful, useful and
openly available tool.

At the moment, I'm having trouble understanding a particular aspect of
Isabelle's behaviour. I've managed to reduce the problem down to this
trivial example.

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. This behaviour allows me to generate Standard ML code that I
think I have proved to be correct, but which actually results in a Match
exception when run.

I guess what I was expecting to see was something like:

> lemma hd_t_list_equals_T : "hd xs = T";
> apply ( case_tac "hd xs",simp );
proof (prove): step 0

goal (1 subgoal):
1. xs = x # xsa ==> hd xs = T

which would then be unsolvable.

If anyone is able to give me some guidance on this, I'd very much appreciate
it.

Duncan.

```

• Follow-Ups:

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