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
> 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
- The Isar command 'by' takes two method arguments: an initial method to
split up the problem, and an (optional) terminal method to solve the
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and