*To*: Duncan Higgins <mail at duncan-higgins.co.uk>*Subject*: Re: [isabelle] Using case_tac with functions that have not been exhaustively defined*From*: Makarius <makarius at sketis.net>*Date*: Thu, 24 Jul 2008 15:48:46 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <004d01c8ece1$44c77c20$0200a8c0@HPXW4200>*References*: <004d01c8ece1$44c77c20$0200a8c0@HPXW4200>

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 > 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. 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 "cases" instead - The Isar command 'by' takes two method arguments: an initial method to split up the problem, and an (optional) terminal method to solve the remaining situation. 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) Makarius

**References**:**[isabelle] Using case_tac with functions that have not been exhaustively defined***From:*Duncan Higgins

- Previous by Date: Re: [isabelle] unfold_locales with names for subgoals
- Next by Date: Re: [isabelle] Using case_tac with functions that have not been exhaustively defined
- Previous by Thread: [isabelle] Using case_tac with functions that have not been exhaustively defined
- Next by Thread: Re: [isabelle] Using case_tac with functions that have not been exhaustively defined
- Cl-isabelle-users July 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list