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