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



Hi Duncan,

Duncan Higgins wrote:

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.

I don't see why this behaviour should
be expected. You perform case distinction on "hd xs" which is of type t, then the cases you get should only involve the constructors of type t, i.e. only the case T. Probably you meant to perform case distinction on xs (empty list, or consed list).

The last goal is provable in this case, since any element of type t is HOL-equal to T and hence hd (x#xsa) = x = T.

Amine.





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