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




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