*To*: Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>*Subject*: Re: [isabelle] dest_Trueprop question*From*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Date*: Mon, 19 Jun 2006 09:58:45 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4492F7E2.2060002@cis.upenn.edu>*Organization*: Australian National University*References*: <4492F7E2.2060002@cis.upenn.edu>*User-agent*: Mozilla Thunderbird 0.9 (X11/20041124)

Dimitrios Vytiniotis wrote:

Hello all, I am puzzled over the first issue and need some advice on the second. Second issue (advice) ======================================================= I have a datatype which has only one constructor that takes a pair. Values of this datatype are paired with naturals and contained in a list. I have very often found out that when I do induction on the list to prove a theorem, in the inductive case I often have to do a "by(cases "x", cases "snd x", blast)" which I hate but want to do it in a one-line step because it is a very ``obvious'' fact for the reader of the proof. How do I do this elegantly (e.g with a single tactic like (cases_deep_break "x", auto) or similar) thanks! -d

Dimitrios, I don't know if the following would help, but of the following, case_tac_frees does case_tac for all free variables and case_tac_params does it for all parameters, ie, variables in a subgoal quantified by !! fun case_tacs (str :: strs) sg state = ((case_tac str THEN_ALL_NEW case_tacs strs) sg state handle _ => case_tacs strs sg state) | case_tacs [] sg state = all_tac state ; fun case_tac_frees sg state = let val tm = nth (prems_of state, sg-1) ; fun freename (Free (name, ty)) = name ; in case_tacs (map freename (term_frees tm)) sg state end ; fun case_tac_params sg state = let val tm = nth (prems_of state, sg-1) ; val params = (strip_qnt_vars "all" tm) ; in case_tacs (map fst params) sg state end ; Alternatively you can just construct your own "exhaust" theorem (for example, case_tac "x" where x is a list seems to be equivalent to (res_inst_tac [("y", "x")] list.exhaust)) Regards, Jeremy

**References**:**[isabelle] dest_Trueprop question***From:*Dimitrios Vytiniotis

- Previous by Date: Re: [isabelle] dest_Trueprop question
- Next by Date: Re: [isabelle] dest_Trueprop question
- Previous by Thread: Re: [isabelle] dest_Trueprop question
- Next by Thread: Re: [isabelle] dest_Trueprop question
- Cl-isabelle-users June 2006 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